[STATEMENT]
lemma beta_imp_beta_norm: assumes "t \<rightarrow>\<^sub>\<beta> t'" "\<not> beta_reducible t'" shows "beta_norm t = Some t'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. beta_norm t = Some t'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
t \<rightarrow>\<^sub>\<beta> t'
\<not> beta_reducible t'

goal (1 subgoal):
 1. beta_norm t = Some t'
[PROOF STEP]
proof (induction rule: beta.induct)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>T s t. \<not> beta_reducible (subst_bv2 s 0 t) \<Longrightarrow> beta_norm (Abs T s $ t) = Some (subst_bv2 s 0 t)
 2. \<And>s t u. \<lbrakk>s \<rightarrow>\<^sub>\<beta> t; \<not> beta_reducible t \<Longrightarrow> beta_norm s = Some t; \<not> beta_reducible (t $ u)\<rbrakk> \<Longrightarrow> beta_norm (s $ u) = Some (t $ u)
 3. \<And>s t u. \<lbrakk>s \<rightarrow>\<^sub>\<beta> t; \<not> beta_reducible t \<Longrightarrow> beta_norm s = Some t; \<not> beta_reducible (u $ t)\<rbrakk> \<Longrightarrow> beta_norm (u $ s) = Some (u $ t)
 4. \<And>s t T. \<lbrakk>s \<rightarrow>\<^sub>\<beta> t; \<not> beta_reducible t \<Longrightarrow> beta_norm s = Some t; \<not> beta_reducible (Abs T t)\<rbrakk> \<Longrightarrow> beta_norm (Abs T s) = Some (Abs T t)
[PROOF STEP]
case (beta T s t)
[PROOF STATE]
proof (state)
this:
\<not> beta_reducible (subst_bv2 s 0 t)

goal (4 subgoals):
 1. \<And>T s t. \<not> beta_reducible (subst_bv2 s 0 t) \<Longrightarrow> beta_norm (Abs T s $ t) = Some (subst_bv2 s 0 t)
 2. \<And>s t u. \<lbrakk>s \<rightarrow>\<^sub>\<beta> t; \<not> beta_reducible t \<Longrightarrow> beta_norm s = Some t; \<not> beta_reducible (t $ u)\<rbrakk> \<Longrightarrow> beta_norm (s $ u) = Some (t $ u)
 3. \<And>s t u. \<lbrakk>s \<rightarrow>\<^sub>\<beta> t; \<not> beta_reducible t \<Longrightarrow> beta_norm s = Some t; \<not> beta_reducible (u $ t)\<rbrakk> \<Longrightarrow> beta_norm (u $ s) = Some (u $ t)
 4. \<And>s t T. \<lbrakk>s \<rightarrow>\<^sub>\<beta> t; \<not> beta_reducible t \<Longrightarrow> beta_norm s = Some t; \<not> beta_reducible (Abs T t)\<rbrakk> \<Longrightarrow> beta_norm (Abs T s) = Some (Abs T t)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> beta_reducible (subst_bv2 s 0 t)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<not> beta_reducible (subst_bv2 s 0 t)

goal (1 subgoal):
 1. beta_norm (Abs T s $ t) = Some (subst_bv2 s 0 t)
[PROOF STEP]
using not_beta_reducible_imp_beta_norm_unchanged
[PROOF STATE]
proof (prove)
using this:
\<not> beta_reducible (subst_bv2 s 0 t)
\<not> beta_reducible ?t \<Longrightarrow> beta_norm ?t = Some ?t

goal (1 subgoal):
 1. beta_norm (Abs T s $ t) = Some (subst_bv2 s 0 t)
[PROOF STEP]
by (auto simp add: subst_bv_def substn_subst_n)
[PROOF STATE]
proof (state)
this:
beta_norm (Abs T s $ t) = Some (subst_bv2 s 0 t)

goal (3 subgoals):
 1. \<And>s t u. \<lbrakk>s \<rightarrow>\<^sub>\<beta> t; \<not> beta_reducible t \<Longrightarrow> beta_norm s = Some t; \<not> beta_reducible (t $ u)\<rbrakk> \<Longrightarrow> beta_norm (s $ u) = Some (t $ u)
 2. \<And>s t u. \<lbrakk>s \<rightarrow>\<^sub>\<beta> t; \<not> beta_reducible t \<Longrightarrow> beta_norm s = Some t; \<not> beta_reducible (u $ t)\<rbrakk> \<Longrightarrow> beta_norm (u $ s) = Some (u $ t)
 3. \<And>s t T. \<lbrakk>s \<rightarrow>\<^sub>\<beta> t; \<not> beta_reducible t \<Longrightarrow> beta_norm s = Some t; \<not> beta_reducible (Abs T t)\<rbrakk> \<Longrightarrow> beta_norm (Abs T s) = Some (Abs T t)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>s t u. \<lbrakk>s \<rightarrow>\<^sub>\<beta> t; \<not> beta_reducible t \<Longrightarrow> beta_norm s = Some t; \<not> beta_reducible (t $ u)\<rbrakk> \<Longrightarrow> beta_norm (s $ u) = Some (t $ u)
 2. \<And>s t u. \<lbrakk>s \<rightarrow>\<^sub>\<beta> t; \<not> beta_reducible t \<Longrightarrow> beta_norm s = Some t; \<not> beta_reducible (u $ t)\<rbrakk> \<Longrightarrow> beta_norm (u $ s) = Some (u $ t)
 3. \<And>s t T. \<lbrakk>s \<rightarrow>\<^sub>\<beta> t; \<not> beta_reducible t \<Longrightarrow> beta_norm s = Some t; \<not> beta_reducible (Abs T t)\<rbrakk> \<Longrightarrow> beta_norm (Abs T s) = Some (Abs T t)
[PROOF STEP]
case (appL s t u)
[PROOF STATE]
proof (state)
this:
s \<rightarrow>\<^sub>\<beta> t
\<not> beta_reducible t \<Longrightarrow> beta_norm s = Some t
\<not> beta_reducible (t $ u)

goal (3 subgoals):
 1. \<And>s t u. \<lbrakk>s \<rightarrow>\<^sub>\<beta> t; \<not> beta_reducible t \<Longrightarrow> beta_norm s = Some t; \<not> beta_reducible (t $ u)\<rbrakk> \<Longrightarrow> beta_norm (s $ u) = Some (t $ u)
 2. \<And>s t u. \<lbrakk>s \<rightarrow>\<^sub>\<beta> t; \<not> beta_reducible t \<Longrightarrow> beta_norm s = Some t; \<not> beta_reducible (u $ t)\<rbrakk> \<Longrightarrow> beta_norm (u $ s) = Some (u $ t)
 3. \<And>s t T. \<lbrakk>s \<rightarrow>\<^sub>\<beta> t; \<not> beta_reducible t \<Longrightarrow> beta_norm s = Some t; \<not> beta_reducible (Abs T t)\<rbrakk> \<Longrightarrow> beta_norm (Abs T s) = Some (Abs T t)
[PROOF STEP]
hence t: "\<not> beta_reducible t"
[PROOF STATE]
proof (prove)
using this:
s \<rightarrow>\<^sub>\<beta> t
\<not> beta_reducible t \<Longrightarrow> beta_norm s = Some t
\<not> beta_reducible (t $ u)

goal (1 subgoal):
 1. \<not> beta_reducible t
[PROOF STEP]
by (fastforce elim: beta_reducible.elims)
[PROOF STATE]
proof (state)
this:
\<not> beta_reducible t

goal (3 subgoals):
 1. \<And>s t u. \<lbrakk>s \<rightarrow>\<^sub>\<beta> t; \<not> beta_reducible t \<Longrightarrow> beta_norm s = Some t; \<not> beta_reducible (t $ u)\<rbrakk> \<Longrightarrow> beta_norm (s $ u) = Some (t $ u)
 2. \<And>s t u. \<lbrakk>s \<rightarrow>\<^sub>\<beta> t; \<not> beta_reducible t \<Longrightarrow> beta_norm s = Some t; \<not> beta_reducible (u $ t)\<rbrakk> \<Longrightarrow> beta_norm (u $ s) = Some (u $ t)
 3. \<And>s t T. \<lbrakk>s \<rightarrow>\<^sub>\<beta> t; \<not> beta_reducible t \<Longrightarrow> beta_norm s = Some t; \<not> beta_reducible (Abs T t)\<rbrakk> \<Longrightarrow> beta_norm (Abs T s) = Some (Abs T t)
[PROOF STEP]
hence IH: "beta_norm s = Some t"
[PROOF STATE]
proof (prove)
using this:
\<not> beta_reducible t

goal (1 subgoal):
 1. beta_norm s = Some t
[PROOF STEP]
using appL.IH
[PROOF STATE]
proof (prove)
using this:
\<not> beta_reducible t
\<not> beta_reducible t \<Longrightarrow> beta_norm s = Some t

goal (1 subgoal):
 1. beta_norm s = Some t
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
beta_norm s = Some t

goal (3 subgoals):
 1. \<And>s t u. \<lbrakk>s \<rightarrow>\<^sub>\<beta> t; \<not> beta_reducible t \<Longrightarrow> beta_norm s = Some t; \<not> beta_reducible (t $ u)\<rbrakk> \<Longrightarrow> beta_norm (s $ u) = Some (t $ u)
 2. \<And>s t u. \<lbrakk>s \<rightarrow>\<^sub>\<beta> t; \<not> beta_reducible t \<Longrightarrow> beta_norm s = Some t; \<not> beta_reducible (u $ t)\<rbrakk> \<Longrightarrow> beta_norm (u $ s) = Some (u $ t)
 3. \<And>s t T. \<lbrakk>s \<rightarrow>\<^sub>\<beta> t; \<not> beta_reducible t \<Longrightarrow> beta_norm s = Some t; \<not> beta_reducible (Abs T t)\<rbrakk> \<Longrightarrow> beta_norm (Abs T s) = Some (Abs T t)
[PROOF STEP]
from appL
[PROOF STATE]
proof (chain)
picking this:
s \<rightarrow>\<^sub>\<beta> t
\<not> beta_reducible t \<Longrightarrow> beta_norm s = Some t
\<not> beta_reducible (t $ u)
[PROOF STEP]
have u: "\<not> beta_reducible u"
[PROOF STATE]
proof (prove)
using this:
s \<rightarrow>\<^sub>\<beta> t
\<not> beta_reducible t \<Longrightarrow> beta_norm s = Some t
\<not> beta_reducible (t $ u)

goal (1 subgoal):
 1. \<not> beta_reducible u
[PROOF STEP]
using beta_reducible.elims
[PROOF STATE]
proof (prove)
using this:
s \<rightarrow>\<^sub>\<beta> t
\<not> beta_reducible t \<Longrightarrow> beta_norm s = Some t
\<not> beta_reducible (t $ u)
\<lbrakk>beta_reducible ?x = ?y; \<And>uu_ uv_ uw_. \<lbrakk>?x = Abs uu_ uv_ $ uw_; ?y\<rbrakk> \<Longrightarrow> ?P; \<And>ux_ t. \<lbrakk>?x = Abs ux_ t; ?y = beta_reducible t\<rbrakk> \<Longrightarrow> ?P; \<And>v va u. \<lbrakk>?x = Ct v va $ u; ?y = (beta_reducible (Ct v va) \<or> beta_reducible u)\<rbrakk> \<Longrightarrow> ?P; \<And>v va u. \<lbrakk>?x = Fv v va $ u; ?y = (beta_reducible (Fv v va) \<or> beta_reducible u)\<rbrakk> \<Longrightarrow> ?P; \<And>v u. \<lbrakk>?x = Bv v $ u; ?y = (beta_reducible (Bv v) \<or> beta_reducible u)\<rbrakk> \<Longrightarrow> ?P; \<And>v va u. \<lbrakk>?x = v $ va $ u; ?y = (beta_reducible (v $ va) \<or> beta_reducible u)\<rbrakk> \<Longrightarrow> ?P; \<And>v va. \<lbrakk>?x = Ct v va; \<not> ?y\<rbrakk> \<Longrightarrow> ?P; \<And>v va. \<lbrakk>?x = Fv v va; \<not> ?y\<rbrakk> \<Longrightarrow> ?P; \<And>v. \<lbrakk>?x = Bv v; \<not> ?y\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>beta_reducible ?x; \<And>uu_ uv_ uw_. ?x = Abs uu_ uv_ $ uw_ \<Longrightarrow> ?P; \<And>ux_ t. \<lbrakk>?x = Abs ux_ t; beta_reducible t\<rbrakk> \<Longrightarrow> ?P; \<And>v va u. \<lbrakk>?x = Ct v va $ u; beta_reducible (Ct v va) \<or> beta_reducible u\<rbrakk> \<Longrightarrow> ?P; \<And>v va u. \<lbrakk>?x = Fv v va $ u; beta_reducible (Fv v va) \<or> beta_reducible u\<rbrakk> \<Longrightarrow> ?P; \<And>v u. \<lbrakk>?x = Bv v $ u; beta_reducible (Bv v) \<or> beta_reducible u\<rbrakk> \<Longrightarrow> ?P; \<And>v va u. \<lbrakk>?x = v $ va $ u; beta_reducible (v $ va) \<or> beta_reducible u\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>\<not> beta_reducible ?x; \<And>ux_ t. \<lbrakk>?x = Abs ux_ t; \<not> beta_reducible t\<rbrakk> \<Longrightarrow> ?P; \<And>v va u. \<lbrakk>?x = Ct v va $ u; \<not> (beta_reducible (Ct v va) \<or> beta_reducible u)\<rbrakk> \<Longrightarrow> ?P; \<And>v va u. \<lbrakk>?x = Fv v va $ u; \<not> (beta_reducible (Fv v va) \<or> beta_reducible u)\<rbrakk> \<Longrightarrow> ?P; \<And>v u. \<lbrakk>?x = Bv v $ u; \<not> (beta_reducible (Bv v) \<or> beta_reducible u)\<rbrakk> \<Longrightarrow> ?P; \<And>v va u. \<lbrakk>?x = v $ va $ u; \<not> (beta_reducible (v $ va) \<or> beta_reducible u)\<rbrakk> \<Longrightarrow> ?P; \<And>v va. ?x = Ct v va \<Longrightarrow> ?P; \<And>v va. ?x = Fv v va \<Longrightarrow> ?P; \<And>v. ?x = Bv v \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. \<not> beta_reducible u
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> beta_reducible u

goal (3 subgoals):
 1. \<And>s t u. \<lbrakk>s \<rightarrow>\<^sub>\<beta> t; \<not> beta_reducible t \<Longrightarrow> beta_norm s = Some t; \<not> beta_reducible (t $ u)\<rbrakk> \<Longrightarrow> beta_norm (s $ u) = Some (t $ u)
 2. \<And>s t u. \<lbrakk>s \<rightarrow>\<^sub>\<beta> t; \<not> beta_reducible t \<Longrightarrow> beta_norm s = Some t; \<not> beta_reducible (u $ t)\<rbrakk> \<Longrightarrow> beta_norm (u $ s) = Some (u $ t)
 3. \<And>s t T. \<lbrakk>s \<rightarrow>\<^sub>\<beta> t; \<not> beta_reducible t \<Longrightarrow> beta_norm s = Some t; \<not> beta_reducible (Abs T t)\<rbrakk> \<Longrightarrow> beta_norm (Abs T s) = Some (Abs T t)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. beta_norm (s $ u) = Some (t $ u)
[PROOF STEP]
apply (cases s; cases t)
[PROOF STATE]
proof (prove)
goal (25 subgoals):
 1. \<And>x11 x12 x11a x12a. \<lbrakk>s = Ct x11 x12; t = Ct x11a x12a\<rbrakk> \<Longrightarrow> beta_norm (s $ u) = Some (t $ u)
 2. \<And>x11 x12 x21 x22. \<lbrakk>s = Ct x11 x12; t = Fv x21 x22\<rbrakk> \<Longrightarrow> beta_norm (s $ u) = Some (t $ u)
 3. \<And>x11 x12 x3. \<lbrakk>s = Ct x11 x12; t = Bv x3\<rbrakk> \<Longrightarrow> beta_norm (s $ u) = Some (t $ u)
 4. \<And>x11 x12 x41 x42. \<lbrakk>s = Ct x11 x12; t = Abs x41 x42\<rbrakk> \<Longrightarrow> beta_norm (s $ u) = Some (t $ u)
 5. \<And>x11 x12 x51 x52. \<lbrakk>s = Ct x11 x12; t = x51 $ x52\<rbrakk> \<Longrightarrow> beta_norm (s $ u) = Some (t $ u)
 6. \<And>x21 x22 x11 x12. \<lbrakk>s = Fv x21 x22; t = Ct x11 x12\<rbrakk> \<Longrightarrow> beta_norm (s $ u) = Some (t $ u)
 7. \<And>x21 x22 x21a x22a. \<lbrakk>s = Fv x21 x22; t = Fv x21a x22a\<rbrakk> \<Longrightarrow> beta_norm (s $ u) = Some (t $ u)
 8. \<And>x21 x22 x3. \<lbrakk>s = Fv x21 x22; t = Bv x3\<rbrakk> \<Longrightarrow> beta_norm (s $ u) = Some (t $ u)
 9. \<And>x21 x22 x41 x42. \<lbrakk>s = Fv x21 x22; t = Abs x41 x42\<rbrakk> \<Longrightarrow> beta_norm (s $ u) = Some (t $ u)
 10. \<And>x21 x22 x51 x52. \<lbrakk>s = Fv x21 x22; t = x51 $ x52\<rbrakk> \<Longrightarrow> beta_norm (s $ u) = Some (t $ u)
A total of 25 subgoals...
[PROOF STEP]
using not_beta_reducible_imp_beta_norm_unchanged IH t u appL.prems
[PROOF STATE]
proof (prove)
using this:
\<not> beta_reducible ?t \<Longrightarrow> beta_norm ?t = Some ?t
beta_norm s = Some t
\<not> beta_reducible t
\<not> beta_reducible u
\<not> beta_reducible (t $ u)

goal (25 subgoals):
 1. \<And>x11 x12 x11a x12a. \<lbrakk>s = Ct x11 x12; t = Ct x11a x12a\<rbrakk> \<Longrightarrow> beta_norm (s $ u) = Some (t $ u)
 2. \<And>x11 x12 x21 x22. \<lbrakk>s = Ct x11 x12; t = Fv x21 x22\<rbrakk> \<Longrightarrow> beta_norm (s $ u) = Some (t $ u)
 3. \<And>x11 x12 x3. \<lbrakk>s = Ct x11 x12; t = Bv x3\<rbrakk> \<Longrightarrow> beta_norm (s $ u) = Some (t $ u)
 4. \<And>x11 x12 x41 x42. \<lbrakk>s = Ct x11 x12; t = Abs x41 x42\<rbrakk> \<Longrightarrow> beta_norm (s $ u) = Some (t $ u)
 5. \<And>x11 x12 x51 x52. \<lbrakk>s = Ct x11 x12; t = x51 $ x52\<rbrakk> \<Longrightarrow> beta_norm (s $ u) = Some (t $ u)
 6. \<And>x21 x22 x11 x12. \<lbrakk>s = Fv x21 x22; t = Ct x11 x12\<rbrakk> \<Longrightarrow> beta_norm (s $ u) = Some (t $ u)
 7. \<And>x21 x22 x21a x22a. \<lbrakk>s = Fv x21 x22; t = Fv x21a x22a\<rbrakk> \<Longrightarrow> beta_norm (s $ u) = Some (t $ u)
 8. \<And>x21 x22 x3. \<lbrakk>s = Fv x21 x22; t = Bv x3\<rbrakk> \<Longrightarrow> beta_norm (s $ u) = Some (t $ u)
 9. \<And>x21 x22 x41 x42. \<lbrakk>s = Fv x21 x22; t = Abs x41 x42\<rbrakk> \<Longrightarrow> beta_norm (s $ u) = Some (t $ u)
 10. \<And>x21 x22 x51 x52. \<lbrakk>s = Fv x21 x22; t = x51 $ x52\<rbrakk> \<Longrightarrow> beta_norm (s $ u) = Some (t $ u)
A total of 25 subgoals...
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
beta_norm (s $ u) = Some (t $ u)

goal (2 subgoals):
 1. \<And>s t u. \<lbrakk>s \<rightarrow>\<^sub>\<beta> t; \<not> beta_reducible t \<Longrightarrow> beta_norm s = Some t; \<not> beta_reducible (u $ t)\<rbrakk> \<Longrightarrow> beta_norm (u $ s) = Some (u $ t)
 2. \<And>s t T. \<lbrakk>s \<rightarrow>\<^sub>\<beta> t; \<not> beta_reducible t \<Longrightarrow> beta_norm s = Some t; \<not> beta_reducible (Abs T t)\<rbrakk> \<Longrightarrow> beta_norm (Abs T s) = Some (Abs T t)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>s t u. \<lbrakk>s \<rightarrow>\<^sub>\<beta> t; \<not> beta_reducible t \<Longrightarrow> beta_norm s = Some t; \<not> beta_reducible (u $ t)\<rbrakk> \<Longrightarrow> beta_norm (u $ s) = Some (u $ t)
 2. \<And>s t T. \<lbrakk>s \<rightarrow>\<^sub>\<beta> t; \<not> beta_reducible t \<Longrightarrow> beta_norm s = Some t; \<not> beta_reducible (Abs T t)\<rbrakk> \<Longrightarrow> beta_norm (Abs T s) = Some (Abs T t)
[PROOF STEP]
case (appR s t u)
[PROOF STATE]
proof (state)
this:
s \<rightarrow>\<^sub>\<beta> t
\<not> beta_reducible t \<Longrightarrow> beta_norm s = Some t
\<not> beta_reducible (u $ t)

goal (2 subgoals):
 1. \<And>s t u. \<lbrakk>s \<rightarrow>\<^sub>\<beta> t; \<not> beta_reducible t \<Longrightarrow> beta_norm s = Some t; \<not> beta_reducible (u $ t)\<rbrakk> \<Longrightarrow> beta_norm (u $ s) = Some (u $ t)
 2. \<And>s t T. \<lbrakk>s \<rightarrow>\<^sub>\<beta> t; \<not> beta_reducible t \<Longrightarrow> beta_norm s = Some t; \<not> beta_reducible (Abs T t)\<rbrakk> \<Longrightarrow> beta_norm (Abs T s) = Some (Abs T t)
[PROOF STEP]
hence t: "\<not> beta_reducible t"
[PROOF STATE]
proof (prove)
using this:
s \<rightarrow>\<^sub>\<beta> t
\<not> beta_reducible t \<Longrightarrow> beta_norm s = Some t
\<not> beta_reducible (u $ t)

goal (1 subgoal):
 1. \<not> beta_reducible t
[PROOF STEP]
using beta_reducible.elims
[PROOF STATE]
proof (prove)
using this:
s \<rightarrow>\<^sub>\<beta> t
\<not> beta_reducible t \<Longrightarrow> beta_norm s = Some t
\<not> beta_reducible (u $ t)
\<lbrakk>beta_reducible ?x = ?y; \<And>uu_ uv_ uw_. \<lbrakk>?x = Abs uu_ uv_ $ uw_; ?y\<rbrakk> \<Longrightarrow> ?P; \<And>ux_ t. \<lbrakk>?x = Abs ux_ t; ?y = beta_reducible t\<rbrakk> \<Longrightarrow> ?P; \<And>v va u. \<lbrakk>?x = Ct v va $ u; ?y = (beta_reducible (Ct v va) \<or> beta_reducible u)\<rbrakk> \<Longrightarrow> ?P; \<And>v va u. \<lbrakk>?x = Fv v va $ u; ?y = (beta_reducible (Fv v va) \<or> beta_reducible u)\<rbrakk> \<Longrightarrow> ?P; \<And>v u. \<lbrakk>?x = Bv v $ u; ?y = (beta_reducible (Bv v) \<or> beta_reducible u)\<rbrakk> \<Longrightarrow> ?P; \<And>v va u. \<lbrakk>?x = v $ va $ u; ?y = (beta_reducible (v $ va) \<or> beta_reducible u)\<rbrakk> \<Longrightarrow> ?P; \<And>v va. \<lbrakk>?x = Ct v va; \<not> ?y\<rbrakk> \<Longrightarrow> ?P; \<And>v va. \<lbrakk>?x = Fv v va; \<not> ?y\<rbrakk> \<Longrightarrow> ?P; \<And>v. \<lbrakk>?x = Bv v; \<not> ?y\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>beta_reducible ?x; \<And>uu_ uv_ uw_. ?x = Abs uu_ uv_ $ uw_ \<Longrightarrow> ?P; \<And>ux_ t. \<lbrakk>?x = Abs ux_ t; beta_reducible t\<rbrakk> \<Longrightarrow> ?P; \<And>v va u. \<lbrakk>?x = Ct v va $ u; beta_reducible (Ct v va) \<or> beta_reducible u\<rbrakk> \<Longrightarrow> ?P; \<And>v va u. \<lbrakk>?x = Fv v va $ u; beta_reducible (Fv v va) \<or> beta_reducible u\<rbrakk> \<Longrightarrow> ?P; \<And>v u. \<lbrakk>?x = Bv v $ u; beta_reducible (Bv v) \<or> beta_reducible u\<rbrakk> \<Longrightarrow> ?P; \<And>v va u. \<lbrakk>?x = v $ va $ u; beta_reducible (v $ va) \<or> beta_reducible u\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>\<not> beta_reducible ?x; \<And>ux_ t. \<lbrakk>?x = Abs ux_ t; \<not> beta_reducible t\<rbrakk> \<Longrightarrow> ?P; \<And>v va u. \<lbrakk>?x = Ct v va $ u; \<not> (beta_reducible (Ct v va) \<or> beta_reducible u)\<rbrakk> \<Longrightarrow> ?P; \<And>v va u. \<lbrakk>?x = Fv v va $ u; \<not> (beta_reducible (Fv v va) \<or> beta_reducible u)\<rbrakk> \<Longrightarrow> ?P; \<And>v u. \<lbrakk>?x = Bv v $ u; \<not> (beta_reducible (Bv v) \<or> beta_reducible u)\<rbrakk> \<Longrightarrow> ?P; \<And>v va u. \<lbrakk>?x = v $ va $ u; \<not> (beta_reducible (v $ va) \<or> beta_reducible u)\<rbrakk> \<Longrightarrow> ?P; \<And>v va. ?x = Ct v va \<Longrightarrow> ?P; \<And>v va. ?x = Fv v va \<Longrightarrow> ?P; \<And>v. ?x = Bv v \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. \<not> beta_reducible t
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> beta_reducible t

goal (2 subgoals):
 1. \<And>s t u. \<lbrakk>s \<rightarrow>\<^sub>\<beta> t; \<not> beta_reducible t \<Longrightarrow> beta_norm s = Some t; \<not> beta_reducible (u $ t)\<rbrakk> \<Longrightarrow> beta_norm (u $ s) = Some (u $ t)
 2. \<And>s t T. \<lbrakk>s \<rightarrow>\<^sub>\<beta> t; \<not> beta_reducible t \<Longrightarrow> beta_norm s = Some t; \<not> beta_reducible (Abs T t)\<rbrakk> \<Longrightarrow> beta_norm (Abs T s) = Some (Abs T t)
[PROOF STEP]
hence IH: "beta_norm s = Some t"
[PROOF STATE]
proof (prove)
using this:
\<not> beta_reducible t

goal (1 subgoal):
 1. beta_norm s = Some t
[PROOF STEP]
using appR.IH
[PROOF STATE]
proof (prove)
using this:
\<not> beta_reducible t
\<not> beta_reducible t \<Longrightarrow> beta_norm s = Some t

goal (1 subgoal):
 1. beta_norm s = Some t
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
beta_norm s = Some t

goal (2 subgoals):
 1. \<And>s t u. \<lbrakk>s \<rightarrow>\<^sub>\<beta> t; \<not> beta_reducible t \<Longrightarrow> beta_norm s = Some t; \<not> beta_reducible (u $ t)\<rbrakk> \<Longrightarrow> beta_norm (u $ s) = Some (u $ t)
 2. \<And>s t T. \<lbrakk>s \<rightarrow>\<^sub>\<beta> t; \<not> beta_reducible t \<Longrightarrow> beta_norm s = Some t; \<not> beta_reducible (Abs T t)\<rbrakk> \<Longrightarrow> beta_norm (Abs T s) = Some (Abs T t)
[PROOF STEP]
from appR
[PROOF STATE]
proof (chain)
picking this:
s \<rightarrow>\<^sub>\<beta> t
\<not> beta_reducible t \<Longrightarrow> beta_norm s = Some t
\<not> beta_reducible (u $ t)
[PROOF STEP]
have u: "\<not> beta_reducible u"
[PROOF STATE]
proof (prove)
using this:
s \<rightarrow>\<^sub>\<beta> t
\<not> beta_reducible t \<Longrightarrow> beta_norm s = Some t
\<not> beta_reducible (u $ t)

goal (1 subgoal):
 1. \<not> beta_reducible u
[PROOF STEP]
using beta_reducible.elims
[PROOF STATE]
proof (prove)
using this:
s \<rightarrow>\<^sub>\<beta> t
\<not> beta_reducible t \<Longrightarrow> beta_norm s = Some t
\<not> beta_reducible (u $ t)
\<lbrakk>beta_reducible ?x = ?y; \<And>uu_ uv_ uw_. \<lbrakk>?x = Abs uu_ uv_ $ uw_; ?y\<rbrakk> \<Longrightarrow> ?P; \<And>ux_ t. \<lbrakk>?x = Abs ux_ t; ?y = beta_reducible t\<rbrakk> \<Longrightarrow> ?P; \<And>v va u. \<lbrakk>?x = Ct v va $ u; ?y = (beta_reducible (Ct v va) \<or> beta_reducible u)\<rbrakk> \<Longrightarrow> ?P; \<And>v va u. \<lbrakk>?x = Fv v va $ u; ?y = (beta_reducible (Fv v va) \<or> beta_reducible u)\<rbrakk> \<Longrightarrow> ?P; \<And>v u. \<lbrakk>?x = Bv v $ u; ?y = (beta_reducible (Bv v) \<or> beta_reducible u)\<rbrakk> \<Longrightarrow> ?P; \<And>v va u. \<lbrakk>?x = v $ va $ u; ?y = (beta_reducible (v $ va) \<or> beta_reducible u)\<rbrakk> \<Longrightarrow> ?P; \<And>v va. \<lbrakk>?x = Ct v va; \<not> ?y\<rbrakk> \<Longrightarrow> ?P; \<And>v va. \<lbrakk>?x = Fv v va; \<not> ?y\<rbrakk> \<Longrightarrow> ?P; \<And>v. \<lbrakk>?x = Bv v; \<not> ?y\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>beta_reducible ?x; \<And>uu_ uv_ uw_. ?x = Abs uu_ uv_ $ uw_ \<Longrightarrow> ?P; \<And>ux_ t. \<lbrakk>?x = Abs ux_ t; beta_reducible t\<rbrakk> \<Longrightarrow> ?P; \<And>v va u. \<lbrakk>?x = Ct v va $ u; beta_reducible (Ct v va) \<or> beta_reducible u\<rbrakk> \<Longrightarrow> ?P; \<And>v va u. \<lbrakk>?x = Fv v va $ u; beta_reducible (Fv v va) \<or> beta_reducible u\<rbrakk> \<Longrightarrow> ?P; \<And>v u. \<lbrakk>?x = Bv v $ u; beta_reducible (Bv v) \<or> beta_reducible u\<rbrakk> \<Longrightarrow> ?P; \<And>v va u. \<lbrakk>?x = v $ va $ u; beta_reducible (v $ va) \<or> beta_reducible u\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>\<not> beta_reducible ?x; \<And>ux_ t. \<lbrakk>?x = Abs ux_ t; \<not> beta_reducible t\<rbrakk> \<Longrightarrow> ?P; \<And>v va u. \<lbrakk>?x = Ct v va $ u; \<not> (beta_reducible (Ct v va) \<or> beta_reducible u)\<rbrakk> \<Longrightarrow> ?P; \<And>v va u. \<lbrakk>?x = Fv v va $ u; \<not> (beta_reducible (Fv v va) \<or> beta_reducible u)\<rbrakk> \<Longrightarrow> ?P; \<And>v u. \<lbrakk>?x = Bv v $ u; \<not> (beta_reducible (Bv v) \<or> beta_reducible u)\<rbrakk> \<Longrightarrow> ?P; \<And>v va u. \<lbrakk>?x = v $ va $ u; \<not> (beta_reducible (v $ va) \<or> beta_reducible u)\<rbrakk> \<Longrightarrow> ?P; \<And>v va. ?x = Ct v va \<Longrightarrow> ?P; \<And>v va. ?x = Fv v va \<Longrightarrow> ?P; \<And>v. ?x = Bv v \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. \<not> beta_reducible u
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> beta_reducible u

goal (2 subgoals):
 1. \<And>s t u. \<lbrakk>s \<rightarrow>\<^sub>\<beta> t; \<not> beta_reducible t \<Longrightarrow> beta_norm s = Some t; \<not> beta_reducible (u $ t)\<rbrakk> \<Longrightarrow> beta_norm (u $ s) = Some (u $ t)
 2. \<And>s t T. \<lbrakk>s \<rightarrow>\<^sub>\<beta> t; \<not> beta_reducible t \<Longrightarrow> beta_norm s = Some t; \<not> beta_reducible (Abs T t)\<rbrakk> \<Longrightarrow> beta_norm (Abs T s) = Some (Abs T t)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. beta_norm (u $ s) = Some (u $ t)
[PROOF STEP]
apply (cases s; cases u)
[PROOF STATE]
proof (prove)
goal (25 subgoals):
 1. \<And>x11 x12 x11a x12a. \<lbrakk>s = Ct x11 x12; u = Ct x11a x12a\<rbrakk> \<Longrightarrow> beta_norm (u $ s) = Some (u $ t)
 2. \<And>x11 x12 x21 x22. \<lbrakk>s = Ct x11 x12; u = Fv x21 x22\<rbrakk> \<Longrightarrow> beta_norm (u $ s) = Some (u $ t)
 3. \<And>x11 x12 x3. \<lbrakk>s = Ct x11 x12; u = Bv x3\<rbrakk> \<Longrightarrow> beta_norm (u $ s) = Some (u $ t)
 4. \<And>x11 x12 x41 x42. \<lbrakk>s = Ct x11 x12; u = Abs x41 x42\<rbrakk> \<Longrightarrow> beta_norm (u $ s) = Some (u $ t)
 5. \<And>x11 x12 x51 x52. \<lbrakk>s = Ct x11 x12; u = x51 $ x52\<rbrakk> \<Longrightarrow> beta_norm (u $ s) = Some (u $ t)
 6. \<And>x21 x22 x11 x12. \<lbrakk>s = Fv x21 x22; u = Ct x11 x12\<rbrakk> \<Longrightarrow> beta_norm (u $ s) = Some (u $ t)
 7. \<And>x21 x22 x21a x22a. \<lbrakk>s = Fv x21 x22; u = Fv x21a x22a\<rbrakk> \<Longrightarrow> beta_norm (u $ s) = Some (u $ t)
 8. \<And>x21 x22 x3. \<lbrakk>s = Fv x21 x22; u = Bv x3\<rbrakk> \<Longrightarrow> beta_norm (u $ s) = Some (u $ t)
 9. \<And>x21 x22 x41 x42. \<lbrakk>s = Fv x21 x22; u = Abs x41 x42\<rbrakk> \<Longrightarrow> beta_norm (u $ s) = Some (u $ t)
 10. \<And>x21 x22 x51 x52. \<lbrakk>s = Fv x21 x22; u = x51 $ x52\<rbrakk> \<Longrightarrow> beta_norm (u $ s) = Some (u $ t)
A total of 25 subgoals...
[PROOF STEP]
using not_beta_reducible_imp_beta_norm_unchanged IH t u appR.prems
[PROOF STATE]
proof (prove)
using this:
\<not> beta_reducible ?t \<Longrightarrow> beta_norm ?t = Some ?t
beta_norm s = Some t
\<not> beta_reducible t
\<not> beta_reducible u
\<not> beta_reducible (u $ t)

goal (25 subgoals):
 1. \<And>x11 x12 x11a x12a. \<lbrakk>s = Ct x11 x12; u = Ct x11a x12a\<rbrakk> \<Longrightarrow> beta_norm (u $ s) = Some (u $ t)
 2. \<And>x11 x12 x21 x22. \<lbrakk>s = Ct x11 x12; u = Fv x21 x22\<rbrakk> \<Longrightarrow> beta_norm (u $ s) = Some (u $ t)
 3. \<And>x11 x12 x3. \<lbrakk>s = Ct x11 x12; u = Bv x3\<rbrakk> \<Longrightarrow> beta_norm (u $ s) = Some (u $ t)
 4. \<And>x11 x12 x41 x42. \<lbrakk>s = Ct x11 x12; u = Abs x41 x42\<rbrakk> \<Longrightarrow> beta_norm (u $ s) = Some (u $ t)
 5. \<And>x11 x12 x51 x52. \<lbrakk>s = Ct x11 x12; u = x51 $ x52\<rbrakk> \<Longrightarrow> beta_norm (u $ s) = Some (u $ t)
 6. \<And>x21 x22 x11 x12. \<lbrakk>s = Fv x21 x22; u = Ct x11 x12\<rbrakk> \<Longrightarrow> beta_norm (u $ s) = Some (u $ t)
 7. \<And>x21 x22 x21a x22a. \<lbrakk>s = Fv x21 x22; u = Fv x21a x22a\<rbrakk> \<Longrightarrow> beta_norm (u $ s) = Some (u $ t)
 8. \<And>x21 x22 x3. \<lbrakk>s = Fv x21 x22; u = Bv x3\<rbrakk> \<Longrightarrow> beta_norm (u $ s) = Some (u $ t)
 9. \<And>x21 x22 x41 x42. \<lbrakk>s = Fv x21 x22; u = Abs x41 x42\<rbrakk> \<Longrightarrow> beta_norm (u $ s) = Some (u $ t)
 10. \<And>x21 x22 x51 x52. \<lbrakk>s = Fv x21 x22; u = x51 $ x52\<rbrakk> \<Longrightarrow> beta_norm (u $ s) = Some (u $ t)
A total of 25 subgoals...
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
beta_norm (u $ s) = Some (u $ t)

goal (1 subgoal):
 1. \<And>s t T. \<lbrakk>s \<rightarrow>\<^sub>\<beta> t; \<not> beta_reducible t \<Longrightarrow> beta_norm s = Some t; \<not> beta_reducible (Abs T t)\<rbrakk> \<Longrightarrow> beta_norm (Abs T s) = Some (Abs T t)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s t T. \<lbrakk>s \<rightarrow>\<^sub>\<beta> t; \<not> beta_reducible t \<Longrightarrow> beta_norm s = Some t; \<not> beta_reducible (Abs T t)\<rbrakk> \<Longrightarrow> beta_norm (Abs T s) = Some (Abs T t)
[PROOF STEP]
case (abs s t T)
[PROOF STATE]
proof (state)
this:
s \<rightarrow>\<^sub>\<beta> t
\<not> beta_reducible t \<Longrightarrow> beta_norm s = Some t
\<not> beta_reducible (Abs T t)

goal (1 subgoal):
 1. \<And>s t T. \<lbrakk>s \<rightarrow>\<^sub>\<beta> t; \<not> beta_reducible t \<Longrightarrow> beta_norm s = Some t; \<not> beta_reducible (Abs T t)\<rbrakk> \<Longrightarrow> beta_norm (Abs T s) = Some (Abs T t)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s \<rightarrow>\<^sub>\<beta> t
\<not> beta_reducible t \<Longrightarrow> beta_norm s = Some t
\<not> beta_reducible (Abs T t)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
s \<rightarrow>\<^sub>\<beta> t
\<not> beta_reducible t \<Longrightarrow> beta_norm s = Some t
\<not> beta_reducible (Abs T t)

goal (1 subgoal):
 1. beta_norm (Abs T s) = Some (Abs T t)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
beta_norm (Abs T s) = Some (Abs T t)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fo_nmlz_add_nth_rem_nth:
  assumes "fo_nmlz AD xs = xs" "i < length xs"
  shows "\<exists>z. fo_nmlz AD (add_nth i z (fo_nmlz AD (rem_nth i xs))) = xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>z. fo_nmlz AD (add_nth i z (fo_nmlz AD (rem_nth i xs))) = xs
[PROOF STEP]
using rem_nth_length[OF assms(2)] fo_nmlz_add_rem[of i "rem_nth i xs" AD "xs ! i",
      unfolded assms(1) add_nth_rem_nth_self[OF assms(2)]] assms(2)
[PROOF STATE]
proof (prove)
using this:
length (rem_nth i xs) = length xs - 1
i \<le> length (rem_nth i xs) \<Longrightarrow> \<exists>z'. xs = fo_nmlz AD (add_nth i z' (fo_nmlz AD (rem_nth i xs)))
i < length xs

goal (1 subgoal):
 1. \<exists>z. fo_nmlz AD (add_nth i z (fo_nmlz AD (rem_nth i xs))) = xs
[PROOF STEP]
by (subst eq_commute) auto


[STATEMENT]
lemma is_sig_red_regularD_lt:
  assumes "is_sig_red (\<prec>\<^sub>t) top_tail {f} p"
  shows "lt f \<prec>\<^sub>t lt p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lt f \<prec>\<^sub>t lt p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lt f \<prec>\<^sub>t lt p
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
is_sig_red (\<prec>\<^sub>t) top_tail {f} p
[PROOF STEP]
obtain s where "rep_list f \<noteq> 0" and "s \<in> keys (rep_list p)"
    and 1: "punit.lt (rep_list f) adds s" and 2: "s \<oplus> lt f \<prec>\<^sub>t punit.lt (rep_list f) \<oplus> lt p"
[PROOF STATE]
proof (prove)
using this:
is_sig_red (\<prec>\<^sub>t) top_tail {f} p

goal (1 subgoal):
 1. (\<And>s. \<lbrakk>rep_list f \<noteq> 0; s \<in> keys (rep_list p); punit.lt (rep_list f) adds s; s \<oplus> lt f \<prec>\<^sub>t punit.lt (rep_list f) \<oplus> lt p\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto elim!: is_sig_red_addsE)
[PROOF STATE]
proof (state)
this:
rep_list f \<noteq> 0
s \<in> keys (rep_list p)
punit.lt (rep_list f) adds s
s \<oplus> lt f \<prec>\<^sub>t punit.lt (rep_list f) \<oplus> lt p

goal (1 subgoal):
 1. lt f \<prec>\<^sub>t lt p
[PROOF STEP]
from 1
[PROOF STATE]
proof (chain)
picking this:
punit.lt (rep_list f) adds s
[PROOF STEP]
obtain t where eq: "s = punit.lt (rep_list f) + t"
[PROOF STATE]
proof (prove)
using this:
punit.lt (rep_list f) adds s

goal (1 subgoal):
 1. (\<And>t. s = punit.lt (rep_list f) + t \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule addsE)
[PROOF STATE]
proof (state)
this:
s = punit.lt (rep_list f) + t

goal (1 subgoal):
 1. lt f \<prec>\<^sub>t lt p
[PROOF STEP]
hence "punit.lt (rep_list f) \<oplus> (t \<oplus> lt f) = s \<oplus> lt f"
[PROOF STATE]
proof (prove)
using this:
s = punit.lt (rep_list f) + t

goal (1 subgoal):
 1. punit.lt (rep_list f) \<oplus> (t \<oplus> lt f) = s \<oplus> lt f
[PROOF STEP]
by (simp add: splus_assoc)
[PROOF STATE]
proof (state)
this:
punit.lt (rep_list f) \<oplus> (t \<oplus> lt f) = s \<oplus> lt f

goal (1 subgoal):
 1. lt f \<prec>\<^sub>t lt p
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
punit.lt (rep_list f) \<oplus> (t \<oplus> lt f) = s \<oplus> lt f

goal (1 subgoal):
 1. lt f \<prec>\<^sub>t lt p
[PROOF STEP]
note 2
[PROOF STATE]
proof (state)
this:
s \<oplus> lt f \<prec>\<^sub>t punit.lt (rep_list f) \<oplus> lt p

goal (1 subgoal):
 1. lt f \<prec>\<^sub>t lt p
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
punit.lt (rep_list f) \<oplus> (t \<oplus> lt f) \<prec>\<^sub>t punit.lt (rep_list f) \<oplus> lt p
[PROOF STEP]
have "t \<oplus> lt f \<prec>\<^sub>t lt p"
[PROOF STATE]
proof (prove)
using this:
punit.lt (rep_list f) \<oplus> (t \<oplus> lt f) \<prec>\<^sub>t punit.lt (rep_list f) \<oplus> lt p

goal (1 subgoal):
 1. t \<oplus> lt f \<prec>\<^sub>t lt p
[PROOF STEP]
by (rule ord_term_strict_canc)
[PROOF STATE]
proof (state)
this:
t \<oplus> lt f \<prec>\<^sub>t lt p

goal (1 subgoal):
 1. lt f \<prec>\<^sub>t lt p
[PROOF STEP]
have "0 \<preceq> t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<preceq> t
[PROOF STEP]
by (fact zero_min)
[PROOF STATE]
proof (state)
this:
(0::'a) \<preceq> t

goal (1 subgoal):
 1. lt f \<prec>\<^sub>t lt p
[PROOF STEP]
hence "0 \<oplus> lt f \<preceq>\<^sub>t t \<oplus> lt f"
[PROOF STATE]
proof (prove)
using this:
(0::'a) \<preceq> t

goal (1 subgoal):
 1. (0::'a) \<oplus> lt f \<preceq>\<^sub>t t \<oplus> lt f
[PROOF STEP]
by (rule splus_mono_left)
[PROOF STATE]
proof (state)
this:
(0::'a) \<oplus> lt f \<preceq>\<^sub>t t \<oplus> lt f

goal (1 subgoal):
 1. lt f \<prec>\<^sub>t lt p
[PROOF STEP]
hence "lt f \<preceq>\<^sub>t t \<oplus> lt f"
[PROOF STATE]
proof (prove)
using this:
(0::'a) \<oplus> lt f \<preceq>\<^sub>t t \<oplus> lt f

goal (1 subgoal):
 1. lt f \<preceq>\<^sub>t t \<oplus> lt f
[PROOF STEP]
by (simp add: term_simps)
[PROOF STATE]
proof (state)
this:
lt f \<preceq>\<^sub>t t \<oplus> lt f

goal (1 subgoal):
 1. lt f \<prec>\<^sub>t lt p
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
lt f \<preceq>\<^sub>t t \<oplus> lt f

goal (1 subgoal):
 1. lt f \<prec>\<^sub>t lt p
[PROOF STEP]
using \<open>t \<oplus> lt f \<prec>\<^sub>t lt p\<close>
[PROOF STATE]
proof (prove)
using this:
lt f \<preceq>\<^sub>t t \<oplus> lt f
t \<oplus> lt f \<prec>\<^sub>t lt p

goal (1 subgoal):
 1. lt f \<prec>\<^sub>t lt p
[PROOF STEP]
by (rule ord_term_lin.le_less_trans)
[PROOF STATE]
proof (state)
this:
lt f \<prec>\<^sub>t lt p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lt_spair':
  assumes "rep_list p \<noteq> 0" and "a + punit.lt (rep_list p) = b + punit.lt (rep_list q)" and "b \<oplus> lt q \<prec>\<^sub>t a \<oplus> lt p"
  shows "lt (spair p q) = (a - gcs a b) \<oplus> lt p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lt (spair p q) = (a - gcs a b) \<oplus> lt p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lt (spair p q) = (a - gcs a b) \<oplus> lt p
[PROOF STEP]
from assms(3)
[PROOF STATE]
proof (chain)
picking this:
b \<oplus> lt q \<prec>\<^sub>t a \<oplus> lt p
[PROOF STEP]
have "punit.lt (rep_list p) \<oplus> (b \<oplus> lt q) \<prec>\<^sub>t punit.lt (rep_list p) \<oplus> (a \<oplus> lt p)"
[PROOF STATE]
proof (prove)
using this:
b \<oplus> lt q \<prec>\<^sub>t a \<oplus> lt p

goal (1 subgoal):
 1. punit.lt (rep_list p) \<oplus> (b \<oplus> lt q) \<prec>\<^sub>t punit.lt (rep_list p) \<oplus> (a \<oplus> lt p)
[PROOF STEP]
by (fact splus_mono_strict)
[PROOF STATE]
proof (state)
this:
punit.lt (rep_list p) \<oplus> (b \<oplus> lt q) \<prec>\<^sub>t punit.lt (rep_list p) \<oplus> (a \<oplus> lt p)

goal (1 subgoal):
 1. lt (spair p q) = (a - gcs a b) \<oplus> lt p
[PROOF STEP]
hence "(b + punit.lt (rep_list p)) \<oplus> lt q \<prec>\<^sub>t (b + punit.lt (rep_list q)) \<oplus> lt p"
[PROOF STATE]
proof (prove)
using this:
punit.lt (rep_list p) \<oplus> (b \<oplus> lt q) \<prec>\<^sub>t punit.lt (rep_list p) \<oplus> (a \<oplus> lt p)

goal (1 subgoal):
 1. (b + punit.lt (rep_list p)) \<oplus> lt q \<prec>\<^sub>t (b + punit.lt (rep_list q)) \<oplus> lt p
[PROOF STEP]
by (simp only: splus_assoc[symmetric] add.commute assms(2))
[PROOF STATE]
proof (state)
this:
(b + punit.lt (rep_list p)) \<oplus> lt q \<prec>\<^sub>t (b + punit.lt (rep_list q)) \<oplus> lt p

goal (1 subgoal):
 1. lt (spair p q) = (a - gcs a b) \<oplus> lt p
[PROOF STEP]
hence "punit.lt (rep_list p) \<oplus> lt q \<prec>\<^sub>t punit.lt (rep_list q) \<oplus> lt p"
[PROOF STATE]
proof (prove)
using this:
(b + punit.lt (rep_list p)) \<oplus> lt q \<prec>\<^sub>t (b + punit.lt (rep_list q)) \<oplus> lt p

goal (1 subgoal):
 1. punit.lt (rep_list p) \<oplus> lt q \<prec>\<^sub>t punit.lt (rep_list q) \<oplus> lt p
[PROOF STEP]
by (simp only: splus_assoc ord_term_strict_canc)
[PROOF STATE]
proof (state)
this:
punit.lt (rep_list p) \<oplus> lt q \<prec>\<^sub>t punit.lt (rep_list q) \<oplus> lt p

goal (1 subgoal):
 1. lt (spair p q) = (a - gcs a b) \<oplus> lt p
[PROOF STEP]
with assms(1)
[PROOF STATE]
proof (chain)
picking this:
rep_list p \<noteq> 0
punit.lt (rep_list p) \<oplus> lt q \<prec>\<^sub>t punit.lt (rep_list q) \<oplus> lt p
[PROOF STEP]
have "lt (spair p q) = (lcs (punit.lt (rep_list p)) (punit.lt (rep_list q)) - punit.lt (rep_list p)) \<oplus> lt p"
[PROOF STATE]
proof (prove)
using this:
rep_list p \<noteq> 0
punit.lt (rep_list p) \<oplus> lt q \<prec>\<^sub>t punit.lt (rep_list q) \<oplus> lt p

goal (1 subgoal):
 1. lt (spair p q) = (lcs (punit.lt (rep_list p)) (punit.lt (rep_list q)) - punit.lt (rep_list p)) \<oplus> lt p
[PROOF STEP]
by (rule lt_spair)
[PROOF STATE]
proof (state)
this:
lt (spair p q) = (lcs (punit.lt (rep_list p)) (punit.lt (rep_list q)) - punit.lt (rep_list p)) \<oplus> lt p

goal (1 subgoal):
 1. lt (spair p q) = (a - gcs a b) \<oplus> lt p
[PROOF STEP]
with assms(2)
[PROOF STATE]
proof (chain)
picking this:
a + punit.lt (rep_list p) = b + punit.lt (rep_list q)
lt (spair p q) = (lcs (punit.lt (rep_list p)) (punit.lt (rep_list q)) - punit.lt (rep_list p)) \<oplus> lt p
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a + punit.lt (rep_list p) = b + punit.lt (rep_list q)
lt (spair p q) = (lcs (punit.lt (rep_list p)) (punit.lt (rep_list q)) - punit.lt (rep_list p)) \<oplus> lt p

goal (1 subgoal):
 1. lt (spair p q) = (a - gcs a b) \<oplus> lt p
[PROOF STEP]
by (simp add: lcs_minus_1)
[PROOF STATE]
proof (state)
this:
lt (spair p q) = (a - gcs a b) \<oplus> lt p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma term_pp_rel_cancel:
  assumes "reflp r"
  shows "term_pp_rel r a (cancel_term_pp_pair a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. term_pp_rel r a (cancel_term_pp_pair a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. term_pp_rel r a (cancel_term_pp_pair a)
[PROOF STEP]
obtain u s where a: "a = (u, s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>u s. a = (u, s) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule prod.exhaust)
[PROOF STATE]
proof (state)
this:
a = (u, s)

goal (1 subgoal):
 1. term_pp_rel r a (cancel_term_pp_pair a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. term_pp_rel r a (cancel_term_pp_pair a)
[PROOF STEP]
proof (simp add: a cancel_term_pp_pair_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. term_pp_rel r (u, s) (u \<ominus> gcs (pp_of_term u) s, s - gcs (pp_of_term u) s)
[PROOF STEP]
let ?g = "gcs (pp_of_term u) s"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. term_pp_rel r (u, s) (u \<ominus> gcs (pp_of_term u) s, s - gcs (pp_of_term u) s)
[PROOF STEP]
have "?g adds s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gcs (pp_of_term u) s adds s
[PROOF STEP]
by (fact gcs_adds_2)
[PROOF STATE]
proof (state)
this:
gcs (pp_of_term u) s adds s

goal (1 subgoal):
 1. term_pp_rel r (u, s) (u \<ominus> gcs (pp_of_term u) s, s - gcs (pp_of_term u) s)
[PROOF STEP]
hence "(s - ?g) \<oplus> (u \<ominus> 0) = s \<oplus> u \<ominus> (?g + 0)"
[PROOF STATE]
proof (prove)
using this:
gcs (pp_of_term u) s adds s

goal (1 subgoal):
 1. (s - gcs (pp_of_term u) s) \<oplus> (u \<ominus> (0::'a)) = s \<oplus> u \<ominus> (gcs (pp_of_term u) s + (0::'a))
[PROOF STEP]
using zero_adds_pp
[PROOF STATE]
proof (prove)
using this:
gcs (pp_of_term u) s adds s
(0::'a) adds\<^sub>p ?v

goal (1 subgoal):
 1. (s - gcs (pp_of_term u) s) \<oplus> (u \<ominus> (0::'a)) = s \<oplus> u \<ominus> (gcs (pp_of_term u) s + (0::'a))
[PROOF STEP]
by (rule minus_splus_sminus)
[PROOF STATE]
proof (state)
this:
(s - gcs (pp_of_term u) s) \<oplus> (u \<ominus> (0::'a)) = s \<oplus> u \<ominus> (gcs (pp_of_term u) s + (0::'a))

goal (1 subgoal):
 1. term_pp_rel r (u, s) (u \<ominus> gcs (pp_of_term u) s, s - gcs (pp_of_term u) s)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(s - gcs (pp_of_term u) s) \<oplus> (u \<ominus> (0::'a)) = s \<oplus> u \<ominus> (gcs (pp_of_term u) s + (0::'a))

goal (1 subgoal):
 1. term_pp_rel r (u, s) (u \<ominus> gcs (pp_of_term u) s, s - gcs (pp_of_term u) s)
[PROOF STEP]
have "... = s \<oplus> (u \<ominus> ?g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<oplus> u \<ominus> (gcs (pp_of_term u) s + (0::'a)) = s \<oplus> (u \<ominus> gcs (pp_of_term u) s)
[PROOF STEP]
by (metis add.left_neutral add.right_neutral adds_pp_def diff_zero gcs_adds_2 gcs_comm
          minus_splus_sminus zero_adds)
[PROOF STATE]
proof (state)
this:
s \<oplus> u \<ominus> (gcs (pp_of_term u) s + (0::'a)) = s \<oplus> (u \<ominus> gcs (pp_of_term u) s)

goal (1 subgoal):
 1. term_pp_rel r (u, s) (u \<ominus> gcs (pp_of_term u) s, s - gcs (pp_of_term u) s)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(s - gcs (pp_of_term u) s) \<oplus> (u \<ominus> (0::'a)) = s \<oplus> (u \<ominus> gcs (pp_of_term u) s)
[PROOF STEP]
have "r ((s - ?g) \<oplus> u) (s \<oplus> (u \<ominus> ?g))"
[PROOF STATE]
proof (prove)
using this:
(s - gcs (pp_of_term u) s) \<oplus> (u \<ominus> (0::'a)) = s \<oplus> (u \<ominus> gcs (pp_of_term u) s)

goal (1 subgoal):
 1. r ((s - gcs (pp_of_term u) s) \<oplus> u) (s \<oplus> (u \<ominus> gcs (pp_of_term u) s))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(s - gcs (pp_of_term u) s) \<oplus> (u \<ominus> (0::'a)) = s \<oplus> (u \<ominus> gcs (pp_of_term u) s)
reflp r

goal (1 subgoal):
 1. r ((s - gcs (pp_of_term u) s) \<oplus> u) (s \<oplus> (u \<ominus> gcs (pp_of_term u) s))
[PROOF STEP]
by (simp add: term_simps reflp_def)
[PROOF STATE]
proof (state)
this:
r ((s - gcs (pp_of_term u) s) \<oplus> u) (s \<oplus> (u \<ominus> gcs (pp_of_term u) s))

goal (1 subgoal):
 1. term_pp_rel r (u, s) (u \<ominus> gcs (pp_of_term u) s, s - gcs (pp_of_term u) s)
[PROOF STEP]
thus "term_pp_rel r (u, s) (u \<ominus> ?g, s - ?g)"
[PROOF STATE]
proof (prove)
using this:
r ((s - gcs (pp_of_term u) s) \<oplus> u) (s \<oplus> (u \<ominus> gcs (pp_of_term u) s))

goal (1 subgoal):
 1. term_pp_rel r (u, s) (u \<ominus> gcs (pp_of_term u) s, s - gcs (pp_of_term u) s)
[PROOF STEP]
by (simp add: a term_pp_rel_def)
[PROOF STATE]
proof (state)
this:
term_pp_rel r (u, s) (u \<ominus> gcs (pp_of_term u) s, s - gcs (pp_of_term u) s)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
term_pp_rel r a (cancel_term_pp_pair a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma spair_alt_spair_sigs:
  "spair p q = monom_mult (1 / punit.lc (rep_list p)) (pp_of_term (fst (spair_sigs p q)) - lp p) p -
                monom_mult (1 / punit.lc (rep_list q)) (pp_of_term (snd (spair_sigs p q)) - lp q) q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spair p q = monom_mult ((1::'b) / punit.lc (rep_list p)) (pp_of_term (fst (spair_sigs p q)) - lp p) p - monom_mult ((1::'b) / punit.lc (rep_list q)) (pp_of_term (snd (spair_sigs p q)) - lp q) q
[PROOF STEP]
by (simp add: spair_def spair_sigs_def Let_def term_simps)


[STATEMENT]
lemma sig_crit'_sym: "sig_crit' bs (Inl (p, q)) \<Longrightarrow> sig_crit' bs (Inl (q, p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sig_crit' bs (Inl (p, q)) \<Longrightarrow> sig_crit' bs (Inl (q, p))
[PROOF STEP]
by (auto simp: spair_sigs_def Let_def lcs_comm)


[STATEMENT]
lemma trivial_phi: "trivial g v \<Longrightarrow> phi g v \<noteq> None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trivial g v \<Longrightarrow> phi g v \<noteq> None
[PROOF STEP]
by (auto simp: trivial_def isTrivialPhi_def split: option.splits)


[STATEMENT]
lemma vfinite_vdoubleton[simp]: "vfinite (set {x, y})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfinite (set {x, y})
[PROOF STEP]
by simp


[STATEMENT]
lemma Dag_unique_ex_conj_simp [simp]:
  "Dag p l r t \<Longrightarrow> (\<exists>t. Dag p l r t \<and> P t) = P t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Dag p l r t \<Longrightarrow> (\<exists>t. Dag p l r t \<and> P t) = P t
[PROOF STEP]
by (auto dest: Dag_unique)


[STATEMENT]
lemma (in CRR_market_viable) real_cond_exp_discount_stock_q_const:
  assumes "N = bernoulli_stream q"
and "q = (1+r-d) / (u-d)"
shows "AE w in N. real_cond_exp N (G n)
   (discounted_value r (prices Mkt stk) (Suc n)) w =
                  discounted_value r (prices Mkt stk) n w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AEeq N (real_cond_exp N (G n) (discounted_value r (prices Mkt stk) (Suc n))) (discounted_value r (prices Mkt stk) n)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. AEeq N (real_cond_exp N (G n) (discounted_value r (prices Mkt stk) (Suc n))) (discounted_value r (prices Mkt stk) n)
[PROOF STEP]
have qlt: "0 < q" and qgt: "q < 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < q &&& q < 1
[PROOF STEP]
using assms gt_param lt_param CRR_viable
[PROOF STATE]
proof (prove)
using this:
N = bernoulli_stream q
q = (1 + r - d) / (u - d)
\<lbrakk>?q = (1 + r - d) / (u - d); viable_market Mkt\<rbrakk> \<Longrightarrow> 0 < ?q
\<lbrakk>?q = (1 + r - d) / (u - d); viable_market Mkt\<rbrakk> \<Longrightarrow> ?q < 1
viable_market Mkt

goal (1 subgoal):
 1. 0 < q &&& q < 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < q
q < 1

goal (1 subgoal):
 1. AEeq N (real_cond_exp N (G n) (discounted_value r (prices Mkt stk) (Suc n))) (discounted_value r (prices Mkt stk) n)
[PROOF STEP]
have "AE w in N. real_cond_exp N (G n) (discounted_value r (prices Mkt stk) (Suc n)) w =
                  discounted_value r (\<lambda>m w. (q * u + (1 - q) * d) * prices Mkt stk n w) (Suc n) w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AEeq N (real_cond_exp N (G n) (discounted_value r (prices Mkt stk) (Suc n))) (discounted_value r (\<lambda>m w. (q * u + (1 - q) * d) * prices Mkt stk n w) (Suc n))
[PROOF STEP]
using assms real_cond_exp_discount_stock[of N q] qlt qgt
[PROOF STATE]
proof (prove)
using this:
N = bernoulli_stream q
q = (1 + r - d) / (u - d)
\<lbrakk>N = bernoulli_stream q; 0 < q; q < 1\<rbrakk> \<Longrightarrow> AEeq N (real_cond_exp N (G ?n) (discounted_value r (prices Mkt stk) (Suc ?n))) (discounted_value r (\<lambda>m w. (q * u + (1 - q) * d) * prices Mkt stk ?n w) (Suc ?n))
0 < q
q < 1

goal (1 subgoal):
 1. AEeq N (real_cond_exp N (G n) (discounted_value r (prices Mkt stk) (Suc n))) (discounted_value r (\<lambda>m w. (q * u + (1 - q) * d) * prices Mkt stk n w) (Suc n))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
AEeq N (real_cond_exp N (G n) (discounted_value r (prices Mkt stk) (Suc n))) (discounted_value r (\<lambda>m w. (q * u + (1 - q) * d) * prices Mkt stk n w) (Suc n))

goal (1 subgoal):
 1. AEeq N (real_cond_exp N (G n) (discounted_value r (prices Mkt stk) (Suc n))) (discounted_value r (prices Mkt stk) n)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
AEeq N (real_cond_exp N (G n) (discounted_value r (prices Mkt stk) (Suc n))) (discounted_value r (\<lambda>m w. (q * u + (1 - q) * d) * prices Mkt stk n w) (Suc n))

goal (1 subgoal):
 1. AEeq N (real_cond_exp N (G n) (discounted_value r (prices Mkt stk) (Suc n))) (discounted_value r (prices Mkt stk) n)
[PROOF STEP]
have "\<forall>w. (q * u + (1 - q) * d) * prices Mkt stk n w =
    (1+r) * prices Mkt stk n w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>w. (q * u + (1 - q) * d) * prices Mkt stk n w = (1 + r) * prices Mkt stk n w
[PROOF STEP]
using risk_neutral_param assms CRR_viable
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?q = (1 + r - d) / (u - d); viable_market Mkt\<rbrakk> \<Longrightarrow> u * ?q + d * (1 - ?q) = 1 + r
N = bernoulli_stream q
q = (1 + r - d) / (u - d)
viable_market Mkt

goal (1 subgoal):
 1. \<forall>w. (q * u + (1 - q) * d) * prices Mkt stk n w = (1 + r) * prices Mkt stk n w
[PROOF STEP]
by (simp add: mult.commute)
[PROOF STATE]
proof (state)
this:
\<forall>w. (q * u + (1 - q) * d) * prices Mkt stk n w = (1 + r) * prices Mkt stk n w

goal (1 subgoal):
 1. AEeq N (real_cond_exp N (G n) (discounted_value r (prices Mkt stk) (Suc n))) (discounted_value r (prices Mkt stk) n)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
AEeq N (real_cond_exp N (G n) (discounted_value r (prices Mkt stk) (Suc n))) (discounted_value r (\<lambda>m w. (q * u + (1 - q) * d) * prices Mkt stk n w) (Suc n))
\<forall>w. (q * u + (1 - q) * d) * prices Mkt stk n w = (1 + r) * prices Mkt stk n w
[PROOF STEP]
have "AE w in N. real_cond_exp N (G n) (discounted_value r (prices Mkt stk) (Suc n)) w =
                  discounted_value r (\<lambda>m w. (1+r) * prices Mkt stk n w) (Suc n) w"
[PROOF STATE]
proof (prove)
using this:
AEeq N (real_cond_exp N (G n) (discounted_value r (prices Mkt stk) (Suc n))) (discounted_value r (\<lambda>m w. (q * u + (1 - q) * d) * prices Mkt stk n w) (Suc n))
\<forall>w. (q * u + (1 - q) * d) * prices Mkt stk n w = (1 + r) * prices Mkt stk n w

goal (1 subgoal):
 1. AEeq N (real_cond_exp N (G n) (discounted_value r (prices Mkt stk) (Suc n))) (discounted_value r (\<lambda>m w. (1 + r) * prices Mkt stk n w) (Suc n))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
AEeq N (real_cond_exp N (G n) (discounted_value r (prices Mkt stk) (Suc n))) (discounted_value r (\<lambda>m w. (1 + r) * prices Mkt stk n w) (Suc n))

goal (1 subgoal):
 1. AEeq N (real_cond_exp N (G n) (discounted_value r (prices Mkt stk) (Suc n))) (discounted_value r (prices Mkt stk) n)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
AEeq N (real_cond_exp N (G n) (discounted_value r (prices Mkt stk) (Suc n))) (discounted_value r (\<lambda>m w. (1 + r) * prices Mkt stk n w) (Suc n))

goal (1 subgoal):
 1. AEeq N (real_cond_exp N (G n) (discounted_value r (prices Mkt stk) (Suc n))) (discounted_value r (prices Mkt stk) n)
[PROOF STEP]
have "\<forall>w\<in> space N. discounted_value r (\<lambda>m w. (1+r) * prices Mkt stk n w) (Suc n) w =
                     discounted_value r (\<lambda>m w. prices Mkt stk n w) n w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>w\<in>space N. discounted_value r (\<lambda>m w. (1 + r) * prices Mkt stk n w) (Suc n) w = discounted_value r (\<lambda>m. prices Mkt stk n) n w
[PROOF STEP]
using  acceptable_rate
[PROOF STATE]
proof (prove)
using this:
- 1 < r

goal (1 subgoal):
 1. \<forall>w\<in>space N. discounted_value r (\<lambda>m w. (1 + r) * prices Mkt stk n w) (Suc n) w = discounted_value r (\<lambda>m. prices Mkt stk n) n w
[PROOF STEP]
by (simp add:discounted_mult_times_rfr)
[PROOF STATE]
proof (state)
this:
\<forall>w\<in>space N. discounted_value r (\<lambda>m w. (1 + r) * prices Mkt stk n w) (Suc n) w = discounted_value r (\<lambda>m. prices Mkt stk n) n w

goal (1 subgoal):
 1. AEeq N (real_cond_exp N (G n) (discounted_value r (prices Mkt stk) (Suc n))) (discounted_value r (prices Mkt stk) n)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>w\<in>space N. discounted_value r (\<lambda>m w. (1 + r) * prices Mkt stk n w) (Suc n) w = discounted_value r (\<lambda>m. prices Mkt stk n) n w

goal (1 subgoal):
 1. AEeq N (real_cond_exp N (G n) (discounted_value r (prices Mkt stk) (Suc n))) (discounted_value r (prices Mkt stk) n)
[PROOF STEP]
hence "\<forall>w\<in> space N. discounted_value r (\<lambda>m w. (1+r) * prices Mkt stk n w) (Suc n) w =
                     discounted_value r (prices Mkt stk) n w"
[PROOF STATE]
proof (prove)
using this:
\<forall>w\<in>space N. discounted_value r (\<lambda>m w. (1 + r) * prices Mkt stk n w) (Suc n) w = discounted_value r (\<lambda>m. prices Mkt stk n) n w

goal (1 subgoal):
 1. \<forall>w\<in>space N. discounted_value r (\<lambda>m w. (1 + r) * prices Mkt stk n w) (Suc n) w = discounted_value r (prices Mkt stk) n w
[PROOF STEP]
using  acceptable_rate
[PROOF STATE]
proof (prove)
using this:
\<forall>w\<in>space N. discounted_value r (\<lambda>m w. (1 + r) * prices Mkt stk n w) (Suc n) w = discounted_value r (\<lambda>m. prices Mkt stk n) n w
- 1 < r

goal (1 subgoal):
 1. \<forall>w\<in>space N. discounted_value r (\<lambda>m w. (1 + r) * prices Mkt stk n w) (Suc n) w = discounted_value r (prices Mkt stk) n w
[PROOF STEP]
by (simp add:discounted_value_def)
[PROOF STATE]
proof (state)
this:
\<forall>w\<in>space N. discounted_value r (\<lambda>m w. (1 + r) * prices Mkt stk n w) (Suc n) w = discounted_value r (prices Mkt stk) n w

goal (1 subgoal):
 1. AEeq N (real_cond_exp N (G n) (discounted_value r (prices Mkt stk) (Suc n))) (discounted_value r (prices Mkt stk) n)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
AEeq N (real_cond_exp N (G n) (discounted_value r (prices Mkt stk) (Suc n))) (discounted_value r (\<lambda>m w. (1 + r) * prices Mkt stk n w) (Suc n))
\<forall>w\<in>space N. discounted_value r (\<lambda>m w. (1 + r) * prices Mkt stk n w) (Suc n) w = discounted_value r (\<lambda>m. prices Mkt stk n) n w
\<forall>w\<in>space N. discounted_value r (\<lambda>m w. (1 + r) * prices Mkt stk n w) (Suc n) w = discounted_value r (prices Mkt stk) n w
[PROOF STEP]
show "AE w in N. real_cond_exp N (G n) (discounted_value r (prices Mkt stk) (Suc n)) w =
                    discounted_value r (prices Mkt stk) n w"
[PROOF STATE]
proof (prove)
using this:
AEeq N (real_cond_exp N (G n) (discounted_value r (prices Mkt stk) (Suc n))) (discounted_value r (\<lambda>m w. (1 + r) * prices Mkt stk n w) (Suc n))
\<forall>w\<in>space N. discounted_value r (\<lambda>m w. (1 + r) * prices Mkt stk n w) (Suc n) w = discounted_value r (\<lambda>m. prices Mkt stk n) n w
\<forall>w\<in>space N. discounted_value r (\<lambda>m w. (1 + r) * prices Mkt stk n w) (Suc n) w = discounted_value r (prices Mkt stk) n w

goal (1 subgoal):
 1. AEeq N (real_cond_exp N (G n) (discounted_value r (prices Mkt stk) (Suc n))) (discounted_value r (prices Mkt stk) n)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
AEeq N (real_cond_exp N (G n) (discounted_value r (prices Mkt stk) (Suc n))) (discounted_value r (prices Mkt stk) n)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma u: "u \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<in> carrier_vec n
[PROOF STEP]
unfolding u_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iP *\<^sub>v of_real_hom.vec_hom v \<in> carrier_vec n
[PROOF STEP]
using JNF(2) v
[PROOF STATE]
proof (prove)
using this:
iP \<in> carrier_mat n n
v \<in> carrier_vec n

goal (1 subgoal):
 1. iP *\<^sub>v of_real_hom.vec_hom v \<in> carrier_vec n
[PROOF STEP]
by auto


[STATEMENT]
lemma OrdP_Trans: "H \<turnstile>  OrdP k \<Longrightarrow> H \<turnstile> i IN j \<Longrightarrow> H \<turnstile> j IN k \<Longrightarrow> H  \<turnstile> i IN k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>H \<turnstile> OrdP k; H \<turnstile> i IN j; H \<turnstile> j IN k\<rbrakk> \<Longrightarrow> H \<turnstile> i IN k
[PROOF STEP]
by (blast intro: cut3 [OF OrdP_Trans_lemma])


[STATEMENT]
lemma g_bnd_mode_cong: assumes "\<And> i. i < m \<Longrightarrow> gso fs i = gso fs' i"
  shows "g_bnd_mode first b fs = g_bnd_mode first b fs'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g_bnd_mode first b fs = g_bnd_mode first b fs'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?i2 < m \<Longrightarrow> gram_schmidt_fs.gso n (map of_int_hom.vec_hom fs) ?i2 = gram_schmidt_fs.gso n (map of_int_hom.vec_hom fs') ?i2

goal (1 subgoal):
 1. g_bnd_mode first b fs = g_bnd_mode first b fs'
[PROOF STEP]
unfolding g_bnd_mode_def g_bnd_def
[PROOF STATE]
proof (prove)
using this:
?i2 < m \<Longrightarrow> gram_schmidt_fs.gso n (map of_int_hom.vec_hom fs) ?i2 = gram_schmidt_fs.gso n (map of_int_hom.vec_hom fs') ?i2

goal (1 subgoal):
 1. (if first \<and> m \<noteq> 0 then \<parallel>gram_schmidt_fs.gso n (map of_int_hom.vec_hom fs) 0\<parallel>\<^sup>2 \<le> b else \<forall>i<m. \<parallel>gram_schmidt_fs.gso n (map of_int_hom.vec_hom fs) i\<parallel>\<^sup>2 \<le> b) = (if first \<and> m \<noteq> 0 then \<parallel>gram_schmidt_fs.gso n (map of_int_hom.vec_hom fs') 0\<parallel>\<^sup>2 \<le> b else \<forall>i<m. \<parallel>gram_schmidt_fs.gso n (map of_int_hom.vec_hom fs') i\<parallel>\<^sup>2 \<le> b)
[PROOF STEP]
by auto


[STATEMENT]
lemma greater_mix_pmf_greater_step_1_aux:
  assumes "v \<succ>[\<R>] u"
  assumes "\<alpha> \<in> {0<..<(1::real)}"
    and "\<beta> \<in> {0<..<(1::real)}"
  assumes "\<beta> > \<alpha>"
  shows "(mix_pmf \<beta> v u) \<succ>[\<R>] (mix_pmf \<alpha> v u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mix_pmf \<beta> v u \<succeq>[\<R>] mix_pmf \<alpha> v u \<and> (mix_pmf \<alpha> v u, mix_pmf \<beta> v u) \<notin> \<R>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mix_pmf \<beta> v u \<succeq>[\<R>] mix_pmf \<alpha> v u \<and> (mix_pmf \<alpha> v u, mix_pmf \<beta> v u) \<notin> \<R>
[PROOF STEP]
define t where
    t: "t = mix_pmf \<beta> v u"
[PROOF STATE]
proof (state)
this:
t = mix_pmf \<beta> v u

goal (1 subgoal):
 1. mix_pmf \<beta> v u \<succeq>[\<R>] mix_pmf \<alpha> v u \<and> (mix_pmf \<alpha> v u, mix_pmf \<beta> v u) \<notin> \<R>
[PROOF STEP]
obtain \<gamma> where
    g: "\<alpha> = \<beta> * \<gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<gamma>. \<alpha> = \<beta> * \<gamma> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis assms(2) assms(4) greaterThanLessThan_iff
        mult.commute nonzero_eq_divide_eq not_less_iff_gr_or_eq)
[PROOF STATE]
proof (state)
this:
\<alpha> = \<beta> * \<gamma>

goal (1 subgoal):
 1. mix_pmf \<beta> v u \<succeq>[\<R>] mix_pmf \<alpha> v u \<and> (mix_pmf \<alpha> v u, mix_pmf \<beta> v u) \<notin> \<R>
[PROOF STEP]
have g1: "\<gamma> > 0 \<and> \<gamma> < 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < \<gamma> \<and> \<gamma> < 1
[PROOF STEP]
by (metis (full_types) assms(2) assms(4) g greaterThanLessThan_iff
        less_trans mult.right_neutral mult_less_cancel_left_pos not_le
        sgn_le_0_iff sgn_pos zero_le_one zero_le_sgn_iff zero_less_mult_iff)
[PROOF STATE]
proof (state)
this:
0 < \<gamma> \<and> \<gamma> < 1

goal (1 subgoal):
 1. mix_pmf \<beta> v u \<succeq>[\<R>] mix_pmf \<alpha> v u \<and> (mix_pmf \<alpha> v u, mix_pmf \<beta> v u) \<notin> \<R>
[PROOF STEP]
have t_in: "mix_pmf \<beta> v u \<in> \
"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mix_pmf \<beta> v u \<in> local.\

[PROOF STEP]
by (meson assms(1) assms(3) mix_pmf_in_lotteries preference_def rational_preference_def rpr)
[PROOF STATE]
proof (state)
this:
mix_pmf \<beta> v u \<in> local.\

goal (1 subgoal):
 1. mix_pmf \<beta> v u \<succeq>[\<R>] mix_pmf \<alpha> v u \<and> (mix_pmf \<alpha> v u, mix_pmf \<beta> v u) \<notin> \<R>
[PROOF STEP]
have "v \<succ>[\<R>] mix_pmf (1 - \<beta>) v u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<succeq>[\<R>] mix_pmf (1 - \<beta>) v u \<and> (mix_pmf (1 - \<beta>) v u, v) \<notin> \<R>
[PROOF STEP]
using x_sg_y_sg_mpmf_right[of u v "1-\<beta>"] assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>u \<succeq>[\<R>] v \<and> (v, u) \<notin> \<R>; 1 - \<beta> \<in> {0<..1}\<rbrakk> \<Longrightarrow> u \<succeq>[\<R>] mix_pmf (1 - \<beta>) v u \<and> (mix_pmf (1 - \<beta>) v u, u) \<notin> \<R>
v \<succeq>[\<R>] u \<and> (u, v) \<notin> \<R>
\<alpha> \<in> {0<..<1}
\<beta> \<in> {0<..<1}
\<alpha> < \<beta>

goal (1 subgoal):
 1. v \<succeq>[\<R>] mix_pmf (1 - \<beta>) v u \<and> (mix_pmf (1 - \<beta>) v u, v) \<notin> \<R>
[PROOF STEP]
by (metis atLeastAtMost_iff greaterThanAtMost_iff greaterThanLessThan_iff
        less_eq_real_def pmf_inverse_switch_eqals x_sg_y_sg_mpmf_right)
[PROOF STATE]
proof (state)
this:
v \<succeq>[\<R>] mix_pmf (1 - \<beta>) v u \<and> (mix_pmf (1 - \<beta>) v u, v) \<notin> \<R>

goal (1 subgoal):
 1. mix_pmf \<beta> v u \<succeq>[\<R>] mix_pmf \<alpha> v u \<and> (mix_pmf \<alpha> v u, mix_pmf \<beta> v u) \<notin> \<R>
[PROOF STEP]
have "t \<succ>[\<R>] u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<succeq>[\<R>] u \<and> (u, t) \<notin> \<R>
[PROOF STEP]
using assms(1) assms(3) ind rpr sg_imp_mix_sg t
[PROOF STATE]
proof (prove)
using this:
v \<succeq>[\<R>] u \<and> (u, v) \<notin> \<R>
\<beta> \<in> {0<..<1}
independent_vnm local.\
 \<R>
rational_preference local.\
 \<R>
\<lbrakk>?x \<succeq>[?\<R>] ?y \<and> (?y, ?x) \<notin> ?\<R>; rational_preference (Neumann_Morgenstern_Utility_Theorem.\
 ?outcomes) ?\<R>; independent_vnm (Neumann_Morgenstern_Utility_Theorem.\
 ?outcomes) ?\<R>; ?\<alpha> \<in> {0<..1}\<rbrakk> \<Longrightarrow> mix_pmf ?\<alpha> ?x ?y \<succeq>[?\<R>] ?y \<and> (?y, mix_pmf ?\<alpha> ?x ?y) \<notin> ?\<R>
t = mix_pmf \<beta> v u

goal (1 subgoal):
 1. t \<succeq>[\<R>] u \<and> (u, t) \<notin> \<R>
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
t \<succeq>[\<R>] u \<and> (u, t) \<notin> \<R>

goal (1 subgoal):
 1. mix_pmf \<beta> v u \<succeq>[\<R>] mix_pmf \<alpha> v u \<and> (mix_pmf \<alpha> v u, mix_pmf \<beta> v u) \<notin> \<R>
[PROOF STEP]
hence t_s: "t \<succ>[\<R>] (mix_pmf \<gamma> t u)"
[PROOF STATE]
proof (prove)
using this:
t \<succeq>[\<R>] u \<and> (u, t) \<notin> \<R>

goal (1 subgoal):
 1. t \<succeq>[\<R>] mix_pmf \<gamma> t u \<and> (mix_pmf \<gamma> t u, t) \<notin> \<R>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. t \<succeq>[\<R>] u \<and> (u, t) \<notin> \<R> \<Longrightarrow> t \<succeq>[\<R>] mix_pmf \<gamma> t u \<and> (mix_pmf \<gamma> t u, t) \<notin> \<R>
[PROOF STEP]
have "(mix_pmf \<gamma> t u) \<in> \
"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mix_pmf \<gamma> t u \<in> local.\

[PROOF STEP]
by (metis assms(1) assms(3) atLeastAtMost_iff g1 mix_in_lot mix_pmf_in_lotteries
          not_less order.asym preference_def rational_preference_def rpr t)
[PROOF STATE]
proof (state)
this:
mix_pmf \<gamma> t u \<in> local.\

goal (1 subgoal):
 1. t \<succeq>[\<R>] u \<and> (u, t) \<notin> \<R> \<Longrightarrow> t \<succeq>[\<R>] mix_pmf \<gamma> t u \<and> (mix_pmf \<gamma> t u, t) \<notin> \<R>
[PROOF STEP]
have "t \<succ>[\<R>] mix_pmf \<gamma> (mix_pmf \<beta> v u) u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<succeq>[\<R>] mix_pmf \<gamma> (mix_pmf \<beta> v u) u \<and> (mix_pmf \<gamma> (mix_pmf \<beta> v u) u, t) \<notin> \<R>
[PROOF STEP]
using neumann_3B_b[of t u \<gamma>] assms t g1
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>t \<succeq>[\<R>] u \<and> (u, t) \<notin> \<R>; \<gamma> \<in> {0<..<1}\<rbrakk> \<Longrightarrow> t \<succeq>[\<R>] mix_pmf \<gamma> t u \<and> (mix_pmf \<gamma> t u, t) \<notin> \<R>
v \<succeq>[\<R>] u \<and> (u, v) \<notin> \<R>
\<alpha> \<in> {0<..<1}
\<beta> \<in> {0<..<1}
\<alpha> < \<beta>
t = mix_pmf \<beta> v u
0 < \<gamma> \<and> \<gamma> < 1

goal (1 subgoal):
 1. t \<succeq>[\<R>] mix_pmf \<gamma> (mix_pmf \<beta> v u) u \<and> (mix_pmf \<gamma> (mix_pmf \<beta> v u) u, t) \<notin> \<R>
[PROOF STEP]
by (meson greaterThanAtMost_iff greaterThanLessThan_iff
          ind less_eq_real_def rpr sg_imp_mix_sg)
[PROOF STATE]
proof (state)
this:
t \<succeq>[\<R>] mix_pmf \<gamma> (mix_pmf \<beta> v u) u \<and> (mix_pmf \<gamma> (mix_pmf \<beta> v u) u, t) \<notin> \<R>

goal (1 subgoal):
 1. t \<succeq>[\<R>] u \<and> (u, t) \<notin> \<R> \<Longrightarrow> t \<succeq>[\<R>] mix_pmf \<gamma> t u \<and> (mix_pmf \<gamma> t u, t) \<notin> \<R>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
t \<succeq>[\<R>] mix_pmf \<gamma> (mix_pmf \<beta> v u) u \<and> (mix_pmf \<gamma> (mix_pmf \<beta> v u) u, t) \<notin> \<R>

goal (1 subgoal):
 1. t \<succeq>[\<R>] mix_pmf \<gamma> t u \<and> (mix_pmf \<gamma> t u, t) \<notin> \<R>
[PROOF STEP]
using t
[PROOF STATE]
proof (prove)
using this:
t \<succeq>[\<R>] mix_pmf \<gamma> (mix_pmf \<beta> v u) u \<and> (mix_pmf \<gamma> (mix_pmf \<beta> v u) u, t) \<notin> \<R>
t = mix_pmf \<beta> v u

goal (1 subgoal):
 1. t \<succeq>[\<R>] mix_pmf \<gamma> t u \<and> (mix_pmf \<gamma> t u, t) \<notin> \<R>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
t \<succeq>[\<R>] mix_pmf \<gamma> t u \<and> (mix_pmf \<gamma> t u, t) \<notin> \<R>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
t \<succeq>[\<R>] mix_pmf \<gamma> t u \<and> (mix_pmf \<gamma> t u, t) \<notin> \<R>

goal (1 subgoal):
 1. mix_pmf \<beta> v u \<succeq>[\<R>] mix_pmf \<alpha> v u \<and> (mix_pmf \<alpha> v u, mix_pmf \<beta> v u) \<notin> \<R>
[PROOF STEP]
from product_mix_pmf_prob_distrib[of _ \<beta> v u] assms
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?a \<in> {0..1}; \<beta> \<in> {0..1}\<rbrakk> \<Longrightarrow> mix_pmf ?a (mix_pmf \<beta> v u) u = mix_pmf (?a * \<beta>) v u
v \<succeq>[\<R>] u \<and> (u, v) \<notin> \<R>
\<alpha> \<in> {0<..<1}
\<beta> \<in> {0<..<1}
\<alpha> < \<beta>
[PROOF STEP]
have "mix_pmf \<beta> v u \<succ>[\<R>] mix_pmf \<alpha> v u"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?a \<in> {0..1}; \<beta> \<in> {0..1}\<rbrakk> \<Longrightarrow> mix_pmf ?a (mix_pmf \<beta> v u) u = mix_pmf (?a * \<beta>) v u
v \<succeq>[\<R>] u \<and> (u, v) \<notin> \<R>
\<alpha> \<in> {0<..<1}
\<beta> \<in> {0<..<1}
\<alpha> < \<beta>

goal (1 subgoal):
 1. mix_pmf \<beta> v u \<succeq>[\<R>] mix_pmf \<alpha> v u \<and> (mix_pmf \<alpha> v u, mix_pmf \<beta> v u) \<notin> \<R>
[PROOF STEP]
by (metis t_s atLeastAtMost_iff g g1 greaterThanLessThan_iff less_eq_real_def mult.commute t)
[PROOF STATE]
proof (state)
this:
mix_pmf \<beta> v u \<succeq>[\<R>] mix_pmf \<alpha> v u \<and> (mix_pmf \<alpha> v u, mix_pmf \<beta> v u) \<notin> \<R>

goal (1 subgoal):
 1. mix_pmf \<beta> v u \<succeq>[\<R>] mix_pmf \<alpha> v u \<and> (mix_pmf \<alpha> v u, mix_pmf \<beta> v u) \<notin> \<R>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
mix_pmf \<beta> v u \<succeq>[\<R>] mix_pmf \<alpha> v u \<and> (mix_pmf \<alpha> v u, mix_pmf \<beta> v u) \<notin> \<R>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
mix_pmf \<beta> v u \<succeq>[\<R>] mix_pmf \<alpha> v u \<and> (mix_pmf \<alpha> v u, mix_pmf \<beta> v u) \<notin> \<R>

goal (1 subgoal):
 1. mix_pmf \<beta> v u \<succeq>[\<R>] mix_pmf \<alpha> v u \<and> (mix_pmf \<alpha> v u, mix_pmf \<beta> v u) \<notin> \<R>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
mix_pmf \<beta> v u \<succeq>[\<R>] mix_pmf \<alpha> v u \<and> (mix_pmf \<alpha> v u, mix_pmf \<beta> v u) \<notin> \<R>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma exists_worst_degenerate:
  "\<exists>x \<in> degenerate_lotteries. \<forall>y \<in> degenerate_lotteries. y \<succeq>[\<R>] x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x\<in>degenerate_lotteries. \<forall>y\<in>degenerate_lotteries. y \<succeq>[\<R>] x
[PROOF STEP]
using degenerate_has_min_preferred
[PROOF STATE]
proof (prove)
using this:
{x \<in> degenerate_lotteries. \<forall>y\<in>degenerate_lotteries. y \<succeq>[\<R>] x} \<noteq> {}

goal (1 subgoal):
 1. \<exists>x\<in>degenerate_lotteries. \<forall>y\<in>degenerate_lotteries. y \<succeq>[\<R>] x
[PROOF STEP]
by blast


[STATEMENT]
lemma i_drop_nth_sub: "n \<le> x \<Longrightarrow> (s \<Up> n) (x - n) = s x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<le> x \<Longrightarrow> (s \<Up> n) (x - n) = s x
[PROOF STEP]
by (simp add: i_drop_def)


[STATEMENT]
lemma resChainI:
  fixes P   :: pi
  and   Q   :: pi
  and   Rel :: "(pi \<times> pi) set"
  and   lst :: "name list"

  assumes eqvtRel: "eqvt Rel"
  and     Res:     "\<And>R S x. (R, S) \<in> Rel \<Longrightarrow> (<\<nu>x>R, <\<nu>x>S) \<in> Rel"
  and     PRelQ:   "P \<leadsto>\<guillemotleft>Rel\<guillemotright> Q"

  shows "(resChain lst) P \<leadsto>\<guillemotleft>Rel\<guillemotright> (resChain lst) Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. resChain lst P \<leadsto>\<guillemotleft>Rel\<guillemotright> resChain lst Q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. resChain lst P \<leadsto>\<guillemotleft>Rel\<guillemotright> resChain lst Q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. resChain lst P \<leadsto>\<guillemotleft>Rel\<guillemotright> resChain lst Q
[PROOF STEP]
proof(induct lst)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. resChain [] P \<leadsto>\<guillemotleft>Rel\<guillemotright> resChain [] Q
 2. \<And>a lst. resChain lst P \<leadsto>\<guillemotleft>Rel\<guillemotright> resChain lst Q \<Longrightarrow> resChain (a # lst) P \<leadsto>\<guillemotleft>Rel\<guillemotright> resChain (a # lst) Q
[PROOF STEP]
(* Base case *)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. resChain [] P \<leadsto>\<guillemotleft>Rel\<guillemotright> resChain [] Q
 2. \<And>a lst. resChain lst P \<leadsto>\<guillemotleft>Rel\<guillemotright> resChain lst Q \<Longrightarrow> resChain (a # lst) P \<leadsto>\<guillemotleft>Rel\<guillemotright> resChain (a # lst) Q
[PROOF STEP]
from PRelQ
[PROOF STATE]
proof (chain)
picking this:
P \<leadsto>\<guillemotleft>Rel\<guillemotright> Q
[PROOF STEP]
show "resChain [] P \<leadsto>\<guillemotleft>Rel\<guillemotright> resChain [] Q"
[PROOF STATE]
proof (prove)
using this:
P \<leadsto>\<guillemotleft>Rel\<guillemotright> Q

goal (1 subgoal):
 1. resChain [] P \<leadsto>\<guillemotleft>Rel\<guillemotright> resChain [] Q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
resChain [] P \<leadsto>\<guillemotleft>Rel\<guillemotright> resChain [] Q

goal (1 subgoal):
 1. \<And>a lst. resChain lst P \<leadsto>\<guillemotleft>Rel\<guillemotright> resChain lst Q \<Longrightarrow> resChain (a # lst) P \<leadsto>\<guillemotleft>Rel\<guillemotright> resChain (a # lst) Q
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a lst. resChain lst P \<leadsto>\<guillemotleft>Rel\<guillemotright> resChain lst Q \<Longrightarrow> resChain (a # lst) P \<leadsto>\<guillemotleft>Rel\<guillemotright> resChain (a # lst) Q
[PROOF STEP]
(* Inductive step *)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a lst. resChain lst P \<leadsto>\<guillemotleft>Rel\<guillemotright> resChain lst Q \<Longrightarrow> resChain (a # lst) P \<leadsto>\<guillemotleft>Rel\<guillemotright> resChain (a # lst) Q
[PROOF STEP]
fix a lst
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a lst. resChain lst P \<leadsto>\<guillemotleft>Rel\<guillemotright> resChain lst Q \<Longrightarrow> resChain (a # lst) P \<leadsto>\<guillemotleft>Rel\<guillemotright> resChain (a # lst) Q
[PROOF STEP]
assume IH: "(resChain lst P) \<leadsto>\<guillemotleft>Rel\<guillemotright> (resChain lst Q)"
[PROOF STATE]
proof (state)
this:
resChain lst P \<leadsto>\<guillemotleft>Rel\<guillemotright> resChain lst Q

goal (1 subgoal):
 1. \<And>a lst. resChain lst P \<leadsto>\<guillemotleft>Rel\<guillemotright> resChain lst Q \<Longrightarrow> resChain (a # lst) P \<leadsto>\<guillemotleft>Rel\<guillemotright> resChain (a # lst) Q
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
resChain lst P \<leadsto>\<guillemotleft>Rel\<guillemotright> resChain lst Q

goal (1 subgoal):
 1. \<And>a lst. resChain lst P \<leadsto>\<guillemotleft>Rel\<guillemotright> resChain lst Q \<Longrightarrow> resChain (a # lst) P \<leadsto>\<guillemotleft>Rel\<guillemotright> resChain (a # lst) Q
[PROOF STEP]
from Res
[PROOF STATE]
proof (chain)
picking this:
(?R, ?S) \<in> Rel \<Longrightarrow> (<\<nu>?x>?R, <\<nu>?x>?S) \<in> Rel
[PROOF STEP]
have "\<And>P Q a. (P, Q) \<in> Rel \<Longrightarrow> (<\<nu>a>P, <\<nu>a>Q) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
(?R, ?S) \<in> Rel \<Longrightarrow> (<\<nu>?x>?R, <\<nu>?x>?S) \<in> Rel

goal (1 subgoal):
 1. \<And>P Q a. (P, Q) \<in> Rel \<Longrightarrow> (<\<nu>a>P, <\<nu>a>Q) \<in> Rel
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(?P, ?Q) \<in> Rel \<Longrightarrow> (<\<nu>?a>?P, <\<nu>?a>?Q) \<in> Rel

goal (1 subgoal):
 1. \<And>a lst. resChain lst P \<leadsto>\<guillemotleft>Rel\<guillemotright> resChain lst Q \<Longrightarrow> resChain (a # lst) P \<leadsto>\<guillemotleft>Rel\<guillemotright> resChain (a # lst) Q
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(?P, ?Q) \<in> Rel \<Longrightarrow> (<\<nu>?a>?P, <\<nu>?a>?Q) \<in> Rel

goal (1 subgoal):
 1. \<And>a lst. resChain lst P \<leadsto>\<guillemotleft>Rel\<guillemotright> resChain lst Q \<Longrightarrow> resChain (a # lst) P \<leadsto>\<guillemotleft>Rel\<guillemotright> resChain (a # lst) Q
[PROOF STEP]
have "Rel \<subseteq> Rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rel \<subseteq> Rel
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Rel \<subseteq> Rel

goal (1 subgoal):
 1. \<And>a lst. resChain lst P \<leadsto>\<guillemotleft>Rel\<guillemotright> resChain lst Q \<Longrightarrow> resChain (a # lst) P \<leadsto>\<guillemotleft>Rel\<guillemotright> resChain (a # lst) Q
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
resChain lst P \<leadsto>\<guillemotleft>Rel\<guillemotright> resChain lst Q
(?P, ?Q) \<in> Rel \<Longrightarrow> (<\<nu>?a>?P, <\<nu>?a>?Q) \<in> Rel
Rel \<subseteq> Rel
[PROOF STEP]
have "<\<nu>a>(resChain lst P) \<leadsto>\<guillemotleft>Rel\<guillemotright> <\<nu>a>(resChain lst Q)"
[PROOF STATE]
proof (prove)
using this:
resChain lst P \<leadsto>\<guillemotleft>Rel\<guillemotright> resChain lst Q
(?P, ?Q) \<in> Rel \<Longrightarrow> (<\<nu>?a>?P, <\<nu>?a>?Q) \<in> Rel
Rel \<subseteq> Rel

goal (1 subgoal):
 1. <\<nu>a>resChain lst P \<leadsto>\<guillemotleft>Rel\<guillemotright> <\<nu>a>resChain lst Q
[PROOF STEP]
using eqvtRel
[PROOF STATE]
proof (prove)
using this:
resChain lst P \<leadsto>\<guillemotleft>Rel\<guillemotright> resChain lst Q
(?P, ?Q) \<in> Rel \<Longrightarrow> (<\<nu>?a>?P, <\<nu>?a>?Q) \<in> Rel
Rel \<subseteq> Rel
eqvt Rel

goal (1 subgoal):
 1. <\<nu>a>resChain lst P \<leadsto>\<guillemotleft>Rel\<guillemotright> <\<nu>a>resChain lst Q
[PROOF STEP]
by(rule_tac resPres)
[PROOF STATE]
proof (state)
this:
<\<nu>a>resChain lst P \<leadsto>\<guillemotleft>Rel\<guillemotright> <\<nu>a>resChain lst Q

goal (1 subgoal):
 1. \<And>a lst. resChain lst P \<leadsto>\<guillemotleft>Rel\<guillemotright> resChain lst Q \<Longrightarrow> resChain (a # lst) P \<leadsto>\<guillemotleft>Rel\<guillemotright> resChain (a # lst) Q
[PROOF STEP]
thus "resChain (a # lst) P \<leadsto>\<guillemotleft>Rel\<guillemotright> resChain (a # lst) Q"
[PROOF STATE]
proof (prove)
using this:
<\<nu>a>resChain lst P \<leadsto>\<guillemotleft>Rel\<guillemotright> <\<nu>a>resChain lst Q

goal (1 subgoal):
 1. resChain (a # lst) P \<leadsto>\<guillemotleft>Rel\<guillemotright> resChain (a # lst) Q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
resChain (a # lst) P \<leadsto>\<guillemotleft>Rel\<guillemotright> resChain (a # lst) Q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
resChain lst P \<leadsto>\<guillemotleft>Rel\<guillemotright> resChain lst Q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma S_ffUnion: "S e = ffUnion (fimage (\<lambda>((s, s'), _). {|s, s'|}) e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S e = ffUnion ((\<lambda>((s, s'), uu_). {|s, s'|}) |`| e)
[PROOF STEP]
unfolding S_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>((s, s'), t). s) |`| e |\<union>| (\<lambda>((s, s'), t). s') |`| e = ffUnion ((\<lambda>((s, s'), uu_). {|s, s'|}) |`| e)
[PROOF STEP]
by(induct e, auto)


[STATEMENT]
lemma ldrop_trans_fusion2 [stream_fusion]:
  "lunstream (ldrop_trans (lgenerator g)) (n, s) = ldrop n (lunstream' g s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lunstream (ldrop_trans (lgenerator g)) (n, s) = ldrop n (lunstream' g s)
[PROOF STEP]
by transfer (rule ldrop_trans_fusion)


[STATEMENT]
lemma divisor_sigma_0 [simp]: "divisor_sigma x 0 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. divisor_sigma x 0 = (0::'a)
[PROOF STEP]
by (simp add: divisor_sigma_def)


[STATEMENT]
lemma to_R1_complement:
  shows "to_R1` (carrier R - A) = carrier (R\<^bsup>1\<^esup>) - to_R1` A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>a. [a]) ` (carrier R - A) = carrier (R\<^bsup>1\<^esup>) - (\<lambda>a. [a]) ` A
[PROOF STEP]
by (metis to_R1_carrier to_R1_diff)


[STATEMENT]
lemma splitting_permutation_case_1_unique:
  assumes "i \<le> l1"
  assumes "y < i"
  assumes "splitting_permutation l1 l2 i j = y"
  shows "j = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j = y
[PROOF STEP]
unfolding splitting_permutation_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j = y
[PROOF STEP]
using assms(2) assms(3) splitting_permutation_def
[PROOF STATE]
proof (prove)
using this:
y < i
splitting_permutation l1 l2 i j = y
splitting_permutation ?l1.0 ?l2.0 ?i ?j = (if ?j < ?i then ?j else if ?i \<le> ?j \<and> ?j < ?l1.0 then ?l2.0 + ?j else if ?j < ?l1.0 + ?l2.0 then ?j - ?l1.0 + ?i else ?j)

goal (1 subgoal):
 1. j = y
[PROOF STEP]
by auto


[STATEMENT]
lemma intersperseE'':
  assumes "\<sigma> permutes ({..<n})"
  assumes "length as + length bs = n"
  assumes "length as = k"
  assumes "i < n"
  assumes "\<sigma> i \<ge> k"
  shows "(intersperse \<sigma> as bs)! i  = bs ! ((\<sigma> i) - k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. intersperse \<sigma> as bs ! i = bs ! (\<sigma> i - k)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. intersperse \<sigma> as bs ! i = bs ! (\<sigma> i - k)
[PROOF STEP]
have 0: "permute_list \<sigma> (as @ bs) ! i = (as @ bs) ! \<sigma> i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. permute_list \<sigma> (as @ bs) ! i = (as @ bs) ! \<sigma> i
[PROOF STEP]
using assms permute_list_nth[of \<sigma> "(as@bs)" i]
[PROOF STATE]
proof (prove)
using this:
\<sigma> permutes {..<n}
length as + length bs = n
length as = k
i < n
k \<le> \<sigma> i
\<lbrakk>\<sigma> permutes {..<length (as @ bs)}; i < length (as @ bs)\<rbrakk> \<Longrightarrow> permute_list \<sigma> (as @ bs) ! i = (as @ bs) ! \<sigma> i

goal (1 subgoal):
 1. permute_list \<sigma> (as @ bs) ! i = (as @ bs) ! \<sigma> i
[PROOF STEP]
unfolding intersperse_def
[PROOF STATE]
proof (prove)
using this:
\<sigma> permutes {..<n}
length as + length bs = n
length as = k
i < n
k \<le> \<sigma> i
\<lbrakk>\<sigma> permutes {..<length (as @ bs)}; i < length (as @ bs)\<rbrakk> \<Longrightarrow> permute_list \<sigma> (as @ bs) ! i = (as @ bs) ! \<sigma> i

goal (1 subgoal):
 1. permute_list \<sigma> (as @ bs) ! i = (as @ bs) ! \<sigma> i
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<sigma> permutes {..<n}; length as + length bs = n; length as = k; i < n; k \<le> \<sigma> i; \<lbrakk>\<sigma> permutes {..<length (as @ bs)}; i < length (as @ bs)\<rbrakk> \<Longrightarrow> permute_list \<sigma> (as @ bs) ! i = (as @ bs) ! \<sigma> i\<rbrakk> \<Longrightarrow> permute_list \<sigma> (as @ bs) ! i = (as @ bs) ! \<sigma> i
[PROOF STEP]
have "(as @ bs) ! \<sigma> i = (as @ bs) ! \<sigma> ([0..<n] ! i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (as @ bs) ! \<sigma> i = (as @ bs) ! \<sigma> ([0..<n] ! i)
[PROOF STEP]
by (simp add: \<open>i < n\<close>)
[PROOF STATE]
proof (state)
this:
(as @ bs) ! \<sigma> i = (as @ bs) ! \<sigma> ([0..<n] ! i)

goal (1 subgoal):
 1. \<lbrakk>\<sigma> permutes {..<n}; length as + length bs = n; length as = k; i < n; k \<le> \<sigma> i; \<lbrakk>\<sigma> permutes {..<length (as @ bs)}; i < length (as @ bs)\<rbrakk> \<Longrightarrow> permute_list \<sigma> (as @ bs) ! i = (as @ bs) ! \<sigma> i\<rbrakk> \<Longrightarrow> permute_list \<sigma> (as @ bs) ! i = (as @ bs) ! \<sigma> i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(as @ bs) ! \<sigma> i = (as @ bs) ! \<sigma> ([0..<n] ! i)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(as @ bs) ! \<sigma> i = (as @ bs) ! \<sigma> ([0..<n] ! i)

goal (1 subgoal):
 1. permute_list \<sigma> (as @ bs) ! i = (as @ bs) ! \<sigma> i
[PROOF STEP]
by (metis (no_types) \<open>i < n\<close> \<open>length as + length bs = n\<close> diff_zero length_append
          length_upt nth_map permute_list_def)
[PROOF STATE]
proof (state)
this:
permute_list \<sigma> (as @ bs) ! i = (as @ bs) ! \<sigma> i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
permute_list \<sigma> (as @ bs) ! i = (as @ bs) ! \<sigma> i

goal (1 subgoal):
 1. intersperse \<sigma> as bs ! i = bs ! (\<sigma> i - k)
[PROOF STEP]
have 1: "\<sigma> i < n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma> i < n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<sigma> permutes {..<n}
length as + length bs = n
length as = k
i < n
k \<le> \<sigma> i

goal (1 subgoal):
 1. \<sigma> i < n
[PROOF STEP]
by (meson lessThan_iff permutes_in_image)
[PROOF STATE]
proof (state)
this:
\<sigma> i < n

goal (1 subgoal):
 1. intersperse \<sigma> as bs ! i = bs ! (\<sigma> i - k)
[PROOF STEP]
have 2: "(\<sigma> i) - k < length bs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma> i - k < length bs
[PROOF STEP]
using "1" assms(2) assms(3) assms(5)
[PROOF STATE]
proof (prove)
using this:
\<sigma> i < n
length as + length bs = n
length as = k
k \<le> \<sigma> i

goal (1 subgoal):
 1. \<sigma> i - k < length bs
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
\<sigma> i - k < length bs

goal (1 subgoal):
 1. intersperse \<sigma> as bs ! i = bs ! (\<sigma> i - k)
[PROOF STEP]
have "(as @ bs) ! (\<sigma> i)  =  bs ! (\<sigma> i - length as)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (as @ bs) ! \<sigma> i = bs ! (\<sigma> i - length as)
[PROOF STEP]
using assms 1 2 nth_append[of as bs "(\<sigma> i)"]
[PROOF STATE]
proof (prove)
using this:
\<sigma> permutes {..<n}
length as + length bs = n
length as = k
i < n
k \<le> \<sigma> i
\<sigma> i < n
\<sigma> i - k < length bs
(as @ bs) ! \<sigma> i = (if \<sigma> i < length as then as ! \<sigma> i else bs ! (\<sigma> i - length as))

goal (1 subgoal):
 1. (as @ bs) ! \<sigma> i = bs ! (\<sigma> i - length as)
[PROOF STEP]
by (meson not_le)
[PROOF STATE]
proof (state)
this:
(as @ bs) ! \<sigma> i = bs ! (\<sigma> i - length as)

goal (1 subgoal):
 1. intersperse \<sigma> as bs ! i = bs ! (\<sigma> i - k)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(as @ bs) ! \<sigma> i = bs ! (\<sigma> i - length as)
[PROOF STEP]
have 3: "(as @ bs) ! (\<sigma> i)  =  bs ! (\<sigma> i - k)"
[PROOF STATE]
proof (prove)
using this:
(as @ bs) ! \<sigma> i = bs ! (\<sigma> i - length as)

goal (1 subgoal):
 1. (as @ bs) ! \<sigma> i = bs ! (\<sigma> i - k)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(as @ bs) ! \<sigma> i = bs ! (\<sigma> i - length as)
\<sigma> permutes {..<n}
length as + length bs = n
length as = k
i < n
k \<le> \<sigma> i

goal (1 subgoal):
 1. (as @ bs) ! \<sigma> i = bs ! (\<sigma> i - k)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(as @ bs) ! \<sigma> i = bs ! (\<sigma> i - k)

goal (1 subgoal):
 1. intersperse \<sigma> as bs ! i = bs ! (\<sigma> i - k)
[PROOF STEP]
have 4: "permute_list \<sigma> (as @ bs) ! i = (as @ bs) ! (\<sigma> i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. permute_list \<sigma> (as @ bs) ! i = (as @ bs) ! \<sigma> i
[PROOF STEP]
using "0"
[PROOF STATE]
proof (prove)
using this:
permute_list \<sigma> (as @ bs) ! i = (as @ bs) ! \<sigma> i

goal (1 subgoal):
 1. permute_list \<sigma> (as @ bs) ! i = (as @ bs) ! \<sigma> i
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
permute_list \<sigma> (as @ bs) ! i = (as @ bs) ! \<sigma> i

goal (1 subgoal):
 1. intersperse \<sigma> as bs ! i = bs ! (\<sigma> i - k)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. intersperse \<sigma> as bs ! i = bs ! (\<sigma> i - k)
[PROOF STEP]
using 4 3
[PROOF STATE]
proof (prove)
using this:
permute_list \<sigma> (as @ bs) ! i = (as @ bs) ! \<sigma> i
(as @ bs) ! \<sigma> i = bs ! (\<sigma> i - k)

goal (1 subgoal):
 1. intersperse \<sigma> as bs ! i = bs ! (\<sigma> i - k)
[PROOF STEP]
unfolding intersperse_def
[PROOF STATE]
proof (prove)
using this:
permute_list \<sigma> (as @ bs) ! i = (as @ bs) ! \<sigma> i
(as @ bs) ! \<sigma> i = bs ! (\<sigma> i - k)

goal (1 subgoal):
 1. permute_list \<sigma> (as @ bs) ! i = bs ! (\<sigma> i - k)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
intersperse \<sigma> as bs ! i = bs ! (\<sigma> i - k)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma coord_partial_eval_generic_poly_lt':
  assumes "as \<in> carrier (R\<^bsup>Suc n\<^esup>)"
  shows "coord_partial_eval R {1..<n+2} (\<zero>\<^bsub>R\<^esub>#as) (generic_poly_lt R n) =
        poly_scalar_mult R (as!n) ((pvar R 0)[^]\<^bsub>coord_ring R 1\<^esub> n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coord_partial_eval R {1..<n + 2} (\<zero> # as) (generic_poly_lt R n) = poly_scalar_mult R (as ! n) (pvar R 0 [^]\<^bsub>R [\<X>\<^bsub>1\<^esub>]\<^esub> n)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. coord_partial_eval R {1..<n + 2} (\<zero> # as) (generic_poly_lt R n) = poly_scalar_mult R (as ! n) (pvar R 0 [^]\<^bsub>R [\<X>\<^bsub>1\<^esub>]\<^esub> n)
[PROOF STEP]
have 0: "coord_partial_eval R {1..<n+2} (\<zero>\<^bsub>R\<^esub>#as) (generic_poly_lt R n) =
        poly_scalar_mult R (as!n) ((pvar R 0)[^]\<^bsub>coord_ring R (n+2)\<^esub> n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coord_partial_eval R {1..<n + 2} (\<zero> # as) (generic_poly_lt R n) = poly_scalar_mult R (as ! n) (pvar R 0 [^]\<^bsub>R [\<X>\<^bsub>n + 2\<^esub>]\<^esub> n)
[PROOF STEP]
using assms coord_partial_eval_generic_poly_lt
[PROOF STATE]
proof (prove)
using this:
as \<in> carrier (R\<^bsup>Suc n\<^esup>)
?as \<in> carrier (R\<^bsup>Suc ?n\<^esup>) \<Longrightarrow> coord_partial_eval R {1..<?n + 2} (\<zero> # ?as) (generic_poly_lt R ?n) = poly_scalar_mult R (?as ! ?n) (pvar R 0 [^]\<^bsub>R [\<X>\<^bsub>?n + 2\<^esub>]\<^esub> ?n)

goal (1 subgoal):
 1. coord_partial_eval R {1..<n + 2} (\<zero> # as) (generic_poly_lt R n) = poly_scalar_mult R (as ! n) (pvar R 0 [^]\<^bsub>R [\<X>\<^bsub>n + 2\<^esub>]\<^esub> n)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
coord_partial_eval R {1..<n + 2} (\<zero> # as) (generic_poly_lt R n) = poly_scalar_mult R (as ! n) (pvar R 0 [^]\<^bsub>R [\<X>\<^bsub>n + 2\<^esub>]\<^esub> n)

goal (1 subgoal):
 1. coord_partial_eval R {1..<n + 2} (\<zero> # as) (generic_poly_lt R n) = poly_scalar_mult R (as ! n) (pvar R 0 [^]\<^bsub>R [\<X>\<^bsub>1\<^esub>]\<^esub> n)
[PROOF STEP]
have 1: "\<And>k::nat. (pvar R 0)[^]\<^bsub>coord_ring R (n+2)\<^esub> k = (pvar R 0)[^]\<^bsub>coord_ring R 1\<^esub> k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. pvar R 0 [^]\<^bsub>R [\<X>\<^bsub>n + 2\<^esub>]\<^esub> k = pvar R 0 [^]\<^bsub>R [\<X>\<^bsub>1\<^esub>]\<^esub> k
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. pvar R 0 [^]\<^bsub>R [\<X>\<^bsub>n + 2\<^esub>]\<^esub> k = pvar R 0 [^]\<^bsub>R [\<X>\<^bsub>1\<^esub>]\<^esub> k
[PROOF STEP]
fix k::nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. pvar R 0 [^]\<^bsub>R [\<X>\<^bsub>n + 2\<^esub>]\<^esub> k = pvar R 0 [^]\<^bsub>R [\<X>\<^bsub>1\<^esub>]\<^esub> k
[PROOF STEP]
show "(pvar R 0)[^]\<^bsub>coord_ring R (n+2)\<^esub> k = (pvar R 0)[^]\<^bsub>coord_ring R 1\<^esub> k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pvar R 0 [^]\<^bsub>R [\<X>\<^bsub>n + 2\<^esub>]\<^esub> k = pvar R 0 [^]\<^bsub>R [\<X>\<^bsub>1\<^esub>]\<^esub> k
[PROOF STEP]
apply(induction k)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. pvar R 0 [^]\<^bsub>R [\<X>\<^bsub>n + 2\<^esub>]\<^esub> 0 = pvar R 0 [^]\<^bsub>R [\<X>\<^bsub>1\<^esub>]\<^esub> 0
 2. \<And>k. pvar R 0 [^]\<^bsub>R [\<X>\<^bsub>n + 2\<^esub>]\<^esub> k = pvar R 0 [^]\<^bsub>R [\<X>\<^bsub>1\<^esub>]\<^esub> k \<Longrightarrow> pvar R 0 [^]\<^bsub>R [\<X>\<^bsub>n + 2\<^esub>]\<^esub> Suc k = pvar R 0 [^]\<^bsub>R [\<X>\<^bsub>1\<^esub>]\<^esub> Suc k
[PROOF STEP]
unfolding coord_ring_def
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. pvar R 0 [^]\<^bsub>Pring R {..<n + 2}\<^esub> 0 = pvar R 0 [^]\<^bsub>Pring R {..<1}\<^esub> 0
 2. \<And>k. pvar R 0 [^]\<^bsub>Pring R {..<n + 2}\<^esub> k = pvar R 0 [^]\<^bsub>Pring R {..<1}\<^esub> k \<Longrightarrow> pvar R 0 [^]\<^bsub>Pring R {..<n + 2}\<^esub> Suc k = pvar R 0 [^]\<^bsub>Pring R {..<1}\<^esub> Suc k
[PROOF STEP]
apply (metis Group.nat_pow_0 R.Pring_one_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. pvar R 0 [^]\<^bsub>Pring R {..<n + 2}\<^esub> k = pvar R 0 [^]\<^bsub>Pring R {..<1}\<^esub> k \<Longrightarrow> pvar R 0 [^]\<^bsub>Pring R {..<n + 2}\<^esub> Suc k = pvar R 0 [^]\<^bsub>Pring R {..<1}\<^esub> Suc k
[PROOF STEP]
using nat_pow_def
[PROOF STATE]
proof (prove)
using this:
?a [^]\<^bsub>?G\<^esub> ?n = rec_nat \<one>\<^bsub>?G\<^esub> (\<lambda>u b. b \<otimes>\<^bsub>?G\<^esub> ?a) ?n

goal (1 subgoal):
 1. \<And>k. pvar R 0 [^]\<^bsub>Pring R {..<n + 2}\<^esub> k = pvar R 0 [^]\<^bsub>Pring R {..<1}\<^esub> k \<Longrightarrow> pvar R 0 [^]\<^bsub>Pring R {..<n + 2}\<^esub> Suc k = pvar R 0 [^]\<^bsub>Pring R {..<1}\<^esub> Suc k
[PROOF STEP]
by (metis R.Pring_mult_eq R.Pring_one add_2_eq_Suc')
[PROOF STATE]
proof (state)
this:
pvar R 0 [^]\<^bsub>R [\<X>\<^bsub>n + 2\<^esub>]\<^esub> k = pvar R 0 [^]\<^bsub>R [\<X>\<^bsub>1\<^esub>]\<^esub> k

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
pvar R 0 [^]\<^bsub>R [\<X>\<^bsub>n + 2\<^esub>]\<^esub> ?k30 = pvar R 0 [^]\<^bsub>R [\<X>\<^bsub>1\<^esub>]\<^esub> ?k30

goal (1 subgoal):
 1. coord_partial_eval R {1..<n + 2} (\<zero> # as) (generic_poly_lt R n) = poly_scalar_mult R (as ! n) (pvar R 0 [^]\<^bsub>R [\<X>\<^bsub>1\<^esub>]\<^esub> n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pvar R 0 [^]\<^bsub>R [\<X>\<^bsub>n + 2\<^esub>]\<^esub> ?k30 = pvar R 0 [^]\<^bsub>R [\<X>\<^bsub>1\<^esub>]\<^esub> ?k30
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
pvar R 0 [^]\<^bsub>R [\<X>\<^bsub>n + 2\<^esub>]\<^esub> ?k30 = pvar R 0 [^]\<^bsub>R [\<X>\<^bsub>1\<^esub>]\<^esub> ?k30

goal (1 subgoal):
 1. coord_partial_eval R {1..<n + 2} (\<zero> # as) (generic_poly_lt R n) = poly_scalar_mult R (as ! n) (pvar R 0 [^]\<^bsub>R [\<X>\<^bsub>1\<^esub>]\<^esub> n)
[PROOF STEP]
using "0"
[PROOF STATE]
proof (prove)
using this:
pvar R 0 [^]\<^bsub>R [\<X>\<^bsub>n + 2\<^esub>]\<^esub> ?k30 = pvar R 0 [^]\<^bsub>R [\<X>\<^bsub>1\<^esub>]\<^esub> ?k30
coord_partial_eval R {1..<n + 2} (\<zero> # as) (generic_poly_lt R n) = poly_scalar_mult R (as ! n) (pvar R 0 [^]\<^bsub>R [\<X>\<^bsub>n + 2\<^esub>]\<^esub> n)

goal (1 subgoal):
 1. coord_partial_eval R {1..<n + 2} (\<zero> # as) (generic_poly_lt R n) = poly_scalar_mult R (as ! n) (pvar R 0 [^]\<^bsub>R [\<X>\<^bsub>1\<^esub>]\<^esub> n)
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
coord_partial_eval R {1..<n + 2} (\<zero> # as) (generic_poly_lt R n) = poly_scalar_mult R (as ! n) (pvar R 0 [^]\<^bsub>R [\<X>\<^bsub>1\<^esub>]\<^esub> n)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma \<open>\<exists>p. q = compl p\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>p. q = compl p
[PROOF STEP]
by (metis compl.simps(1))


[STATEMENT]
lemma angle_sum_triangle:
  assumes "a \<noteq> b \<or> b \<noteq> c \<or> a \<noteq> c"
  shows   "angle c a b + angle a b c + angle b c a = pi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. angle c a b + angle a b c + angle b c a = pi
[PROOF STEP]
proof (rule cos_minus1_imp_pi)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. cos (angle c a b + angle a b c + angle b c a) = - 1
 2. 0 \<le> angle c a b + angle a b c + angle b c a
 3. angle c a b + angle a b c + angle b c a < 3 * pi
[PROOF STEP]
show "cos (angle c a b + angle a b c + angle b c a) = - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cos (angle c a b + angle a b c + angle b c a) = - 1
[PROOF STEP]
proof (cases "a \<noteq> b")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a \<noteq> b \<Longrightarrow> cos (angle c a b + angle a b c + angle b c a) = - 1
 2. \<not> a \<noteq> b \<Longrightarrow> cos (angle c a b + angle a b c + angle b c a) = - 1
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
a \<noteq> b

goal (2 subgoals):
 1. a \<noteq> b \<Longrightarrow> cos (angle c a b + angle a b c + angle b c a) = - 1
 2. \<not> a \<noteq> b \<Longrightarrow> cos (angle c a b + angle a b c + angle b c a) = - 1
[PROOF STEP]
thus "cos (angle c a b + angle a b c + angle b c a) = -1"
[PROOF STATE]
proof (prove)
using this:
a \<noteq> b

goal (1 subgoal):
 1. cos (angle c a b + angle a b c + angle b c a) = - 1
[PROOF STEP]
apply (simp add: cos_add sin_add cosine_law_triangle'' field_simps
                       sine_law_triangle''[of a b c] sine_law_triangle''[of b a c]
                       angle_commute dist_commute gather_squares sin_squared_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<noteq> b \<Longrightarrow> b \<noteq> c \<longrightarrow> a \<noteq> c \<longrightarrow> dist b c * (dist a b ^ 6 * (dist a c ^ 4 * (128 * dist b c ^ 12))) + (dist b c * (32 * ((dist a b)\<^sup>2 * ((dist a c)\<^sup>2 * (dist a b ^ 6 * dist b c ^ 12)))) + (dist b c * (32 * ((dist b c)\<^sup>2 * (dist a c ^ 4 * (dist a b ^ 8 * dist b c ^ 8)))) + (dist b c * (32 * ((dist a b)\<^sup>2 * ((dist a c)\<^sup>2 * ((dist b c)\<^sup>2 * (dist a b ^ 4 * dist b c ^ 12))))) + (dist b c * (32 * ((dist a b)\<^sup>2 * ((dist a c)\<^sup>2 * ((dist b c)\<^sup>2 * (dist a b ^ 4 * (dist a c ^ 4 * dist b c ^ 8)))))) + (dist b c * (32 * ((dist a c)\<^sup>2 * (dist a b ^ 4 * (dist b c ^ 12 * ((dist a c)\<^sup>2 + (dist b c)\<^sup>2 - (dist a b)\<^sup>2)\<^sup>2)))) + (dist b c * (32 * (dist a b ^ 4 * (dist a c ^ 4 * (dist b c ^ 10 * ((dist a c)\<^sup>2 + (dist b c)\<^sup>2 - (dist a b)\<^sup>2)\<^sup>2)))) + dist b c * ((dist a b)\<^sup>2 * ((dist a c)\<^sup>2 * ((dist b c)\<^sup>2 * (64 * (dist a b ^ 4 * (dist b c ^ 8 * ((dist a c)\<^sup>2 + (dist b c)\<^sup>2 - (dist a b)\<^sup>2)\<^sup>2)))))))))))) = dist b c * (32 * ((dist a c)\<^sup>2 * (dist a b ^ 4 * dist b c ^ 16))) + (dist b c * (96 * (dist a b ^ 4 * (dist a c ^ 4 * dist b c ^ 14))) + (dist b c * (96 * (dist a b ^ 4 * (dist a c ^ 6 * dist b c ^ 12))) + (dist b c * (32 * ((dist a b)\<^sup>2 * ((dist a c)\<^sup>2 * (dist a b ^ 8 * dist b c ^ 10)))) + (dist b c * ((dist a b)\<^sup>2 * (64 * (dist a b ^ 4 * (dist a c ^ 4 * dist b c ^ 12)))) + (dist b c * (32 * ((dist a c)\<^sup>2 * ((dist b c)\<^sup>2 * (dist a b ^ 4 * (dist a c ^ 6 * dist b c ^ 8))))) + dist b c * (32 * ((dist a b)\<^sup>2 * ((dist a c)\<^sup>2 * (dist a b ^ 4 * (dist b c ^ 10 * ((dist a c)\<^sup>2 + (dist b c)\<^sup>2 - (dist a b)\<^sup>2)\<^sup>2))))))))))
[PROOF STEP]
apply (simp add: eval_power algebra_simps dist_commute)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
cos (angle c a b + angle a b c + angle b c a) = - 1

goal (1 subgoal):
 1. \<not> a \<noteq> b \<Longrightarrow> cos (angle c a b + angle a b c + angle b c a) = - 1
[PROOF STEP]
qed (insert assms, auto)
[PROOF STATE]
proof (state)
this:
cos (angle c a b + angle a b c + angle b c a) = - 1

goal (2 subgoals):
 1. 0 \<le> angle c a b + angle a b c + angle b c a
 2. angle c a b + angle a b c + angle b c a < 3 * pi
[PROOF STEP]
show "angle c a b + angle a b c + angle b c a < 3 * pi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. angle c a b + angle a b c + angle b c a < 3 * pi
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> angle c a b + angle a b c + angle b c a < 3 * pi \<Longrightarrow> False
[PROOF STEP]
assume "\<not>(angle c a b + angle a b c + angle b c a < 3 * pi)"
[PROOF STATE]
proof (state)
this:
\<not> angle c a b + angle a b c + angle b c a < 3 * pi

goal (1 subgoal):
 1. \<not> angle c a b + angle a b c + angle b c a < 3 * pi \<Longrightarrow> False
[PROOF STEP]
with angle_le_pi[of c a b] angle_le_pi[of a b c] angle_le_pi[of b c a]
[PROOF STATE]
proof (chain)
picking this:
angle c a b \<le> pi
angle a b c \<le> pi
angle b c a \<le> pi
\<not> angle c a b + angle a b c + angle b c a < 3 * pi
[PROOF STEP]
have A: "angle c a b = pi" "angle a b c = pi"
[PROOF STATE]
proof (prove)
using this:
angle c a b \<le> pi
angle a b c \<le> pi
angle b c a \<le> pi
\<not> angle c a b + angle a b c + angle b c a < 3 * pi

goal (1 subgoal):
 1. angle c a b = pi &&& angle a b c = pi
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
angle c a b = pi
angle a b c = pi

goal (1 subgoal):
 1. \<not> angle c a b + angle a b c + angle b c a < 3 * pi \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
angle c a b = pi
angle a b c = pi

goal (1 subgoal):
 1. False
[PROOF STEP]
using angle_eq_pi_imp_dist_additive[of c a b]
                     angle_eq_pi_imp_dist_additive[of a b c]
[PROOF STATE]
proof (prove)
using this:
angle c a b = pi
angle a b c = pi
angle c a b = pi \<Longrightarrow> dist c b = dist c a + dist a b
angle a b c = pi \<Longrightarrow> dist a c = dist a b + dist b c

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
angle c a b + angle a b c + angle b c a < 3 * pi

goal (1 subgoal):
 1. 0 \<le> angle c a b + angle a b c + angle b c a
[PROOF STEP]
qed (auto intro!: add_nonneg_nonneg angle_nonneg)


[STATEMENT]
lemma nsqn_quality_increases_nsqn_eq_le [elim]:
  assumes "i\<in>kD(rt \<xi>)"
      and "quality_increases \<xi> \<xi>'"
      and "s = nsqn (rt \<xi>) i"
    shows "s < nsqn (rt \<xi>') i \<or> (s = nsqn (rt \<xi>') i \<and> the (dhops (rt \<xi>) i) \<ge> the (dhops (rt \<xi>') i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s < nsqn (rt \<xi>') i \<or> s = nsqn (rt \<xi>') i \<and> the (dhops (rt \<xi>') i) \<le> the (dhops (rt \<xi>) i)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i \<in> kD (rt \<xi>)
quality_increases \<xi> \<xi>'
s = nsqn (rt \<xi>) i

goal (1 subgoal):
 1. s < nsqn (rt \<xi>') i \<or> s = nsqn (rt \<xi>') i \<and> the (dhops (rt \<xi>') i) \<le> the (dhops (rt \<xi>) i)
[PROOF STEP]
by (metis nat_less_le nsqn_quality_increases nsqn_quality_increases_dhops)


[STATEMENT]
lemma gcsort_stab_inv:
  assumes
    A: "index_less index key" and
    B: "index_same index key" and
    C: "add_inv n t" and
    D: "n \<le> p"
  shows "\<lbrakk>t' \<in> gcsort_set index key p t; stab_inv f key t\<rbrakk> \<Longrightarrow>
    stab_inv f key t'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t' \<in> gcsort_set index key p t; stab_inv f key t\<rbrakk> \<Longrightarrow> stab_inv f key t'
[PROOF STEP]
by (erule gcsort_set.induct, simp, drule gcsort_add_inv [OF A _ C D],
 rule round_stab_inv [OF A B], simp_all del: bn_inv.simps, erule conjE,
 frule sym, erule subst, rule bn_inv_intro, insert D, simp)


[STATEMENT]
lemma [def_pat_rules]: "Network.cf_set$c \<equiv> UNPROTECT cf_set"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Network.cf_set $ c \<equiv> UNPROTECT cf_set
[PROOF STEP]
by simp