[STATEMENT]
lemma T1_3[semantics]:
    "(w \<Turnstile> \<lparr>F,x,y,z\<rparr>) = (\<exists> r o\<^sub>1 o\<^sub>2 o\<^sub>3 . Some r = d\<^sub>3 F \<and> Some o\<^sub>1 = d\<^sub>\<kappa> x
                                    \<and> Some o\<^sub>2 = d\<^sub>\<kappa> y \<and> Some o\<^sub>3 = d\<^sub>\<kappa> z
                                    \<and> (o\<^sub>1, o\<^sub>2, o\<^sub>3) \<in> ex3 r w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (w \<Turnstile> \<lparr>F,x,y,z\<rparr>) = (\<exists>r o\<^sub>1 o\<^sub>2 o\<^sub>3. Some r = d\<^sub>3 F \<and> Some o\<^sub>1 = d\<^sub>\<kappa> x \<and> Some o\<^sub>2 = d\<^sub>\<kappa> y \<and> Some o\<^sub>3 = d\<^sub>\<kappa> z \<and> (o\<^sub>1, o\<^sub>2, o\<^sub>3) \<in> ex3 r w)
[PROOF STEP]
unfolding semantics_defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (w \<Turnstile> \<lparr>F,x,y,z\<rparr>) = (\<exists>r o\<^sub>1 o\<^sub>2 o\<^sub>3. Some r = map_fun eval\<Pi>\<^sub>3 id Some F \<and> Some o\<^sub>1 = map_fun eval\<kappa> id id x \<and> Some o\<^sub>2 = map_fun eval\<kappa> id id y \<and> Some o\<^sub>3 = map_fun eval\<kappa> id id z \<and> (o\<^sub>1, o\<^sub>2, o\<^sub>3) \<in> {(x, y, z). r (\<nu>\<upsilon> x) (\<nu>\<upsilon> y) (\<nu>\<upsilon> z) dj w})
[PROOF STEP]
apply (simp add: meta_defs meta_aux rep_def proper_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (None \<noteq> eval\<kappa> x \<and> None \<noteq> eval\<kappa> y \<and> None \<noteq> eval\<kappa> z \<and> eval\<Pi>\<^sub>3 F (\<nu>\<upsilon> (the (eval\<kappa> x))) (\<nu>\<upsilon> (the (eval\<kappa> y))) (\<nu>\<upsilon> (the (eval\<kappa> z))) dj w) = (\<exists>o\<^sub>1. Some o\<^sub>1 = eval\<kappa> x \<and> (\<exists>o\<^sub>2. Some o\<^sub>2 = eval\<kappa> y \<and> (\<exists>o\<^sub>3. Some o\<^sub>3 = eval\<kappa> z \<and> eval\<Pi>\<^sub>3 F (\<nu>\<upsilon> o\<^sub>1) (\<nu>\<upsilon> o\<^sub>2) (\<nu>\<upsilon> o\<^sub>3) dj w)))
[PROOF STEP]
by (metis option.discI option.exhaust option.sel)


[STATEMENT]
lemma T3[semantics]:
    "(w \<Turnstile> \<lparr>F\<rparr>) = (\<exists> r . Some r = d\<^sub>0 F \<and> ex0 r w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (w \<Turnstile> \<lparr>F\<rparr>) = (\<exists>r. Some r = d\<^sub>0 F \<and> ex0 r w)
[PROOF STEP]
unfolding semantics_defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (w \<Turnstile> \<lparr>F\<rparr>) = (\<exists>r. Some r = map_fun eval\<o> id Some F \<and> r dj w)
[PROOF STEP]
by (simp add: meta_defs meta_aux)


[STATEMENT]
lemma T2[semantics]:
    "(w \<Turnstile> \<lbrace>x,F\<rbrace>) = (\<exists> r o\<^sub>1 . Some r = d\<^sub>1 F \<and> Some o\<^sub>1 = d\<^sub>\<kappa> x \<and> o\<^sub>1 \<in> en r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (w \<Turnstile> \<lbrace>x,F\<rbrace>) = (\<exists>r o\<^sub>1. Some r = d\<^sub>1 F \<and> Some o\<^sub>1 = d\<^sub>\<kappa> x \<and> o\<^sub>1 \<in> en r)
[PROOF STEP]
unfolding semantics_defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (w \<Turnstile> \<lbrace>x,F\<rbrace>) = (\<exists>r o\<^sub>1. Some r = map_fun eval\<Pi>\<^sub>1 id Some F \<and> Some o\<^sub>1 = map_fun eval\<kappa> id id x \<and> o\<^sub>1 \<in> Collect (case_\<nu> (\<lambda>\<omega>. False) ((\<in>) (make\<Pi>\<^sub>1 r))))
[PROOF STEP]
apply (simp add: meta_defs meta_aux rep_def proper_def split: \<nu>.split)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<exists>x1. the (eval\<kappa> x) = \<omega>\<nu> x1) \<longrightarrow> (\<forall>x2. Some (\<alpha>\<nu> x2) = eval\<kappa> x \<longrightarrow> F \<notin> x2)) \<and> (\<forall>x2. the (eval\<kappa> x) = \<alpha>\<nu> x2 \<longrightarrow> (None \<noteq> eval\<kappa> x \<and> F \<in> x2) = (\<exists>o\<^sub>1. (\<forall>x1. o\<^sub>1 \<noteq> \<omega>\<nu> x1) \<and> (\<forall>x2. o\<^sub>1 = \<alpha>\<nu> x2 \<longrightarrow> Some (\<alpha>\<nu> x2) = eval\<kappa> x \<and> F \<in> x2)))
[PROOF STEP]
by (metis \<nu>.exhaust \<nu>.inject(2) \<nu>.simps(4) \<nu>\<kappa>.rep_eq option.collapse
              option.discI rep.rep_eq rep_proper_id)


[STATEMENT]
lemma T4[semantics]: "(w \<Turnstile> \<^bold>\<not>\<psi>) = (\<not>(w \<Turnstile> \<psi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (w \<Turnstile> \<^bold>\<not>\<psi>) = (\<not> (w \<Turnstile> \<psi>))
[PROOF STEP]
by (simp add: meta_defs meta_aux)


[STATEMENT]
lemma T5[semantics]: "(w \<Turnstile> \<psi> \<^bold>\<rightarrow> \<chi>) = (\<not>(w \<Turnstile> \<psi>) \<or> (w \<Turnstile> \<chi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (w \<Turnstile> \<psi> \<^bold>\<rightarrow> \<chi>) = (\<not> (w \<Turnstile> \<psi>) \<or> (w \<Turnstile> \<chi>))
[PROOF STEP]
by (simp add: meta_defs meta_aux)


[STATEMENT]
lemma T6[semantics]: "(w \<Turnstile> \<^bold>\<box>\<psi>) = (\<forall> v . (v \<Turnstile> \<psi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (w \<Turnstile> \<^bold>\<box>\<psi>) = (\<forall>v. (v \<Turnstile> \<psi>))
[PROOF STEP]
by (simp add: meta_defs meta_aux)


[STATEMENT]
lemma T7[semantics]: "(w \<Turnstile> \<^bold>\<A>\<psi>) = (dw \<Turnstile> \<psi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (w \<Turnstile> \<^bold>\<A>\<psi>) = (dw \<Turnstile> \<psi>)
[PROOF STEP]
by (simp add: meta_defs meta_aux)


[STATEMENT]
lemma T8_\<nu>[semantics]: "(w \<Turnstile> \<^bold>\<forall>\<^sub>\<nu> x. \<psi> x) = (\<forall> x . (w \<Turnstile> \<psi> x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (w \<Turnstile> \<^bold>\<forall>\<^sub>\<nu>x. \<psi> x) = (\<forall>x. (w \<Turnstile> \<psi> x))
[PROOF STEP]
by (simp add: meta_defs meta_aux)


[STATEMENT]
lemma T8_0[semantics]: "(w \<Turnstile> \<^bold>\<forall>\<^sub>0 x. \<psi> x) = (\<forall> x . (w \<Turnstile> \<psi> x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (w \<Turnstile> \<^bold>\<forall>\<^sub>0x. \<psi> x) = (\<forall>x. (w \<Turnstile> \<psi> x))
[PROOF STEP]
by (simp add: meta_defs meta_aux)


[STATEMENT]
lemma T8_1[semantics]: "(w \<Turnstile> \<^bold>\<forall>\<^sub>1 x. \<psi> x) = (\<forall> x . (w \<Turnstile> \<psi> x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (w \<Turnstile> \<^bold>\<forall>\<^sub>1x. \<psi> x) = (\<forall>x. (w \<Turnstile> \<psi> x))
[PROOF STEP]
by (simp add: meta_defs meta_aux)


[STATEMENT]
lemma T8_2[semantics]: "(w \<Turnstile> \<^bold>\<forall>\<^sub>2 x. \<psi> x) = (\<forall> x . (w \<Turnstile> \<psi> x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (w \<Turnstile> \<^bold>\<forall>\<^sub>2x. \<psi> x) = (\<forall>x. (w \<Turnstile> \<psi> x))
[PROOF STEP]
by (simp add: meta_defs meta_aux)


[STATEMENT]
lemma T8_3[semantics]: "(w \<Turnstile> \<^bold>\<forall>\<^sub>3 x. \<psi> x) = (\<forall> x . (w \<Turnstile> \<psi> x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (w \<Turnstile> \<^bold>\<forall>\<^sub>3x. \<psi> x) = (\<forall>x. (w \<Turnstile> \<psi> x))
[PROOF STEP]
by (simp add: meta_defs meta_aux)


[STATEMENT]
lemma T8_\<o>[semantics]: "(w \<Turnstile> \<^bold>\<forall>\<^sub>\<o> x. \<psi> x) = (\<forall> x . (w \<Turnstile> \<psi> x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (w \<Turnstile> \<^bold>\<forall>\<^sub>\<o>x. \<psi> x) = (\<forall>x. (w \<Turnstile> \<psi> x))
[PROOF STEP]
by (simp add: meta_defs meta_aux)


[STATEMENT]
lemma D3[semantics]:
    "d\<^sub>\<kappa> (\<^bold>\<iota>x . \<psi> x) = (if (\<exists>x . (w\<^sub>0 \<Turnstile> \<psi> x) \<and> (\<forall> y . (w\<^sub>0  \<Turnstile> \<psi> y) \<longrightarrow> y = x))
                      then (Some (THE x . (w\<^sub>0 \<Turnstile> \<psi> x))) else None)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d\<^sub>\<kappa> (\<^bold>\<iota>x. \<psi> x) = (if \<exists>x. (w\<^sub>0 \<Turnstile> \<psi> x) \<and> (\<forall>y. (w\<^sub>0 \<Turnstile> \<psi> y) \<longrightarrow> y = x) then Some (THE x. (w\<^sub>0 \<Turnstile> \<psi> x)) else None)
[PROOF STEP]
unfolding semantics_defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_fun eval\<kappa> id id (\<^bold>\<iota>x. \<psi> x) = (if \<exists>x. (dw \<Turnstile> \<psi> x) \<and> (\<forall>y. (dw \<Turnstile> \<psi> y) \<longrightarrow> y = x) then Some (THE x. (dw \<Turnstile> \<psi> x)) else None)
[PROOF STEP]
by (auto simp: meta_defs meta_aux)


[STATEMENT]
lemma D4_1[semantics]: "d\<^sub>1 (\<^bold>\<lambda> x . \<lparr>F, x\<^sup>P\<rparr>) = d\<^sub>1 F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d\<^sub>1 (\<^bold>\<lambda>x. \<lparr>F,x\<^sup>P\<rparr>) = d\<^sub>1 F
[PROOF STEP]
by (simp add: meta_defs meta_aux)


[STATEMENT]
lemma D4_2[semantics]: "d\<^sub>2 (\<^bold>\<lambda>\<^sup>2 (\<lambda> x y . \<lparr>F, x\<^sup>P, y\<^sup>P\<rparr>)) = d\<^sub>2 F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d\<^sub>2 (\<^bold>\<lambda>\<^sup>2 (\<lambda>x y. \<lparr>F,x\<^sup>P,y\<^sup>P\<rparr>)) = d\<^sub>2 F
[PROOF STEP]
by (simp add: meta_defs meta_aux)


[STATEMENT]
lemma D4_3[semantics]: "d\<^sub>3 (\<^bold>\<lambda>\<^sup>3 (\<lambda> x y z . \<lparr>F, x\<^sup>P, y\<^sup>P, z\<^sup>P\<rparr>)) = d\<^sub>3 F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d\<^sub>3 (\<^bold>\<lambda>\<^sup>3 (\<lambda>x y z. \<lparr>F,x\<^sup>P,y\<^sup>P,z\<^sup>P\<rparr>)) = d\<^sub>3 F
[PROOF STEP]
by (simp add: meta_defs meta_aux)


[STATEMENT]
lemma D5_1[semantics]:
    assumes "IsProperInX \<phi>"
    shows "\<And> w o\<^sub>1 r . Some r = d\<^sub>1 (\<^bold>\<lambda> x . (\<phi> (x\<^sup>P))) \<and> Some o\<^sub>1 = d\<^sub>\<kappa> x
                      \<longrightarrow> (o\<^sub>1 \<in> ex1 r w) = (w \<Turnstile> \<phi> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>w o\<^sub>1 r. Some r = d\<^sub>1 (\<^bold>\<lambda>x. \<phi> (x\<^sup>P)) \<and> Some o\<^sub>1 = d\<^sub>\<kappa> x \<longrightarrow> (o\<^sub>1 \<in> ex1 r w) = (w \<Turnstile> \<phi> x)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
IsProperInX \<phi>

goal (1 subgoal):
 1. \<And>w o\<^sub>1 r. Some r = d\<^sub>1 (\<^bold>\<lambda>x. \<phi> (x\<^sup>P)) \<and> Some o\<^sub>1 = d\<^sub>\<kappa> x \<longrightarrow> (o\<^sub>1 \<in> ex1 r w) = (w \<Turnstile> \<phi> x)
[PROOF STEP]
unfolding IsProperInX_def semantics_defs
[PROOF STATE]
proof (prove)
using this:
map_fun (map_fun id eval\<o>) id (\<lambda>\<phi>. \<forall>x v. (\<exists>a. \<nu>\<upsilon> a = \<nu>\<upsilon> x \<and> \<phi> (a\<^sup>P) dj v) = \<phi> (x\<^sup>P) dj v) \<phi>

goal (1 subgoal):
 1. \<And>w o\<^sub>1 r. Some r = map_fun eval\<Pi>\<^sub>1 id Some (\<^bold>\<lambda>x. \<phi> (x\<^sup>P)) \<and> Some o\<^sub>1 = map_fun eval\<kappa> id id x \<longrightarrow> (o\<^sub>1 \<in> {x. r (\<nu>\<upsilon> x) dj w}) = (w \<Turnstile> \<phi> x)
[PROOF STEP]
by (auto simp: meta_defs meta_aux rep_def proper_def \<nu>\<kappa>.abs_eq)


[STATEMENT]
lemma D5_2[semantics]:
    assumes "IsProperInXY \<phi>"
    shows "\<And> w o\<^sub>1 o\<^sub>2 r . Some r = d\<^sub>2 (\<^bold>\<lambda>\<^sup>2 (\<lambda> x y . \<phi> (x\<^sup>P) (y\<^sup>P)))
                       \<and> Some o\<^sub>1 = d\<^sub>\<kappa> x \<and> Some o\<^sub>2 = d\<^sub>\<kappa> y
                       \<longrightarrow> ((o\<^sub>1,o\<^sub>2) \<in> ex2 r w) = (w \<Turnstile> \<phi> x y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>w o\<^sub>1 o\<^sub>2 r. Some r = d\<^sub>2 (\<^bold>\<lambda>\<^sup>2 (\<lambda>x y. \<phi> (x\<^sup>P) (y\<^sup>P))) \<and> Some o\<^sub>1 = d\<^sub>\<kappa> x \<and> Some o\<^sub>2 = d\<^sub>\<kappa> y \<longrightarrow> ((o\<^sub>1, o\<^sub>2) \<in> ex2 r w) = (w \<Turnstile> \<phi> x y)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
IsProperInXY \<phi>

goal (1 subgoal):
 1. \<And>w o\<^sub>1 o\<^sub>2 r. Some r = d\<^sub>2 (\<^bold>\<lambda>\<^sup>2 (\<lambda>x y. \<phi> (x\<^sup>P) (y\<^sup>P))) \<and> Some o\<^sub>1 = d\<^sub>\<kappa> x \<and> Some o\<^sub>2 = d\<^sub>\<kappa> y \<longrightarrow> ((o\<^sub>1, o\<^sub>2) \<in> ex2 r w) = (w \<Turnstile> \<phi> x y)
[PROOF STEP]
unfolding IsProperInXY_def semantics_defs
[PROOF STATE]
proof (prove)
using this:
map_fun (map_fun id (map_fun id eval\<o>)) id (\<lambda>\<phi>. \<forall>x y v. (\<exists>a b. \<nu>\<upsilon> a = \<nu>\<upsilon> x \<and> \<nu>\<upsilon> b = \<nu>\<upsilon> y \<and> \<phi> (a\<^sup>P) (b\<^sup>P) dj v) = \<phi> (x\<^sup>P) (y\<^sup>P) dj v) \<phi>

goal (1 subgoal):
 1. \<And>w o\<^sub>1 o\<^sub>2 r. Some r = map_fun eval\<Pi>\<^sub>2 id Some (\<^bold>\<lambda>\<^sup>2 (\<lambda>x y. \<phi> (x\<^sup>P) (y\<^sup>P))) \<and> Some o\<^sub>1 = map_fun eval\<kappa> id id x \<and> Some o\<^sub>2 = map_fun eval\<kappa> id id y \<longrightarrow> ((o\<^sub>1, o\<^sub>2) \<in> {(x, y). r (\<nu>\<upsilon> x) (\<nu>\<upsilon> y) dj w}) = (w \<Turnstile> \<phi> x y)
[PROOF STEP]
by (auto simp: meta_defs meta_aux rep_def proper_def \<nu>\<kappa>.abs_eq)


[STATEMENT]
lemma D5_3[semantics]:
    assumes "IsProperInXYZ \<phi>"
    shows "\<And> w o\<^sub>1 o\<^sub>2 o\<^sub>3 r . Some r = d\<^sub>3 (\<^bold>\<lambda>\<^sup>3 (\<lambda> x y z . \<phi> (x\<^sup>P) (y\<^sup>P) (z\<^sup>P)))
                          \<and> Some o\<^sub>1 = d\<^sub>\<kappa> x \<and> Some o\<^sub>2 = d\<^sub>\<kappa> y \<and> Some o\<^sub>3 = d\<^sub>\<kappa> z
                          \<longrightarrow> ((o\<^sub>1,o\<^sub>2,o\<^sub>3) \<in> ex3 r w) = (w \<Turnstile> \<phi> x y z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>w o\<^sub>1 o\<^sub>2 o\<^sub>3 r. Some r = d\<^sub>3 (\<^bold>\<lambda>\<^sup>3 (\<lambda>x y z. \<phi> (x\<^sup>P) (y\<^sup>P) (z\<^sup>P))) \<and> Some o\<^sub>1 = d\<^sub>\<kappa> x \<and> Some o\<^sub>2 = d\<^sub>\<kappa> y \<and> Some o\<^sub>3 = d\<^sub>\<kappa> z \<longrightarrow> ((o\<^sub>1, o\<^sub>2, o\<^sub>3) \<in> ex3 r w) = (w \<Turnstile> \<phi> x y z)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
IsProperInXYZ \<phi>

goal (1 subgoal):
 1. \<And>w o\<^sub>1 o\<^sub>2 o\<^sub>3 r. Some r = d\<^sub>3 (\<^bold>\<lambda>\<^sup>3 (\<lambda>x y z. \<phi> (x\<^sup>P) (y\<^sup>P) (z\<^sup>P))) \<and> Some o\<^sub>1 = d\<^sub>\<kappa> x \<and> Some o\<^sub>2 = d\<^sub>\<kappa> y \<and> Some o\<^sub>3 = d\<^sub>\<kappa> z \<longrightarrow> ((o\<^sub>1, o\<^sub>2, o\<^sub>3) \<in> ex3 r w) = (w \<Turnstile> \<phi> x y z)
[PROOF STEP]
unfolding IsProperInXYZ_def semantics_defs
[PROOF STATE]
proof (prove)
using this:
map_fun (map_fun id (map_fun id (map_fun id eval\<o>))) id (\<lambda>\<phi>. \<forall>x y z v. (\<exists>a b c. \<nu>\<upsilon> a = \<nu>\<upsilon> x \<and> \<nu>\<upsilon> b = \<nu>\<upsilon> y \<and> \<nu>\<upsilon> c = \<nu>\<upsilon> z \<and> \<phi> (a\<^sup>P) (b\<^sup>P) (c\<^sup>P) dj v) = \<phi> (x\<^sup>P) (y\<^sup>P) (z\<^sup>P) dj v) \<phi>

goal (1 subgoal):
 1. \<And>w o\<^sub>1 o\<^sub>2 o\<^sub>3 r. Some r = map_fun eval\<Pi>\<^sub>3 id Some (\<^bold>\<lambda>\<^sup>3 (\<lambda>x y z. \<phi> (x\<^sup>P) (y\<^sup>P) (z\<^sup>P))) \<and> Some o\<^sub>1 = map_fun eval\<kappa> id id x \<and> Some o\<^sub>2 = map_fun eval\<kappa> id id y \<and> Some o\<^sub>3 = map_fun eval\<kappa> id id z \<longrightarrow> ((o\<^sub>1, o\<^sub>2, o\<^sub>3) \<in> {(x, y, z). r (\<nu>\<upsilon> x) (\<nu>\<upsilon> y) (\<nu>\<upsilon> z) dj w}) = (w \<Turnstile> \<phi> x y z)
[PROOF STEP]
by (auto simp: meta_defs meta_aux rep_def proper_def \<nu>\<kappa>.abs_eq)


[STATEMENT]
lemma D6[semantics]: "(\<And> w r . Some r = d\<^sub>0 (\<^bold>\<lambda>\<^sup>0 \<phi>) \<longrightarrow> ex0 r w = (w \<Turnstile> \<phi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>w r. Some r = d\<^sub>0 (\<^bold>\<lambda>\<^sup>0 \<phi>) \<longrightarrow> ex0 r w = (w \<Turnstile> \<phi>)
[PROOF STEP]
by (auto simp: meta_defs meta_aux semantics_defs)


[STATEMENT]
lemma propex\<^sub>0: "\<exists> r . Some r = d\<^sub>0 F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>r. Some r = d\<^sub>0 F
[PROOF STEP]
unfolding d\<^sub>0_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>r. Some r = map_fun eval\<o> id Some F
[PROOF STEP]
by simp


[STATEMENT]
lemma propex\<^sub>1: "\<exists> r . Some r = d\<^sub>1 F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>r. Some r = d\<^sub>1 F
[PROOF STEP]
unfolding d\<^sub>1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>r. Some r = map_fun eval\<Pi>\<^sub>1 id Some F
[PROOF STEP]
by simp


[STATEMENT]
lemma propex\<^sub>2: "\<exists> r . Some r = d\<^sub>2 F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>r. Some r = d\<^sub>2 F
[PROOF STEP]
unfolding d\<^sub>2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>r. Some r = map_fun eval\<Pi>\<^sub>2 id Some F
[PROOF STEP]
by simp


[STATEMENT]
lemma propex\<^sub>3: "\<exists> r . Some r = d\<^sub>3 F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>r. Some r = d\<^sub>3 F
[PROOF STEP]
unfolding d\<^sub>3_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>r. Some r = map_fun eval\<Pi>\<^sub>3 id Some F
[PROOF STEP]
by simp


[STATEMENT]
lemma d\<^sub>\<kappa>_proper: "d\<^sub>\<kappa> (u\<^sup>P) = Some u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d\<^sub>\<kappa> (u\<^sup>P) = Some u
[PROOF STEP]
unfolding d\<^sub>\<kappa>_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_fun eval\<kappa> id id (u\<^sup>P) = Some u
[PROOF STEP]
by (simp add: \<nu>\<kappa>_def meta_aux)


[STATEMENT]
lemma ConcretenessSemantics1:
    "Some r = d\<^sub>1 E! \<Longrightarrow> (\<exists> w . \<omega>\<nu> x \<in> ex1 r w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Some r = d\<^sub>1 E! \<Longrightarrow> \<exists>w. \<omega>\<nu> x \<in> ex1 r w
[PROOF STEP]
unfolding semantics_defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Some r = map_fun eval\<Pi>\<^sub>1 id Some E! \<Longrightarrow> \<exists>w. \<omega>\<nu> x \<in> {x. r (\<nu>\<upsilon> x) dj w}
[PROOF STEP]
apply transfer
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r x. Some r = map_fun (\<lambda>x. x) id Some (\<lambda>u s w. case u of \<omega>\<upsilon> x \<Rightarrow> ConcreteInWorld x w | \<sigma>\<upsilon> \<sigma> \<Rightarrow> False) \<Longrightarrow> \<exists>w. \<omega>\<nu> x \<in> {x. r (\<nu>\<upsilon> x) dj w}
[PROOF STEP]
by (simp add: OrdinaryObjectsPossiblyConcreteAxiom \<nu>\<upsilon>_\<omega>\<nu>_is_\<omega>\<upsilon>)


[STATEMENT]
lemma ConcretenessSemantics2:
    "Some r = d\<^sub>1 E! \<Longrightarrow> (x \<in> ex1 r w \<longrightarrow> (\<exists>y. x = \<omega>\<nu> y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Some r = d\<^sub>1 E! \<Longrightarrow> x \<in> ex1 r w \<longrightarrow> (\<exists>y. x = \<omega>\<nu> y)
[PROOF STEP]
unfolding semantics_defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Some r = map_fun eval\<Pi>\<^sub>1 id Some E! \<Longrightarrow> x \<in> {x. r (\<nu>\<upsilon> x) dj w} \<longrightarrow> (\<exists>y. x = \<omega>\<nu> y)
[PROOF STEP]
apply transfer
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r x w. Some r = map_fun (\<lambda>x. x) id Some (\<lambda>u s w. case u of \<omega>\<upsilon> x \<Rightarrow> ConcreteInWorld x w | \<sigma>\<upsilon> \<sigma> \<Rightarrow> False) \<Longrightarrow> x \<in> {x. r (\<nu>\<upsilon> x) dj w} \<longrightarrow> (\<exists>y. x = \<omega>\<nu> y)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r x w. r = (\<lambda>u s w. case u of \<omega>\<upsilon> x \<Rightarrow> ConcreteInWorld x w | \<sigma>\<upsilon> \<sigma> \<Rightarrow> False) \<Longrightarrow> (case \<nu>\<upsilon> x of \<omega>\<upsilon> x \<Rightarrow> ConcreteInWorld x w | \<sigma>\<upsilon> \<sigma> \<Rightarrow> False) \<longrightarrow> (\<exists>y. x = \<omega>\<nu> y)
[PROOF STEP]
by (metis \<nu>.exhaust \<upsilon>.exhaust \<upsilon>.simps(6) no_\<alpha>\<omega>)


[STATEMENT]
lemma d\<^sub>0_inject: "\<And>x y. d\<^sub>0 x = d\<^sub>0 y \<Longrightarrow> x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. d\<^sub>0 x = d\<^sub>0 y \<Longrightarrow> x = y
[PROOF STEP]
unfolding d\<^sub>0_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. map_fun eval\<o> id Some x = map_fun eval\<o> id Some y \<Longrightarrow> x = y
[PROOF STEP]
by (simp add: eval\<o>_inject)


[STATEMENT]
lemma d\<^sub>2_inject: "\<And>x y. d\<^sub>2 x = d\<^sub>2 y \<Longrightarrow> x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. d\<^sub>2 x = d\<^sub>2 y \<Longrightarrow> x = y
[PROOF STEP]
unfolding d\<^sub>2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. map_fun eval\<Pi>\<^sub>2 id Some x = map_fun eval\<Pi>\<^sub>2 id Some y \<Longrightarrow> x = y
[PROOF STEP]
by (simp add: eval\<Pi>\<^sub>2_inject)


[STATEMENT]
lemma d\<^sub>3_inject: "\<And>x y. d\<^sub>3 x = d\<^sub>3 y \<Longrightarrow> x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. d\<^sub>3 x = d\<^sub>3 y \<Longrightarrow> x = y
[PROOF STEP]
unfolding d\<^sub>3_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. map_fun eval\<Pi>\<^sub>3 id Some x = map_fun eval\<Pi>\<^sub>3 id Some y \<Longrightarrow> x = y
[PROOF STEP]
by (simp add: eval\<Pi>\<^sub>3_inject)


[STATEMENT]
lemma d\<^sub>\<kappa>_inject: "\<And>x y o\<^sub>1. Some o\<^sub>1 = d\<^sub>\<kappa> x \<and> Some o\<^sub>1 = d\<^sub>\<kappa> y \<Longrightarrow> x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y o\<^sub>1. Some o\<^sub>1 = d\<^sub>\<kappa> x \<and> Some o\<^sub>1 = d\<^sub>\<kappa> y \<Longrightarrow> x = y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y o\<^sub>1. Some o\<^sub>1 = d\<^sub>\<kappa> x \<and> Some o\<^sub>1 = d\<^sub>\<kappa> y \<Longrightarrow> x = y
[PROOF STEP]
fix x :: \<kappa> and y :: \<kappa> and o\<^sub>1 :: \<nu>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y o\<^sub>1. Some o\<^sub>1 = d\<^sub>\<kappa> x \<and> Some o\<^sub>1 = d\<^sub>\<kappa> y \<Longrightarrow> x = y
[PROOF STEP]
assume "Some o\<^sub>1 = d\<^sub>\<kappa> x \<and> Some o\<^sub>1 = d\<^sub>\<kappa> y"
[PROOF STATE]
proof (state)
this:
Some o\<^sub>1 = d\<^sub>\<kappa> x \<and> Some o\<^sub>1 = d\<^sub>\<kappa> y

goal (1 subgoal):
 1. \<And>x y o\<^sub>1. Some o\<^sub>1 = d\<^sub>\<kappa> x \<and> Some o\<^sub>1 = d\<^sub>\<kappa> y \<Longrightarrow> x = y
[PROOF STEP]
thus "x = y"
[PROOF STATE]
proof (prove)
using this:
Some o\<^sub>1 = d\<^sub>\<kappa> x \<and> Some o\<^sub>1 = d\<^sub>\<kappa> y

goal (1 subgoal):
 1. x = y
[PROOF STEP]
apply transfer
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>o\<^sub>1 x y. Some o\<^sub>1 = id x \<and> Some o\<^sub>1 = id y \<Longrightarrow> x = y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x = y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma IsProperInX_intro[IsProper_intros]:
  "IsProperInX (\<lambda> x . \<chi>
    \<comment> \<open>one place:\<close> (\<lambda> F . \<lparr>F,x\<rparr>)
    \<comment> \<open>two place:\<close> (\<lambda> F . \<lparr>F,x,x\<rparr>) (\<lambda> F a . \<lparr>F,x,a\<rparr>) (\<lambda> F a . \<lparr>F,a,x\<rparr>)
    \<comment> \<open>three place three \<open>x\<close>:\<close> (\<lambda> F . \<lparr>F,x,x,x\<rparr>)
    \<comment> \<open>three place two \<open>x\<close>:\<close> (\<lambda> F a . \<lparr>F,x,x,a\<rparr>) (\<lambda> F a . \<lparr>F,x,a,x\<rparr>)
                            (\<lambda> F a . \<lparr>F,a,x,x\<rparr>)
    \<comment> \<open>three place one \<open>x\<close>:\<close> (\<lambda> F a b. \<lparr>F,x,a,b\<rparr>) (\<lambda> F a b. \<lparr>F,a,x,b\<rparr>)
                            (\<lambda> F a b . \<lparr>F,a,b,x\<rparr>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. IsProperInX (\<lambda>x. \<chi> (\<lambda>F. \<lparr>F,x\<rparr>) (\<lambda>F. \<lparr>F,x,x\<rparr>) (\<lambda>F. exe2 F x) (\<lambda>F a. \<lparr>F,a,x\<rparr>) (\<lambda>F. \<lparr>F,x,x,x\<rparr>) (\<lambda>F. exe3 F x x) (\<lambda>F a. \<lparr>F,x,a,x\<rparr>) (\<lambda>F a. \<lparr>F,a,x,x\<rparr>) (\<lambda>F. exe3 F x) (\<lambda>F a. exe3 F a x) (\<lambda>F a b. \<lparr>F,a,b,x\<rparr>))
[PROOF STEP]
unfolding IsProperInX_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_fun (map_fun id eval\<o>) id (\<lambda>\<phi>. \<forall>x v. (\<exists>a. \<nu>\<upsilon> a = \<nu>\<upsilon> x \<and> \<phi> (a\<^sup>P) dj v) = \<phi> (x\<^sup>P) dj v) (\<lambda>x. \<chi> (\<lambda>F. \<lparr>F,x\<rparr>) (\<lambda>F. \<lparr>F,x,x\<rparr>) (\<lambda>F. exe2 F x) (\<lambda>F a. \<lparr>F,a,x\<rparr>) (\<lambda>F. \<lparr>F,x,x,x\<rparr>) (\<lambda>F. exe3 F x x) (\<lambda>F a. \<lparr>F,x,a,x\<rparr>) (\<lambda>F a. \<lparr>F,a,x,x\<rparr>) (\<lambda>F. exe3 F x) (\<lambda>F a. exe3 F a x) (\<lambda>F a b. \<lparr>F,a,b,x\<rparr>))
[PROOF STEP]
by (auto simp: meta_defs meta_aux)


[STATEMENT]
lemma IsProperInXY_intro[IsProper_intros]:
  "IsProperInXY (\<lambda> x y . \<chi>
    \<comment> \<open>only \<open>x\<close>\<close>
      \<comment> \<open>one place:\<close> (\<lambda> F . \<lparr>F,x\<rparr>)
      \<comment> \<open>two place:\<close> (\<lambda> F . \<lparr>F,x,x\<rparr>) (\<lambda> F a . \<lparr>F,x,a\<rparr>) (\<lambda> F a . \<lparr>F,a,x\<rparr>)
      \<comment> \<open>three place three \<open>x\<close>:\<close> (\<lambda> F . \<lparr>F,x,x,x\<rparr>)
      \<comment> \<open>three place two \<open>x\<close>:\<close> (\<lambda> F a . \<lparr>F,x,x,a\<rparr>) (\<lambda> F a . \<lparr>F,x,a,x\<rparr>)
                              (\<lambda> F a . \<lparr>F,a,x,x\<rparr>)
      \<comment> \<open>three place one \<open>x\<close>:\<close> (\<lambda> F a b. \<lparr>F,x,a,b\<rparr>) (\<lambda> F a b. \<lparr>F,a,x,b\<rparr>)
                              (\<lambda> F a b . \<lparr>F,a,b,x\<rparr>)
    \<comment> \<open>only \<open>y\<close>\<close>
      \<comment> \<open>one place:\<close> (\<lambda> F . \<lparr>F,y\<rparr>)
      \<comment> \<open>two place:\<close> (\<lambda> F . \<lparr>F,y,y\<rparr>) (\<lambda> F a . \<lparr>F,y,a\<rparr>) (\<lambda> F a . \<lparr>F,a,y\<rparr>)
      \<comment> \<open>three place three \<open>y\<close>:\<close> (\<lambda> F . \<lparr>F,y,y,y\<rparr>)
      \<comment> \<open>three place two \<open>y\<close>:\<close> (\<lambda> F a . \<lparr>F,y,y,a\<rparr>) (\<lambda> F a . \<lparr>F,y,a,y\<rparr>)
                              (\<lambda> F a . \<lparr>F,a,y,y\<rparr>)
      \<comment> \<open>three place one \<open>y\<close>:\<close> (\<lambda> F a b. \<lparr>F,y,a,b\<rparr>) (\<lambda> F a b. \<lparr>F,a,y,b\<rparr>)
                              (\<lambda> F a b . \<lparr>F,a,b,y\<rparr>)
    \<comment> \<open>\<open>x\<close> and \<open>y\<close>\<close>
      \<comment> \<open>two place:\<close> (\<lambda> F . \<lparr>F,x,y\<rparr>) (\<lambda> F . \<lparr>F,y,x\<rparr>)
      \<comment> \<open>three place \<open>(x,y)\<close>:\<close> (\<lambda> F a . \<lparr>F,x,y,a\<rparr>) (\<lambda> F a . \<lparr>F,x,a,y\<rparr>)
                              (\<lambda> F a . \<lparr>F,a,x,y\<rparr>)
      \<comment> \<open>three place \<open>(y,x)\<close>:\<close> (\<lambda> F a . \<lparr>F,y,x,a\<rparr>) (\<lambda> F a . \<lparr>F,y,a,x\<rparr>)
                              (\<lambda> F a . \<lparr>F,a,y,x\<rparr>)
      \<comment> \<open>three place \<open>(x,x,y)\<close>:\<close> (\<lambda> F . \<lparr>F,x,x,y\<rparr>) (\<lambda> F . \<lparr>F,x,y,x\<rparr>)
                                (\<lambda> F . \<lparr>F,y,x,x\<rparr>)
      \<comment> \<open>three place \<open>(x,y,y)\<close>:\<close> (\<lambda> F . \<lparr>F,x,y,y\<rparr>) (\<lambda> F . \<lparr>F,y,x,y\<rparr>)
                                (\<lambda> F . \<lparr>F,y,y,x\<rparr>)
      \<comment> \<open>three place \<open>(x,x,x)\<close>:\<close> (\<lambda> F . \<lparr>F,x,x,x\<rparr>)
      \<comment> \<open>three place \<open>(y,y,y)\<close>:\<close> (\<lambda> F . \<lparr>F,y,y,y\<rparr>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. IsProperInXY (\<lambda>x y. \<chi> (\<lambda>F. \<lparr>F,x\<rparr>) (\<lambda>F. \<lparr>F,x,x\<rparr>) (\<lambda>F. exe2 F x) (\<lambda>F a. \<lparr>F,a,x\<rparr>) (\<lambda>F. \<lparr>F,x,x,x\<rparr>) (\<lambda>F. exe3 F x x) (\<lambda>F a. \<lparr>F,x,a,x\<rparr>) (\<lambda>F a. \<lparr>F,a,x,x\<rparr>) (\<lambda>F. exe3 F x) (\<lambda>F a. exe3 F a x) (\<lambda>F a b. \<lparr>F,a,b,x\<rparr>) (\<lambda>F. \<lparr>F,y\<rparr>) (\<lambda>F. \<lparr>F,y,y\<rparr>) (\<lambda>F. exe2 F y) (\<lambda>F a. \<lparr>F,a,y\<rparr>) (\<lambda>F. \<lparr>F,y,y,y\<rparr>) (\<lambda>F. exe3 F y y) (\<lambda>F a. \<lparr>F,y,a,y\<rparr>) (\<lambda>F a. \<lparr>F,a,y,y\<rparr>) (\<lambda>F. exe3 F y) (\<lambda>F a. exe3 F a y) (\<lambda>F a b. \<lparr>F,a,b,y\<rparr>) (\<lambda>F. \<lparr>F,x,y\<rparr>) (\<lambda>F. \<lparr>F,y,x\<rparr>) (\<lambda>F. exe3 F x y) (\<lambda>F a. \<lparr>F,x,a,y\<rparr>) (\<lambda>F a. \<lparr>F,a,x,y\<rparr>) (\<lambda>F. exe3 F y x) (\<lambda>F a. \<lparr>F,y,a,x\<rparr>) (\<lambda>F a. \<lparr>F,a,y,x\<rparr>) (\<lambda>F. \<lparr>F,x,x,y\<rparr>) (\<lambda>F. \<lparr>F,x,y,x\<rparr>) (\<lambda>F. \<lparr>F,y,x,x\<rparr>) (\<lambda>F. \<lparr>F,x,y,y\<rparr>) (\<lambda>F. \<lparr>F,y,x,y\<rparr>) (\<lambda>F. \<lparr>F,y,y,x\<rparr>) (\<lambda>F. \<lparr>F,x,x,x\<rparr>) (\<lambda>F. \<lparr>F,y,y,y\<rparr>))
[PROOF STEP]
unfolding IsProperInXY_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_fun (map_fun id (map_fun id eval\<o>)) id (\<lambda>\<phi>. \<forall>x y v. (\<exists>a b. \<nu>\<upsilon> a = \<nu>\<upsilon> x \<and> \<nu>\<upsilon> b = \<nu>\<upsilon> y \<and> \<phi> (a\<^sup>P) (b\<^sup>P) dj v) = \<phi> (x\<^sup>P) (y\<^sup>P) dj v) (\<lambda>x y. \<chi> (\<lambda>F. \<lparr>F,x\<rparr>) (\<lambda>F. \<lparr>F,x,x\<rparr>) (\<lambda>F. exe2 F x) (\<lambda>F a. \<lparr>F,a,x\<rparr>) (\<lambda>F. \<lparr>F,x,x,x\<rparr>) (\<lambda>F. exe3 F x x) (\<lambda>F a. \<lparr>F,x,a,x\<rparr>) (\<lambda>F a. \<lparr>F,a,x,x\<rparr>) (\<lambda>F. exe3 F x) (\<lambda>F a. exe3 F a x) (\<lambda>F a b. \<lparr>F,a,b,x\<rparr>) (\<lambda>F. \<lparr>F,y\<rparr>) (\<lambda>F. \<lparr>F,y,y\<rparr>) (\<lambda>F. exe2 F y) (\<lambda>F a. \<lparr>F,a,y\<rparr>) (\<lambda>F. \<lparr>F,y,y,y\<rparr>) (\<lambda>F. exe3 F y y) (\<lambda>F a. \<lparr>F,y,a,y\<rparr>) (\<lambda>F a. \<lparr>F,a,y,y\<rparr>) (\<lambda>F. exe3 F y) (\<lambda>F a. exe3 F a y) (\<lambda>F a b. \<lparr>F,a,b,y\<rparr>) (\<lambda>F. \<lparr>F,x,y\<rparr>) (\<lambda>F. \<lparr>F,y,x\<rparr>) (\<lambda>F. exe3 F x y) (\<lambda>F a. \<lparr>F,x,a,y\<rparr>) (\<lambda>F a. \<lparr>F,a,x,y\<rparr>) (\<lambda>F. exe3 F y x) (\<lambda>F a. \<lparr>F,y,a,x\<rparr>) (\<lambda>F a. \<lparr>F,a,y,x\<rparr>) (\<lambda>F. \<lparr>F,x,x,y\<rparr>) (\<lambda>F. \<lparr>F,x,y,x\<rparr>) (\<lambda>F. \<lparr>F,y,x,x\<rparr>) (\<lambda>F. \<lparr>F,x,y,y\<rparr>) (\<lambda>F. \<lparr>F,y,x,y\<rparr>) (\<lambda>F. \<lparr>F,y,y,x\<rparr>) (\<lambda>F. \<lparr>F,x,x,x\<rparr>) (\<lambda>F. \<lparr>F,y,y,y\<rparr>))
[PROOF STEP]
by (auto simp: meta_defs meta_aux)


[STATEMENT]
lemma IsProperInXYZ_intro[IsProper_intros]:
  "IsProperInXYZ (\<lambda> x y z . \<chi>
    \<comment> \<open>only \<open>x\<close>\<close>
      \<comment> \<open>one place:\<close> (\<lambda> F . \<lparr>F,x\<rparr>)
      \<comment> \<open>two place:\<close> (\<lambda> F . \<lparr>F,x,x\<rparr>) (\<lambda> F a . \<lparr>F,x,a\<rparr>) (\<lambda> F a . \<lparr>F,a,x\<rparr>)
      \<comment> \<open>three place three \<open>x\<close>:\<close> (\<lambda> F . \<lparr>F,x,x,x\<rparr>)
      \<comment> \<open>three place two \<open>x\<close>:\<close> (\<lambda> F a . \<lparr>F,x,x,a\<rparr>) (\<lambda> F a . \<lparr>F,x,a,x\<rparr>)
                              (\<lambda> F a . \<lparr>F,a,x,x\<rparr>)
      \<comment> \<open>three place one \<open>x\<close>:\<close> (\<lambda> F a b. \<lparr>F,x,a,b\<rparr>) (\<lambda> F a b. \<lparr>F,a,x,b\<rparr>)
                              (\<lambda> F a b . \<lparr>F,a,b,x\<rparr>)
    \<comment> \<open>only \<open>y\<close>\<close>
      \<comment> \<open>one place:\<close> (\<lambda> F . \<lparr>F,y\<rparr>)
      \<comment> \<open>two place:\<close> (\<lambda> F . \<lparr>F,y,y\<rparr>) (\<lambda> F a . \<lparr>F,y,a\<rparr>) (\<lambda> F a . \<lparr>F,a,y\<rparr>)
      \<comment> \<open>three place three \<open>y\<close>:\<close> (\<lambda> F . \<lparr>F,y,y,y\<rparr>)
      \<comment> \<open>three place two \<open>y\<close>:\<close> (\<lambda> F a . \<lparr>F,y,y,a\<rparr>) (\<lambda> F a . \<lparr>F,y,a,y\<rparr>)
                              (\<lambda> F a . \<lparr>F,a,y,y\<rparr>)
      \<comment> \<open>three place one \<open>y\<close>:\<close> (\<lambda> F a b. \<lparr>F,y,a,b\<rparr>) (\<lambda> F a b. \<lparr>F,a,y,b\<rparr>)
                              (\<lambda> F a b . \<lparr>F,a,b,y\<rparr>)
    \<comment> \<open>only \<open>z\<close>\<close>
      \<comment> \<open>one place:\<close> (\<lambda> F . \<lparr>F,z\<rparr>)
      \<comment> \<open>two place:\<close> (\<lambda> F . \<lparr>F,z,z\<rparr>) (\<lambda> F a . \<lparr>F,z,a\<rparr>) (\<lambda> F a . \<lparr>F,a,z\<rparr>)
      \<comment> \<open>three place three \<open>z\<close>:\<close> (\<lambda> F . \<lparr>F,z,z,z\<rparr>)
      \<comment> \<open>three place two \<open>z\<close>:\<close> (\<lambda> F a . \<lparr>F,z,z,a\<rparr>) (\<lambda> F a . \<lparr>F,z,a,z\<rparr>)
                              (\<lambda> F a . \<lparr>F,a,z,z\<rparr>)
      \<comment> \<open>three place one \<open>z\<close>:\<close> (\<lambda> F a b. \<lparr>F,z,a,b\<rparr>) (\<lambda> F a b. \<lparr>F,a,z,b\<rparr>)
                              (\<lambda> F a b . \<lparr>F,a,b,z\<rparr>)
    \<comment> \<open>\<open>x\<close> and \<open>y\<close>\<close>
      \<comment> \<open>two place:\<close> (\<lambda> F . \<lparr>F,x,y\<rparr>) (\<lambda> F . \<lparr>F,y,x\<rparr>)
      \<comment> \<open>three place \<open>(x,y)\<close>:\<close> (\<lambda> F a . \<lparr>F,x,y,a\<rparr>) (\<lambda> F a . \<lparr>F,x,a,y\<rparr>)
                              (\<lambda> F a . \<lparr>F,a,x,y\<rparr>)
      \<comment> \<open>three place \<open>(y,x)\<close>:\<close> (\<lambda> F a . \<lparr>F,y,x,a\<rparr>) (\<lambda> F a . \<lparr>F,y,a,x\<rparr>)
                              (\<lambda> F a . \<lparr>F,a,y,x\<rparr>)
      \<comment> \<open>three place \<open>(x,x,y)\<close>:\<close> (\<lambda> F . \<lparr>F,x,x,y\<rparr>) (\<lambda> F . \<lparr>F,x,y,x\<rparr>)
                                (\<lambda> F . \<lparr>F,y,x,x\<rparr>)
      \<comment> \<open>three place \<open>(x,y,y)\<close>:\<close> (\<lambda> F . \<lparr>F,x,y,y\<rparr>) (\<lambda> F . \<lparr>F,y,x,y\<rparr>)
                                (\<lambda> F . \<lparr>F,y,y,x\<rparr>)
      \<comment> \<open>three place \<open>(x,x,x)\<close>:\<close> (\<lambda> F . \<lparr>F,x,x,x\<rparr>)
      \<comment> \<open>three place \<open>(y,y,y)\<close>:\<close> (\<lambda> F . \<lparr>F,y,y,y\<rparr>)
    \<comment> \<open>\<open>x\<close> and \<open>z\<close>\<close>
      \<comment> \<open>two place:\<close> (\<lambda> F . \<lparr>F,x,z\<rparr>) (\<lambda> F . \<lparr>F,z,x\<rparr>)
      \<comment> \<open>three place \<open>(x,z)\<close>:\<close> (\<lambda> F a . \<lparr>F,x,z,a\<rparr>) (\<lambda> F a . \<lparr>F,x,a,z\<rparr>)
                              (\<lambda> F a . \<lparr>F,a,x,z\<rparr>)
      \<comment> \<open>three place \<open>(z,x)\<close>:\<close> (\<lambda> F a . \<lparr>F,z,x,a\<rparr>) (\<lambda> F a . \<lparr>F,z,a,x\<rparr>)
                              (\<lambda> F a . \<lparr>F,a,z,x\<rparr>)
      \<comment> \<open>three place \<open>(x,x,z)\<close>:\<close> (\<lambda> F . \<lparr>F,x,x,z\<rparr>) (\<lambda> F . \<lparr>F,x,z,x\<rparr>)
                                (\<lambda> F . \<lparr>F,z,x,x\<rparr>)
      \<comment> \<open>three place \<open>(x,z,z)\<close>:\<close> (\<lambda> F . \<lparr>F,x,z,z\<rparr>) (\<lambda> F . \<lparr>F,z,x,z\<rparr>)
                                (\<lambda> F . \<lparr>F,z,z,x\<rparr>)
      \<comment> \<open>three place \<open>(x,x,x)\<close>:\<close> (\<lambda> F . \<lparr>F,x,x,x\<rparr>)
      \<comment> \<open>three place \<open>(z,z,z)\<close>:\<close> (\<lambda> F . \<lparr>F,z,z,z\<rparr>)
    \<comment> \<open>\<open>y\<close> and \<open>z\<close>\<close>
      \<comment> \<open>two place:\<close> (\<lambda> F . \<lparr>F,y,z\<rparr>) (\<lambda> F . \<lparr>F,z,y\<rparr>)
      \<comment> \<open>three place \<open>(y,z)\<close>:\<close> (\<lambda> F a . \<lparr>F,y,z,a\<rparr>) (\<lambda> F a . \<lparr>F,y,a,z\<rparr>)
                              (\<lambda> F a . \<lparr>F,a,y,z\<rparr>)
      \<comment> \<open>three place \<open>(z,y)\<close>:\<close> (\<lambda> F a . \<lparr>F,z,y,a\<rparr>) (\<lambda> F a . \<lparr>F,z,a,y\<rparr>)
                              (\<lambda> F a . \<lparr>F,a,z,y\<rparr>)
      \<comment> \<open>three place \<open>(y,y,z)\<close>:\<close> (\<lambda> F . \<lparr>F,y,y,z\<rparr>) (\<lambda> F . \<lparr>F,y,z,y\<rparr>)
                                (\<lambda> F . \<lparr>F,z,y,y\<rparr>)
      \<comment> \<open>three place \<open>(y,z,z)\<close>:\<close> (\<lambda> F . \<lparr>F,y,z,z\<rparr>) (\<lambda> F . \<lparr>F,z,y,z\<rparr>)
                                (\<lambda> F . \<lparr>F,z,z,y\<rparr>)
      \<comment> \<open>three place \<open>(y,y,y)\<close>:\<close> (\<lambda> F . \<lparr>F,y,y,y\<rparr>)
      \<comment> \<open>three place \<open>(z,z,z)\<close>:\<close> (\<lambda> F . \<lparr>F,z,z,z\<rparr>)
    \<comment> \<open>\<open>x y z\<close>\<close>
      \<comment> \<open>three place \<open>(x,\<dots>)\<close>:\<close> (\<lambda> F . \<lparr>F,x,y,z\<rparr>) (\<lambda> F . \<lparr>F,x,z,y\<rparr>)
      \<comment> \<open>three place \<open>(y,\<dots>)\<close>:\<close> (\<lambda> F . \<lparr>F,y,x,z\<rparr>) (\<lambda> F . \<lparr>F,y,z,x\<rparr>)
      \<comment> \<open>three place \<open>(z,\<dots>)\<close>:\<close> (\<lambda> F . \<lparr>F,z,x,y\<rparr>) (\<lambda> F . \<lparr>F,z,y,x\<rparr>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. IsProperInXYZ (\<lambda>x y z. \<chi> (\<lambda>F. \<lparr>F,x\<rparr>) (\<lambda>F. \<lparr>F,x,x\<rparr>) (\<lambda>F. exe2 F x) (\<lambda>F a. \<lparr>F,a,x\<rparr>) (\<lambda>F. \<lparr>F,x,x,x\<rparr>) (\<lambda>F. exe3 F x x) (\<lambda>F a. \<lparr>F,x,a,x\<rparr>) (\<lambda>F a. \<lparr>F,a,x,x\<rparr>) (\<lambda>F. exe3 F x) (\<lambda>F a. exe3 F a x) (\<lambda>F a b. \<lparr>F,a,b,x\<rparr>) (\<lambda>F. \<lparr>F,y\<rparr>) (\<lambda>F. \<lparr>F,y,y\<rparr>) (\<lambda>F. exe2 F y) (\<lambda>F a. \<lparr>F,a,y\<rparr>) (\<lambda>F. \<lparr>F,y,y,y\<rparr>) (\<lambda>F. exe3 F y y) (\<lambda>F a. \<lparr>F,y,a,y\<rparr>) (\<lambda>F a. \<lparr>F,a,y,y\<rparr>) (\<lambda>F. exe3 F y) (\<lambda>F a. exe3 F a y) (\<lambda>F a b. \<lparr>F,a,b,y\<rparr>) (\<lambda>F. \<lparr>F,z\<rparr>) (\<lambda>F. \<lparr>F,z,z\<rparr>) (\<lambda>F. exe2 F z) (\<lambda>F a. \<lparr>F,a,z\<rparr>) (\<lambda>F. \<lparr>F,z,z,z\<rparr>) (\<lambda>F. exe3 F z z) (\<lambda>F a. \<lparr>F,z,a,z\<rparr>) (\<lambda>F a. \<lparr>F,a,z,z\<rparr>) (\<lambda>F. exe3 F z) (\<lambda>F a. exe3 F a z) (\<lambda>F a b. \<lparr>F,a,b,z\<rparr>) (\<lambda>F. \<lparr>F,x,y\<rparr>) (\<lambda>F. \<lparr>F,y,x\<rparr>) (\<lambda>F. exe3 F x y) (\<lambda>F a. \<lparr>F,x,a,y\<rparr>) (\<lambda>F a. \<lparr>F,a,x,y\<rparr>) (\<lambda>F. exe3 F y x) (\<lambda>F a. \<lparr>F,y,a,x\<rparr>) (\<lambda>F a. \<lparr>F,a,y,x\<rparr>) (\<lambda>F. \<lparr>F,x,x,y\<rparr>) (\<lambda>F. \<lparr>F,x,y,x\<rparr>) (\<lambda>F. \<lparr>F,y,x,x\<rparr>) (\<lambda>F. \<lparr>F,x,y,y\<rparr>) (\<lambda>F. \<lparr>F,y,x,y\<rparr>) (\<lambda>F. \<lparr>F,y,y,x\<rparr>) (\<lambda>F. \<lparr>F,x,x,x\<rparr>) (\<lambda>F. \<lparr>F,y,y,y\<rparr>) (\<lambda>F. \<lparr>F,x,z\<rparr>) (\<lambda>F. \<lparr>F,z,x\<rparr>) (\<lambda>F. exe3 F x z) (\<lambda>F a. \<lparr>F,x,a,z\<rparr>) (\<lambda>F a. \<lparr>F,a,x,z\<rparr>) (\<lambda>F. exe3 F z x) (\<lambda>F a. \<lparr>F,z,a,x\<rparr>) (\<lambda>F a. \<lparr>F,a,z,x\<rparr>) (\<lambda>F. \<lparr>F,x,x,z\<rparr>) (\<lambda>F. \<lparr>F,x,z,x\<rparr>) (\<lambda>F. \<lparr>F,z,x,x\<rparr>) (\<lambda>F. \<lparr>F,x,z,z\<rparr>) (\<lambda>F. \<lparr>F,z,x,z\<rparr>) (\<lambda>F. \<lparr>F,z,z,x\<rparr>) (\<lambda>F. \<lparr>F,x,x,x\<rparr>) (\<lambda>F. \<lparr>F,z,z,z\<rparr>) (\<lambda>F. \<lparr>F,y,z\<rparr>) (\<lambda>F. \<lparr>F,z,y\<rparr>) (\<lambda>F. exe3 F y z) (\<lambda>F a. \<lparr>F,y,a,z\<rparr>) (\<lambda>F a. \<lparr>F,a,y,z\<rparr>) (\<lambda>F. exe3 F z y) (\<lambda>F a. \<lparr>F,z,a,y\<rparr>) (\<lambda>F a. \<lparr>F,a,z,y\<rparr>) (\<lambda>F. \<lparr>F,y,y,z\<rparr>) (\<lambda>F. \<lparr>F,y,z,y\<rparr>) (\<lambda>F. \<lparr>F,z,y,y\<rparr>) (\<lambda>F. \<lparr>F,y,z,z\<rparr>) (\<lambda>F. \<lparr>F,z,y,z\<rparr>) (\<lambda>F. \<lparr>F,z,z,y\<rparr>) (\<lambda>F. \<lparr>F,y,y,y\<rparr>) (\<lambda>F. \<lparr>F,z,z,z\<rparr>) (\<lambda>F. \<lparr>F,x,y,z\<rparr>) (\<lambda>F. \<lparr>F,x,z,y\<rparr>) (\<lambda>F. \<lparr>F,y,x,z\<rparr>) (\<lambda>F. \<lparr>F,y,z,x\<rparr>) (\<lambda>F. \<lparr>F,z,x,y\<rparr>) (\<lambda>F. \<lparr>F,z,y,x\<rparr>))
[PROOF STEP]
unfolding IsProperInXYZ_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_fun (map_fun id (map_fun id (map_fun id eval\<o>))) id (\<lambda>\<phi>. \<forall>x y z v. (\<exists>a b c. \<nu>\<upsilon> a = \<nu>\<upsilon> x \<and> \<nu>\<upsilon> b = \<nu>\<upsilon> y \<and> \<nu>\<upsilon> c = \<nu>\<upsilon> z \<and> \<phi> (a\<^sup>P) (b\<^sup>P) (c\<^sup>P) dj v) = \<phi> (x\<^sup>P) (y\<^sup>P) (z\<^sup>P) dj v) (\<lambda>x y z. \<chi> (\<lambda>F. \<lparr>F,x\<rparr>) (\<lambda>F. \<lparr>F,x,x\<rparr>) (\<lambda>F. exe2 F x) (\<lambda>F a. \<lparr>F,a,x\<rparr>) (\<lambda>F. \<lparr>F,x,x,x\<rparr>) (\<lambda>F. exe3 F x x) (\<lambda>F a. \<lparr>F,x,a,x\<rparr>) (\<lambda>F a. \<lparr>F,a,x,x\<rparr>) (\<lambda>F. exe3 F x) (\<lambda>F a. exe3 F a x) (\<lambda>F a b. \<lparr>F,a,b,x\<rparr>) (\<lambda>F. \<lparr>F,y\<rparr>) (\<lambda>F. \<lparr>F,y,y\<rparr>) (\<lambda>F. exe2 F y) (\<lambda>F a. \<lparr>F,a,y\<rparr>) (\<lambda>F. \<lparr>F,y,y,y\<rparr>) (\<lambda>F. exe3 F y y) (\<lambda>F a. \<lparr>F,y,a,y\<rparr>) (\<lambda>F a. \<lparr>F,a,y,y\<rparr>) (\<lambda>F. exe3 F y) (\<lambda>F a. exe3 F a y) (\<lambda>F a b. \<lparr>F,a,b,y\<rparr>) (\<lambda>F. \<lparr>F,z\<rparr>) (\<lambda>F. \<lparr>F,z,z\<rparr>) (\<lambda>F. exe2 F z) (\<lambda>F a. \<lparr>F,a,z\<rparr>) (\<lambda>F. \<lparr>F,z,z,z\<rparr>) (\<lambda>F. exe3 F z z) (\<lambda>F a. \<lparr>F,z,a,z\<rparr>) (\<lambda>F a. \<lparr>F,a,z,z\<rparr>) (\<lambda>F. exe3 F z) (\<lambda>F a. exe3 F a z) (\<lambda>F a b. \<lparr>F,a,b,z\<rparr>) (\<lambda>F. \<lparr>F,x,y\<rparr>) (\<lambda>F. \<lparr>F,y,x\<rparr>) (\<lambda>F. exe3 F x y) (\<lambda>F a. \<lparr>F,x,a,y\<rparr>) (\<lambda>F a. \<lparr>F,a,x,y\<rparr>) (\<lambda>F. exe3 F y x) (\<lambda>F a. \<lparr>F,y,a,x\<rparr>) (\<lambda>F a. \<lparr>F,a,y,x\<rparr>) (\<lambda>F. \<lparr>F,x,x,y\<rparr>) (\<lambda>F. \<lparr>F,x,y,x\<rparr>) (\<lambda>F. \<lparr>F,y,x,x\<rparr>) (\<lambda>F. \<lparr>F,x,y,y\<rparr>) (\<lambda>F. \<lparr>F,y,x,y\<rparr>) (\<lambda>F. \<lparr>F,y,y,x\<rparr>) (\<lambda>F. \<lparr>F,x,x,x\<rparr>) (\<lambda>F. \<lparr>F,y,y,y\<rparr>) (\<lambda>F. \<lparr>F,x,z\<rparr>) (\<lambda>F. \<lparr>F,z,x\<rparr>) (\<lambda>F. exe3 F x z) (\<lambda>F a. \<lparr>F,x,a,z\<rparr>) (\<lambda>F a. \<lparr>F,a,x,z\<rparr>) (\<lambda>F. exe3 F z x) (\<lambda>F a. \<lparr>F,z,a,x\<rparr>) (\<lambda>F a. \<lparr>F,a,z,x\<rparr>) (\<lambda>F. \<lparr>F,x,x,z\<rparr>) (\<lambda>F. \<lparr>F,x,z,x\<rparr>) (\<lambda>F. \<lparr>F,z,x,x\<rparr>) (\<lambda>F. \<lparr>F,x,z,z\<rparr>) (\<lambda>F. \<lparr>F,z,x,z\<rparr>) (\<lambda>F. \<lparr>F,z,z,x\<rparr>) (\<lambda>F. \<lparr>F,x,x,x\<rparr>) (\<lambda>F. \<lparr>F,z,z,z\<rparr>) (\<lambda>F. \<lparr>F,y,z\<rparr>) (\<lambda>F. \<lparr>F,z,y\<rparr>) (\<lambda>F. exe3 F y z) (\<lambda>F a. \<lparr>F,y,a,z\<rparr>) (\<lambda>F a. \<lparr>F,a,y,z\<rparr>) (\<lambda>F. exe3 F z y) (\<lambda>F a. \<lparr>F,z,a,y\<rparr>) (\<lambda>F a. \<lparr>F,a,z,y\<rparr>) (\<lambda>F. \<lparr>F,y,y,z\<rparr>) (\<lambda>F. \<lparr>F,y,z,y\<rparr>) (\<lambda>F. \<lparr>F,z,y,y\<rparr>) (\<lambda>F. \<lparr>F,y,z,z\<rparr>) (\<lambda>F. \<lparr>F,z,y,z\<rparr>) (\<lambda>F. \<lparr>F,z,z,y\<rparr>) (\<lambda>F. \<lparr>F,y,y,y\<rparr>) (\<lambda>F. \<lparr>F,z,z,z\<rparr>) (\<lambda>F. \<lparr>F,x,y,z\<rparr>) (\<lambda>F. \<lparr>F,x,z,y\<rparr>) (\<lambda>F. \<lparr>F,y,x,z\<rparr>) (\<lambda>F. \<lparr>F,y,z,x\<rparr>) (\<lambda>F. \<lparr>F,z,x,y\<rparr>) (\<lambda>F. \<lparr>F,z,y,x\<rparr>))
[PROOF STEP]
by (auto simp: meta_defs meta_aux)


[STATEMENT]
lemma (in wellorder) min_Least:
  "\<lbrakk>\<exists>n. P n; \<exists>n. Q n\<rbrakk> \<Longrightarrow> min (Least P) (Least Q) = (LEAST n. P n \<or> Q n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>n. P n; \<exists>n. Q n\<rbrakk> \<Longrightarrow> min (Least P) (Least Q) = (LEAST n. P n \<or> Q n)
[PROOF STEP]
proof (intro sym[OF Least_equality])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<exists>n. P n; \<exists>n. Q n\<rbrakk> \<Longrightarrow> P (min (Least P) (Least Q)) \<or> Q (min (Least P) (Least Q))
 2. \<And>y. \<lbrakk>\<exists>n. P n; \<exists>n. Q n; P y \<or> Q y\<rbrakk> \<Longrightarrow> min (Least P) (Least Q) \<le> y
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<exists>n. P n; \<exists>n. Q n\<rbrakk> \<Longrightarrow> P (min (Least P) (Least Q)) \<or> Q (min (Least P) (Least Q))
 2. \<And>y. \<lbrakk>\<exists>n. P n; \<exists>n. Q n; P y \<or> Q y\<rbrakk> \<Longrightarrow> min (Least P) (Least Q) \<le> y
[PROOF STEP]
assume "P y \<or> Q y"
[PROOF STATE]
proof (state)
this:
P y \<or> Q y

goal (2 subgoals):
 1. \<lbrakk>\<exists>n. P n; \<exists>n. Q n\<rbrakk> \<Longrightarrow> P (min (Least P) (Least Q)) \<or> Q (min (Least P) (Least Q))
 2. \<And>y. \<lbrakk>\<exists>n. P n; \<exists>n. Q n; P y \<or> Q y\<rbrakk> \<Longrightarrow> min (Least P) (Least Q) \<le> y
[PROOF STEP]
thus "min (Least P) (Least Q) \<le> y"
[PROOF STATE]
proof (prove)
using this:
P y \<or> Q y

goal (1 subgoal):
 1. min (Least P) (Least Q) \<le> y
[PROOF STEP]
proof (elim disjE)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. P y \<Longrightarrow> min (Least P) (Least Q) \<le> y
 2. Q y \<Longrightarrow> min (Least P) (Least Q) \<le> y
[PROOF STEP]
assume "P y"
[PROOF STATE]
proof (state)
this:
P y

goal (2 subgoals):
 1. P y \<Longrightarrow> min (Least P) (Least Q) \<le> y
 2. Q y \<Longrightarrow> min (Least P) (Least Q) \<le> y
[PROOF STEP]
hence "Least P \<le> y"
[PROOF STATE]
proof (prove)
using this:
P y

goal (1 subgoal):
 1. Least P \<le> y
[PROOF STEP]
by (auto intro: LeastI2_wellorder)
[PROOF STATE]
proof (state)
this:
Least P \<le> y

goal (2 subgoals):
 1. P y \<Longrightarrow> min (Least P) (Least Q) \<le> y
 2. Q y \<Longrightarrow> min (Least P) (Least Q) \<le> y
[PROOF STEP]
thus "min (Least P) (Least Q) \<le> y"
[PROOF STATE]
proof (prove)
using this:
Least P \<le> y

goal (1 subgoal):
 1. min (Least P) (Least Q) \<le> y
[PROOF STEP]
unfolding min_def
[PROOF STATE]
proof (prove)
using this:
Least P \<le> y

goal (1 subgoal):
 1. (if Least P \<le> Least Q then Least P else Least Q) \<le> y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
min (Least P) (Least Q) \<le> y

goal (1 subgoal):
 1. Q y \<Longrightarrow> min (Least P) (Least Q) \<le> y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Q y \<Longrightarrow> min (Least P) (Least Q) \<le> y
[PROOF STEP]
assume "Q y"
[PROOF STATE]
proof (state)
this:
Q y

goal (1 subgoal):
 1. Q y \<Longrightarrow> min (Least P) (Least Q) \<le> y
[PROOF STEP]
hence "Least Q \<le> y"
[PROOF STATE]
proof (prove)
using this:
Q y

goal (1 subgoal):
 1. Least Q \<le> y
[PROOF STEP]
by (auto intro: LeastI2_wellorder)
[PROOF STATE]
proof (state)
this:
Least Q \<le> y

goal (1 subgoal):
 1. Q y \<Longrightarrow> min (Least P) (Least Q) \<le> y
[PROOF STEP]
thus "min (Least P) (Least Q) \<le> y"
[PROOF STATE]
proof (prove)
using this:
Least Q \<le> y

goal (1 subgoal):
 1. min (Least P) (Least Q) \<le> y
[PROOF STEP]
unfolding min_def
[PROOF STATE]
proof (prove)
using this:
Least Q \<le> y

goal (1 subgoal):
 1. (if Least P \<le> Least Q then Least P else Least Q) \<le> y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
min (Least P) (Least Q) \<le> y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
min (Least P) (Least Q) \<le> y

goal (1 subgoal):
 1. \<lbrakk>\<exists>n. P n; \<exists>n. Q n\<rbrakk> \<Longrightarrow> P (min (Least P) (Least Q)) \<or> Q (min (Least P) (Least Q))
[PROOF STEP]
qed (metis LeastI_ex min_def)


[STATEMENT]
lemma sconst_collapse: "y ## sconst y = sconst y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y ## sconst y = sconst y
[PROOF STEP]
by (subst (2) siterate.ctr) auto


[STATEMENT]
lemma shift_sconst_inj: "\<lbrakk>length x = length y; x @- sconst z = y @- sconst z\<rbrakk> \<Longrightarrow> x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length x = length y; x @- sconst z = y @- sconst z\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
by (induct rule: list_induct2) auto


[STATEMENT]
lemma any_\<Sigma>[simp]: "any \<in> set \<Sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. any \<in> set \<Sigma>
[PROOF STEP]
unfolding any_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hd \<Sigma> \<in> set \<Sigma>
[PROOF STEP]
by (auto simp: nonempty intro: someI[of _ "hd \<Sigma>"])


[STATEMENT]
lemma any_\<sigma>[simp]: "length bs = n \<Longrightarrow> (any, bs) \<in> set (\<sigma> \<Sigma> n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length bs = n \<Longrightarrow> (any, bs) \<in> set (\<sigma> \<Sigma> n)
[PROOF STEP]
by (auto simp: \<sigma>_def set_n_lists)


[STATEMENT]
lemma tl_stream_enc[simp]: "smap \<pi> (stream_enc (w, x # I)) = stream_enc (w, I)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. smap \<pi> (stream_enc (w, x # I)) = stream_enc (w, I)
[PROOF STEP]
by (auto simp: comp_def \<pi>_def)


[STATEMENT]
lemma enc_atom_max: "\<lbrakk>\<forall>x\<in>set I. case x of Inl p \<Rightarrow> p \<le> n | Inr P \<Rightarrow> \<forall>p\<in>P. p \<le> n; n \<le> n'\<rbrakk> \<Longrightarrow>
  enc_atom I (Suc n') a = (a, replicate (length I) False)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>set I. case x of Inl p \<Rightarrow> p \<le> n | Inr P \<Rightarrow> \<forall>p\<in>P. p \<le> n; n \<le> n'\<rbrakk> \<Longrightarrow> enc_atom I (Suc n') a = (a, replicate (length I) False)
[PROOF STEP]
by (induct I) (auto split: sum.splits)


[STATEMENT]
lemma ex_Loop_stream_enc:
assumes "\<forall>x \<in> set I. case x of Inr P \<Rightarrow> finite P | _ \<Rightarrow> True"
shows "\<exists>n. sdrop n (stream_enc (w, I)) = sconst (any, replicate (length I) False)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n. sdrop n (stream_enc (w, I)) = sconst (any, replicate (length I) False)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>n. sdrop n (stream_enc (w, I)) = sconst (any, replicate (length I) False)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>set I. case x of Inl a \<Rightarrow> True | Inr P \<Rightarrow> finite P
[PROOF STEP]
have "\<exists>n > length w. \<forall>x\<in>set I. case x of Inl p \<Rightarrow> p \<le> n | Inr P \<Rightarrow> \<forall>p\<in>P. p \<le> n"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set I. case x of Inl a \<Rightarrow> True | Inr P \<Rightarrow> finite P

goal (1 subgoal):
 1. \<exists>n>length w. \<forall>x\<in>set I. case x of Inl p \<Rightarrow> p \<le> n | Inr P \<Rightarrow> \<forall>p\<in>P. p \<le> n
[PROOF STEP]
proof (induct I)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Ball (set []) (case_sum (\<lambda>a. True) finite) \<Longrightarrow> \<exists>n>length w. Ball (set []) (case_sum (\<lambda>p. p \<le> n) (\<lambda>P. \<forall>p\<in>P. p \<le> n))
 2. \<And>a I. \<lbrakk>Ball (set I) (case_sum (\<lambda>a. True) finite) \<Longrightarrow> \<exists>n>length w. Ball (set I) (case_sum (\<lambda>p. p \<le> n) (\<lambda>P. \<forall>p\<in>P. p \<le> n)); Ball (set (a # I)) (case_sum (\<lambda>a. True) finite)\<rbrakk> \<Longrightarrow> \<exists>n>length w. Ball (set (a # I)) (case_sum (\<lambda>p. p \<le> n) (\<lambda>P. \<forall>p\<in>P. p \<le> n))
[PROOF STEP]
case (Cons x I)
[PROOF STATE]
proof (state)
this:
\<forall>a\<in>set I. case a of Inl a \<Rightarrow> True | Inr a \<Rightarrow> finite a \<Longrightarrow> \<exists>n>length w. \<forall>a\<in>set I. case a of Inl p \<Rightarrow> p \<le> n | Inr P \<Rightarrow> \<forall>p\<in>P. p \<le> n
\<forall>a\<in>set (x # I). case a of Inl a \<Rightarrow> True | Inr a \<Rightarrow> finite a

goal (2 subgoals):
 1. Ball (set []) (case_sum (\<lambda>a. True) finite) \<Longrightarrow> \<exists>n>length w. Ball (set []) (case_sum (\<lambda>p. p \<le> n) (\<lambda>P. \<forall>p\<in>P. p \<le> n))
 2. \<And>a I. \<lbrakk>Ball (set I) (case_sum (\<lambda>a. True) finite) \<Longrightarrow> \<exists>n>length w. Ball (set I) (case_sum (\<lambda>p. p \<le> n) (\<lambda>P. \<forall>p\<in>P. p \<le> n)); Ball (set (a # I)) (case_sum (\<lambda>a. True) finite)\<rbrakk> \<Longrightarrow> \<exists>n>length w. Ball (set (a # I)) (case_sum (\<lambda>p. p \<le> n) (\<lambda>P. \<forall>p\<in>P. p \<le> n))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>a\<in>set I. case a of Inl a \<Rightarrow> True | Inr a \<Rightarrow> finite a \<Longrightarrow> \<exists>n>length w. \<forall>a\<in>set I. case a of Inl p \<Rightarrow> p \<le> n | Inr P \<Rightarrow> \<forall>p\<in>P. p \<le> n
\<forall>a\<in>set (x # I). case a of Inl a \<Rightarrow> True | Inr a \<Rightarrow> finite a
[PROOF STEP]
obtain n where IH: "length w < n"
      "\<forall>x\<in>set I. case x of Inl p \<Rightarrow> p \<le> n | Inr P \<Rightarrow> \<forall>p\<in>P. p \<le> n"
[PROOF STATE]
proof (prove)
using this:
\<forall>a\<in>set I. case a of Inl a \<Rightarrow> True | Inr a \<Rightarrow> finite a \<Longrightarrow> \<exists>n>length w. \<forall>a\<in>set I. case a of Inl p \<Rightarrow> p \<le> n | Inr P \<Rightarrow> \<forall>p\<in>P. p \<le> n
\<forall>a\<in>set (x # I). case a of Inl a \<Rightarrow> True | Inr a \<Rightarrow> finite a

goal (1 subgoal):
 1. (\<And>n. \<lbrakk>length w < n; \<forall>x\<in>set I. case x of Inl p \<Rightarrow> p \<le> n | Inr P \<Rightarrow> \<forall>p\<in>P. p \<le> n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length w < n
\<forall>x\<in>set I. case x of Inl p \<Rightarrow> p \<le> n | Inr P \<Rightarrow> \<forall>p\<in>P. p \<le> n

goal (2 subgoals):
 1. Ball (set []) (case_sum (\<lambda>a. True) finite) \<Longrightarrow> \<exists>n>length w. Ball (set []) (case_sum (\<lambda>p. p \<le> n) (\<lambda>P. \<forall>p\<in>P. p \<le> n))
 2. \<And>a I. \<lbrakk>Ball (set I) (case_sum (\<lambda>a. True) finite) \<Longrightarrow> \<exists>n>length w. Ball (set I) (case_sum (\<lambda>p. p \<le> n) (\<lambda>P. \<forall>p\<in>P. p \<le> n)); Ball (set (a # I)) (case_sum (\<lambda>a. True) finite)\<rbrakk> \<Longrightarrow> \<exists>n>length w. Ball (set (a # I)) (case_sum (\<lambda>p. p \<le> n) (\<lambda>P. \<forall>p\<in>P. p \<le> n))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
length w < n
\<forall>x\<in>set I. case x of Inl p \<Rightarrow> p \<le> n | Inr P \<Rightarrow> \<forall>p\<in>P. p \<le> n

goal (1 subgoal):
 1. \<exists>n>length w. \<forall>a\<in>set (x # I). case a of Inl p \<Rightarrow> p \<le> n | Inr P \<Rightarrow> \<forall>p\<in>P. p \<le> n
[PROOF STEP]
proof (cases x)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>length w < n; \<forall>x\<in>set I. case x of Inl p \<Rightarrow> p \<le> n | Inr P \<Rightarrow> \<forall>p\<in>P. p \<le> n; x = Inl a\<rbrakk> \<Longrightarrow> \<exists>n>length w. \<forall>a\<in>set (x # I). case a of Inl p \<Rightarrow> p \<le> n | Inr P \<Rightarrow> \<forall>p\<in>P. p \<le> n
 2. \<And>b. \<lbrakk>length w < n; \<forall>x\<in>set I. case x of Inl p \<Rightarrow> p \<le> n | Inr P \<Rightarrow> \<forall>p\<in>P. p \<le> n; x = Inr b\<rbrakk> \<Longrightarrow> \<exists>n>length w. \<forall>a\<in>set (x # I). case a of Inl p \<Rightarrow> p \<le> n | Inr P \<Rightarrow> \<forall>p\<in>P. p \<le> n
[PROOF STEP]
case (Inl p)
[PROOF STATE]
proof (state)
this:
x = Inl p

goal (2 subgoals):
 1. \<And>a. \<lbrakk>length w < n; \<forall>x\<in>set I. case x of Inl p \<Rightarrow> p \<le> n | Inr P \<Rightarrow> \<forall>p\<in>P. p \<le> n; x = Inl a\<rbrakk> \<Longrightarrow> \<exists>n>length w. \<forall>a\<in>set (x # I). case a of Inl p \<Rightarrow> p \<le> n | Inr P \<Rightarrow> \<forall>p\<in>P. p \<le> n
 2. \<And>b. \<lbrakk>length w < n; \<forall>x\<in>set I. case x of Inl p \<Rightarrow> p \<le> n | Inr P \<Rightarrow> \<forall>p\<in>P. p \<le> n; x = Inr b\<rbrakk> \<Longrightarrow> \<exists>n>length w. \<forall>a\<in>set (x # I). case a of Inl p \<Rightarrow> p \<le> n | Inr P \<Rightarrow> \<forall>p\<in>P. p \<le> n
[PROOF STEP]
with IH
[PROOF STATE]
proof (chain)
picking this:
length w < n
\<forall>x\<in>set I. case x of Inl p \<Rightarrow> p \<le> n | Inr P \<Rightarrow> \<forall>p\<in>P. p \<le> n
x = Inl p
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
length w < n
\<forall>x\<in>set I. case x of Inl p \<Rightarrow> p \<le> n | Inr P \<Rightarrow> \<forall>p\<in>P. p \<le> n
x = Inl p

goal (1 subgoal):
 1. \<exists>n>length w. \<forall>a\<in>set (x # I). case a of Inl p \<Rightarrow> p \<le> n | Inr P \<Rightarrow> \<forall>p\<in>P. p \<le> n
[PROOF STEP]
by (intro exI[of _ "max p n"]) (fastforce split: sum.splits)
[PROOF STATE]
proof (state)
this:
\<exists>n>length w. \<forall>a\<in>set (x # I). case a of Inl p \<Rightarrow> p \<le> n | Inr P \<Rightarrow> \<forall>p\<in>P. p \<le> n

goal (1 subgoal):
 1. \<And>b. \<lbrakk>length w < n; \<forall>x\<in>set I. case x of Inl p \<Rightarrow> p \<le> n | Inr P \<Rightarrow> \<forall>p\<in>P. p \<le> n; x = Inr b\<rbrakk> \<Longrightarrow> \<exists>n>length w. \<forall>a\<in>set (x # I). case a of Inl p \<Rightarrow> p \<le> n | Inr P \<Rightarrow> \<forall>p\<in>P. p \<le> n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>length w < n; \<forall>x\<in>set I. case x of Inl p \<Rightarrow> p \<le> n | Inr P \<Rightarrow> \<forall>p\<in>P. p \<le> n; x = Inr b\<rbrakk> \<Longrightarrow> \<exists>n>length w. \<forall>a\<in>set (x # I). case a of Inl p \<Rightarrow> p \<le> n | Inr P \<Rightarrow> \<forall>p\<in>P. p \<le> n
[PROOF STEP]
case (Inr P)
[PROOF STATE]
proof (state)
this:
x = Inr P

goal (1 subgoal):
 1. \<And>b. \<lbrakk>length w < n; \<forall>x\<in>set I. case x of Inl p \<Rightarrow> p \<le> n | Inr P \<Rightarrow> \<forall>p\<in>P. p \<le> n; x = Inr b\<rbrakk> \<Longrightarrow> \<exists>n>length w. \<forall>a\<in>set (x # I). case a of Inl p \<Rightarrow> p \<le> n | Inr P \<Rightarrow> \<forall>p\<in>P. p \<le> n
[PROOF STEP]
with IH Cons(2)
[PROOF STATE]
proof (chain)
picking this:
length w < n
\<forall>x\<in>set I. case x of Inl p \<Rightarrow> p \<le> n | Inr P \<Rightarrow> \<forall>p\<in>P. p \<le> n
\<forall>a\<in>set (x # I). case a of Inl a \<Rightarrow> True | Inr a \<Rightarrow> finite a
x = Inr P
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
length w < n
\<forall>x\<in>set I. case x of Inl p \<Rightarrow> p \<le> n | Inr P \<Rightarrow> \<forall>p\<in>P. p \<le> n
\<forall>a\<in>set (x # I). case a of Inl a \<Rightarrow> True | Inr a \<Rightarrow> finite a
x = Inr P

goal (1 subgoal):
 1. \<exists>n>length w. \<forall>a\<in>set (x # I). case a of Inl p \<Rightarrow> p \<le> n | Inr P \<Rightarrow> \<forall>p\<in>P. p \<le> n
[PROOF STEP]
by (intro exI[of _ "max (Max P) n"]) (fastforce dest: Max_ge split: sum.splits)
[PROOF STATE]
proof (state)
this:
\<exists>n>length w. \<forall>a\<in>set (x # I). case a of Inl p \<Rightarrow> p \<le> n | Inr P \<Rightarrow> \<forall>p\<in>P. p \<le> n

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>n>length w. \<forall>a\<in>set (x # I). case a of Inl p \<Rightarrow> p \<le> n | Inr P \<Rightarrow> \<forall>p\<in>P. p \<le> n

goal (1 subgoal):
 1. Ball (set []) (case_sum (\<lambda>a. True) finite) \<Longrightarrow> \<exists>n>length w. Ball (set []) (case_sum (\<lambda>p. p \<le> n) (\<lambda>P. \<forall>p\<in>P. p \<le> n))
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
\<exists>n>length w. \<forall>x\<in>set I. case x of Inl p \<Rightarrow> p \<le> n | Inr P \<Rightarrow> \<forall>p\<in>P. p \<le> n

goal (1 subgoal):
 1. \<exists>n. sdrop n (stream_enc (w, I)) = sconst (any, replicate (length I) False)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>n>length w. \<forall>x\<in>set I. case x of Inl p \<Rightarrow> p \<le> n | Inr P \<Rightarrow> \<forall>p\<in>P. p \<le> n
[PROOF STEP]
obtain n where "length w < n" "\<forall>x\<in>set I. case x of Inl p \<Rightarrow> p \<le> n | Inr P \<Rightarrow> \<forall>p\<in>P. p \<le> n"
[PROOF STATE]
proof (prove)
using this:
\<exists>n>length w. \<forall>x\<in>set I. case x of Inl p \<Rightarrow> p \<le> n | Inr P \<Rightarrow> \<forall>p\<in>P. p \<le> n

goal (1 subgoal):
 1. (\<And>n. \<lbrakk>length w < n; \<forall>x\<in>set I. case x of Inl p \<Rightarrow> p \<le> n | Inr P \<Rightarrow> \<forall>p\<in>P. p \<le> n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (elim exE conjE)
[PROOF STATE]
proof (state)
this:
length w < n
\<forall>x\<in>set I. case x of Inl p \<Rightarrow> p \<le> n | Inr P \<Rightarrow> \<forall>p\<in>P. p \<le> n

goal (1 subgoal):
 1. \<exists>n. sdrop n (stream_enc (w, I)) = sconst (any, replicate (length I) False)
[PROOF STEP]
hence "sdrop (Suc n) (stream_enc (w, I)) = sconst (any, replicate (length I) False)"
    (is "?s1 n = ?s2")
[PROOF STATE]
proof (prove)
using this:
length w < n
\<forall>x\<in>set I. case x of Inl p \<Rightarrow> p \<le> n | Inr P \<Rightarrow> \<forall>p\<in>P. p \<le> n

goal (1 subgoal):
 1. sdrop (Suc n) (stream_enc (w, I)) = sconst (any, replicate (length I) False)
[PROOF STEP]
by (intro stream.coinduct[of "\<lambda>s1 s2. \<exists>n'\<ge> n. s1 = ?s1 n' \<and> s2 = ?s2"])
      (auto simp: enc_atom_max dest: le_SucI)
[PROOF STATE]
proof (state)
this:
sdrop (Suc n) (stream_enc (w, I)) = sconst (any, replicate (length I) False)

goal (1 subgoal):
 1. \<exists>n. sdrop n (stream_enc (w, I)) = sconst (any, replicate (length I) False)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
sdrop (Suc n) (stream_enc (w, I)) = sconst (any, replicate (length I) False)

goal (1 subgoal):
 1. \<exists>n. sdrop n (stream_enc (w, I)) = sconst (any, replicate (length I) False)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>n. sdrop n (stream_enc (w, I)) = sconst (any, replicate (length I) False)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma length_snth_enc[simp]: "length (snd (stream_enc (w, I) !! n)) = length I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (snd (stream_enc (w, I) !! n)) = length I
[PROOF STEP]
by auto


[STATEMENT]
lemma sset_singleton[simp]: "sset s \<subseteq> {x} \<longleftrightarrow> sset s = {x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sset s \<subseteq> {x}) = (sset s = {x})
[PROOF STEP]
by (cases s) auto


[STATEMENT]
lemma drop_sconstE: "\<lbrakk>drop n w @- sconst y = sconst y; p < length w; \<not> p < n\<rbrakk> \<Longrightarrow> w ! p = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>drop n w @- sconst y = sconst y; p < length w; \<not> p < n\<rbrakk> \<Longrightarrow> w ! p = y
[PROOF STEP]
unfolding not_less sconst_alt
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sset (drop n w @- sconst y) = {y}; p < length w; n \<le> p\<rbrakk> \<Longrightarrow> w ! p = y
[PROOF STEP]
proof (induct p arbitrary: w n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>w n. \<lbrakk>sset (drop n w @- sconst y) = {y}; 0 < length w; n \<le> 0\<rbrakk> \<Longrightarrow> w ! 0 = y
 2. \<And>p w n. \<lbrakk>\<And>w n. \<lbrakk>sset (drop n w @- sconst y) = {y}; p < length w; n \<le> p\<rbrakk> \<Longrightarrow> w ! p = y; sset (drop n w @- sconst y) = {y}; Suc p < length w; n \<le> Suc p\<rbrakk> \<Longrightarrow> w ! Suc p = y
[PROOF STEP]
case (Suc p)
[PROOF STATE]
proof (state)
this:
\<lbrakk>sset (drop ?n ?w @- sconst y) = {y}; p < length ?w; ?n \<le> p\<rbrakk> \<Longrightarrow> ?w ! p = y
sset (drop n w @- sconst y) = {y}
Suc p < length w
n \<le> Suc p

goal (2 subgoals):
 1. \<And>w n. \<lbrakk>sset (drop n w @- sconst y) = {y}; 0 < length w; n \<le> 0\<rbrakk> \<Longrightarrow> w ! 0 = y
 2. \<And>p w n. \<lbrakk>\<And>w n. \<lbrakk>sset (drop n w @- sconst y) = {y}; p < length w; n \<le> p\<rbrakk> \<Longrightarrow> w ! p = y; sset (drop n w @- sconst y) = {y}; Suc p < length w; n \<le> Suc p\<rbrakk> \<Longrightarrow> w ! Suc p = y
[PROOF STEP]
with Suc(1)[of 0 "tl w"]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>sset (drop 0 (tl w) @- sconst y) = {y}; p < length (tl w); 0 \<le> p\<rbrakk> \<Longrightarrow> tl w ! p = y
\<lbrakk>sset (drop ?n ?w @- sconst y) = {y}; p < length ?w; ?n \<le> p\<rbrakk> \<Longrightarrow> ?w ! p = y
sset (drop n w @- sconst y) = {y}
Suc p < length w
n \<le> Suc p
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>sset (drop 0 (tl w) @- sconst y) = {y}; p < length (tl w); 0 \<le> p\<rbrakk> \<Longrightarrow> tl w ! p = y
\<lbrakk>sset (drop ?n ?w @- sconst y) = {y}; p < length ?w; ?n \<le> p\<rbrakk> \<Longrightarrow> ?w ! p = y
sset (drop n w @- sconst y) = {y}
Suc p < length w
n \<le> Suc p

goal (1 subgoal):
 1. w ! Suc p = y
[PROOF STEP]
by (cases w n rule: list.exhaust[case_product nat.exhaust]) auto
[PROOF STATE]
proof (state)
this:
w ! Suc p = y

goal (1 subgoal):
 1. \<And>w n. \<lbrakk>sset (drop n w @- sconst y) = {y}; 0 < length w; n \<le> 0\<rbrakk> \<Longrightarrow> w ! 0 = y
[PROOF STEP]
qed (auto simp add: neq_Nil_conv)


[STATEMENT]
lemma less_length_cut_same:
  "\<lbrakk>(w @- sconst y) !! p = a\<rbrakk> \<Longrightarrow> a = y \<or> (p < length (cut_same y (w @- sconst y)) \<and> w ! p = a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (w @- sconst y) !! p = a \<Longrightarrow> a = y \<or> p < length (cut_same y (w @- sconst y)) \<and> w ! p = a
[PROOF STEP]
unfolding cut_same_def length_stake
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (w @- sconst y) !! p = a \<Longrightarrow> a = y \<or> p < (LEAST n. sdrop n (w @- sconst y) = sconst y) \<and> w ! p = a
[PROOF STEP]
by (rule LeastI2_ex[OF exI[of _ "length w"]])
    (auto simp: sdrop_shift shift_snth split: if_split_asm elim!: drop_sconstE)


[STATEMENT]
lemma less_length_cut_same_Inl:
  "\<lbrakk>(\<forall>x \<in> set I. case x of Inr P \<Rightarrow> finite P | _ \<Rightarrow> True); r < length I; I ! r = Inl p\<rbrakk> \<Longrightarrow>
  p < length (cut_same (any, replicate (length I) False) (stream_enc (w, I)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>set I. case x of Inl a \<Rightarrow> True | Inr P \<Rightarrow> finite P; r < length I; I ! r = Inl p\<rbrakk> \<Longrightarrow> p < length (cut_same (any, replicate (length I) False) (stream_enc (w, I)))
[PROOF STEP]
unfolding cut_same_def length_stake
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>set I. case x of Inl a \<Rightarrow> True | Inr P \<Rightarrow> finite P; r < length I; I ! r = Inl p\<rbrakk> \<Longrightarrow> p < (LEAST n. sdrop n (stream_enc (w, I)) = sconst (any, replicate (length I) False))
[PROOF STEP]
by (erule LeastI2_ex[OF ex_Loop_stream_enc ccontr],
    auto simp: smap2_alt list_eq_iff_nth_eq add.commute dest!: add_diff_inverse split: sum.splits,
    metis)


[STATEMENT]
lemma less_length_cut_same_Inr:
  "\<lbrakk>(\<forall>x \<in> set I. case x of Inr P \<Rightarrow> finite P | _ \<Rightarrow> True); r < length I; I ! r = Inr P\<rbrakk> \<Longrightarrow>
  \<forall>p \<in> P. p < length (cut_same (any, replicate (length I) False) (stream_enc (w, I)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>set I. case x of Inl a \<Rightarrow> True | Inr P \<Rightarrow> finite P; r < length I; I ! r = Inr P\<rbrakk> \<Longrightarrow> \<forall>p\<in>P. p < length (cut_same (any, replicate (length I) False) (stream_enc (w, I)))
[PROOF STEP]
unfolding cut_same_def length_stake
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>set I. case x of Inl a \<Rightarrow> True | Inr P \<Rightarrow> finite P; r < length I; I ! r = Inr P\<rbrakk> \<Longrightarrow> \<forall>p\<in>P. p < (LEAST n. sdrop n (stream_enc (w, I)) = sconst (any, replicate (length I) False))
[PROOF STEP]
by (rule ballI, erule LeastI2_ex[OF ex_Loop_stream_enc ccontr],
    auto simp: smap2_alt list_eq_iff_nth_eq add.commute dest!: add_diff_inverse split: sum.splits,
    metis)


[STATEMENT]
lemma cut_same_all[simp]: "cut_same x (sconst x) = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cut_same x (sconst x) = []
[PROOF STEP]
unfolding cut_same_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stake (LEAST n. sdrop n (sconst x) = sconst x) (sconst x) = []
[PROOF STEP]
by (auto intro: Least_equality)


[STATEMENT]
lemma cut_same_stop[simp]:
  assumes "x \<noteq> y"
  shows "cut_same x (xs @- y ## sconst x) = xs @ [y]" (is "cut_same x ?s = _")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cut_same x (xs @- y ## sconst x) = xs @ [y]
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cut_same x (xs @- y ## sconst x) = xs @ [y]
[PROOF STEP]
have "(LEAST n. sdrop n ?s = sconst x) = Suc (length xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST n. sdrop n (xs @- y ## sconst x) = sconst x) = Suc (length xs)
[PROOF STEP]
proof (rule Least_equality)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. sdrop (Suc (length xs)) (xs @- y ## sconst x) = sconst x
 2. \<And>ya. sdrop ya (xs @- y ## sconst x) = sconst x \<Longrightarrow> Suc (length xs) \<le> ya
[PROOF STEP]
show "sdrop (Suc (length xs)) ?s = sconst x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sdrop (Suc (length xs)) (xs @- y ## sconst x) = sconst x
[PROOF STEP]
by (auto simp: sdrop_shift)
[PROOF STATE]
proof (state)
this:
sdrop (Suc (length xs)) (xs @- y ## sconst x) = sconst x

goal (1 subgoal):
 1. \<And>ya. sdrop ya (xs @- y ## sconst x) = sconst x \<Longrightarrow> Suc (length xs) \<le> ya
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ya. sdrop ya (xs @- y ## sconst x) = sconst x \<Longrightarrow> Suc (length xs) \<le> ya
[PROOF STEP]
fix m
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ya. sdrop ya (xs @- y ## sconst x) = sconst x \<Longrightarrow> Suc (length xs) \<le> ya
[PROOF STEP]
assume *: "sdrop m ?s = sconst x"
[PROOF STATE]
proof (state)
this:
sdrop m (xs @- y ## sconst x) = sconst x

goal (1 subgoal):
 1. \<And>ya. sdrop ya (xs @- y ## sconst x) = sconst x \<Longrightarrow> Suc (length xs) \<le> ya
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
sdrop m (xs @- y ## sconst x) = sconst x

goal (1 subgoal):
 1. \<And>ya. sdrop ya (xs @- y ## sconst x) = sconst x \<Longrightarrow> Suc (length xs) \<le> ya
[PROOF STEP]
assume "m < Suc (length xs)"
[PROOF STATE]
proof (state)
this:
m < Suc (length xs)

goal (1 subgoal):
 1. \<And>ya. sdrop ya (xs @- y ## sconst x) = sconst x \<Longrightarrow> Suc (length xs) \<le> ya
[PROOF STEP]
hence "m \<le> length xs"
[PROOF STATE]
proof (prove)
using this:
m < Suc (length xs)

goal (1 subgoal):
 1. m \<le> length xs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
m \<le> length xs

goal (1 subgoal):
 1. \<And>ya. sdrop ya (xs @- y ## sconst x) = sconst x \<Longrightarrow> Suc (length xs) \<le> ya
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
m \<le> length xs
[PROOF STEP]
obtain ys where "sdrop m ?s = ys @- y ## sconst x"
[PROOF STATE]
proof (prove)
using this:
m \<le> length xs

goal (1 subgoal):
 1. (\<And>ys. sdrop m (xs @- y ## sconst x) = ys @- y ## sconst x \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by atomize_elim (induct m arbitrary: xs, auto)
[PROOF STATE]
proof (state)
this:
sdrop m (xs @- y ## sconst x) = ys @- y ## sconst x

goal (1 subgoal):
 1. \<And>ya. sdrop ya (xs @- y ## sconst x) = sconst x \<Longrightarrow> Suc (length xs) \<le> ya
[PROOF STEP]
with *
[PROOF STATE]
proof (chain)
picking this:
sdrop m (xs @- y ## sconst x) = sconst x
sdrop m (xs @- y ## sconst x) = ys @- y ## sconst x
[PROOF STEP]
obtain "ys @- y ## sconst x = sconst x"
[PROOF STATE]
proof (prove)
using this:
sdrop m (xs @- y ## sconst x) = sconst x
sdrop m (xs @- y ## sconst x) = ys @- y ## sconst x

goal (1 subgoal):
 1. (ys @- y ## sconst x = sconst x \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ys @- y ## sconst x = sconst x

goal (1 subgoal):
 1. \<And>ya. sdrop ya (xs @- y ## sconst x) = sconst x \<Longrightarrow> Suc (length xs) \<le> ya
[PROOF STEP]
from arg_cong[OF this, of "sdrop (length ys)"]
[PROOF STATE]
proof (chain)
picking this:
sdrop (length ys) (ys @- y ## sconst x) = sdrop (length ys) (sconst x)
[PROOF STEP]
have "y ## sconst x = sconst x"
[PROOF STATE]
proof (prove)
using this:
sdrop (length ys) (ys @- y ## sconst x) = sdrop (length ys) (sconst x)

goal (1 subgoal):
 1. y ## sconst x = sconst x
[PROOF STEP]
by (auto simp: sdrop_shift)
[PROOF STATE]
proof (state)
this:
y ## sconst x = sconst x

goal (1 subgoal):
 1. \<And>ya. sdrop ya (xs @- y ## sconst x) = sconst x \<Longrightarrow> Suc (length xs) \<le> ya
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> y
y ## sconst x = sconst x
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
x \<noteq> y
y ## sconst x = sconst x

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

goal (1 subgoal):
 1. \<And>ya. sdrop ya (xs @- y ## sconst x) = sconst x \<Longrightarrow> Suc (length xs) \<le> ya
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
m < Suc (length xs) \<Longrightarrow> False

goal (1 subgoal):
 1. \<And>ya. sdrop ya (xs @- y ## sconst x) = sconst x \<Longrightarrow> Suc (length xs) \<le> ya
[PROOF STEP]
thus "Suc (length xs) \<le> m"
[PROOF STATE]
proof (prove)
using this:
m < Suc (length xs) \<Longrightarrow> False

goal (1 subgoal):
 1. Suc (length xs) \<le> m
[PROOF STEP]
by (blast intro: leI)
[PROOF STATE]
proof (state)
this:
Suc (length xs) \<le> m

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(LEAST n. sdrop n (xs @- y ## sconst x) = sconst x) = Suc (length xs)

goal (1 subgoal):
 1. cut_same x (xs @- y ## sconst x) = xs @ [y]
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(LEAST n. sdrop n (xs @- y ## sconst x) = sconst x) = Suc (length xs)

goal (1 subgoal):
 1. cut_same x (xs @- y ## sconst x) = xs @ [y]
[PROOF STEP]
unfolding cut_same_def stake_shift
[PROOF STATE]
proof (prove)
using this:
(LEAST n. sdrop n (xs @- y ## sconst x) = sconst x) = Suc (length xs)

goal (1 subgoal):
 1. take (LEAST n. sdrop n (xs @- y ## sconst x) = sconst x) xs @ stake ((LEAST n. sdrop n (xs @- y ## sconst x) = sconst x) - length xs) (y ## sconst x) = xs @ [y]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cut_same x (xs @- y ## sconst x) = xs @ [y]

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cut_same_shift_sconst: "\<exists>n. w = cut_same x (w @- sconst x) @ replicate n x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n. w = cut_same x (w @- sconst x) @ replicate n x
[PROOF STEP]
proof (induct w rule: rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>n. [] = cut_same x ([] @- sconst x) @ replicate n x
 2. \<And>xa xs. \<exists>n. xs = cut_same x (xs @- sconst x) @ replicate n x \<Longrightarrow> \<exists>n. xs @ [xa] = cut_same x ((xs @ [xa]) @- sconst x) @ replicate n x
[PROOF STEP]
case (snoc a w)
[PROOF STATE]
proof (state)
this:
\<exists>n. w = cut_same x (w @- sconst x) @ replicate n x

goal (2 subgoals):
 1. \<exists>n. [] = cut_same x ([] @- sconst x) @ replicate n x
 2. \<And>xa xs. \<exists>n. xs = cut_same x (xs @- sconst x) @ replicate n x \<Longrightarrow> \<exists>n. xs @ [xa] = cut_same x ((xs @ [xa]) @- sconst x) @ replicate n x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>n. w = cut_same x (w @- sconst x) @ replicate n x
[PROOF STEP]
obtain n where "w = cut_same x (w @- sconst x) @ replicate n x"
[PROOF STATE]
proof (prove)
using this:
\<exists>n. w = cut_same x (w @- sconst x) @ replicate n x

goal (1 subgoal):
 1. (\<And>n. w = cut_same x (w @- sconst x) @ replicate n x \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
w = cut_same x (w @- sconst x) @ replicate n x

goal (2 subgoals):
 1. \<exists>n. [] = cut_same x ([] @- sconst x) @ replicate n x
 2. \<And>xa xs. \<exists>n. xs = cut_same x (xs @- sconst x) @ replicate n x \<Longrightarrow> \<exists>n. xs @ [xa] = cut_same x ((xs @ [xa]) @- sconst x) @ replicate n x
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
w = cut_same x (w @- sconst x) @ replicate n x

goal (1 subgoal):
 1. \<exists>n. w @ [a] = cut_same x ((w @ [a]) @- sconst x) @ replicate n x
[PROOF STEP]
by (cases "a = x")
     (auto simp: id_def[symmetric] siterate.code[of id, simplified id_apply, symmetric]
      replicate_append_same[symmetric] intro!: exI[of _ "Suc n"])
[PROOF STATE]
proof (state)
this:
\<exists>n. w @ [a] = cut_same x ((w @ [a]) @- sconst x) @ replicate n x

goal (1 subgoal):
 1. \<exists>n. [] = cut_same x ([] @- sconst x) @ replicate n x
[PROOF STEP]
qed (simp add: id_def[symmetric])


[STATEMENT]
lemma set_cut_same: "set (cut_same x (w @- sconst x)) \<subseteq> set w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (cut_same x (w @- sconst x)) \<subseteq> set w
[PROOF STEP]
proof (induct w rule: rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. set (cut_same x ([] @- sconst x)) \<subseteq> set []
 2. \<And>xa xs. set (cut_same x (xs @- sconst x)) \<subseteq> set xs \<Longrightarrow> set (cut_same x ((xs @ [xa]) @- sconst x)) \<subseteq> set (xs @ [xa])
[PROOF STEP]
case (snoc a w)
[PROOF STATE]
proof (state)
this:
set (cut_same x (w @- sconst x)) \<subseteq> set w

goal (2 subgoals):
 1. set (cut_same x ([] @- sconst x)) \<subseteq> set []
 2. \<And>xa xs. set (cut_same x (xs @- sconst x)) \<subseteq> set xs \<Longrightarrow> set (cut_same x ((xs @ [xa]) @- sconst x)) \<subseteq> set (xs @ [xa])
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
set (cut_same x (w @- sconst x)) \<subseteq> set w

goal (1 subgoal):
 1. set (cut_same x ((w @ [a]) @- sconst x)) \<subseteq> set (w @ [a])
[PROOF STEP]
by (cases "a = x")
    (auto simp: id_def[symmetric] siterate.code[of id, simplified id_apply, symmetric])
[PROOF STATE]
proof (state)
this:
set (cut_same x ((w @ [a]) @- sconst x)) \<subseteq> set (w @ [a])

goal (1 subgoal):
 1. set (cut_same x ([] @- sconst x)) \<subseteq> set []
[PROOF STEP]
qed  (simp add: id_def[symmetric])


[STATEMENT]
lemma stream_enc_cut_same:
  assumes "(\<forall>x \<in> set I. case x of Inr P \<Rightarrow> finite P | _ \<Rightarrow> True)"
  shows "stream_enc (w, I) = cut_same (any, replicate (length I) False) (stream_enc (w, I)) @-
    sconst (any, replicate (length I) False)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stream_enc (w, I) = cut_same (any, replicate (length I) False) (stream_enc (w, I)) @- sconst (any, replicate (length I) False)
[PROOF STEP]
unfolding cut_same_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stream_enc (w, I) = stake (LEAST n. sdrop n (stream_enc (w, I)) = sconst (any, replicate (length I) False)) (stream_enc (w, I)) @- sconst (any, replicate (length I) False)
[PROOF STEP]
by (rule trans[OF sym[OF stake_sdrop] arg_cong2[of _ _ _ _ "(@-)", OF refl]])
     (rule LeastI_ex[OF ex_Loop_stream_enc[OF assms]])


[STATEMENT]
lemma stream_enc_enc:
  assumes "(\<forall>x \<in> set I. case x of Inr P \<Rightarrow> finite P | _ \<Rightarrow> True)" and  v: "v \<in> enc (w, I)"
  shows "stream_enc (w, I) = v @- sconst (any, replicate (length I) False)"
  (is "?s = ?v @- sconst ?F")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stream_enc (w, I) = v @- sconst (any, replicate (length I) False)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. stream_enc (w, I) = v @- sconst (any, replicate (length I) False)
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>set I. case x of Inl a \<Rightarrow> True | Inr P \<Rightarrow> finite P
[PROOF STEP]
obtain n where "sdrop n (stream_enc (w, I)) = sconst ?F"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set I. case x of Inl a \<Rightarrow> True | Inr P \<Rightarrow> finite P

goal (1 subgoal):
 1. (\<And>n. sdrop n (stream_enc (w, I)) = sconst (any, replicate (length I) False) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis ex_Loop_stream_enc)
[PROOF STATE]
proof (state)
this:
sdrop n (stream_enc (w, I)) = sconst (any, replicate (length I) False)

goal (1 subgoal):
 1. stream_enc (w, I) = v @- sconst (any, replicate (length I) False)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sdrop n (stream_enc (w, I)) = sconst (any, replicate (length I) False)

goal (1 subgoal):
 1. stream_enc (w, I) = v @- sconst (any, replicate (length I) False)
[PROOF STEP]
from v
[PROOF STATE]
proof (chain)
picking this:
v \<in> enc (w, I)
[PROOF STEP]
obtain m where "?v = cut_same ?F ?s @ replicate m ?F"
[PROOF STATE]
proof (prove)
using this:
v \<in> enc (w, I)

goal (1 subgoal):
 1. (\<And>m. v = cut_same (any, replicate (length I) False) (stream_enc (w, I)) @ replicate m (any, replicate (length I) False) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v = cut_same (any, replicate (length I) False) (stream_enc (w, I)) @ replicate m (any, replicate (length I) False)

goal (1 subgoal):
 1. stream_enc (w, I) = v @- sconst (any, replicate (length I) False)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
sdrop n (stream_enc (w, I)) = sconst (any, replicate (length I) False)
v = cut_same (any, replicate (length I) False) (stream_enc (w, I)) @ replicate m (any, replicate (length I) False)
[PROOF STEP]
show "?s = v @- sconst ?F"
[PROOF STATE]
proof (prove)
using this:
sdrop n (stream_enc (w, I)) = sconst (any, replicate (length I) False)
v = cut_same (any, replicate (length I) False) (stream_enc (w, I)) @ replicate m (any, replicate (length I) False)

goal (1 subgoal):
 1. stream_enc (w, I) = v @- sconst (any, replicate (length I) False)
[PROOF STEP]
by (auto simp del: stream_enc.simps intro: stream_enc_cut_same[OF assms(1)])
[PROOF STATE]
proof (state)
this:
stream_enc (w, I) = v @- sconst (any, replicate (length I) False)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma stream_enc_enc_some:
  assumes "(\<forall>x \<in> set I. case x of Inr P \<Rightarrow> finite P | _ \<Rightarrow> True)"
  shows "stream_enc (w, I) = (SOME v. v \<in> enc (w, I)) @- sconst (any, replicate (length I) False)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stream_enc (w, I) = (SOME v. v \<in> enc (w, I)) @- sconst (any, replicate (length I) False)
[PROOF STEP]
by (rule stream_enc_enc[OF assms], rule someI_ex) auto


[STATEMENT]
lemma enc_unique_length: "v \<in> enc (w, I) \<Longrightarrow> \<forall>v'. length v' = length v \<and> v' \<in> enc (w, I) \<longrightarrow> v = v'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> enc (w, I) \<Longrightarrow> \<forall>v'. length v' = length v \<and> v' \<in> enc (w, I) \<longrightarrow> v = v'
[PROOF STEP]
by auto


[STATEMENT]
lemma sdrop_sconst: "sdrop n s = sconst x \<Longrightarrow> n \<le> m \<Longrightarrow> s !! m = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sdrop n s = sconst x; n \<le> m\<rbrakk> \<Longrightarrow> s !! m = x
[PROOF STEP]
by (metis le_iff_add sdrop_snth snth_siterate[of id, simplified id_funpow id_apply])


[STATEMENT]
lemma fin_cut_same_tl:
  assumes "\<exists>n. sdrop n s = sconst x"
  shows "fin_cut_same (\<pi> x) (map \<pi> (cut_same x s)) = cut_same (\<pi> x) (smap \<pi> s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fin_cut_same (\<pi> x) (map \<pi> (cut_same x s)) = cut_same (\<pi> x) (smap \<pi> s)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fin_cut_same (\<pi> x) (map \<pi> (cut_same x s)) = cut_same (\<pi> x) (smap \<pi> s)
[PROOF STEP]
define min where "min = (LEAST n. sdrop n s = sconst x)"
[PROOF STATE]
proof (state)
this:
min = (LEAST n. sdrop n s = sconst x)

goal (1 subgoal):
 1. fin_cut_same (\<pi> x) (map \<pi> (cut_same x s)) = cut_same (\<pi> x) (smap \<pi> s)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<exists>n. sdrop n s = sconst x
[PROOF STEP]
have min: "sdrop min s = sconst x" "\<And>m. sdrop m s = sconst x \<Longrightarrow> min \<le> m"
[PROOF STATE]
proof (prove)
using this:
\<exists>n. sdrop n s = sconst x

goal (1 subgoal):
 1. sdrop min s = sconst x &&& (\<And>m. sdrop m s = sconst x \<Longrightarrow> min \<le> m)
[PROOF STEP]
unfolding min_def
[PROOF STATE]
proof (prove)
using this:
\<exists>n. sdrop n s = sconst x

goal (1 subgoal):
 1. sdrop (LEAST n. sdrop n s = sconst x) s = sconst x &&& (\<And>m. sdrop m s = sconst x \<Longrightarrow> (LEAST n. sdrop n s = sconst x) \<le> m)
[PROOF STEP]
by (auto intro: LeastI Least_le)
[PROOF STATE]
proof (state)
this:
sdrop min s = sconst x
sdrop ?m s = sconst x \<Longrightarrow> min \<le> ?m

goal (1 subgoal):
 1. fin_cut_same (\<pi> x) (map \<pi> (cut_same x s)) = cut_same (\<pi> x) (smap \<pi> s)
[PROOF STEP]
have Ex: "\<exists>n. drop n (map \<pi> (stake min s)) = replicate (length (map \<pi> (stake min s)) - n) (\<pi> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n. drop n (map \<pi> (stake min s)) = replicate (length (map \<pi> (stake min s)) - n) (\<pi> x)
[PROOF STEP]
by (auto intro: exI[of _ "length (map \<pi> (stake min s))"])
[PROOF STATE]
proof (state)
this:
\<exists>n. drop n (map \<pi> (stake min s)) = replicate (length (map \<pi> (stake min s)) - n) (\<pi> x)

goal (1 subgoal):
 1. fin_cut_same (\<pi> x) (map \<pi> (cut_same x s)) = cut_same (\<pi> x) (smap \<pi> s)
[PROOF STEP]
have "fin_cut_same (\<pi> x) (map \<pi> (cut_same x s)) =
     map \<pi> (stake  (LEAST n.
       map \<pi> (stake (min - n) (sdrop n s)) = replicate (min - n) (\<pi> x) \<or> sdrop n s = sconst x) s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fin_cut_same (\<pi> x) (map \<pi> (cut_same x s)) = map \<pi> (stake (LEAST n. map \<pi> (stake (min - n) (sdrop n s)) = replicate (min - n) (\<pi> x) \<or> sdrop n s = sconst x) s)
[PROOF STEP]
unfolding fin_cut_same_def cut_same_def take_map take_stake min_Least[OF Ex assms, folded min_def]
      min_def[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map \<pi> (stake (LEAST n. drop n (map \<pi> (stake min s)) = replicate (length (map \<pi> (stake min s)) - n) (\<pi> x) \<or> sdrop n s = sconst x) s) = map \<pi> (stake (LEAST n. map \<pi> (stake (min - n) (sdrop n s)) = replicate (min - n) (\<pi> x) \<or> sdrop n s = sconst x) s)
[PROOF STEP]
by (auto simp: drop_map drop_stake)
[PROOF STATE]
proof (state)
this:
fin_cut_same (\<pi> x) (map \<pi> (cut_same x s)) = map \<pi> (stake (LEAST n. map \<pi> (stake (min - n) (sdrop n s)) = replicate (min - n) (\<pi> x) \<or> sdrop n s = sconst x) s)

goal (1 subgoal):
 1. fin_cut_same (\<pi> x) (map \<pi> (cut_same x s)) = cut_same (\<pi> x) (smap \<pi> s)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
fin_cut_same (\<pi> x) (map \<pi> (cut_same x s)) = map \<pi> (stake (LEAST n. map \<pi> (stake (min - n) (sdrop n s)) = replicate (min - n) (\<pi> x) \<or> sdrop n s = sconst x) s)

goal (1 subgoal):
 1. fin_cut_same (\<pi> x) (map \<pi> (cut_same x s)) = cut_same (\<pi> x) (smap \<pi> s)
[PROOF STEP]
have "(\<lambda>n. map \<pi> (stake (min - n) (sdrop n s)) = replicate (min - n) (\<pi> x) \<or> sdrop n s = sconst x) =
     (\<lambda>n. smap \<pi> (sdrop n s) = sconst (\<pi> x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. map \<pi> (stake (min - n) (sdrop n s)) = replicate (min - n) (\<pi> x) \<or> sdrop n s = sconst x) = (\<lambda>n. smap \<pi> (sdrop n s) = sconst (\<pi> x))
[PROOF STEP]
proof (rule ext, unfold smap_alt snth_siterate[of id, simplified id_funpow id_apply], safe)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>n na. map \<pi> (stake (min - n) (sdrop n s)) = replicate (min - n) (\<pi> x) \<Longrightarrow> \<pi> (sdrop n s !! na) = \<pi> x
 2. \<And>n na. sdrop n s = sconst x \<Longrightarrow> \<pi> (sdrop n s !! na) = \<pi> x
 3. \<And>n. \<lbrakk>\<forall>na. \<pi> (sdrop n s !! na) = \<pi> x; sdrop n s \<noteq> sconst x\<rbrakk> \<Longrightarrow> map \<pi> (stake (min - n) (sdrop n s)) = replicate (min - n) (\<pi> x)
[PROOF STEP]
fix n m
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>n na. map \<pi> (stake (min - n) (sdrop n s)) = replicate (min - n) (\<pi> x) \<Longrightarrow> \<pi> (sdrop n s !! na) = \<pi> x
 2. \<And>n na. sdrop n s = sconst x \<Longrightarrow> \<pi> (sdrop n s !! na) = \<pi> x
 3. \<And>n. \<lbrakk>\<forall>na. \<pi> (sdrop n s !! na) = \<pi> x; sdrop n s \<noteq> sconst x\<rbrakk> \<Longrightarrow> map \<pi> (stake (min - n) (sdrop n s)) = replicate (min - n) (\<pi> x)
[PROOF STEP]
assume "map \<pi> (stake (min - n) (sdrop n s)) = replicate (min - n) (\<pi> x)"
[PROOF STATE]
proof (state)
this:
map \<pi> (stake (min - n) (sdrop n s)) = replicate (min - n) (\<pi> x)

goal (3 subgoals):
 1. \<And>n na. map \<pi> (stake (min - n) (sdrop n s)) = replicate (min - n) (\<pi> x) \<Longrightarrow> \<pi> (sdrop n s !! na) = \<pi> x
 2. \<And>n na. sdrop n s = sconst x \<Longrightarrow> \<pi> (sdrop n s !! na) = \<pi> x
 3. \<And>n. \<lbrakk>\<forall>na. \<pi> (sdrop n s !! na) = \<pi> x; sdrop n s \<noteq> sconst x\<rbrakk> \<Longrightarrow> map \<pi> (stake (min - n) (sdrop n s)) = replicate (min - n) (\<pi> x)
[PROOF STEP]
hence "\<forall>y\<in>set (stake (min - n) (sdrop n s)). \<pi> y = \<pi> x"
[PROOF STATE]
proof (prove)
using this:
map \<pi> (stake (min - n) (sdrop n s)) = replicate (min - n) (\<pi> x)

goal (1 subgoal):
 1. \<forall>y\<in>set (stake (min - n) (sdrop n s)). \<pi> y = \<pi> x
[PROOF STEP]
by (intro iffD1[OF map_eq_conv]) (metis length_stake map_replicate_const)
[PROOF STATE]
proof (state)
this:
\<forall>y\<in>set (stake (min - n) (sdrop n s)). \<pi> y = \<pi> x

goal (3 subgoals):
 1. \<And>n na. map \<pi> (stake (min - n) (sdrop n s)) = replicate (min - n) (\<pi> x) \<Longrightarrow> \<pi> (sdrop n s !! na) = \<pi> x
 2. \<And>n na. sdrop n s = sconst x \<Longrightarrow> \<pi> (sdrop n s !! na) = \<pi> x
 3. \<And>n. \<lbrakk>\<forall>na. \<pi> (sdrop n s !! na) = \<pi> x; sdrop n s \<noteq> sconst x\<rbrakk> \<Longrightarrow> map \<pi> (stake (min - n) (sdrop n s)) = replicate (min - n) (\<pi> x)
[PROOF STEP]
hence "\<forall>i<min - n. \<pi> (sdrop n s !! i) = \<pi> x"
[PROOF STATE]
proof (prove)
using this:
\<forall>y\<in>set (stake (min - n) (sdrop n s)). \<pi> y = \<pi> x

goal (1 subgoal):
 1. \<forall>i<min - n. \<pi> (sdrop n s !! i) = \<pi> x
[PROOF STEP]
unfolding all_set_conv_all_nth
[PROOF STATE]
proof (prove)
using this:
\<forall>i<length (stake (min - n) (sdrop n s)). \<pi> (stake (min - n) (sdrop n s) ! i) = \<pi> x

goal (1 subgoal):
 1. \<forall>i<min - n. \<pi> (sdrop n s !! i) = \<pi> x
[PROOF STEP]
by (auto simp: sdrop_snth)
[PROOF STATE]
proof (state)
this:
\<forall>i<min - n. \<pi> (sdrop n s !! i) = \<pi> x

goal (3 subgoals):
 1. \<And>n na. map \<pi> (stake (min - n) (sdrop n s)) = replicate (min - n) (\<pi> x) \<Longrightarrow> \<pi> (sdrop n s !! na) = \<pi> x
 2. \<And>n na. sdrop n s = sconst x \<Longrightarrow> \<pi> (sdrop n s !! na) = \<pi> x
 3. \<And>n. \<lbrakk>\<forall>na. \<pi> (sdrop n s !! na) = \<pi> x; sdrop n s \<noteq> sconst x\<rbrakk> \<Longrightarrow> map \<pi> (stake (min - n) (sdrop n s)) = replicate (min - n) (\<pi> x)
[PROOF STEP]
thus "\<pi> (sdrop n s !! m) = \<pi> x"
[PROOF STATE]
proof (prove)
using this:
\<forall>i<min - n. \<pi> (sdrop n s !! i) = \<pi> x

goal (1 subgoal):
 1. \<pi> (sdrop n s !! m) = \<pi> x
[PROOF STEP]
proof (cases "m < min - n")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<forall>i<min - n. \<pi> (sdrop n s !! i) = \<pi> x; m < min - n\<rbrakk> \<Longrightarrow> \<pi> (sdrop n s !! m) = \<pi> x
 2. \<lbrakk>\<forall>i<min - n. \<pi> (sdrop n s !! i) = \<pi> x; \<not> m < min - n\<rbrakk> \<Longrightarrow> \<pi> (sdrop n s !! m) = \<pi> x
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> m < min - n

goal (2 subgoals):
 1. \<lbrakk>\<forall>i<min - n. \<pi> (sdrop n s !! i) = \<pi> x; m < min - n\<rbrakk> \<Longrightarrow> \<pi> (sdrop n s !! m) = \<pi> x
 2. \<lbrakk>\<forall>i<min - n. \<pi> (sdrop n s !! i) = \<pi> x; \<not> m < min - n\<rbrakk> \<Longrightarrow> \<pi> (sdrop n s !! m) = \<pi> x
[PROOF STEP]
hence "min \<le> n + m"
[PROOF STATE]
proof (prove)
using this:
\<not> m < min - n

goal (1 subgoal):
 1. min \<le> n + m
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
min \<le> n + m

goal (2 subgoals):
 1. \<lbrakk>\<forall>i<min - n. \<pi> (sdrop n s !! i) = \<pi> x; m < min - n\<rbrakk> \<Longrightarrow> \<pi> (sdrop n s !! m) = \<pi> x
 2. \<lbrakk>\<forall>i<min - n. \<pi> (sdrop n s !! i) = \<pi> x; \<not> m < min - n\<rbrakk> \<Longrightarrow> \<pi> (sdrop n s !! m) = \<pi> x
[PROOF STEP]
hence "sdrop n s !! m = x"
[PROOF STATE]
proof (prove)
using this:
min \<le> n + m

goal (1 subgoal):
 1. sdrop n s !! m = x
[PROOF STEP]
unfolding sdrop_snth
[PROOF STATE]
proof (prove)
using this:
min \<le> n + m

goal (1 subgoal):
 1. s !! (n + m) = x
[PROOF STEP]
by (rule sdrop_sconst[OF min(1)])
[PROOF STATE]
proof (state)
this:
sdrop n s !! m = x

goal (2 subgoals):
 1. \<lbrakk>\<forall>i<min - n. \<pi> (sdrop n s !! i) = \<pi> x; m < min - n\<rbrakk> \<Longrightarrow> \<pi> (sdrop n s !! m) = \<pi> x
 2. \<lbrakk>\<forall>i<min - n. \<pi> (sdrop n s !! i) = \<pi> x; \<not> m < min - n\<rbrakk> \<Longrightarrow> \<pi> (sdrop n s !! m) = \<pi> x
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
sdrop n s !! m = x

goal (1 subgoal):
 1. \<pi> (sdrop n s !! m) = \<pi> x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<pi> (sdrop n s !! m) = \<pi> x

goal (1 subgoal):
 1. \<lbrakk>\<forall>i<min - n. \<pi> (sdrop n s !! i) = \<pi> x; m < min - n\<rbrakk> \<Longrightarrow> \<pi> (sdrop n s !! m) = \<pi> x
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
\<pi> (sdrop n s !! m) = \<pi> x

goal (2 subgoals):
 1. \<And>n na. sdrop n s = sconst x \<Longrightarrow> \<pi> (sdrop n s !! na) = \<pi> x
 2. \<And>n. \<lbrakk>\<forall>na. \<pi> (sdrop n s !! na) = \<pi> x; sdrop n s \<noteq> sconst x\<rbrakk> \<Longrightarrow> map \<pi> (stake (min - n) (sdrop n s)) = replicate (min - n) (\<pi> x)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n na. sdrop n s = sconst x \<Longrightarrow> \<pi> (sdrop n s !! na) = \<pi> x
 2. \<And>n. \<lbrakk>\<forall>na. \<pi> (sdrop n s !! na) = \<pi> x; sdrop n s \<noteq> sconst x\<rbrakk> \<Longrightarrow> map \<pi> (stake (min - n) (sdrop n s)) = replicate (min - n) (\<pi> x)
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n na. sdrop n s = sconst x \<Longrightarrow> \<pi> (sdrop n s !! na) = \<pi> x
 2. \<And>n. \<lbrakk>\<forall>na. \<pi> (sdrop n s !! na) = \<pi> x; sdrop n s \<noteq> sconst x\<rbrakk> \<Longrightarrow> map \<pi> (stake (min - n) (sdrop n s)) = replicate (min - n) (\<pi> x)
[PROOF STEP]
assume "\<forall>m. \<pi> (sdrop n s !! m) = \<pi> x"
[PROOF STATE]
proof (state)
this:
\<forall>m. \<pi> (sdrop n s !! m) = \<pi> x

goal (2 subgoals):
 1. \<And>n na. sdrop n s = sconst x \<Longrightarrow> \<pi> (sdrop n s !! na) = \<pi> x
 2. \<And>n. \<lbrakk>\<forall>na. \<pi> (sdrop n s !! na) = \<pi> x; sdrop n s \<noteq> sconst x\<rbrakk> \<Longrightarrow> map \<pi> (stake (min - n) (sdrop n s)) = replicate (min - n) (\<pi> x)
[PROOF STEP]
thus "map \<pi> (stake (min - n) (sdrop n s)) = replicate (min - n) (\<pi> x)"
[PROOF STATE]
proof (prove)
using this:
\<forall>m. \<pi> (sdrop n s !! m) = \<pi> x

goal (1 subgoal):
 1. map \<pi> (stake (min - n) (sdrop n s)) = replicate (min - n) (\<pi> x)
[PROOF STEP]
unfolding stake_smap[symmetric] smap_alt[symmetric, of \<pi> "sdrop n s" "sconst (\<pi> x)", simplified]
[PROOF STATE]
proof (prove)
using this:
smap \<pi> (sdrop n s) = sconst (\<pi> x)

goal (1 subgoal):
 1. stake (min - n) (smap \<pi> (sdrop n s)) = replicate (min - n) (\<pi> x)
[PROOF STEP]
by (auto simp: map_replicate_const)
[PROOF STATE]
proof (state)
this:
map \<pi> (stake (min - n) (sdrop n s)) = replicate (min - n) (\<pi> x)

goal (1 subgoal):
 1. \<And>n na. sdrop n s = sconst x \<Longrightarrow> \<pi> (sdrop n s !! na) = \<pi> x
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
(\<lambda>n. map \<pi> (stake (min - n) (sdrop n s)) = replicate (min - n) (\<pi> x) \<or> sdrop n s = sconst x) = (\<lambda>n. smap \<pi> (sdrop n s) = sconst (\<pi> x))

goal (1 subgoal):
 1. fin_cut_same (\<pi> x) (map \<pi> (cut_same x s)) = cut_same (\<pi> x) (smap \<pi> s)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
fin_cut_same (\<pi> x) (map \<pi> (cut_same x s)) = map \<pi> (stake (LEAST n. smap \<pi> (sdrop n s) = sconst (\<pi> x)) s)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
fin_cut_same (\<pi> x) (map \<pi> (cut_same x s)) = map \<pi> (stake (LEAST n. smap \<pi> (sdrop n s) = sconst (\<pi> x)) s)

goal (1 subgoal):
 1. fin_cut_same (\<pi> x) (map \<pi> (cut_same x s)) = cut_same (\<pi> x) (smap \<pi> s)
[PROOF STEP]
unfolding cut_same_def sdrop_smap stake_smap
[PROOF STATE]
proof (prove)
using this:
fin_cut_same (\<pi> x) (map \<pi> (stake (LEAST n. sdrop n s = sconst x) s)) = map \<pi> (stake (LEAST n. smap \<pi> (sdrop n s) = sconst (\<pi> x)) s)

goal (1 subgoal):
 1. fin_cut_same (\<pi> x) (map \<pi> (stake (LEAST n. sdrop n s = sconst x) s)) = map \<pi> (stake (LEAST n. smap \<pi> (sdrop n s) = sconst (\<pi> x)) s)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
fin_cut_same (\<pi> x) (map \<pi> (cut_same x s)) = cut_same (\<pi> x) (smap \<pi> s)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma tl_enc[simp]:
  assumes "\<forall>x \<in> set (x # I). case x of Inr P \<Rightarrow> finite P | _ \<Rightarrow> True"
  shows "SAMEQUOT (any, replicate (length I) False) (map \<pi> ` enc (w, x # I)) = enc (w, I)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SAMEQUOT (any, replicate (length I) False) (map \<pi> ` enc (w, x # I)) = enc (w, I)
[PROOF STEP]
unfolding SAMEQUOT_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {fin_cut_same (any, replicate (length I) False) xa @ replicate m (any, replicate (length I) False) |xa m. xa \<in> map \<pi> ` enc (w, x # I)} = enc (w, I)
[PROOF STEP]
by (fastforce simp: assms \<pi>_def
    fin_cut_same_tl[OF ex_Loop_stream_enc[OF assms], unfolded \<pi>_def, simplified, symmetric])