[STATEMENT]
lemma power_set_Suc2:
  "A *^ (Suc n) = A *^ n ** A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A *^ Suc n = A *^ n ** A
[PROOF STEP]
apply (induct_tac n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. A *^ Suc 0 = A *^ 0 ** A
 2. \<And>n. A *^ Suc n = A *^ n ** A \<Longrightarrow> A *^ Suc (Suc n) = A *^ Suc n ** A
[PROOF STEP]
apply (simp add: times_set_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. A *^ Suc n = A *^ n ** A \<Longrightarrow> A *^ Suc (Suc n) = A *^ Suc n ** A
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. A ** A *^ n = A *^ n ** A \<Longrightarrow> A ** (A *^ n ** A) = A *^ n ** A ** A
[PROOF STEP]
apply (subst times_set_assoc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. A ** A *^ n = A *^ n ** A \<Longrightarrow> A ** A *^ n ** A = A *^ n ** A ** A
[PROOF STEP]
by simp


[STATEMENT]
lemma Act\<^sub>\<alpha>_eq_iff: "Act\<^sub>\<alpha> \<alpha>1 t1 = Act\<^sub>\<alpha> \<alpha>2 t2 \<longleftrightarrow> tAct \<alpha>1 (rep_Tree\<^sub>\<alpha> t1) =\<^sub>\<alpha> tAct \<alpha>2 (rep_Tree\<^sub>\<alpha> t2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Act\<^sub>\<alpha> \<alpha>1 t1 = Act\<^sub>\<alpha> \<alpha>2 t2) = (tAct \<alpha>1 (rep_Tree\<^sub>\<alpha> t1) =\<^sub>\<alpha> tAct \<alpha>2 (rep_Tree\<^sub>\<alpha> t2))
[PROOF STEP]
by (metis Act\<^sub>\<alpha>.abs_eq Tree\<^sub>\<alpha>.abs_eq_iff Tree\<^sub>\<alpha>_abs_rep)


[STATEMENT]
lemma sorted_list_of_set_insert_remove_cons:
  assumes "finite A" "less_sets {a} A"
  shows "sorted_list_of_set (insert a A) = a # sorted_list_of_set A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted_list_of_set (insert a A) = a # sorted_list_of_set A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sorted_list_of_set (insert a A) = a # sorted_list_of_set A
[PROOF STEP]
have "strict_sorted (a # sorted_list_of_set A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strict_sorted (a # sorted_list_of_set A)
[PROOF STEP]
using assms less_setsD
[PROOF STATE]
proof (prove)
using this:
finite A
{a} \<lless> A
\<lbrakk>?A \<lless> ?B; ?a \<in> ?A; ?b \<in> ?B\<rbrakk> \<Longrightarrow> ?a < ?b

goal (1 subgoal):
 1. strict_sorted (a # sorted_list_of_set A)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
strict_sorted (a # sorted_list_of_set A)

goal (1 subgoal):
 1. sorted_list_of_set (insert a A) = a # sorted_list_of_set A
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
strict_sorted (a # sorted_list_of_set A)

goal (1 subgoal):
 1. sorted_list_of_set (insert a A) = a # sorted_list_of_set A
[PROOF STEP]
have "list.set (a # sorted_list_of_set A) = insert a A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list.set (a # sorted_list_of_set A) = insert a A
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite A
{a} \<lless> A

goal (1 subgoal):
 1. list.set (a # sorted_list_of_set A) = insert a A
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
list.set (a # sorted_list_of_set A) = insert a A

goal (1 subgoal):
 1. sorted_list_of_set (insert a A) = a # sorted_list_of_set A
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
list.set (a # sorted_list_of_set A) = insert a A

goal (1 subgoal):
 1. sorted_list_of_set (insert a A) = a # sorted_list_of_set A
[PROOF STEP]
have "length (a # sorted_list_of_set A) = card (insert a A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (a # sorted_list_of_set A) = card (insert a A)
[PROOF STEP]
using assms card_insert_if less_setsD
[PROOF STATE]
proof (prove)
using this:
finite A
{a} \<lless> A
finite ?A \<Longrightarrow> card (insert ?x ?A) = (if ?x \<in> ?A then card ?A else Suc (card ?A))
\<lbrakk>?A \<lless> ?B; ?a \<in> ?A; ?b \<in> ?B\<rbrakk> \<Longrightarrow> ?a < ?b

goal (1 subgoal):
 1. length (a # sorted_list_of_set A) = card (insert a A)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
length (a # sorted_list_of_set A) = card (insert a A)

goal (1 subgoal):
 1. sorted_list_of_set (insert a A) = a # sorted_list_of_set A
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
strict_sorted (a # sorted_list_of_set A)
list.set (a # sorted_list_of_set A) = insert a A
length (a # sorted_list_of_set A) = card (insert a A)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
strict_sorted (a # sorted_list_of_set A)
list.set (a # sorted_list_of_set A) = insert a A
length (a # sorted_list_of_set A) = card (insert a A)

goal (1 subgoal):
 1. sorted_list_of_set (insert a A) = a # sorted_list_of_set A
[PROOF STEP]
by (metis \<open>finite A\<close> finite_insert sorted_list_of_set_unique)
[PROOF STATE]
proof (state)
this:
sorted_list_of_set (insert a A) = a # sorted_list_of_set A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma non_empty_cycle_root_move_root_loop:
  assumes "non_empty_cycle_root r x"
      and "point q"
      and "q \<le> x\<^sup>\<star>;r"
    shows "q \<le> x\<^sup>+;q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q \<le> x\<^sup>+ ; q
[PROOF STEP]
using assms non_empty_cycle_root_loop_converse non_empty_cycle_root_move_root
[PROOF STATE]
proof (prove)
using this:
non_empty_cycle_root r x
point q
q \<le> x\<^sup>\<star> ; r
non_empty_cycle_root ?r ?x \<Longrightarrow> ?r \<le> ?x\<^sup>+ ; ?r
\<lbrakk>non_empty_cycle_root ?r ?x; point ?q; ?q \<le> ?x\<^sup>\<star> ; ?r\<rbrakk> \<Longrightarrow> non_empty_cycle_root ?q ?x

goal (1 subgoal):
 1. q \<le> x\<^sup>+ ; q
[PROOF STEP]
by blast


[STATEMENT]
lemma non_empty_cycle_root_move_root_forward:
  assumes "non_empty_cycle_root r x"
      and "point q"
      and "r \<le> x\<^sup>\<star>;q"
    shows "non_empty_cycle_root q x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. non_empty_cycle_root q x
[PROOF STEP]
by (metis assms backward_finite_path_root_move_root non_empty_cycle_root_no_start_end_points
          non_empty_cycle_root_point_exchange non_empty_cycle_root_rtc_start_points)


[STATEMENT]
lemma "Der_1b \<D> \<Longrightarrow> Der_3 \<D> \<Longrightarrow> MT1(\<^bold>\<not>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Der_1b \<D>; Fr_3 \<D>\<rbrakk> \<Longrightarrow> MT1 \<^bold>\<not>
[PROOF STEP]
unfolding Defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Der_1b \<D>; Fr_3 \<D>\<rbrakk> \<Longrightarrow> \<forall>a. contains (\<lambda>b. [\<^bold>\<turnstile> \<lambda>w. \<^bold>\<not> a w = \<^bold>\<top> w]) (\<lambda>b. contains (\<^bold>\<not> b) a \<and> [\<^bold>\<turnstile> \<lambda>w. b w = \<^bold>\<top> w])
[PROOF STEP]
by (metis (full_types) NOR_def PD1 bottom_def compl_def diff_def ineg_prop top_def)


[STATEMENT]
lemma valid_lists_subset: "xs \<in> valid_lists S G \<Longrightarrow> set xs \<subseteq> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<in> valid_lists S G \<Longrightarrow> set xs \<subseteq> S
[PROOF STEP]
by (induction rule: valid_lists.induct) auto


[STATEMENT]
lemma fmap_ball_all4':
  fixes
  Px :: "'c \<Rightarrow> 'd \<Rightarrow> 'e \<Rightarrow> 'f \<Rightarrow> bool" and
  P :: "'c \<Rightarrow> 'd \<Rightarrow> 'e \<Rightarrow> 'f \<Rightarrow> 'b option \<Rightarrow> ('a::finite) \<Rightarrow> bool"
  assumes
  "\<forall>l\<in>dom (f::('a -~> 'b)).
    \<forall>(x::'c) (y::'d) (z::'e) (a::'f). Px x y z a \<longrightarrow> P x y z a (f l) l"
  shows
  "\<forall>x y z a. Px x y z a \<longrightarrow> (\<forall>l\<in>dom f. P x y z a (f l) l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x y z a. Px x y z a \<longrightarrow> (\<forall>l\<in>dom f. P x y z a (f l) l)
[PROOF STEP]
proof (intro strip)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y z a l. \<lbrakk>Px x y z a; l \<in> dom f\<rbrakk> \<Longrightarrow> P x y z a (f l) l
[PROOF STEP]
fix x y z a l
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y z a l. \<lbrakk>Px x y z a; l \<in> dom f\<rbrakk> \<Longrightarrow> P x y z a (f l) l
[PROOF STEP]
assume "Px x y z a" and "l \<in> dom f"
[PROOF STATE]
proof (state)
this:
Px x y z a
l \<in> dom f

goal (1 subgoal):
 1. \<And>x y z a l. \<lbrakk>Px x y z a; l \<in> dom f\<rbrakk> \<Longrightarrow> P x y z a (f l) l
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
\<forall>l\<in>dom f. \<forall>x y z a. Px x y z a \<longrightarrow> P x y z a (f l) l
Px x y z a
l \<in> dom f
[PROOF STEP]
show "P x y z a (f l) l"
[PROOF STATE]
proof (prove)
using this:
\<forall>l\<in>dom f. \<forall>x y z a. Px x y z a \<longrightarrow> P x y z a (f l) l
Px x y z a
l \<in> dom f

goal (1 subgoal):
 1. P x y z a (f l) l
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
P x y z a (f l) l

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fast_ppoint_mult_even [simp]:
  "n \<noteq> 0 \<Longrightarrow> n mod 2 = 0 \<Longrightarrow>
   fast_ppoint_mult m a n p = mpdouble m a (fast_ppoint_mult m a (n div 2) p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<noteq> 0; n mod 2 = 0\<rbrakk> \<Longrightarrow> fast_ppoint_mult m a n p = mpdouble m a (fast_ppoint_mult m a (n div 2) p)
[PROOF STEP]
by simp


[STATEMENT]
lemma subst_idemE: "subst_idem \<sigma> \<Longrightarrow> subst_domain \<sigma> \<inter> range_vars \<sigma> = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst_idem \<sigma> \<Longrightarrow> subst_domain \<sigma> \<inter> range_vars \<sigma> = {}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. subst_idem \<sigma> \<Longrightarrow> subst_domain \<sigma> \<inter> range_vars \<sigma> = {}
[PROOF STEP]
assume "subst_idem \<sigma>"
[PROOF STATE]
proof (state)
this:
subst_idem \<sigma>

goal (1 subgoal):
 1. subst_idem \<sigma> \<Longrightarrow> subst_domain \<sigma> \<inter> range_vars \<sigma> = {}
[PROOF STEP]
hence "\<And>v. fv (\<sigma> v) \<inter> subst_domain \<sigma> = {}"
[PROOF STATE]
proof (prove)
using this:
subst_idem \<sigma>

goal (1 subgoal):
 1. \<And>v. fv (\<sigma> v) \<inter> subst_domain \<sigma> = {}
[PROOF STEP]
unfolding subst_idem_def subst_compose_def
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. \<sigma> x \<cdot> \<sigma>) = \<sigma>

goal (1 subgoal):
 1. \<And>v. fv (\<sigma> v) \<inter> subst_domain \<sigma> = {}
[PROOF STEP]
by (metis trm_subst_disj)
[PROOF STATE]
proof (state)
this:
fv (\<sigma> ?v) \<inter> subst_domain \<sigma> = {}

goal (1 subgoal):
 1. subst_idem \<sigma> \<Longrightarrow> subst_domain \<sigma> \<inter> range_vars \<sigma> = {}
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
fv (\<sigma> ?v) \<inter> subst_domain \<sigma> = {}

goal (1 subgoal):
 1. subst_domain \<sigma> \<inter> range_vars \<sigma> = {}
[PROOF STEP]
unfolding range_vars_alt_def
[PROOF STATE]
proof (prove)
using this:
fv (\<sigma> ?v) \<inter> subst_domain \<sigma> = {}

goal (1 subgoal):
 1. subst_domain \<sigma> \<inter> fv\<^sub>s\<^sub>e\<^sub>t (subst_range \<sigma>) = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subst_domain \<sigma> \<inter> range_vars \<sigma> = {}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bij_finite_ground_subst_exists:
  assumes "finite (S::'v set)" "infinite (U::('f,'v) term set)" "ground U"
  shows "\<exists>\<sigma>::('f,'v) subst. subst_domain \<sigma> = S
                          \<and> bij_betw \<sigma> (subst_domain \<sigma>) (subst_range \<sigma>)
                          \<and> subst_range \<sigma> \<subseteq> U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<sigma>. subst_domain \<sigma> = S \<and> bij_betw \<sigma> (subst_domain \<sigma>) (subst_range \<sigma>) \<and> subst_range \<sigma> \<subseteq> U
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>\<sigma>. subst_domain \<sigma> = S \<and> bij_betw \<sigma> (subst_domain \<sigma>) (subst_range \<sigma>) \<and> subst_range \<sigma> \<subseteq> U
[PROOF STEP]
obtain T' where "T' \<subseteq> U" "card T' = card S" "finite T'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>T'. \<lbrakk>T' \<subseteq> U; card T' = card S; finite T'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson assms(2) finite_Diff2 infinite_arbitrarily_large)
[PROOF STATE]
proof (state)
this:
T' \<subseteq> U
card T' = card S
finite T'

goal (1 subgoal):
 1. \<exists>\<sigma>. subst_domain \<sigma> = S \<and> bij_betw \<sigma> (subst_domain \<sigma>) (subst_range \<sigma>) \<and> subst_range \<sigma> \<subseteq> U
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
T' \<subseteq> U
card T' = card S
finite T'
[PROOF STEP]
obtain f::"'v \<Rightarrow> ('f,'v) term" where f_bij: "bij_betw f S T'"
[PROOF STATE]
proof (prove)
using this:
T' \<subseteq> U
card T' = card S
finite T'

goal (1 subgoal):
 1. (\<And>f. bij_betw f S T' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using finite_same_card_bij[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
T' \<subseteq> U
card T' = card S
finite T'
\<lbrakk>finite ?B; card S = card ?B\<rbrakk> \<Longrightarrow> \<exists>h. bij_betw h S ?B

goal (1 subgoal):
 1. (\<And>f. bij_betw f S T' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
bij_betw f S T'

goal (1 subgoal):
 1. \<exists>\<sigma>. subst_domain \<sigma> = S \<and> bij_betw \<sigma> (subst_domain \<sigma>) (subst_range \<sigma>) \<and> subst_range \<sigma> \<subseteq> U
[PROOF STEP]
hence *: "\<And>v. v \<in> S \<Longrightarrow> f v \<noteq> Var v"
[PROOF STATE]
proof (prove)
using this:
bij_betw f S T'

goal (1 subgoal):
 1. \<And>v. v \<in> S \<Longrightarrow> f v \<noteq> Var v
[PROOF STEP]
using \<open>ground U\<close> \<open>T' \<subseteq> U\<close> bij_betwE
[PROOF STATE]
proof (prove)
using this:
bij_betw f S T'
ground U
T' \<subseteq> U
bij_betw ?f ?A ?B \<Longrightarrow> \<forall>a\<in>?A. ?f a \<in> ?B

goal (1 subgoal):
 1. \<And>v. v \<in> S \<Longrightarrow> f v \<noteq> Var v
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
?v \<in> S \<Longrightarrow> f ?v \<noteq> Var ?v

goal (1 subgoal):
 1. \<exists>\<sigma>. subst_domain \<sigma> = S \<and> bij_betw \<sigma> (subst_domain \<sigma>) (subst_range \<sigma>) \<and> subst_range \<sigma> \<subseteq> U
[PROOF STEP]
let ?\<sigma> = "\<lambda>v. if v \<in> S then f v else Var v"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>\<sigma>. subst_domain \<sigma> = S \<and> bij_betw \<sigma> (subst_domain \<sigma>) (subst_range \<sigma>) \<and> subst_range \<sigma> \<subseteq> U
[PROOF STEP]
have "subst_domain ?\<sigma> = S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst_domain (\<lambda>v. if v \<in> S then f v else Var v) = S
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. subst_domain (\<lambda>v. if v \<in> S then f v else Var v) \<subseteq> S
 2. S \<subseteq> subst_domain (\<lambda>v. if v \<in> S then f v else Var v)
[PROOF STEP]
show "subst_domain ?\<sigma> \<subseteq> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst_domain (\<lambda>v. if v \<in> S then f v else Var v) \<subseteq> S
[PROOF STEP]
by (auto simp add: subst_domain_def)
[PROOF STATE]
proof (state)
this:
subst_domain (\<lambda>v. if v \<in> S then f v else Var v) \<subseteq> S

goal (1 subgoal):
 1. S \<subseteq> subst_domain (\<lambda>v. if v \<in> S then f v else Var v)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
subst_domain (\<lambda>v. if v \<in> S then f v else Var v) \<subseteq> S

goal (1 subgoal):
 1. S \<subseteq> subst_domain (\<lambda>v. if v \<in> S then f v else Var v)
[PROOF STEP]
fix v
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. S \<subseteq> subst_domain (\<lambda>v. if v \<in> S then f v else Var v)
[PROOF STEP]
assume "v \<in> S" "v \<notin> subst_domain ?\<sigma>"
[PROOF STATE]
proof (state)
this:
v \<in> S
v \<notin> subst_domain (\<lambda>v. if v \<in> S then f v else Var v)

goal (1 subgoal):
 1. S \<subseteq> subst_domain (\<lambda>v. if v \<in> S then f v else Var v)
[PROOF STEP]
hence "f v = Var v"
[PROOF STATE]
proof (prove)
using this:
v \<in> S
v \<notin> subst_domain (\<lambda>v. if v \<in> S then f v else Var v)

goal (1 subgoal):
 1. f v = Var v
[PROOF STEP]
by (simp add: subst_domain_def)
[PROOF STATE]
proof (state)
this:
f v = Var v

goal (1 subgoal):
 1. S \<subseteq> subst_domain (\<lambda>v. if v \<in> S then f v else Var v)
[PROOF STEP]
hence False
[PROOF STATE]
proof (prove)
using this:
f v = Var v

goal (1 subgoal):
 1. False
[PROOF STEP]
using *[OF \<open>v \<in> S\<close>]
[PROOF STATE]
proof (prove)
using this:
f v = Var v
f v \<noteq> Var v

goal (1 subgoal):
 1. False
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. S \<subseteq> subst_domain (\<lambda>v. if v \<in> S then f v else Var v)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?v2 \<in> S; ?v2 \<notin> subst_domain (\<lambda>v. if v \<in> S then f v else Var v)\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. S \<subseteq> subst_domain (\<lambda>v. if v \<in> S then f v else Var v)
[PROOF STEP]
thus "S \<subseteq> subst_domain ?\<sigma>"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?v2 \<in> S; ?v2 \<notin> subst_domain (\<lambda>v. if v \<in> S then f v else Var v)\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. S \<subseteq> subst_domain (\<lambda>v. if v \<in> S then f v else Var v)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
S \<subseteq> subst_domain (\<lambda>v. if v \<in> S then f v else Var v)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
subst_domain (\<lambda>v. if v \<in> S then f v else Var v) = S

goal (1 subgoal):
 1. \<exists>\<sigma>. subst_domain \<sigma> = S \<and> bij_betw \<sigma> (subst_domain \<sigma>) (subst_range \<sigma>) \<and> subst_range \<sigma> \<subseteq> U
[PROOF STEP]
hence "\<And>v w. \<lbrakk>v \<in> subst_domain ?\<sigma>; w \<notin> subst_domain ?\<sigma>\<rbrakk> \<Longrightarrow> ?\<sigma> w \<noteq> ?\<sigma> v"
[PROOF STATE]
proof (prove)
using this:
subst_domain (\<lambda>v. if v \<in> S then f v else Var v) = S

goal (1 subgoal):
 1. \<And>v w. \<lbrakk>v \<in> subst_domain (\<lambda>v. if v \<in> S then f v else Var v); w \<notin> subst_domain (\<lambda>v. if v \<in> S then f v else Var v)\<rbrakk> \<Longrightarrow> (if w \<in> S then f w else Var w) \<noteq> (if v \<in> S then f v else Var v)
[PROOF STEP]
using \<open>ground U\<close> bij_betwE[OF f_bij] set_rev_mp[OF _ \<open>T' \<subseteq> U\<close>]
[PROOF STATE]
proof (prove)
using this:
subst_domain (\<lambda>v. if v \<in> S then f v else Var v) = S
ground U
\<forall>a\<in>S. f a \<in> T'
?c \<in> T' \<Longrightarrow> ?c \<in> U

goal (1 subgoal):
 1. \<And>v w. \<lbrakk>v \<in> subst_domain (\<lambda>v. if v \<in> S then f v else Var v); w \<notin> subst_domain (\<lambda>v. if v \<in> S then f v else Var v)\<rbrakk> \<Longrightarrow> (if w \<in> S then f w else Var w) \<noteq> (if v \<in> S then f v else Var v)
[PROOF STEP]
by (metis (no_types, lifting) UN_iff empty_iff vars_iff_subterm_or_eq fv\<^sub>s\<^sub>e\<^sub>t.simps)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?v \<in> subst_domain (\<lambda>v. if v \<in> S then f v else Var v); ?w \<notin> subst_domain (\<lambda>v. if v \<in> S then f v else Var v)\<rbrakk> \<Longrightarrow> (if ?w \<in> S then f ?w else Var ?w) \<noteq> (if ?v \<in> S then f ?v else Var ?v)

goal (1 subgoal):
 1. \<exists>\<sigma>. subst_domain \<sigma> = S \<and> bij_betw \<sigma> (subst_domain \<sigma>) (subst_range \<sigma>) \<and> subst_range \<sigma> \<subseteq> U
[PROOF STEP]
hence "inj_on ?\<sigma> (subst_domain ?\<sigma>)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?v \<in> subst_domain (\<lambda>v. if v \<in> S then f v else Var v); ?w \<notin> subst_domain (\<lambda>v. if v \<in> S then f v else Var v)\<rbrakk> \<Longrightarrow> (if ?w \<in> S then f ?w else Var ?w) \<noteq> (if ?v \<in> S then f ?v else Var ?v)

goal (1 subgoal):
 1. inj_on (\<lambda>v. if v \<in> S then f v else Var v) (subst_domain (\<lambda>v. if v \<in> S then f v else Var v))
[PROOF STEP]
using f_bij \<open>subst_domain ?\<sigma> = S\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?v \<in> subst_domain (\<lambda>v. if v \<in> S then f v else Var v); ?w \<notin> subst_domain (\<lambda>v. if v \<in> S then f v else Var v)\<rbrakk> \<Longrightarrow> (if ?w \<in> S then f ?w else Var ?w) \<noteq> (if ?v \<in> S then f ?v else Var ?v)
bij_betw f S T'
subst_domain (\<lambda>v. if v \<in> S then f v else Var v) = S

goal (1 subgoal):
 1. inj_on (\<lambda>v. if v \<in> S then f v else Var v) (subst_domain (\<lambda>v. if v \<in> S then f v else Var v))
[PROOF STEP]
unfolding bij_betw_def inj_on_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?v \<in> subst_domain (\<lambda>v. if v \<in> S then f v else Var v); ?w \<notin> subst_domain (\<lambda>v. if v \<in> S then f v else Var v)\<rbrakk> \<Longrightarrow> (if ?w \<in> S then f ?w else Var ?w) \<noteq> (if ?v \<in> S then f ?v else Var ?v)
(\<forall>x\<in>S. \<forall>y\<in>S. f x = f y \<longrightarrow> x = y) \<and> f ` S = T'
subst_domain (\<lambda>v. if v \<in> S then f v else Var v) = S

goal (1 subgoal):
 1. \<forall>x\<in>subst_domain (\<lambda>v. if v \<in> S then f v else Var v). \<forall>y\<in>subst_domain (\<lambda>v. if v \<in> S then f v else Var v). (if x \<in> S then f x else Var x) = (if y \<in> S then f y else Var y) \<longrightarrow> x = y
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
inj_on (\<lambda>v. if v \<in> S then f v else Var v) (subst_domain (\<lambda>v. if v \<in> S then f v else Var v))

goal (1 subgoal):
 1. \<exists>\<sigma>. subst_domain \<sigma> = S \<and> bij_betw \<sigma> (subst_domain \<sigma>) (subst_range \<sigma>) \<and> subst_range \<sigma> \<subseteq> U
[PROOF STEP]
hence "bij_betw ?\<sigma> (subst_domain ?\<sigma>) (subst_range ?\<sigma>)"
[PROOF STATE]
proof (prove)
using this:
inj_on (\<lambda>v. if v \<in> S then f v else Var v) (subst_domain (\<lambda>v. if v \<in> S then f v else Var v))

goal (1 subgoal):
 1. bij_betw (\<lambda>v. if v \<in> S then f v else Var v) (subst_domain (\<lambda>v. if v \<in> S then f v else Var v)) (subst_range (\<lambda>v. if v \<in> S then f v else Var v))
[PROOF STEP]
using inj_on_imp_bij_betw[of ?\<sigma>]
[PROOF STATE]
proof (prove)
using this:
inj_on (\<lambda>v. if v \<in> S then f v else Var v) (subst_domain (\<lambda>v. if v \<in> S then f v else Var v))
inj_on (\<lambda>v. if v \<in> S then f v else Var v) ?A \<Longrightarrow> bij_betw (\<lambda>v. if v \<in> S then f v else Var v) ?A ((\<lambda>v. if v \<in> S then f v else Var v) ` ?A)

goal (1 subgoal):
 1. bij_betw (\<lambda>v. if v \<in> S then f v else Var v) (subst_domain (\<lambda>v. if v \<in> S then f v else Var v)) (subst_range (\<lambda>v. if v \<in> S then f v else Var v))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
bij_betw (\<lambda>v. if v \<in> S then f v else Var v) (subst_domain (\<lambda>v. if v \<in> S then f v else Var v)) (subst_range (\<lambda>v. if v \<in> S then f v else Var v))

goal (1 subgoal):
 1. \<exists>\<sigma>. subst_domain \<sigma> = S \<and> bij_betw \<sigma> (subst_domain \<sigma>) (subst_range \<sigma>) \<and> subst_range \<sigma> \<subseteq> U
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
bij_betw (\<lambda>v. if v \<in> S then f v else Var v) (subst_domain (\<lambda>v. if v \<in> S then f v else Var v)) (subst_range (\<lambda>v. if v \<in> S then f v else Var v))

goal (1 subgoal):
 1. \<exists>\<sigma>. subst_domain \<sigma> = S \<and> bij_betw \<sigma> (subst_domain \<sigma>) (subst_range \<sigma>) \<and> subst_range \<sigma> \<subseteq> U
[PROOF STEP]
have "subst_range ?\<sigma> = T'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst_range (\<lambda>v. if v \<in> S then f v else Var v) = T'
[PROOF STEP]
using \<open>bij_betw f S T'\<close> \<open>subst_domain ?\<sigma> = S\<close>
[PROOF STATE]
proof (prove)
using this:
bij_betw f S T'
subst_domain (\<lambda>v. if v \<in> S then f v else Var v) = S

goal (1 subgoal):
 1. subst_range (\<lambda>v. if v \<in> S then f v else Var v) = T'
[PROOF STEP]
unfolding bij_betw_def
[PROOF STATE]
proof (prove)
using this:
inj_on f S \<and> f ` S = T'
subst_domain (\<lambda>v. if v \<in> S then f v else Var v) = S

goal (1 subgoal):
 1. subst_range (\<lambda>v. if v \<in> S then f v else Var v) = T'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subst_range (\<lambda>v. if v \<in> S then f v else Var v) = T'

goal (1 subgoal):
 1. \<exists>\<sigma>. subst_domain \<sigma> = S \<and> bij_betw \<sigma> (subst_domain \<sigma>) (subst_range \<sigma>) \<and> subst_range \<sigma> \<subseteq> U
[PROOF STEP]
hence "subst_range ?\<sigma> \<subseteq> U"
[PROOF STATE]
proof (prove)
using this:
subst_range (\<lambda>v. if v \<in> S then f v else Var v) = T'

goal (1 subgoal):
 1. subst_range (\<lambda>v. if v \<in> S then f v else Var v) \<subseteq> U
[PROOF STEP]
using \<open>T' \<subseteq> U\<close>
[PROOF STATE]
proof (prove)
using this:
subst_range (\<lambda>v. if v \<in> S then f v else Var v) = T'
T' \<subseteq> U

goal (1 subgoal):
 1. subst_range (\<lambda>v. if v \<in> S then f v else Var v) \<subseteq> U
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subst_range (\<lambda>v. if v \<in> S then f v else Var v) \<subseteq> U

goal (1 subgoal):
 1. \<exists>\<sigma>. subst_domain \<sigma> = S \<and> bij_betw \<sigma> (subst_domain \<sigma>) (subst_range \<sigma>) \<and> subst_range \<sigma> \<subseteq> U
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
bij_betw (\<lambda>v. if v \<in> S then f v else Var v) (subst_domain (\<lambda>v. if v \<in> S then f v else Var v)) (subst_range (\<lambda>v. if v \<in> S then f v else Var v))
subst_range (\<lambda>v. if v \<in> S then f v else Var v) \<subseteq> U
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
bij_betw (\<lambda>v. if v \<in> S then f v else Var v) (subst_domain (\<lambda>v. if v \<in> S then f v else Var v)) (subst_range (\<lambda>v. if v \<in> S then f v else Var v))
subst_range (\<lambda>v. if v \<in> S then f v else Var v) \<subseteq> U

goal (1 subgoal):
 1. \<exists>\<sigma>. subst_domain \<sigma> = S \<and> bij_betw \<sigma> (subst_domain \<sigma>) (subst_range \<sigma>) \<and> subst_range \<sigma> \<subseteq> U
[PROOF STEP]
using \<open>subst_domain ?\<sigma> = S\<close>
[PROOF STATE]
proof (prove)
using this:
bij_betw (\<lambda>v. if v \<in> S then f v else Var v) (subst_domain (\<lambda>v. if v \<in> S then f v else Var v)) (subst_range (\<lambda>v. if v \<in> S then f v else Var v))
subst_range (\<lambda>v. if v \<in> S then f v else Var v) \<subseteq> U
subst_domain (\<lambda>v. if v \<in> S then f v else Var v) = S

goal (1 subgoal):
 1. \<exists>\<sigma>. subst_domain \<sigma> = S \<and> bij_betw \<sigma> (subst_domain \<sigma>) (subst_range \<sigma>) \<and> subst_range \<sigma> \<subseteq> U
[PROOF STEP]
by (metis (lifting))
[PROOF STATE]
proof (state)
this:
\<exists>\<sigma>. subst_domain \<sigma> = S \<and> bij_betw \<sigma> (subst_domain \<sigma>) (subst_range \<sigma>) \<and> subst_range \<sigma> \<subseteq> U

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma subterm_inj_on_alt_def:
    "subterm_inj_on f A \<longleftrightarrow>
     (inj_on f A \<and> (\<forall>s \<in> f`A. \<forall>u \<in> f`A. (\<exists>v. v \<sqsubseteq> s \<and> v \<sqsubseteq> u) \<longrightarrow> s = u))"
    (is "?A \<longleftrightarrow> ?B")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subterm_inj_on f A = (inj_on f A \<and> (\<forall>s\<in>f ` A. \<forall>u\<in>f ` A. (\<exists>v. v \<sqsubseteq> s \<and> v \<sqsubseteq> u) \<longrightarrow> s = u))
[PROOF STEP]
unfolding subterm_inj_on_def inj_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x\<in>A. \<forall>y\<in>A. (\<exists>v. v \<sqsubseteq> f x \<and> v \<sqsubseteq> f y) \<longrightarrow> x = y) = ((\<forall>x\<in>A. \<forall>y\<in>A. f x = f y \<longrightarrow> x = y) \<and> (\<forall>s\<in>f ` A. \<forall>u\<in>f ` A. (\<exists>v. v \<sqsubseteq> s \<and> v \<sqsubseteq> u) \<longrightarrow> s = u))
[PROOF STEP]
by fastforce


[STATEMENT]
lemma is_pure_iff_pure_assn: "is_pure P = (\<forall>x x'. is_pure_assn (P x x'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_pure P = (\<forall>x x'. is_pure_assn (P x x'))
[PROOF STEP]
unfolding is_pure_def is_pure_assn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>P'. \<forall>x x'. P x x' = \<up> (P' x x')) = (\<forall>x x'. \<exists>Pa. P x x' = \<up> Pa)
[PROOF STEP]
by metis


[STATEMENT]
lemma restrict_relp_cong:
  "\<lbrakk> P = P'; Q = Q'; \<And>x y. \<lbrakk> P x; Q y \<rbrakk> \<Longrightarrow> R x y = R' x y \<rbrakk> \<Longrightarrow> R \<upharpoonleft> P \<otimes> Q = R' \<upharpoonleft> P' \<otimes> Q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P = P'; Q = Q'; \<And>x y. \<lbrakk>P x; Q y\<rbrakk> \<Longrightarrow> R x y = R' x y\<rbrakk> \<Longrightarrow> R \<upharpoonleft> P \<otimes> Q = R' \<upharpoonleft> P' \<otimes> Q'
[PROOF STEP]
by(auto simp add: fun_eq_iff)


[STATEMENT]
lemma circline_set_conjugate_circline [simp]:
  shows "circline_set (conjugate_circline H) = conjugate ` circline_set H" (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. circline_set (conjugate_circline H) = conjugate ` circline_set H
[PROOF STEP]
proof (safe)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> circline_set (conjugate_circline H) \<Longrightarrow> x \<in> conjugate ` circline_set H
 2. \<And>x xa. xa \<in> circline_set H \<Longrightarrow> conjugate xa \<in> circline_set (conjugate_circline H)
[PROOF STEP]
fix z
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> circline_set (conjugate_circline H) \<Longrightarrow> x \<in> conjugate ` circline_set H
 2. \<And>x xa. xa \<in> circline_set H \<Longrightarrow> conjugate xa \<in> circline_set (conjugate_circline H)
[PROOF STEP]
assume "z \<in> ?lhs"
[PROOF STATE]
proof (state)
this:
z \<in> circline_set (conjugate_circline H)

goal (2 subgoals):
 1. \<And>x. x \<in> circline_set (conjugate_circline H) \<Longrightarrow> x \<in> conjugate ` circline_set H
 2. \<And>x xa. xa \<in> circline_set H \<Longrightarrow> conjugate xa \<in> circline_set (conjugate_circline H)
[PROOF STEP]
show "z \<in> ?rhs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z \<in> conjugate ` circline_set H
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. z = conjugate ?x
 2. ?x \<in> circline_set H
[PROOF STEP]
show "z = conjugate (conjugate z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z = conjugate (conjugate z)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
z = conjugate (conjugate z)

goal (1 subgoal):
 1. conjugate z \<in> circline_set H
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. conjugate z \<in> circline_set H
[PROOF STEP]
show "conjugate z \<in> circline_set H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. conjugate z \<in> circline_set H
[PROOF STEP]
using \<open>z \<in> circline_set (conjugate_circline H)\<close>
[PROOF STATE]
proof (prove)
using this:
z \<in> circline_set (conjugate_circline H)

goal (1 subgoal):
 1. conjugate z \<in> circline_set H
[PROOF STEP]
using conjugate_circline_set'[of "conjugate_circline H"]
[PROOF STATE]
proof (prove)
using this:
z \<in> circline_set (conjugate_circline H)
conjugate ` circline_set (conjugate_circline H) \<subseteq> circline_set (conjugate_circline (conjugate_circline H))

goal (1 subgoal):
 1. conjugate z \<in> circline_set H
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
conjugate z \<in> circline_set H

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
z \<in> conjugate ` circline_set H

goal (1 subgoal):
 1. \<And>x xa. xa \<in> circline_set H \<Longrightarrow> conjugate xa \<in> circline_set (conjugate_circline H)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa. xa \<in> circline_set H \<Longrightarrow> conjugate xa \<in> circline_set (conjugate_circline H)
[PROOF STEP]
fix z
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa. xa \<in> circline_set H \<Longrightarrow> conjugate xa \<in> circline_set (conjugate_circline H)
[PROOF STEP]
assume "z \<in> circline_set H"
[PROOF STATE]
proof (state)
this:
z \<in> circline_set H

goal (1 subgoal):
 1. \<And>x xa. xa \<in> circline_set H \<Longrightarrow> conjugate xa \<in> circline_set (conjugate_circline H)
[PROOF STEP]
thus "conjugate z \<in> circline_set (conjugate_circline H)"
[PROOF STATE]
proof (prove)
using this:
z \<in> circline_set H

goal (1 subgoal):
 1. conjugate z \<in> circline_set (conjugate_circline H)
[PROOF STEP]
using conjugate_circline_set'[of H]
[PROOF STATE]
proof (prove)
using this:
z \<in> circline_set H
conjugate ` circline_set H \<subseteq> circline_set (conjugate_circline H)

goal (1 subgoal):
 1. conjugate z \<in> circline_set (conjugate_circline H)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
conjugate z \<in> circline_set (conjugate_circline H)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma trans_path_non_nil: "ps \<noteq> [] \<Longrightarrow> trans_path (k\<^sub>1,k\<^sub>2) ps \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ps \<noteq> [] \<Longrightarrow> trans_path (k\<^sub>1, k\<^sub>2) ps \<noteq> []
[PROOF STEP]
by (induction ps) auto


[STATEMENT]
lemma cka_1: "(x \<cdot> y)\<^sup>\<star> \<le> x\<^sup>\<star> \<cdot> y\<^sup>\<star>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<cdot> y)\<^sup>\<star> \<le> x\<^sup>\<star> \<cdot> y\<^sup>\<star>
[PROOF STEP]
by (metis conway_c3 star_invol star_iso star_subdist_var_2)


[STATEMENT]
lemma nres_relD: "(c,a)\<in>\<langle>R\<rangle>nres_rel \<Longrightarrow> c \<le>\<Down>R a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (c, a) \<in> \<langle>R\<rangle>nres_rel \<Longrightarrow> c \<le> \<Down> R a
[PROOF STEP]
by (simp add: nres_rel_def)


[STATEMENT]
lemma nu_iso: "x \<le> y \<Longrightarrow> \<nu> x \<le> \<nu> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> y \<Longrightarrow> \<nu> x \<le> \<nu> y
[PROOF STEP]
using local.inf_mono nu_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?a \<le> ?c; ?b \<le> ?d\<rbrakk> \<Longrightarrow> ?a \<sqinter> ?b \<le> ?c \<sqinter> ?d
\<nu> ?x = ?x \<sqinter> nc

goal (1 subgoal):
 1. x \<le> y \<Longrightarrow> \<nu> x \<le> \<nu> y
[PROOF STEP]
by auto


[STATEMENT]
lemma (in is_functor) op_cf_obj_comma_ArrMap_vdomain[cat_comma_cs_simps]:
  "\<D>\<^sub>\<circ> (op_cf_obj_comma \<FF> b\<lparr>ArrMap\<rparr>) = \<FF> \<^sub>C\<^sub>F\<down> b\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (op_cf_obj_comma \<FF> b\<lparr>ArrMap\<rparr>) = \<FF> \<^sub>C\<^sub>F\<down> b\<lparr>Arr\<rparr>
[PROOF STEP]
unfolding op_cf_obj_comma_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (op_cf_comma \<FF> (dghm_const (cat_1 []\<^sub>\<circ> []\<^sub>\<circ>) \<BB> b (\<BB>\<lparr>CId\<rparr>\<lparr>b\<rparr>))\<lparr>ArrMap\<rparr>) = \<FF> \<^sub>C\<^sub>F\<down> b\<lparr>Arr\<rparr>
[PROOF STEP]
by
    (
      cs_concl cs_shallow
        cs_simp: cat_comma_cs_simps cat_cf_obj_comma_def[symmetric]
    )


[STATEMENT]
lemma dgrad_set_subset:
  assumes "m \<le> n"
  shows "dgrad_set d m \<subseteq> dgrad_set d n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dgrad_set d m \<subseteq> dgrad_set d n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
m \<le> n

goal (1 subgoal):
 1. dgrad_set d m \<subseteq> dgrad_set d n
[PROOF STEP]
by (auto simp: dgrad_set_def)


[STATEMENT]
lemma ladder_cut_prefix_i:
  assumes index_bound: "index < length L"
  assumes length_L: "length L > 0"
  shows "ladder_i (ladder_cut_prefix d L) index = ladder_i L index - d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ladder_i (ladder_cut_prefix d L) index = ladder_i L index - d
[PROOF STEP]
apply (simp add: ladder_i_def ladder_cut_prefix_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (index = 0 \<longrightarrow> deriv_i (hd ((ladder_shift_j d L)[0 := (ladder_n L 0, ladder_j L 0 - d, deriv_i (hd L) - d)])) = deriv_i (hd L) - d) \<and> (0 < index \<longrightarrow> ladder_j ((ladder_shift_j d L)[0 := (ladder_n L 0, ladder_j L 0 - d, deriv_i (hd L) - d)]) (index - Suc 0) = ladder_j L (index - Suc 0) - d)
[PROOF STEP]
apply (cases index)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. index = 0 \<Longrightarrow> (index = 0 \<longrightarrow> deriv_i (hd ((ladder_shift_j d L)[0 := (ladder_n L 0, ladder_j L 0 - d, deriv_i (hd L) - d)])) = deriv_i (hd L) - d) \<and> (0 < index \<longrightarrow> ladder_j ((ladder_shift_j d L)[0 := (ladder_n L 0, ladder_j L 0 - d, deriv_i (hd L) - d)]) (index - Suc 0) = ladder_j L (index - Suc 0) - d)
 2. \<And>nat. index = Suc nat \<Longrightarrow> (index = 0 \<longrightarrow> deriv_i (hd ((ladder_shift_j d L)[0 := (ladder_n L 0, ladder_j L 0 - d, deriv_i (hd L) - d)])) = deriv_i (hd L) - d) \<and> (0 < index \<longrightarrow> ladder_j ((ladder_shift_j d L)[0 := (ladder_n L 0, ladder_j L 0 - d, deriv_i (hd L) - d)]) (index - Suc 0) = ladder_j L (index - Suc 0) - d)
[PROOF STEP]
apply auto[1]
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. index = 0 \<Longrightarrow> deriv_i (hd ((ladder_shift_j d L)[0 := (ladder_n L 0, ladder_j L 0 - d, deriv_i (hd L) - d)])) = deriv_i (hd L) - d
 2. \<And>nat. index = Suc nat \<Longrightarrow> (index = 0 \<longrightarrow> deriv_i (hd ((ladder_shift_j d L)[0 := (ladder_n L 0, ladder_j L 0 - d, deriv_i (hd L) - d)])) = deriv_i (hd L) - d) \<and> (0 < index \<longrightarrow> ladder_j ((ladder_shift_j d L)[0 := (ladder_n L 0, ladder_j L 0 - d, deriv_i (hd L) - d)]) (index - Suc 0) = ladder_j L (index - Suc 0) - d)
[PROOF STEP]
apply (subst hd_0_subst)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. index = 0 \<Longrightarrow> 0 < length (ladder_shift_j d L)
 2. index = 0 \<Longrightarrow> deriv_i (ladder_n L 0, ladder_j L 0 - d, deriv_i (hd L) - d) = deriv_i (hd L) - d
 3. \<And>nat. index = Suc nat \<Longrightarrow> (index = 0 \<longrightarrow> deriv_i (hd ((ladder_shift_j d L)[0 := (ladder_n L 0, ladder_j L 0 - d, deriv_i (hd L) - d)])) = deriv_i (hd L) - d) \<and> (0 < index \<longrightarrow> ladder_j ((ladder_shift_j d L)[0 := (ladder_n L 0, ladder_j L 0 - d, deriv_i (hd L) - d)]) (index - Suc 0) = ladder_j L (index - Suc 0) - d)
[PROOF STEP]
using length_L ladder_shift_j_length
[PROOF STATE]
proof (prove)
using this:
0 < length L
length (ladder_shift_j ?d ?L) = length ?L

goal (3 subgoals):
 1. index = 0 \<Longrightarrow> 0 < length (ladder_shift_j d L)
 2. index = 0 \<Longrightarrow> deriv_i (ladder_n L 0, ladder_j L 0 - d, deriv_i (hd L) - d) = deriv_i (hd L) - d
 3. \<And>nat. index = Suc nat \<Longrightarrow> (index = 0 \<longrightarrow> deriv_i (hd ((ladder_shift_j d L)[0 := (ladder_n L 0, ladder_j L 0 - d, deriv_i (hd L) - d)])) = deriv_i (hd L) - d) \<and> (0 < index \<longrightarrow> ladder_j ((ladder_shift_j d L)[0 := (ladder_n L 0, ladder_j L 0 - d, deriv_i (hd L) - d)]) (index - Suc 0) = ladder_j L (index - Suc 0) - d)
[PROOF STEP]
apply metis
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. index = 0 \<Longrightarrow> deriv_i (ladder_n L 0, ladder_j L 0 - d, deriv_i (hd L) - d) = deriv_i (hd L) - d
 2. \<And>nat. index = Suc nat \<Longrightarrow> (index = 0 \<longrightarrow> deriv_i (hd ((ladder_shift_j d L)[0 := (ladder_n L 0, ladder_j L 0 - d, deriv_i (hd L) - d)])) = deriv_i (hd L) - d) \<and> (0 < index \<longrightarrow> ladder_j ((ladder_shift_j d L)[0 := (ladder_n L 0, ladder_j L 0 - d, deriv_i (hd L) - d)]) (index - Suc 0) = ladder_j L (index - Suc 0) - d)
[PROOF STEP]
apply (auto simp add: deriv_i_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>nat. index = Suc nat \<Longrightarrow> ladder_j ((ladder_shift_j d L)[0 := (ladder_n L 0, ladder_j L 0 - d, snd (snd (hd L)) - d)]) nat = ladder_j L nat - d
[PROOF STEP]
apply (case_tac nat)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>nat. \<lbrakk>index = Suc nat; nat = 0\<rbrakk> \<Longrightarrow> ladder_j ((ladder_shift_j d L)[0 := (ladder_n L 0, ladder_j L 0 - d, snd (snd (hd L)) - d)]) nat = ladder_j L nat - d
 2. \<And>nat nata. \<lbrakk>index = Suc nat; nat = Suc nata\<rbrakk> \<Longrightarrow> ladder_j ((ladder_shift_j d L)[0 := (ladder_n L 0, ladder_j L 0 - d, snd (snd (hd L)) - d)]) nat = ladder_j L nat - d
[PROOF STEP]
apply (simp add: ladder_j_def deriv_j_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>nat. \<lbrakk>index = Suc 0; nat = 0\<rbrakk> \<Longrightarrow> fst (snd ((ladder_shift_j d L)[0 := (ladder_n L 0, fst (snd (L ! 0)) - d, snd (snd (hd L)) - d)] ! 0)) = fst (snd (L ! 0)) - d
 2. \<And>nat nata. \<lbrakk>index = Suc nat; nat = Suc nata\<rbrakk> \<Longrightarrow> ladder_j ((ladder_shift_j d L)[0 := (ladder_n L 0, ladder_j L 0 - d, snd (snd (hd L)) - d)]) nat = ladder_j L nat - d
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. index = Suc 0 \<Longrightarrow> fst (snd ((ladder_shift_j d L)[0 := (ladder_n L 0, fst (snd (L ! 0)) - d, snd (snd (hd L)) - d)] ! 0)) = fst (snd (L ! 0)) - d
 2. \<And>nata. index = Suc (Suc nata) \<Longrightarrow> ladder_j ((ladder_shift_j d L)[0 := (ladder_n L 0, ladder_j L 0 - d, snd (snd (hd L)) - d)]) (Suc nata) = ladder_j L (Suc nata) - d
[PROOF STEP]
apply (subst nth_list_update_eq)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. index = Suc 0 \<Longrightarrow> 0 < length (ladder_shift_j d L)
 2. index = Suc 0 \<Longrightarrow> fst (snd (ladder_n L 0, fst (snd (L ! 0)) - d, snd (snd (hd L)) - d)) = fst (snd (L ! 0)) - d
 3. \<And>nata. index = Suc (Suc nata) \<Longrightarrow> ladder_j ((ladder_shift_j d L)[0 := (ladder_n L 0, ladder_j L 0 - d, snd (snd (hd L)) - d)]) (Suc nata) = ladder_j L (Suc nata) - d
[PROOF STEP]
using length_L ladder_shift_j_length
[PROOF STATE]
proof (prove)
using this:
0 < length L
length (ladder_shift_j ?d ?L) = length ?L

goal (3 subgoals):
 1. index = Suc 0 \<Longrightarrow> 0 < length (ladder_shift_j d L)
 2. index = Suc 0 \<Longrightarrow> fst (snd (ladder_n L 0, fst (snd (L ! 0)) - d, snd (snd (hd L)) - d)) = fst (snd (L ! 0)) - d
 3. \<And>nata. index = Suc (Suc nata) \<Longrightarrow> ladder_j ((ladder_shift_j d L)[0 := (ladder_n L 0, ladder_j L 0 - d, snd (snd (hd L)) - d)]) (Suc nata) = ladder_j L (Suc nata) - d
[PROOF STEP]
apply auto[1]
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. index = Suc 0 \<Longrightarrow> fst (snd (ladder_n L 0, fst (snd (L ! 0)) - d, snd (snd (hd L)) - d)) = fst (snd (L ! 0)) - d
 2. \<And>nata. index = Suc (Suc nata) \<Longrightarrow> ladder_j ((ladder_shift_j d L)[0 := (ladder_n L 0, ladder_j L 0 - d, snd (snd (hd L)) - d)]) (Suc nata) = ladder_j L (Suc nata) - d
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>nata. index = Suc (Suc nata) \<Longrightarrow> ladder_j ((ladder_shift_j d L)[0 := (ladder_n L 0, ladder_j L 0 - d, snd (snd (hd L)) - d)]) (Suc nata) = ladder_j L (Suc nata) - d
[PROOF STEP]
apply (simp add: ladder_j_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>nata. index = Suc (Suc nata) \<Longrightarrow> deriv_j (ladder_shift_j d L ! Suc nata) = deriv_j (L ! Suc nata) - d
[PROOF STEP]
apply (subst deriv_j_ladder_shift_j)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>nata. index = Suc (Suc nata) \<Longrightarrow> Suc nata < length L
 2. \<And>nata. index = Suc (Suc nata) \<Longrightarrow> deriv_j (L ! Suc nata) - d = deriv_j (L ! Suc nata) - d
[PROOF STEP]
using index_bound
[PROOF STATE]
proof (prove)
using this:
index < length L

goal (2 subgoals):
 1. \<And>nata. index = Suc (Suc nata) \<Longrightarrow> Suc nata < length L
 2. \<And>nata. index = Suc (Suc nata) \<Longrightarrow> deriv_j (L ! Suc nata) - d = deriv_j (L ! Suc nata) - d
[PROOF STEP]
apply arith
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>nata. index = Suc (Suc nata) \<Longrightarrow> deriv_j (L ! Suc nata) - d = deriv_j (L ! Suc nata) - d
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma successor_is_node[elim]: "\<lbrakk>n \<in> set (predecessors g n'); n \<in> set (\<alpha>n g); invar g\<rbrakk> \<Longrightarrow> n' \<in> set (\<alpha>n g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<in> set (predecessors g n'); n \<in> set (\<alpha>n g); invar g\<rbrakk> \<Longrightarrow> n' \<in> set (\<alpha>n g)
[PROOF STEP]
unfolding predecessors_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<in> set (map getFrom (inEdges g n')); n \<in> set (\<alpha>n g); invar g\<rbrakk> \<Longrightarrow> n' \<in> set (\<alpha>n g)
[PROOF STEP]
by (fastforce intro: rev_image_eqI)


[STATEMENT]
lemma seq_cont_Sup_distl:
    assumes "P is \<H>" "A \<subseteq> \<lbrakk>\<H>\<rbrakk>\<^sub>H" "A \<noteq> {}"
    shows "P ;; (\<^bold>\<Sqinter> A) = \<^bold>\<Sqinter> {P ;; Q | Q. Q \<in> A }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P ;; \<^bold>\<Sqinter>A = \<^bold>\<Sqinter>{uu_. \<exists>Q. uu_ = P ;; Q \<and> Q \<in> A}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P ;; \<^bold>\<Sqinter>A = \<^bold>\<Sqinter>{uu_. \<exists>Q. uu_ = P ;; Q \<and> Q \<in> A}
[PROOF STEP]
have "{P ;; Q | Q. Q \<in> A } \<subseteq> \<lbrakk>\<H>\<rbrakk>\<^sub>H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {uu_. \<exists>Q. uu_ = P ;; Q \<and> Q \<in> A} \<subseteq> \<lbrakk>\<H>\<rbrakk>\<^sub>H
[PROOF STEP]
using Healthy_Sequence assms(1) assms(2)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?P is \<H>; ?Q is \<H>\<rbrakk> \<Longrightarrow> ?P ;; ?Q is \<H>
P is \<H>
A \<subseteq> \<lbrakk>\<H>\<rbrakk>\<^sub>H

goal (1 subgoal):
 1. {uu_. \<exists>Q. uu_ = P ;; Q \<and> Q \<in> A} \<subseteq> \<lbrakk>\<H>\<rbrakk>\<^sub>H
[PROOF STEP]
by (auto)
[PROOF STATE]
proof (state)
this:
{uu_. \<exists>Q. uu_ = P ;; Q \<and> Q \<in> A} \<subseteq> \<lbrakk>\<H>\<rbrakk>\<^sub>H

goal (1 subgoal):
 1. P ;; \<^bold>\<Sqinter>A = \<^bold>\<Sqinter>{uu_. \<exists>Q. uu_ = P ;; Q \<and> Q \<in> A}
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
{uu_. \<exists>Q. uu_ = P ;; Q \<and> Q \<in> A} \<subseteq> \<lbrakk>\<H>\<rbrakk>\<^sub>H

goal (1 subgoal):
 1. P ;; \<^bold>\<Sqinter>A = \<^bold>\<Sqinter>{uu_. \<exists>Q. uu_ = P ;; Q \<and> Q \<in> A}
[PROOF STEP]
by (simp add: healthy_inf_cont seq_Sup_distl setcompr_eq_image assms)
[PROOF STATE]
proof (state)
this:
P ;; \<^bold>\<Sqinter>A = \<^bold>\<Sqinter>{uu_. \<exists>Q. uu_ = P ;; Q \<and> Q \<in> A}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pgallery_least_length:
  assumes "chamber C" "chamber D" "C\<noteq>D"
  defines "Cs \<equiv> ARG_MIN length Cs. gallery (C#Cs@[D])"
  shows   "pgallery (C#Cs@[D])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pgallery (C # Cs @ [D])
[PROOF STEP]
using   assms min_gallery_least_length min_gallery_pgallery
[PROOF STATE]
proof (prove)
using this:
chamber C
chamber D
C \<noteq> D
Cs \<equiv> ARG_MIN length Cs. gallery (C # Cs @ [D])
\<lbrakk>chamber ?C; chamber ?D; ?C \<noteq> ?D\<rbrakk> \<Longrightarrow> min_gallery (?C # (ARG_MIN length Cs. gallery (?C # Cs @ [?D])) @ [?D])
min_gallery ?xs \<Longrightarrow> pgallery ?xs

goal (1 subgoal):
 1. pgallery (C # Cs @ [D])
[PROOF STEP]
by      fast


[STATEMENT]
lemma coherent_Lunit'_Ide:
    assumes "Ide a"
    shows "coherent \<^bold>\<l>\<^sup>-\<^sup>1\<^bold>[a\<^bold>]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coherent \<^bold>\<l>\<^sup>-\<^sup>1\<^bold>[a\<^bold>]
[PROOF STEP]
using assms Ide_implies_Can coherent_Lunit_Ide
            coherent_iff_coherent_Inv [of "Lunit a"]
[PROOF STATE]
proof (prove)
using this:
Ide a
Ide ?t \<Longrightarrow> Can ?t
Ide ?t \<Longrightarrow> coherent \<^bold>\<l>\<^bold>[?t\<^bold>]
Can \<^bold>\<l>\<^bold>[a\<^bold>] \<Longrightarrow> coherent \<^bold>\<l>\<^bold>[a\<^bold>] = coherent (Inv \<^bold>\<l>\<^bold>[a\<^bold>])

goal (1 subgoal):
 1. coherent \<^bold>\<l>\<^sup>-\<^sup>1\<^bold>[a\<^bold>]
[PROOF STEP]
by simp


[STATEMENT]
lemma comp_arr_point\<^sub>S\<^sub>C:
    assumes "arr f" and "\<guillemotleft>x : unity \<rightarrow> dom f\<guillemotright>"
    shows "f \<cdot> x = inv_into (hom unity (cod f)) img (Fun f (img x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<cdot> x = inv_into (hom unity (cod f)) img (Fun f (img x))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f \<cdot> x = inv_into (hom unity (cod f)) img (Fun f (img x))
[PROOF STEP]
have "\<guillemotleft>f \<cdot> x : unity \<rightarrow> cod f\<guillemotright>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<guillemotleft>f \<cdot> x : unity \<rightarrow> cod f\<guillemotright>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
arr f
\<guillemotleft>x : unity \<rightarrow> local.dom f\<guillemotright>

goal (1 subgoal):
 1. \<guillemotleft>f \<cdot> x : unity \<rightarrow> cod f\<guillemotright>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<guillemotleft>f \<cdot> x : unity \<rightarrow> cod f\<guillemotright>

goal (1 subgoal):
 1. f \<cdot> x = inv_into (hom unity (cod f)) img (Fun f (img x))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<guillemotleft>f \<cdot> x : unity \<rightarrow> cod f\<guillemotright>

goal (1 subgoal):
 1. f \<cdot> x = inv_into (hom unity (cod f)) img (Fun f (img x))
[PROOF STEP]
using assms Fun_def inj_img set_def
[PROOF STATE]
proof (prove)
using this:
\<guillemotleft>f \<cdot> x : unity \<rightarrow> cod f\<guillemotright>
arr f
\<guillemotleft>x : unity \<rightarrow> local.dom f\<guillemotright>
Fun ?f = restrict (img \<circ> (\<cdot>) ?f \<circ> inv_into (hom unity (local.dom ?f)) img) (local.set (local.dom ?f))
ide ?a \<Longrightarrow> inj_on img (hom unity ?a)
local.set ?a = img ` hom unity ?a

goal (1 subgoal):
 1. f \<cdot> x = inv_into (hom unity (cod f)) img (Fun f (img x))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f \<cdot> x = inv_into (hom unity (cod f)) img (Fun f (img x))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Fun_incl:
    assumes "incl f"
    shows "Fun f = (\<lambda>x \<in> set (dom f). x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Fun f = (\<lambda>x\<in>local.set (local.dom f). x)
[PROOF STEP]
using assms incl_def
[PROOF STATE]
proof (prove)
using this:
incl f
incl ?f = (arr ?f \<and> local.set (local.dom ?f) \<subseteq> local.set (cod ?f) \<and> ?f = mkArr (local.set (local.dom ?f)) (local.set (cod ?f)) (\<lambda>x. x))

goal (1 subgoal):
 1. Fun f = (\<lambda>x\<in>local.set (local.dom f). x)
[PROOF STEP]
by (metis Fun_mkArr)


[STATEMENT]
lemma desargues_config_2D_rkABPa_rkABPb_rkABPc :
  assumes "desargues_config_2D A B C A' B' C' P \<alpha> \<beta> \<gamma>" and "rk {A, B, C, A', B', C', P, Q} \<ge> 4"
and "rk {P, Q, R} = 2" and "rk {P, R} = 2" and "rk {A', P} = 2" and "rk {B', P} = 2" and
"rk {Q, A', a} = 2" and "rk {R, A, a} = 2" and "rk {Q, B', b} = 2" and "rk {R, B, b} = 2" and
"rk {Q, C', c} = 2" and "rk {R, C, c} = 2"
  shows "rk {A, B, P, a} \<ge> 4" and "rk {A, B, P, b} \<ge> 4" and "rk {A, B, P, c} \<ge> 4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 4 \<le> rk {A, B, P, a} &&& 4 \<le> rk {A, B, P, b} &&& 4 \<le> rk {A, B, P, c}
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. 4 \<le> rk {A, B, P, a}
 2. 4 \<le> rk {A, B, P, b}
 3. 4 \<le> rk {A, B, P, c}
[PROOF STEP]
have f1:"rk {A, B, C, A', B', C', P} = 3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rk {A, B, C, A', B', C', P} = 3
[PROOF STEP]
using assms(1) desargues_config_2D_def[of A B C A' B' C' P \<alpha> \<beta> \<gamma>] coplanar_ABCA'B'C'P
[PROOF STATE]
proof (prove)
using this:
desargues_config_2D A B C A' B' C' P \<alpha> \<beta> \<gamma>
desargues_config_2D A B C A' B' C' P \<alpha> \<beta> \<gamma> \<equiv> rk {A, B, C} = 3 \<and> rk {A', B', C'} = 3 \<and> rk {A, A', P} = 2 \<and> rk {B, B', P} = 2 \<and> rk {C, C', P} = 2 \<and> rk {A, B, \<gamma>} = 2 \<and> rk {A', B', \<gamma>} = 2 \<and> rk {A, C, \<beta>} = 2 \<and> rk {A', C', \<beta>} = 2 \<and> rk {B, C, \<alpha>} = 2 \<and> rk {B', C', \<alpha>} = 2 \<and> rk {A, B, C, A', B', C'} = 3 \<and> rk {A, B, P} = 3 \<and> rk {A, C, P} = 3 \<and> rk {B, C, P} = 3 \<and> rk {A, A'} = 2 \<and> rk {B, B'} = 2 \<and> rk {C, C'} = 2
\<lbrakk>rk {?A, ?A'} = 2; rk {?A, ?B, ?C, ?A', ?B', ?C'} = 3; rk {?A, ?A', ?P} = 2\<rbrakk> \<Longrightarrow> rk {?A, ?B, ?C, ?A', ?B', ?C', ?P} = 3

goal (1 subgoal):
 1. rk {A, B, C, A', B', C', P} = 3
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rk {A, B, C, A', B', C', P} = 3

goal (3 subgoals):
 1. 4 \<le> rk {A, B, P, a}
 2. 4 \<le> rk {A, B, P, b}
 3. 4 \<le> rk {A, B, P, c}
[PROOF STEP]
have f2:"rk {A', B', P, Q} = 4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rk {A', B', P, Q} = 4
[PROOF STEP]
using assms(1) desargues_config_2D_def[of A B C A' B' C' P \<alpha> \<beta> \<gamma>] assms(2) assms(5) assms(6)
      rk_A'B'PQ[of "A" "A'" "B" "C" "B'" "C'" "P" "Q"]
[PROOF STATE]
proof (prove)
using this:
desargues_config_2D A B C A' B' C' P \<alpha> \<beta> \<gamma>
desargues_config_2D A B C A' B' C' P \<alpha> \<beta> \<gamma> \<equiv> rk {A, B, C} = 3 \<and> rk {A', B', C'} = 3 \<and> rk {A, A', P} = 2 \<and> rk {B, B', P} = 2 \<and> rk {C, C', P} = 2 \<and> rk {A, B, \<gamma>} = 2 \<and> rk {A', B', \<gamma>} = 2 \<and> rk {A, C, \<beta>} = 2 \<and> rk {A', C', \<beta>} = 2 \<and> rk {B, C, \<alpha>} = 2 \<and> rk {B', C', \<alpha>} = 2 \<and> rk {A, B, C, A', B', C'} = 3 \<and> rk {A, B, P} = 3 \<and> rk {A, C, P} = 3 \<and> rk {B, C, P} = 3 \<and> rk {A, A'} = 2 \<and> rk {B, B'} = 2 \<and> rk {C, C'} = 2
4 \<le> rk {A, B, C, A', B', C', P, Q}
rk {A', P} = 2
rk {B', P} = 2
\<lbrakk>rk {A, A'} = 2; rk {A, B, C, A', B', C'} = 3; rk {A, A', P} = 2; rk {A, B, P} = 3; rk {B, B', P} = 2; rk {A', P} = 2; rk {B', P} = 2; 4 \<le> rk {A, B, C, A', B', C', P, Q}\<rbrakk> \<Longrightarrow> rk {A', B', P, Q} = 4

goal (1 subgoal):
 1. rk {A', B', P, Q} = 4
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rk {A', B', P, Q} = 4

goal (3 subgoals):
 1. 4 \<le> rk {A, B, P, a}
 2. 4 \<le> rk {A, B, P, b}
 3. 4 \<le> rk {A, B, P, c}
[PROOF STEP]
show "rk {A, B, P, a} \<ge> 4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 4 \<le> rk {A, B, P, a}
[PROOF STEP]
using f1 f2 assms(1) desargues_config_2D_def[of A B C A' B' C' P \<alpha> \<beta> \<gamma>] assms(7) assms(2) assms(3)
      assms(4) assms(8) rk_ABPa
[PROOF STATE]
proof (prove)
using this:
rk {A, B, C, A', B', C', P} = 3
rk {A', B', P, Q} = 4
desargues_config_2D A B C A' B' C' P \<alpha> \<beta> \<gamma>
desargues_config_2D A B C A' B' C' P \<alpha> \<beta> \<gamma> \<equiv> rk {A, B, C} = 3 \<and> rk {A', B', C'} = 3 \<and> rk {A, A', P} = 2 \<and> rk {B, B', P} = 2 \<and> rk {C, C', P} = 2 \<and> rk {A, B, \<gamma>} = 2 \<and> rk {A', B', \<gamma>} = 2 \<and> rk {A, C, \<beta>} = 2 \<and> rk {A', C', \<beta>} = 2 \<and> rk {B, C, \<alpha>} = 2 \<and> rk {B', C', \<alpha>} = 2 \<and> rk {A, B, C, A', B', C'} = 3 \<and> rk {A, B, P} = 3 \<and> rk {A, C, P} = 3 \<and> rk {B, C, P} = 3 \<and> rk {A, A'} = 2 \<and> rk {B, B'} = 2 \<and> rk {C, C'} = 2
rk {Q, A', a} = 2
4 \<le> rk {A, B, C, A', B', C', P, Q}
rk {P, Q, R} = 2
rk {P, R} = 2
rk {R, A, a} = 2
\<lbrakk>rk {?A, ?B, ?P} = 3; rk {?A, ?A'} = 2; rk {?A, ?A', ?P} = 2; rk {?Q, ?A', ?a} = 2; 4 \<le> rk {?A, ?B, ?C, ?A', ?B', ?C', ?P, ?Q}; rk {?A, ?B, ?C, ?A', ?B', ?C', ?P} = 3; rk {?P, ?Q, ?R} = 2; rk {?P, ?R} = 2; rk {?A', ?B', ?P, ?Q} = 4; rk {?R, ?A, ?a} = 2\<rbrakk> \<Longrightarrow> 4 \<le> rk {?A, ?B, ?P, ?a}

goal (1 subgoal):
 1. 4 \<le> rk {A, B, P, a}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
4 \<le> rk {A, B, P, a}

goal (2 subgoals):
 1. 4 \<le> rk {A, B, P, b}
 2. 4 \<le> rk {A, B, P, c}
[PROOF STEP]
show "rk {A, B, P, b} \<ge> 4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 4 \<le> rk {A, B, P, b}
[PROOF STEP]
using f1 f2 assms(1) desargues_config_2D_def[of A B C A' B' C' P \<alpha> \<beta> \<gamma>] assms(9) assms(2) assms(3)
      assms(4) assms(10) rk_ABPa[of "B" "A" "P" "B'" "Q" "b" "C" "A'" "C'" "R"]
[PROOF STATE]
proof (prove)
using this:
rk {A, B, C, A', B', C', P} = 3
rk {A', B', P, Q} = 4
desargues_config_2D A B C A' B' C' P \<alpha> \<beta> \<gamma>
desargues_config_2D A B C A' B' C' P \<alpha> \<beta> \<gamma> \<equiv> rk {A, B, C} = 3 \<and> rk {A', B', C'} = 3 \<and> rk {A, A', P} = 2 \<and> rk {B, B', P} = 2 \<and> rk {C, C', P} = 2 \<and> rk {A, B, \<gamma>} = 2 \<and> rk {A', B', \<gamma>} = 2 \<and> rk {A, C, \<beta>} = 2 \<and> rk {A', C', \<beta>} = 2 \<and> rk {B, C, \<alpha>} = 2 \<and> rk {B', C', \<alpha>} = 2 \<and> rk {A, B, C, A', B', C'} = 3 \<and> rk {A, B, P} = 3 \<and> rk {A, C, P} = 3 \<and> rk {B, C, P} = 3 \<and> rk {A, A'} = 2 \<and> rk {B, B'} = 2 \<and> rk {C, C'} = 2
rk {Q, B', b} = 2
4 \<le> rk {A, B, C, A', B', C', P, Q}
rk {P, Q, R} = 2
rk {P, R} = 2
rk {R, B, b} = 2
\<lbrakk>rk {B, A, P} = 3; rk {B, B'} = 2; rk {B, B', P} = 2; rk {Q, B', b} = 2; 4 \<le> rk {B, A, C, B', A', C', P, Q}; rk {B, A, C, B', A', C', P} = 3; rk {P, Q, R} = 2; rk {P, R} = 2; rk {B', A', P, Q} = 4; rk {R, B, b} = 2\<rbrakk> \<Longrightarrow> 4 \<le> rk {B, A, P, b}

goal (1 subgoal):
 1. 4 \<le> rk {A, B, P, b}
[PROOF STEP]
by (metis insert_commute)
[PROOF STATE]
proof (state)
this:
4 \<le> rk {A, B, P, b}

goal (1 subgoal):
 1. 4 \<le> rk {A, B, P, c}
[PROOF STEP]
show "rk {A, B, P, c} \<ge> 4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 4 \<le> rk {A, B, P, c}
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 4 \<le> rk {A, B, P, c}
[PROOF STEP]
have f3:"rk {A, B, P, R, c} \<ge> 4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 4 \<le> rk {A, B, P, R, c}
[PROOF STEP]
using rk_ABPRa[of A B P C A' B' C' Q R c] assms(1) desargues_config_2D_def[of A B C A' B' C' P \<alpha> \<beta> \<gamma>]
        f1 assms(3) assms(4) f2
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>rk {A, B, P} = 3; rk {A, B, C, A', B', C', P} = 3; rk {P, Q, R} = 2; rk {P, R} = 2; rk {A', B', P, Q} = 4\<rbrakk> \<Longrightarrow> 4 \<le> rk {A, B, P, R, c}
desargues_config_2D A B C A' B' C' P \<alpha> \<beta> \<gamma>
desargues_config_2D A B C A' B' C' P \<alpha> \<beta> \<gamma> \<equiv> rk {A, B, C} = 3 \<and> rk {A', B', C'} = 3 \<and> rk {A, A', P} = 2 \<and> rk {B, B', P} = 2 \<and> rk {C, C', P} = 2 \<and> rk {A, B, \<gamma>} = 2 \<and> rk {A', B', \<gamma>} = 2 \<and> rk {A, C, \<beta>} = 2 \<and> rk {A', C', \<beta>} = 2 \<and> rk {B, C, \<alpha>} = 2 \<and> rk {B', C', \<alpha>} = 2 \<and> rk {A, B, C, A', B', C'} = 3 \<and> rk {A, B, P} = 3 \<and> rk {A, C, P} = 3 \<and> rk {B, C, P} = 3 \<and> rk {A, A'} = 2 \<and> rk {B, B'} = 2 \<and> rk {C, C'} = 2
rk {A, B, C, A', B', C', P} = 3
rk {P, Q, R} = 2
rk {P, R} = 2
rk {A', B', P, Q} = 4

goal (1 subgoal):
 1. 4 \<le> rk {A, B, P, R, c}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
4 \<le> rk {A, B, P, R, c}

goal (1 subgoal):
 1. 4 \<le> rk {A, B, P, c}
[PROOF STEP]
have "{A, B, P, R, c} \<subseteq> {A, B, C, P, R, c}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {A, B, P, R, c} \<subseteq> {A, B, C, P, R, c}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{A, B, P, R, c} \<subseteq> {A, B, C, P, R, c}

goal (1 subgoal):
 1. 4 \<le> rk {A, B, P, c}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{A, B, P, R, c} \<subseteq> {A, B, C, P, R, c}
[PROOF STEP]
have f4:"rk {A, B, C, P, R, c} \<ge> 4"
[PROOF STATE]
proof (prove)
using this:
{A, B, P, R, c} \<subseteq> {A, B, C, P, R, c}

goal (1 subgoal):
 1. 4 \<le> rk {A, B, C, P, R, c}
[PROOF STEP]
using matroid_ax_2 f3
[PROOF STATE]
proof (prove)
using this:
{A, B, P, R, c} \<subseteq> {A, B, C, P, R, c}
?X \<subseteq> ?Y \<longrightarrow> rk ?X \<le> rk ?Y
4 \<le> rk {A, B, P, R, c}

goal (1 subgoal):
 1. 4 \<le> rk {A, B, C, P, R, c}
[PROOF STEP]
by (meson dual_order.trans)
[PROOF STATE]
proof (state)
this:
4 \<le> rk {A, B, C, P, R, c}

goal (1 subgoal):
 1. 4 \<le> rk {A, B, P, c}
[PROOF STEP]
have "rk {A, B, C, P, R, c} + rk {C, c} \<le> rk {A, B, C, P, c} + rk {R, C, c}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rk {A, B, C, P, R, c} + rk {C, c} \<le> rk {A, B, C, P, c} + rk {R, C, c}
[PROOF STEP]
using matroid_ax_3_alt[of "{C,c}" "{A, B, C, P, c}" "{R, C, c}"]
[PROOF STATE]
proof (prove)
using this:
{C, c} \<subseteq> {A, B, C, P, c} \<inter> {R, C, c} \<Longrightarrow> rk ({A, B, C, P, c} \<union> {R, C, c}) + rk {C, c} \<le> rk {A, B, C, P, c} + rk {R, C, c}

goal (1 subgoal):
 1. rk {A, B, C, P, R, c} + rk {C, c} \<le> rk {A, B, C, P, c} + rk {R, C, c}
[PROOF STEP]
by (simp add: insert_commute)
[PROOF STATE]
proof (state)
this:
rk {A, B, C, P, R, c} + rk {C, c} \<le> rk {A, B, C, P, c} + rk {R, C, c}

goal (1 subgoal):
 1. 4 \<le> rk {A, B, P, c}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
rk {A, B, C, P, R, c} + rk {C, c} \<le> rk {A, B, C, P, c} + rk {R, C, c}
[PROOF STEP]
have f5:"rk {A, B, C, P, c} \<ge> 4"
[PROOF STATE]
proof (prove)
using this:
rk {A, B, C, P, R, c} + rk {C, c} \<le> rk {A, B, C, P, c} + rk {R, C, c}

goal (1 subgoal):
 1. 4 \<le> rk {A, B, C, P, c}
[PROOF STEP]
using f4 assms(12) desargues_config_2D_rkAa_rkBb_rkCc assms(1) assms(9) assms(11) assms(2) assms(7)
[PROOF STATE]
proof (prove)
using this:
rk {A, B, C, P, R, c} + rk {C, c} \<le> rk {A, B, C, P, c} + rk {R, C, c}
4 \<le> rk {A, B, C, P, R, c}
rk {R, C, c} = 2
\<lbrakk>desargues_config_2D ?A ?B ?C ?A' ?B' ?C' ?P ?\<alpha> ?\<beta> ?\<gamma>; 4 \<le> rk {?A, ?B, ?C, ?A', ?B', ?C', ?P, ?Q}; rk {?Q, ?A', ?a} = 2; rk {?Q, ?B', ?b} = 2; rk {?Q, ?C', ?c} = 2\<rbrakk> \<Longrightarrow> rk {?A, ?a} = 2
\<lbrakk>desargues_config_2D ?A ?B ?C ?A' ?B' ?C' ?P ?\<alpha> ?\<beta> ?\<gamma>; 4 \<le> rk {?A, ?B, ?C, ?A', ?B', ?C', ?P, ?Q}; rk {?Q, ?A', ?a} = 2; rk {?Q, ?B', ?b} = 2; rk {?Q, ?C', ?c} = 2\<rbrakk> \<Longrightarrow> rk {?B, ?b} = 2
\<lbrakk>desargues_config_2D ?A ?B ?C ?A' ?B' ?C' ?P ?\<alpha> ?\<beta> ?\<gamma>; 4 \<le> rk {?A, ?B, ?C, ?A', ?B', ?C', ?P, ?Q}; rk {?Q, ?A', ?a} = 2; rk {?Q, ?B', ?b} = 2; rk {?Q, ?C', ?c} = 2\<rbrakk> \<Longrightarrow> rk {?C, ?c} = 2
desargues_config_2D A B C A' B' C' P \<alpha> \<beta> \<gamma>
rk {Q, B', b} = 2
rk {Q, C', c} = 2
4 \<le> rk {A, B, C, A', B', C', P, Q}
rk {Q, A', a} = 2

goal (1 subgoal):
 1. 4 \<le> rk {A, B, C, P, c}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
4 \<le> rk {A, B, C, P, c}

goal (1 subgoal):
 1. 4 \<le> rk {A, B, P, c}
[PROOF STEP]
have f6:"rk {A, B, C, P} \<le> 3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rk {A, B, C, P} \<le> 3
[PROOF STEP]
using matroid_ax_2 f1
[PROOF STATE]
proof (prove)
using this:
?X \<subseteq> ?Y \<longrightarrow> rk ?X \<le> rk ?Y
rk {A, B, C, A', B', C', P} = 3

goal (1 subgoal):
 1. rk {A, B, C, P} \<le> 3
[PROOF STEP]
by (smt insert_iff subsetI)
[PROOF STATE]
proof (state)
this:
rk {A, B, C, P} \<le> 3

goal (1 subgoal):
 1. 4 \<le> rk {A, B, P, c}
[PROOF STEP]
have "rk {A, B, C, P, c} + rk {A, B, P} \<le> rk {A, B, P, c} + rk {A, B, C, P}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rk {A, B, C, P, c} + rk {A, B, P} \<le> rk {A, B, P, c} + rk {A, B, C, P}
[PROOF STEP]
using matroid_ax_3_alt[of "{A, B, P}" "{A, B, P, c}" "{A, B, C, P}"]
[PROOF STATE]
proof (prove)
using this:
{A, B, P} \<subseteq> {A, B, P, c} \<inter> {A, B, C, P} \<Longrightarrow> rk ({A, B, P, c} \<union> {A, B, C, P}) + rk {A, B, P} \<le> rk {A, B, P, c} + rk {A, B, C, P}

goal (1 subgoal):
 1. rk {A, B, C, P, c} + rk {A, B, P} \<le> rk {A, B, P, c} + rk {A, B, C, P}
[PROOF STEP]
by (simp add: insert_commute)
[PROOF STATE]
proof (state)
this:
rk {A, B, C, P, c} + rk {A, B, P} \<le> rk {A, B, P, c} + rk {A, B, C, P}

goal (1 subgoal):
 1. 4 \<le> rk {A, B, P, c}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
rk {A, B, C, P, c} + rk {A, B, P} \<le> rk {A, B, P, c} + rk {A, B, C, P}
[PROOF STEP]
have "rk {A, B, P, c} \<ge> rk {A, B, C, P, c}"
[PROOF STATE]
proof (prove)
using this:
rk {A, B, C, P, c} + rk {A, B, P} \<le> rk {A, B, P, c} + rk {A, B, C, P}

goal (1 subgoal):
 1. rk {A, B, C, P, c} \<le> rk {A, B, P, c}
[PROOF STEP]
using assms(1) desargues_config_2D_def[of A B C A' B' C' P \<alpha> \<beta> \<gamma>] f6
[PROOF STATE]
proof (prove)
using this:
rk {A, B, C, P, c} + rk {A, B, P} \<le> rk {A, B, P, c} + rk {A, B, C, P}
desargues_config_2D A B C A' B' C' P \<alpha> \<beta> \<gamma>
desargues_config_2D A B C A' B' C' P \<alpha> \<beta> \<gamma> \<equiv> rk {A, B, C} = 3 \<and> rk {A', B', C'} = 3 \<and> rk {A, A', P} = 2 \<and> rk {B, B', P} = 2 \<and> rk {C, C', P} = 2 \<and> rk {A, B, \<gamma>} = 2 \<and> rk {A', B', \<gamma>} = 2 \<and> rk {A, C, \<beta>} = 2 \<and> rk {A', C', \<beta>} = 2 \<and> rk {B, C, \<alpha>} = 2 \<and> rk {B', C', \<alpha>} = 2 \<and> rk {A, B, C, A', B', C'} = 3 \<and> rk {A, B, P} = 3 \<and> rk {A, C, P} = 3 \<and> rk {B, C, P} = 3 \<and> rk {A, A'} = 2 \<and> rk {B, B'} = 2 \<and> rk {C, C'} = 2
rk {A, B, C, P} \<le> 3

goal (1 subgoal):
 1. rk {A, B, C, P, c} \<le> rk {A, B, P, c}
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
rk {A, B, C, P, c} \<le> rk {A, B, P, c}

goal (1 subgoal):
 1. 4 \<le> rk {A, B, P, c}
[PROOF STEP]
thus "rk {A, B, P, c} \<ge> 4"
[PROOF STATE]
proof (prove)
using this:
rk {A, B, C, P, c} \<le> rk {A, B, P, c}

goal (1 subgoal):
 1. 4 \<le> rk {A, B, P, c}
[PROOF STEP]
using f5
[PROOF STATE]
proof (prove)
using this:
rk {A, B, C, P, c} \<le> rk {A, B, P, c}
4 \<le> rk {A, B, C, P, c}

goal (1 subgoal):
 1. 4 \<le> rk {A, B, P, c}
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
4 \<le> rk {A, B, P, c}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
4 \<le> rk {A, B, P, c}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bin_lists_len_count: assumes "x \<noteq> y" and "ws \<in> lists {x,y}" shows
  "count_list ws x + count_list ws y = \<^bold>|ws\<^bold>|"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count_list ws x + count_list ws y = \<^bold>|ws\<^bold>|
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. count_list ws x + count_list ws y = \<^bold>|ws\<^bold>|
[PROOF STEP]
have "finite {x,y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {x, y}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite {x, y}

goal (1 subgoal):
 1. count_list ws x + count_list ws y = \<^bold>|ws\<^bold>|
[PROOF STEP]
have "set ws \<subseteq> {x,y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set ws \<subseteq> {x, y}
[PROOF STEP]
using \<open>ws \<in> lists{x,y}\<close>
[PROOF STATE]
proof (prove)
using this:
ws \<in> lists {x, y}

goal (1 subgoal):
 1. set ws \<subseteq> {x, y}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
set ws \<subseteq> {x, y}

goal (1 subgoal):
 1. count_list ws x + count_list ws y = \<^bold>|ws\<^bold>|
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count_list ws x + count_list ws y = \<^bold>|ws\<^bold>|
[PROOF STEP]
using sum_count_set[OF \<open>set ws \<subseteq> {x,y}\<close> \<open>finite {x,y}\<close>] \<open>x \<noteq> y\<close>
[PROOF STATE]
proof (prove)
using this:
sum (count_list ws) {x, y} = \<^bold>|ws\<^bold>|
x \<noteq> y

goal (1 subgoal):
 1. count_list ws x + count_list ws y = \<^bold>|ws\<^bold>|
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
count_list ws x + count_list ws y = \<^bold>|ws\<^bold>|

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma "w \<le>p w \<Longrightarrow> \<^bold>|w\<^bold>| = 2 \<Longrightarrow> w \<in> lists {a,b} \<Longrightarrow> hd w = a \<Longrightarrow>  w = [a, b] \<or> w = [a, a]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>w \<le>p w; \<^bold>|w\<^bold>| = 2; w \<in> lists {a, b}; hd w = a\<rbrakk> \<Longrightarrow> w = [a, b] \<or> w = [a, a]
[PROOF STEP]
by list_inspection


[STATEMENT]
lemma pow_pref_root_one: assumes "k \<noteq> 0" and "r \<noteq> \<epsilon>" and "r\<^sup>@k \<le>p r"
  shows  "k = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k = 1
[PROOF STEP]
unfolding eq_pow_exp[OF \<open>r \<noteq> \<epsilon>\<close>, of k 1, symmetric] pow_one'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<^sup>@ k = r
[PROOF STEP]
using \<open>r\<^sup>@k \<le>p r\<close> triv_pref[of r "r\<^sup>@(k-1)", folded pop_pow_one[OF \<open>k \<noteq> 0\<close>]]
[PROOF STATE]
proof (prove)
using this:
r \<^sup>@ k \<le>p r
r \<le>p r \<^sup>@ k

goal (1 subgoal):
 1. r \<^sup>@ k = r
[PROOF STEP]
by auto


[STATEMENT]
lemma per_drop_exp: "u \<le>p (r\<^sup>@m)\<^sup>\<omega>  \<Longrightarrow> u \<le>p r\<^sup>\<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<le>p r \<^sup>@ m\<^sup>\<omega> \<Longrightarrow> u \<le>p r\<^sup>\<omega>
[PROOF STEP]
unfolding per_pref[of u r] per_pref[of u "r\<^sup>@m"] pow_mult[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>k. u \<le>p r \<^sup>@ (m * k)) \<and> r \<^sup>@ m \<noteq> \<epsilon> \<Longrightarrow> (\<exists>k. u \<le>p r \<^sup>@ k) \<and> r \<noteq> \<epsilon>
[PROOF STEP]
using nemp_pow_nemp
[PROOF STATE]
proof (prove)
using this:
?t \<^sup>@ ?m \<noteq> \<epsilon> \<Longrightarrow> ?t \<noteq> \<epsilon>

goal (1 subgoal):
 1. (\<exists>k. u \<le>p r \<^sup>@ (m * k)) \<and> r \<^sup>@ m \<noteq> \<epsilon> \<Longrightarrow> (\<exists>k. u \<le>p r \<^sup>@ k) \<and> r \<noteq> \<epsilon>
[PROOF STEP]
by blast


[STATEMENT]
lemma conjug_concat_conjug: "xs \<sim> ys \<Longrightarrow> concat xs \<sim> concat ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<sim> ys \<Longrightarrow> concat xs \<sim> concat ys
[PROOF STEP]
unfolding conjugate_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>r s. r \<cdot> s = xs \<and> s \<cdot> r = ys \<Longrightarrow> \<exists>r s. r \<cdot> s = concat xs \<and> s \<cdot> r = concat ys
[PROOF STEP]
using concat_morph
[PROOF STATE]
proof (prove)
using this:
concat (?xs \<cdot> ?ys) = concat ?xs \<cdot> concat ?ys

goal (1 subgoal):
 1. \<exists>r s. r \<cdot> s = xs \<and> s \<cdot> r = ys \<Longrightarrow> \<exists>r s. r \<cdot> s = concat xs \<and> s \<cdot> r = concat ys
[PROOF STEP]
by metis


[STATEMENT]
lemma rtrancl_join_join:
  assumes "(a, b) \<in> A\<^sup>*" and "(b, c) \<in> A\<^sup>\<down>" shows "(a, c) \<in> A\<^sup>\<down>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a, c) \<in> A\<^sup>\<down>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (a, c) \<in> A\<^sup>\<down>
[PROOF STEP]
from \<open>(b, c) \<in> A\<^sup>\<down>\<close>
[PROOF STATE]
proof (chain)
picking this:
(b, c) \<in> A\<^sup>\<down>
[PROOF STEP]
obtain b' where "(b, b') \<in> A\<^sup>*" and "(b', c) \<in> (A\<inverse>)\<^sup>*"
[PROOF STATE]
proof (prove)
using this:
(b, c) \<in> A\<^sup>\<down>

goal (1 subgoal):
 1. (\<And>b'. \<lbrakk>(b, b') \<in> A\<^sup>*; (b', c) \<in> (A\<inverse>)\<^sup>*\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding join_def
[PROOF STATE]
proof (prove)
using this:
(b, c) \<in> A\<^sup>* O (A\<inverse>)\<^sup>*

goal (1 subgoal):
 1. (\<And>b'. \<lbrakk>(b, b') \<in> A\<^sup>*; (b', c) \<in> (A\<inverse>)\<^sup>*\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(b, b') \<in> A\<^sup>*
(b', c) \<in> (A\<inverse>)\<^sup>*

goal (1 subgoal):
 1. (a, c) \<in> A\<^sup>\<down>
[PROOF STEP]
with \<open>(a, b) \<in> A\<^sup>*\<close>
[PROOF STATE]
proof (chain)
picking this:
(a, b) \<in> A\<^sup>*
(b, b') \<in> A\<^sup>*
(b', c) \<in> (A\<inverse>)\<^sup>*
[PROOF STEP]
have "(a, b') \<in> A\<^sup>*"
[PROOF STATE]
proof (prove)
using this:
(a, b) \<in> A\<^sup>*
(b, b') \<in> A\<^sup>*
(b', c) \<in> (A\<inverse>)\<^sup>*

goal (1 subgoal):
 1. (a, b') \<in> A\<^sup>*
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(a, b') \<in> A\<^sup>*

goal (1 subgoal):
 1. (a, c) \<in> A\<^sup>\<down>
[PROOF STEP]
with \<open>(b', c) \<in> (A\<inverse>)\<^sup>*\<close>
[PROOF STATE]
proof (chain)
picking this:
(b', c) \<in> (A\<inverse>)\<^sup>*
(a, b') \<in> A\<^sup>*
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(b', c) \<in> (A\<inverse>)\<^sup>*
(a, b') \<in> A\<^sup>*

goal (1 subgoal):
 1. (a, c) \<in> A\<^sup>\<down>
[PROOF STEP]
unfolding join_def
[PROOF STATE]
proof (prove)
using this:
(b', c) \<in> (A\<inverse>)\<^sup>*
(a, b') \<in> A\<^sup>*

goal (1 subgoal):
 1. (a, c) \<in> A\<^sup>* O (A\<inverse>)\<^sup>*
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(a, c) \<in> A\<^sup>\<down>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Image_SN_on:
  assumes "SN_on r (r `` A)"
  shows "SN_on r A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SN_on r A
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. \<lbrakk>f 0 \<in> A; \<forall>i. (f i, f (Suc i)) \<in> r\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
fix f
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. \<lbrakk>f 0 \<in> A; \<forall>i. (f i, f (Suc i)) \<in> r\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "f 0 \<in> A" and chain: "chain r f"
[PROOF STATE]
proof (state)
this:
f 0 \<in> A
\<forall>i. (f i, f (Suc i)) \<in> r

goal (1 subgoal):
 1. \<And>f. \<lbrakk>f 0 \<in> A; \<forall>i. (f i, f (Suc i)) \<in> r\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f 0 \<in> A
\<forall>i. (f i, f (Suc i)) \<in> r
[PROOF STEP]
have "f (Suc 0) \<in> r `` A"
[PROOF STATE]
proof (prove)
using this:
f 0 \<in> A
\<forall>i. (f i, f (Suc i)) \<in> r

goal (1 subgoal):
 1. f (Suc 0) \<in> r `` A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f (Suc 0) \<in> r `` A

goal (1 subgoal):
 1. \<And>f. \<lbrakk>f 0 \<in> A; \<forall>i. (f i, f (Suc i)) \<in> r\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
SN_on r (r `` A)
f (Suc 0) \<in> r `` A
[PROOF STEP]
have "SN_on r {f (Suc 0)}"
[PROOF STATE]
proof (prove)
using this:
SN_on r (r `` A)
f (Suc 0) \<in> r `` A

goal (1 subgoal):
 1. SN_on r {f (Suc 0)}
[PROOF STEP]
by (auto simp add: \<open>f 0 \<in> A\<close> SN_defs)
[PROOF STATE]
proof (state)
this:
SN_on r {f (Suc 0)}

goal (1 subgoal):
 1. \<And>f. \<lbrakk>f 0 \<in> A; \<forall>i. (f i, f (Suc i)) \<in> r\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
SN_on r {f (Suc 0)}

goal (1 subgoal):
 1. \<And>f. \<lbrakk>f 0 \<in> A; \<forall>i. (f i, f (Suc i)) \<in> r\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "\<not> SN_on r {f (Suc 0)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> SN_on r {f (Suc 0)}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> SN_on r {f (Suc 0)}
[PROOF STEP]
have "f (Suc 0) \<in> {f (Suc 0)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (Suc 0) \<in> {f (Suc 0)}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f (Suc 0) \<in> {f (Suc 0)}

goal (1 subgoal):
 1. \<not> SN_on r {f (Suc 0)}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f (Suc 0) \<in> {f (Suc 0)}

goal (1 subgoal):
 1. \<not> SN_on r {f (Suc 0)}
[PROOF STEP]
from chain
[PROOF STATE]
proof (chain)
picking this:
\<forall>i. (f i, f (Suc i)) \<in> r
[PROOF STEP]
have "chain r (f \<circ> Suc)"
[PROOF STATE]
proof (prove)
using this:
\<forall>i. (f i, f (Suc i)) \<in> r

goal (1 subgoal):
 1. \<forall>i. ((f \<circ> Suc) i, (f \<circ> Suc) (Suc i)) \<in> r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>i. ((f \<circ> Suc) i, (f \<circ> Suc) (Suc i)) \<in> r

goal (1 subgoal):
 1. \<not> SN_on r {f (Suc 0)}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
f (Suc 0) \<in> {f (Suc 0)}
\<forall>i. ((f \<circ> Suc) i, (f \<circ> Suc) (Suc i)) \<in> r
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f (Suc 0) \<in> {f (Suc 0)}
\<forall>i. ((f \<circ> Suc) i, (f \<circ> Suc) (Suc i)) \<in> r

goal (1 subgoal):
 1. \<not> SN_on r {f (Suc 0)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> SN_on r {f (Suc 0)}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> SN_on r {f (Suc 0)}

goal (1 subgoal):
 1. \<And>f. \<lbrakk>f 0 \<in> A; \<forall>i. (f i, f (Suc i)) \<in> r\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
SN_on r {f (Suc 0)}
\<not> SN_on r {f (Suc 0)}
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
SN_on r {f (Suc 0)}
\<not> SN_on r {f (Suc 0)}

goal (1 subgoal):
 1. False
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma find_remove_2_removeAll :
  assumes "find_remove_2 P xs ys = Some (x,y,xs')"
  and     "distinct xs"
shows "xs' = removeAll x xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs' = removeAll x xs
[PROOF STEP]
using find_remove_2_set(6)[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
xs' = remove1 x xs

goal (1 subgoal):
 1. xs' = removeAll x xs
[PROOF STEP]
by (simp add: assms(2) distinct_remove1_removeAll)


[STATEMENT]
lemma Lact_Ract_noStateChange_set:
assumes "set al \<subseteq> Lact ` UNIV \<union> Ract ` UNIV"
shows "snd (sstep s al) = s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (sstep s al) = s
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
set al \<subseteq> range Lact \<union> range Ract

goal (1 subgoal):
 1. snd (sstep s al) = s
[PROOF STEP]
by (induct al) (auto split: prod.splits)


[STATEMENT]
lemma szip_sconst_smap_fst: "sconst a ||| xs = smap (Pair a) xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sconst a ||| xs = smap (Pair a) xs
[PROOF STEP]
by (coinduction arbitrary: xs) (auto)


[STATEMENT]
lemma RS1N_DA[simp]: "removeShadowRules1_alternative (a@[DenyAll]) = [DenyAll]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. removeShadowRules1_alternative (a @ [DenyAll]) = [DenyAll]
[PROOF STEP]
by (simp add: removeShadowRules1_alternative_def)


[STATEMENT]
lemma (in is_cat_limit) is_cat_colimit_op'[cat_op_intros]:
  assumes "\<FF>' = op_cf \<FF>" and "\<JJ>' = op_cat \<JJ>" and "\<CC>' = op_cat \<CC>"
  shows "op_ntcf u : \<FF>' >\<^sub>C\<^sub>F\<^sub>.\<^sub>c\<^sub>o\<^sub>l\<^sub>i\<^sub>m r : \<JJ>' \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_ntcf u : \<FF>' >\<^sub>C\<^sub>F\<^sub>.\<^sub>c\<^sub>o\<^sub>l\<^sub>i\<^sub>m r : \<JJ>' \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>'
[PROOF STEP]
unfolding assms
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_ntcf u : op_cf \<FF> >\<^sub>C\<^sub>F\<^sub>.\<^sub>c\<^sub>o\<^sub>l\<^sub>i\<^sub>m r : op_cat \<JJ> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<CC>
[PROOF STEP]
by (rule is_cat_colimit_op)


[STATEMENT]
lemma count_it_ex:
  assumes "\<pi>: (WHILE b DO c,s) \<Rightarrow> t"
  shows "\<exists>n. count_it \<pi> b c s n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n. count_it \<pi> b c s n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<pi>: (WHILE b DO c, s) \<Rightarrow> t

goal (1 subgoal):
 1. \<exists>n. count_it \<pi> b c s n
[PROOF STEP]
apply (induction \<pi> "WHILE b DO c" s t arbitrary: b c)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>b s \<pi> c. \<not> bval b s \<Longrightarrow> Ex (count_it \<pi> b c s)
 2. \<And>b s\<^sub>1 \<pi> c s\<^sub>2 s\<^sub>3. \<lbrakk>bval b s\<^sub>1; \<pi>: (c, s\<^sub>1) \<Rightarrow> s\<^sub>2; \<And>b ca. c = WHILE b DO ca \<Longrightarrow> \<exists>a. count_it \<pi> b ca s\<^sub>1 a; \<pi>: (WHILE b DO c, s\<^sub>2) \<Rightarrow> s\<^sub>3; Ex (count_it \<pi> b c s\<^sub>2)\<rbrakk> \<Longrightarrow> Ex (count_it \<pi> b c s\<^sub>1)
[PROOF STEP]
apply (auto intro: count_it.intros)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma MkI_0: "MkI\<cdot>0 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MkI\<cdot>0 = 0
[PROOF STEP]
by simp


[STATEMENT]
lemma lmap_Lazy_llist [code]:
  "lmap f (Lazy_llist xs) = Lazy_llist (\<lambda>_. map_option (map_prod f (lmap f)) (xs ()))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lmap f (Lazy_llist xs) = Lazy_llist (\<lambda>_. map_option (map_prod f (lmap f)) (xs ()))
[PROOF STEP]
by simp


[STATEMENT]
theorem Subject_reductions:
assumes wf: "wf_J_prog P" and reds: "P \<turnstile> \<langle>e,s,b\<rangle> \<rightarrow>* \<langle>e',s',b'\<rangle>"
shows "\<And>T. P,E,s \<turnstile> e:T \<surd> \<Longrightarrow> \<exists>T'. P,E,s' \<turnstile> e':T' \<surd> \<and> P \<turnstile> T' \<le> T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>T. P,E,s \<turnstile> e : T \<surd> \<Longrightarrow> \<exists>T'. P,E,s' \<turnstile> e' : T' \<surd> \<and> P \<turnstile> T' \<le> T
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>T. P,E,s \<turnstile> e : T \<surd> \<Longrightarrow> \<exists>T'. P,E,s' \<turnstile> e' : T' \<surd> \<and> P \<turnstile> T' \<le> T
[PROOF STEP]
using reds
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> \<langle>e,s,b\<rangle> \<rightarrow>* \<langle>e',s',b'\<rangle>

goal (1 subgoal):
 1. \<And>T. P,E,s \<turnstile> e : T \<surd> \<Longrightarrow> \<exists>T'. P,E,s' \<turnstile> e' : T' \<surd> \<and> P \<turnstile> T' \<le> T
[PROOF STEP]
proof (induct rule:converse_rtrancl_induct3)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>T. P,E,s' \<turnstile> e' : T \<surd> \<Longrightarrow> \<exists>T'. P,E,s' \<turnstile> e' : T' \<surd> \<and> P \<turnstile> T' \<le> T
 2. \<And>a aa b ab ac ba T. \<lbrakk>P \<turnstile> \<langle>a,aa,b\<rangle> \<rightarrow> \<langle>ab,ac,ba\<rangle>; P \<turnstile> \<langle>ab,ac,ba\<rangle> \<rightarrow>* \<langle>e',s',b'\<rangle>; \<And>T. P,E,ac \<turnstile> ab : T \<surd> \<Longrightarrow> \<exists>T'. P,E,s' \<turnstile> e' : T' \<surd> \<and> P \<turnstile> T' \<le> T; P,E,aa \<turnstile> a : T \<surd>\<rbrakk> \<Longrightarrow> \<exists>T'. P,E,s' \<turnstile> e' : T' \<surd> \<and> P \<turnstile> T' \<le> T
[PROOF STEP]
case refl
[PROOF STATE]
proof (state)
this:
P,E,s' \<turnstile> e' : T \<surd>

goal (2 subgoals):
 1. \<And>T. P,E,s' \<turnstile> e' : T \<surd> \<Longrightarrow> \<exists>T'. P,E,s' \<turnstile> e' : T' \<surd> \<and> P \<turnstile> T' \<le> T
 2. \<And>a aa b ab ac ba T. \<lbrakk>P \<turnstile> \<langle>a,aa,b\<rangle> \<rightarrow> \<langle>ab,ac,ba\<rangle>; P \<turnstile> \<langle>ab,ac,ba\<rangle> \<rightarrow>* \<langle>e',s',b'\<rangle>; \<And>T. P,E,ac \<turnstile> ab : T \<surd> \<Longrightarrow> \<exists>T'. P,E,s' \<turnstile> e' : T' \<surd> \<and> P \<turnstile> T' \<le> T; P,E,aa \<turnstile> a : T \<surd>\<rbrakk> \<Longrightarrow> \<exists>T'. P,E,s' \<turnstile> e' : T' \<surd> \<and> P \<turnstile> T' \<le> T
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
P,E,s' \<turnstile> e' : T \<surd>

goal (1 subgoal):
 1. \<exists>T'. P,E,s' \<turnstile> e' : T' \<surd> \<and> P \<turnstile> T' \<le> T
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>T'. P,E,s' \<turnstile> e' : T' \<surd> \<and> P \<turnstile> T' \<le> T

goal (1 subgoal):
 1. \<And>a aa b ab ac ba T. \<lbrakk>P \<turnstile> \<langle>a,aa,b\<rangle> \<rightarrow> \<langle>ab,ac,ba\<rangle>; P \<turnstile> \<langle>ab,ac,ba\<rangle> \<rightarrow>* \<langle>e',s',b'\<rangle>; \<And>T. P,E,ac \<turnstile> ab : T \<surd> \<Longrightarrow> \<exists>T'. P,E,s' \<turnstile> e' : T' \<surd> \<and> P \<turnstile> T' \<le> T; P,E,aa \<turnstile> a : T \<surd>\<rbrakk> \<Longrightarrow> \<exists>T'. P,E,s' \<turnstile> e' : T' \<surd> \<and> P \<turnstile> T' \<le> T
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a aa b ab ac ba T. \<lbrakk>P \<turnstile> \<langle>a,aa,b\<rangle> \<rightarrow> \<langle>ab,ac,ba\<rangle>; P \<turnstile> \<langle>ab,ac,ba\<rangle> \<rightarrow>* \<langle>e',s',b'\<rangle>; \<And>T. P,E,ac \<turnstile> ab : T \<surd> \<Longrightarrow> \<exists>T'. P,E,s' \<turnstile> e' : T' \<surd> \<and> P \<turnstile> T' \<le> T; P,E,aa \<turnstile> a : T \<surd>\<rbrakk> \<Longrightarrow> \<exists>T'. P,E,s' \<turnstile> e' : T' \<surd> \<and> P \<turnstile> T' \<le> T
[PROOF STEP]
case step
[PROOF STATE]
proof (state)
this:
P \<turnstile> \<langle>a___,aa___,ba___\<rangle> \<rightarrow> \<langle>ab___,a_,b_\<rangle>
P \<turnstile> \<langle>ab___,a_,b_\<rangle> \<rightarrow>* \<langle>e',s',b'\<rangle>
P,E,a_ \<turnstile> ab___ : ?T \<surd> \<Longrightarrow> \<exists>T'. P,E,s' \<turnstile> e' : T' \<surd> \<and> P \<turnstile> T' \<le> ?T
P,E,aa___ \<turnstile> a___ : T \<surd>

goal (1 subgoal):
 1. \<And>a aa b ab ac ba T. \<lbrakk>P \<turnstile> \<langle>a,aa,b\<rangle> \<rightarrow> \<langle>ab,ac,ba\<rangle>; P \<turnstile> \<langle>ab,ac,ba\<rangle> \<rightarrow>* \<langle>e',s',b'\<rangle>; \<And>T. P,E,ac \<turnstile> ab : T \<surd> \<Longrightarrow> \<exists>T'. P,E,s' \<turnstile> e' : T' \<surd> \<and> P \<turnstile> T' \<le> T; P,E,aa \<turnstile> a : T \<surd>\<rbrakk> \<Longrightarrow> \<exists>T'. P,E,s' \<turnstile> e' : T' \<surd> \<and> P \<turnstile> T' \<le> T
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> \<langle>a___,aa___,ba___\<rangle> \<rightarrow> \<langle>ab___,a_,b_\<rangle>
P \<turnstile> \<langle>ab___,a_,b_\<rangle> \<rightarrow>* \<langle>e',s',b'\<rangle>
P,E,a_ \<turnstile> ab___ : ?T \<surd> \<Longrightarrow> \<exists>T'. P,E,s' \<turnstile> e' : T' \<surd> \<and> P \<turnstile> T' \<le> ?T
P,E,aa___ \<turnstile> a___ : T \<surd>

goal (1 subgoal):
 1. \<exists>T'. P,E,s' \<turnstile> e' : T' \<surd> \<and> P \<turnstile> T' \<le> T
[PROOF STEP]
by(blast dest:Subject_reduction[OF wf] intro:widen_trans)
[PROOF STATE]
proof (state)
this:
\<exists>T'. P,E,s' \<turnstile> e' : T' \<surd> \<and> P \<turnstile> T' \<le> T

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma zless_zle_trans:"\<lbrakk> (i::int) < j; j \<le> k\<rbrakk> \<Longrightarrow> i < k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i < j; j \<le> k\<rbrakk> \<Longrightarrow> i < k
[PROOF STEP]
by arith


[STATEMENT]
lemma pos_zmult_pos:"\<lbrakk> 0 \<le> (a::int); 0 < (b::int)\<rbrakk> \<Longrightarrow> a \<le> a * b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 \<le> a; 0 < b\<rbrakk> \<Longrightarrow> a \<le> a * b
[PROOF STEP]
apply (case_tac "a = 0")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 \<le> a; 0 < b; a = 0\<rbrakk> \<Longrightarrow> a \<le> a * b
 2. \<lbrakk>0 \<le> a; 0 < b; a \<noteq> 0\<rbrakk> \<Longrightarrow> a \<le> a * b
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 \<le> a; 0 < b; a \<noteq> 0\<rbrakk> \<Longrightarrow> a \<le> a * b
[PROOF STEP]
apply (frule zle_imp_zless_or_eq[of "0" "a"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 \<le> a; 0 < b; a \<noteq> 0; 0 < a \<or> 0 = a\<rbrakk> \<Longrightarrow> a \<le> a * b
[PROOF STEP]
apply (thin_tac "0 \<le> a")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < b; a \<noteq> 0; 0 < a \<or> 0 = a\<rbrakk> \<Longrightarrow> a \<le> a * b
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma cmp_fun_image:"\<lbrakk>f \<in> A \<rightarrow> B; g \<in> B \<rightarrow> C \<rbrakk> \<Longrightarrow>
                          (cmp g f) ` A =  g ` (f ` A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f \<in> A \<rightarrow> B; g \<in> B \<rightarrow> C\<rbrakk> \<Longrightarrow> cmp g f ` A = g ` f ` A
[PROOF STEP]
apply (rule equalityI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>f \<in> A \<rightarrow> B; g \<in> B \<rightarrow> C\<rbrakk> \<Longrightarrow> cmp g f ` A \<subseteq> g ` f ` A
 2. \<lbrakk>f \<in> A \<rightarrow> B; g \<in> B \<rightarrow> C\<rbrakk> \<Longrightarrow> g ` f ` A \<subseteq> cmp g f ` A
[PROOF STEP]
apply (rule subsetI, simp add:image_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>f \<in> A \<rightarrow> B; g \<in> B \<rightarrow> C; \<exists>xa\<in>A. x = cmp g f xa\<rbrakk> \<Longrightarrow> \<exists>xa. (\<exists>x\<in>A. xa = f x) \<and> x = g xa
 2. \<lbrakk>f \<in> A \<rightarrow> B; g \<in> B \<rightarrow> C\<rbrakk> \<Longrightarrow> g ` f ` A \<subseteq> cmp g f ` A
[PROOF STEP]
apply (erule bexE, simp add:cmp_def, blast)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f \<in> A \<rightarrow> B; g \<in> B \<rightarrow> C\<rbrakk> \<Longrightarrow> g ` f ` A \<subseteq> cmp g f ` A
[PROOF STEP]
apply (rule subsetI, simp add:image_def[of g])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>f \<in> A \<rightarrow> B; g \<in> B \<rightarrow> C; \<exists>xa\<in>A. x = g (f xa)\<rbrakk> \<Longrightarrow> x \<in> cmp g f ` A
[PROOF STEP]
apply (erule bexE, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>f \<in> A \<rightarrow> B; g \<in> B \<rightarrow> C; xa \<in> A; x = g (f xa)\<rbrakk> \<Longrightarrow> g (f xa) \<in> cmp g f ` A
[PROOF STEP]
apply (simp add:image_def cmp_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>f \<in> A \<rightarrow> B; g \<in> B \<rightarrow> C; xa \<in> A; x = g (f xa)\<rbrakk> \<Longrightarrow> \<exists>x\<in>A. g (f xa) = g (f x)
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma a_mpi[simp]:"-\<infinity> + \<infinity>  = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - \<infinity> + \<infinity> = 0
[PROOF STEP]
apply (simp add:add_ant_def inf_ant_def,
       cut_tac ant_inf_in_Ainteg,
       cut_tac ant_minf_in_Ainteg,
       simp add:minus_ant_def,
       simp add:Abs_Ainteg_inverse,
       simp add:Zero_ant_def ant_def zag_pl_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma aadd_0_r: "x + (0::ant) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x + 0 = x
[PROOF STEP]
apply (cut_tac mem_ant[of "x"], simp add:Zero_ant_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = - \<infinity> \<or> (\<exists>z. x = ant z) \<or> x = \<infinity> \<Longrightarrow> x + ant 0 = x
[PROOF STEP]
apply ((erule disjE)+, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>z. x = ant z) \<or> x = \<infinity> \<Longrightarrow> x + ant 0 = x
[PROOF STEP]
apply (erule disjE, erule exE, simp add:a_zpz,
       simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma agsprod_assoc:"\<lbrakk>m \<noteq> 0; n \<noteq> 0\<rbrakk> \<Longrightarrow> m *\<^sub>a (n *\<^sub>a x) = (m * n) *\<^sub>a x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<noteq> 0; n \<noteq> 0\<rbrakk> \<Longrightarrow> m *\<^sub>a (n *\<^sub>a x) = (m * n) *\<^sub>a x
[PROOF STEP]
apply (cut_tac less_linear[of "m" "0"], cut_tac less_linear[of "n" "0"],
       cut_tac mem_ant[of "x"],
      (erule disjE)+, simp,
      frule zmult_neg_neg[of "m" "n"], assumption+, simp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m \<noteq> 0; n \<noteq> 0; m < 0; n < 0; (\<exists>z. x = ant z) \<or> x = \<infinity>\<rbrakk> \<Longrightarrow> m *\<^sub>a (n *\<^sub>a x) = (m * n) *\<^sub>a x
 2. \<lbrakk>m \<noteq> 0; n \<noteq> 0; x = - \<infinity> \<or> (\<exists>z. x = ant z) \<or> x = \<infinity>; m < 0; n = 0 \<or> 0 < n\<rbrakk> \<Longrightarrow> m *\<^sub>a (n *\<^sub>a x) = (m * n) *\<^sub>a x
 3. \<lbrakk>m \<noteq> 0; n \<noteq> 0; n < 0 \<or> n = 0 \<or> 0 < n; x = - \<infinity> \<or> (\<exists>z. x = ant z) \<or> x = \<infinity>; m = 0 \<or> 0 < m\<rbrakk> \<Longrightarrow> m *\<^sub>a (n *\<^sub>a x) = (m * n) *\<^sub>a x
[PROOF STEP]
apply (erule disjE, erule exE, simp add:asprod_mult,
      frule zmult_neg_neg[of "m" "n"], assumption+, simp+,
      erule disjE, simp,
      frule zmult_neg_pos[of "m" "n"], assumption+, simp,
      erule disjE, erule exE, simp,
      frule zmult_neg_pos[of "m" "n"], assumption+, simp add:asprod_mult,
      frule zmult_neg_pos[of "m" "n"], assumption+, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<noteq> 0; n \<noteq> 0; n < 0 \<or> n = 0 \<or> 0 < n; x = - \<infinity> \<or> (\<exists>z. x = ant z) \<or> x = \<infinity>; m = 0 \<or> 0 < m\<rbrakk> \<Longrightarrow> m *\<^sub>a (n *\<^sub>a x) = (m * n) *\<^sub>a x
[PROOF STEP]
apply (simp, (erule disjE)+,
      frule zmult_pos_neg[of "m" "n"], assumption+,
      simp,
      erule disjE, erule exE, simp add:asprod_mult,
      frule zmult_pos_neg[of "m" "n"], assumption+, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<noteq> 0; x = - \<infinity> \<or> (\<exists>z. x = ant z) \<or> x = \<infinity>; 0 < m; 0 < n\<rbrakk> \<Longrightarrow> m *\<^sub>a (n *\<^sub>a x) = (m * n) *\<^sub>a x
[PROOF STEP]
apply (frule zmult_pos_pos[of "m" "n"], assumption+,
      erule disjE, simp,
      erule disjE, erule exE, simp add:asprod_mult, simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Nset2finite_inj:"\<lbrakk>finite A; card A = Suc n; surj_to f {i. i \<le> n} A \<rbrakk> \<Longrightarrow>
        inj_on f {i. i \<le> n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite A; card A = Suc n; surj_to f {i. i \<le> n} A\<rbrakk> \<Longrightarrow> inj_on f {i. i \<le> n}
[PROOF STEP]
by (metis card_Collect_le_nat eq_card_imp_inj_on finite_Collect_le_nat surj_to_def)


[STATEMENT]
lemma (in Order) ord_isom_surj_forall:"\<lbrakk>Order E; ord_isom D E f\<rbrakk> \<Longrightarrow>
              \<forall>b \<in> carrier E. \<exists>a\<in>carrier D. b = f a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Order E; ord_isom D E f\<rbrakk> \<Longrightarrow> \<forall>b\<in>carrier E. \<exists>a\<in>carrier D. b = f a
[PROOF STEP]
apply (rule ballI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>Order E; ord_isom D E f; b \<in> carrier E\<rbrakk> \<Longrightarrow> \<exists>a\<in>carrier D. b = f a
[PROOF STEP]
apply (rule ord_isom_surj[of "E" "f"], assumption+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Worder) Tw_mem:"\<lbrakk>Worder E; x \<in> carrier D;
     \<forall>a\<in>carrier D. \<exists>b\<in>carrier E. ord_equiv (Iod D (segment D a))
         (Iod E (segment E b))\<rbrakk> \<Longrightarrow> (Tw\<^bsub>D,E\<^esub>) x \<in> carrier E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Worder E; x \<in> carrier D; \<forall>a\<in>carrier D. \<exists>b\<in>carrier E. ord_equiv (Iod D (segment D a)) (Iod E (segment E b))\<rbrakk> \<Longrightarrow> (Tw\<^bsub>D,E\<^esub>) x \<in> carrier E
[PROOF STEP]
by (frule Tw_func[of E], assumption,
       simp add:Pi_def)


[STATEMENT]
lemma euler_imp_connected:
  assumes "euler_trail u p v" shows "connected G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Digraph_Component.connected G
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Digraph_Component.connected G
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Digraph_Component.connected G
[PROOF STEP]
have "verts G \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. verts G \<noteq> {}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
euler_trail u p v

goal (1 subgoal):
 1. verts G \<noteq> {}
[PROOF STEP]
unfolding euler_trail_def trail_def
[PROOF STATE]
proof (prove)
using this:
(awalk u p v \<and> distinct p) \<and> set p = arcs G \<and> set (awalk_verts u p) = verts G

goal (1 subgoal):
 1. verts G \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
verts G \<noteq> {}

goal (1 subgoal):
 1. Digraph_Component.connected G
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
verts G \<noteq> {}

goal (1 subgoal):
 1. Digraph_Component.connected G
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
verts G \<noteq> {}

goal (1 subgoal):
 1. Digraph_Component.connected G
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
verts G \<noteq> {}

goal (1 subgoal):
 1. Digraph_Component.connected G
[PROOF STEP]
fix w1 w2
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Digraph_Component.connected G
[PROOF STEP]
assume "w1 \<in> verts G" "w2 \<in> verts G"
[PROOF STATE]
proof (state)
this:
w1 \<in> verts G
w2 \<in> verts G

goal (1 subgoal):
 1. Digraph_Component.connected G
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
w1 \<in> verts G
w2 \<in> verts G
[PROOF STEP]
have "awalk u p v " "w1 \<in> set (awalk_verts u p)" "w2 \<in> set (awalk_verts u p)"
[PROOF STATE]
proof (prove)
using this:
w1 \<in> verts G
w2 \<in> verts G

goal (1 subgoal):
 1. awalk u p v &&& w1 \<in> set (awalk_verts u p) &&& w2 \<in> set (awalk_verts u p)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
w1 \<in> verts G
w2 \<in> verts G
euler_trail u p v

goal (1 subgoal):
 1. awalk u p v &&& w1 \<in> set (awalk_verts u p) &&& w2 \<in> set (awalk_verts u p)
[PROOF STEP]
by (auto simp: euler_trail_def trail_def)
[PROOF STATE]
proof (state)
this:
awalk u p v
w1 \<in> set (awalk_verts u p)
w2 \<in> set (awalk_verts u p)

goal (1 subgoal):
 1. Digraph_Component.connected G
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
awalk u p v
w1 \<in> set (awalk_verts u p)
w2 \<in> set (awalk_verts u p)
[PROOF STEP]
have "w1 \<rightarrow>\<^sup>*\<^bsub>mk_symmetric G\<^esub> w2"
[PROOF STATE]
proof (prove)
using this:
awalk u p v
w1 \<in> set (awalk_verts u p)
w2 \<in> set (awalk_verts u p)

goal (1 subgoal):
 1. w1 \<rightarrow>\<^sup>*\<^bsub>with_proj (mk_symmetric G)\<^esub> w2
[PROOF STEP]
by (rule sym_reachableI_in_awalk)
[PROOF STATE]
proof (state)
this:
w1 \<rightarrow>\<^sup>*\<^bsub>with_proj (mk_symmetric G)\<^esub> w2

goal (1 subgoal):
 1. Digraph_Component.connected G
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?w1.4 \<in> verts G; ?w2.4 \<in> verts G\<rbrakk> \<Longrightarrow> ?w1.4 \<rightarrow>\<^sup>*\<^bsub>with_proj (mk_symmetric G)\<^esub> ?w2.4

goal (1 subgoal):
 1. Digraph_Component.connected G
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
verts G \<noteq> {}
\<lbrakk>?w1.4 \<in> verts G; ?w2.4 \<in> verts G\<rbrakk> \<Longrightarrow> ?w1.4 \<rightarrow>\<^sup>*\<^bsub>with_proj (mk_symmetric G)\<^esub> ?w2.4
[PROOF STEP]
show "connected G"
[PROOF STATE]
proof (prove)
using this:
verts G \<noteq> {}
\<lbrakk>?w1.4 \<in> verts G; ?w2.4 \<in> verts G\<rbrakk> \<Longrightarrow> ?w1.4 \<rightarrow>\<^sup>*\<^bsub>with_proj (mk_symmetric G)\<^esub> ?w2.4

goal (1 subgoal):
 1. Digraph_Component.connected G
[PROOF STEP]
by (rule connectedI)
[PROOF STATE]
proof (state)
this:
Digraph_Component.connected G

goal:
No subgoals!
[PROOF STEP]
qed