[STATEMENT]
lemma nth_plus_list [rule_format, simp]:
  "\<forall>xs ys i. size xs = n \<longrightarrow> size ys = n \<longrightarrow> i<n \<longrightarrow> (xs [\<squnion>\<^bsub>f\<^esub>] ys)!i = (xs!i) \<squnion>\<^sub>f (ys!i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>xs ys i. length xs = n \<longrightarrow> length ys = n \<longrightarrow> i < n \<longrightarrow> (xs [+f] ys) ! i = xs ! i \<squnion>\<^bsub>f\<^esub> ys ! i
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>xs ys i. length xs = n \<longrightarrow> length ys = n \<longrightarrow> i < n \<longrightarrow> (xs [+f] ys) ! i = xs ! i \<squnion>\<^bsub>f\<^esub> ys ! i
[PROOF STEP]
apply (induct n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>xs ys i. length xs = 0 \<longrightarrow> length ys = 0 \<longrightarrow> i < 0 \<longrightarrow> (xs [+f] ys) ! i = xs ! i \<squnion>\<^bsub>f\<^esub> ys ! i
 2. \<And>n. \<forall>xs ys i. length xs = n \<longrightarrow> length ys = n \<longrightarrow> i < n \<longrightarrow> (xs [+f] ys) ! i = xs ! i \<squnion>\<^bsub>f\<^esub> ys ! i \<Longrightarrow> \<forall>xs ys i. length xs = Suc n \<longrightarrow> length ys = Suc n \<longrightarrow> i < Suc n \<longrightarrow> (xs [+f] ys) ! i = xs ! i \<squnion>\<^bsub>f\<^esub> ys ! i
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<forall>xs ys i. length xs = n \<longrightarrow> length ys = n \<longrightarrow> i < n \<longrightarrow> (xs [+f] ys) ! i = xs ! i \<squnion>\<^bsub>f\<^esub> ys ! i \<Longrightarrow> \<forall>xs ys i. length xs = Suc n \<longrightarrow> length ys = Suc n \<longrightarrow> i < Suc n \<longrightarrow> (xs [+f] ys) ! i = xs ! i \<squnion>\<^bsub>f\<^esub> ys ! i
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n xs ys i. \<lbrakk>\<forall>xs ys i. length xs = n \<longrightarrow> length ys = n \<longrightarrow> i < n \<longrightarrow> (xs [+f] ys) ! i = xs ! i \<squnion>\<^bsub>f\<^esub> ys ! i; length xs = Suc n; length ys = Suc n; i < Suc n\<rbrakk> \<Longrightarrow> (xs [+f] ys) ! i = xs ! i \<squnion>\<^bsub>f\<^esub> ys ! i
[PROOF STEP]
apply (case_tac xs)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n xs ys i. \<lbrakk>\<forall>xs ys i. length xs = n \<longrightarrow> length ys = n \<longrightarrow> i < n \<longrightarrow> (xs [+f] ys) ! i = xs ! i \<squnion>\<^bsub>f\<^esub> ys ! i; length xs = Suc n; length ys = Suc n; i < Suc n; xs = []\<rbrakk> \<Longrightarrow> (xs [+f] ys) ! i = xs ! i \<squnion>\<^bsub>f\<^esub> ys ! i
 2. \<And>n xs ys i a list. \<lbrakk>\<forall>xs ys i. length xs = n \<longrightarrow> length ys = n \<longrightarrow> i < n \<longrightarrow> (xs [+f] ys) ! i = xs ! i \<squnion>\<^bsub>f\<^esub> ys ! i; length xs = Suc n; length ys = Suc n; i < Suc n; xs = a # list\<rbrakk> \<Longrightarrow> (xs [+f] ys) ! i = xs ! i \<squnion>\<^bsub>f\<^esub> ys ! i
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n xs ys i a list. \<lbrakk>\<forall>xs ys i. length xs = n \<longrightarrow> length ys = n \<longrightarrow> i < n \<longrightarrow> (xs [+f] ys) ! i = xs ! i \<squnion>\<^bsub>f\<^esub> ys ! i; length xs = Suc n; length ys = Suc n; i < Suc n; xs = a # list\<rbrakk> \<Longrightarrow> (xs [+f] ys) ! i = xs ! i \<squnion>\<^bsub>f\<^esub> ys ! i
[PROOF STEP]
apply (force simp add: nth_Cons split: list.split nat.split)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Semilat) plus_list_ub1 [rule_format]:
 "\<lbrakk> set xs \<subseteq> A; set ys \<subseteq> A; size xs = size ys \<rbrakk>
  \<Longrightarrow> xs [\<sqsubseteq>\<^bsub>r\<^esub>] xs [\<squnion>\<^bsub>f\<^esub>] ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>set xs \<subseteq> A; set ys \<subseteq> A; length xs = length ys\<rbrakk> \<Longrightarrow> xs [\<sqsubseteq>\<^bsub>r\<^esub>] xs [+f] ys
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>set xs \<subseteq> A; set ys \<subseteq> A; length xs = length ys\<rbrakk> \<Longrightarrow> xs [\<sqsubseteq>\<^bsub>r\<^esub>] xs [+f] ys
[PROOF STEP]
apply (unfold unfold_lesub_list)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>set xs \<subseteq> A; set ys \<subseteq> A; length xs = length ys\<rbrakk> \<Longrightarrow> Listn.le r xs (xs [+f] ys)
[PROOF STEP]
apply (simp add: Listn.le_def list_all2_conv_all_nth)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Semilat) plus_list_ub2:
 "\<lbrakk>set xs \<subseteq> A; set ys \<subseteq> A; size xs = size ys \<rbrakk> \<Longrightarrow> ys [\<sqsubseteq>\<^bsub>r\<^esub>] xs [\<squnion>\<^bsub>f\<^esub>] ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>set xs \<subseteq> A; set ys \<subseteq> A; length xs = length ys\<rbrakk> \<Longrightarrow> ys [\<sqsubseteq>\<^bsub>r\<^esub>] xs [+f] ys
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>set xs \<subseteq> A; set ys \<subseteq> A; length xs = length ys\<rbrakk> \<Longrightarrow> ys [\<sqsubseteq>\<^bsub>r\<^esub>] xs [+f] ys
[PROOF STEP]
apply (unfold unfold_lesub_list)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>set xs \<subseteq> A; set ys \<subseteq> A; length xs = length ys\<rbrakk> \<Longrightarrow> Listn.le r ys (xs [+f] ys)
[PROOF STEP]
apply (simp add: Listn.le_def list_all2_conv_all_nth)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Semilat) plus_list_lub [rule_format]:
shows "\<forall>xs ys zs. set xs \<subseteq> A \<longrightarrow> set ys \<subseteq> A \<longrightarrow> set zs \<subseteq> A
  \<longrightarrow> size xs = n \<and> size ys = n \<longrightarrow>
  xs [\<sqsubseteq>\<^bsub>r\<^esub>] zs \<and> ys [\<sqsubseteq>\<^bsub>r\<^esub>] zs \<longrightarrow> xs [\<squnion>\<^bsub>f\<^esub>] ys [\<sqsubseteq>\<^bsub>r\<^esub>] zs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>xs ys zs. set xs \<subseteq> A \<longrightarrow> set ys \<subseteq> A \<longrightarrow> set zs \<subseteq> A \<longrightarrow> length xs = n \<and> length ys = n \<longrightarrow> xs [\<sqsubseteq>\<^bsub>r\<^esub>] zs \<and> ys [\<sqsubseteq>\<^bsub>r\<^esub>] zs \<longrightarrow> xs [+f] ys [\<sqsubseteq>\<^bsub>r\<^esub>] zs
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>xs ys zs. set xs \<subseteq> A \<longrightarrow> set ys \<subseteq> A \<longrightarrow> set zs \<subseteq> A \<longrightarrow> length xs = n \<and> length ys = n \<longrightarrow> xs [\<sqsubseteq>\<^bsub>r\<^esub>] zs \<and> ys [\<sqsubseteq>\<^bsub>r\<^esub>] zs \<longrightarrow> xs [+f] ys [\<sqsubseteq>\<^bsub>r\<^esub>] zs
[PROOF STEP]
apply (unfold unfold_lesub_list)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>xs ys zs. set xs \<subseteq> A \<longrightarrow> set ys \<subseteq> A \<longrightarrow> set zs \<subseteq> A \<longrightarrow> length xs = n \<and> length ys = n \<longrightarrow> Listn.le r xs zs \<and> Listn.le r ys zs \<longrightarrow> Listn.le r (xs [+f] ys) zs
[PROOF STEP]
apply (simp add: Listn.le_def list_all2_conv_all_nth)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Semilat) list_update_incr [rule_format]:
 "x\<in>A \<Longrightarrow> set xs \<subseteq> A \<longrightarrow>
  (\<forall>i. i<size xs \<longrightarrow> xs [\<sqsubseteq>\<^bsub>r\<^esub>] xs[i := x \<squnion>\<^sub>f xs!i])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> A \<Longrightarrow> set xs \<subseteq> A \<longrightarrow> (\<forall>i<length xs. xs [\<sqsubseteq>\<^bsub>r\<^esub>] xs[i := x \<squnion>\<^bsub>f\<^esub> xs ! i])
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> A \<Longrightarrow> set xs \<subseteq> A \<longrightarrow> (\<forall>i<length xs. xs [\<sqsubseteq>\<^bsub>r\<^esub>] xs[i := x \<squnion>\<^bsub>f\<^esub> xs ! i])
[PROOF STEP]
apply (unfold unfold_lesub_list)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> A \<Longrightarrow> set xs \<subseteq> A \<longrightarrow> (\<forall>i<length xs. Listn.le r xs (xs[i := x \<squnion>\<^bsub>f\<^esub> xs ! i]))
[PROOF STEP]
apply (simp add: Listn.le_def list_all2_conv_all_nth)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> A \<Longrightarrow> set xs \<subseteq> A \<longrightarrow> (\<forall>i<length xs. \<forall>ia<length xs. xs ! ia \<sqsubseteq>\<^bsub>r\<^esub> xs[i := x \<squnion>\<^bsub>f\<^esub> xs ! i] ! ia)
[PROOF STEP]
apply (induct xs)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. x \<in> A \<Longrightarrow> set [] \<subseteq> A \<longrightarrow> (\<forall>i<length []. \<forall>ia<length []. [] ! ia \<sqsubseteq>\<^bsub>r\<^esub> [][i := x \<squnion>\<^bsub>f\<^esub> [] ! i] ! ia)
 2. \<And>a xs. \<lbrakk>x \<in> A \<Longrightarrow> set xs \<subseteq> A \<longrightarrow> (\<forall>i<length xs. \<forall>ia<length xs. xs ! ia \<sqsubseteq>\<^bsub>r\<^esub> xs[i := x \<squnion>\<^bsub>f\<^esub> xs ! i] ! ia); x \<in> A\<rbrakk> \<Longrightarrow> set (a # xs) \<subseteq> A \<longrightarrow> (\<forall>i<length (a # xs). \<forall>ia<length (a # xs). (a # xs) ! ia \<sqsubseteq>\<^bsub>r\<^esub> (a # xs)[i := x \<squnion>\<^bsub>f\<^esub> (a # xs) ! i] ! ia)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>x \<in> A \<Longrightarrow> set xs \<subseteq> A \<longrightarrow> (\<forall>i<length xs. \<forall>ia<length xs. xs ! ia \<sqsubseteq>\<^bsub>r\<^esub> xs[i := x \<squnion>\<^bsub>f\<^esub> xs ! i] ! ia); x \<in> A\<rbrakk> \<Longrightarrow> set (a # xs) \<subseteq> A \<longrightarrow> (\<forall>i<length (a # xs). \<forall>ia<length (a # xs). (a # xs) ! ia \<sqsubseteq>\<^bsub>r\<^esub> (a # xs)[i := x \<squnion>\<^bsub>f\<^esub> (a # xs) ! i] ! ia)
[PROOF STEP]
apply (simp add: in_list_Suc_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>set xs \<subseteq> A \<longrightarrow> (\<forall>i<length xs. \<forall>ia<length xs. xs ! ia \<sqsubseteq>\<^bsub>r\<^esub> xs[i := x \<squnion>\<^bsub>f\<^esub> xs ! i] ! ia); x \<in> A\<rbrakk> \<Longrightarrow> a \<in> A \<and> set xs \<subseteq> A \<longrightarrow> (\<forall>i<Suc (length xs). \<forall>ia<Suc (length xs). (a # xs) ! ia \<sqsubseteq>\<^bsub>r\<^esub> (case i of 0 \<Rightarrow> (x \<squnion>\<^bsub>f\<^esub> (a # xs) ! i) # xs | Suc j \<Rightarrow> a # xs[j := x \<squnion>\<^bsub>f\<^esub> (a # xs) ! i]) ! ia)
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a xs i ia. \<lbrakk>x \<in> A; a \<in> A; set xs \<subseteq> A; i < Suc (length xs); ia < Suc (length xs); \<forall>i<length xs. \<forall>ia<length xs. xs ! ia \<sqsubseteq>\<^bsub>r\<^esub> xs[i := x \<squnion>\<^bsub>f\<^esub> xs ! i] ! ia\<rbrakk> \<Longrightarrow> (a # xs) ! ia \<sqsubseteq>\<^bsub>r\<^esub> (case i of 0 \<Rightarrow> (x \<squnion>\<^bsub>f\<^esub> (a # xs) ! i) # xs | Suc j \<Rightarrow> a # xs[j := x \<squnion>\<^bsub>f\<^esub> (a # xs) ! i]) ! ia
[PROOF STEP]
apply (simp add: nth_Cons split: nat.split)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma acc_le_listI' [intro!]:
  "\<lbrakk> order r; acc A r \<rbrakk> \<Longrightarrow> acc (\<Union>n. list n A) (Listn.le r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>order r; acc A r\<rbrakk> \<Longrightarrow> acc (\<Union>n. list n A) (Listn.le r)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>order r; acc A r\<rbrakk> \<Longrightarrow> acc (\<Union>n. list n A) (Listn.le r)
[PROOF STEP]
apply (unfold acc_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>order r; wf {(y, x). x \<in> A \<and> y \<in> A \<and> x \<sqsubset>\<^bsub>r\<^esub> y}\<rbrakk> \<Longrightarrow> wf {(y, x). x \<in> (\<Union>n. list n A) \<and> y \<in> (\<Union>n. list n A) \<and> x [\<sqsubset>\<^bsub>r\<^esub>] y}
[PROOF STEP]
apply (subgoal_tac
 "wf(UN n. {(ys,xs). xs \<in> list n A \<and> ys \<in> list n A \<and> xs <_(Listn.le r) ys})")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>order r; wf {(y, x). x \<in> A \<and> y \<in> A \<and> x \<sqsubset>\<^bsub>r\<^esub> y}; wf (\<Union>n. {(ys, xs). xs \<in> list n A \<and> ys \<in> list n A \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys})\<rbrakk> \<Longrightarrow> wf {(y, x). x \<in> (\<Union>n. list n A) \<and> y \<in> (\<Union>n. list n A) \<and> x [\<sqsubset>\<^bsub>r\<^esub>] y}
 2. \<lbrakk>order r; wf {(y, x). x \<in> A \<and> y \<in> A \<and> x \<sqsubset>\<^bsub>r\<^esub> y}\<rbrakk> \<Longrightarrow> wf (\<Union>n. {(ys, xs). xs \<in> list n A \<and> ys \<in> list n A \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys})
[PROOF STEP]
apply (erule wf_subset)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>order r; wf {(y, x). x \<in> A \<and> y \<in> A \<and> x \<sqsubset>\<^bsub>r\<^esub> y}\<rbrakk> \<Longrightarrow> {(y, x). x \<in> (\<Union>n. list n A) \<and> y \<in> (\<Union>n. list n A) \<and> x [\<sqsubset>\<^bsub>r\<^esub>] y} \<subseteq> (\<Union>n. {(ys, xs). xs \<in> list n A \<and> ys \<in> list n A \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys})
 2. \<lbrakk>order r; wf {(y, x). x \<in> A \<and> y \<in> A \<and> x \<sqsubset>\<^bsub>r\<^esub> y}\<rbrakk> \<Longrightarrow> wf (\<Union>n. {(ys, xs). xs \<in> list n A \<and> ys \<in> list n A \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys})
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b n na. \<lbrakk>order r; wf {(y, x). x \<in> A \<and> y \<in> A \<and> x \<sqsubset>\<^bsub>r\<^esub> y}; n \<in> UNIV; b \<in> list n A; b [\<sqsubset>\<^bsub>r\<^esub>] a; na \<in> UNIV; a \<in> list na A\<rbrakk> \<Longrightarrow> (a, b) \<in> (\<Union>n. {(ys, xs). xs \<in> list n A \<and> ys \<in> list n A \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys})
 2. \<lbrakk>order r; wf {(y, x). x \<in> A \<and> y \<in> A \<and> x \<sqsubset>\<^bsub>r\<^esub> y}\<rbrakk> \<Longrightarrow> wf (\<Union>n. {(ys, xs). xs \<in> list n A \<and> ys \<in> list n A \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys})
[PROOF STEP]
apply(rule UN_I)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b n na. \<lbrakk>order r; wf {(y, x). x \<in> A \<and> y \<in> A \<and> x \<sqsubset>\<^bsub>r\<^esub> y}; n \<in> UNIV; b \<in> list n A; b [\<sqsubset>\<^bsub>r\<^esub>] a; na \<in> UNIV; a \<in> list na A\<rbrakk> \<Longrightarrow> ?a11 a b n na \<in> UNIV
 2. \<And>a b n na. \<lbrakk>order r; wf {(y, x). x \<in> A \<and> y \<in> A \<and> x \<sqsubset>\<^bsub>r\<^esub> y}; n \<in> UNIV; b \<in> list n A; b [\<sqsubset>\<^bsub>r\<^esub>] a; na \<in> UNIV; a \<in> list na A\<rbrakk> \<Longrightarrow> (a, b) \<in> {(ys, xs). xs \<in> list (?a11 a b n na) A \<and> ys \<in> list (?a11 a b n na) A \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys}
 3. \<lbrakk>order r; wf {(y, x). x \<in> A \<and> y \<in> A \<and> x \<sqsubset>\<^bsub>r\<^esub> y}\<rbrakk> \<Longrightarrow> wf (\<Union>n. {(ys, xs). xs \<in> list n A \<and> ys \<in> list n A \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys})
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b n na. \<lbrakk>order r; wf {(y, x). x \<in> A \<and> y \<in> A \<and> x \<sqsubset>\<^bsub>r\<^esub> y}; n \<in> UNIV; b \<in> list n A; b [\<sqsubset>\<^bsub>r\<^esub>] a; na \<in> UNIV; a \<in> list na A\<rbrakk> \<Longrightarrow> (a, b) \<in> {(ys, xs). xs \<in> list (?a11 a b n na) A \<and> ys \<in> list (?a11 a b n na) A \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys}
 2. \<And>a b n na. \<lbrakk>order r; wf {(y, x). x \<in> A \<and> y \<in> A \<and> x \<sqsubset>\<^bsub>r\<^esub> y}; n \<in> UNIV; b \<in> list n A; b [\<sqsubset>\<^bsub>r\<^esub>] a; na \<in> UNIV; a \<in> list na A\<rbrakk> \<Longrightarrow> ?a11 a b n na \<in> UNIV
 3. \<lbrakk>order r; wf {(y, x). x \<in> A \<and> y \<in> A \<and> x \<sqsubset>\<^bsub>r\<^esub> y}\<rbrakk> \<Longrightarrow> wf (\<Union>n. {(ys, xs). xs \<in> list n A \<and> ys \<in> list n A \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys})
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b n na. \<lbrakk>order r; wf {(y, x). x \<in> A \<and> y \<in> A \<and> x \<sqsubset>\<^bsub>r\<^esub> y}; n \<in> UNIV; b \<in> list n A; b [\<sqsubset>\<^bsub>r\<^esub>] a; na \<in> UNIV; a \<in> list na A\<rbrakk> \<Longrightarrow> b \<in> list (?a11 a b n na) A \<and> a \<in> list (?a11 a b n na) A \<and> b [\<sqsubset>\<^bsub>r\<^esub>] a
 2. \<And>a b n na. \<lbrakk>order r; wf {(y, x). x \<in> A \<and> y \<in> A \<and> x \<sqsubset>\<^bsub>r\<^esub> y}; n \<in> UNIV; b \<in> list n A; b [\<sqsubset>\<^bsub>r\<^esub>] a; na \<in> UNIV; a \<in> list na A\<rbrakk> \<Longrightarrow> ?a11 a b n na \<in> UNIV
 3. \<lbrakk>order r; wf {(y, x). x \<in> A \<and> y \<in> A \<and> x \<sqsubset>\<^bsub>r\<^esub> y}\<rbrakk> \<Longrightarrow> wf (\<Union>n. {(ys, xs). xs \<in> list n A \<and> ys \<in> list n A \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys})
[PROOF STEP]
apply(frule lesssub_lengthD)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b n na. \<lbrakk>order r; wf {(y, x). x \<in> A \<and> y \<in> A \<and> x \<sqsubset>\<^bsub>r\<^esub> y}; n \<in> UNIV; b \<in> list n A; b [\<sqsubset>\<^bsub>r\<^esub>] a; na \<in> UNIV; a \<in> list na A; length a = length b\<rbrakk> \<Longrightarrow> b \<in> list (?a11 a b n na) A \<and> a \<in> list (?a11 a b n na) A \<and> b [\<sqsubset>\<^bsub>r\<^esub>] a
 2. \<And>a b n na. \<lbrakk>order r; wf {(y, x). x \<in> A \<and> y \<in> A \<and> x \<sqsubset>\<^bsub>r\<^esub> y}; n \<in> UNIV; b \<in> list n A; b [\<sqsubset>\<^bsub>r\<^esub>] a; na \<in> UNIV; a \<in> list na A\<rbrakk> \<Longrightarrow> ?a11 a b n na \<in> UNIV
 3. \<lbrakk>order r; wf {(y, x). x \<in> A \<and> y \<in> A \<and> x \<sqsubset>\<^bsub>r\<^esub> y}\<rbrakk> \<Longrightarrow> wf (\<Union>n. {(ys, xs). xs \<in> list n A \<and> ys \<in> list n A \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys})
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b n na. \<lbrakk>order r; wf {(y, x). x \<in> A \<and> y \<in> A \<and> x \<sqsubset>\<^bsub>r\<^esub> y}; n \<in> UNIV; b \<in> list n A; b [\<sqsubset>\<^bsub>r\<^esub>] a; na \<in> UNIV; a \<in> list na A\<rbrakk> \<Longrightarrow> na \<in> UNIV
 2. \<lbrakk>order r; wf {(y, x). x \<in> A \<and> y \<in> A \<and> x \<sqsubset>\<^bsub>r\<^esub> y}\<rbrakk> \<Longrightarrow> wf (\<Union>n. {(ys, xs). xs \<in> list n A \<and> ys \<in> list n A \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys})
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>order r; wf {(y, x). x \<in> A \<and> y \<in> A \<and> x \<sqsubset>\<^bsub>r\<^esub> y}\<rbrakk> \<Longrightarrow> wf (\<Union>n. {(ys, xs). xs \<in> list n A \<and> ys \<in> list n A \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys})
[PROOF STEP]
apply (rule wf_UN)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>order r; wf {(y, x). x \<in> A \<and> y \<in> A \<and> x \<sqsubset>\<^bsub>r\<^esub> y}; n \<in> UNIV\<rbrakk> \<Longrightarrow> wf {(ys, xs). xs \<in> list n A \<and> ys \<in> list n A \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys}
 2. \<And>n j. \<lbrakk>order r; wf {(y, x). x \<in> A \<and> y \<in> A \<and> x \<sqsubset>\<^bsub>r\<^esub> y}; n \<in> UNIV; j \<in> UNIV; {(ys, xs). xs \<in> list n A \<and> ys \<in> list n A \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys} \<noteq> {(ys, xs). xs \<in> list j A \<and> ys \<in> list j A \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys}\<rbrakk> \<Longrightarrow> Domain {(ys, xs). xs \<in> list n A \<and> ys \<in> list n A \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys} \<inter> Range {(ys, xs). xs \<in> list j A \<and> ys \<in> list j A \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys} = {}
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n j. \<lbrakk>order r; wf {(y, x). x \<in> A \<and> y \<in> A \<and> x \<sqsubset>\<^bsub>r\<^esub> y}; n \<in> UNIV; j \<in> UNIV; {(ys, xs). xs \<in> list n A \<and> ys \<in> list n A \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys} \<noteq> {(ys, xs). xs \<in> list j A \<and> ys \<in> list j A \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys}\<rbrakk> \<Longrightarrow> Domain {(ys, xs). xs \<in> list n A \<and> ys \<in> list n A \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys} \<inter> Range {(ys, xs). xs \<in> list j A \<and> ys \<in> list j A \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys} = {}
 2. \<And>n. \<lbrakk>order r; wf {(y, x). x \<in> A \<and> y \<in> A \<and> x \<sqsubset>\<^bsub>r\<^esub> y}; n \<in> UNIV\<rbrakk> \<Longrightarrow> wf {(ys, xs). xs \<in> list n A \<and> ys \<in> list n A \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys}
[PROOF STEP]
apply (rename_tac m n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m n. \<lbrakk>order r; wf {(y, x). x \<in> A \<and> y \<in> A \<and> x \<sqsubset>\<^bsub>r\<^esub> y}; m \<in> UNIV; n \<in> UNIV; {(ys, xs). xs \<in> list m A \<and> ys \<in> list m A \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys} \<noteq> {(ys, xs). xs \<in> list n A \<and> ys \<in> list n A \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys}\<rbrakk> \<Longrightarrow> Domain {(ys, xs). xs \<in> list m A \<and> ys \<in> list m A \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys} \<inter> Range {(ys, xs). xs \<in> list n A \<and> ys \<in> list n A \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys} = {}
 2. \<And>n. \<lbrakk>order r; wf {(y, x). x \<in> A \<and> y \<in> A \<and> x \<sqsubset>\<^bsub>r\<^esub> y}; n \<in> UNIV\<rbrakk> \<Longrightarrow> wf {(ys, xs). xs \<in> list n A \<and> ys \<in> list n A \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys}
[PROOF STEP]
apply (case_tac "m=n")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>m n. \<lbrakk>order r; wf {(y, x). x \<in> A \<and> y \<in> A \<and> x \<sqsubset>\<^bsub>r\<^esub> y}; m \<in> UNIV; n \<in> UNIV; {(ys, xs). xs \<in> list m A \<and> ys \<in> list m A \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys} \<noteq> {(ys, xs). xs \<in> list n A \<and> ys \<in> list n A \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys}; m = n\<rbrakk> \<Longrightarrow> Domain {(ys, xs). xs \<in> list m A \<and> ys \<in> list m A \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys} \<inter> Range {(ys, xs). xs \<in> list n A \<and> ys \<in> list n A \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys} = {}
 2. \<And>m n. \<lbrakk>order r; wf {(y, x). x \<in> A \<and> y \<in> A \<and> x \<sqsubset>\<^bsub>r\<^esub> y}; m \<in> UNIV; n \<in> UNIV; {(ys, xs). xs \<in> list m A \<and> ys \<in> list m A \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys} \<noteq> {(ys, xs). xs \<in> list n A \<and> ys \<in> list n A \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys}; m \<noteq> n\<rbrakk> \<Longrightarrow> Domain {(ys, xs). xs \<in> list m A \<and> ys \<in> list m A \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys} \<inter> Range {(ys, xs). xs \<in> list n A \<and> ys \<in> list n A \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys} = {}
 3. \<And>n. \<lbrakk>order r; wf {(y, x). x \<in> A \<and> y \<in> A \<and> x \<sqsubset>\<^bsub>r\<^esub> y}; n \<in> UNIV\<rbrakk> \<Longrightarrow> wf {(ys, xs). xs \<in> list n A \<and> ys \<in> list n A \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m n. \<lbrakk>order r; wf {(y, x). x \<in> A \<and> y \<in> A \<and> x \<sqsubset>\<^bsub>r\<^esub> y}; m \<in> UNIV; n \<in> UNIV; {(ys, xs). xs \<in> list m A \<and> ys \<in> list m A \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys} \<noteq> {(ys, xs). xs \<in> list n A \<and> ys \<in> list n A \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys}; m \<noteq> n\<rbrakk> \<Longrightarrow> Domain {(ys, xs). xs \<in> list m A \<and> ys \<in> list m A \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys} \<inter> Range {(ys, xs). xs \<in> list n A \<and> ys \<in> list n A \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys} = {}
 2. \<And>n. \<lbrakk>order r; wf {(y, x). x \<in> A \<and> y \<in> A \<and> x \<sqsubset>\<^bsub>r\<^esub> y}; n \<in> UNIV\<rbrakk> \<Longrightarrow> wf {(ys, xs). xs \<in> list n A \<and> ys \<in> list n A \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys}
[PROOF STEP]
apply (clarsimp intro!: equals0I)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m n y xs ys. \<lbrakk>order r; wf {(y, x). x \<in> A \<and> y \<in> A \<and> x \<sqsubset>\<^bsub>r\<^esub> y}; {(ys, xs). xs \<in> list m A \<and> ys \<in> list m A \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys} \<noteq> {(ys, xs). xs \<in> list n A \<and> ys \<in> list n A \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys}; m \<noteq> n; y \<in> list n A; xs \<in> list m A; ys \<in> list n A; y [\<sqsubset>\<^bsub>r\<^esub>] ys; y \<in> list m A; xs [\<sqsubset>\<^bsub>r\<^esub>] y\<rbrakk> \<Longrightarrow> False
 2. \<And>n. \<lbrakk>order r; wf {(y, x). x \<in> A \<and> y \<in> A \<and> x \<sqsubset>\<^bsub>r\<^esub> y}; n \<in> UNIV\<rbrakk> \<Longrightarrow> wf {(ys, xs). xs \<in> list n A \<and> ys \<in> list n A \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys}
[PROOF STEP]
apply (drule lesssub_lengthD)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m n y xs ys. \<lbrakk>order r; wf {(y, x). x \<in> A \<and> y \<in> A \<and> x \<sqsubset>\<^bsub>r\<^esub> y}; {(ys, xs). xs \<in> list m A \<and> ys \<in> list m A \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys} \<noteq> {(ys, xs). xs \<in> list n A \<and> ys \<in> list n A \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys}; m \<noteq> n; y \<in> list n A; xs \<in> list m A; ys \<in> list n A; y \<in> list m A; length ys = length y; length y = length xs\<rbrakk> \<Longrightarrow> False
 2. \<And>n. \<lbrakk>order r; wf {(y, x). x \<in> A \<and> y \<in> A \<and> x \<sqsubset>\<^bsub>r\<^esub> y}; n \<in> UNIV\<rbrakk> \<Longrightarrow> wf {(ys, xs). xs \<in> list n A \<and> ys \<in> list n A \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>order r; wf {(y, x). x \<in> A \<and> y \<in> A \<and> x \<sqsubset>\<^bsub>r\<^esub> y}; n \<in> UNIV\<rbrakk> \<Longrightarrow> wf {(ys, xs). xs \<in> list n A \<and> ys \<in> list n A \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys}
[PROOF STEP]
apply (induct_tac n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>order r; wf {(y, x). x \<in> A \<and> y \<in> A \<and> x \<sqsubset>\<^bsub>r\<^esub> y}; n \<in> UNIV\<rbrakk> \<Longrightarrow> wf {a. case a of (ys, xs) \<Rightarrow> xs \<in> list 0 A \<and> ys \<in> list 0 A \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys}
 2. \<And>n na. \<lbrakk>order r; wf {(y, x). x \<in> A \<and> y \<in> A \<and> x \<sqsubset>\<^bsub>r\<^esub> y}; n \<in> UNIV; wf {a. case a of (ys, xs) \<Rightarrow> xs \<in> list na A \<and> ys \<in> list na A \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys}\<rbrakk> \<Longrightarrow> wf {a. case a of (ys, xs) \<Rightarrow> xs \<in> list (Suc na) A \<and> ys \<in> list (Suc na) A \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys}
[PROOF STEP]
apply (simp add: lesssub_def cong: conj_cong)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n na. \<lbrakk>order r; wf {(y, x). x \<in> A \<and> y \<in> A \<and> x \<sqsubset>\<^bsub>r\<^esub> y}; n \<in> UNIV; wf {a. case a of (ys, xs) \<Rightarrow> xs \<in> list na A \<and> ys \<in> list na A \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys}\<rbrakk> \<Longrightarrow> wf {a. case a of (ys, xs) \<Rightarrow> xs \<in> list (Suc na) A \<and> ys \<in> list (Suc na) A \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys}
[PROOF STEP]
apply (rename_tac k)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n k. \<lbrakk>order r; wf {(y, x). x \<in> A \<and> y \<in> A \<and> x \<sqsubset>\<^bsub>r\<^esub> y}; n \<in> UNIV; wf {a. case a of (ys, xs) \<Rightarrow> xs \<in> list k A \<and> ys \<in> list k A \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys}\<rbrakk> \<Longrightarrow> wf {a. case a of (ys, xs) \<Rightarrow> xs \<in> list (Suc k) A \<and> ys \<in> list (Suc k) A \<and> xs [\<sqsubset>\<^bsub>r\<^esub>] ys}
[PROOF STEP]
apply (simp add: wf_eq_minimal)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>order r; \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. z \<in> A \<and> y \<in> A \<and> z \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> y \<notin> Q); \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. z \<in> list k A \<and> y \<in> list k A \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> Q)\<rbrakk> \<Longrightarrow> \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. z \<in> list (Suc k) A \<and> y \<in> list (Suc k) A \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> Q)
[PROOF STEP]
apply (simp (no_asm) add: in_list_Suc_iff cong: conj_cong)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>order r; \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. z \<in> A \<and> y \<in> A \<and> z \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> y \<notin> Q); \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. z \<in> list k A \<and> y \<in> list k A \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> Q)\<rbrakk> \<Longrightarrow> \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. (\<exists>y\<in>A. \<exists>ys\<in>list k A. z = y # ys) \<and> (\<exists>ya\<in>A. \<exists>ys\<in>list k A. y = ya # ys) \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> Q)
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k Q x. \<lbrakk>order r; \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. z \<in> A \<and> y \<in> A \<and> z \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> y \<notin> Q); \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. z \<in> list k A \<and> y \<in> list k A \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> Q); x \<in> Q\<rbrakk> \<Longrightarrow> \<exists>z\<in>Q. \<forall>y. (\<exists>y\<in>A. \<exists>ys\<in>list k A. z = y # ys) \<and> (\<exists>ya\<in>A. \<exists>ys\<in>list k A. y = ya # ys) \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> Q
[PROOF STEP]
apply (rename_tac M m)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k M m. \<lbrakk>order r; \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. z \<in> A \<and> y \<in> A \<and> z \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> y \<notin> Q); \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. z \<in> list k A \<and> y \<in> list k A \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> Q); m \<in> M\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y\<in>A. \<exists>ys\<in>list k A. z = y # ys) \<and> (\<exists>ya\<in>A. \<exists>ys\<in>list k A. y = ya # ys) \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> M
[PROOF STEP]
apply (case_tac "\<exists>x\<in>A. \<exists>xs\<in>list k A. x#xs \<in> M")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>k M m. \<lbrakk>order r; \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. z \<in> A \<and> y \<in> A \<and> z \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> y \<notin> Q); \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. z \<in> list k A \<and> y \<in> list k A \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> Q); m \<in> M; \<exists>x\<in>A. \<exists>xs\<in>list k A. x # xs \<in> M\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y\<in>A. \<exists>ys\<in>list k A. z = y # ys) \<and> (\<exists>ya\<in>A. \<exists>ys\<in>list k A. y = ya # ys) \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> M
 2. \<And>k M m. \<lbrakk>order r; \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. z \<in> A \<and> y \<in> A \<and> z \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> y \<notin> Q); \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. z \<in> list k A \<and> y \<in> list k A \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> Q); m \<in> M; \<not> (\<exists>x\<in>A. \<exists>xs\<in>list k A. x # xs \<in> M)\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y\<in>A. \<exists>ys\<in>list k A. z = y # ys) \<and> (\<exists>ya\<in>A. \<exists>ys\<in>list k A. y = ya # ys) \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> M
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>k M m. \<lbrakk>order r; \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. z \<in> A \<and> y \<in> A \<and> z \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> y \<notin> Q); \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. z \<in> list k A \<and> y \<in> list k A \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> Q); m \<in> M; \<not> (\<exists>x\<in>A. \<exists>xs\<in>list k A. x # xs \<in> M)\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y\<in>A. \<exists>ys\<in>list k A. z = y # ys) \<and> (\<exists>ya\<in>A. \<exists>ys\<in>list k A. y = ya # ys) \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> M
 2. \<And>k M m. \<lbrakk>order r; \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. z \<in> A \<and> y \<in> A \<and> z \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> y \<notin> Q); \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. z \<in> list k A \<and> y \<in> list k A \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> Q); m \<in> M; \<exists>x\<in>A. \<exists>xs\<in>list k A. x # xs \<in> M\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y\<in>A. \<exists>ys\<in>list k A. z = y # ys) \<and> (\<exists>ya\<in>A. \<exists>ys\<in>list k A. y = ya # ys) \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> M
[PROOF STEP]
apply (erule thin_rl)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>k M m. \<lbrakk>\<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. z \<in> A \<and> y \<in> A \<and> z \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> y \<notin> Q); \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. z \<in> list k A \<and> y \<in> list k A \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> Q); m \<in> M; \<not> (\<exists>x\<in>A. \<exists>xs\<in>list k A. x # xs \<in> M)\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y\<in>A. \<exists>ys\<in>list k A. z = y # ys) \<and> (\<exists>ya\<in>A. \<exists>ys\<in>list k A. y = ya # ys) \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> M
 2. \<And>k M m. \<lbrakk>order r; \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. z \<in> A \<and> y \<in> A \<and> z \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> y \<notin> Q); \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. z \<in> list k A \<and> y \<in> list k A \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> Q); m \<in> M; \<exists>x\<in>A. \<exists>xs\<in>list k A. x # xs \<in> M\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y\<in>A. \<exists>ys\<in>list k A. z = y # ys) \<and> (\<exists>ya\<in>A. \<exists>ys\<in>list k A. y = ya # ys) \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> M
[PROOF STEP]
apply (erule thin_rl)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>k M m. \<lbrakk>\<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. z \<in> list k A \<and> y \<in> list k A \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> Q); m \<in> M; \<not> (\<exists>x\<in>A. \<exists>xs\<in>list k A. x # xs \<in> M)\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y\<in>A. \<exists>ys\<in>list k A. z = y # ys) \<and> (\<exists>ya\<in>A. \<exists>ys\<in>list k A. y = ya # ys) \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> M
 2. \<And>k M m. \<lbrakk>order r; \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. z \<in> A \<and> y \<in> A \<and> z \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> y \<notin> Q); \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. z \<in> list k A \<and> y \<in> list k A \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> Q); m \<in> M; \<exists>x\<in>A. \<exists>xs\<in>list k A. x # xs \<in> M\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y\<in>A. \<exists>ys\<in>list k A. z = y # ys) \<and> (\<exists>ya\<in>A. \<exists>ys\<in>list k A. y = ya # ys) \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> M
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k M m. \<lbrakk>order r; \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. z \<in> A \<and> y \<in> A \<and> z \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> y \<notin> Q); \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. z \<in> list k A \<and> y \<in> list k A \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> Q); m \<in> M; \<exists>x\<in>A. \<exists>xs\<in>list k A. x # xs \<in> M\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y\<in>A. \<exists>ys\<in>list k A. z = y # ys) \<and> (\<exists>ya\<in>A. \<exists>ys\<in>list k A. y = ya # ys) \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> M
[PROOF STEP]
apply (erule_tac x = "{a. a \<in> A \<and> (\<exists>xs\<in>list k A. a#xs\<in>M)}" in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k M m. \<lbrakk>order r; \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. z \<in> list k A \<and> y \<in> list k A \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> Q); m \<in> M; \<exists>x\<in>A. \<exists>xs\<in>list k A. x # xs \<in> M; (\<exists>x. x \<in> {a \<in> A. \<exists>xs\<in>list k A. a # xs \<in> M}) \<longrightarrow> (\<exists>z\<in>{a \<in> A. \<exists>xs\<in>list k A. a # xs \<in> M}. \<forall>y. z \<in> A \<and> y \<in> A \<and> z \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> y \<notin> {a \<in> A. \<exists>xs\<in>list k A. a # xs \<in> M})\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y\<in>A. \<exists>ys\<in>list k A. z = y # ys) \<and> (\<exists>ya\<in>A. \<exists>ys\<in>list k A. y = ya # ys) \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> M
[PROOF STEP]
apply (erule impE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>k M m. \<lbrakk>order r; \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. z \<in> list k A \<and> y \<in> list k A \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> Q); m \<in> M; \<exists>x\<in>A. \<exists>xs\<in>list k A. x # xs \<in> M\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> {a \<in> A. \<exists>xs\<in>list k A. a # xs \<in> M}
 2. \<And>k M m. \<lbrakk>order r; \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. z \<in> list k A \<and> y \<in> list k A \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> Q); m \<in> M; \<exists>x\<in>A. \<exists>xs\<in>list k A. x # xs \<in> M; \<exists>z\<in>{a \<in> A. \<exists>xs\<in>list k A. a # xs \<in> M}. \<forall>y. z \<in> A \<and> y \<in> A \<and> z \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> y \<notin> {a \<in> A. \<exists>xs\<in>list k A. a # xs \<in> M}\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y\<in>A. \<exists>ys\<in>list k A. z = y # ys) \<and> (\<exists>ya\<in>A. \<exists>ys\<in>list k A. y = ya # ys) \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> M
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k M m. \<lbrakk>order r; \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. z \<in> list k A \<and> y \<in> list k A \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> Q); m \<in> M; \<exists>x\<in>A. \<exists>xs\<in>list k A. x # xs \<in> M; \<exists>z\<in>{a \<in> A. \<exists>xs\<in>list k A. a # xs \<in> M}. \<forall>y. z \<in> A \<and> y \<in> A \<and> z \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> y \<notin> {a \<in> A. \<exists>xs\<in>list k A. a # xs \<in> M}\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y\<in>A. \<exists>ys\<in>list k A. z = y # ys) \<and> (\<exists>ya\<in>A. \<exists>ys\<in>list k A. y = ya # ys) \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> M
[PROOF STEP]
apply (thin_tac "\<exists>x\<in>A. \<exists>xs\<in>list k A. P x xs" for P)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k M m. \<lbrakk>order r; \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. z \<in> list k A \<and> y \<in> list k A \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> Q); m \<in> M; \<exists>z\<in>{a \<in> A. \<exists>xs\<in>list k A. a # xs \<in> M}. \<forall>y. z \<in> A \<and> y \<in> A \<and> z \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> y \<notin> {a \<in> A. \<exists>xs\<in>list k A. a # xs \<in> M}\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y\<in>A. \<exists>ys\<in>list k A. z = y # ys) \<and> (\<exists>ya\<in>A. \<exists>ys\<in>list k A. y = ya # ys) \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> M
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k M m z xs. \<lbrakk>order r; \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. z \<in> list k A \<and> y \<in> list k A \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> Q); m \<in> M; \<forall>y. z \<in> A \<and> y \<in> A \<and> z \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> y \<notin> {a \<in> A. \<exists>xs\<in>list k A. a # xs \<in> M}; z \<in> A; xs \<in> list k A; z # xs \<in> M\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y\<in>A. \<exists>ys\<in>list k A. z = y # ys) \<and> (\<exists>ya\<in>A. \<exists>ys\<in>list k A. y = ya # ys) \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> M
[PROOF STEP]
apply (rename_tac maxA xs)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k M m maxA xs. \<lbrakk>order r; \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. z \<in> list k A \<and> y \<in> list k A \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> Q); m \<in> M; \<forall>y. maxA \<in> A \<and> y \<in> A \<and> maxA \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> y \<notin> {a \<in> A. \<exists>xs\<in>list k A. a # xs \<in> M}; maxA \<in> A; xs \<in> list k A; maxA # xs \<in> M\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y\<in>A. \<exists>ys\<in>list k A. z = y # ys) \<and> (\<exists>ya\<in>A. \<exists>ys\<in>list k A. y = ya # ys) \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> M
[PROOF STEP]
apply (erule_tac x = "{ys. ys \<in> list k A \<and> maxA#ys \<in> M}" in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k M m maxA xs. \<lbrakk>order r; m \<in> M; \<forall>y. maxA \<in> A \<and> y \<in> A \<and> maxA \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> y \<notin> {a \<in> A. \<exists>xs\<in>list k A. a # xs \<in> M}; maxA \<in> A; xs \<in> list k A; maxA # xs \<in> M; (\<exists>x. x \<in> {ys \<in> list k A. maxA # ys \<in> M}) \<longrightarrow> (\<exists>z\<in>{ys \<in> list k A. maxA # ys \<in> M}. \<forall>y. z \<in> list k A \<and> y \<in> list k A \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> {ys \<in> list k A. maxA # ys \<in> M})\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y\<in>A. \<exists>ys\<in>list k A. z = y # ys) \<and> (\<exists>ya\<in>A. \<exists>ys\<in>list k A. y = ya # ys) \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> M
[PROOF STEP]
apply (erule impE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>k M m maxA xs. \<lbrakk>order r; m \<in> M; \<forall>y. maxA \<in> A \<and> y \<in> A \<and> maxA \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> y \<notin> {a \<in> A. \<exists>xs\<in>list k A. a # xs \<in> M}; maxA \<in> A; xs \<in> list k A; maxA # xs \<in> M\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> {ys \<in> list k A. maxA # ys \<in> M}
 2. \<And>k M m maxA xs. \<lbrakk>order r; m \<in> M; \<forall>y. maxA \<in> A \<and> y \<in> A \<and> maxA \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> y \<notin> {a \<in> A. \<exists>xs\<in>list k A. a # xs \<in> M}; maxA \<in> A; xs \<in> list k A; maxA # xs \<in> M; \<exists>z\<in>{ys \<in> list k A. maxA # ys \<in> M}. \<forall>y. z \<in> list k A \<and> y \<in> list k A \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> {ys \<in> list k A. maxA # ys \<in> M}\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y\<in>A. \<exists>ys\<in>list k A. z = y # ys) \<and> (\<exists>ya\<in>A. \<exists>ys\<in>list k A. y = ya # ys) \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> M
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k M m maxA xs. \<lbrakk>order r; m \<in> M; \<forall>y. maxA \<in> A \<and> y \<in> A \<and> maxA \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> y \<notin> {a \<in> A. \<exists>xs\<in>list k A. a # xs \<in> M}; maxA \<in> A; xs \<in> list k A; maxA # xs \<in> M; \<exists>z\<in>{ys \<in> list k A. maxA # ys \<in> M}. \<forall>y. z \<in> list k A \<and> y \<in> list k A \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> {ys \<in> list k A. maxA # ys \<in> M}\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y\<in>A. \<exists>ys\<in>list k A. z = y # ys) \<and> (\<exists>ya\<in>A. \<exists>ys\<in>list k A. y = ya # ys) \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> M
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k M m maxA xs z. \<lbrakk>order r; m \<in> M; \<forall>y. maxA \<in> A \<and> y \<in> A \<and> maxA \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> y \<notin> {a \<in> A. \<exists>xs\<in>list k A. a # xs \<in> M}; maxA \<in> A; xs \<in> list k A; maxA # xs \<in> M; \<forall>y. z \<in> list k A \<and> y \<in> list k A \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> {ys \<in> list k A. maxA # ys \<in> M}; z \<in> list k A; maxA # z \<in> M\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y\<in>A. \<exists>ys\<in>list k A. z = y # ys) \<and> (\<exists>ya\<in>A. \<exists>ys\<in>list k A. y = ya # ys) \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> M
[PROOF STEP]
apply (thin_tac "m \<in> M")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k M m maxA xs z. \<lbrakk>order r; \<forall>y. maxA \<in> A \<and> y \<in> A \<and> maxA \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> y \<notin> {a \<in> A. \<exists>xs\<in>list k A. a # xs \<in> M}; maxA \<in> A; xs \<in> list k A; maxA # xs \<in> M; \<forall>y. z \<in> list k A \<and> y \<in> list k A \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> {ys \<in> list k A. maxA # ys \<in> M}; z \<in> list k A; maxA # z \<in> M\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y\<in>A. \<exists>ys\<in>list k A. z = y # ys) \<and> (\<exists>ya\<in>A. \<exists>ys\<in>list k A. y = ya # ys) \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> M
[PROOF STEP]
apply (thin_tac "maxA#xs \<in> M")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k M m maxA xs z. \<lbrakk>order r; \<forall>y. maxA \<in> A \<and> y \<in> A \<and> maxA \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> y \<notin> {a \<in> A. \<exists>xs\<in>list k A. a # xs \<in> M}; maxA \<in> A; xs \<in> list k A; \<forall>y. z \<in> list k A \<and> y \<in> list k A \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> {ys \<in> list k A. maxA # ys \<in> M}; z \<in> list k A; maxA # z \<in> M\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y\<in>A. \<exists>ys\<in>list k A. z = y # ys) \<and> (\<exists>ya\<in>A. \<exists>ys\<in>list k A. y = ya # ys) \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> M
[PROOF STEP]
apply (rule bexI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>k M m maxA xs z. \<lbrakk>order r; \<forall>y. maxA \<in> A \<and> y \<in> A \<and> maxA \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> y \<notin> {a \<in> A. \<exists>xs\<in>list k A. a # xs \<in> M}; maxA \<in> A; xs \<in> list k A; \<forall>y. z \<in> list k A \<and> y \<in> list k A \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> {ys \<in> list k A. maxA # ys \<in> M}; z \<in> list k A; maxA # z \<in> M\<rbrakk> \<Longrightarrow> \<forall>y. (\<exists>y\<in>A. \<exists>ys\<in>list k A. ?z167 k M m maxA xs z = y # ys) \<and> (\<exists>ya\<in>A. \<exists>ys\<in>list k A. y = ya # ys) \<and> ?z167 k M m maxA xs z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> M
 2. \<And>k M m maxA xs z. \<lbrakk>order r; \<forall>y. maxA \<in> A \<and> y \<in> A \<and> maxA \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> y \<notin> {a \<in> A. \<exists>xs\<in>list k A. a # xs \<in> M}; maxA \<in> A; xs \<in> list k A; \<forall>y. z \<in> list k A \<and> y \<in> list k A \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> {ys \<in> list k A. maxA # ys \<in> M}; z \<in> list k A; maxA # z \<in> M\<rbrakk> \<Longrightarrow> ?z167 k M m maxA xs z \<in> M
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>k M m maxA xs z. \<lbrakk>order r; \<forall>y. maxA \<in> A \<and> y \<in> A \<and> maxA \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> y \<notin> {a \<in> A. \<exists>xs\<in>list k A. a # xs \<in> M}; maxA \<in> A; xs \<in> list k A; \<forall>y. z \<in> list k A \<and> y \<in> list k A \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> {ys \<in> list k A. maxA # ys \<in> M}; z \<in> list k A; maxA # z \<in> M\<rbrakk> \<Longrightarrow> ?z167 k M m maxA xs z \<in> M
 2. \<And>k M m maxA xs z. \<lbrakk>order r; \<forall>y. maxA \<in> A \<and> y \<in> A \<and> maxA \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> y \<notin> {a \<in> A. \<exists>xs\<in>list k A. a # xs \<in> M}; maxA \<in> A; xs \<in> list k A; \<forall>y. z \<in> list k A \<and> y \<in> list k A \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> {ys \<in> list k A. maxA # ys \<in> M}; z \<in> list k A; maxA # z \<in> M\<rbrakk> \<Longrightarrow> \<forall>y. (\<exists>y\<in>A. \<exists>ys\<in>list k A. ?z167 k M m maxA xs z = y # ys) \<and> (\<exists>ya\<in>A. \<exists>ys\<in>list k A. y = ya # ys) \<and> ?z167 k M m maxA xs z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> M
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k M m maxA xs z. \<lbrakk>order r; \<forall>y. maxA \<in> A \<and> y \<in> A \<and> maxA \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> y \<notin> {a \<in> A. \<exists>xs\<in>list k A. a # xs \<in> M}; maxA \<in> A; xs \<in> list k A; \<forall>y. z \<in> list k A \<and> y \<in> list k A \<and> z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> {ys \<in> list k A. maxA # ys \<in> M}; z \<in> list k A; maxA # z \<in> M\<rbrakk> \<Longrightarrow> \<forall>y. (\<exists>y\<in>A. \<exists>ys\<in>list k A. maxA # z = y # ys) \<and> (\<exists>ya\<in>A. \<exists>ys\<in>list k A. y = ya # ys) \<and> maxA # z [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> M
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k M m maxA xs z y ya ys yb ysa. \<lbrakk>order r; \<forall>y. ya \<in> A \<and> y \<in> A \<and> ya \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> y \<notin> {a \<in> A. \<exists>xs\<in>list k A. a # xs \<in> M}; ya \<in> A; xs \<in> list k A; \<forall>y. ys \<in> list k A \<and> y \<in> list k A \<and> ys [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> y \<notin> {ys \<in> list k A. ya # ys \<in> M}; ys \<in> list k A; ya # ys \<in> M; ya \<in> A; ys \<in> list k A; ya # ys [\<sqsubset>\<^bsub>r\<^esub>] yb # ysa; yb \<in> A; ysa \<in> list k A; yb # ysa \<in> M\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k M xs ya ys yb ysa. \<lbrakk>order r; \<forall>y. y \<in> A \<and> ya \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> (\<forall>xs\<in>list k A. y # xs \<notin> M); xs \<in> list k A; \<forall>y. y \<in> list k A \<and> ys [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> ya # y \<notin> M; ya # ys \<in> M; ya \<in> A; ys \<in> list k A; ya \<sqsubset>\<^bsub>r\<^esub> yb \<and> ys [\<sqsubseteq>\<^bsub>r\<^esub>] ysa \<or> ya = yb \<and> ys [\<sqsubset>\<^bsub>r\<^esub>] ysa; yb \<in> A; ysa \<in> list k A; yb # ysa \<in> M\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (erule disjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>k M xs ya ys yb ysa. \<lbrakk>order r; \<forall>y. y \<in> A \<and> ya \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> (\<forall>xs\<in>list k A. y # xs \<notin> M); xs \<in> list k A; \<forall>y. y \<in> list k A \<and> ys [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> ya # y \<notin> M; ya # ys \<in> M; ya \<in> A; ys \<in> list k A; yb \<in> A; ysa \<in> list k A; yb # ysa \<in> M; ya \<sqsubset>\<^bsub>r\<^esub> yb \<and> ys [\<sqsubseteq>\<^bsub>r\<^esub>] ysa\<rbrakk> \<Longrightarrow> False
 2. \<And>k M xs ya ys yb ysa. \<lbrakk>order r; \<forall>y. y \<in> A \<and> ya \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> (\<forall>xs\<in>list k A. y # xs \<notin> M); xs \<in> list k A; \<forall>y. y \<in> list k A \<and> ys [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> ya # y \<notin> M; ya # ys \<in> M; ya \<in> A; ys \<in> list k A; yb \<in> A; ysa \<in> list k A; yb # ysa \<in> M; ya = yb \<and> ys [\<sqsubset>\<^bsub>r\<^esub>] ysa\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>k M xs ya ys yb ysa. \<lbrakk>order r; \<forall>y. y \<in> A \<and> ya \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> (\<forall>xs\<in>list k A. y # xs \<notin> M); xs \<in> list k A; \<forall>y. y \<in> list k A \<and> ys [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> ya # y \<notin> M; ya # ys \<in> M; ya \<in> A; ys \<in> list k A; yb \<in> A; ysa \<in> list k A; yb # ysa \<in> M; ya = yb \<and> ys [\<sqsubset>\<^bsub>r\<^esub>] ysa\<rbrakk> \<Longrightarrow> False
 2. \<And>k M xs ya ys yb ysa. \<lbrakk>order r; \<forall>y. y \<in> A \<and> ya \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> (\<forall>xs\<in>list k A. y # xs \<notin> M); xs \<in> list k A; \<forall>y. y \<in> list k A \<and> ys [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> ya # y \<notin> M; ya # ys \<in> M; ya \<in> A; ys \<in> list k A; yb \<in> A; ysa \<in> list k A; yb # ysa \<in> M; ya \<sqsubset>\<^bsub>r\<^esub> yb \<and> ys [\<sqsubseteq>\<^bsub>r\<^esub>] ysa\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k M xs ya ys yb ysa. \<lbrakk>order r; \<forall>y. y \<in> A \<and> ya \<sqsubset>\<^bsub>r\<^esub> y \<longrightarrow> (\<forall>xs\<in>list k A. y # xs \<notin> M); xs \<in> list k A; \<forall>y. y \<in> list k A \<and> ys [\<sqsubset>\<^bsub>r\<^esub>] y \<longrightarrow> ya # y \<notin> M; ya # ys \<in> M; ya \<in> A; ys \<in> list k A; yb \<in> A; ysa \<in> list k A; yb # ysa \<in> M; ya \<sqsubset>\<^bsub>r\<^esub> yb \<and> ys [\<sqsubseteq>\<^bsub>r\<^esub>] ysa\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by fastforce


[STATEMENT]
lemma acc_le_listI [intro!]:
  "\<lbrakk> order r; acc A r \<rbrakk> \<Longrightarrow> acc (list n A) (Listn.le r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>order r; acc A r\<rbrakk> \<Longrightarrow> acc (list n A) (Listn.le r)
[PROOF STEP]
apply(drule (1) acc_le_listI')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>acc A r; acc (\<Union>n. list n A) (Listn.le r)\<rbrakk> \<Longrightarrow> acc (list n A) (Listn.le r)
[PROOF STEP]
apply(erule thin_rl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. acc (\<Union>n. list n A) (Listn.le r) \<Longrightarrow> acc (list n A) (Listn.le r)
[PROOF STEP]
apply(unfold acc_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf {(y, x). x \<in> (\<Union>n. list n A) \<and> y \<in> (\<Union>n. list n A) \<and> x [\<sqsubset>\<^bsub>r\<^esub>] y} \<Longrightarrow> wf {(y, x). x \<in> list n A \<and> y \<in> list n A \<and> x [\<sqsubset>\<^bsub>r\<^esub>] y}
[PROOF STEP]
apply(erule wf_subset)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(y, x). x \<in> list n A \<and> y \<in> list n A \<and> x [\<sqsubset>\<^bsub>r\<^esub>] y} \<subseteq> {(y, x). x \<in> (\<Union>n. list n A) \<and> y \<in> (\<Union>n. list n A) \<and> x [\<sqsubset>\<^bsub>r\<^esub>] y}
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma acc_le_list_uptoI [intro!]:
  "\<lbrakk> order r; acc A r \<rbrakk> \<Longrightarrow> acc (\<Union>{list n A|n. n \<le> mxs}) (Listn.le r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>order r; acc A r\<rbrakk> \<Longrightarrow> acc (\<Union> {list n A |n. n \<le> mxs}) (Listn.le r)
[PROOF STEP]
apply(drule (1) acc_le_listI')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>acc A r; acc (\<Union>n. list n A) (Listn.le r)\<rbrakk> \<Longrightarrow> acc (\<Union> {list n A |n. n \<le> mxs}) (Listn.le r)
[PROOF STEP]
apply(erule thin_rl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. acc (\<Union>n. list n A) (Listn.le r) \<Longrightarrow> acc (\<Union> {list n A |n. n \<le> mxs}) (Listn.le r)
[PROOF STEP]
apply(unfold acc_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf {(y, x). x \<in> (\<Union>n. list n A) \<and> y \<in> (\<Union>n. list n A) \<and> x [\<sqsubset>\<^bsub>r\<^esub>] y} \<Longrightarrow> wf {(y, x). x \<in> \<Union> {list n A |n. n \<le> mxs} \<and> y \<in> \<Union> {list n A |n. n \<le> mxs} \<and> x [\<sqsubset>\<^bsub>r\<^esub>] y}
[PROOF STEP]
apply(erule wf_subset)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(y, x). x \<in> \<Union> {list n A |n. n \<le> mxs} \<and> y \<in> \<Union> {list n A |n. n \<le> mxs} \<and> x [\<sqsubset>\<^bsub>r\<^esub>] y} \<subseteq> {(y, x). x \<in> (\<Union>n. list n A) \<and> y \<in> (\<Union>n. list n A) \<and> x [\<sqsubset>\<^bsub>r\<^esub>] y}
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma closed_listI:
  "closed S f \<Longrightarrow> closed (list n S) (map2 f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed S f \<Longrightarrow> closed (list n S) (map2 f)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed S f \<Longrightarrow> closed (list n S) (map2 f)
[PROOF STEP]
apply (unfold closed_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>S. \<forall>y\<in>S. x \<squnion>\<^bsub>f\<^esub> y \<in> S \<Longrightarrow> \<forall>x\<in>list n S. \<forall>y\<in>list n S. x [+f] y \<in> list n S
[PROOF STEP]
apply (induct n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>x\<in>S. \<forall>y\<in>S. x \<squnion>\<^bsub>f\<^esub> y \<in> S \<Longrightarrow> \<forall>x\<in>list 0 S. \<forall>y\<in>list 0 S. x [+f] y \<in> list 0 S
 2. \<And>n. \<lbrakk>\<forall>x\<in>S. \<forall>y\<in>S. x \<squnion>\<^bsub>f\<^esub> y \<in> S \<Longrightarrow> \<forall>x\<in>list n S. \<forall>y\<in>list n S. x [+f] y \<in> list n S; \<forall>x\<in>S. \<forall>y\<in>S. x \<squnion>\<^bsub>f\<^esub> y \<in> S\<rbrakk> \<Longrightarrow> \<forall>x\<in>list (Suc n) S. \<forall>y\<in>list (Suc n) S. x [+f] y \<in> list (Suc n) S
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>x\<in>S. \<forall>y\<in>S. x \<squnion>\<^bsub>f\<^esub> y \<in> S \<Longrightarrow> \<forall>x\<in>list n S. \<forall>y\<in>list n S. x [+f] y \<in> list n S; \<forall>x\<in>S. \<forall>y\<in>S. x \<squnion>\<^bsub>f\<^esub> y \<in> S\<rbrakk> \<Longrightarrow> \<forall>x\<in>list (Suc n) S. \<forall>y\<in>list (Suc n) S. x [+f] y \<in> list (Suc n) S
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n x y. \<lbrakk>\<forall>x\<in>S. \<forall>y\<in>S. x \<squnion>\<^bsub>f\<^esub> y \<in> S \<Longrightarrow> \<forall>x\<in>list n S. \<forall>y\<in>list n S. x [+f] y \<in> list n S; \<forall>x\<in>S. \<forall>y\<in>S. x \<squnion>\<^bsub>f\<^esub> y \<in> S; x \<in> list (Suc n) S; y \<in> list (Suc n) S\<rbrakk> \<Longrightarrow> x [+f] y \<in> list (Suc n) S
[PROOF STEP]
apply (simp add: in_list_Suc_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n x y. \<lbrakk>\<forall>x\<in>list n S. \<forall>y\<in>list n S. x [+f] y \<in> list n S; \<forall>x\<in>S. \<forall>y\<in>S. x \<squnion>\<^bsub>f\<^esub> y \<in> S; \<exists>y\<in>S. \<exists>ys\<in>list n S. x = y # ys; \<exists>ya\<in>S. \<exists>ys\<in>list n S. y = ya # ys\<rbrakk> \<Longrightarrow> \<exists>ya\<in>S. \<exists>ys\<in>list n S. x [+f] y = ya # ys
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n x y ya yb ys ysa. \<lbrakk>\<forall>x\<in>list n S. \<forall>y\<in>list n S. x [+f] y \<in> list n S; \<forall>x\<in>S. \<forall>y\<in>S. x \<squnion>\<^bsub>f\<^esub> y \<in> S; ya \<in> S; yb \<in> S; ys \<in> list n S; ysa \<in> list n S\<rbrakk> \<Longrightarrow> \<exists>y\<in>S. \<exists>ysb\<in>list n S. ya # ys [+f] (yb # ysa) = y # ysb
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Listn_sl_aux:
assumes "Semilat A r f" shows "semilat (Listn.sl n (A,r,f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. semilat (Listn.sl n (A, r, f))
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. semilat (Listn.sl n (A, r, f))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. semilat (Listn.sl n (A, r, f))
[PROOF STEP]
interpret Semilat A r f
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Semilat A r f
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. semilat (Listn.sl n (A, r, f))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. semilat (Listn.sl n (A, r, f))
[PROOF STEP]
apply (unfold Listn.sl_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. semilat (case (A, r, f) of (A, r, f) \<Rightarrow> (list n A, Listn.le r, map2 f))
[PROOF STEP]
apply (simp (no_asm) only: semilat_Def split_conv)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. order (Listn.le r) \<and> closed (list n A) (map2 f) \<and> (\<forall>x\<in>list n A. \<forall>y\<in>list n A. x [\<sqsubseteq>\<^bsub>r\<^esub>] x [+f] y) \<and> (\<forall>x\<in>list n A. \<forall>y\<in>list n A. y [\<sqsubseteq>\<^bsub>r\<^esub>] x [+f] y) \<and> (\<forall>x\<in>list n A. \<forall>y\<in>list n A. \<forall>z\<in>list n A. x [\<sqsubseteq>\<^bsub>r\<^esub>] z \<and> y [\<sqsubseteq>\<^bsub>r\<^esub>] z \<longrightarrow> x [+f] y [\<sqsubseteq>\<^bsub>r\<^esub>] z)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. order (Listn.le r)
 2. closed (list n A) (map2 f) \<and> (\<forall>x\<in>list n A. \<forall>y\<in>list n A. x [\<sqsubseteq>\<^bsub>r\<^esub>] x [+f] y) \<and> (\<forall>x\<in>list n A. \<forall>y\<in>list n A. y [\<sqsubseteq>\<^bsub>r\<^esub>] x [+f] y) \<and> (\<forall>x\<in>list n A. \<forall>y\<in>list n A. \<forall>z\<in>list n A. x [\<sqsubseteq>\<^bsub>r\<^esub>] z \<and> y [\<sqsubseteq>\<^bsub>r\<^esub>] z \<longrightarrow> x [+f] y [\<sqsubseteq>\<^bsub>r\<^esub>] z)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed (list n A) (map2 f) \<and> (\<forall>x\<in>list n A. \<forall>y\<in>list n A. x [\<sqsubseteq>\<^bsub>r\<^esub>] x [+f] y) \<and> (\<forall>x\<in>list n A. \<forall>y\<in>list n A. y [\<sqsubseteq>\<^bsub>r\<^esub>] x [+f] y) \<and> (\<forall>x\<in>list n A. \<forall>y\<in>list n A. \<forall>z\<in>list n A. x [\<sqsubseteq>\<^bsub>r\<^esub>] z \<and> y [\<sqsubseteq>\<^bsub>r\<^esub>] z \<longrightarrow> x [+f] y [\<sqsubseteq>\<^bsub>r\<^esub>] z)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. closed (list n A) (map2 f)
 2. (\<forall>x\<in>list n A. \<forall>y\<in>list n A. x [\<sqsubseteq>\<^bsub>r\<^esub>] x [+f] y) \<and> (\<forall>x\<in>list n A. \<forall>y\<in>list n A. y [\<sqsubseteq>\<^bsub>r\<^esub>] x [+f] y) \<and> (\<forall>x\<in>list n A. \<forall>y\<in>list n A. \<forall>z\<in>list n A. x [\<sqsubseteq>\<^bsub>r\<^esub>] z \<and> y [\<sqsubseteq>\<^bsub>r\<^esub>] z \<longrightarrow> x [+f] y [\<sqsubseteq>\<^bsub>r\<^esub>] z)
[PROOF STEP]
apply (simp only: closedI closed_listI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x\<in>list n A. \<forall>y\<in>list n A. x [\<sqsubseteq>\<^bsub>r\<^esub>] x [+f] y) \<and> (\<forall>x\<in>list n A. \<forall>y\<in>list n A. y [\<sqsubseteq>\<^bsub>r\<^esub>] x [+f] y) \<and> (\<forall>x\<in>list n A. \<forall>y\<in>list n A. \<forall>z\<in>list n A. x [\<sqsubseteq>\<^bsub>r\<^esub>] z \<and> y [\<sqsubseteq>\<^bsub>r\<^esub>] z \<longrightarrow> x [+f] y [\<sqsubseteq>\<^bsub>r\<^esub>] z)
[PROOF STEP]
apply (simp (no_asm) only: list_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x\<in>{xs. length xs = n \<and> set xs \<subseteq> A}. \<forall>y\<in>{xs. length xs = n \<and> set xs \<subseteq> A}. x [\<sqsubseteq>\<^bsub>r\<^esub>] x [+f] y) \<and> (\<forall>x\<in>{xs. length xs = n \<and> set xs \<subseteq> A}. \<forall>y\<in>{xs. length xs = n \<and> set xs \<subseteq> A}. y [\<sqsubseteq>\<^bsub>r\<^esub>] x [+f] y) \<and> (\<forall>x\<in>{xs. length xs = n \<and> set xs \<subseteq> A}. \<forall>y\<in>{xs. length xs = n \<and> set xs \<subseteq> A}. \<forall>z\<in>{xs. length xs = n \<and> set xs \<subseteq> A}. x [\<sqsubseteq>\<^bsub>r\<^esub>] z \<and> y [\<sqsubseteq>\<^bsub>r\<^esub>] z \<longrightarrow> x [+f] y [\<sqsubseteq>\<^bsub>r\<^esub>] z)
[PROOF STEP]
apply (simp (no_asm_simp) add: plus_list_ub1 plus_list_ub2 plus_list_lub)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
semilat (Listn.sl n (A, r, f))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Listn_sl: "semilat L \<Longrightarrow> semilat (Listn.sl n L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. semilat L \<Longrightarrow> semilat (Listn.sl n L)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. semilat L \<Longrightarrow> semilat (Listn.sl n L)
[PROOF STEP]
apply (cases L)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>semilat L; L = (a, b, c)\<rbrakk> \<Longrightarrow> semilat (Listn.sl n L)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>semilat (a, b, c); L = (a, b, c)\<rbrakk> \<Longrightarrow> semilat (Listn.sl n (a, b, c))
[PROOF STEP]
apply (drule Semilat.intro)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>L = (a, b, c); Semilat a b c\<rbrakk> \<Longrightarrow> semilat (Listn.sl n (a, b, c))
[PROOF STEP]
by (simp add: Listn_sl_aux split_tupled_all)


[STATEMENT]
lemma coalesce_in_err_list [rule_format]:
  "\<forall>xes. xes \<in> list n (err A) \<longrightarrow> coalesce xes \<in> err(list n A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>xes. xes \<in> list n (err A) \<longrightarrow> coalesce xes \<in> err (list n A)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>xes. xes \<in> list n (err A) \<longrightarrow> coalesce xes \<in> err (list n A)
[PROOF STEP]
apply (induct n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>xes. xes \<in> list 0 (err A) \<longrightarrow> coalesce xes \<in> err (list 0 A)
 2. \<And>n. \<forall>xes. xes \<in> list n (err A) \<longrightarrow> coalesce xes \<in> err (list n A) \<Longrightarrow> \<forall>xes. xes \<in> list (Suc n) (err A) \<longrightarrow> coalesce xes \<in> err (list (Suc n) A)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<forall>xes. xes \<in> list n (err A) \<longrightarrow> coalesce xes \<in> err (list n A) \<Longrightarrow> \<forall>xes. xes \<in> list (Suc n) (err A) \<longrightarrow> coalesce xes \<in> err (list (Suc n) A)
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n xes. \<lbrakk>\<forall>xes. xes \<in> list n (err A) \<longrightarrow> coalesce xes \<in> err (list n A); xes \<in> list (Suc n) (err A)\<rbrakk> \<Longrightarrow> coalesce xes \<in> err (list (Suc n) A)
[PROOF STEP]
apply (simp add: in_list_Suc_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n xes. \<lbrakk>\<forall>xes. xes \<in> list n (err A) \<longrightarrow> coalesce xes \<in> err (list n A); \<exists>y\<in>err A. \<exists>ys\<in>list n (err A). xes = y # ys\<rbrakk> \<Longrightarrow> coalesce xes \<in> err (list (Suc n) A)
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n xes y ys. \<lbrakk>\<forall>xes. xes \<in> list n (err A) \<longrightarrow> coalesce xes \<in> err (list n A); y \<in> err A; ys \<in> list n (err A)\<rbrakk> \<Longrightarrow> coalesce (y # ys) \<in> err (list (Suc n) A)
[PROOF STEP]
apply (simp (no_asm) add: plussub_def Err.sup_def lift2_def split: err.split)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n y ys. \<lbrakk>\<forall>xes. xes \<in> list n (err A) \<longrightarrow> coalesce xes \<in> err (list n A); y \<in> err A; ys \<in> list n (err A)\<rbrakk> \<Longrightarrow> \<forall>x2 x2a. coalesce ys = OK x2a \<longrightarrow> y = OK x2 \<longrightarrow> x2 \<in> A \<and> x2a \<in> list n A
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma lem: "\<And>x xs. x \<squnion>\<^bsub>(#)\<^esub> xs = x#xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xs. x \<squnion>\<^bsub>(#)\<^esub> xs = x # xs
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xs. x \<squnion>\<^bsub>(#)\<^esub> xs = x # xs
[PROOF STEP]
by (simp add: plussub_def)


[STATEMENT]
lemma coalesce_eq_OK1_D [rule_format]:
  "semilat(err A, Err.le r, lift2 f) \<Longrightarrow>
  \<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>ys. ys \<in> list n A \<longrightarrow>
  (\<forall>zs. coalesce (xs [\<squnion>\<^bsub>f\<^esub>] ys) = OK zs \<longrightarrow> xs [\<sqsubseteq>\<^bsub>r\<^esub>] zs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. semilat (err A, Err.le r, lift2 f) \<Longrightarrow> \<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>ys. ys \<in> list n A \<longrightarrow> (\<forall>zs. coalesce (xs [+f] ys) = OK zs \<longrightarrow> xs [\<sqsubseteq>\<^bsub>r\<^esub>] zs))
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. semilat (err A, Err.le r, lift2 f) \<Longrightarrow> \<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>ys. ys \<in> list n A \<longrightarrow> (\<forall>zs. coalesce (xs [+f] ys) = OK zs \<longrightarrow> xs [\<sqsubseteq>\<^bsub>r\<^esub>] zs))
[PROOF STEP]
apply (induct n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. semilat (err A, Err.le r, lift2 f) \<Longrightarrow> \<forall>xs. xs \<in> list 0 A \<longrightarrow> (\<forall>ys. ys \<in> list 0 A \<longrightarrow> (\<forall>zs. coalesce (xs [+f] ys) = OK zs \<longrightarrow> xs [\<sqsubseteq>\<^bsub>r\<^esub>] zs))
 2. \<And>n. \<lbrakk>semilat (err A, Err.le r, lift2 f) \<Longrightarrow> \<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>ys. ys \<in> list n A \<longrightarrow> (\<forall>zs. coalesce (xs [+f] ys) = OK zs \<longrightarrow> xs [\<sqsubseteq>\<^bsub>r\<^esub>] zs)); semilat (err A, Err.le r, lift2 f)\<rbrakk> \<Longrightarrow> \<forall>xs. xs \<in> list (Suc n) A \<longrightarrow> (\<forall>ys. ys \<in> list (Suc n) A \<longrightarrow> (\<forall>zs. coalesce (xs [+f] ys) = OK zs \<longrightarrow> xs [\<sqsubseteq>\<^bsub>r\<^esub>] zs))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>semilat (err A, Err.le r, lift2 f) \<Longrightarrow> \<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>ys. ys \<in> list n A \<longrightarrow> (\<forall>zs. coalesce (xs [+f] ys) = OK zs \<longrightarrow> xs [\<sqsubseteq>\<^bsub>r\<^esub>] zs)); semilat (err A, Err.le r, lift2 f)\<rbrakk> \<Longrightarrow> \<forall>xs. xs \<in> list (Suc n) A \<longrightarrow> (\<forall>ys. ys \<in> list (Suc n) A \<longrightarrow> (\<forall>zs. coalesce (xs [+f] ys) = OK zs \<longrightarrow> xs [\<sqsubseteq>\<^bsub>r\<^esub>] zs))
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n xs ys zs. \<lbrakk>semilat (err A, Err.le r, lift2 f) \<Longrightarrow> \<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>ys. ys \<in> list n A \<longrightarrow> (\<forall>zs. coalesce (xs [+f] ys) = OK zs \<longrightarrow> xs [\<sqsubseteq>\<^bsub>r\<^esub>] zs)); semilat (err A, Err.le r, lift2 f); xs \<in> list (Suc n) A; ys \<in> list (Suc n) A; coalesce (xs [+f] ys) = OK zs\<rbrakk> \<Longrightarrow> xs [\<sqsubseteq>\<^bsub>r\<^esub>] zs
[PROOF STEP]
apply (simp add: in_list_Suc_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n xs ys zs. \<lbrakk>\<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>ys. ys \<in> list n A \<longrightarrow> (\<forall>zs. coalesce (xs [+f] ys) = OK zs \<longrightarrow> xs [\<sqsubseteq>\<^bsub>r\<^esub>] zs)); semilat (err A, Err.le r, lift2 f); \<exists>y\<in>A. \<exists>ys\<in>list n A. xs = y # ys; \<exists>y\<in>A. \<exists>ysa\<in>list n A. ys = y # ysa; coalesce (xs [+f] ys) = OK zs\<rbrakk> \<Longrightarrow> xs [\<sqsubseteq>\<^bsub>r\<^esub>] zs
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n xs ys zs y ya ysa ysb. \<lbrakk>\<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>ys. ys \<in> list n A \<longrightarrow> (\<forall>zs. coalesce (xs [+f] ys) = OK zs \<longrightarrow> xs [\<sqsubseteq>\<^bsub>r\<^esub>] zs)); semilat (err A, Err.le r, lift2 f); coalesce (y # ysa [+f] (ya # ysb)) = OK zs; y \<in> A; ya \<in> A; ysa \<in> list n A; ysb \<in> list n A\<rbrakk> \<Longrightarrow> y # ysa [\<sqsubseteq>\<^bsub>r\<^esub>] zs
[PROOF STEP]
apply (simp split: err.split_asm add: lem Err.sup_def lift2_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n zs y ya ysa ysb x2 x2a. \<lbrakk>y \<in> A; ya \<in> A; ysa \<in> list n A; ysb \<in> list n A; \<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>ys. ys \<in> list n A \<longrightarrow> (\<forall>zs. coalesce (xs [+f] ys) = OK zs \<longrightarrow> xs [\<sqsubseteq>\<^bsub>r\<^esub>] zs)); semilat (err A, Err.le r, lift2 f); y \<squnion>\<^bsub>f\<^esub> ya = OK x2; coalesce (ysa [+f] ysb) = OK x2a; x2 # x2a = zs\<rbrakk> \<Longrightarrow> y # ysa [\<sqsubseteq>\<^bsub>r\<^esub>] zs
[PROOF STEP]
apply (force simp add: semilat_le_err_OK1)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma coalesce_eq_OK2_D [rule_format]:
  "semilat(err A, Err.le r, lift2 f) \<Longrightarrow>
  \<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>ys. ys \<in> list n A \<longrightarrow>
  (\<forall>zs. coalesce (xs [\<squnion>\<^bsub>f\<^esub>] ys) = OK zs \<longrightarrow> ys [\<sqsubseteq>\<^bsub>r\<^esub>] zs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. semilat (err A, Err.le r, lift2 f) \<Longrightarrow> \<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>ys. ys \<in> list n A \<longrightarrow> (\<forall>zs. coalesce (xs [+f] ys) = OK zs \<longrightarrow> ys [\<sqsubseteq>\<^bsub>r\<^esub>] zs))
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. semilat (err A, Err.le r, lift2 f) \<Longrightarrow> \<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>ys. ys \<in> list n A \<longrightarrow> (\<forall>zs. coalesce (xs [+f] ys) = OK zs \<longrightarrow> ys [\<sqsubseteq>\<^bsub>r\<^esub>] zs))
[PROOF STEP]
apply (induct n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. semilat (err A, Err.le r, lift2 f) \<Longrightarrow> \<forall>xs. xs \<in> list 0 A \<longrightarrow> (\<forall>ys. ys \<in> list 0 A \<longrightarrow> (\<forall>zs. coalesce (xs [+f] ys) = OK zs \<longrightarrow> ys [\<sqsubseteq>\<^bsub>r\<^esub>] zs))
 2. \<And>n. \<lbrakk>semilat (err A, Err.le r, lift2 f) \<Longrightarrow> \<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>ys. ys \<in> list n A \<longrightarrow> (\<forall>zs. coalesce (xs [+f] ys) = OK zs \<longrightarrow> ys [\<sqsubseteq>\<^bsub>r\<^esub>] zs)); semilat (err A, Err.le r, lift2 f)\<rbrakk> \<Longrightarrow> \<forall>xs. xs \<in> list (Suc n) A \<longrightarrow> (\<forall>ys. ys \<in> list (Suc n) A \<longrightarrow> (\<forall>zs. coalesce (xs [+f] ys) = OK zs \<longrightarrow> ys [\<sqsubseteq>\<^bsub>r\<^esub>] zs))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>semilat (err A, Err.le r, lift2 f) \<Longrightarrow> \<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>ys. ys \<in> list n A \<longrightarrow> (\<forall>zs. coalesce (xs [+f] ys) = OK zs \<longrightarrow> ys [\<sqsubseteq>\<^bsub>r\<^esub>] zs)); semilat (err A, Err.le r, lift2 f)\<rbrakk> \<Longrightarrow> \<forall>xs. xs \<in> list (Suc n) A \<longrightarrow> (\<forall>ys. ys \<in> list (Suc n) A \<longrightarrow> (\<forall>zs. coalesce (xs [+f] ys) = OK zs \<longrightarrow> ys [\<sqsubseteq>\<^bsub>r\<^esub>] zs))
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n xs ys zs. \<lbrakk>semilat (err A, Err.le r, lift2 f) \<Longrightarrow> \<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>ys. ys \<in> list n A \<longrightarrow> (\<forall>zs. coalesce (xs [+f] ys) = OK zs \<longrightarrow> ys [\<sqsubseteq>\<^bsub>r\<^esub>] zs)); semilat (err A, Err.le r, lift2 f); xs \<in> list (Suc n) A; ys \<in> list (Suc n) A; coalesce (xs [+f] ys) = OK zs\<rbrakk> \<Longrightarrow> ys [\<sqsubseteq>\<^bsub>r\<^esub>] zs
[PROOF STEP]
apply (simp add: in_list_Suc_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n xs ys zs. \<lbrakk>\<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>ys. ys \<in> list n A \<longrightarrow> (\<forall>zs. coalesce (xs [+f] ys) = OK zs \<longrightarrow> ys [\<sqsubseteq>\<^bsub>r\<^esub>] zs)); semilat (err A, Err.le r, lift2 f); \<exists>y\<in>A. \<exists>ys\<in>list n A. xs = y # ys; \<exists>y\<in>A. \<exists>ysa\<in>list n A. ys = y # ysa; coalesce (xs [+f] ys) = OK zs\<rbrakk> \<Longrightarrow> ys [\<sqsubseteq>\<^bsub>r\<^esub>] zs
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n xs ys zs y ya ysa ysb. \<lbrakk>\<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>ys. ys \<in> list n A \<longrightarrow> (\<forall>zs. coalesce (xs [+f] ys) = OK zs \<longrightarrow> ys [\<sqsubseteq>\<^bsub>r\<^esub>] zs)); semilat (err A, Err.le r, lift2 f); coalesce (y # ysa [+f] (ya # ysb)) = OK zs; y \<in> A; ya \<in> A; ysa \<in> list n A; ysb \<in> list n A\<rbrakk> \<Longrightarrow> ya # ysb [\<sqsubseteq>\<^bsub>r\<^esub>] zs
[PROOF STEP]
apply (simp split: err.split_asm add: lem Err.sup_def lift2_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n zs y ya ysa ysb x2 x2a. \<lbrakk>y \<in> A; ya \<in> A; ysa \<in> list n A; ysb \<in> list n A; \<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>ys. ys \<in> list n A \<longrightarrow> (\<forall>zs. coalesce (xs [+f] ys) = OK zs \<longrightarrow> ys [\<sqsubseteq>\<^bsub>r\<^esub>] zs)); semilat (err A, Err.le r, lift2 f); y \<squnion>\<^bsub>f\<^esub> ya = OK x2; coalesce (ysa [+f] ysb) = OK x2a; x2 # x2a = zs\<rbrakk> \<Longrightarrow> ya # ysb [\<sqsubseteq>\<^bsub>r\<^esub>] zs
[PROOF STEP]
apply (force simp add: semilat_le_err_OK2)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma lift2_le_ub:
  "\<lbrakk> semilat(err A, Err.le r, lift2 f); x\<in>A; y\<in>A; x \<squnion>\<^sub>f y = OK z;
      u\<in>A; x \<sqsubseteq>\<^sub>r u; y \<sqsubseteq>\<^sub>r u \<rbrakk> \<Longrightarrow> z \<sqsubseteq>\<^sub>r u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>semilat (err A, Err.le r, lift2 f); x \<in> A; y \<in> A; x \<squnion>\<^bsub>f\<^esub> y = OK z; u \<in> A; x \<sqsubseteq>\<^bsub>r\<^esub> u; y \<sqsubseteq>\<^bsub>r\<^esub> u\<rbrakk> \<Longrightarrow> z \<sqsubseteq>\<^bsub>r\<^esub> u
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>semilat (err A, Err.le r, lift2 f); x \<in> A; y \<in> A; x \<squnion>\<^bsub>f\<^esub> y = OK z; u \<in> A; x \<sqsubseteq>\<^bsub>r\<^esub> u; y \<sqsubseteq>\<^bsub>r\<^esub> u\<rbrakk> \<Longrightarrow> z \<sqsubseteq>\<^bsub>r\<^esub> u
[PROOF STEP]
apply (unfold semilat_Def plussub_def err_def')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>order (Err.le r) \<and> closed (insert Err {x. \<exists>y\<in>A. x = OK y}) (lift2 f) \<and> (\<forall>x\<in>insert Err {x. \<exists>y\<in>A. x = OK y}. \<forall>y\<in>insert Err {x. \<exists>y\<in>A. x = OK y}. x \<sqsubseteq>\<^bsub>Err.le r\<^esub> lift2 f x y) \<and> (\<forall>x\<in>insert Err {x. \<exists>y\<in>A. x = OK y}. \<forall>y\<in>insert Err {x. \<exists>y\<in>A. x = OK y}. y \<sqsubseteq>\<^bsub>Err.le r\<^esub> lift2 f x y) \<and> (\<forall>x\<in>insert Err {x. \<exists>y\<in>A. x = OK y}. \<forall>y\<in>insert Err {x. \<exists>y\<in>A. x = OK y}. \<forall>z\<in>insert Err {x. \<exists>y\<in>A. x = OK y}. x \<sqsubseteq>\<^bsub>Err.le r\<^esub> z \<and> y \<sqsubseteq>\<^bsub>Err.le r\<^esub> z \<longrightarrow> lift2 f x y \<sqsubseteq>\<^bsub>Err.le r\<^esub> z); x \<in> A; y \<in> A; f x y = OK z; u \<in> A; x \<sqsubseteq>\<^bsub>r\<^esub> u; y \<sqsubseteq>\<^bsub>r\<^esub> u\<rbrakk> \<Longrightarrow> z \<sqsubseteq>\<^bsub>r\<^esub> u
[PROOF STEP]
apply (simp add: lift2_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>order r \<and> closed (insert Err {x. \<exists>y\<in>A. x = OK y}) (lift2 f) \<and> (\<forall>y\<in>A. \<forall>ya\<in>A. OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> f y ya) \<and> (\<forall>y\<in>A. \<forall>ya\<in>A. OK ya \<sqsubseteq>\<^bsub>Err.le r\<^esub> f y ya) \<and> (\<forall>y\<in>A. \<forall>ya\<in>A. \<forall>yb\<in>A. y \<sqsubseteq>\<^bsub>r\<^esub> yb \<and> ya \<sqsubseteq>\<^bsub>r\<^esub> yb \<longrightarrow> (\<exists>yc. f y ya = OK yc \<and> yc \<sqsubseteq>\<^bsub>r\<^esub> yb)); x \<in> A; y \<in> A; f x y = OK z; u \<in> A; x \<sqsubseteq>\<^bsub>r\<^esub> u; y \<sqsubseteq>\<^bsub>r\<^esub> u\<rbrakk> \<Longrightarrow> z \<sqsubseteq>\<^bsub>r\<^esub> u
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> A; y \<in> A; f x y = OK z; u \<in> A; x \<sqsubseteq>\<^bsub>r\<^esub> u; y \<sqsubseteq>\<^bsub>r\<^esub> u; order r; closed (insert Err {x. \<exists>y\<in>A. x = OK y}) (lift2 f); \<forall>y\<in>A. \<forall>ya\<in>A. OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> f y ya; \<forall>y\<in>A. \<forall>ya\<in>A. OK ya \<sqsubseteq>\<^bsub>Err.le r\<^esub> f y ya; \<forall>y\<in>A. \<forall>ya\<in>A. \<forall>yb\<in>A. y \<sqsubseteq>\<^bsub>r\<^esub> yb \<and> ya \<sqsubseteq>\<^bsub>r\<^esub> yb \<longrightarrow> (\<exists>yc. f y ya = OK yc \<and> yc \<sqsubseteq>\<^bsub>r\<^esub> yb)\<rbrakk> \<Longrightarrow> z \<sqsubseteq>\<^bsub>r\<^esub> u
[PROOF STEP]
apply (rotate_tac -3)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>y\<in>A. \<forall>ya\<in>A. OK y \<sqsubseteq>\<^bsub>Err.le r\<^esub> f y ya; \<forall>y\<in>A. \<forall>ya\<in>A. OK ya \<sqsubseteq>\<^bsub>Err.le r\<^esub> f y ya; \<forall>y\<in>A. \<forall>ya\<in>A. \<forall>yb\<in>A. y \<sqsubseteq>\<^bsub>r\<^esub> yb \<and> ya \<sqsubseteq>\<^bsub>r\<^esub> yb \<longrightarrow> (\<exists>yc. f y ya = OK yc \<and> yc \<sqsubseteq>\<^bsub>r\<^esub> yb); x \<in> A; y \<in> A; f x y = OK z; u \<in> A; x \<sqsubseteq>\<^bsub>r\<^esub> u; y \<sqsubseteq>\<^bsub>r\<^esub> u; order r; closed (insert Err {x. \<exists>y\<in>A. x = OK y}) (lift2 f)\<rbrakk> \<Longrightarrow> z \<sqsubseteq>\<^bsub>r\<^esub> u
[PROOF STEP]
apply (erule thin_rl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>y\<in>A. \<forall>ya\<in>A. OK ya \<sqsubseteq>\<^bsub>Err.le r\<^esub> f y ya; \<forall>y\<in>A. \<forall>ya\<in>A. \<forall>yb\<in>A. y \<sqsubseteq>\<^bsub>r\<^esub> yb \<and> ya \<sqsubseteq>\<^bsub>r\<^esub> yb \<longrightarrow> (\<exists>yc. f y ya = OK yc \<and> yc \<sqsubseteq>\<^bsub>r\<^esub> yb); x \<in> A; y \<in> A; f x y = OK z; u \<in> A; x \<sqsubseteq>\<^bsub>r\<^esub> u; y \<sqsubseteq>\<^bsub>r\<^esub> u; order r; closed (insert Err {x. \<exists>y\<in>A. x = OK y}) (lift2 f)\<rbrakk> \<Longrightarrow> z \<sqsubseteq>\<^bsub>r\<^esub> u
[PROOF STEP]
apply (erule thin_rl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>y\<in>A. \<forall>ya\<in>A. \<forall>yb\<in>A. y \<sqsubseteq>\<^bsub>r\<^esub> yb \<and> ya \<sqsubseteq>\<^bsub>r\<^esub> yb \<longrightarrow> (\<exists>yc. f y ya = OK yc \<and> yc \<sqsubseteq>\<^bsub>r\<^esub> yb); x \<in> A; y \<in> A; f x y = OK z; u \<in> A; x \<sqsubseteq>\<^bsub>r\<^esub> u; y \<sqsubseteq>\<^bsub>r\<^esub> u; order r; closed (insert Err {x. \<exists>y\<in>A. x = OK y}) (lift2 f)\<rbrakk> \<Longrightarrow> z \<sqsubseteq>\<^bsub>r\<^esub> u
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma coalesce_eq_OK_ub_D [rule_format]:
  "semilat(err A, Err.le r, lift2 f) \<Longrightarrow>
  \<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>ys. ys \<in> list n A \<longrightarrow>
  (\<forall>zs us. coalesce (xs [\<squnion>\<^bsub>f\<^esub>] ys) = OK zs \<and> xs [\<sqsubseteq>\<^bsub>r\<^esub>] us \<and> ys [\<sqsubseteq>\<^bsub>r\<^esub>] us
           \<and> us \<in> list n A \<longrightarrow> zs [\<sqsubseteq>\<^bsub>r\<^esub>] us))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. semilat (err A, Err.le r, lift2 f) \<Longrightarrow> \<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>ys. ys \<in> list n A \<longrightarrow> (\<forall>zs us. coalesce (xs [+f] ys) = OK zs \<and> xs [\<sqsubseteq>\<^bsub>r\<^esub>] us \<and> ys [\<sqsubseteq>\<^bsub>r\<^esub>] us \<and> us \<in> list n A \<longrightarrow> zs [\<sqsubseteq>\<^bsub>r\<^esub>] us))
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. semilat (err A, Err.le r, lift2 f) \<Longrightarrow> \<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>ys. ys \<in> list n A \<longrightarrow> (\<forall>zs us. coalesce (xs [+f] ys) = OK zs \<and> xs [\<sqsubseteq>\<^bsub>r\<^esub>] us \<and> ys [\<sqsubseteq>\<^bsub>r\<^esub>] us \<and> us \<in> list n A \<longrightarrow> zs [\<sqsubseteq>\<^bsub>r\<^esub>] us))
[PROOF STEP]
apply (induct n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. semilat (err A, Err.le r, lift2 f) \<Longrightarrow> \<forall>xs. xs \<in> list 0 A \<longrightarrow> (\<forall>ys. ys \<in> list 0 A \<longrightarrow> (\<forall>zs us. coalesce (xs [+f] ys) = OK zs \<and> xs [\<sqsubseteq>\<^bsub>r\<^esub>] us \<and> ys [\<sqsubseteq>\<^bsub>r\<^esub>] us \<and> us \<in> list 0 A \<longrightarrow> zs [\<sqsubseteq>\<^bsub>r\<^esub>] us))
 2. \<And>n. \<lbrakk>semilat (err A, Err.le r, lift2 f) \<Longrightarrow> \<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>ys. ys \<in> list n A \<longrightarrow> (\<forall>zs us. coalesce (xs [+f] ys) = OK zs \<and> xs [\<sqsubseteq>\<^bsub>r\<^esub>] us \<and> ys [\<sqsubseteq>\<^bsub>r\<^esub>] us \<and> us \<in> list n A \<longrightarrow> zs [\<sqsubseteq>\<^bsub>r\<^esub>] us)); semilat (err A, Err.le r, lift2 f)\<rbrakk> \<Longrightarrow> \<forall>xs. xs \<in> list (Suc n) A \<longrightarrow> (\<forall>ys. ys \<in> list (Suc n) A \<longrightarrow> (\<forall>zs us. coalesce (xs [+f] ys) = OK zs \<and> xs [\<sqsubseteq>\<^bsub>r\<^esub>] us \<and> ys [\<sqsubseteq>\<^bsub>r\<^esub>] us \<and> us \<in> list (Suc n) A \<longrightarrow> zs [\<sqsubseteq>\<^bsub>r\<^esub>] us))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>semilat (err A, Err.le r, lift2 f) \<Longrightarrow> \<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>ys. ys \<in> list n A \<longrightarrow> (\<forall>zs us. coalesce (xs [+f] ys) = OK zs \<and> xs [\<sqsubseteq>\<^bsub>r\<^esub>] us \<and> ys [\<sqsubseteq>\<^bsub>r\<^esub>] us \<and> us \<in> list n A \<longrightarrow> zs [\<sqsubseteq>\<^bsub>r\<^esub>] us)); semilat (err A, Err.le r, lift2 f)\<rbrakk> \<Longrightarrow> \<forall>xs. xs \<in> list (Suc n) A \<longrightarrow> (\<forall>ys. ys \<in> list (Suc n) A \<longrightarrow> (\<forall>zs us. coalesce (xs [+f] ys) = OK zs \<and> xs [\<sqsubseteq>\<^bsub>r\<^esub>] us \<and> ys [\<sqsubseteq>\<^bsub>r\<^esub>] us \<and> us \<in> list (Suc n) A \<longrightarrow> zs [\<sqsubseteq>\<^bsub>r\<^esub>] us))
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n xs ys zs us. \<lbrakk>semilat (err A, Err.le r, lift2 f) \<Longrightarrow> \<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>ys. ys \<in> list n A \<longrightarrow> (\<forall>zs us. coalesce (xs [+f] ys) = OK zs \<and> xs [\<sqsubseteq>\<^bsub>r\<^esub>] us \<and> ys [\<sqsubseteq>\<^bsub>r\<^esub>] us \<and> us \<in> list n A \<longrightarrow> zs [\<sqsubseteq>\<^bsub>r\<^esub>] us)); semilat (err A, Err.le r, lift2 f); xs \<in> list (Suc n) A; ys \<in> list (Suc n) A; coalesce (xs [+f] ys) = OK zs; xs [\<sqsubseteq>\<^bsub>r\<^esub>] us; ys [\<sqsubseteq>\<^bsub>r\<^esub>] us; us \<in> list (Suc n) A\<rbrakk> \<Longrightarrow> zs [\<sqsubseteq>\<^bsub>r\<^esub>] us
[PROOF STEP]
apply (simp add: in_list_Suc_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n xs ys zs us. \<lbrakk>\<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>ys. ys \<in> list n A \<longrightarrow> (\<forall>zs us. coalesce (xs [+f] ys) = OK zs \<and> xs [\<sqsubseteq>\<^bsub>r\<^esub>] us \<and> ys [\<sqsubseteq>\<^bsub>r\<^esub>] us \<and> us \<in> list n A \<longrightarrow> zs [\<sqsubseteq>\<^bsub>r\<^esub>] us)); semilat (err A, Err.le r, lift2 f); \<exists>y\<in>A. \<exists>ys\<in>list n A. xs = y # ys; \<exists>y\<in>A. \<exists>ysa\<in>list n A. ys = y # ysa; coalesce (xs [+f] ys) = OK zs; xs [\<sqsubseteq>\<^bsub>r\<^esub>] us; ys [\<sqsubseteq>\<^bsub>r\<^esub>] us; \<exists>y\<in>A. \<exists>ys\<in>list n A. us = y # ys\<rbrakk> \<Longrightarrow> zs [\<sqsubseteq>\<^bsub>r\<^esub>] us
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n xs ys zs us y ya yb ysa ysb ysc. \<lbrakk>\<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>ys. ys \<in> list n A \<longrightarrow> (\<forall>zs us. coalesce (xs [+f] ys) = OK zs \<and> xs [\<sqsubseteq>\<^bsub>r\<^esub>] us \<and> ys [\<sqsubseteq>\<^bsub>r\<^esub>] us \<and> us \<in> list n A \<longrightarrow> zs [\<sqsubseteq>\<^bsub>r\<^esub>] us)); semilat (err A, Err.le r, lift2 f); coalesce (y # ysa [+f] (ya # ysb)) = OK zs; y \<in> A; ya \<in> A; yb \<in> A; ysa \<in> list n A; ysb \<in> list n A; ysc \<in> list n A; y \<sqsubseteq>\<^bsub>r\<^esub> yb; ysa [\<sqsubseteq>\<^bsub>r\<^esub>] ysc; ya \<sqsubseteq>\<^bsub>r\<^esub> yb; ysb [\<sqsubseteq>\<^bsub>r\<^esub>] ysc\<rbrakk> \<Longrightarrow> zs [\<sqsubseteq>\<^bsub>r\<^esub>] yb # ysc
[PROOF STEP]
apply (simp (no_asm_use) split: err.split_asm add: lem Err.sup_def lift2_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n zs y ya yb ysa ysb ysc x2 x2a. \<lbrakk>y \<in> A; ya \<in> A; yb \<in> A; ysa \<in> list n A; ysb \<in> list n A; ysc \<in> list n A; y \<sqsubseteq>\<^bsub>r\<^esub> yb; ysa [\<sqsubseteq>\<^bsub>r\<^esub>] ysc; ya \<sqsubseteq>\<^bsub>r\<^esub> yb; ysb [\<sqsubseteq>\<^bsub>r\<^esub>] ysc; \<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>ys. ys \<in> list n A \<longrightarrow> (\<forall>zs us. coalesce (xs [+f] ys) = OK zs \<and> xs [\<sqsubseteq>\<^bsub>r\<^esub>] us \<and> ys [\<sqsubseteq>\<^bsub>r\<^esub>] us \<and> us \<in> list n A \<longrightarrow> zs [\<sqsubseteq>\<^bsub>r\<^esub>] us)); semilat (err A, Err.le r, lift2 f); y \<squnion>\<^bsub>f\<^esub> ya = OK x2; coalesce (ysa [+f] ysb) = OK x2a; x2 # x2a = zs\<rbrakk> \<Longrightarrow> zs [\<sqsubseteq>\<^bsub>r\<^esub>] yb # ysc
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n zs y ya yb ysa ysb ysc x2 x2a. \<lbrakk>y \<in> A; ya \<in> A; yb \<in> A; ysa \<in> list n A; ysb \<in> list n A; ysc \<in> list n A; y \<sqsubseteq>\<^bsub>r\<^esub> yb; ysa [\<sqsubseteq>\<^bsub>r\<^esub>] ysc; ya \<sqsubseteq>\<^bsub>r\<^esub> yb; ysb [\<sqsubseteq>\<^bsub>r\<^esub>] ysc; \<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>ys. ys \<in> list n A \<longrightarrow> (\<forall>zs us. coalesce (xs [+f] ys) = OK zs \<and> xs [\<sqsubseteq>\<^bsub>r\<^esub>] us \<and> ys [\<sqsubseteq>\<^bsub>r\<^esub>] us \<and> us \<in> list n A \<longrightarrow> zs [\<sqsubseteq>\<^bsub>r\<^esub>] us)); semilat (err A, Err.le r, lift2 f); y \<squnion>\<^bsub>f\<^esub> ya = OK x2; coalesce (ysa [+f] ysb) = OK x2a\<rbrakk> \<Longrightarrow> x2 \<sqsubseteq>\<^bsub>r\<^esub> yb \<and> x2a [\<sqsubseteq>\<^bsub>r\<^esub>] ysc
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n zs y ya yb ysa ysb ysc x2 x2a. \<lbrakk>y \<in> A; ya \<in> A; yb \<in> A; ysa \<in> list n A; ysb \<in> list n A; ysc \<in> list n A; y \<sqsubseteq>\<^bsub>r\<^esub> yb; ysa [\<sqsubseteq>\<^bsub>r\<^esub>] ysc; ya \<sqsubseteq>\<^bsub>r\<^esub> yb; ysb [\<sqsubseteq>\<^bsub>r\<^esub>] ysc; \<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>ys. ys \<in> list n A \<longrightarrow> (\<forall>zs us. coalesce (xs [+f] ys) = OK zs \<and> xs [\<sqsubseteq>\<^bsub>r\<^esub>] us \<and> ys [\<sqsubseteq>\<^bsub>r\<^esub>] us \<and> us \<in> list n A \<longrightarrow> zs [\<sqsubseteq>\<^bsub>r\<^esub>] us)); semilat (err A, Err.le r, lift2 f); y \<squnion>\<^bsub>f\<^esub> ya = OK x2; coalesce (ysa [+f] ysb) = OK x2a\<rbrakk> \<Longrightarrow> x2 \<sqsubseteq>\<^bsub>r\<^esub> yb
 2. \<And>n zs y ya yb ysa ysb ysc x2 x2a. \<lbrakk>y \<in> A; ya \<in> A; yb \<in> A; ysa \<in> list n A; ysb \<in> list n A; ysc \<in> list n A; y \<sqsubseteq>\<^bsub>r\<^esub> yb; ysa [\<sqsubseteq>\<^bsub>r\<^esub>] ysc; ya \<sqsubseteq>\<^bsub>r\<^esub> yb; ysb [\<sqsubseteq>\<^bsub>r\<^esub>] ysc; \<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>ys. ys \<in> list n A \<longrightarrow> (\<forall>zs us. coalesce (xs [+f] ys) = OK zs \<and> xs [\<sqsubseteq>\<^bsub>r\<^esub>] us \<and> ys [\<sqsubseteq>\<^bsub>r\<^esub>] us \<and> us \<in> list n A \<longrightarrow> zs [\<sqsubseteq>\<^bsub>r\<^esub>] us)); semilat (err A, Err.le r, lift2 f); y \<squnion>\<^bsub>f\<^esub> ya = OK x2; coalesce (ysa [+f] ysb) = OK x2a\<rbrakk> \<Longrightarrow> x2a [\<sqsubseteq>\<^bsub>r\<^esub>] ysc
[PROOF STEP]
apply (blast intro: lift2_le_ub)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n zs y ya yb ysa ysb ysc x2 x2a. \<lbrakk>y \<in> A; ya \<in> A; yb \<in> A; ysa \<in> list n A; ysb \<in> list n A; ysc \<in> list n A; y \<sqsubseteq>\<^bsub>r\<^esub> yb; ysa [\<sqsubseteq>\<^bsub>r\<^esub>] ysc; ya \<sqsubseteq>\<^bsub>r\<^esub> yb; ysb [\<sqsubseteq>\<^bsub>r\<^esub>] ysc; \<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>ys. ys \<in> list n A \<longrightarrow> (\<forall>zs us. coalesce (xs [+f] ys) = OK zs \<and> xs [\<sqsubseteq>\<^bsub>r\<^esub>] us \<and> ys [\<sqsubseteq>\<^bsub>r\<^esub>] us \<and> us \<in> list n A \<longrightarrow> zs [\<sqsubseteq>\<^bsub>r\<^esub>] us)); semilat (err A, Err.le r, lift2 f); y \<squnion>\<^bsub>f\<^esub> ya = OK x2; coalesce (ysa [+f] ysb) = OK x2a\<rbrakk> \<Longrightarrow> x2a [\<sqsubseteq>\<^bsub>r\<^esub>] ysc
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma lift2_eq_ErrD:
  "\<lbrakk> x \<squnion>\<^sub>f y = Err; semilat(err A, Err.le r, lift2 f); x\<in>A; y\<in>A \<rbrakk>
  \<Longrightarrow> \<not>(\<exists>u\<in>A. x \<sqsubseteq>\<^sub>r u \<and> y \<sqsubseteq>\<^sub>r u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<squnion>\<^bsub>f\<^esub> y = Err; semilat (err A, Err.le r, lift2 f); x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> \<not> (\<exists>u\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> u \<and> y \<sqsubseteq>\<^bsub>r\<^esub> u)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<squnion>\<^bsub>f\<^esub> y = Err; semilat (err A, Err.le r, lift2 f); x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> \<not> (\<exists>u\<in>A. x \<sqsubseteq>\<^bsub>r\<^esub> u \<and> y \<sqsubseteq>\<^bsub>r\<^esub> u)
[PROOF STEP]
by (simp add: OK_plus_OK_eq_Err_conv [THEN iffD1])