[STATEMENT]
lemma chain_reparam_chain'_pathimg_subset':
  assumes "chain_reparam_chain' one_chain subdiv"
  assumes "(k,\<gamma>)\<in> subdiv"
  shows " \<exists>k' \<gamma>'. (k',\<gamma>')\<in> one_chain \<and> path_image \<gamma> \<subseteq> path_image \<gamma>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k' \<gamma>'. (k', \<gamma>') \<in> one_chain \<and> path_image \<gamma> \<subseteq> path_image \<gamma>'
[PROOF STEP]
using assms chain_reparam_weak_path_pathimg_subset
[PROOF STATE]
proof (prove)
using this:
chain_reparam_chain' one_chain subdiv
(k, \<gamma>) \<in> subdiv
chain_reparam_weak_path ?\<gamma> ?subdiv \<Longrightarrow> \<forall>(k', \<gamma>')\<in>?subdiv. path_image \<gamma>' \<subseteq> path_image ?\<gamma>

goal (1 subgoal):
 1. \<exists>k' \<gamma>'. (k', \<gamma>') \<in> one_chain \<and> path_image \<gamma> \<subseteq> path_image \<gamma>'
[PROOF STEP]
apply(auto simp add: chain_reparam_chain'_def set_eq_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f. \<lbrakk>(k, \<gamma>) \<in> subdiv; \<And>\<gamma> subdiv. chain_reparam_weak_path \<gamma> subdiv \<Longrightarrow> \<forall>x\<in>subdiv. case x of (k', \<gamma>') \<Rightarrow> path_image \<gamma>' \<subseteq> path_image \<gamma>; \<forall>a b. (\<exists>x\<in>one_chain. (a, b) \<in> f x) = ((a, b) \<in> subdiv); \<forall>cube\<in>one_chain. chain_reparam_weak_path (coeff_cube_to_path cube) (f cube); \<forall>p\<in>one_chain. \<forall>p'\<in>one_chain. p \<noteq> p' \<longrightarrow> (\<forall>a b. (a, b) \<in> f p \<longrightarrow> (a, b) \<notin> f p'); \<forall>x\<in>one_chain. finite (f x)\<rbrakk> \<Longrightarrow> \<exists>k' \<gamma>'. (k', \<gamma>') \<in> one_chain \<and> path_image \<gamma> \<subseteq> path_image \<gamma>'
[PROOF STEP]
using  path_image_reversepath case_prodE case_prodD old.prod.exhaust
[PROOF STATE]
proof (prove)
using this:
path_image (reversepath ?g) = path_image ?g
\<lbrakk>case ?p of (a, b) \<Rightarrow> ?c a b; \<And>x y. \<lbrakk>?p = (x, y); ?c x y\<rbrakk> \<Longrightarrow> ?Q\<rbrakk> \<Longrightarrow> ?Q
case (?a, ?b) of (c, d) \<Rightarrow> ?f c d \<Longrightarrow> ?f ?a ?b
(\<And>a b. ?y = (a, b) \<Longrightarrow> ?P) \<Longrightarrow> ?P

goal (1 subgoal):
 1. \<And>f. \<lbrakk>(k, \<gamma>) \<in> subdiv; \<And>\<gamma> subdiv. chain_reparam_weak_path \<gamma> subdiv \<Longrightarrow> \<forall>x\<in>subdiv. case x of (k', \<gamma>') \<Rightarrow> path_image \<gamma>' \<subseteq> path_image \<gamma>; \<forall>a b. (\<exists>x\<in>one_chain. (a, b) \<in> f x) = ((a, b) \<in> subdiv); \<forall>cube\<in>one_chain. chain_reparam_weak_path (coeff_cube_to_path cube) (f cube); \<forall>p\<in>one_chain. \<forall>p'\<in>one_chain. p \<noteq> p' \<longrightarrow> (\<forall>a b. (a, b) \<in> f p \<longrightarrow> (a, b) \<notin> f p'); \<forall>x\<in>one_chain. finite (f x)\<rbrakk> \<Longrightarrow> \<exists>k' \<gamma>'. (k', \<gamma>') \<in> one_chain \<and> path_image \<gamma> \<subseteq> path_image \<gamma>'
[PROOF STEP]
apply (simp add: list.distinct(1) list.inject rec_join.elims)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f. \<lbrakk>(k, \<gamma>) \<in> subdiv; \<And>\<gamma> subdiv. chain_reparam_weak_path \<gamma> subdiv \<Longrightarrow> \<forall>x\<in>subdiv. case x of (k', \<gamma>') \<Rightarrow> path_image \<gamma>' \<subseteq> path_image \<gamma>; \<forall>a b. (\<exists>x\<in>one_chain. (a, b) \<in> f x) = ((a, b) \<in> subdiv); \<forall>cube\<in>one_chain. chain_reparam_weak_path (coeff_cube_to_path cube) (f cube); \<forall>p\<in>one_chain. \<forall>p'\<in>one_chain. p \<noteq> p' \<longrightarrow> (\<forall>a b. (a, b) \<in> f p \<longrightarrow> (a, b) \<notin> f p'); \<forall>x\<in>one_chain. finite (f x); \<And>c p Q. \<lbrakk>case p of (x, xa) \<Rightarrow> c x xa; \<And>x y. \<lbrakk>p = (x, y); c x y\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q; \<And>f a b. f a b \<Longrightarrow> f a b; \<And>y P. (\<And>a b. y = (a, b) \<Longrightarrow> P) \<Longrightarrow> P\<rbrakk> \<Longrightarrow> \<exists>k' \<gamma>'. (k', \<gamma>') \<in> one_chain \<and> path_image \<gamma> \<subseteq> path_image \<gamma>'
[PROOF STEP]
by (smt case_prodD coeff_cube_to_path.simps rec_join.simps(2) reversepath_simps(2) surj_pair)


[STATEMENT]
lemma common_reparam_exists_imp_eq_line_integral:
  assumes finite_basis: "finite basis" and
    "finite one_chain1"
    "finite one_chain2"
    "boundary_chain (one_chain1::(int \<times> (real \<Rightarrow> real \<times> real)) set)"
    "boundary_chain (one_chain2::(int \<times> (real \<Rightarrow> real \<times> real)) set)"
    " \<forall>(k2, \<gamma>2)\<in>one_chain2. \<forall>b\<in>basis. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)"
    "(common_reparam_exists one_chain1 one_chain2)"
    "(\<forall>(k, \<gamma>)\<in>one_chain1.  valid_path \<gamma>)"
    "(\<forall>(k, \<gamma>)\<in>one_chain2.  valid_path \<gamma>)"
  shows "one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2"
    "\<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2 &&& \<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2
 2. \<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>
[PROOF STEP]
obtain subdiv ps1 ps2 where props:
    "chain_reparam_chain' (one_chain1 - ps1) subdiv"
    "chain_reparam_chain' (one_chain2 - ps2) subdiv "
    "(\<forall>(k, \<gamma>)\<in>subdiv.  \<gamma> C1_differentiable_on {0..1})"
    "boundary_chain subdiv"
    "(\<forall>(k, \<gamma>)\<in>ps1. point_path \<gamma>)"
    "(\<forall>(k, \<gamma>)\<in>ps2. point_path \<gamma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ps1 subdiv ps2. \<lbrakk>chain_reparam_chain' (one_chain1 - ps1) subdiv; chain_reparam_chain' (one_chain2 - ps2) subdiv; \<forall>(k, \<gamma>)\<in>subdiv. \<gamma> C1_differentiable_on {0..1}; boundary_chain subdiv; \<forall>(k, \<gamma>)\<in>ps1. point_path \<gamma>; \<forall>(k, \<gamma>)\<in>ps2. point_path \<gamma>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite basis
finite one_chain1
finite one_chain2
boundary_chain one_chain1
boundary_chain one_chain2
\<forall>(k2, \<gamma>2)\<in>one_chain2. \<forall>b\<in>basis. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)
common_reparam_exists one_chain1 one_chain2
\<forall>(k, \<gamma>)\<in>one_chain1. valid_path \<gamma>
\<forall>(k, \<gamma>)\<in>one_chain2. valid_path \<gamma>

goal (1 subgoal):
 1. (\<And>ps1 subdiv ps2. \<lbrakk>chain_reparam_chain' (one_chain1 - ps1) subdiv; chain_reparam_chain' (one_chain2 - ps2) subdiv; \<forall>(k, \<gamma>)\<in>subdiv. \<gamma> C1_differentiable_on {0..1}; boundary_chain subdiv; \<forall>(k, \<gamma>)\<in>ps1. point_path \<gamma>; \<forall>(k, \<gamma>)\<in>ps2. point_path \<gamma>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: common_reparam_exists_def)
[PROOF STATE]
proof (state)
this:
chain_reparam_chain' (one_chain1 - ps1) subdiv
chain_reparam_chain' (one_chain2 - ps2) subdiv
\<forall>(k, \<gamma>)\<in>subdiv. \<gamma> C1_differentiable_on {0..1}
boundary_chain subdiv
\<forall>(k, \<gamma>)\<in>ps1. point_path \<gamma>
\<forall>(k, \<gamma>)\<in>ps2. point_path \<gamma>

goal (2 subgoals):
 1. one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2
 2. \<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>
[PROOF STEP]
have subdiv_valid: "(\<forall>(k, \<gamma>)\<in>subdiv.  valid_path \<gamma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>(k, \<gamma>)\<in>subdiv. valid_path \<gamma>
[PROOF STEP]
apply(simp add: valid_path_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>subdiv. case x of (k, \<gamma>) \<Rightarrow> \<gamma> piecewise_C1_differentiable_on {0..1}
[PROOF STEP]
using props(3)
[PROOF STATE]
proof (prove)
using this:
\<forall>(k, \<gamma>)\<in>subdiv. \<gamma> C1_differentiable_on {0..1}

goal (1 subgoal):
 1. \<forall>x\<in>subdiv. case x of (k, \<gamma>) \<Rightarrow> \<gamma> piecewise_C1_differentiable_on {0..1}
[PROOF STEP]
using C1_differentiable_imp_piecewise
[PROOF STATE]
proof (prove)
using this:
\<forall>(k, \<gamma>)\<in>subdiv. \<gamma> C1_differentiable_on {0..1}
?f C1_differentiable_on ?S \<Longrightarrow> ?f piecewise_C1_differentiable_on ?S

goal (1 subgoal):
 1. \<forall>x\<in>subdiv. case x of (k, \<gamma>) \<Rightarrow> \<gamma> piecewise_C1_differentiable_on {0..1}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>(k, \<gamma>)\<in>subdiv. valid_path \<gamma>

goal (2 subgoals):
 1. one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2
 2. \<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>
[PROOF STEP]
have onechain_boundary1: "boundary_chain (one_chain1 - ps1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. boundary_chain (one_chain1 - ps1)
[PROOF STEP]
using assms(4)
[PROOF STATE]
proof (prove)
using this:
boundary_chain one_chain1

goal (1 subgoal):
 1. boundary_chain (one_chain1 - ps1)
[PROOF STEP]
by (auto simp add: boundary_chain_def)
[PROOF STATE]
proof (state)
this:
boundary_chain (one_chain1 - ps1)

goal (2 subgoals):
 1. one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2
 2. \<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>
[PROOF STEP]
have onechain_boundary2: "boundary_chain (one_chain2 - ps1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. boundary_chain (one_chain2 - ps1)
[PROOF STEP]
using assms(5)
[PROOF STATE]
proof (prove)
using this:
boundary_chain one_chain2

goal (1 subgoal):
 1. boundary_chain (one_chain2 - ps1)
[PROOF STEP]
by (auto simp add: boundary_chain_def)
[PROOF STATE]
proof (state)
this:
boundary_chain (one_chain2 - ps1)

goal (2 subgoals):
 1. one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2
 2. \<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
boundary_chain (one_chain2 - ps1)

goal (2 subgoals):
 1. one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2
 2. \<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>
[PROOF STEP]
fix k2 \<gamma>2 b
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2
 2. \<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>
[PROOF STEP]
assume ass: "(k2, \<gamma>2)\<in>subdiv "" b\<in>basis"
[PROOF STATE]
proof (state)
this:
(k2, \<gamma>2) \<in> subdiv
b \<in> basis

goal (2 subgoals):
 1. one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2
 2. \<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>
[PROOF STEP]
have "\<And> k \<gamma>. (k, \<gamma>) \<in> subdiv \<Longrightarrow> \<exists>k' \<gamma>'. (k', \<gamma>') \<in> one_chain2 \<and> path_image \<gamma> \<subseteq> path_image \<gamma>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k \<gamma>. (k, \<gamma>) \<in> subdiv \<Longrightarrow> \<exists>k' \<gamma>'. (k', \<gamma>') \<in> one_chain2 \<and> path_image \<gamma> \<subseteq> path_image \<gamma>'
[PROOF STEP]
by (meson chain_reparam_chain'_pathimg_subset' props Diff_subset subsetCE)
[PROOF STATE]
proof (state)
this:
(?k, ?\<gamma>) \<in> subdiv \<Longrightarrow> \<exists>k' \<gamma>'. (k', \<gamma>') \<in> one_chain2 \<and> path_image ?\<gamma> \<subseteq> path_image \<gamma>'

goal (2 subgoals):
 1. one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2
 2. \<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(?k, ?\<gamma>) \<in> subdiv \<Longrightarrow> \<exists>k' \<gamma>'. (k', \<gamma>') \<in> one_chain2 \<and> path_image ?\<gamma> \<subseteq> path_image \<gamma>'
[PROOF STEP]
have "continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)"
[PROOF STATE]
proof (prove)
using this:
(?k, ?\<gamma>) \<in> subdiv \<Longrightarrow> \<exists>k' \<gamma>'. (k', \<gamma>') \<in> one_chain2 \<and> path_image ?\<gamma> \<subseteq> path_image \<gamma>'

goal (1 subgoal):
 1. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)
[PROOF STEP]
using assms(6) continuous_on_subset[where ?f = " (\<lambda>x. F x \<bullet> b)"] ass
[PROOF STATE]
proof (prove)
using this:
(?k, ?\<gamma>) \<in> subdiv \<Longrightarrow> \<exists>k' \<gamma>'. (k', \<gamma>') \<in> one_chain2 \<and> path_image ?\<gamma> \<subseteq> path_image \<gamma>'
\<forall>(k2, \<gamma>2)\<in>one_chain2. \<forall>b\<in>basis. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)
\<lbrakk>continuous_on ?s (\<lambda>x. F x \<bullet> b); ?t \<subseteq> ?s\<rbrakk> \<Longrightarrow> continuous_on ?t (\<lambda>x. F x \<bullet> b)
(k2, \<gamma>2) \<in> subdiv
b \<in> basis

goal (1 subgoal):
 1. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)
[PROOF STEP]
apply(auto simp add:  subset_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>k \<gamma>. (k, \<gamma>) \<in> subdiv \<Longrightarrow> \<exists>k' \<gamma>'. (k', \<gamma>') \<in> one_chain2 \<and> (\<forall>a b. (a, b) \<in> path_image \<gamma> \<longrightarrow> (a, b) \<in> path_image \<gamma>'); \<forall>x\<in>one_chain2. case x of (k2, \<gamma>2) \<Rightarrow> \<forall>b\<in>basis. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b); \<And>s t. \<lbrakk>continuous_on s (\<lambda>x. F x \<bullet> b); \<forall>a b. (a, b) \<in> t \<longrightarrow> (a, b) \<in> s\<rbrakk> \<Longrightarrow> continuous_on t (\<lambda>x. F x \<bullet> b); (k2, \<gamma>2) \<in> subdiv; b \<in> basis\<rbrakk> \<Longrightarrow> continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)
[PROOF STEP]
by (metis (mono_tags, lifting) case_prodD)
[PROOF STATE]
proof (state)
this:
continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)

goal (2 subgoals):
 1. one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2
 2. \<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?k2.2, ?\<gamma>2.2) \<in> subdiv; ?b2 \<in> basis\<rbrakk> \<Longrightarrow> continuous_on (path_image ?\<gamma>2.2) (\<lambda>x. F x \<bullet> ?b2)

goal (2 subgoals):
 1. one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2
 2. \<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>(?k2.2, ?\<gamma>2.2) \<in> subdiv; ?b2 \<in> basis\<rbrakk> \<Longrightarrow> continuous_on (path_image ?\<gamma>2.2) (\<lambda>x. F x \<bullet> ?b2)
[PROOF STEP]
have cont_field: "\<forall>b\<in>basis. \<forall>(k2, \<gamma>2)\<in>subdiv. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?k2.2, ?\<gamma>2.2) \<in> subdiv; ?b2 \<in> basis\<rbrakk> \<Longrightarrow> continuous_on (path_image ?\<gamma>2.2) (\<lambda>x. F x \<bullet> ?b2)

goal (1 subgoal):
 1. \<forall>b\<in>basis. \<forall>(k2, \<gamma>2)\<in>subdiv. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>b\<in>basis. \<forall>(k2, \<gamma>2)\<in>subdiv. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)

goal (2 subgoals):
 1. one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2
 2. \<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>
[PROOF STEP]
have one_chain1_ps_valid: "(\<forall>(k, \<gamma>)\<in>one_chain1 - ps1.  valid_path \<gamma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>(k, \<gamma>)\<in>one_chain1 - ps1. valid_path \<gamma>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite basis
finite one_chain1
finite one_chain2
boundary_chain one_chain1
boundary_chain one_chain2
\<forall>(k2, \<gamma>2)\<in>one_chain2. \<forall>b\<in>basis. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)
common_reparam_exists one_chain1 one_chain2
\<forall>(k, \<gamma>)\<in>one_chain1. valid_path \<gamma>
\<forall>(k, \<gamma>)\<in>one_chain2. valid_path \<gamma>

goal (1 subgoal):
 1. \<forall>(k, \<gamma>)\<in>one_chain1 - ps1. valid_path \<gamma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>(k, \<gamma>)\<in>one_chain1 - ps1. valid_path \<gamma>

goal (2 subgoals):
 1. one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2
 2. \<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>
[PROOF STEP]
have one_chain2_ps_valid: "(\<forall>(k, \<gamma>)\<in>one_chain2 - ps1.  valid_path \<gamma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>(k, \<gamma>)\<in>one_chain2 - ps1. valid_path \<gamma>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite basis
finite one_chain1
finite one_chain2
boundary_chain one_chain1
boundary_chain one_chain2
\<forall>(k2, \<gamma>2)\<in>one_chain2. \<forall>b\<in>basis. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)
common_reparam_exists one_chain1 one_chain2
\<forall>(k, \<gamma>)\<in>one_chain1. valid_path \<gamma>
\<forall>(k, \<gamma>)\<in>one_chain2. valid_path \<gamma>

goal (1 subgoal):
 1. \<forall>(k, \<gamma>)\<in>one_chain2 - ps1. valid_path \<gamma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>(k, \<gamma>)\<in>one_chain2 - ps1. valid_path \<gamma>

goal (2 subgoals):
 1. one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2
 2. \<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>
[PROOF STEP]
have 0: "one_chain_line_integral F basis (one_chain1 - ps1) = one_chain_line_integral F basis subdiv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. one_chain_line_integral F basis (one_chain1 - ps1) = one_chain_line_integral F basis subdiv
[PROOF STEP]
apply(rule chain_reparam_chain'_line_integral_smooth_cubes[OF props(1) props(3) cont_field finite_basis])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. finite (one_chain1 - ps1)
 2. boundary_chain (one_chain1 - ps1)
 3. boundary_chain subdiv
 4. \<forall>(k, \<gamma>)\<in>one_chain1 - ps1. valid_path \<gamma>
[PROOF STEP]
using props assms
[PROOF STATE]
proof (prove)
using this:
chain_reparam_chain' (one_chain1 - ps1) subdiv
chain_reparam_chain' (one_chain2 - ps2) subdiv
\<forall>(k, \<gamma>)\<in>subdiv. \<gamma> C1_differentiable_on {0..1}
boundary_chain subdiv
\<forall>(k, \<gamma>)\<in>ps1. point_path \<gamma>
\<forall>(k, \<gamma>)\<in>ps2. point_path \<gamma>
finite basis
finite one_chain1
finite one_chain2
boundary_chain one_chain1
boundary_chain one_chain2
\<forall>(k2, \<gamma>2)\<in>one_chain2. \<forall>b\<in>basis. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)
common_reparam_exists one_chain1 one_chain2
\<forall>(k, \<gamma>)\<in>one_chain1. valid_path \<gamma>
\<forall>(k, \<gamma>)\<in>one_chain2. valid_path \<gamma>

goal (4 subgoals):
 1. finite (one_chain1 - ps1)
 2. boundary_chain (one_chain1 - ps1)
 3. boundary_chain subdiv
 4. \<forall>(k, \<gamma>)\<in>one_chain1 - ps1. valid_path \<gamma>
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. boundary_chain (one_chain1 - ps1)
 2. boundary_chain subdiv
 3. \<forall>(k, \<gamma>)\<in>one_chain1 - ps1. valid_path \<gamma>
[PROOF STEP]
using props assms
[PROOF STATE]
proof (prove)
using this:
chain_reparam_chain' (one_chain1 - ps1) subdiv
chain_reparam_chain' (one_chain2 - ps2) subdiv
\<forall>(k, \<gamma>)\<in>subdiv. \<gamma> C1_differentiable_on {0..1}
boundary_chain subdiv
\<forall>(k, \<gamma>)\<in>ps1. point_path \<gamma>
\<forall>(k, \<gamma>)\<in>ps2. point_path \<gamma>
finite basis
finite one_chain1
finite one_chain2
boundary_chain one_chain1
boundary_chain one_chain2
\<forall>(k2, \<gamma>2)\<in>one_chain2. \<forall>b\<in>basis. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)
common_reparam_exists one_chain1 one_chain2
\<forall>(k, \<gamma>)\<in>one_chain1. valid_path \<gamma>
\<forall>(k, \<gamma>)\<in>one_chain2. valid_path \<gamma>

goal (3 subgoals):
 1. boundary_chain (one_chain1 - ps1)
 2. boundary_chain subdiv
 3. \<forall>(k, \<gamma>)\<in>one_chain1 - ps1. valid_path \<gamma>
[PROOF STEP]
using onechain_boundary1
[PROOF STATE]
proof (prove)
using this:
chain_reparam_chain' (one_chain1 - ps1) subdiv
chain_reparam_chain' (one_chain2 - ps2) subdiv
\<forall>(k, \<gamma>)\<in>subdiv. \<gamma> C1_differentiable_on {0..1}
boundary_chain subdiv
\<forall>(k, \<gamma>)\<in>ps1. point_path \<gamma>
\<forall>(k, \<gamma>)\<in>ps2. point_path \<gamma>
finite basis
finite one_chain1
finite one_chain2
boundary_chain one_chain1
boundary_chain one_chain2
\<forall>(k2, \<gamma>2)\<in>one_chain2. \<forall>b\<in>basis. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)
common_reparam_exists one_chain1 one_chain2
\<forall>(k, \<gamma>)\<in>one_chain1. valid_path \<gamma>
\<forall>(k, \<gamma>)\<in>one_chain2. valid_path \<gamma>
boundary_chain (one_chain1 - ps1)

goal (3 subgoals):
 1. boundary_chain (one_chain1 - ps1)
 2. boundary_chain subdiv
 3. \<forall>(k, \<gamma>)\<in>one_chain1 - ps1. valid_path \<gamma>
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. boundary_chain subdiv
 2. \<forall>(k, \<gamma>)\<in>one_chain1 - ps1. valid_path \<gamma>
[PROOF STEP]
using props assms
[PROOF STATE]
proof (prove)
using this:
chain_reparam_chain' (one_chain1 - ps1) subdiv
chain_reparam_chain' (one_chain2 - ps2) subdiv
\<forall>(k, \<gamma>)\<in>subdiv. \<gamma> C1_differentiable_on {0..1}
boundary_chain subdiv
\<forall>(k, \<gamma>)\<in>ps1. point_path \<gamma>
\<forall>(k, \<gamma>)\<in>ps2. point_path \<gamma>
finite basis
finite one_chain1
finite one_chain2
boundary_chain one_chain1
boundary_chain one_chain2
\<forall>(k2, \<gamma>2)\<in>one_chain2. \<forall>b\<in>basis. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)
common_reparam_exists one_chain1 one_chain2
\<forall>(k, \<gamma>)\<in>one_chain1. valid_path \<gamma>
\<forall>(k, \<gamma>)\<in>one_chain2. valid_path \<gamma>

goal (2 subgoals):
 1. boundary_chain subdiv
 2. \<forall>(k, \<gamma>)\<in>one_chain1 - ps1. valid_path \<gamma>
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>(k, \<gamma>)\<in>one_chain1 - ps1. valid_path \<gamma>
[PROOF STEP]
using one_chain1_ps_valid
[PROOF STATE]
proof (prove)
using this:
\<forall>(k, \<gamma>)\<in>one_chain1 - ps1. valid_path \<gamma>

goal (1 subgoal):
 1. \<forall>(k, \<gamma>)\<in>one_chain1 - ps1. valid_path \<gamma>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
one_chain_line_integral F basis (one_chain1 - ps1) = one_chain_line_integral F basis subdiv

goal (2 subgoals):
 1. one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2
 2. \<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>
[PROOF STEP]
have 1:"\<forall>(k, \<gamma>)\<in>(one_chain1 - ps1). line_integral_exists F basis \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>(k, \<gamma>)\<in>one_chain1 - ps1. line_integral_exists F basis \<gamma>
[PROOF STEP]
apply(rule chain_reparam_chain'_line_integral_smooth_cubes[OF props(1) props(3) cont_field finite_basis])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. finite (one_chain1 - ps1)
 2. boundary_chain (one_chain1 - ps1)
 3. boundary_chain subdiv
 4. \<forall>(k, \<gamma>)\<in>one_chain1 - ps1. valid_path \<gamma>
[PROOF STEP]
using props assms
[PROOF STATE]
proof (prove)
using this:
chain_reparam_chain' (one_chain1 - ps1) subdiv
chain_reparam_chain' (one_chain2 - ps2) subdiv
\<forall>(k, \<gamma>)\<in>subdiv. \<gamma> C1_differentiable_on {0..1}
boundary_chain subdiv
\<forall>(k, \<gamma>)\<in>ps1. point_path \<gamma>
\<forall>(k, \<gamma>)\<in>ps2. point_path \<gamma>
finite basis
finite one_chain1
finite one_chain2
boundary_chain one_chain1
boundary_chain one_chain2
\<forall>(k2, \<gamma>2)\<in>one_chain2. \<forall>b\<in>basis. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)
common_reparam_exists one_chain1 one_chain2
\<forall>(k, \<gamma>)\<in>one_chain1. valid_path \<gamma>
\<forall>(k, \<gamma>)\<in>one_chain2. valid_path \<gamma>

goal (4 subgoals):
 1. finite (one_chain1 - ps1)
 2. boundary_chain (one_chain1 - ps1)
 3. boundary_chain subdiv
 4. \<forall>(k, \<gamma>)\<in>one_chain1 - ps1. valid_path \<gamma>
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. boundary_chain (one_chain1 - ps1)
 2. boundary_chain subdiv
 3. \<forall>(k, \<gamma>)\<in>one_chain1 - ps1. valid_path \<gamma>
[PROOF STEP]
using props assms
[PROOF STATE]
proof (prove)
using this:
chain_reparam_chain' (one_chain1 - ps1) subdiv
chain_reparam_chain' (one_chain2 - ps2) subdiv
\<forall>(k, \<gamma>)\<in>subdiv. \<gamma> C1_differentiable_on {0..1}
boundary_chain subdiv
\<forall>(k, \<gamma>)\<in>ps1. point_path \<gamma>
\<forall>(k, \<gamma>)\<in>ps2. point_path \<gamma>
finite basis
finite one_chain1
finite one_chain2
boundary_chain one_chain1
boundary_chain one_chain2
\<forall>(k2, \<gamma>2)\<in>one_chain2. \<forall>b\<in>basis. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)
common_reparam_exists one_chain1 one_chain2
\<forall>(k, \<gamma>)\<in>one_chain1. valid_path \<gamma>
\<forall>(k, \<gamma>)\<in>one_chain2. valid_path \<gamma>

goal (3 subgoals):
 1. boundary_chain (one_chain1 - ps1)
 2. boundary_chain subdiv
 3. \<forall>(k, \<gamma>)\<in>one_chain1 - ps1. valid_path \<gamma>
[PROOF STEP]
using onechain_boundary1
[PROOF STATE]
proof (prove)
using this:
chain_reparam_chain' (one_chain1 - ps1) subdiv
chain_reparam_chain' (one_chain2 - ps2) subdiv
\<forall>(k, \<gamma>)\<in>subdiv. \<gamma> C1_differentiable_on {0..1}
boundary_chain subdiv
\<forall>(k, \<gamma>)\<in>ps1. point_path \<gamma>
\<forall>(k, \<gamma>)\<in>ps2. point_path \<gamma>
finite basis
finite one_chain1
finite one_chain2
boundary_chain one_chain1
boundary_chain one_chain2
\<forall>(k2, \<gamma>2)\<in>one_chain2. \<forall>b\<in>basis. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)
common_reparam_exists one_chain1 one_chain2
\<forall>(k, \<gamma>)\<in>one_chain1. valid_path \<gamma>
\<forall>(k, \<gamma>)\<in>one_chain2. valid_path \<gamma>
boundary_chain (one_chain1 - ps1)

goal (3 subgoals):
 1. boundary_chain (one_chain1 - ps1)
 2. boundary_chain subdiv
 3. \<forall>(k, \<gamma>)\<in>one_chain1 - ps1. valid_path \<gamma>
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. boundary_chain subdiv
 2. \<forall>(k, \<gamma>)\<in>one_chain1 - ps1. valid_path \<gamma>
[PROOF STEP]
using props assms
[PROOF STATE]
proof (prove)
using this:
chain_reparam_chain' (one_chain1 - ps1) subdiv
chain_reparam_chain' (one_chain2 - ps2) subdiv
\<forall>(k, \<gamma>)\<in>subdiv. \<gamma> C1_differentiable_on {0..1}
boundary_chain subdiv
\<forall>(k, \<gamma>)\<in>ps1. point_path \<gamma>
\<forall>(k, \<gamma>)\<in>ps2. point_path \<gamma>
finite basis
finite one_chain1
finite one_chain2
boundary_chain one_chain1
boundary_chain one_chain2
\<forall>(k2, \<gamma>2)\<in>one_chain2. \<forall>b\<in>basis. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)
common_reparam_exists one_chain1 one_chain2
\<forall>(k, \<gamma>)\<in>one_chain1. valid_path \<gamma>
\<forall>(k, \<gamma>)\<in>one_chain2. valid_path \<gamma>

goal (2 subgoals):
 1. boundary_chain subdiv
 2. \<forall>(k, \<gamma>)\<in>one_chain1 - ps1. valid_path \<gamma>
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>(k, \<gamma>)\<in>one_chain1 - ps1. valid_path \<gamma>
[PROOF STEP]
using one_chain1_ps_valid
[PROOF STATE]
proof (prove)
using this:
\<forall>(k, \<gamma>)\<in>one_chain1 - ps1. valid_path \<gamma>

goal (1 subgoal):
 1. \<forall>(k, \<gamma>)\<in>one_chain1 - ps1. valid_path \<gamma>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>(k, \<gamma>)\<in>one_chain1 - ps1. line_integral_exists F basis \<gamma>

goal (2 subgoals):
 1. one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2
 2. \<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>
[PROOF STEP]
have 2: "one_chain_line_integral F basis (one_chain2 - ps2) = one_chain_line_integral F basis subdiv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. one_chain_line_integral F basis (one_chain2 - ps2) = one_chain_line_integral F basis subdiv
[PROOF STEP]
apply(rule chain_reparam_chain'_line_integral_smooth_cubes[OF props(2) props(3) cont_field finite_basis])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. finite (one_chain2 - ps2)
 2. boundary_chain (one_chain2 - ps2)
 3. boundary_chain subdiv
 4. \<forall>(k, \<gamma>)\<in>one_chain2 - ps2. valid_path \<gamma>
[PROOF STEP]
using props assms
[PROOF STATE]
proof (prove)
using this:
chain_reparam_chain' (one_chain1 - ps1) subdiv
chain_reparam_chain' (one_chain2 - ps2) subdiv
\<forall>(k, \<gamma>)\<in>subdiv. \<gamma> C1_differentiable_on {0..1}
boundary_chain subdiv
\<forall>(k, \<gamma>)\<in>ps1. point_path \<gamma>
\<forall>(k, \<gamma>)\<in>ps2. point_path \<gamma>
finite basis
finite one_chain1
finite one_chain2
boundary_chain one_chain1
boundary_chain one_chain2
\<forall>(k2, \<gamma>2)\<in>one_chain2. \<forall>b\<in>basis. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)
common_reparam_exists one_chain1 one_chain2
\<forall>(k, \<gamma>)\<in>one_chain1. valid_path \<gamma>
\<forall>(k, \<gamma>)\<in>one_chain2. valid_path \<gamma>

goal (4 subgoals):
 1. finite (one_chain2 - ps2)
 2. boundary_chain (one_chain2 - ps2)
 3. boundary_chain subdiv
 4. \<forall>(k, \<gamma>)\<in>one_chain2 - ps2. valid_path \<gamma>
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. boundary_chain (one_chain2 - ps2)
 2. boundary_chain subdiv
 3. \<forall>(k, \<gamma>)\<in>one_chain2 - ps2. valid_path \<gamma>
[PROOF STEP]
apply (simp add: assms(5) boundary_chain_diff)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. boundary_chain subdiv
 2. \<forall>(k, \<gamma>)\<in>one_chain2 - ps2. valid_path \<gamma>
[PROOF STEP]
apply (simp add: props(4))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>(k, \<gamma>)\<in>one_chain2 - ps2. valid_path \<gamma>
[PROOF STEP]
by (simp add: assms(9))
[PROOF STATE]
proof (state)
this:
one_chain_line_integral F basis (one_chain2 - ps2) = one_chain_line_integral F basis subdiv

goal (2 subgoals):
 1. one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2
 2. \<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>
[PROOF STEP]
have 3:"\<forall>(k, \<gamma>)\<in>(one_chain2 - ps2). line_integral_exists F basis \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>(k, \<gamma>)\<in>one_chain2 - ps2. line_integral_exists F basis \<gamma>
[PROOF STEP]
apply(rule chain_reparam_chain'_line_integral_smooth_cubes[OF props(2) props(3) cont_field finite_basis])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. finite (one_chain2 - ps2)
 2. boundary_chain (one_chain2 - ps2)
 3. boundary_chain subdiv
 4. \<forall>(k, \<gamma>)\<in>one_chain2 - ps2. valid_path \<gamma>
[PROOF STEP]
using props assms
[PROOF STATE]
proof (prove)
using this:
chain_reparam_chain' (one_chain1 - ps1) subdiv
chain_reparam_chain' (one_chain2 - ps2) subdiv
\<forall>(k, \<gamma>)\<in>subdiv. \<gamma> C1_differentiable_on {0..1}
boundary_chain subdiv
\<forall>(k, \<gamma>)\<in>ps1. point_path \<gamma>
\<forall>(k, \<gamma>)\<in>ps2. point_path \<gamma>
finite basis
finite one_chain1
finite one_chain2
boundary_chain one_chain1
boundary_chain one_chain2
\<forall>(k2, \<gamma>2)\<in>one_chain2. \<forall>b\<in>basis. continuous_on (path_image \<gamma>2) (\<lambda>x. F x \<bullet> b)
common_reparam_exists one_chain1 one_chain2
\<forall>(k, \<gamma>)\<in>one_chain1. valid_path \<gamma>
\<forall>(k, \<gamma>)\<in>one_chain2. valid_path \<gamma>

goal (4 subgoals):
 1. finite (one_chain2 - ps2)
 2. boundary_chain (one_chain2 - ps2)
 3. boundary_chain subdiv
 4. \<forall>(k, \<gamma>)\<in>one_chain2 - ps2. valid_path \<gamma>
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. boundary_chain (one_chain2 - ps2)
 2. boundary_chain subdiv
 3. \<forall>(k, \<gamma>)\<in>one_chain2 - ps2. valid_path \<gamma>
[PROOF STEP]
apply (simp add: assms(5) boundary_chain_diff)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. boundary_chain subdiv
 2. \<forall>(k, \<gamma>)\<in>one_chain2 - ps2. valid_path \<gamma>
[PROOF STEP]
apply (simp add: props(4))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>(k, \<gamma>)\<in>one_chain2 - ps2. valid_path \<gamma>
[PROOF STEP]
by (simp add: assms(9))
[PROOF STATE]
proof (state)
this:
\<forall>(k, \<gamma>)\<in>one_chain2 - ps2. line_integral_exists F basis \<gamma>

goal (2 subgoals):
 1. one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2
 2. \<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>
[PROOF STEP]
show line_int_ex_chain1: "\<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>
[PROOF STEP]
using 0
[PROOF STATE]
proof (prove)
using this:
one_chain_line_integral F basis (one_chain1 - ps1) = one_chain_line_integral F basis subdiv

goal (1 subgoal):
 1. \<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>
[PROOF STEP]
using "1" finite_basis line_integral_exists_point_path props(5)
[PROOF STATE]
proof (prove)
using this:
one_chain_line_integral F basis (one_chain1 - ps1) = one_chain_line_integral F basis subdiv
\<forall>(k, \<gamma>)\<in>one_chain1 - ps1. line_integral_exists F basis \<gamma>
finite basis
\<lbrakk>finite ?basis; point_path ?\<gamma>\<rbrakk> \<Longrightarrow> line_integral_exists ?F ?basis ?\<gamma>
\<forall>(k, \<gamma>)\<in>ps1. point_path \<gamma>

goal (1 subgoal):
 1. \<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>

goal (1 subgoal):
 1. one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>
[PROOF STEP]
show "one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2"
[PROOF STATE]
proof (prove)
using this:
\<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>

goal (1 subgoal):
 1. one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2
[PROOF STEP]
using 0 1 2 3
[PROOF STATE]
proof (prove)
using this:
\<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>
one_chain_line_integral F basis (one_chain1 - ps1) = one_chain_line_integral F basis subdiv
\<forall>(k, \<gamma>)\<in>one_chain1 - ps1. line_integral_exists F basis \<gamma>
one_chain_line_integral F basis (one_chain2 - ps2) = one_chain_line_integral F basis subdiv
\<forall>(k, \<gamma>)\<in>one_chain2 - ps2. line_integral_exists F basis \<gamma>

goal (1 subgoal):
 1. one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2
[PROOF STEP]
using assms(2-3) finite_basis one_chain_line_integral_point_paths props(5) props(6)
[PROOF STATE]
proof (prove)
using this:
\<forall>(k, \<gamma>)\<in>one_chain1. line_integral_exists F basis \<gamma>
one_chain_line_integral F basis (one_chain1 - ps1) = one_chain_line_integral F basis subdiv
\<forall>(k, \<gamma>)\<in>one_chain1 - ps1. line_integral_exists F basis \<gamma>
one_chain_line_integral F basis (one_chain2 - ps2) = one_chain_line_integral F basis subdiv
\<forall>(k, \<gamma>)\<in>one_chain2 - ps2. line_integral_exists F basis \<gamma>
finite one_chain1
finite one_chain2
finite basis
\<lbrakk>finite ?one_chain; finite ?basis; \<forall>(k, \<gamma>)\<in>?ps. point_path \<gamma>\<rbrakk> \<Longrightarrow> one_chain_line_integral ?F ?basis (?one_chain - ?ps) = one_chain_line_integral ?F ?basis ?one_chain
\<forall>(k, \<gamma>)\<in>ps1. point_path \<gamma>
\<forall>(k, \<gamma>)\<in>ps2. point_path \<gamma>

goal (1 subgoal):
 1. one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
one_chain_line_integral F basis one_chain1 = one_chain_line_integral F basis one_chain2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma subcube_valid_path:
  assumes "valid_path (snd cube)" "a \<in> {0..1}" "b \<in> {0..1}"
  shows "valid_path (snd (subcube a b cube))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_path (snd (subcube a b cube))
[PROOF STEP]
using valid_path_subpath[OF assms]
[PROOF STATE]
proof (prove)
using this:
valid_path (subpath a b (snd cube))

goal (1 subgoal):
 1. valid_path (snd (subcube a b cube))
[PROOF STEP]
by (auto simp add: subcube_def)


[STATEMENT]
lemma dg_prod_components:
  shows "(\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)\<lparr>Obj\<rparr> = (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Obj\<rparr>)"
    and "(\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)\<lparr>Arr\<rparr> = (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Arr\<rparr>)"
    and "(\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)\<lparr>Dom\<rparr> =
      (\<lambda>f\<in>\<^sub>\<circ>(\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Arr\<rparr>). (\<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Dom\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>))"
    and "(\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)\<lparr>Cod\<rparr> =
      (\<lambda>f\<in>\<^sub>\<circ>(\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Arr\<rparr>). (\<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Cod\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (dg_prod I \<AA>\<lparr>Obj\<rparr> = (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Obj\<rparr>) &&& dg_prod I \<AA>\<lparr>Arr\<rparr> = (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Arr\<rparr>)) &&& dg_prod I \<AA>\<lparr>Dom\<rparr> = (\<lambda>f\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Arr\<rparr>. \<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Dom\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>) &&& dg_prod I \<AA>\<lparr>Cod\<rparr> = (\<lambda>f\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Arr\<rparr>. \<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Cod\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>)
[PROOF STEP]
unfolding dg_prod_def dg_field_simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>[]\<^sub>\<circ>\<rparr>, \<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>1\<^sub>\<nat>\<rparr>, \<lambda>f\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>1\<^sub>\<nat>\<rparr>. \<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>, \<lambda>f\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>1\<^sub>\<nat>\<rparr>. \<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>]\<^sub>\<circ>\<lparr>[]\<^sub>\<circ>\<rparr> = (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>[]\<^sub>\<circ>\<rparr>) &&& [\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>[]\<^sub>\<circ>\<rparr>, \<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>1\<^sub>\<nat>\<rparr>, \<lambda>f\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>1\<^sub>\<nat>\<rparr>. \<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>, \<lambda>f\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>1\<^sub>\<nat>\<rparr>. \<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr> = (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>1\<^sub>\<nat>\<rparr>)) &&& [\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>[]\<^sub>\<circ>\<rparr>, \<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>1\<^sub>\<nat>\<rparr>, \<lambda>f\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>1\<^sub>\<nat>\<rparr>. \<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>, \<lambda>f\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>1\<^sub>\<nat>\<rparr>. \<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr> = (\<lambda>f\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>1\<^sub>\<nat>\<rparr>. \<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>) &&& [\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>[]\<^sub>\<circ>\<rparr>, \<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>1\<^sub>\<nat>\<rparr>, \<lambda>f\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>1\<^sub>\<nat>\<rparr>. \<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>, \<lambda>f\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>1\<^sub>\<nat>\<rparr>. \<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr> = (\<lambda>f\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>1\<^sub>\<nat>\<rparr>. \<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>)
[PROOF STEP]
by (simp_all add: nat_omega_simps)


[STATEMENT]
lemma (in pdigraph_base) pdigraph_base_axioms'[dg_prod_cs_intros]:
  assumes "\<alpha>' = \<alpha>" and "I' = I"
  shows "pdigraph_base \<alpha>' I' \<AA>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pdigraph_base \<alpha>' I' \<AA>
[PROOF STEP]
unfolding assms
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pdigraph_base \<alpha> I \<AA>
[PROOF STEP]
by (rule pdigraph_base_axioms)


[STATEMENT]
lemma (in pdigraph_base) pdg_Obj_in_Vset:
  assumes "\<Z> \<beta>" and "\<alpha> \<in>\<^sub>\<circ> \<beta>"
  shows "(\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Obj\<rparr>) \<in>\<^sub>\<circ> Vset \<beta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Obj\<rparr>) \<in>\<^sub>\<circ> Vset \<beta>
[PROOF STEP]
proof(rule Vset_trans)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Obj\<rparr>) \<in>\<^sub>\<circ> ?X
 2. ?X \<in>\<^sub>\<circ> Vset \<beta>
[PROOF STEP]
interpret \<beta>: \<Z> \<beta>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Z> \<beta>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Obj\<rparr>) \<in>\<^sub>\<circ> ?X
 2. ?X \<in>\<^sub>\<circ> Vset \<beta>
[PROOF STEP]
show "(\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Obj\<rparr>) \<in>\<^sub>\<circ> Vset (succ (succ \<alpha>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Obj\<rparr>) \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ (ZFC_in_HOL.succ \<alpha>))
[PROOF STEP]
proof
    (
      rule vsubset_in_VsetI,
      rule Limit_vproduct_vsubset_Vset_succI,
      rule Limit_\<alpha>,
      intro dg_cs_intros
    )
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> \<AA> i\<lparr>Obj\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>
 2. Vset (ZFC_in_HOL.succ \<alpha>) \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ (ZFC_in_HOL.succ \<alpha>))
[PROOF STEP]
show "Vset (succ \<alpha>) \<in>\<^sub>\<circ> Vset (succ (succ \<alpha>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Vset (ZFC_in_HOL.succ \<alpha>) \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ (ZFC_in_HOL.succ \<alpha>))
[PROOF STEP]
by (cs_concl cs_shallow cs_intro: V_cs_intros)
[PROOF STATE]
proof (state)
this:
Vset (ZFC_in_HOL.succ \<alpha>) \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ (ZFC_in_HOL.succ \<alpha>))

goal (1 subgoal):
 1. \<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> \<AA> i\<lparr>Obj\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> \<AA> i\<lparr>Obj\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
assume "i \<in>\<^sub>\<circ> I"
[PROOF STATE]
proof (state)
this:
i \<in>\<^sub>\<circ> I

goal (1 subgoal):
 1. \<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> \<AA> i\<lparr>Obj\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<in>\<^sub>\<circ> I
[PROOF STEP]
interpret digraph \<alpha> \<open>\<AA> i\<close>
[PROOF STATE]
proof (prove)
using this:
i \<in>\<^sub>\<circ> I

goal (1 subgoal):
 1. digraph \<alpha> (\<AA> i)
[PROOF STEP]
by (cs_concl cs_shallow cs_intro: dg_cs_intros dg_prod_cs_intros)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> \<AA> i\<lparr>Obj\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
show "\<AA> i\<lparr>Obj\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<AA> i\<lparr>Obj\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (rule dg_Obj_vsubset_Vset)
[PROOF STATE]
proof (state)
this:
\<AA> i\<lparr>Obj\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Obj\<rparr>) \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ (ZFC_in_HOL.succ \<alpha>))

goal (1 subgoal):
 1. Vset (ZFC_in_HOL.succ (ZFC_in_HOL.succ \<alpha>)) \<in>\<^sub>\<circ> Vset \<beta>
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
\<alpha> \<in>\<^sub>\<circ> \<beta>
[PROOF STEP]
show "Vset (succ (succ \<alpha>)) \<in>\<^sub>\<circ> Vset \<beta>"
[PROOF STATE]
proof (prove)
using this:
\<alpha> \<in>\<^sub>\<circ> \<beta>

goal (1 subgoal):
 1. Vset (ZFC_in_HOL.succ (ZFC_in_HOL.succ \<alpha>)) \<in>\<^sub>\<circ> Vset \<beta>
[PROOF STEP]
by (cs_concl cs_shallow cs_intro: V_cs_intros succ_in_Limit_iff[THEN iffD2])
[PROOF STATE]
proof (state)
this:
Vset (ZFC_in_HOL.succ (ZFC_in_HOL.succ \<alpha>)) \<in>\<^sub>\<circ> Vset \<beta>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in pdigraph_base) pdg_Arr_in_Vset:
  assumes "\<Z> \<beta>" and "\<alpha> \<in>\<^sub>\<circ> \<beta>"
  shows "(\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Arr\<rparr>) \<in>\<^sub>\<circ> Vset \<beta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Arr\<rparr>) \<in>\<^sub>\<circ> Vset \<beta>
[PROOF STEP]
proof(rule Vset_trans)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Arr\<rparr>) \<in>\<^sub>\<circ> ?X
 2. ?X \<in>\<^sub>\<circ> Vset \<beta>
[PROOF STEP]
interpret \<beta>: \<Z> \<beta>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Z> \<beta>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Arr\<rparr>) \<in>\<^sub>\<circ> ?X
 2. ?X \<in>\<^sub>\<circ> Vset \<beta>
[PROOF STEP]
show "(\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Arr\<rparr>) \<in>\<^sub>\<circ> Vset (succ (succ \<alpha>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Arr\<rparr>) \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ (ZFC_in_HOL.succ \<alpha>))
[PROOF STEP]
proof
    (
      rule vsubset_in_VsetI,
      rule Limit_vproduct_vsubset_Vset_succI,
      rule Limit_\<alpha>,
      intro dg_cs_intros
    )
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> \<AA> i\<lparr>Arr\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>
 2. Vset (ZFC_in_HOL.succ \<alpha>) \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ (ZFC_in_HOL.succ \<alpha>))
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> \<AA> i\<lparr>Arr\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>
 2. Vset (ZFC_in_HOL.succ \<alpha>) \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ (ZFC_in_HOL.succ \<alpha>))
[PROOF STEP]
assume "i \<in>\<^sub>\<circ> I"
[PROOF STATE]
proof (state)
this:
i \<in>\<^sub>\<circ> I

goal (2 subgoals):
 1. \<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> \<AA> i\<lparr>Arr\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>
 2. Vset (ZFC_in_HOL.succ \<alpha>) \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ (ZFC_in_HOL.succ \<alpha>))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<in>\<^sub>\<circ> I
[PROOF STEP]
interpret digraph \<alpha> \<open>\<AA> i\<close>
[PROOF STATE]
proof (prove)
using this:
i \<in>\<^sub>\<circ> I

goal (1 subgoal):
 1. digraph \<alpha> (\<AA> i)
[PROOF STEP]
by (cs_concl cs_shallow cs_intro: dg_prod_cs_intros)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> \<AA> i\<lparr>Arr\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>
 2. Vset (ZFC_in_HOL.succ \<alpha>) \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ (ZFC_in_HOL.succ \<alpha>))
[PROOF STEP]
show "\<AA> i\<lparr>Arr\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<AA> i\<lparr>Arr\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (rule dg_Arr_vsubset_Vset)
[PROOF STATE]
proof (state)
this:
\<AA> i\<lparr>Arr\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. Vset (ZFC_in_HOL.succ \<alpha>) \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ (ZFC_in_HOL.succ \<alpha>))
[PROOF STEP]
qed (cs_concl cs_shallow cs_intro: V_cs_intros)
[PROOF STATE]
proof (state)
this:
(\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Arr\<rparr>) \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ (ZFC_in_HOL.succ \<alpha>))

goal (1 subgoal):
 1. Vset (ZFC_in_HOL.succ (ZFC_in_HOL.succ \<alpha>)) \<in>\<^sub>\<circ> Vset \<beta>
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
\<alpha> \<in>\<^sub>\<circ> \<beta>
[PROOF STEP]
show "Vset (succ (succ \<alpha>)) \<in>\<^sub>\<circ> Vset \<beta>"
[PROOF STATE]
proof (prove)
using this:
\<alpha> \<in>\<^sub>\<circ> \<beta>

goal (1 subgoal):
 1. Vset (ZFC_in_HOL.succ (ZFC_in_HOL.succ \<alpha>)) \<in>\<^sub>\<circ> Vset \<beta>
[PROOF STEP]
by (cs_concl cs_shallow cs_intro: V_cs_intros succ_in_Limit_iff[THEN iffD2])
[PROOF STATE]
proof (state)
this:
Vset (ZFC_in_HOL.succ (ZFC_in_HOL.succ \<alpha>)) \<in>\<^sub>\<circ> Vset \<beta>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in pdigraph_base) pdg_vsubset_index_pdigraph_base:
  assumes "J \<subseteq>\<^sub>\<circ> I"
  shows "pdigraph_base \<alpha> J \<AA>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pdigraph_base \<alpha> J \<AA>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
J \<subseteq>\<^sub>\<circ> I

goal (1 subgoal):
 1. pdigraph_base \<alpha> J \<AA>
[PROOF STEP]
by (intro pdigraph_baseI)
    (auto simp: vsubset_in_VsetI dg_cs_intros intro: dg_prod_cs_intros)


[STATEMENT]
lemma dg_prod_ObjI:
  assumes "vsv a" and "\<D>\<^sub>\<circ> a = I" and "\<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> a\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>"
  shows "a \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
vsv a
\<D>\<^sub>\<circ> a = I
?i \<in>\<^sub>\<circ> I \<Longrightarrow> a\<lparr>?i\<rparr> \<in>\<^sub>\<circ> \<AA> ?i\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
unfolding dg_prod_components
[PROOF STATE]
proof (prove)
using this:
vsv a
\<D>\<^sub>\<circ> a = I
?i \<in>\<^sub>\<circ> I \<Longrightarrow> a\<lparr>?i\<rparr> \<in>\<^sub>\<circ> \<AA> ?i\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Obj\<rparr>)
[PROOF STEP]
by auto


[STATEMENT]
lemma dg_prod_ObjD:
  assumes "a \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)\<lparr>Obj\<rparr>"
  shows "vsv a" and "\<D>\<^sub>\<circ> a = I" and "\<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> a\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv a &&& \<D>\<^sub>\<circ> a = I &&& (\<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> a\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. vsv a &&& \<D>\<^sub>\<circ> a = I &&& (\<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> a\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>)
[PROOF STEP]
unfolding dg_prod_components
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Obj\<rparr>)

goal (1 subgoal):
 1. vsv a &&& \<D>\<^sub>\<circ> a = I &&& (\<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> a\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>)
[PROOF STEP]
by auto


[STATEMENT]
lemma dg_prod_ObjE:
  assumes "a \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)\<lparr>Obj\<rparr>"
  obtains "vsv a" and "\<D>\<^sub>\<circ> a = I" and "\<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> a\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>vsv a; \<D>\<^sub>\<circ> a = I; \<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> a\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. (\<lbrakk>vsv a; \<D>\<^sub>\<circ> a = I; \<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> a\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto dest: dg_prod_ObjD)


[STATEMENT]
lemma dg_prod_Obj_cong:
  assumes "g \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)\<lparr>Obj\<rparr>"
    and "f \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)\<lparr>Obj\<rparr>"
    and "\<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> g\<lparr>i\<rparr> = f\<lparr>i\<rparr>"
  shows "g = f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g = f
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
g \<in>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Obj\<rparr>
f \<in>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Obj\<rparr>
?i \<in>\<^sub>\<circ> I \<Longrightarrow> g\<lparr>?i\<rparr> = f\<lparr>?i\<rparr>

goal (1 subgoal):
 1. g = f
[PROOF STEP]
by (intro vsv_eqI[of g f]) (force simp: dg_prod_components)+


[STATEMENT]
lemma dg_prod_ArrI:
  assumes "vsv f" and "\<D>\<^sub>\<circ> f = I" and "\<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> f\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>"
  shows "f \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Arr\<rparr>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
vsv f
\<D>\<^sub>\<circ> f = I
?i \<in>\<^sub>\<circ> I \<Longrightarrow> f\<lparr>?i\<rparr> \<in>\<^sub>\<circ> \<AA> ?i\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. f \<in>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Arr\<rparr>
[PROOF STEP]
unfolding dg_prod_components
[PROOF STATE]
proof (prove)
using this:
vsv f
\<D>\<^sub>\<circ> f = I
?i \<in>\<^sub>\<circ> I \<Longrightarrow> f\<lparr>?i\<rparr> \<in>\<^sub>\<circ> \<AA> ?i\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. f \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Arr\<rparr>)
[PROOF STEP]
by auto


[STATEMENT]
lemma dg_prod_ArrD:
  assumes "f \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)\<lparr>Arr\<rparr>"
  shows "vsv f" and "\<D>\<^sub>\<circ> f = I" and "\<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> f\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv f &&& \<D>\<^sub>\<circ> f = I &&& (\<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> f\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
f \<in>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. vsv f &&& \<D>\<^sub>\<circ> f = I &&& (\<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> f\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>)
[PROOF STEP]
unfolding dg_prod_components
[PROOF STATE]
proof (prove)
using this:
f \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Arr\<rparr>)

goal (1 subgoal):
 1. vsv f &&& \<D>\<^sub>\<circ> f = I &&& (\<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> f\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>)
[PROOF STEP]
by auto


[STATEMENT]
lemma dg_prod_ArrE:
  assumes "f \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)\<lparr>Arr\<rparr>"
  obtains "vsv f" and "\<D>\<^sub>\<circ> f = I" and "\<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> f\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>vsv f; \<D>\<^sub>\<circ> f = I; \<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> f\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
f \<in>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. (\<lbrakk>vsv f; \<D>\<^sub>\<circ> f = I; \<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> f\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto dest: dg_prod_ArrD)


[STATEMENT]
lemma dg_prod_Arr_cong:
  assumes "g \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)\<lparr>Arr\<rparr>"
    and "f \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)\<lparr>Arr\<rparr>"
    and "\<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> g\<lparr>i\<rparr> = f\<lparr>i\<rparr>"
  shows "g = f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g = f
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
g \<in>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Arr\<rparr>
f \<in>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Arr\<rparr>
?i \<in>\<^sub>\<circ> I \<Longrightarrow> g\<lparr>?i\<rparr> = f\<lparr>?i\<rparr>

goal (1 subgoal):
 1. g = f
[PROOF STEP]
by (intro vsv_eqI[of g f]) (force simp: dg_prod_components)+


[STATEMENT]
lemma (in pdigraph_base) dg_prod_Dom_app_in_Obj[dg_cs_intros]:
  assumes "f \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)\<lparr>Arr\<rparr>"
  shows "(\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)\<lparr>Dom\<rparr>\<lparr>f\<rparr> \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dg_prod I \<AA>\<lparr>Dom\<rparr>\<lparr>f\<rparr> \<in>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
unfolding dg_prod_components(1) dg_prod_Dom_app[OF assms]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Dom\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>) \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Obj\<rparr>)
[PROOF STEP]
proof(intro vproductI ballI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. vsv (\<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Dom\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>)
 2. \<D>\<^sub>\<circ> (\<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Dom\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>) = I
 3. \<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> (\<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Dom\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. vsv (\<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Dom\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>)
 2. \<D>\<^sub>\<circ> (\<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Dom\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>) = I
 3. \<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> (\<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Dom\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>
[PROOF STEP]
assume prems: "i \<in>\<^sub>\<circ> I"
[PROOF STATE]
proof (state)
this:
i \<in>\<^sub>\<circ> I

goal (3 subgoals):
 1. vsv (\<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Dom\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>)
 2. \<D>\<^sub>\<circ> (\<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Dom\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>) = I
 3. \<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> (\<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Dom\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>
[PROOF STEP]
interpret digraph \<alpha> \<open>\<AA> i\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. digraph \<alpha> (\<AA> i)
[PROOF STEP]
by (auto simp: prems intro: dg_prod_cs_intros)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. vsv (\<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Dom\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>)
 2. \<D>\<^sub>\<circ> (\<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Dom\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>) = I
 3. \<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> (\<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Dom\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>
[PROOF STEP]
from assms prems
[PROOF STATE]
proof (chain)
picking this:
f \<in>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Arr\<rparr>
i \<in>\<^sub>\<circ> I
[PROOF STEP]
show "(\<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Dom\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
using this:
f \<in>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Arr\<rparr>
i \<in>\<^sub>\<circ> I

goal (1 subgoal):
 1. (\<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Dom\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>
[PROOF STEP]
unfolding dg_prod_components(2)
[PROOF STATE]
proof (prove)
using this:
f \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Arr\<rparr>)
i \<in>\<^sub>\<circ> I

goal (1 subgoal):
 1. (\<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Dom\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(\<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Dom\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>

goal (2 subgoals):
 1. vsv (\<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Dom\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>)
 2. \<D>\<^sub>\<circ> (\<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Dom\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>) = I
[PROOF STEP]
qed simp_all


[STATEMENT]
lemma dg_prod_Dom_app_component_app[dg_cs_simps]:
  assumes "f \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)\<lparr>Arr\<rparr>" and "i \<in>\<^sub>\<circ> I"
  shows "(\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)\<lparr>Dom\<rparr>\<lparr>f\<rparr>\<lparr>i\<rparr> = \<AA> i\<lparr>Dom\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dg_prod I \<AA>\<lparr>Dom\<rparr>\<lparr>f\<rparr>\<lparr>i\<rparr> = \<AA> i\<lparr>Dom\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
i \<in>\<^sub>\<circ> I

goal (1 subgoal):
 1. dg_prod I \<AA>\<lparr>Dom\<rparr>\<lparr>f\<rparr>\<lparr>i\<rparr> = \<AA> i\<lparr>Dom\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>
[PROOF STEP]
unfolding dg_prod_Dom_app[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
i \<in>\<^sub>\<circ> I

goal (1 subgoal):
 1. (\<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Dom\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>)\<lparr>i\<rparr> = \<AA> i\<lparr>Dom\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>
[PROOF STEP]
by simp


[STATEMENT]
lemma (in pdigraph_base) dg_prod_Cod_app_in_Obj[dg_cs_intros]:
  assumes "f \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)\<lparr>Arr\<rparr>"
  shows "(\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)\<lparr>Cod\<rparr>\<lparr>f\<rparr> \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dg_prod I \<AA>\<lparr>Cod\<rparr>\<lparr>f\<rparr> \<in>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
unfolding dg_prod_components(1) dg_prod_Cod_app[OF assms]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Cod\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>) \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Obj\<rparr>)
[PROOF STEP]
proof(rule vproductI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. vsv (\<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Cod\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>)
 2. \<D>\<^sub>\<circ> (\<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Cod\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>) = I
 3. \<forall>i\<in>elts I. (\<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Cod\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>
[PROOF STEP]
show "\<forall>i\<in>\<^sub>\<circ>I. (\<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Cod\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i\<in>elts I. (\<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Cod\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>
[PROOF STEP]
proof(intro ballI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> (\<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Cod\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> (\<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Cod\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>
[PROOF STEP]
assume prems: "i \<in>\<^sub>\<circ> I"
[PROOF STATE]
proof (state)
this:
i \<in>\<^sub>\<circ> I

goal (1 subgoal):
 1. \<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> (\<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Cod\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<in>\<^sub>\<circ> I
[PROOF STEP]
interpret digraph \<alpha> \<open>\<AA> i\<close>
[PROOF STATE]
proof (prove)
using this:
i \<in>\<^sub>\<circ> I

goal (1 subgoal):
 1. digraph \<alpha> (\<AA> i)
[PROOF STEP]
by (auto intro: dg_prod_cs_intros)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> (\<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Cod\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>
[PROOF STEP]
from assms prems
[PROOF STATE]
proof (chain)
picking this:
f \<in>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Arr\<rparr>
i \<in>\<^sub>\<circ> I
[PROOF STEP]
show "(\<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Cod\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
using this:
f \<in>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Arr\<rparr>
i \<in>\<^sub>\<circ> I

goal (1 subgoal):
 1. (\<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Cod\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>
[PROOF STEP]
unfolding dg_prod_components(2)
[PROOF STATE]
proof (prove)
using this:
f \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Arr\<rparr>)
i \<in>\<^sub>\<circ> I

goal (1 subgoal):
 1. (\<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Cod\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(\<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Cod\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>i\<in>elts I. (\<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Cod\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>

goal (2 subgoals):
 1. vsv (\<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Cod\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>)
 2. \<D>\<^sub>\<circ> (\<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Cod\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>) = I
[PROOF STEP]
qed simp_all


[STATEMENT]
lemma dg_prod_Cod_app_component_app[dg_cs_simps]:
  assumes "f \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)\<lparr>Arr\<rparr>" and "i \<in>\<^sub>\<circ> I"
  shows "(\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)\<lparr>Cod\<rparr>\<lparr>f\<rparr>\<lparr>i\<rparr> = \<AA> i\<lparr>Cod\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dg_prod I \<AA>\<lparr>Cod\<rparr>\<lparr>f\<rparr>\<lparr>i\<rparr> = \<AA> i\<lparr>Cod\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
i \<in>\<^sub>\<circ> I

goal (1 subgoal):
 1. dg_prod I \<AA>\<lparr>Cod\<rparr>\<lparr>f\<rparr>\<lparr>i\<rparr> = \<AA> i\<lparr>Cod\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>
[PROOF STEP]
unfolding dg_prod_Cod_app[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
i \<in>\<^sub>\<circ> I

goal (1 subgoal):
 1. (\<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Cod\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>)\<lparr>i\<rparr> = \<AA> i\<lparr>Cod\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>
[PROOF STEP]
by simp


[STATEMENT]
lemma (in pdigraph_base) pdg_tiny_digraph_dg_prod:
  assumes "\<Z> \<beta>" and "\<alpha> \<in>\<^sub>\<circ> \<beta>"
  shows "tiny_digraph \<beta> (\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tiny_digraph \<beta> (dg_prod I \<AA>)
[PROOF STEP]
proof(intro tiny_digraphI)
[PROOF STATE]
proof (state)
goal (11 subgoals):
 1. \<Z> \<beta>
 2. vfsequence (dg_prod I \<AA>)
 3. vsv (dg_prod I \<AA>\<lparr>Dom\<rparr>)
 4. vsv (dg_prod I \<AA>\<lparr>Cod\<rparr>)
 5. vcard (dg_prod I \<AA>) = 4\<^sub>\<nat>
 6. \<D>\<^sub>\<circ> (dg_prod I \<AA>\<lparr>Dom\<rparr>) = dg_prod I \<AA>\<lparr>Arr\<rparr>
 7. \<R>\<^sub>\<circ> (dg_prod I \<AA>\<lparr>Dom\<rparr>) \<subseteq>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Obj\<rparr>
 8. \<D>\<^sub>\<circ> (dg_prod I \<AA>\<lparr>Cod\<rparr>) = dg_prod I \<AA>\<lparr>Arr\<rparr>
 9. \<R>\<^sub>\<circ> (dg_prod I \<AA>\<lparr>Cod\<rparr>) \<subseteq>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Obj\<rparr>
 10. dg_prod I \<AA>\<lparr>Obj\<rparr> \<in>\<^sub>\<circ> Vset \<beta>
A total of 11 subgoals...
[PROOF STEP]
show "vfsequence (\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence (dg_prod I \<AA>)
[PROOF STEP]
unfolding dg_prod_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence [\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Obj\<rparr>, \<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Arr\<rparr>, \<lambda>f\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Arr\<rparr>. \<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Dom\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>, \<lambda>f\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Arr\<rparr>. \<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Cod\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>]\<^sub>\<circ>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vfsequence (dg_prod I \<AA>)

goal (10 subgoals):
 1. \<Z> \<beta>
 2. vsv (dg_prod I \<AA>\<lparr>Dom\<rparr>)
 3. vsv (dg_prod I \<AA>\<lparr>Cod\<rparr>)
 4. vcard (dg_prod I \<AA>) = 4\<^sub>\<nat>
 5. \<D>\<^sub>\<circ> (dg_prod I \<AA>\<lparr>Dom\<rparr>) = dg_prod I \<AA>\<lparr>Arr\<rparr>
 6. \<R>\<^sub>\<circ> (dg_prod I \<AA>\<lparr>Dom\<rparr>) \<subseteq>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Obj\<rparr>
 7. \<D>\<^sub>\<circ> (dg_prod I \<AA>\<lparr>Cod\<rparr>) = dg_prod I \<AA>\<lparr>Arr\<rparr>
 8. \<R>\<^sub>\<circ> (dg_prod I \<AA>\<lparr>Cod\<rparr>) \<subseteq>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Obj\<rparr>
 9. dg_prod I \<AA>\<lparr>Obj\<rparr> \<in>\<^sub>\<circ> Vset \<beta>
 10. dg_prod I \<AA>\<lparr>Arr\<rparr> \<in>\<^sub>\<circ> Vset \<beta>
[PROOF STEP]
show "vcard (\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i) = 4\<^sub>\<nat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard (dg_prod I \<AA>) = 4\<^sub>\<nat>
[PROOF STEP]
unfolding dg_prod_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard [\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Obj\<rparr>, \<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Arr\<rparr>, \<lambda>f\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Arr\<rparr>. \<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Dom\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>, \<lambda>f\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Arr\<rparr>. \<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Cod\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>]\<^sub>\<circ> = 4\<^sub>\<nat>
[PROOF STEP]
by (simp add: nat_omega_simps)
[PROOF STATE]
proof (state)
this:
vcard (dg_prod I \<AA>) = 4\<^sub>\<nat>

goal (9 subgoals):
 1. \<Z> \<beta>
 2. vsv (dg_prod I \<AA>\<lparr>Dom\<rparr>)
 3. vsv (dg_prod I \<AA>\<lparr>Cod\<rparr>)
 4. \<D>\<^sub>\<circ> (dg_prod I \<AA>\<lparr>Dom\<rparr>) = dg_prod I \<AA>\<lparr>Arr\<rparr>
 5. \<R>\<^sub>\<circ> (dg_prod I \<AA>\<lparr>Dom\<rparr>) \<subseteq>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Obj\<rparr>
 6. \<D>\<^sub>\<circ> (dg_prod I \<AA>\<lparr>Cod\<rparr>) = dg_prod I \<AA>\<lparr>Arr\<rparr>
 7. \<R>\<^sub>\<circ> (dg_prod I \<AA>\<lparr>Cod\<rparr>) \<subseteq>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Obj\<rparr>
 8. dg_prod I \<AA>\<lparr>Obj\<rparr> \<in>\<^sub>\<circ> Vset \<beta>
 9. dg_prod I \<AA>\<lparr>Arr\<rparr> \<in>\<^sub>\<circ> Vset \<beta>
[PROOF STEP]
show vsv_dg_prod_Dom: "vsv ((\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)\<lparr>Dom\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv (dg_prod I \<AA>\<lparr>Dom\<rparr>)
[PROOF STEP]
unfolding dg_prod_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv (\<lambda>f\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Arr\<rparr>. \<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Dom\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vsv (dg_prod I \<AA>\<lparr>Dom\<rparr>)

goal (8 subgoals):
 1. \<Z> \<beta>
 2. vsv (dg_prod I \<AA>\<lparr>Cod\<rparr>)
 3. \<D>\<^sub>\<circ> (dg_prod I \<AA>\<lparr>Dom\<rparr>) = dg_prod I \<AA>\<lparr>Arr\<rparr>
 4. \<R>\<^sub>\<circ> (dg_prod I \<AA>\<lparr>Dom\<rparr>) \<subseteq>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Obj\<rparr>
 5. \<D>\<^sub>\<circ> (dg_prod I \<AA>\<lparr>Cod\<rparr>) = dg_prod I \<AA>\<lparr>Arr\<rparr>
 6. \<R>\<^sub>\<circ> (dg_prod I \<AA>\<lparr>Cod\<rparr>) \<subseteq>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Obj\<rparr>
 7. dg_prod I \<AA>\<lparr>Obj\<rparr> \<in>\<^sub>\<circ> Vset \<beta>
 8. dg_prod I \<AA>\<lparr>Arr\<rparr> \<in>\<^sub>\<circ> Vset \<beta>
[PROOF STEP]
show vdomain_dg_prod_Dom: "\<D>\<^sub>\<circ> ((\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)\<lparr>Dom\<rparr>) = (\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (dg_prod I \<AA>\<lparr>Dom\<rparr>) = dg_prod I \<AA>\<lparr>Arr\<rparr>
[PROOF STEP]
unfolding dg_prod_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (\<lambda>f\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Arr\<rparr>. \<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Dom\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>) = (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Arr\<rparr>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> (dg_prod I \<AA>\<lparr>Dom\<rparr>) = dg_prod I \<AA>\<lparr>Arr\<rparr>

goal (7 subgoals):
 1. \<Z> \<beta>
 2. vsv (dg_prod I \<AA>\<lparr>Cod\<rparr>)
 3. \<R>\<^sub>\<circ> (dg_prod I \<AA>\<lparr>Dom\<rparr>) \<subseteq>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Obj\<rparr>
 4. \<D>\<^sub>\<circ> (dg_prod I \<AA>\<lparr>Cod\<rparr>) = dg_prod I \<AA>\<lparr>Arr\<rparr>
 5. \<R>\<^sub>\<circ> (dg_prod I \<AA>\<lparr>Cod\<rparr>) \<subseteq>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Obj\<rparr>
 6. dg_prod I \<AA>\<lparr>Obj\<rparr> \<in>\<^sub>\<circ> Vset \<beta>
 7. dg_prod I \<AA>\<lparr>Arr\<rparr> \<in>\<^sub>\<circ> Vset \<beta>
[PROOF STEP]
show "\<R>\<^sub>\<circ> ((\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)\<lparr>Dom\<rparr>) \<subseteq>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (dg_prod I \<AA>\<lparr>Dom\<rparr>) \<subseteq>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
by (rule vsubsetI)
      (
        metis
          dg_prod_Dom_app_in_Obj
          dg_prod_Dom_vdomain
          vsv.vrange_atE
          vsv_dg_prod_Dom
      )
[PROOF STATE]
proof (state)
this:
\<R>\<^sub>\<circ> (dg_prod I \<AA>\<lparr>Dom\<rparr>) \<subseteq>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Obj\<rparr>

goal (6 subgoals):
 1. \<Z> \<beta>
 2. vsv (dg_prod I \<AA>\<lparr>Cod\<rparr>)
 3. \<D>\<^sub>\<circ> (dg_prod I \<AA>\<lparr>Cod\<rparr>) = dg_prod I \<AA>\<lparr>Arr\<rparr>
 4. \<R>\<^sub>\<circ> (dg_prod I \<AA>\<lparr>Cod\<rparr>) \<subseteq>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Obj\<rparr>
 5. dg_prod I \<AA>\<lparr>Obj\<rparr> \<in>\<^sub>\<circ> Vset \<beta>
 6. dg_prod I \<AA>\<lparr>Arr\<rparr> \<in>\<^sub>\<circ> Vset \<beta>
[PROOF STEP]
show vsv_dg_prod_Cod: "vsv ((\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)\<lparr>Cod\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv (dg_prod I \<AA>\<lparr>Cod\<rparr>)
[PROOF STEP]
unfolding dg_prod_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv (\<lambda>f\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Arr\<rparr>. \<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Cod\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vsv (dg_prod I \<AA>\<lparr>Cod\<rparr>)

goal (5 subgoals):
 1. \<Z> \<beta>
 2. \<D>\<^sub>\<circ> (dg_prod I \<AA>\<lparr>Cod\<rparr>) = dg_prod I \<AA>\<lparr>Arr\<rparr>
 3. \<R>\<^sub>\<circ> (dg_prod I \<AA>\<lparr>Cod\<rparr>) \<subseteq>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Obj\<rparr>
 4. dg_prod I \<AA>\<lparr>Obj\<rparr> \<in>\<^sub>\<circ> Vset \<beta>
 5. dg_prod I \<AA>\<lparr>Arr\<rparr> \<in>\<^sub>\<circ> Vset \<beta>
[PROOF STEP]
show vdomain_dg_prod_Cod: "\<D>\<^sub>\<circ> ((\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)\<lparr>Cod\<rparr>) = (\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (dg_prod I \<AA>\<lparr>Cod\<rparr>) = dg_prod I \<AA>\<lparr>Arr\<rparr>
[PROOF STEP]
unfolding dg_prod_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (\<lambda>f\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Arr\<rparr>. \<lambda>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Cod\<rparr>\<lparr>f\<lparr>i\<rparr>\<rparr>) = (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Arr\<rparr>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> (dg_prod I \<AA>\<lparr>Cod\<rparr>) = dg_prod I \<AA>\<lparr>Arr\<rparr>

goal (4 subgoals):
 1. \<Z> \<beta>
 2. \<R>\<^sub>\<circ> (dg_prod I \<AA>\<lparr>Cod\<rparr>) \<subseteq>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Obj\<rparr>
 3. dg_prod I \<AA>\<lparr>Obj\<rparr> \<in>\<^sub>\<circ> Vset \<beta>
 4. dg_prod I \<AA>\<lparr>Arr\<rparr> \<in>\<^sub>\<circ> Vset \<beta>
[PROOF STEP]
show "\<R>\<^sub>\<circ> ((\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)\<lparr>Cod\<rparr>) \<subseteq>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (dg_prod I \<AA>\<lparr>Cod\<rparr>) \<subseteq>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
by (rule vsubsetI)
      (
        metis
          dg_prod_Cod_app_in_Obj
          vdomain_dg_prod_Cod
          vsv.vrange_atE
          vsv_dg_prod_Cod
      )
[PROOF STATE]
proof (state)
this:
\<R>\<^sub>\<circ> (dg_prod I \<AA>\<lparr>Cod\<rparr>) \<subseteq>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Obj\<rparr>

goal (3 subgoals):
 1. \<Z> \<beta>
 2. dg_prod I \<AA>\<lparr>Obj\<rparr> \<in>\<^sub>\<circ> Vset \<beta>
 3. dg_prod I \<AA>\<lparr>Arr\<rparr> \<in>\<^sub>\<circ> Vset \<beta>
[PROOF STEP]
qed
  (
    auto simp:
      dg_cs_intros
      assms
      pdg_dg_prod_Arr_in_Vset[OF assms(1,2)]
      pdg_dg_prod_Obj_in_Vset[OF assms(1,2)]
  )


[STATEMENT]
lemma (in pdigraph_base) pdg_tiny_digraph_dg_prod':
  "tiny_digraph (\<alpha> + \<omega>) (\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tiny_digraph (\<alpha> + \<omega>) (dg_prod I \<AA>)
[PROOF STEP]
by (rule pdg_tiny_digraph_dg_prod)
    (simp_all add: \<Z>_\<alpha>_\<alpha>\<omega> \<Z>.intro \<Z>_Limit_\<alpha>\<omega> \<Z>_\<omega>_\<alpha>\<omega>)