[STATEMENT]
lemma acc_le_listI1 [intro!]:
  " acc (subtype P) \<Longrightarrow> acc (Listn.le (subtype P))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. acc (subtype P) \<Longrightarrow> acc (Listn.le (subtype P))
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. acc (subtype P) \<Longrightarrow> acc (Listn.le (subtype P))
[PROOF STEP]
apply (unfold acc_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf {(y, x). x \<sqsubset>\<^bsub>subtype P\<^esub> y} \<Longrightarrow> wf {(y, x). x [\<sqsubset>\<^bsub>subtype P\<^esub>] y}
[PROOF STEP]
apply (subgoal_tac
 "wf(UN n. {(ys,xs). size xs = n \<and> size ys = n \<and> xs <_(Listn.le (subtype P)) ys})")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>wf {(y, x). x \<sqsubset>\<^bsub>subtype P\<^esub> y}; wf (\<Union>n. {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>subtype P\<^esub>] ys})\<rbrakk> \<Longrightarrow> wf {(y, x). x [\<sqsubset>\<^bsub>subtype P\<^esub>] y}
 2. wf {(y, x). x \<sqsubset>\<^bsub>subtype P\<^esub> y} \<Longrightarrow> wf (\<Union>n. {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>subtype P\<^esub>] ys})
[PROOF STEP]
apply (erule wf_subset)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. wf {(y, x). x \<sqsubset>\<^bsub>subtype P\<^esub> y} \<Longrightarrow> {(y, x). x [\<sqsubset>\<^bsub>subtype P\<^esub>] y} \<subseteq> (\<Union>n. {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>subtype P\<^esub>] ys})
 2. wf {(y, x). x \<sqsubset>\<^bsub>subtype P\<^esub> y} \<Longrightarrow> wf (\<Union>n. {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>subtype P\<^esub>] ys})
[PROOF STEP]
apply (blast intro: lesssub_lengthD)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf {(y, x). x \<sqsubset>\<^bsub>subtype P\<^esub> y} \<Longrightarrow> wf (\<Union>n. {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>subtype P\<^esub>] ys})
[PROOF STEP]
apply (rule wf_UN)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>wf {(y, x). x \<sqsubset>\<^bsub>subtype P\<^esub> y}; n \<in> UNIV\<rbrakk> \<Longrightarrow> wf {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>subtype P\<^esub>] ys}
 2. \<And>n j. \<lbrakk>wf {(y, x). x \<sqsubset>\<^bsub>subtype P\<^esub> y}; n \<in> UNIV; j \<in> UNIV; {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>subtype P\<^esub>] ys} \<noteq> {(ys, xs). length xs = j \<and> length ys = j \<and> xs [\<sqsubset>\<^bsub>subtype P\<^esub>] ys}\<rbrakk> \<Longrightarrow> Domain {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>subtype P\<^esub>] ys} \<inter> Range {(ys, xs). length xs = j \<and> length ys = j \<and> xs [\<sqsubset>\<^bsub>subtype P\<^esub>] ys} = {}
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n j. \<lbrakk>wf {(y, x). x \<sqsubset>\<^bsub>subtype P\<^esub> y}; n \<in> UNIV; j \<in> UNIV; {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>subtype P\<^esub>] ys} \<noteq> {(ys, xs). length xs = j \<and> length ys = j \<and> xs [\<sqsubset>\<^bsub>subtype P\<^esub>] ys}\<rbrakk> \<Longrightarrow> Domain {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>subtype P\<^esub>] ys} \<inter> Range {(ys, xs). length xs = j \<and> length ys = j \<and> xs [\<sqsubset>\<^bsub>subtype P\<^esub>] ys} = {}
 2. \<And>n. \<lbrakk>wf {(y, x). x \<sqsubset>\<^bsub>subtype P\<^esub> y}; n \<in> UNIV\<rbrakk> \<Longrightarrow> wf {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>subtype P\<^esub>] ys}
[PROOF STEP]
apply (rename_tac m n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m n. \<lbrakk>wf {(y, x). x \<sqsubset>\<^bsub>subtype P\<^esub> y}; m \<in> UNIV; n \<in> UNIV; {(ys, xs). length xs = m \<and> length ys = m \<and> xs [\<sqsubset>\<^bsub>subtype P\<^esub>] ys} \<noteq> {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>subtype P\<^esub>] ys}\<rbrakk> \<Longrightarrow> Domain {(ys, xs). length xs = m \<and> length ys = m \<and> xs [\<sqsubset>\<^bsub>subtype P\<^esub>] ys} \<inter> Range {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>subtype P\<^esub>] ys} = {}
 2. \<And>n. \<lbrakk>wf {(y, x). x \<sqsubset>\<^bsub>subtype P\<^esub> y}; n \<in> UNIV\<rbrakk> \<Longrightarrow> wf {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>subtype P\<^esub>] ys}
[PROOF STEP]
apply (case_tac "m=n")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>m n. \<lbrakk>wf {(y, x). x \<sqsubset>\<^bsub>subtype P\<^esub> y}; m \<in> UNIV; n \<in> UNIV; {(ys, xs). length xs = m \<and> length ys = m \<and> xs [\<sqsubset>\<^bsub>subtype P\<^esub>] ys} \<noteq> {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>subtype P\<^esub>] ys}; m = n\<rbrakk> \<Longrightarrow> Domain {(ys, xs). length xs = m \<and> length ys = m \<and> xs [\<sqsubset>\<^bsub>subtype P\<^esub>] ys} \<inter> Range {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>subtype P\<^esub>] ys} = {}
 2. \<And>m n. \<lbrakk>wf {(y, x). x \<sqsubset>\<^bsub>subtype P\<^esub> y}; m \<in> UNIV; n \<in> UNIV; {(ys, xs). length xs = m \<and> length ys = m \<and> xs [\<sqsubset>\<^bsub>subtype P\<^esub>] ys} \<noteq> {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>subtype P\<^esub>] ys}; m \<noteq> n\<rbrakk> \<Longrightarrow> Domain {(ys, xs). length xs = m \<and> length ys = m \<and> xs [\<sqsubset>\<^bsub>subtype P\<^esub>] ys} \<inter> Range {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>subtype P\<^esub>] ys} = {}
 3. \<And>n. \<lbrakk>wf {(y, x). x \<sqsubset>\<^bsub>subtype P\<^esub> y}; n \<in> UNIV\<rbrakk> \<Longrightarrow> wf {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>subtype P\<^esub>] ys}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m n. \<lbrakk>wf {(y, x). x \<sqsubset>\<^bsub>subtype P\<^esub> y}; m \<in> UNIV; n \<in> UNIV; {(ys, xs). length xs = m \<and> length ys = m \<and> xs [\<sqsubset>\<^bsub>subtype P\<^esub>] ys} \<noteq> {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>subtype P\<^esub>] ys}; m \<noteq> n\<rbrakk> \<Longrightarrow> Domain {(ys, xs). length xs = m \<and> length ys = m \<and> xs [\<sqsubset>\<^bsub>subtype P\<^esub>] ys} \<inter> Range {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>subtype P\<^esub>] ys} = {}
 2. \<And>n. \<lbrakk>wf {(y, x). x \<sqsubset>\<^bsub>subtype P\<^esub> y}; n \<in> UNIV\<rbrakk> \<Longrightarrow> wf {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>subtype P\<^esub>] ys}
[PROOF STEP]
apply (fast intro!: equals0I dest: not_sym)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>wf {(y, x). x \<sqsubset>\<^bsub>subtype P\<^esub> y}; n \<in> UNIV\<rbrakk> \<Longrightarrow> wf {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>subtype P\<^esub>] ys}
[PROOF STEP]
apply (rename_tac n)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>wf {(y, x). x \<sqsubset>\<^bsub>subtype P\<^esub> y}; n \<in> UNIV\<rbrakk> \<Longrightarrow> wf {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>subtype P\<^esub>] ys}
[PROOF STEP]
apply (induct_tac n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>wf {(y, x). x \<sqsubset>\<^bsub>subtype P\<^esub> y}; n \<in> UNIV\<rbrakk> \<Longrightarrow> wf {a. case a of (ys, xs) \<Rightarrow> length xs = 0 \<and> length ys = 0 \<and> xs [\<sqsubset>\<^bsub>subtype P\<^esub>] ys}
 2. \<And>n na. \<lbrakk>wf {(y, x). x \<sqsubset>\<^bsub>subtype P\<^esub> y}; n \<in> UNIV; wf {a. case a of (ys, xs) \<Rightarrow> length xs = na \<and> length ys = na \<and> xs [\<sqsubset>\<^bsub>subtype P\<^esub>] ys}\<rbrakk> \<Longrightarrow> wf {a. case a of (ys, xs) \<Rightarrow> length xs = Suc na \<and> length ys = Suc na \<and> xs [\<sqsubset>\<^bsub>subtype P\<^esub>] ys}
[PROOF STEP]
apply (simp add: lesssub_def cong: conj_cong)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n na. \<lbrakk>wf {(y, x). x \<sqsubset>\<^bsub>subtype P\<^esub> y}; n \<in> UNIV; wf {a. case a of (ys, xs) \<Rightarrow> length xs = na \<and> length ys = na \<and> xs [\<sqsubset>\<^bsub>subtype P\<^esub>] ys}\<rbrakk> \<Longrightarrow> wf {a. case a of (ys, xs) \<Rightarrow> length xs = Suc na \<and> length ys = Suc na \<and> xs [\<sqsubset>\<^bsub>subtype P\<^esub>] ys}
[PROOF STEP]
apply (rename_tac k)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n k. \<lbrakk>wf {(y, x). x \<sqsubset>\<^bsub>subtype P\<^esub> y}; n \<in> UNIV; wf {a. case a of (ys, xs) \<Rightarrow> length xs = k \<and> length ys = k \<and> xs [\<sqsubset>\<^bsub>subtype P\<^esub>] ys}\<rbrakk> \<Longrightarrow> wf {a. case a of (ys, xs) \<Rightarrow> length xs = Suc k \<and> length ys = Suc k \<and> xs [\<sqsubset>\<^bsub>subtype P\<^esub>] ys}
[PROOF STEP]
apply (simp add: wf_eq_minimal)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. z \<sqsubset>\<^bsub>subtype P\<^esub> y \<longrightarrow> y \<notin> Q); \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. length z = k \<and> length y = k \<and> z [\<sqsubset>\<^bsub>subtype P\<^esub>] y \<longrightarrow> y \<notin> Q)\<rbrakk> \<Longrightarrow> \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. length z = Suc k \<and> length y = Suc k \<and> z [\<sqsubset>\<^bsub>subtype P\<^esub>] y \<longrightarrow> y \<notin> Q)
[PROOF STEP]
apply (simp (no_asm) add: length_Suc_conv cong: conj_cong)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. z \<sqsubset>\<^bsub>subtype P\<^esub> y \<longrightarrow> y \<notin> Q); \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. length z = k \<and> length y = k \<and> z [\<sqsubset>\<^bsub>subtype P\<^esub>] y \<longrightarrow> y \<notin> Q)\<rbrakk> \<Longrightarrow> \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = k) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = k) \<and> z [\<sqsubset>\<^bsub>subtype P\<^esub>] y \<longrightarrow> y \<notin> Q)
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k Q x. \<lbrakk>\<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. z \<sqsubset>\<^bsub>subtype P\<^esub> y \<longrightarrow> y \<notin> Q); \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. length z = k \<and> length y = k \<and> z [\<sqsubset>\<^bsub>subtype P\<^esub>] y \<longrightarrow> y \<notin> Q); x \<in> Q\<rbrakk> \<Longrightarrow> \<exists>z\<in>Q. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = k) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = k) \<and> z [\<sqsubset>\<^bsub>subtype P\<^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>\<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. z \<sqsubset>\<^bsub>subtype P\<^esub> y \<longrightarrow> y \<notin> Q); \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. length z = k \<and> length y = k \<and> z [\<sqsubset>\<^bsub>subtype P\<^esub>] y \<longrightarrow> y \<notin> Q); m \<in> M\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = k) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = k) \<and> z [\<sqsubset>\<^bsub>subtype P\<^esub>] y \<longrightarrow> y \<notin> M
[PROOF STEP]
apply (case_tac "\<exists>x xs. size xs = k \<and> x#xs \<in> M")
[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 \<sqsubset>\<^bsub>subtype P\<^esub> y \<longrightarrow> y \<notin> Q); \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. length z = k \<and> length y = k \<and> z [\<sqsubset>\<^bsub>subtype P\<^esub>] y \<longrightarrow> y \<notin> Q); m \<in> M; \<exists>x xs. length xs = k \<and> x # xs \<in> M\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = k) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = k) \<and> z [\<sqsubset>\<^bsub>subtype P\<^esub>] y \<longrightarrow> y \<notin> M
 2. \<And>k M m. \<lbrakk>\<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. z \<sqsubset>\<^bsub>subtype P\<^esub> y \<longrightarrow> y \<notin> Q); \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. length z = k \<and> length y = k \<and> z [\<sqsubset>\<^bsub>subtype P\<^esub>] y \<longrightarrow> y \<notin> Q); m \<in> M; \<nexists>x xs. length xs = k \<and> x # xs \<in> M\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = k) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = k) \<and> z [\<sqsubset>\<^bsub>subtype P\<^esub>] y \<longrightarrow> y \<notin> M
[PROOF STEP]
prefer 2
[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 \<sqsubset>\<^bsub>subtype P\<^esub> y \<longrightarrow> y \<notin> Q); \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. length z = k \<and> length y = k \<and> z [\<sqsubset>\<^bsub>subtype P\<^esub>] y \<longrightarrow> y \<notin> Q); m \<in> M; \<nexists>x xs. length xs = k \<and> x # xs \<in> M\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = k) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = k) \<and> z [\<sqsubset>\<^bsub>subtype P\<^esub>] y \<longrightarrow> y \<notin> M
 2. \<And>k M m. \<lbrakk>\<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. z \<sqsubset>\<^bsub>subtype P\<^esub> y \<longrightarrow> y \<notin> Q); \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. length z = k \<and> length y = k \<and> z [\<sqsubset>\<^bsub>subtype P\<^esub>] y \<longrightarrow> y \<notin> Q); m \<in> M; \<exists>x xs. length xs = k \<and> x # xs \<in> M\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = k) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = k) \<and> z [\<sqsubset>\<^bsub>subtype P\<^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. length z = k \<and> length y = k \<and> z [\<sqsubset>\<^bsub>subtype P\<^esub>] y \<longrightarrow> y \<notin> Q); m \<in> M; \<nexists>x xs. length xs = k \<and> x # xs \<in> M\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = k) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = k) \<and> z [\<sqsubset>\<^bsub>subtype P\<^esub>] y \<longrightarrow> y \<notin> M
 2. \<And>k M m. \<lbrakk>\<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. z \<sqsubset>\<^bsub>subtype P\<^esub> y \<longrightarrow> y \<notin> Q); \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. length z = k \<and> length y = k \<and> z [\<sqsubset>\<^bsub>subtype P\<^esub>] y \<longrightarrow> y \<notin> Q); m \<in> M; \<exists>x xs. length xs = k \<and> x # xs \<in> M\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = k) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = k) \<and> z [\<sqsubset>\<^bsub>subtype P\<^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>m \<in> M; \<nexists>x xs. length xs = k \<and> x # xs \<in> M\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = k) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = k) \<and> z [\<sqsubset>\<^bsub>subtype P\<^esub>] y \<longrightarrow> y \<notin> M
 2. \<And>k M m. \<lbrakk>\<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. z \<sqsubset>\<^bsub>subtype P\<^esub> y \<longrightarrow> y \<notin> Q); \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. length z = k \<and> length y = k \<and> z [\<sqsubset>\<^bsub>subtype P\<^esub>] y \<longrightarrow> y \<notin> Q); m \<in> M; \<exists>x xs. length xs = k \<and> x # xs \<in> M\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = k) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = k) \<and> z [\<sqsubset>\<^bsub>subtype P\<^esub>] y \<longrightarrow> y \<notin> M
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k M m. \<lbrakk>\<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. z \<sqsubset>\<^bsub>subtype P\<^esub> y \<longrightarrow> y \<notin> Q); \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. length z = k \<and> length y = k \<and> z [\<sqsubset>\<^bsub>subtype P\<^esub>] y \<longrightarrow> y \<notin> Q); m \<in> M; \<exists>x xs. length xs = k \<and> x # xs \<in> M\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = k) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = k) \<and> z [\<sqsubset>\<^bsub>subtype P\<^esub>] y \<longrightarrow> y \<notin> M
[PROOF STEP]
apply (erule_tac x = "{a. \<exists>xs. size xs = k \<and> a#xs:M}" in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k M m. \<lbrakk>\<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. length z = k \<and> length y = k \<and> z [\<sqsubset>\<^bsub>subtype P\<^esub>] y \<longrightarrow> y \<notin> Q); m \<in> M; \<exists>x xs. length xs = k \<and> x # xs \<in> M; (\<exists>x. x \<in> {a. \<exists>xs. length xs = k \<and> a # xs \<in> M}) \<longrightarrow> (\<exists>z\<in>{a. \<exists>xs. length xs = k \<and> a # xs \<in> M}. \<forall>y. z \<sqsubset>\<^bsub>subtype P\<^esub> y \<longrightarrow> y \<notin> {a. \<exists>xs. length xs = k \<and> a # xs \<in> M})\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = k) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = k) \<and> z [\<sqsubset>\<^bsub>subtype P\<^esub>] y \<longrightarrow> y \<notin> M
[PROOF STEP]
apply (erule impE)
[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. length z = k \<and> length y = k \<and> z [\<sqsubset>\<^bsub>subtype P\<^esub>] y \<longrightarrow> y \<notin> Q); m \<in> M; \<exists>x xs. length xs = k \<and> x # xs \<in> M\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> {a. \<exists>xs. length xs = k \<and> a # xs \<in> M}
 2. \<And>k M m. \<lbrakk>\<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. length z = k \<and> length y = k \<and> z [\<sqsubset>\<^bsub>subtype P\<^esub>] y \<longrightarrow> y \<notin> Q); m \<in> M; \<exists>x xs. length xs = k \<and> x # xs \<in> M; \<exists>z\<in>{a. \<exists>xs. length xs = k \<and> a # xs \<in> M}. \<forall>y. z \<sqsubset>\<^bsub>subtype P\<^esub> y \<longrightarrow> y \<notin> {a. \<exists>xs. length xs = k \<and> a # xs \<in> M}\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = k) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = k) \<and> z [\<sqsubset>\<^bsub>subtype P\<^esub>] y \<longrightarrow> y \<notin> M
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k M m. \<lbrakk>\<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. length z = k \<and> length y = k \<and> z [\<sqsubset>\<^bsub>subtype P\<^esub>] y \<longrightarrow> y \<notin> Q); m \<in> M; \<exists>x xs. length xs = k \<and> x # xs \<in> M; \<exists>z\<in>{a. \<exists>xs. length xs = k \<and> a # xs \<in> M}. \<forall>y. z \<sqsubset>\<^bsub>subtype P\<^esub> y \<longrightarrow> y \<notin> {a. \<exists>xs. length xs = k \<and> a # xs \<in> M}\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = k) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = k) \<and> z [\<sqsubset>\<^bsub>subtype P\<^esub>] y \<longrightarrow> y \<notin> M
[PROOF STEP]
apply (thin_tac "\<exists>x xs. P x xs" for P)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k M m. \<lbrakk>\<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. length z = k \<and> length y = k \<and> z [\<sqsubset>\<^bsub>subtype P\<^esub>] y \<longrightarrow> y \<notin> Q); m \<in> M; \<exists>z\<in>{a. \<exists>xs. length xs = k \<and> a # xs \<in> M}. \<forall>y. z \<sqsubset>\<^bsub>subtype P\<^esub> y \<longrightarrow> y \<notin> {a. \<exists>xs. length xs = k \<and> a # xs \<in> M}\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = k) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = k) \<and> z [\<sqsubset>\<^bsub>subtype P\<^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>\<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. length z = length xs \<and> length y = length xs \<and> z [\<sqsubset>\<^bsub>subtype P\<^esub>] y \<longrightarrow> y \<notin> Q); m \<in> M; \<forall>y. z \<sqsubset>\<^bsub>subtype P\<^esub> y \<longrightarrow> y \<notin> {a. \<exists>xsa. length xsa = length xs \<and> a # xsa \<in> M}; z # xs \<in> M\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = length xs) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = length xs) \<and> z [\<sqsubset>\<^bsub>subtype P\<^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>\<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. length z = length xs \<and> length y = length xs \<and> z [\<sqsubset>\<^bsub>subtype P\<^esub>] y \<longrightarrow> y \<notin> Q); m \<in> M; \<forall>y. maxA \<sqsubset>\<^bsub>subtype P\<^esub> y \<longrightarrow> y \<notin> {a. \<exists>xsa. length xsa = length xs \<and> a # xsa \<in> M}; maxA # xs \<in> M\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = length xs) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = length xs) \<and> z [\<sqsubset>\<^bsub>subtype P\<^esub>] y \<longrightarrow> y \<notin> M
[PROOF STEP]
apply (erule_tac x = "{ys. size ys = size xs \<and> maxA#ys \<in> M}" in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k M m maxA xs. \<lbrakk>m \<in> M; \<forall>y. maxA \<sqsubset>\<^bsub>subtype P\<^esub> y \<longrightarrow> y \<notin> {a. \<exists>xsa. length xsa = length xs \<and> a # xsa \<in> M}; maxA # xs \<in> M; (\<exists>x. x \<in> {ys. length ys = length xs \<and> maxA # ys \<in> M}) \<longrightarrow> (\<exists>z\<in>{ys. length ys = length xs \<and> maxA # ys \<in> M}. \<forall>y. length z = length xs \<and> length y = length xs \<and> z [\<sqsubset>\<^bsub>subtype P\<^esub>] y \<longrightarrow> y \<notin> {ys. length ys = length xs \<and> maxA # ys \<in> M})\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = length xs) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = length xs) \<and> z [\<sqsubset>\<^bsub>subtype P\<^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>m \<in> M; \<forall>y. maxA \<sqsubset>\<^bsub>subtype P\<^esub> y \<longrightarrow> y \<notin> {a. \<exists>xsa. length xsa = length xs \<and> a # xsa \<in> M}; maxA # xs \<in> M\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> {ys. length ys = length xs \<and> maxA # ys \<in> M}
 2. \<And>k M m maxA xs. \<lbrakk>m \<in> M; \<forall>y. maxA \<sqsubset>\<^bsub>subtype P\<^esub> y \<longrightarrow> y \<notin> {a. \<exists>xsa. length xsa = length xs \<and> a # xsa \<in> M}; maxA # xs \<in> M; \<exists>z\<in>{ys. length ys = length xs \<and> maxA # ys \<in> M}. \<forall>y. length z = length xs \<and> length y = length xs \<and> z [\<sqsubset>\<^bsub>subtype P\<^esub>] y \<longrightarrow> y \<notin> {ys. length ys = length xs \<and> maxA # ys \<in> M}\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = length xs) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = length xs) \<and> z [\<sqsubset>\<^bsub>subtype P\<^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>m \<in> M; \<forall>y. maxA \<sqsubset>\<^bsub>subtype P\<^esub> y \<longrightarrow> y \<notin> {a. \<exists>xsa. length xsa = length xs \<and> a # xsa \<in> M}; maxA # xs \<in> M; \<exists>z\<in>{ys. length ys = length xs \<and> maxA # ys \<in> M}. \<forall>y. length z = length xs \<and> length y = length xs \<and> z [\<sqsubset>\<^bsub>subtype P\<^esub>] y \<longrightarrow> y \<notin> {ys. length ys = length xs \<and> maxA # ys \<in> M}\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = length xs) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = length xs) \<and> z [\<sqsubset>\<^bsub>subtype P\<^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>m \<in> M; \<forall>y. maxA \<sqsubset>\<^bsub>subtype P\<^esub> y \<longrightarrow> y \<notin> {a. \<exists>xsa. length xsa = length xs \<and> a # xsa \<in> M}; maxA # xs \<in> M; \<forall>y. length z = length xs \<and> length y = length xs \<and> z [\<sqsubset>\<^bsub>subtype P\<^esub>] y \<longrightarrow> y \<notin> {ys. length ys = length xs \<and> maxA # ys \<in> M}; length z = length xs; maxA # z \<in> M\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = length xs) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = length xs) \<and> z [\<sqsubset>\<^bsub>subtype P\<^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>\<forall>y. maxA \<sqsubset>\<^bsub>subtype P\<^esub> y \<longrightarrow> y \<notin> {a. \<exists>xsa. length xsa = length xs \<and> a # xsa \<in> M}; maxA # xs \<in> M; \<forall>y. length z = length xs \<and> length y = length xs \<and> z [\<sqsubset>\<^bsub>subtype P\<^esub>] y \<longrightarrow> y \<notin> {ys. length ys = length xs \<and> maxA # ys \<in> M}; length z = length xs; maxA # z \<in> M\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = length xs) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = length xs) \<and> z [\<sqsubset>\<^bsub>subtype P\<^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>\<forall>y. maxA \<sqsubset>\<^bsub>subtype P\<^esub> y \<longrightarrow> y \<notin> {a. \<exists>xsa. length xsa = length xs \<and> a # xsa \<in> M}; \<forall>y. length z = length xs \<and> length y = length xs \<and> z [\<sqsubset>\<^bsub>subtype P\<^esub>] y \<longrightarrow> y \<notin> {ys. length ys = length xs \<and> maxA # ys \<in> M}; length z = length xs; maxA # z \<in> M\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = length xs) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = length xs) \<and> z [\<sqsubset>\<^bsub>subtype P\<^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>\<forall>y. maxA \<sqsubset>\<^bsub>subtype P\<^esub> y \<longrightarrow> y \<notin> {a. \<exists>xsa. length xsa = length xs \<and> a # xsa \<in> M}; \<forall>y. length z = length xs \<and> length y = length xs \<and> z [\<sqsubset>\<^bsub>subtype P\<^esub>] y \<longrightarrow> y \<notin> {ys. length ys = length xs \<and> maxA # ys \<in> M}; length z = length xs; maxA # z \<in> M\<rbrakk> \<Longrightarrow> \<forall>y. (\<exists>y ys. ?z205 k M m maxA xs z = y # ys \<and> length ys = length xs) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = length xs) \<and> ?z205 k M m maxA xs z [\<sqsubset>\<^bsub>subtype P\<^esub>] y \<longrightarrow> y \<notin> M
 2. \<And>k M m maxA xs z. \<lbrakk>\<forall>y. maxA \<sqsubset>\<^bsub>subtype P\<^esub> y \<longrightarrow> y \<notin> {a. \<exists>xsa. length xsa = length xs \<and> a # xsa \<in> M}; \<forall>y. length z = length xs \<and> length y = length xs \<and> z [\<sqsubset>\<^bsub>subtype P\<^esub>] y \<longrightarrow> y \<notin> {ys. length ys = length xs \<and> maxA # ys \<in> M}; length z = length xs; maxA # z \<in> M\<rbrakk> \<Longrightarrow> ?z205 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>\<forall>y. maxA \<sqsubset>\<^bsub>subtype P\<^esub> y \<longrightarrow> y \<notin> {a. \<exists>xsa. length xsa = length xs \<and> a # xsa \<in> M}; \<forall>y. length z = length xs \<and> length y = length xs \<and> z [\<sqsubset>\<^bsub>subtype P\<^esub>] y \<longrightarrow> y \<notin> {ys. length ys = length xs \<and> maxA # ys \<in> M}; length z = length xs; maxA # z \<in> M\<rbrakk> \<Longrightarrow> ?z205 k M m maxA xs z \<in> M
 2. \<And>k M m maxA xs z. \<lbrakk>\<forall>y. maxA \<sqsubset>\<^bsub>subtype P\<^esub> y \<longrightarrow> y \<notin> {a. \<exists>xsa. length xsa = length xs \<and> a # xsa \<in> M}; \<forall>y. length z = length xs \<and> length y = length xs \<and> z [\<sqsubset>\<^bsub>subtype P\<^esub>] y \<longrightarrow> y \<notin> {ys. length ys = length xs \<and> maxA # ys \<in> M}; length z = length xs; maxA # z \<in> M\<rbrakk> \<Longrightarrow> \<forall>y. (\<exists>y ys. ?z205 k M m maxA xs z = y # ys \<and> length ys = length xs) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = length xs) \<and> ?z205 k M m maxA xs z [\<sqsubset>\<^bsub>subtype P\<^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>\<forall>y. maxA \<sqsubset>\<^bsub>subtype P\<^esub> y \<longrightarrow> y \<notin> {a. \<exists>xsa. length xsa = length xs \<and> a # xsa \<in> M}; \<forall>y. length z = length xs \<and> length y = length xs \<and> z [\<sqsubset>\<^bsub>subtype P\<^esub>] y \<longrightarrow> y \<notin> {ys. length ys = length xs \<and> maxA # ys \<in> M}; length z = length xs; maxA # z \<in> M\<rbrakk> \<Longrightarrow> \<forall>y. (\<exists>y ys. maxA # z = y # ys \<and> length ys = length xs) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = length xs) \<and> maxA # z [\<sqsubset>\<^bsub>subtype P\<^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>\<forall>y. ya \<sqsubset>\<^bsub>subtype P\<^esub> y \<longrightarrow> y \<notin> {a. \<exists>xsa. length xsa = length xs \<and> a # xsa \<in> M}; \<forall>y. length ys = length xs \<and> length y = length xs \<and> ys [\<sqsubset>\<^bsub>subtype P\<^esub>] y \<longrightarrow> y \<notin> {ys. length ys = length xs \<and> ya # ys \<in> M}; length ys = length xs; ya # ys \<in> M; ya # ys [\<sqsubset>\<^bsub>subtype P\<^esub>] yb # ysa; length ys = length xs; length ysa = length xs; yb # ysa \<in> M\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>M xs ya ys yb ysa. \<lbrakk>\<forall>y. ya \<sqsubset>\<^bsub>subtype P\<^esub> y \<longrightarrow> (\<forall>xsa. length xsa = length xs \<longrightarrow> y # xsa \<notin> M); \<forall>y. length y = length xs \<and> ys [\<sqsubset>\<^bsub>subtype P\<^esub>] y \<longrightarrow> ya # y \<notin> M; ya # ys \<in> M; ya \<sqsubset>\<^bsub>subtype P\<^esub> yb \<and> ys [\<sqsubseteq>\<^bsub>subtype P\<^esub>] ysa \<or> ya = yb \<and> ys [\<sqsubset>\<^bsub>subtype P\<^esub>] ysa; length ys = length xs; length ysa = length xs; yb # ysa \<in> M\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma acc_le_listI2 [intro!]:
  " acc (Err.le (subtype P)) \<Longrightarrow> acc (Listn.le (Err.le (subtype P)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. acc (Err.le (subtype P)) \<Longrightarrow> acc (Listn.le (Err.le (subtype P)))
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. acc (Err.le (subtype P)) \<Longrightarrow> acc (Listn.le (Err.le (subtype P)))
[PROOF STEP]
apply (unfold acc_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf {(y, x). x \<sqsubset>\<^bsub>Err.le (subtype P)\<^esub> y} \<Longrightarrow> wf {(y, x). x [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] y}
[PROOF STEP]
apply (subgoal_tac
 "wf(UN n. {(ys,xs). size xs = n \<and> size ys = n \<and> xs <_(Listn.le (Err.le (subtype P))) ys})")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>wf {(y, x). x \<sqsubset>\<^bsub>Err.le (subtype P)\<^esub> y}; wf (\<Union>n. {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] ys})\<rbrakk> \<Longrightarrow> wf {(y, x). x [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] y}
 2. wf {(y, x). x \<sqsubset>\<^bsub>Err.le (subtype P)\<^esub> y} \<Longrightarrow> wf (\<Union>n. {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] ys})
[PROOF STEP]
apply (erule wf_subset)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. wf {(y, x). x \<sqsubset>\<^bsub>Err.le (subtype P)\<^esub> y} \<Longrightarrow> {(y, x). x [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] y} \<subseteq> (\<Union>n. {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] ys})
 2. wf {(y, x). x \<sqsubset>\<^bsub>Err.le (subtype P)\<^esub> y} \<Longrightarrow> wf (\<Union>n. {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] ys})
[PROOF STEP]
apply (blast intro: lesssub_lengthD)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf {(y, x). x \<sqsubset>\<^bsub>Err.le (subtype P)\<^esub> y} \<Longrightarrow> wf (\<Union>n. {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] ys})
[PROOF STEP]
apply (rule wf_UN)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>wf {(y, x). x \<sqsubset>\<^bsub>Err.le (subtype P)\<^esub> y}; n \<in> UNIV\<rbrakk> \<Longrightarrow> wf {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] ys}
 2. \<And>n j. \<lbrakk>wf {(y, x). x \<sqsubset>\<^bsub>Err.le (subtype P)\<^esub> y}; n \<in> UNIV; j \<in> UNIV; {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] ys} \<noteq> {(ys, xs). length xs = j \<and> length ys = j \<and> xs [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] ys}\<rbrakk> \<Longrightarrow> Domain {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] ys} \<inter> Range {(ys, xs). length xs = j \<and> length ys = j \<and> xs [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] ys} = {}
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n j. \<lbrakk>wf {(y, x). x \<sqsubset>\<^bsub>Err.le (subtype P)\<^esub> y}; n \<in> UNIV; j \<in> UNIV; {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] ys} \<noteq> {(ys, xs). length xs = j \<and> length ys = j \<and> xs [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] ys}\<rbrakk> \<Longrightarrow> Domain {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] ys} \<inter> Range {(ys, xs). length xs = j \<and> length ys = j \<and> xs [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] ys} = {}
 2. \<And>n. \<lbrakk>wf {(y, x). x \<sqsubset>\<^bsub>Err.le (subtype P)\<^esub> y}; n \<in> UNIV\<rbrakk> \<Longrightarrow> wf {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] ys}
[PROOF STEP]
apply (rename_tac m n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m n. \<lbrakk>wf {(y, x). x \<sqsubset>\<^bsub>Err.le (subtype P)\<^esub> y}; m \<in> UNIV; n \<in> UNIV; {(ys, xs). length xs = m \<and> length ys = m \<and> xs [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] ys} \<noteq> {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] ys}\<rbrakk> \<Longrightarrow> Domain {(ys, xs). length xs = m \<and> length ys = m \<and> xs [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] ys} \<inter> Range {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] ys} = {}
 2. \<And>n. \<lbrakk>wf {(y, x). x \<sqsubset>\<^bsub>Err.le (subtype P)\<^esub> y}; n \<in> UNIV\<rbrakk> \<Longrightarrow> wf {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] ys}
[PROOF STEP]
apply (case_tac "m=n")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>m n. \<lbrakk>wf {(y, x). x \<sqsubset>\<^bsub>Err.le (subtype P)\<^esub> y}; m \<in> UNIV; n \<in> UNIV; {(ys, xs). length xs = m \<and> length ys = m \<and> xs [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] ys} \<noteq> {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] ys}; m = n\<rbrakk> \<Longrightarrow> Domain {(ys, xs). length xs = m \<and> length ys = m \<and> xs [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] ys} \<inter> Range {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] ys} = {}
 2. \<And>m n. \<lbrakk>wf {(y, x). x \<sqsubset>\<^bsub>Err.le (subtype P)\<^esub> y}; m \<in> UNIV; n \<in> UNIV; {(ys, xs). length xs = m \<and> length ys = m \<and> xs [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] ys} \<noteq> {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] ys}; m \<noteq> n\<rbrakk> \<Longrightarrow> Domain {(ys, xs). length xs = m \<and> length ys = m \<and> xs [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] ys} \<inter> Range {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] ys} = {}
 3. \<And>n. \<lbrakk>wf {(y, x). x \<sqsubset>\<^bsub>Err.le (subtype P)\<^esub> y}; n \<in> UNIV\<rbrakk> \<Longrightarrow> wf {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] ys}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m n. \<lbrakk>wf {(y, x). x \<sqsubset>\<^bsub>Err.le (subtype P)\<^esub> y}; m \<in> UNIV; n \<in> UNIV; {(ys, xs). length xs = m \<and> length ys = m \<and> xs [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] ys} \<noteq> {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] ys}; m \<noteq> n\<rbrakk> \<Longrightarrow> Domain {(ys, xs). length xs = m \<and> length ys = m \<and> xs [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] ys} \<inter> Range {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] ys} = {}
 2. \<And>n. \<lbrakk>wf {(y, x). x \<sqsubset>\<^bsub>Err.le (subtype P)\<^esub> y}; n \<in> UNIV\<rbrakk> \<Longrightarrow> wf {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] ys}
[PROOF STEP]
apply (fast intro!: equals0I dest: not_sym)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>wf {(y, x). x \<sqsubset>\<^bsub>Err.le (subtype P)\<^esub> y}; n \<in> UNIV\<rbrakk> \<Longrightarrow> wf {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] ys}
[PROOF STEP]
apply (rename_tac n)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>wf {(y, x). x \<sqsubset>\<^bsub>Err.le (subtype P)\<^esub> y}; n \<in> UNIV\<rbrakk> \<Longrightarrow> wf {(ys, xs). length xs = n \<and> length ys = n \<and> xs [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] ys}
[PROOF STEP]
apply (induct_tac n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>wf {(y, x). x \<sqsubset>\<^bsub>Err.le (subtype P)\<^esub> y}; n \<in> UNIV\<rbrakk> \<Longrightarrow> wf {a. case a of (ys, xs) \<Rightarrow> length xs = 0 \<and> length ys = 0 \<and> xs [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] ys}
 2. \<And>n na. \<lbrakk>wf {(y, x). x \<sqsubset>\<^bsub>Err.le (subtype P)\<^esub> y}; n \<in> UNIV; wf {a. case a of (ys, xs) \<Rightarrow> length xs = na \<and> length ys = na \<and> xs [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] ys}\<rbrakk> \<Longrightarrow> wf {a. case a of (ys, xs) \<Rightarrow> length xs = Suc na \<and> length ys = Suc na \<and> xs [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] ys}
[PROOF STEP]
apply (simp add: lesssub_def cong: conj_cong)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n na. \<lbrakk>wf {(y, x). x \<sqsubset>\<^bsub>Err.le (subtype P)\<^esub> y}; n \<in> UNIV; wf {a. case a of (ys, xs) \<Rightarrow> length xs = na \<and> length ys = na \<and> xs [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] ys}\<rbrakk> \<Longrightarrow> wf {a. case a of (ys, xs) \<Rightarrow> length xs = Suc na \<and> length ys = Suc na \<and> xs [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] ys}
[PROOF STEP]
apply (rename_tac k)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n k. \<lbrakk>wf {(y, x). x \<sqsubset>\<^bsub>Err.le (subtype P)\<^esub> y}; n \<in> UNIV; wf {a. case a of (ys, xs) \<Rightarrow> length xs = k \<and> length ys = k \<and> xs [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] ys}\<rbrakk> \<Longrightarrow> wf {a. case a of (ys, xs) \<Rightarrow> length xs = Suc k \<and> length ys = Suc k \<and> xs [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] ys}
[PROOF STEP]
apply (simp add: wf_eq_minimal)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. z \<sqsubset>\<^bsub>Err.le (subtype P)\<^esub> y \<longrightarrow> y \<notin> Q); \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. length z = k \<and> length y = k \<and> z [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] y \<longrightarrow> y \<notin> Q)\<rbrakk> \<Longrightarrow> \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. length z = Suc k \<and> length y = Suc k \<and> z [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] y \<longrightarrow> y \<notin> Q)
[PROOF STEP]
apply (simp (no_asm) add: length_Suc_conv cong: conj_cong)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. z \<sqsubset>\<^bsub>Err.le (subtype P)\<^esub> y \<longrightarrow> y \<notin> Q); \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. length z = k \<and> length y = k \<and> z [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] y \<longrightarrow> y \<notin> Q)\<rbrakk> \<Longrightarrow> \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = k) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = k) \<and> z [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] y \<longrightarrow> y \<notin> Q)
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k Q x. \<lbrakk>\<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. z \<sqsubset>\<^bsub>Err.le (subtype P)\<^esub> y \<longrightarrow> y \<notin> Q); \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. length z = k \<and> length y = k \<and> z [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] y \<longrightarrow> y \<notin> Q); x \<in> Q\<rbrakk> \<Longrightarrow> \<exists>z\<in>Q. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = k) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = k) \<and> z [\<sqsubset>\<^bsub>Err.le (subtype P)\<^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>\<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. z \<sqsubset>\<^bsub>Err.le (subtype P)\<^esub> y \<longrightarrow> y \<notin> Q); \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. length z = k \<and> length y = k \<and> z [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] y \<longrightarrow> y \<notin> Q); m \<in> M\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = k) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = k) \<and> z [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] y \<longrightarrow> y \<notin> M
[PROOF STEP]
apply (case_tac "\<exists>x xs. size xs = k \<and> x#xs \<in> M")
[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 \<sqsubset>\<^bsub>Err.le (subtype P)\<^esub> y \<longrightarrow> y \<notin> Q); \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. length z = k \<and> length y = k \<and> z [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] y \<longrightarrow> y \<notin> Q); m \<in> M; \<exists>x xs. length xs = k \<and> x # xs \<in> M\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = k) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = k) \<and> z [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] y \<longrightarrow> y \<notin> M
 2. \<And>k M m. \<lbrakk>\<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. z \<sqsubset>\<^bsub>Err.le (subtype P)\<^esub> y \<longrightarrow> y \<notin> Q); \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. length z = k \<and> length y = k \<and> z [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] y \<longrightarrow> y \<notin> Q); m \<in> M; \<nexists>x xs. length xs = k \<and> x # xs \<in> M\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = k) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = k) \<and> z [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] y \<longrightarrow> y \<notin> M
[PROOF STEP]
prefer 2
[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 \<sqsubset>\<^bsub>Err.le (subtype P)\<^esub> y \<longrightarrow> y \<notin> Q); \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. length z = k \<and> length y = k \<and> z [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] y \<longrightarrow> y \<notin> Q); m \<in> M; \<nexists>x xs. length xs = k \<and> x # xs \<in> M\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = k) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = k) \<and> z [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] y \<longrightarrow> y \<notin> M
 2. \<And>k M m. \<lbrakk>\<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. z \<sqsubset>\<^bsub>Err.le (subtype P)\<^esub> y \<longrightarrow> y \<notin> Q); \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. length z = k \<and> length y = k \<and> z [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] y \<longrightarrow> y \<notin> Q); m \<in> M; \<exists>x xs. length xs = k \<and> x # xs \<in> M\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = k) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = k) \<and> z [\<sqsubset>\<^bsub>Err.le (subtype P)\<^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. length z = k \<and> length y = k \<and> z [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] y \<longrightarrow> y \<notin> Q); m \<in> M; \<nexists>x xs. length xs = k \<and> x # xs \<in> M\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = k) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = k) \<and> z [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] y \<longrightarrow> y \<notin> M
 2. \<And>k M m. \<lbrakk>\<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. z \<sqsubset>\<^bsub>Err.le (subtype P)\<^esub> y \<longrightarrow> y \<notin> Q); \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. length z = k \<and> length y = k \<and> z [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] y \<longrightarrow> y \<notin> Q); m \<in> M; \<exists>x xs. length xs = k \<and> x # xs \<in> M\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = k) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = k) \<and> z [\<sqsubset>\<^bsub>Err.le (subtype P)\<^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>m \<in> M; \<nexists>x xs. length xs = k \<and> x # xs \<in> M\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = k) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = k) \<and> z [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] y \<longrightarrow> y \<notin> M
 2. \<And>k M m. \<lbrakk>\<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. z \<sqsubset>\<^bsub>Err.le (subtype P)\<^esub> y \<longrightarrow> y \<notin> Q); \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. length z = k \<and> length y = k \<and> z [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] y \<longrightarrow> y \<notin> Q); m \<in> M; \<exists>x xs. length xs = k \<and> x # xs \<in> M\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = k) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = k) \<and> z [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] y \<longrightarrow> y \<notin> M
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k M m. \<lbrakk>\<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. z \<sqsubset>\<^bsub>Err.le (subtype P)\<^esub> y \<longrightarrow> y \<notin> Q); \<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. length z = k \<and> length y = k \<and> z [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] y \<longrightarrow> y \<notin> Q); m \<in> M; \<exists>x xs. length xs = k \<and> x # xs \<in> M\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = k) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = k) \<and> z [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] y \<longrightarrow> y \<notin> M
[PROOF STEP]
apply (erule_tac x = "{a. \<exists>xs. size xs = k \<and> a#xs:M}" in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k M m. \<lbrakk>\<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. length z = k \<and> length y = k \<and> z [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] y \<longrightarrow> y \<notin> Q); m \<in> M; \<exists>x xs. length xs = k \<and> x # xs \<in> M; (\<exists>x. x \<in> {a. \<exists>xs. length xs = k \<and> a # xs \<in> M}) \<longrightarrow> (\<exists>z\<in>{a. \<exists>xs. length xs = k \<and> a # xs \<in> M}. \<forall>y. z \<sqsubset>\<^bsub>Err.le (subtype P)\<^esub> y \<longrightarrow> y \<notin> {a. \<exists>xs. length xs = k \<and> a # xs \<in> M})\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = k) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = k) \<and> z [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] y \<longrightarrow> y \<notin> M
[PROOF STEP]
apply (erule impE)
[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. length z = k \<and> length y = k \<and> z [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] y \<longrightarrow> y \<notin> Q); m \<in> M; \<exists>x xs. length xs = k \<and> x # xs \<in> M\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> {a. \<exists>xs. length xs = k \<and> a # xs \<in> M}
 2. \<And>k M m. \<lbrakk>\<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. length z = k \<and> length y = k \<and> z [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] y \<longrightarrow> y \<notin> Q); m \<in> M; \<exists>x xs. length xs = k \<and> x # xs \<in> M; \<exists>z\<in>{a. \<exists>xs. length xs = k \<and> a # xs \<in> M}. \<forall>y. z \<sqsubset>\<^bsub>Err.le (subtype P)\<^esub> y \<longrightarrow> y \<notin> {a. \<exists>xs. length xs = k \<and> a # xs \<in> M}\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = k) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = k) \<and> z [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] y \<longrightarrow> y \<notin> M
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k M m. \<lbrakk>\<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. length z = k \<and> length y = k \<and> z [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] y \<longrightarrow> y \<notin> Q); m \<in> M; \<exists>x xs. length xs = k \<and> x # xs \<in> M; \<exists>z\<in>{a. \<exists>xs. length xs = k \<and> a # xs \<in> M}. \<forall>y. z \<sqsubset>\<^bsub>Err.le (subtype P)\<^esub> y \<longrightarrow> y \<notin> {a. \<exists>xs. length xs = k \<and> a # xs \<in> M}\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = k) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = k) \<and> z [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] y \<longrightarrow> y \<notin> M
[PROOF STEP]
apply (thin_tac "\<exists>x xs. P x xs" for P)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k M m. \<lbrakk>\<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. length z = k \<and> length y = k \<and> z [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] y \<longrightarrow> y \<notin> Q); m \<in> M; \<exists>z\<in>{a. \<exists>xs. length xs = k \<and> a # xs \<in> M}. \<forall>y. z \<sqsubset>\<^bsub>Err.le (subtype P)\<^esub> y \<longrightarrow> y \<notin> {a. \<exists>xs. length xs = k \<and> a # xs \<in> M}\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = k) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = k) \<and> z [\<sqsubset>\<^bsub>Err.le (subtype P)\<^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>\<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. length z = length xs \<and> length y = length xs \<and> z [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] y \<longrightarrow> y \<notin> Q); m \<in> M; \<forall>y. z \<sqsubset>\<^bsub>Err.le (subtype P)\<^esub> y \<longrightarrow> y \<notin> {a. \<exists>xsa. length xsa = length xs \<and> a # xsa \<in> M}; z # xs \<in> M\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = length xs) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = length xs) \<and> z [\<sqsubset>\<^bsub>Err.le (subtype P)\<^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>\<forall>Q. (\<exists>x. x \<in> Q) \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. length z = length xs \<and> length y = length xs \<and> z [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] y \<longrightarrow> y \<notin> Q); m \<in> M; \<forall>y. maxA \<sqsubset>\<^bsub>Err.le (subtype P)\<^esub> y \<longrightarrow> y \<notin> {a. \<exists>xsa. length xsa = length xs \<and> a # xsa \<in> M}; maxA # xs \<in> M\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = length xs) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = length xs) \<and> z [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] y \<longrightarrow> y \<notin> M
[PROOF STEP]
apply (erule_tac x = "{ys. size ys = size xs \<and> maxA#ys \<in> M}" in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k M m maxA xs. \<lbrakk>m \<in> M; \<forall>y. maxA \<sqsubset>\<^bsub>Err.le (subtype P)\<^esub> y \<longrightarrow> y \<notin> {a. \<exists>xsa. length xsa = length xs \<and> a # xsa \<in> M}; maxA # xs \<in> M; (\<exists>x. x \<in> {ys. length ys = length xs \<and> maxA # ys \<in> M}) \<longrightarrow> (\<exists>z\<in>{ys. length ys = length xs \<and> maxA # ys \<in> M}. \<forall>y. length z = length xs \<and> length y = length xs \<and> z [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] y \<longrightarrow> y \<notin> {ys. length ys = length xs \<and> maxA # ys \<in> M})\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = length xs) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = length xs) \<and> z [\<sqsubset>\<^bsub>Err.le (subtype P)\<^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>m \<in> M; \<forall>y. maxA \<sqsubset>\<^bsub>Err.le (subtype P)\<^esub> y \<longrightarrow> y \<notin> {a. \<exists>xsa. length xsa = length xs \<and> a # xsa \<in> M}; maxA # xs \<in> M\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> {ys. length ys = length xs \<and> maxA # ys \<in> M}
 2. \<And>k M m maxA xs. \<lbrakk>m \<in> M; \<forall>y. maxA \<sqsubset>\<^bsub>Err.le (subtype P)\<^esub> y \<longrightarrow> y \<notin> {a. \<exists>xsa. length xsa = length xs \<and> a # xsa \<in> M}; maxA # xs \<in> M; \<exists>z\<in>{ys. length ys = length xs \<and> maxA # ys \<in> M}. \<forall>y. length z = length xs \<and> length y = length xs \<and> z [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] y \<longrightarrow> y \<notin> {ys. length ys = length xs \<and> maxA # ys \<in> M}\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = length xs) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = length xs) \<and> z [\<sqsubset>\<^bsub>Err.le (subtype P)\<^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>m \<in> M; \<forall>y. maxA \<sqsubset>\<^bsub>Err.le (subtype P)\<^esub> y \<longrightarrow> y \<notin> {a. \<exists>xsa. length xsa = length xs \<and> a # xsa \<in> M}; maxA # xs \<in> M; \<exists>z\<in>{ys. length ys = length xs \<and> maxA # ys \<in> M}. \<forall>y. length z = length xs \<and> length y = length xs \<and> z [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] y \<longrightarrow> y \<notin> {ys. length ys = length xs \<and> maxA # ys \<in> M}\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = length xs) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = length xs) \<and> z [\<sqsubset>\<^bsub>Err.le (subtype P)\<^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>m \<in> M; \<forall>y. maxA \<sqsubset>\<^bsub>Err.le (subtype P)\<^esub> y \<longrightarrow> y \<notin> {a. \<exists>xsa. length xsa = length xs \<and> a # xsa \<in> M}; maxA # xs \<in> M; \<forall>y. length z = length xs \<and> length y = length xs \<and> z [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] y \<longrightarrow> y \<notin> {ys. length ys = length xs \<and> maxA # ys \<in> M}; length z = length xs; maxA # z \<in> M\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = length xs) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = length xs) \<and> z [\<sqsubset>\<^bsub>Err.le (subtype P)\<^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>\<forall>y. maxA \<sqsubset>\<^bsub>Err.le (subtype P)\<^esub> y \<longrightarrow> y \<notin> {a. \<exists>xsa. length xsa = length xs \<and> a # xsa \<in> M}; maxA # xs \<in> M; \<forall>y. length z = length xs \<and> length y = length xs \<and> z [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] y \<longrightarrow> y \<notin> {ys. length ys = length xs \<and> maxA # ys \<in> M}; length z = length xs; maxA # z \<in> M\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = length xs) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = length xs) \<and> z [\<sqsubset>\<^bsub>Err.le (subtype P)\<^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>\<forall>y. maxA \<sqsubset>\<^bsub>Err.le (subtype P)\<^esub> y \<longrightarrow> y \<notin> {a. \<exists>xsa. length xsa = length xs \<and> a # xsa \<in> M}; \<forall>y. length z = length xs \<and> length y = length xs \<and> z [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] y \<longrightarrow> y \<notin> {ys. length ys = length xs \<and> maxA # ys \<in> M}; length z = length xs; maxA # z \<in> M\<rbrakk> \<Longrightarrow> \<exists>z\<in>M. \<forall>y. (\<exists>y ys. z = y # ys \<and> length ys = length xs) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = length xs) \<and> z [\<sqsubset>\<^bsub>Err.le (subtype P)\<^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>\<forall>y. maxA \<sqsubset>\<^bsub>Err.le (subtype P)\<^esub> y \<longrightarrow> y \<notin> {a. \<exists>xsa. length xsa = length xs \<and> a # xsa \<in> M}; \<forall>y. length z = length xs \<and> length y = length xs \<and> z [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] y \<longrightarrow> y \<notin> {ys. length ys = length xs \<and> maxA # ys \<in> M}; length z = length xs; maxA # z \<in> M\<rbrakk> \<Longrightarrow> \<forall>y. (\<exists>y ys. ?z205 k M m maxA xs z = y # ys \<and> length ys = length xs) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = length xs) \<and> ?z205 k M m maxA xs z [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] y \<longrightarrow> y \<notin> M
 2. \<And>k M m maxA xs z. \<lbrakk>\<forall>y. maxA \<sqsubset>\<^bsub>Err.le (subtype P)\<^esub> y \<longrightarrow> y \<notin> {a. \<exists>xsa. length xsa = length xs \<and> a # xsa \<in> M}; \<forall>y. length z = length xs \<and> length y = length xs \<and> z [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] y \<longrightarrow> y \<notin> {ys. length ys = length xs \<and> maxA # ys \<in> M}; length z = length xs; maxA # z \<in> M\<rbrakk> \<Longrightarrow> ?z205 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>\<forall>y. maxA \<sqsubset>\<^bsub>Err.le (subtype P)\<^esub> y \<longrightarrow> y \<notin> {a. \<exists>xsa. length xsa = length xs \<and> a # xsa \<in> M}; \<forall>y. length z = length xs \<and> length y = length xs \<and> z [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] y \<longrightarrow> y \<notin> {ys. length ys = length xs \<and> maxA # ys \<in> M}; length z = length xs; maxA # z \<in> M\<rbrakk> \<Longrightarrow> ?z205 k M m maxA xs z \<in> M
 2. \<And>k M m maxA xs z. \<lbrakk>\<forall>y. maxA \<sqsubset>\<^bsub>Err.le (subtype P)\<^esub> y \<longrightarrow> y \<notin> {a. \<exists>xsa. length xsa = length xs \<and> a # xsa \<in> M}; \<forall>y. length z = length xs \<and> length y = length xs \<and> z [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] y \<longrightarrow> y \<notin> {ys. length ys = length xs \<and> maxA # ys \<in> M}; length z = length xs; maxA # z \<in> M\<rbrakk> \<Longrightarrow> \<forall>y. (\<exists>y ys. ?z205 k M m maxA xs z = y # ys \<and> length ys = length xs) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = length xs) \<and> ?z205 k M m maxA xs z [\<sqsubset>\<^bsub>Err.le (subtype P)\<^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>\<forall>y. maxA \<sqsubset>\<^bsub>Err.le (subtype P)\<^esub> y \<longrightarrow> y \<notin> {a. \<exists>xsa. length xsa = length xs \<and> a # xsa \<in> M}; \<forall>y. length z = length xs \<and> length y = length xs \<and> z [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] y \<longrightarrow> y \<notin> {ys. length ys = length xs \<and> maxA # ys \<in> M}; length z = length xs; maxA # z \<in> M\<rbrakk> \<Longrightarrow> \<forall>y. (\<exists>y ys. maxA # z = y # ys \<and> length ys = length xs) \<and> (\<exists>ya ys. y = ya # ys \<and> length ys = length xs) \<and> maxA # z [\<sqsubset>\<^bsub>Err.le (subtype P)\<^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>\<forall>y. ya \<sqsubset>\<^bsub>Err.le (subtype P)\<^esub> y \<longrightarrow> y \<notin> {a. \<exists>xsa. length xsa = length xs \<and> a # xsa \<in> M}; \<forall>y. length ys = length xs \<and> length y = length xs \<and> ys [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] y \<longrightarrow> y \<notin> {ys. length ys = length xs \<and> ya # ys \<in> M}; length ys = length xs; ya # ys \<in> M; ya # ys [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] yb # ysa; length ys = length xs; length ysa = length xs; yb # ysa \<in> M\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>M xs ya ys yb ysa. \<lbrakk>\<forall>y. ya \<sqsubset>\<^bsub>Err.le (subtype P)\<^esub> y \<longrightarrow> (\<forall>xsa. length xsa = length xs \<longrightarrow> y # xsa \<notin> M); \<forall>y. length y = length xs \<and> ys [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] y \<longrightarrow> ya # y \<notin> M; ya # ys \<in> M; ya \<sqsubset>\<^bsub>Err.le (subtype P)\<^esub> yb \<and> ys [\<sqsubseteq>\<^bsub>Err.le (subtype P)\<^esub>] ysa \<or> ya = yb \<and> ys [\<sqsubset>\<^bsub>Err.le (subtype P)\<^esub>] ysa; length ys = length xs; length ysa = length xs; yb # ysa \<in> M\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma acc_JVM [intro]:
  "wf_prog wf_mb P \<Longrightarrow> acc (JVM_SemiType.le P mxs mxl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_prog wf_mb P \<Longrightarrow> acc (JVM_SemiType.le P mxs mxl)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_prog wf_mb P \<Longrightarrow> acc (JVM_SemiType.le P mxs mxl)
[PROOF STEP]
by (unfold JVM_le_unfold) blast (*>*)  \<comment>\<open> use acc_listI1, acc_listI2 \<close>


[STATEMENT]
lemma hadd: "x @+ y = x \<squnion> RepFun y (\<lambda>z. x @+ z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x @+ y = x \<squnion> RepFun y ((@+) x)
[PROOF STEP]
by (metis def_hmemrec RepFun_ecut hadd_def order_refl)


[STATEMENT]
lemma hmem_hadd_E:
  assumes l: "l \<^bold>\<in> x @+ y"
  obtains "l \<^bold>\<in> x" | z where "z \<^bold>\<in> y" "l = x @+ z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>l \<^bold>\<in> x \<Longrightarrow> thesis; \<And>z. \<lbrakk>z \<^bold>\<in> y; l = x @+ z\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using l
[PROOF STATE]
proof (prove)
using this:
l \<^bold>\<in> x @+ y

goal (1 subgoal):
 1. \<lbrakk>l \<^bold>\<in> x \<Longrightarrow> thesis; \<And>z. \<lbrakk>z \<^bold>\<in> y; l = x @+ z\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: hadd [of x y])


[STATEMENT]
lemma hadd_0_right [simp]: "x @+ 0 = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x @+ 0 = x
[PROOF STEP]
by (subst hadd) simp


[STATEMENT]
lemma hadd_hinsert_right: "x @+ hinsert y z = hinsert (x @+ y) (x @+ z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x @+ (z \<triangleleft> y) = x @+ z \<triangleleft> x @+ y
[PROOF STEP]
by (metis hadd hunion_hinsert_right RepFun_hinsert)


[STATEMENT]
lemma not_add_less_right: "\<not> (x @+ y < x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> x @+ y < x
[PROOF STEP]
apply (induct y, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y1 y2. \<lbrakk>\<not> x @+ y1 < x; \<not> x @+ y2 < x; y1 \<^bold>\<notin> y2; x @+ (y2 \<triangleleft> y1) < x\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (metis less_supI1 hadd order_less_le)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma not_add_mem_right: "\<not> (x @+ y \<^bold>\<in> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x @+ y \<^bold>\<notin> x
[PROOF STEP]
by (metis hadd hmem_not_refl hunion_iff)


[STATEMENT]
lemma hadd_0_left [simp]: "0 @+ x = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 @+ x = x
[PROOF STEP]
by (induct x) (auto simp: hadd_hinsert_right)


[STATEMENT]
lemma hadd_succ_left [simp]: "Ord y \<Longrightarrow> succ x @+ y = succ (x @+ y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ord y \<Longrightarrow> succ x @+ y = succ (x @+ y)
[PROOF STEP]
by (induct y rule: Ord_induct2) auto


[STATEMENT]
lemma hadd_assoc: "(x @+ y) @+ z = x @+ (y @+ z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x @+ y @+ z = x @+ (y @+ z)
[PROOF STEP]
by (induct z) (auto simp: hadd_hinsert_right)


[STATEMENT]
lemma RepFun_hadd_disjoint: "x \<sqinter> RepFun y ((@+) x) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<sqinter> RepFun y ((@+) x) = 0
[PROOF STEP]
by (metis hf_equalityI RepFun_iff hinter_iff not_add_mem_right hmem_hempty)


[STATEMENT]
lemma Rep_le_Cancel: "x \<squnion> RepFun y ((@+) x) \<le> x \<squnion> RepFun z ((@+) x)
                      \<Longrightarrow> RepFun y ((@+) x) \<le> RepFun z ((@+) x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<squnion> RepFun y ((@+) x) \<le> x \<squnion> RepFun z ((@+) x) \<Longrightarrow> RepFun y ((@+) x) \<le> RepFun z ((@+) x)
[PROOF STEP]
by (auto simp add: not_add_mem_right)


[STATEMENT]
lemma hadd_cancel_right [simp]: "x @+ y = x @+ z \<longleftrightarrow> y=z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x @+ y = x @+ z) = (y = z)
[PROOF STEP]
proof (induct y arbitrary: z rule: hmem_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa z. (\<And>y z. y \<^bold>\<in> xa \<Longrightarrow> (x @+ y = x @+ z) = (y = z)) \<Longrightarrow> (x @+ xa = x @+ z) = (xa = z)
[PROOF STEP]
case (step y z)
[PROOF STATE]
proof (state)
this:
?y \<^bold>\<in> y \<Longrightarrow> (x @+ ?y = x @+ ?z) = (?y = ?z)

goal (1 subgoal):
 1. \<And>xa z. (\<And>y z. y \<^bold>\<in> xa \<Longrightarrow> (x @+ y = x @+ z) = (y = z)) \<Longrightarrow> (x @+ xa = x @+ z) = (xa = z)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x @+ y = x @+ z) = (y = z)
[PROOF STEP]
proof auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x @+ y = x @+ z \<Longrightarrow> y = z
[PROOF STEP]
assume eq: "x @+ y = x @+ z"
[PROOF STATE]
proof (state)
this:
x @+ y = x @+ z

goal (1 subgoal):
 1. x @+ y = x @+ z \<Longrightarrow> y = z
[PROOF STEP]
hence  "RepFun y ((@+) x) = RepFun z ((@+) x)"
[PROOF STATE]
proof (prove)
using this:
x @+ y = x @+ z

goal (1 subgoal):
 1. RepFun y ((@+) x) = RepFun z ((@+) x)
[PROOF STEP]
by (metis hadd Rep_le_Cancel order_antisym order_refl)
[PROOF STATE]
proof (state)
this:
RepFun y ((@+) x) = RepFun z ((@+) x)

goal (1 subgoal):
 1. x @+ y = x @+ z \<Longrightarrow> y = z
[PROOF STEP]
thus  "y = z"
[PROOF STATE]
proof (prove)
using this:
RepFun y ((@+) x) = RepFun z ((@+) x)

goal (1 subgoal):
 1. y = z
[PROOF STEP]
by (metis hf_equalityI RepFun_iff step)
[PROOF STATE]
proof (state)
this:
y = z

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(x @+ y = x @+ z) = (y = z)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma RepFun_hadd_cancel: "RepFun y (\<lambda>z. x @+ z) = RepFun z (\<lambda>z. x @+ z) \<longleftrightarrow> y=z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (RepFun y ((@+) x) = RepFun z ((@+) x)) = (y = z)
[PROOF STEP]
by (metis hadd hadd_cancel_right)


[STATEMENT]
lemma hadd_hmem_cancel [simp]: "x @+ y \<^bold>\<in> x @+ z \<longleftrightarrow> y \<^bold>\<in> z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x @+ y \<^bold>\<in> x @+ z) = (y \<^bold>\<in> z)
[PROOF STEP]
apply (auto simp: hadd [of _ y] hadd [of _ z] not_add_mem_right)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. x \<squnion> RepFun y ((@+) x) \<^bold>\<in> x \<Longrightarrow> y \<^bold>\<in> z
 2. \<And>u. \<lbrakk>u \<^bold>\<in> z; x \<squnion> RepFun y ((@+) x) = x @+ u\<rbrakk> \<Longrightarrow> y \<^bold>\<in> z
[PROOF STEP]
apply (metis hmem_not_refl hunion_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>u. \<lbrakk>u \<^bold>\<in> z; x \<squnion> RepFun y ((@+) x) = x @+ u\<rbrakk> \<Longrightarrow> y \<^bold>\<in> z
[PROOF STEP]
apply (metis hadd hadd_cancel_right)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ord_of_add: "ord_of (i+j) = ord_of i @+ ord_of j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ord_of (i + j) = ord_of i @+ ord_of j
[PROOF STEP]
by (induct j) auto


[STATEMENT]
lemma Ord_hadd: "Ord x \<Longrightarrow> Ord y \<Longrightarrow> Ord (x @+ y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ord x; Ord y\<rbrakk> \<Longrightarrow> Ord (x @+ y)
[PROOF STEP]
by (induct x rule: Ord_induct2) auto


[STATEMENT]
lemma hmem_self_hadd [simp]: "k1 \<^bold>\<in> k1 @+ k2 \<longleftrightarrow> 0 \<^bold>\<in> k2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (k1 \<^bold>\<in> k1 @+ k2) = (0 \<^bold>\<in> k2)
[PROOF STEP]
by (metis hadd_0_right hadd_hmem_cancel)


[STATEMENT]
lemma hadd_commute: "Ord x \<Longrightarrow> Ord y \<Longrightarrow> x @+ y = y @+ x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ord x; Ord y\<rbrakk> \<Longrightarrow> x @+ y = y @+ x
[PROOF STEP]
by (induct x rule: Ord_induct2) auto


[STATEMENT]
lemma hadd_cancel_left [simp]: "Ord x \<Longrightarrow> y @+ x = z @+ x \<longleftrightarrow> y=z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ord x \<Longrightarrow> (y @+ x = z @+ x) = (y = z)
[PROOF STEP]
by (induct x rule: Ord_induct2) auto


[STATEMENT]
lemma pred_succ [simp]: "pred (succ x) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pred (succ x) = x
[PROOF STEP]
by (simp add: pred_def)


[STATEMENT]
lemma pred_0 [simp]: "pred 0 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pred 0 = 0
[PROOF STEP]
by (simp add: pred_def)


[STATEMENT]
lemma succ_pred [simp]: "Ord x \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> succ (pred x) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ord x; x \<noteq> 0\<rbrakk> \<Longrightarrow> succ (pred x) = x
[PROOF STEP]
by (metis Ord_cases pred_succ)


[STATEMENT]
lemma pred_mem [simp]: "Ord x \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> pred x \<^bold>\<in> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ord x; x \<noteq> 0\<rbrakk> \<Longrightarrow> pred x \<^bold>\<in> x
[PROOF STEP]
by (metis succ_iff succ_pred)


[STATEMENT]
lemma Ord_pred [simp]: "Ord x \<Longrightarrow> Ord (pred x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ord x \<Longrightarrow> Ord (pred x)
[PROOF STEP]
by (metis Ord_in_Ord pred_0 pred_mem)


[STATEMENT]
lemma hadd_pred_right: "Ord y \<Longrightarrow> y \<noteq> 0 \<Longrightarrow> x @+ pred y = pred (x @+ y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ord y; y \<noteq> 0\<rbrakk> \<Longrightarrow> x @+ pred y = pred (x @+ y)
[PROOF STEP]
by (metis hadd_succ_right pred_succ succ_pred)


[STATEMENT]
lemma Ord_pred_HUnion: "Ord(k) \<Longrightarrow> pred k = \<Squnion>k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ord k \<Longrightarrow> pred k = \<Squnion>k
[PROOF STEP]
by (metis HUnion_hempty Ordinal.Ord_pred pred_0 pred_succ)


[STATEMENT]
lemma shiftD: "x \<^bold>\<in> shift f delta \<Longrightarrow> \<exists>u. u \<^bold>\<in> f \<and> x = \<langle>delta @+ hfst u, hsnd u\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<^bold>\<in> shift f delta \<Longrightarrow> \<exists>u. u \<^bold>\<in> f \<and> x = \<langle>delta @+ hfst u, hsnd u\<rangle>
[PROOF STEP]
by (auto simp: shift_def hsplit_def)


[STATEMENT]
lemma hmem_shift_iff: "\<langle>m, y\<rangle> \<^bold>\<in> shift f delta \<longleftrightarrow> (\<exists>n. m = delta @+ n \<and> \<langle>n, y\<rangle> \<^bold>\<in> f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<langle>m, y\<rangle> \<^bold>\<in> shift f delta) = (\<exists>n. m = delta @+ n \<and> \<langle>n, y\<rangle> \<^bold>\<in> f)
[PROOF STEP]
by (auto simp: shift_def hrelation_def is_hpair_def)


[STATEMENT]
lemma hmem_shift_add_iff [simp]: "\<langle>delta @+ n, y\<rangle> \<^bold>\<in> shift f delta \<longleftrightarrow> \<langle>n, y\<rangle> \<^bold>\<in> f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<langle>delta @+ n, y\<rangle> \<^bold>\<in> shift f delta) = (\<langle>n, y\<rangle> \<^bold>\<in> f)
[PROOF STEP]
by (metis hadd_cancel_right hmem_shift_iff)


[STATEMENT]
lemma hrelation_shift [simp]: "hrelation (shift f delta)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hrelation (shift f delta)
[PROOF STEP]
by (auto simp: shift_def hrelation_def hsplit_def)


[STATEMENT]
lemma app_shift [simp]: "app (shift f k) (k @+ j) = app f j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. app (shift f k) (k @+ j) = app f j
[PROOF STEP]
by (simp add: app_def)


[STATEMENT]
lemma hfunction_shift_iff [simp]: "hfunction (shift f delta) = hfunction f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hfunction (shift f delta) = hfunction f
[PROOF STEP]
by (auto simp: hfunction_def hmem_shift_iff)


[STATEMENT]
lemma hdomain_shift_add: "hdomain (shift f delta) = \<lbrace>delta @+ n . n \<^bold>\<in> hdomain f\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hdomain (shift f delta) = RepFun (hdomain f) ((@+) delta)
[PROOF STEP]
by  (rule hf_equalityI) (force simp add: hdomain_def hmem_shift_iff)


[STATEMENT]
lemma hrelation_seq_append [simp]: "hrelation (seq_append k f g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hrelation (seq_append k f g)
[PROOF STEP]
by (simp add: seq_append_def)


[STATEMENT]
lemma Seq_append: "Seq s1 k1 \<Longrightarrow> Seq s2 k2 \<Longrightarrow> Seq (seq_append k1 s1 s2) (k1 @+ k2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Seq s1 k1; Seq s2 k2\<rbrakk> \<Longrightarrow> Seq (seq_append k1 s1 s2) (k1 @+ k2)
[PROOF STEP]
apply (auto simp: Seq_def seq_append_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>hrelation s1; hrelation s2; hfunction s1; k1 \<le> hdomain s1; hfunction s2; k2 \<le> hdomain s2\<rbrakk> \<Longrightarrow> hfunction (hrestrict s1 k1 \<squnion> shift s2 k1)
 2. \<And>x. \<lbrakk>hrelation s1; hrelation s2; hfunction s1; k1 \<le> hdomain s1; hfunction s2; k2 \<le> hdomain s2; x \<^bold>\<in> k1 @+ k2; x \<^bold>\<notin> hdomain (shift s2 k1)\<rbrakk> \<Longrightarrow> x \<^bold>\<in> hdomain s1
 3. \<And>x. \<lbrakk>hrelation s1; hrelation s2; hfunction s1; k1 \<le> hdomain s1; hfunction s2; k2 \<le> hdomain s2; x \<^bold>\<in> k1 @+ k2; x \<^bold>\<notin> hdomain (shift s2 k1)\<rbrakk> \<Longrightarrow> x \<^bold>\<in> k1
[PROOF STEP]
apply (metis hdomain_restr hdomain_shift_disjoint hfunction_hunion hfunction_restr hfunction_shift_iff inf_absorb2 seq_append_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>hrelation s1; hrelation s2; hfunction s1; k1 \<le> hdomain s1; hfunction s2; k2 \<le> hdomain s2; x \<^bold>\<in> k1 @+ k2; x \<^bold>\<notin> hdomain (shift s2 k1)\<rbrakk> \<Longrightarrow> x \<^bold>\<in> hdomain s1
 2. \<And>x. \<lbrakk>hrelation s1; hrelation s2; hfunction s1; k1 \<le> hdomain s1; hfunction s2; k2 \<le> hdomain s2; x \<^bold>\<in> k1 @+ k2; x \<^bold>\<notin> hdomain (shift s2 k1)\<rbrakk> \<Longrightarrow> x \<^bold>\<in> k1
[PROOF STEP]
apply (simp add: hdomain_shift_add)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>hrelation s1; hrelation s2; hfunction s1; k1 \<le> hdomain s1; hfunction s2; k2 \<le> hdomain s2; x \<^bold>\<in> k1 @+ k2; \<forall>u. u \<^bold>\<in> hdomain s2 \<longrightarrow> x \<noteq> k1 @+ u\<rbrakk> \<Longrightarrow> x \<^bold>\<in> hdomain s1
 2. \<And>x. \<lbrakk>hrelation s1; hrelation s2; hfunction s1; k1 \<le> hdomain s1; hfunction s2; k2 \<le> hdomain s2; x \<^bold>\<in> k1 @+ k2; x \<^bold>\<notin> hdomain (shift s2 k1)\<rbrakk> \<Longrightarrow> x \<^bold>\<in> k1
[PROOF STEP]
apply (metis hmem_hadd_E rev_hsubsetD)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>hrelation s1; hrelation s2; hfunction s1; k1 \<le> hdomain s1; hfunction s2; k2 \<le> hdomain s2; x \<^bold>\<in> k1 @+ k2; x \<^bold>\<notin> hdomain (shift s2 k1)\<rbrakk> \<Longrightarrow> x \<^bold>\<in> k1
[PROOF STEP]
apply (erule hmem_hadd_E, assumption, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>hrelation s1; hrelation s2; hfunction s1; k1 \<le> hdomain s1; hfunction s2; k2 \<le> hdomain s2; k1 @+ z \<^bold>\<notin> hdomain (shift s2 k1); z \<^bold>\<in> k2\<rbrakk> \<Longrightarrow> k1 @+ z \<^bold>\<in> k1
[PROOF STEP]
apply (metis Seq_def Seq_iff_app hdomainI hmem_shift_add_iff)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma app_hunion1: "x \<^bold>\<notin> hdomain g \<Longrightarrow> app (f \<squnion> g) x = app f x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<^bold>\<notin> hdomain g \<Longrightarrow> app (f \<squnion> g) x = app f x
[PROOF STEP]
by (auto simp: app_def) (metis hdomainI)


[STATEMENT]
lemma app_hunion2: "x \<^bold>\<notin> hdomain f \<Longrightarrow> app (f \<squnion> g) x = app g x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<^bold>\<notin> hdomain f \<Longrightarrow> app (f \<squnion> g) x = app g x
[PROOF STEP]
by (auto simp: app_def) (metis hdomainI)


[STATEMENT]
lemma Seq_append_app1: "Seq s k \<Longrightarrow> l \<^bold>\<in> k \<Longrightarrow> app (seq_append k s s') l = app s l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Seq s k; l \<^bold>\<in> k\<rbrakk> \<Longrightarrow> app (seq_append k s s') l = app s l
[PROOF STEP]
apply (auto simp: Seq_def seq_append_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>l \<^bold>\<in> k; hrelation s; hfunction s; k \<le> hdomain s\<rbrakk> \<Longrightarrow> app (hrestrict s k \<squnion> shift s' k) l = app s l
[PROOF STEP]
apply (metis app_hunion1 hdomain_shift_disjoint hemptyE hinter_iff app_hrestrict)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Seq_append_app2: "Seq s1 k1 \<Longrightarrow> Seq s2 k2 \<Longrightarrow> l = k1 @+ j \<Longrightarrow> app (seq_append k1 s1 s2) l = app s2 j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Seq s1 k1; Seq s2 k2; l = k1 @+ j\<rbrakk> \<Longrightarrow> app (seq_append k1 s1 s2) l = app s2 j
[PROOF STEP]
by (metis seq_append_def app_hunion2 app_shift hdomain_restr hinter_iff not_add_mem_right)


[STATEMENT]
lemma OrdDom_insf: "\<lbrakk>OrdDom s; Ord k\<rbrakk> \<Longrightarrow> OrdDom (insf s (succ k) y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>OrdDom s; Ord k\<rbrakk> \<Longrightarrow> OrdDom (insf s (succ k) y)
[PROOF STEP]
by (auto simp: insf_def OrdDom_def)


[STATEMENT]
lemma OrdDom_hunion [simp]: "OrdDom (s1 \<squnion> s2) \<longleftrightarrow> OrdDom s1 \<and> OrdDom s2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OrdDom (s1 \<squnion> s2) = (OrdDom s1 \<and> OrdDom s2)
[PROOF STEP]
by (auto simp: OrdDom_def)


[STATEMENT]
lemma OrdDom_hrestrict: "OrdDom s \<Longrightarrow> OrdDom (hrestrict s A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OrdDom s \<Longrightarrow> OrdDom (hrestrict s A)
[PROOF STEP]
by (auto simp: OrdDom_def)


[STATEMENT]
lemma OrdDom_shift: "\<lbrakk>OrdDom s; Ord k\<rbrakk> \<Longrightarrow> OrdDom (shift s k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>OrdDom s; Ord k\<rbrakk> \<Longrightarrow> OrdDom (shift s k)
[PROOF STEP]
by (auto simp: OrdDom_def shift_def Ord_hadd)


[STATEMENT]
lemma LstSeq_imp_Seq_same: "LstSeq s k y \<Longrightarrow> Seq s k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LstSeq s k y \<Longrightarrow> Seq s k
[PROOF STEP]
by (metis LstSeq_imp_Seq_succ Seq_succ_D)


[STATEMENT]
lemma LstSeq_imp_Ord: "LstSeq s k y \<Longrightarrow> Ord k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LstSeq s k y \<Longrightarrow> Ord k
[PROOF STEP]
by (metis LstSeq_def)


[STATEMENT]
lemma LstSeq_trunc: "LstSeq s k y \<Longrightarrow> l \<^bold>\<in> k \<Longrightarrow> LstSeq s l (app s l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>LstSeq s k y; l \<^bold>\<in> k\<rbrakk> \<Longrightarrow> LstSeq s l (app s l)
[PROOF STEP]
apply (auto simp: LstSeq_def Seq_iff_app)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>l \<^bold>\<in> k; Seq s (succ k); Ord k; OrdDom s; y = app s k\<rbrakk> \<Longrightarrow> Seq s (succ l)
 2. \<lbrakk>l \<^bold>\<in> k; Seq s (succ k); Ord k; OrdDom s; y = app s k\<rbrakk> \<Longrightarrow> Ord l
[PROOF STEP]
apply (metis Ord_succ Seq_Ord_D mem_succ_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>l \<^bold>\<in> k; Seq s (succ k); Ord k; OrdDom s; y = app s k\<rbrakk> \<Longrightarrow> Ord l
[PROOF STEP]
apply (metis Ord_in_Ord)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma LstSeq_insf: "LstSeq s k z \<Longrightarrow> LstSeq (insf s (succ k) y) (succ k) y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LstSeq s k z \<Longrightarrow> LstSeq (insf s (succ k) y) (succ k) y
[PROOF STEP]
by (metis OrdDom_insf LstSeq_def Ord_succ_iff Seq_imp_eq_app Seq_insf Seq_succ_iff app_insf_Seq)


[STATEMENT]
lemma app_insf_LstSeq: "LstSeq s k z \<Longrightarrow> app (insf s (succ k) y) (succ k) = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LstSeq s k z \<Longrightarrow> app (insf s (succ k) y) (succ k) = y
[PROOF STEP]
by (metis LstSeq_imp_Seq_succ app_insf_Seq)


[STATEMENT]
lemma app_insf2_LstSeq: "LstSeq s k z \<Longrightarrow> k' \<noteq> succ k \<Longrightarrow> app (insf s (succ k) y) k' = app s k'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>LstSeq s k z; k' \<noteq> succ k\<rbrakk> \<Longrightarrow> app (insf s (succ k) y) k' = app s k'
[PROOF STEP]
by (metis LstSeq_imp_Seq_succ app_insf2_Seq)


[STATEMENT]
lemma app_insf_LstSeq_if: "LstSeq s k z \<Longrightarrow> app (insf s (succ k) y) k' = (if k' = succ k then y else app s k')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LstSeq s k z \<Longrightarrow> app (insf s (succ k) y) k' = (if k' = succ k then y else app s k')
[PROOF STEP]
by (metis app_insf2_LstSeq app_insf_LstSeq)


[STATEMENT]
lemma LstSeq_append_app1:
  "LstSeq s k y \<Longrightarrow> l \<^bold>\<in> succ k \<Longrightarrow> app (seq_append (succ k) s s') l = app s l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>LstSeq s k y; l \<^bold>\<in> succ k\<rbrakk> \<Longrightarrow> app (seq_append (succ k) s s') l = app s l
[PROOF STEP]
by (metis LstSeq_imp_Seq_succ Seq_append_app1)


[STATEMENT]
lemma LstSeq_append_app2:
  "\<lbrakk>LstSeq s1 k1 y1; LstSeq s2 k2 y2; l = succ k1 @+ j\<rbrakk>
   \<Longrightarrow> app (seq_append (succ k1) s1 s2) l = app s2 j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>LstSeq s1 k1 y1; LstSeq s2 k2 y2; l = succ k1 @+ j\<rbrakk> \<Longrightarrow> app (seq_append (succ k1) s1 s2) l = app s2 j
[PROOF STEP]
by (metis LstSeq_imp_Seq_succ Seq_append_app2)


[STATEMENT]
lemma Seq_append_pair:
  "\<lbrakk>Seq s1 k1; Seq s2 (succ n);  \<langle>n, y\<rangle> \<^bold>\<in> s2; Ord n\<rbrakk> \<Longrightarrow> \<langle>k1 @+ n, y\<rangle> \<^bold>\<in> (seq_append k1 s1 s2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Seq s1 k1; Seq s2 (succ n); \<langle>n, y\<rangle> \<^bold>\<in> s2; Ord n\<rbrakk> \<Longrightarrow> \<langle>k1 @+ n, y\<rangle> \<^bold>\<in> seq_append k1 s1 s2
[PROOF STEP]
by (metis hmem_shift_add_iff hunion_iff seq_append_def)


[STATEMENT]
lemma Seq_append_OrdDom: "\<lbrakk>Ord k; OrdDom s1; OrdDom s2\<rbrakk> \<Longrightarrow> OrdDom (seq_append k s1 s2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Ord k; OrdDom s1; OrdDom s2\<rbrakk> \<Longrightarrow> OrdDom (seq_append k s1 s2)
[PROOF STEP]
by (auto simp: seq_append_def OrdDom_hrestrict OrdDom_shift)


[STATEMENT]
lemma LstSeq_append:
  "\<lbrakk>LstSeq s1 k1 y1; LstSeq s2 k2 y2\<rbrakk> \<Longrightarrow> LstSeq (seq_append (succ k1) s1 s2) (succ (k1 @+ k2)) y2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>LstSeq s1 k1 y1; LstSeq s2 k2 y2\<rbrakk> \<Longrightarrow> LstSeq (seq_append (succ k1) s1 s2) (succ (k1 @+ k2)) y2
[PROOF STEP]
apply (auto simp: LstSeq_def Seq_append Ord_hadd Seq_append_pair)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>Seq s1 (succ k1); Seq s2 (succ k2); Ord k1; Ord k2; \<langle>k1, y1\<rangle> \<^bold>\<in> s1; OrdDom s1; \<langle>k2, y2\<rangle> \<^bold>\<in> s2; OrdDom s2\<rbrakk> \<Longrightarrow> Seq (seq_append (succ k1) s1 s2) (succ (succ (k1 @+ k2)))
 2. \<lbrakk>Seq s1 (succ k1); Seq s2 (succ k2); Ord k1; Ord k2; \<langle>k1, y1\<rangle> \<^bold>\<in> s1; OrdDom s1; \<langle>k2, y2\<rangle> \<^bold>\<in> s2; OrdDom s2\<rbrakk> \<Longrightarrow> \<langle>succ (k1 @+ k2), y2\<rangle> \<^bold>\<in> seq_append (succ k1) s1 s2
 3. \<lbrakk>Seq s1 (succ k1); Seq s2 (succ k2); Ord k1; Ord k2; \<langle>k1, y1\<rangle> \<^bold>\<in> s1; OrdDom s1; \<langle>k2, y2\<rangle> \<^bold>\<in> s2; OrdDom s2\<rbrakk> \<Longrightarrow> OrdDom (seq_append (succ k1) s1 s2)
[PROOF STEP]
apply (metis Seq_append hadd_succ_left hadd_succ_right)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Seq s1 (succ k1); Seq s2 (succ k2); Ord k1; Ord k2; \<langle>k1, y1\<rangle> \<^bold>\<in> s1; OrdDom s1; \<langle>k2, y2\<rangle> \<^bold>\<in> s2; OrdDom s2\<rbrakk> \<Longrightarrow> \<langle>succ (k1 @+ k2), y2\<rangle> \<^bold>\<in> seq_append (succ k1) s1 s2
 2. \<lbrakk>Seq s1 (succ k1); Seq s2 (succ k2); Ord k1; Ord k2; \<langle>k1, y1\<rangle> \<^bold>\<in> s1; OrdDom s1; \<langle>k2, y2\<rangle> \<^bold>\<in> s2; OrdDom s2\<rbrakk> \<Longrightarrow> OrdDom (seq_append (succ k1) s1 s2)
[PROOF STEP]
apply (metis Seq_append_pair hadd_succ_left)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Seq s1 (succ k1); Seq s2 (succ k2); Ord k1; Ord k2; \<langle>k1, y1\<rangle> \<^bold>\<in> s1; OrdDom s1; \<langle>k2, y2\<rangle> \<^bold>\<in> s2; OrdDom s2\<rbrakk> \<Longrightarrow> OrdDom (seq_append (succ k1) s1 s2)
[PROOF STEP]
apply (metis Ord_succ Seq_append_OrdDom)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma LstSeq_app [simp]: "LstSeq s k y \<Longrightarrow> app s k = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LstSeq s k y \<Longrightarrow> app s k = y
[PROOF STEP]
by (metis LstSeq_def Seq_imp_eq_app)


[STATEMENT]
lemma BuildSeqI: "LstSeq s k y \<Longrightarrow> (\<And>l. l \<^bold>\<in> succ k \<Longrightarrow> Builds B C s l) \<Longrightarrow> BuildSeq B C s k y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>LstSeq s k y; \<And>l. l \<^bold>\<in> succ k \<Longrightarrow> Builds B C s l\<rbrakk> \<Longrightarrow> BuildSeq B C s k y
[PROOF STEP]
by (simp add: BuildSeq_def)


[STATEMENT]
lemma BuildSeq_imp_LstSeq: "BuildSeq B C s k y \<Longrightarrow> LstSeq s k y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. BuildSeq B C s k y \<Longrightarrow> LstSeq s k y
[PROOF STEP]
by (metis BuildSeq_def)


[STATEMENT]
lemma BuildSeq_imp_Seq: "BuildSeq B C s k y \<Longrightarrow> Seq s (succ k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. BuildSeq B C s k y \<Longrightarrow> Seq s (succ k)
[PROOF STEP]
by (metis LstSeq_imp_Seq_succ BuildSeq_imp_LstSeq)


[STATEMENT]
lemma BuildSeq_conj_distrib:
 "BuildSeq (\<lambda>x. B x \<and> P x) (\<lambda>x y z. C x y z \<and> P x) s k y \<longleftrightarrow>
  BuildSeq B C s k y \<and> (\<forall>l \<^bold>\<in> succ k. P (app s l))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. BuildSeq (\<lambda>x. B x \<and> P x) (\<lambda>x y z. C x y z \<and> P x) s k y = (BuildSeq B C s k y \<and> (\<forall>l\<^bold>\<in>succ k. P (app s l)))
[PROOF STEP]
by (auto simp: BuildSeq_def Builds_def)


[STATEMENT]
lemma BuildSeq_mono:
  assumes y: "BuildSeq B C s k y"
      and B: "\<And>x. B x \<Longrightarrow> B' x" and C: "\<And>x y z. C x y z \<Longrightarrow> C' x y z"
  shows "BuildSeq B' C' s k y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. BuildSeq B' C' s k y
[PROOF STEP]
using y
[PROOF STATE]
proof (prove)
using this:
BuildSeq B C s k y

goal (1 subgoal):
 1. BuildSeq B' C' s k y
[PROOF STEP]
by (auto simp: BuildSeq_def Builds_def intro!: B C)


[STATEMENT]
lemma BuildSeq_trunc:
  assumes b: "BuildSeq B C s k y"
      and l: "l \<^bold>\<in> k"
  shows "BuildSeq B C s l (app s l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. BuildSeq B C s l (app s l)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. BuildSeq B C s l (app s l)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. BuildSeq B C s l (app s l)
[PROOF STEP]
fix j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. BuildSeq B C s l (app s l)
[PROOF STEP]
assume j: "j \<^bold>\<in> succ l"
[PROOF STATE]
proof (state)
this:
j \<^bold>\<in> succ l

goal (1 subgoal):
 1. BuildSeq B C s l (app s l)
[PROOF STEP]
have k: "Ord k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ord k
[PROOF STEP]
by (metis BuildSeq_imp_LstSeq LstSeq_def b)
[PROOF STATE]
proof (state)
this:
Ord k

goal (1 subgoal):
 1. BuildSeq B C s l (app s l)
[PROOF STEP]
hence "Builds B C s j"
[PROOF STATE]
proof (prove)
using this:
Ord k

goal (1 subgoal):
 1. Builds B C s j
[PROOF STEP]
by (metis BuildSeq_def OrdmemD b hballE hsubsetD j l succ_iff)
[PROOF STATE]
proof (state)
this:
Builds B C s j

goal (1 subgoal):
 1. BuildSeq B C s l (app s l)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?j2 \<^bold>\<in> succ l \<Longrightarrow> Builds B C s ?j2

goal (1 subgoal):
 1. BuildSeq B C s l (app s l)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
?j2 \<^bold>\<in> succ l \<Longrightarrow> Builds B C s ?j2

goal (1 subgoal):
 1. BuildSeq B C s l (app s l)
[PROOF STEP]
using b l
[PROOF STATE]
proof (prove)
using this:
?j2 \<^bold>\<in> succ l \<Longrightarrow> Builds B C s ?j2
BuildSeq B C s k y
l \<^bold>\<in> k

goal (1 subgoal):
 1. BuildSeq B C s l (app s l)
[PROOF STEP]
by (auto simp: BuildSeq_def LstSeq_trunc)
[PROOF STATE]
proof (state)
this:
BuildSeq B C s l (app s l)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Builds_insf: "Builds B C s l \<Longrightarrow> LstSeq s k z \<Longrightarrow> l \<^bold>\<in> succ k \<Longrightarrow> Builds B C (insf s (succ k) y) l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Builds B C s l; LstSeq s k z; l \<^bold>\<in> succ k\<rbrakk> \<Longrightarrow> Builds B C (insf s (succ k) y) l
[PROOF STEP]
by (auto simp: HBall_def hmem_not_refl Builds_def app_insf_LstSeq_if simp del: succ_iff)
   (metis hmem_not_sym)