[STATEMENT]
lemma terminatess_impl_not_inf:
 assumes termi: "\<Gamma>\<turnstile>cs,css\<Down>s"
  shows "\<not>inf \<Gamma> cs css s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> AlternativeSmallStep.inf \<Gamma> cs css s
[PROOF STEP]
using termi
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile>cs,css \<Down> s

goal (1 subgoal):
 1. \<not> AlternativeSmallStep.inf \<Gamma> cs css s
[PROOF STEP]
proof (induct)
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>s. \<not> AlternativeSmallStep.inf \<Gamma> [] [] s
 2. \<And>nrms css s abrs. \<lbrakk>\<Gamma>\<turnstile>nrms,css \<Down> Normal s; \<not> AlternativeSmallStep.inf \<Gamma> nrms css (Normal s)\<rbrakk> \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> [] ((nrms, abrs) # css) (Normal s)
 3. \<And>abrs css s nrms. \<lbrakk>\<Gamma>\<turnstile>abrs,css \<Down> Normal s; \<not> AlternativeSmallStep.inf \<Gamma> abrs css (Normal s)\<rbrakk> \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> [] ((nrms, abrs) # css) (Abrupt s)
 4. \<And>nrms css f abrs. \<lbrakk>\<Gamma>\<turnstile>nrms,css \<Down> Fault f; \<not> AlternativeSmallStep.inf \<Gamma> nrms css (Fault f)\<rbrakk> \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> [] ((nrms, abrs) # css) (Fault f)
 5. \<And>nrms css abrs. \<lbrakk>\<Gamma>\<turnstile>nrms,css \<Down> Stuck; \<not> AlternativeSmallStep.inf \<Gamma> nrms css Stuck\<rbrakk> \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> [] ((nrms, abrs) # css) Stuck
 6. \<And>c s cs css. \<lbrakk>\<Gamma>\<turnstile>c \<down> s; \<forall>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> t \<and> \<not> AlternativeSmallStep.inf \<Gamma> cs css t\<rbrakk> \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> (c # cs) css s
[PROOF STEP]
case (Nil s)
[PROOF STATE]
proof (state)
this:

goal (6 subgoals):
 1. \<And>s. \<not> AlternativeSmallStep.inf \<Gamma> [] [] s
 2. \<And>nrms css s abrs. \<lbrakk>\<Gamma>\<turnstile>nrms,css \<Down> Normal s; \<not> AlternativeSmallStep.inf \<Gamma> nrms css (Normal s)\<rbrakk> \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> [] ((nrms, abrs) # css) (Normal s)
 3. \<And>abrs css s nrms. \<lbrakk>\<Gamma>\<turnstile>abrs,css \<Down> Normal s; \<not> AlternativeSmallStep.inf \<Gamma> abrs css (Normal s)\<rbrakk> \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> [] ((nrms, abrs) # css) (Abrupt s)
 4. \<And>nrms css f abrs. \<lbrakk>\<Gamma>\<turnstile>nrms,css \<Down> Fault f; \<not> AlternativeSmallStep.inf \<Gamma> nrms css (Fault f)\<rbrakk> \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> [] ((nrms, abrs) # css) (Fault f)
 5. \<And>nrms css abrs. \<lbrakk>\<Gamma>\<turnstile>nrms,css \<Down> Stuck; \<not> AlternativeSmallStep.inf \<Gamma> nrms css Stuck\<rbrakk> \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> [] ((nrms, abrs) # css) Stuck
 6. \<And>c s cs css. \<lbrakk>\<Gamma>\<turnstile>c \<down> s; \<forall>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> t \<and> \<not> AlternativeSmallStep.inf \<Gamma> cs css t\<rbrakk> \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> (c # cs) css s
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> AlternativeSmallStep.inf \<Gamma> [] [] s
[PROOF STEP]
proof (rule not_infI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. \<lbrakk>f 0 = ([], [], s); \<And>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
fix f
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. \<lbrakk>f 0 = ([], [], s); \<And>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "\<And>i. \<Gamma>\<turnstile>f i \<rightarrow> f (Suc i)"
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> f ?i \<rightarrow> f (Suc ?i)

goal (1 subgoal):
 1. \<And>f. \<lbrakk>f 0 = ([], [], s); \<And>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence "\<Gamma>\<turnstile>f 0 \<rightarrow> f (Suc 0)"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> f ?i \<rightarrow> f (Suc ?i)

goal (1 subgoal):
 1. \<Gamma>\<turnstile> f 0 \<rightarrow> f (Suc 0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> f 0 \<rightarrow> f (Suc 0)

goal (1 subgoal):
 1. \<And>f. \<lbrakk>f 0 = ([], [], s); \<And>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> f 0 \<rightarrow> f (Suc 0)

goal (1 subgoal):
 1. \<And>f. \<lbrakk>f 0 = ([], [], s); \<And>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "f 0 = ([], [], s)"
[PROOF STATE]
proof (state)
this:
f 0 = ([], [], s)

goal (1 subgoal):
 1. \<And>f. \<lbrakk>f 0 = ([], [], s); \<And>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> f 0 \<rightarrow> f (Suc 0)
f 0 = ([], [], s)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> f 0 \<rightarrow> f (Suc 0)
f 0 = ([], [], s)

goal (1 subgoal):
 1. False
[PROOF STEP]
by (fastforce elim: step.cases)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> AlternativeSmallStep.inf \<Gamma> [] [] s

goal (5 subgoals):
 1. \<And>nrms css s abrs. \<lbrakk>\<Gamma>\<turnstile>nrms,css \<Down> Normal s; \<not> AlternativeSmallStep.inf \<Gamma> nrms css (Normal s)\<rbrakk> \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> [] ((nrms, abrs) # css) (Normal s)
 2. \<And>abrs css s nrms. \<lbrakk>\<Gamma>\<turnstile>abrs,css \<Down> Normal s; \<not> AlternativeSmallStep.inf \<Gamma> abrs css (Normal s)\<rbrakk> \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> [] ((nrms, abrs) # css) (Abrupt s)
 3. \<And>nrms css f abrs. \<lbrakk>\<Gamma>\<turnstile>nrms,css \<Down> Fault f; \<not> AlternativeSmallStep.inf \<Gamma> nrms css (Fault f)\<rbrakk> \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> [] ((nrms, abrs) # css) (Fault f)
 4. \<And>nrms css abrs. \<lbrakk>\<Gamma>\<turnstile>nrms,css \<Down> Stuck; \<not> AlternativeSmallStep.inf \<Gamma> nrms css Stuck\<rbrakk> \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> [] ((nrms, abrs) # css) Stuck
 5. \<And>c s cs css. \<lbrakk>\<Gamma>\<turnstile>c \<down> s; \<forall>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> t \<and> \<not> AlternativeSmallStep.inf \<Gamma> cs css t\<rbrakk> \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> (c # cs) css s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>nrms css s abrs. \<lbrakk>\<Gamma>\<turnstile>nrms,css \<Down> Normal s; \<not> AlternativeSmallStep.inf \<Gamma> nrms css (Normal s)\<rbrakk> \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> [] ((nrms, abrs) # css) (Normal s)
 2. \<And>abrs css s nrms. \<lbrakk>\<Gamma>\<turnstile>abrs,css \<Down> Normal s; \<not> AlternativeSmallStep.inf \<Gamma> abrs css (Normal s)\<rbrakk> \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> [] ((nrms, abrs) # css) (Abrupt s)
 3. \<And>nrms css f abrs. \<lbrakk>\<Gamma>\<turnstile>nrms,css \<Down> Fault f; \<not> AlternativeSmallStep.inf \<Gamma> nrms css (Fault f)\<rbrakk> \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> [] ((nrms, abrs) # css) (Fault f)
 4. \<And>nrms css abrs. \<lbrakk>\<Gamma>\<turnstile>nrms,css \<Down> Stuck; \<not> AlternativeSmallStep.inf \<Gamma> nrms css Stuck\<rbrakk> \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> [] ((nrms, abrs) # css) Stuck
 5. \<And>c s cs css. \<lbrakk>\<Gamma>\<turnstile>c \<down> s; \<forall>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> t \<and> \<not> AlternativeSmallStep.inf \<Gamma> cs css t\<rbrakk> \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> (c # cs) css s
[PROOF STEP]
case (ExitBlockNormal nrms css s abrs)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>nrms,css \<Down> Normal s
\<not> AlternativeSmallStep.inf \<Gamma> nrms css (Normal s)

goal (5 subgoals):
 1. \<And>nrms css s abrs. \<lbrakk>\<Gamma>\<turnstile>nrms,css \<Down> Normal s; \<not> AlternativeSmallStep.inf \<Gamma> nrms css (Normal s)\<rbrakk> \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> [] ((nrms, abrs) # css) (Normal s)
 2. \<And>abrs css s nrms. \<lbrakk>\<Gamma>\<turnstile>abrs,css \<Down> Normal s; \<not> AlternativeSmallStep.inf \<Gamma> abrs css (Normal s)\<rbrakk> \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> [] ((nrms, abrs) # css) (Abrupt s)
 3. \<And>nrms css f abrs. \<lbrakk>\<Gamma>\<turnstile>nrms,css \<Down> Fault f; \<not> AlternativeSmallStep.inf \<Gamma> nrms css (Fault f)\<rbrakk> \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> [] ((nrms, abrs) # css) (Fault f)
 4. \<And>nrms css abrs. \<lbrakk>\<Gamma>\<turnstile>nrms,css \<Down> Stuck; \<not> AlternativeSmallStep.inf \<Gamma> nrms css Stuck\<rbrakk> \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> [] ((nrms, abrs) # css) Stuck
 5. \<And>c s cs css. \<lbrakk>\<Gamma>\<turnstile>c \<down> s; \<forall>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> t \<and> \<not> AlternativeSmallStep.inf \<Gamma> cs css t\<rbrakk> \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> (c # cs) css s
[PROOF STEP]
have hyp: "\<not> inf \<Gamma> nrms css (Normal s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> AlternativeSmallStep.inf \<Gamma> nrms css (Normal s)
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
\<not> AlternativeSmallStep.inf \<Gamma> nrms css (Normal s)

goal (5 subgoals):
 1. \<And>nrms css s abrs. \<lbrakk>\<Gamma>\<turnstile>nrms,css \<Down> Normal s; \<not> AlternativeSmallStep.inf \<Gamma> nrms css (Normal s)\<rbrakk> \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> [] ((nrms, abrs) # css) (Normal s)
 2. \<And>abrs css s nrms. \<lbrakk>\<Gamma>\<turnstile>abrs,css \<Down> Normal s; \<not> AlternativeSmallStep.inf \<Gamma> abrs css (Normal s)\<rbrakk> \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> [] ((nrms, abrs) # css) (Abrupt s)
 3. \<And>nrms css f abrs. \<lbrakk>\<Gamma>\<turnstile>nrms,css \<Down> Fault f; \<not> AlternativeSmallStep.inf \<Gamma> nrms css (Fault f)\<rbrakk> \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> [] ((nrms, abrs) # css) (Fault f)
 4. \<And>nrms css abrs. \<lbrakk>\<Gamma>\<turnstile>nrms,css \<Down> Stuck; \<not> AlternativeSmallStep.inf \<Gamma> nrms css Stuck\<rbrakk> \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> [] ((nrms, abrs) # css) Stuck
 5. \<And>c s cs css. \<lbrakk>\<Gamma>\<turnstile>c \<down> s; \<forall>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> t \<and> \<not> AlternativeSmallStep.inf \<Gamma> cs css t\<rbrakk> \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> (c # cs) css s
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> AlternativeSmallStep.inf \<Gamma> [] ((nrms, abrs) # css) (Normal s)
[PROOF STEP]
proof (rule not_infI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. \<lbrakk>f 0 = ([], (nrms, abrs) # css, Normal s); \<And>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
fix f
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. \<lbrakk>f 0 = ([], (nrms, abrs) # css, Normal s); \<And>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume f_step: "\<And>i. \<Gamma>\<turnstile>f i \<rightarrow> f (Suc i)"
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> f ?i \<rightarrow> f (Suc ?i)

goal (1 subgoal):
 1. \<And>f. \<lbrakk>f 0 = ([], (nrms, abrs) # css, Normal s); \<And>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume f0: "f 0 = ([], (nrms, abrs) # css, Normal s)"
[PROOF STATE]
proof (state)
this:
f 0 = ([], (nrms, abrs) # css, Normal s)

goal (1 subgoal):
 1. \<And>f. \<lbrakk>f 0 = ([], (nrms, abrs) # css, Normal s); \<And>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with f_step [of 0]
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> f 0 \<rightarrow> f (Suc 0)
f 0 = ([], (nrms, abrs) # css, Normal s)
[PROOF STEP]
have "f (Suc 0) = (nrms,css,Normal s)"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> f 0 \<rightarrow> f (Suc 0)
f 0 = ([], (nrms, abrs) # css, Normal s)

goal (1 subgoal):
 1. f (Suc 0) = (nrms, css, Normal s)
[PROOF STEP]
by (auto elim: step_Normal_elim_cases)
[PROOF STATE]
proof (state)
this:
f (Suc 0) = (nrms, css, Normal s)

goal (1 subgoal):
 1. \<And>f. \<lbrakk>f 0 = ([], (nrms, abrs) # css, Normal s); \<And>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with f_step
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> f ?i \<rightarrow> f (Suc ?i)
f (Suc 0) = (nrms, css, Normal s)
[PROOF STEP]
have "inf \<Gamma> nrms css (Normal s)"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> f ?i \<rightarrow> f (Suc ?i)
f (Suc 0) = (nrms, css, Normal s)

goal (1 subgoal):
 1. AlternativeSmallStep.inf \<Gamma> nrms css (Normal s)
[PROOF STEP]
apply (simp add: inf_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i); f (Suc 0) = (nrms, css, Normal s)\<rbrakk> \<Longrightarrow> \<exists>f. f 0 = (nrms, css, Normal s) \<and> (\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i))
[PROOF STEP]
apply (rule_tac x="\<lambda>i. f (Suc i)" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i); f (Suc 0) = (nrms, css, Normal s)\<rbrakk> \<Longrightarrow> f (Suc 0) = (nrms, css, Normal s) \<and> (\<forall>i. \<Gamma>\<turnstile> f (Suc i) \<rightarrow> f (Suc (Suc i)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
AlternativeSmallStep.inf \<Gamma> nrms css (Normal s)

goal (1 subgoal):
 1. \<And>f. \<lbrakk>f 0 = ([], (nrms, abrs) # css, Normal s); \<And>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with hyp
[PROOF STATE]
proof (chain)
picking this:
\<not> AlternativeSmallStep.inf \<Gamma> nrms css (Normal s)
AlternativeSmallStep.inf \<Gamma> nrms css (Normal s)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<not> AlternativeSmallStep.inf \<Gamma> nrms css (Normal s)
AlternativeSmallStep.inf \<Gamma> nrms css (Normal s)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> AlternativeSmallStep.inf \<Gamma> [] ((nrms, abrs) # css) (Normal s)

goal (4 subgoals):
 1. \<And>abrs css s nrms. \<lbrakk>\<Gamma>\<turnstile>abrs,css \<Down> Normal s; \<not> AlternativeSmallStep.inf \<Gamma> abrs css (Normal s)\<rbrakk> \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> [] ((nrms, abrs) # css) (Abrupt s)
 2. \<And>nrms css f abrs. \<lbrakk>\<Gamma>\<turnstile>nrms,css \<Down> Fault f; \<not> AlternativeSmallStep.inf \<Gamma> nrms css (Fault f)\<rbrakk> \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> [] ((nrms, abrs) # css) (Fault f)
 3. \<And>nrms css abrs. \<lbrakk>\<Gamma>\<turnstile>nrms,css \<Down> Stuck; \<not> AlternativeSmallStep.inf \<Gamma> nrms css Stuck\<rbrakk> \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> [] ((nrms, abrs) # css) Stuck
 4. \<And>c s cs css. \<lbrakk>\<Gamma>\<turnstile>c \<down> s; \<forall>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> t \<and> \<not> AlternativeSmallStep.inf \<Gamma> cs css t\<rbrakk> \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> (c # cs) css s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>abrs css s nrms. \<lbrakk>\<Gamma>\<turnstile>abrs,css \<Down> Normal s; \<not> AlternativeSmallStep.inf \<Gamma> abrs css (Normal s)\<rbrakk> \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> [] ((nrms, abrs) # css) (Abrupt s)
 2. \<And>nrms css f abrs. \<lbrakk>\<Gamma>\<turnstile>nrms,css \<Down> Fault f; \<not> AlternativeSmallStep.inf \<Gamma> nrms css (Fault f)\<rbrakk> \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> [] ((nrms, abrs) # css) (Fault f)
 3. \<And>nrms css abrs. \<lbrakk>\<Gamma>\<turnstile>nrms,css \<Down> Stuck; \<not> AlternativeSmallStep.inf \<Gamma> nrms css Stuck\<rbrakk> \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> [] ((nrms, abrs) # css) Stuck
 4. \<And>c s cs css. \<lbrakk>\<Gamma>\<turnstile>c \<down> s; \<forall>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> t \<and> \<not> AlternativeSmallStep.inf \<Gamma> cs css t\<rbrakk> \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> (c # cs) css s
[PROOF STEP]
case (ExitBlockAbrupt abrs css s nrms)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>abrs,css \<Down> Normal s
\<not> AlternativeSmallStep.inf \<Gamma> abrs css (Normal s)

goal (4 subgoals):
 1. \<And>abrs css s nrms. \<lbrakk>\<Gamma>\<turnstile>abrs,css \<Down> Normal s; \<not> AlternativeSmallStep.inf \<Gamma> abrs css (Normal s)\<rbrakk> \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> [] ((nrms, abrs) # css) (Abrupt s)
 2. \<And>nrms css f abrs. \<lbrakk>\<Gamma>\<turnstile>nrms,css \<Down> Fault f; \<not> AlternativeSmallStep.inf \<Gamma> nrms css (Fault f)\<rbrakk> \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> [] ((nrms, abrs) # css) (Fault f)
 3. \<And>nrms css abrs. \<lbrakk>\<Gamma>\<turnstile>nrms,css \<Down> Stuck; \<not> AlternativeSmallStep.inf \<Gamma> nrms css Stuck\<rbrakk> \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> [] ((nrms, abrs) # css) Stuck
 4. \<And>c s cs css. \<lbrakk>\<Gamma>\<turnstile>c \<down> s; \<forall>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> t \<and> \<not> AlternativeSmallStep.inf \<Gamma> cs css t\<rbrakk> \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> (c # cs) css s
[PROOF STEP]
have hyp: "\<not> inf \<Gamma> abrs css (Normal s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> AlternativeSmallStep.inf \<Gamma> abrs css (Normal s)
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
\<not> AlternativeSmallStep.inf \<Gamma> abrs css (Normal s)

goal (4 subgoals):
 1. \<And>abrs css s nrms. \<lbrakk>\<Gamma>\<turnstile>abrs,css \<Down> Normal s; \<not> AlternativeSmallStep.inf \<Gamma> abrs css (Normal s)\<rbrakk> \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> [] ((nrms, abrs) # css) (Abrupt s)
 2. \<And>nrms css f abrs. \<lbrakk>\<Gamma>\<turnstile>nrms,css \<Down> Fault f; \<not> AlternativeSmallStep.inf \<Gamma> nrms css (Fault f)\<rbrakk> \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> [] ((nrms, abrs) # css) (Fault f)
 3. \<And>nrms css abrs. \<lbrakk>\<Gamma>\<turnstile>nrms,css \<Down> Stuck; \<not> AlternativeSmallStep.inf \<Gamma> nrms css Stuck\<rbrakk> \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> [] ((nrms, abrs) # css) Stuck
 4. \<And>c s cs css. \<lbrakk>\<Gamma>\<turnstile>c \<down> s; \<forall>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> t \<and> \<not> AlternativeSmallStep.inf \<Gamma> cs css t\<rbrakk> \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> (c # cs) css s
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> AlternativeSmallStep.inf \<Gamma> [] ((nrms, abrs) # css) (Abrupt s)
[PROOF STEP]
proof (rule not_infI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. \<lbrakk>f 0 = ([], (nrms, abrs) # css, Abrupt s); \<And>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
fix f
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. \<lbrakk>f 0 = ([], (nrms, abrs) # css, Abrupt s); \<And>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume f_step: "\<And>i. \<Gamma>\<turnstile>f i \<rightarrow> f (Suc i)"
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> f ?i \<rightarrow> f (Suc ?i)

goal (1 subgoal):
 1. \<And>f. \<lbrakk>f 0 = ([], (nrms, abrs) # css, Abrupt s); \<And>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume f0: "f 0 = ([], (nrms, abrs) # css, Abrupt s)"
[PROOF STATE]
proof (state)
this:
f 0 = ([], (nrms, abrs) # css, Abrupt s)

goal (1 subgoal):
 1. \<And>f. \<lbrakk>f 0 = ([], (nrms, abrs) # css, Abrupt s); \<And>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with f_step [of 0]
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> f 0 \<rightarrow> f (Suc 0)
f 0 = ([], (nrms, abrs) # css, Abrupt s)
[PROOF STEP]
have "f (Suc 0) = (abrs,css,Normal s)"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> f 0 \<rightarrow> f (Suc 0)
f 0 = ([], (nrms, abrs) # css, Abrupt s)

goal (1 subgoal):
 1. f (Suc 0) = (abrs, css, Normal s)
[PROOF STEP]
by (auto elim: step_Normal_elim_cases)
[PROOF STATE]
proof (state)
this:
f (Suc 0) = (abrs, css, Normal s)

goal (1 subgoal):
 1. \<And>f. \<lbrakk>f 0 = ([], (nrms, abrs) # css, Abrupt s); \<And>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with f_step
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> f ?i \<rightarrow> f (Suc ?i)
f (Suc 0) = (abrs, css, Normal s)
[PROOF STEP]
have "inf \<Gamma> abrs css (Normal s)"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> f ?i \<rightarrow> f (Suc ?i)
f (Suc 0) = (abrs, css, Normal s)

goal (1 subgoal):
 1. AlternativeSmallStep.inf \<Gamma> abrs css (Normal s)
[PROOF STEP]
apply (simp add: inf_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i); f (Suc 0) = (abrs, css, Normal s)\<rbrakk> \<Longrightarrow> \<exists>f. f 0 = (abrs, css, Normal s) \<and> (\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i))
[PROOF STEP]
apply (rule_tac x="\<lambda>i. f (Suc i)" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i); f (Suc 0) = (abrs, css, Normal s)\<rbrakk> \<Longrightarrow> f (Suc 0) = (abrs, css, Normal s) \<and> (\<forall>i. \<Gamma>\<turnstile> f (Suc i) \<rightarrow> f (Suc (Suc i)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
AlternativeSmallStep.inf \<Gamma> abrs css (Normal s)

goal (1 subgoal):
 1. \<And>f. \<lbrakk>f 0 = ([], (nrms, abrs) # css, Abrupt s); \<And>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with hyp
[PROOF STATE]
proof (chain)
picking this:
\<not> AlternativeSmallStep.inf \<Gamma> abrs css (Normal s)
AlternativeSmallStep.inf \<Gamma> abrs css (Normal s)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<not> AlternativeSmallStep.inf \<Gamma> abrs css (Normal s)
AlternativeSmallStep.inf \<Gamma> abrs css (Normal s)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> AlternativeSmallStep.inf \<Gamma> [] ((nrms, abrs) # css) (Abrupt s)

goal (3 subgoals):
 1. \<And>nrms css f abrs. \<lbrakk>\<Gamma>\<turnstile>nrms,css \<Down> Fault f; \<not> AlternativeSmallStep.inf \<Gamma> nrms css (Fault f)\<rbrakk> \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> [] ((nrms, abrs) # css) (Fault f)
 2. \<And>nrms css abrs. \<lbrakk>\<Gamma>\<turnstile>nrms,css \<Down> Stuck; \<not> AlternativeSmallStep.inf \<Gamma> nrms css Stuck\<rbrakk> \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> [] ((nrms, abrs) # css) Stuck
 3. \<And>c s cs css. \<lbrakk>\<Gamma>\<turnstile>c \<down> s; \<forall>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> t \<and> \<not> AlternativeSmallStep.inf \<Gamma> cs css t\<rbrakk> \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> (c # cs) css s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>nrms css f abrs. \<lbrakk>\<Gamma>\<turnstile>nrms,css \<Down> Fault f; \<not> AlternativeSmallStep.inf \<Gamma> nrms css (Fault f)\<rbrakk> \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> [] ((nrms, abrs) # css) (Fault f)
 2. \<And>nrms css abrs. \<lbrakk>\<Gamma>\<turnstile>nrms,css \<Down> Stuck; \<not> AlternativeSmallStep.inf \<Gamma> nrms css Stuck\<rbrakk> \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> [] ((nrms, abrs) # css) Stuck
 3. \<And>c s cs css. \<lbrakk>\<Gamma>\<turnstile>c \<down> s; \<forall>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> t \<and> \<not> AlternativeSmallStep.inf \<Gamma> cs css t\<rbrakk> \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> (c # cs) css s
[PROOF STEP]
case (ExitBlockFault nrms css f abrs)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>nrms,css \<Down> Fault f
\<not> AlternativeSmallStep.inf \<Gamma> nrms css (Fault f)

goal (3 subgoals):
 1. \<And>nrms css f abrs. \<lbrakk>\<Gamma>\<turnstile>nrms,css \<Down> Fault f; \<not> AlternativeSmallStep.inf \<Gamma> nrms css (Fault f)\<rbrakk> \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> [] ((nrms, abrs) # css) (Fault f)
 2. \<And>nrms css abrs. \<lbrakk>\<Gamma>\<turnstile>nrms,css \<Down> Stuck; \<not> AlternativeSmallStep.inf \<Gamma> nrms css Stuck\<rbrakk> \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> [] ((nrms, abrs) # css) Stuck
 3. \<And>c s cs css. \<lbrakk>\<Gamma>\<turnstile>c \<down> s; \<forall>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> t \<and> \<not> AlternativeSmallStep.inf \<Gamma> cs css t\<rbrakk> \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> (c # cs) css s
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> AlternativeSmallStep.inf \<Gamma> [] ((nrms, abrs) # css) (Fault f)
[PROOF STEP]
by (rule not_inf_Fault)
[PROOF STATE]
proof (state)
this:
\<not> AlternativeSmallStep.inf \<Gamma> [] ((nrms, abrs) # css) (Fault f)

goal (2 subgoals):
 1. \<And>nrms css abrs. \<lbrakk>\<Gamma>\<turnstile>nrms,css \<Down> Stuck; \<not> AlternativeSmallStep.inf \<Gamma> nrms css Stuck\<rbrakk> \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> [] ((nrms, abrs) # css) Stuck
 2. \<And>c s cs css. \<lbrakk>\<Gamma>\<turnstile>c \<down> s; \<forall>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> t \<and> \<not> AlternativeSmallStep.inf \<Gamma> cs css t\<rbrakk> \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> (c # cs) css s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>nrms css abrs. \<lbrakk>\<Gamma>\<turnstile>nrms,css \<Down> Stuck; \<not> AlternativeSmallStep.inf \<Gamma> nrms css Stuck\<rbrakk> \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> [] ((nrms, abrs) # css) Stuck
 2. \<And>c s cs css. \<lbrakk>\<Gamma>\<turnstile>c \<down> s; \<forall>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> t \<and> \<not> AlternativeSmallStep.inf \<Gamma> cs css t\<rbrakk> \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> (c # cs) css s
[PROOF STEP]
case (ExitBlockStuck nrms css abrs)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>nrms,css \<Down> Stuck
\<not> AlternativeSmallStep.inf \<Gamma> nrms css Stuck

goal (2 subgoals):
 1. \<And>nrms css abrs. \<lbrakk>\<Gamma>\<turnstile>nrms,css \<Down> Stuck; \<not> AlternativeSmallStep.inf \<Gamma> nrms css Stuck\<rbrakk> \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> [] ((nrms, abrs) # css) Stuck
 2. \<And>c s cs css. \<lbrakk>\<Gamma>\<turnstile>c \<down> s; \<forall>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> t \<and> \<not> AlternativeSmallStep.inf \<Gamma> cs css t\<rbrakk> \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> (c # cs) css s
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> AlternativeSmallStep.inf \<Gamma> [] ((nrms, abrs) # css) Stuck
[PROOF STEP]
by (rule not_inf_Stuck)
[PROOF STATE]
proof (state)
this:
\<not> AlternativeSmallStep.inf \<Gamma> [] ((nrms, abrs) # css) Stuck

goal (1 subgoal):
 1. \<And>c s cs css. \<lbrakk>\<Gamma>\<turnstile>c \<down> s; \<forall>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> t \<and> \<not> AlternativeSmallStep.inf \<Gamma> cs css t\<rbrakk> \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> (c # cs) css s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>c s cs css. \<lbrakk>\<Gamma>\<turnstile>c \<down> s; \<forall>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> t \<and> \<not> AlternativeSmallStep.inf \<Gamma> cs css t\<rbrakk> \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> (c # cs) css s
[PROOF STEP]
case (Cons c s cs css)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>c \<down> s
\<forall>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> t \<and> \<not> AlternativeSmallStep.inf \<Gamma> cs css t

goal (1 subgoal):
 1. \<And>c s cs css. \<lbrakk>\<Gamma>\<turnstile>c \<down> s; \<forall>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> t \<and> \<not> AlternativeSmallStep.inf \<Gamma> cs css t\<rbrakk> \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> (c # cs) css s
[PROOF STEP]
have termi_c: "\<Gamma>\<turnstile>c \<down> s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>c \<down> s
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>c \<down> s

goal (1 subgoal):
 1. \<And>c s cs css. \<lbrakk>\<Gamma>\<turnstile>c \<down> s; \<forall>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> t \<and> \<not> AlternativeSmallStep.inf \<Gamma> cs css t\<rbrakk> \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> (c # cs) css s
[PROOF STEP]
have hyp: "\<forall>t. \<Gamma>\<turnstile>\<langle>c,s\<rangle> \<Rightarrow> t \<longrightarrow> \<Gamma>\<turnstile>cs,css\<Down>t \<and> \<not> inf \<Gamma> cs css t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> t \<and> \<not> AlternativeSmallStep.inf \<Gamma> cs css t
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
\<forall>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> t \<and> \<not> AlternativeSmallStep.inf \<Gamma> cs css t

goal (1 subgoal):
 1. \<And>c s cs css. \<lbrakk>\<Gamma>\<turnstile>c \<down> s; \<forall>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> t \<and> \<not> AlternativeSmallStep.inf \<Gamma> cs css t\<rbrakk> \<Longrightarrow> \<not> AlternativeSmallStep.inf \<Gamma> (c # cs) css s
[PROOF STEP]
show "\<not> inf \<Gamma> (c # cs) css s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> AlternativeSmallStep.inf \<Gamma> (c # cs) css s
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. AlternativeSmallStep.inf \<Gamma> (c # cs) css s \<Longrightarrow> False
[PROOF STEP]
assume "inf \<Gamma> (c # cs) css s"
[PROOF STATE]
proof (state)
this:
AlternativeSmallStep.inf \<Gamma> (c # cs) css s

goal (1 subgoal):
 1. AlternativeSmallStep.inf \<Gamma> (c # cs) css s \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
AlternativeSmallStep.inf \<Gamma> (c # cs) css s

goal (1 subgoal):
 1. False
[PROOF STEP]
proof (rule infE)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. AlternativeSmallStep.inf \<Gamma> [c] [] s \<Longrightarrow> False
 2. \<And>t. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t; AlternativeSmallStep.inf \<Gamma> cs css t\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "inf \<Gamma> [c] [] s"
[PROOF STATE]
proof (state)
this:
AlternativeSmallStep.inf \<Gamma> [c] [] s

goal (2 subgoals):
 1. AlternativeSmallStep.inf \<Gamma> [c] [] s \<Longrightarrow> False
 2. \<And>t. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t; AlternativeSmallStep.inf \<Gamma> cs css t\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with terminates_impl_not_inf [OF termi_c]
[PROOF STATE]
proof (chain)
picking this:
\<not> AlternativeSmallStep.inf \<Gamma> [c] [] s
AlternativeSmallStep.inf \<Gamma> [c] [] s
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<not> AlternativeSmallStep.inf \<Gamma> [c] [] s
AlternativeSmallStep.inf \<Gamma> [c] [] s

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

goal (1 subgoal):
 1. \<And>t. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t; AlternativeSmallStep.inf \<Gamma> cs css t\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t; AlternativeSmallStep.inf \<Gamma> cs css t\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
fix t
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t; AlternativeSmallStep.inf \<Gamma> cs css t\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "\<Gamma>\<turnstile>\<langle>c,s\<rangle> \<Rightarrow> t" "inf \<Gamma> cs css t"
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t
AlternativeSmallStep.inf \<Gamma> cs css t

goal (1 subgoal):
 1. \<And>t. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t; AlternativeSmallStep.inf \<Gamma> cs css t\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with hyp
[PROOF STATE]
proof (chain)
picking this:
\<forall>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> t \<and> \<not> AlternativeSmallStep.inf \<Gamma> cs css t
\<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t
AlternativeSmallStep.inf \<Gamma> cs css t
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<forall>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> t \<and> \<not> AlternativeSmallStep.inf \<Gamma> cs css t
\<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t
AlternativeSmallStep.inf \<Gamma> cs css t

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> AlternativeSmallStep.inf \<Gamma> (c # cs) css s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lem:
  "\<forall>y. r\<^sup>+\<^sup>+ a y \<longrightarrow> P a \<longrightarrow> P y
   \<Longrightarrow> ((b,a) \<in> {(y,x). P x \<and> r x y}\<^sup>+) = ((b,a) \<in> {(y,x). P x \<and> r\<^sup>+\<^sup>+ x y})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>y. r\<^sup>+\<^sup>+ a y \<longrightarrow> P a \<longrightarrow> P y \<Longrightarrow> ((b, a) \<in> {(y, x). P x \<and> r x y}\<^sup>+) = ((b, a) \<in> {(y, x). P x \<and> r\<^sup>+\<^sup>+ x y})
[PROOF STEP]
apply(rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>y. r\<^sup>+\<^sup>+ a y \<longrightarrow> P a \<longrightarrow> P y; (b, a) \<in> {(y, x). P x \<and> r x y}\<^sup>+\<rbrakk> \<Longrightarrow> (b, a) \<in> {(y, x). P x \<and> r\<^sup>+\<^sup>+ x y}
 2. \<lbrakk>\<forall>y. r\<^sup>+\<^sup>+ a y \<longrightarrow> P a \<longrightarrow> P y; (b, a) \<in> {(y, x). P x \<and> r\<^sup>+\<^sup>+ x y}\<rbrakk> \<Longrightarrow> (b, a) \<in> {(y, x). P x \<and> r x y}\<^sup>+
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>y. r\<^sup>+\<^sup>+ a y \<longrightarrow> P a \<longrightarrow> P y; (b, a) \<in> {(y, x). P x \<and> r x y}\<^sup>+\<rbrakk> \<Longrightarrow> P a \<and> r\<^sup>+\<^sup>+ a b
 2. \<lbrakk>\<forall>y. r\<^sup>+\<^sup>+ a y \<longrightarrow> P a \<longrightarrow> P y; (b, a) \<in> {(y, x). P x \<and> r\<^sup>+\<^sup>+ x y}\<rbrakk> \<Longrightarrow> (b, a) \<in> {(y, x). P x \<and> r x y}\<^sup>+
[PROOF STEP]
apply(erule trancl_induct)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>y. \<lbrakk>\<forall>y. r\<^sup>+\<^sup>+ a y \<longrightarrow> P a \<longrightarrow> P y; (b, y) \<in> {(y, x). P x \<and> r x y}\<rbrakk> \<Longrightarrow> P y \<and> r\<^sup>+\<^sup>+ y b
 2. \<And>y z. \<lbrakk>\<forall>y. r\<^sup>+\<^sup>+ a y \<longrightarrow> P a \<longrightarrow> P y; (b, y) \<in> {(y, x). P x \<and> r x y}\<^sup>+; (y, z) \<in> {(y, x). P x \<and> r x y}; P y \<and> r\<^sup>+\<^sup>+ y b\<rbrakk> \<Longrightarrow> P z \<and> r\<^sup>+\<^sup>+ z b
 3. \<lbrakk>\<forall>y. r\<^sup>+\<^sup>+ a y \<longrightarrow> P a \<longrightarrow> P y; (b, a) \<in> {(y, x). P x \<and> r\<^sup>+\<^sup>+ x y}\<rbrakk> \<Longrightarrow> (b, a) \<in> {(y, x). P x \<and> r x y}\<^sup>+
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>y z. \<lbrakk>\<forall>y. r\<^sup>+\<^sup>+ a y \<longrightarrow> P a \<longrightarrow> P y; (b, y) \<in> {(y, x). P x \<and> r x y}\<^sup>+; (y, z) \<in> {(y, x). P x \<and> r x y}; P y \<and> r\<^sup>+\<^sup>+ y b\<rbrakk> \<Longrightarrow> P z \<and> r\<^sup>+\<^sup>+ z b
 2. \<lbrakk>\<forall>y. r\<^sup>+\<^sup>+ a y \<longrightarrow> P a \<longrightarrow> P y; (b, a) \<in> {(y, x). P x \<and> r\<^sup>+\<^sup>+ x y}\<rbrakk> \<Longrightarrow> (b, a) \<in> {(y, x). P x \<and> r x y}\<^sup>+
[PROOF STEP]
apply(blast intro:tranclp_trans)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>y. r\<^sup>+\<^sup>+ a y \<longrightarrow> P a \<longrightarrow> P y; (b, a) \<in> {(y, x). P x \<and> r\<^sup>+\<^sup>+ x y}\<rbrakk> \<Longrightarrow> (b, a) \<in> {(y, x). P x \<and> r x y}\<^sup>+
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>y. r\<^sup>+\<^sup>+ a y \<longrightarrow> P a \<longrightarrow> P y; P a; r\<^sup>+\<^sup>+ a b\<rbrakk> \<Longrightarrow> (b, a) \<in> {(y, x). P x \<and> r x y}\<^sup>+
[PROOF STEP]
apply(erule tranclp_induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>\<forall>y. r\<^sup>+\<^sup>+ a y \<longrightarrow> P a \<longrightarrow> P y; P a; r a y\<rbrakk> \<Longrightarrow> (y, a) \<in> {a. case a of (y, x) \<Rightarrow> P x \<and> r x y}\<^sup>+
 2. \<And>y z. \<lbrakk>\<forall>y. r\<^sup>+\<^sup>+ a y \<longrightarrow> P a \<longrightarrow> P y; P a; r\<^sup>+\<^sup>+ a y; r y z; (y, a) \<in> {a. case a of (y, x) \<Rightarrow> P x \<and> r x y}\<^sup>+\<rbrakk> \<Longrightarrow> (z, a) \<in> {a. case a of (y, x) \<Rightarrow> P x \<and> r x y}\<^sup>+
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>\<forall>y. r\<^sup>+\<^sup>+ a y \<longrightarrow> P a \<longrightarrow> P y; P a; r\<^sup>+\<^sup>+ a y; r y z; (y, a) \<in> {a. case a of (y, x) \<Rightarrow> P x \<and> r x y}\<^sup>+\<rbrakk> \<Longrightarrow> (z, a) \<in> {a. case a of (y, x) \<Rightarrow> P x \<and> r x y}\<^sup>+
[PROOF STEP]
apply(blast intro:trancl_trans)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
theorem wf_termi_call_steps: "wf (termi_call_steps \<Gamma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf (termi_call_steps \<Gamma>)
[PROOF STEP]
proof (simp only: termi_call_steps_def wf_iff_no_infinite_down_chain,
       clarify,simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. \<forall>i. (case f (Suc i) of (t, q) \<Rightarrow> \<lambda>(s, p). \<Gamma>\<turnstile>the (\<Gamma> p) \<down> Normal s \<and> (\<exists>css. \<Gamma>\<turnstile> ([the (\<Gamma> p)], [], Normal s) \<rightarrow>\<^sup>+ ([the (\<Gamma> q)], css, Normal t))) (f i) \<Longrightarrow> False
[PROOF STEP]
fix S
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. \<forall>i. (case f (Suc i) of (t, q) \<Rightarrow> \<lambda>(s, p). \<Gamma>\<turnstile>the (\<Gamma> p) \<down> Normal s \<and> (\<exists>css. \<Gamma>\<turnstile> ([the (\<Gamma> p)], [], Normal s) \<rightarrow>\<^sup>+ ([the (\<Gamma> q)], css, Normal t))) (f i) \<Longrightarrow> False
[PROOF STEP]
assume inf:
     "\<forall>i. (\<lambda>(t,q) (s,p). \<Gamma>\<turnstile>(the (\<Gamma> p)) \<down> Normal s \<and>
                 (\<exists>css. \<Gamma>\<turnstile>([the (\<Gamma> p)],[],Normal s) \<rightarrow>\<^sup>+ ([the (\<Gamma> q)],css,Normal t)))
           (S (Suc i)) (S i)"
[PROOF STATE]
proof (state)
this:
\<forall>i. (case S (Suc i) of (t, q) \<Rightarrow> \<lambda>(s, p). \<Gamma>\<turnstile>the (\<Gamma> p) \<down> Normal s \<and> (\<exists>css. \<Gamma>\<turnstile> ([the (\<Gamma> p)], [], Normal s) \<rightarrow>\<^sup>+ ([the (\<Gamma> q)], css, Normal t))) (S i)

goal (1 subgoal):
 1. \<And>f. \<forall>i. (case f (Suc i) of (t, q) \<Rightarrow> \<lambda>(s, p). \<Gamma>\<turnstile>the (\<Gamma> p) \<down> Normal s \<and> (\<exists>css. \<Gamma>\<turnstile> ([the (\<Gamma> p)], [], Normal s) \<rightarrow>\<^sup>+ ([the (\<Gamma> q)], css, Normal t))) (f i) \<Longrightarrow> False
[PROOF STEP]
obtain s p where "s = (\<lambda>i. fst (S i))" and "p = (\<lambda>i. snd (S i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s p. \<lbrakk>s = (\<lambda>i. fst (S i)); p = (\<lambda>i. snd (S i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s = (\<lambda>i. fst (S i))
p = (\<lambda>i. snd (S i))

goal (1 subgoal):
 1. \<And>f. \<forall>i. (case f (Suc i) of (t, q) \<Rightarrow> \<lambda>(s, p). \<Gamma>\<turnstile>the (\<Gamma> p) \<down> Normal s \<and> (\<exists>css. \<Gamma>\<turnstile> ([the (\<Gamma> p)], [], Normal s) \<rightarrow>\<^sup>+ ([the (\<Gamma> q)], css, Normal t))) (f i) \<Longrightarrow> False
[PROOF STEP]
with inf
[PROOF STATE]
proof (chain)
picking this:
\<forall>i. (case S (Suc i) of (t, q) \<Rightarrow> \<lambda>(s, p). \<Gamma>\<turnstile>the (\<Gamma> p) \<down> Normal s \<and> (\<exists>css. \<Gamma>\<turnstile> ([the (\<Gamma> p)], [], Normal s) \<rightarrow>\<^sup>+ ([the (\<Gamma> q)], css, Normal t))) (S i)
s = (\<lambda>i. fst (S i))
p = (\<lambda>i. snd (S i))
[PROOF STEP]
have inf':
     "\<forall>i. \<Gamma>\<turnstile>(the (\<Gamma> (p i))) \<down> Normal (s i) \<and>
                 (\<exists>css. \<Gamma>\<turnstile>([the (\<Gamma> (p i))],[],Normal (s i)) \<rightarrow>\<^sup>+
                           ([the (\<Gamma> (p (Suc i)))],css,Normal (s (Suc i))))"
[PROOF STATE]
proof (prove)
using this:
\<forall>i. (case S (Suc i) of (t, q) \<Rightarrow> \<lambda>(s, p). \<Gamma>\<turnstile>the (\<Gamma> p) \<down> Normal s \<and> (\<exists>css. \<Gamma>\<turnstile> ([the (\<Gamma> p)], [], Normal s) \<rightarrow>\<^sup>+ ([the (\<Gamma> q)], css, Normal t))) (S i)
s = (\<lambda>i. fst (S i))
p = (\<lambda>i. snd (S i))

goal (1 subgoal):
 1. \<forall>i. \<Gamma>\<turnstile>the (\<Gamma> (p i)) \<down> Normal (s i) \<and> (\<exists>css. \<Gamma>\<turnstile> ([the (\<Gamma> (p i))], [], Normal (s i)) \<rightarrow>\<^sup>+ ([the (\<Gamma> (p (Suc i)))], css, Normal (s (Suc i))))
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>i. (case S (Suc i) of (t, q) \<Rightarrow> \<lambda>(s, p). \<Gamma>\<turnstile>the (\<Gamma> p) \<down> Normal s \<and> (\<exists>css. \<Gamma>\<turnstile> ([the (\<Gamma> p)], [], Normal s) \<rightarrow>\<^sup>+ ([the (\<Gamma> q)], css, Normal t))) (S i); s = (\<lambda>i. fst (S i)); p = (\<lambda>i. snd (S i))\<rbrakk> \<Longrightarrow> \<forall>i. \<Gamma>\<turnstile>the (\<Gamma> (p i)) \<down> Normal (s i) \<and> (\<exists>css. \<Gamma>\<turnstile> ([the (\<Gamma> (p i))], [], Normal (s i)) \<rightarrow>\<^sup>+ ([the (\<Gamma> (p (Suc i)))], css, Normal (s (Suc i))))
[PROOF STEP]
apply (rule allI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>\<forall>i. (case S (Suc i) of (t, q) \<Rightarrow> \<lambda>(s, p). \<Gamma>\<turnstile>the (\<Gamma> p) \<down> Normal s \<and> (\<exists>css. \<Gamma>\<turnstile> ([the (\<Gamma> p)], [], Normal s) \<rightarrow>\<^sup>+ ([the (\<Gamma> q)], css, Normal t))) (S i); s = (\<lambda>i. fst (S i)); p = (\<lambda>i. snd (S i))\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>the (\<Gamma> (p i)) \<down> Normal (s i) \<and> (\<exists>css. \<Gamma>\<turnstile> ([the (\<Gamma> (p i))], [], Normal (s i)) \<rightarrow>\<^sup>+ ([the (\<Gamma> (p (Suc i)))], css, Normal (s (Suc i))))
[PROOF STEP]
apply (erule_tac x=i in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>s = (\<lambda>i. fst (S i)); p = (\<lambda>i. snd (S i)); (case S (Suc i) of (t, q) \<Rightarrow> \<lambda>(s, p). \<Gamma>\<turnstile>the (\<Gamma> p) \<down> Normal s \<and> (\<exists>css. \<Gamma>\<turnstile> ([the (\<Gamma> p)], [], Normal s) \<rightarrow>\<^sup>+ ([the (\<Gamma> q)], css, Normal t))) (S i)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>the (\<Gamma> (p i)) \<down> Normal (s i) \<and> (\<exists>css. \<Gamma>\<turnstile> ([the (\<Gamma> (p i))], [], Normal (s i)) \<rightarrow>\<^sup>+ ([the (\<Gamma> (p (Suc i)))], css, Normal (s (Suc i))))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<forall>i. \<Gamma>\<turnstile>the (\<Gamma> (p i)) \<down> Normal (s i) \<and> (\<exists>css. \<Gamma>\<turnstile> ([the (\<Gamma> (p i))], [], Normal (s i)) \<rightarrow>\<^sup>+ ([the (\<Gamma> (p (Suc i)))], css, Normal (s (Suc i))))

goal (1 subgoal):
 1. \<And>f. \<forall>i. (case f (Suc i) of (t, q) \<Rightarrow> \<lambda>(s, p). \<Gamma>\<turnstile>the (\<Gamma> p) \<down> Normal s \<and> (\<exists>css. \<Gamma>\<turnstile> ([the (\<Gamma> p)], [], Normal s) \<rightarrow>\<^sup>+ ([the (\<Gamma> q)], css, Normal t))) (f i) \<Longrightarrow> False
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. False
[PROOF STEP]
from inf' \<comment> \<open>Skolemization of css with axiom of choice\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>i. \<Gamma>\<turnstile>the (\<Gamma> (p i)) \<down> Normal (s i) \<and> (\<exists>css. \<Gamma>\<turnstile> ([the (\<Gamma> (p i))], [], Normal (s i)) \<rightarrow>\<^sup>+ ([the (\<Gamma> (p (Suc i)))], css, Normal (s (Suc i))))
[PROOF STEP]
have "\<exists>css. \<forall>i. \<Gamma>\<turnstile>(the (\<Gamma> (p i))) \<down> Normal (s i) \<and>
                 \<Gamma>\<turnstile>([the (\<Gamma> (p i))],[],Normal (s i)) \<rightarrow>\<^sup>+
                           ([the (\<Gamma> (p (Suc i)))],css i,Normal (s (Suc i)))"
[PROOF STATE]
proof (prove)
using this:
\<forall>i. \<Gamma>\<turnstile>the (\<Gamma> (p i)) \<down> Normal (s i) \<and> (\<exists>css. \<Gamma>\<turnstile> ([the (\<Gamma> (p i))], [], Normal (s i)) \<rightarrow>\<^sup>+ ([the (\<Gamma> (p (Suc i)))], css, Normal (s (Suc i))))

goal (1 subgoal):
 1. \<exists>css. \<forall>i. \<Gamma>\<turnstile>the (\<Gamma> (p i)) \<down> Normal (s i) \<and> \<Gamma>\<turnstile> ([the (\<Gamma> (p i))], [], Normal (s i)) \<rightarrow>\<^sup>+ ([the (\<Gamma> (p (Suc i)))], css i, Normal (s (Suc i)))
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. \<Gamma>\<turnstile>the (\<Gamma> (p i)) \<down> Normal (s i) \<and> (\<exists>css. \<Gamma>\<turnstile> ([the (\<Gamma> (p i))], [], Normal (s i)) \<rightarrow>\<^sup>+ ([the (\<Gamma> (p (Suc i)))], css, Normal (s (Suc i)))) \<Longrightarrow> \<exists>css. \<forall>i. \<Gamma>\<turnstile>the (\<Gamma> (p i)) \<down> Normal (s i) \<and> \<Gamma>\<turnstile> ([the (\<Gamma> (p i))], [], Normal (s i)) \<rightarrow>\<^sup>+ ([the (\<Gamma> (p (Suc i)))], css i, Normal (s (Suc i)))
[PROOF STEP]
apply (rule choice)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. \<Gamma>\<turnstile>the (\<Gamma> (p i)) \<down> Normal (s i) \<and> (\<exists>css. \<Gamma>\<turnstile> ([the (\<Gamma> (p i))], [], Normal (s i)) \<rightarrow>\<^sup>+ ([the (\<Gamma> (p (Suc i)))], css, Normal (s (Suc i)))) \<Longrightarrow> \<forall>i. \<exists>y. \<Gamma>\<turnstile>the (\<Gamma> (p i)) \<down> Normal (s i) \<and> \<Gamma>\<turnstile> ([the (\<Gamma> (p i))], [], Normal (s i)) \<rightarrow>\<^sup>+ ([the (\<Gamma> (p (Suc i)))], y, Normal (s (Suc i)))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>css. \<forall>i. \<Gamma>\<turnstile>the (\<Gamma> (p i)) \<down> Normal (s i) \<and> \<Gamma>\<turnstile> ([the (\<Gamma> (p i))], [], Normal (s i)) \<rightarrow>\<^sup>+ ([the (\<Gamma> (p (Suc i)))], css i, Normal (s (Suc i)))

goal (1 subgoal):
 1. False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>css. \<forall>i. \<Gamma>\<turnstile>the (\<Gamma> (p i)) \<down> Normal (s i) \<and> \<Gamma>\<turnstile> ([the (\<Gamma> (p i))], [], Normal (s i)) \<rightarrow>\<^sup>+ ([the (\<Gamma> (p (Suc i)))], css i, Normal (s (Suc i)))
[PROOF STEP]
obtain css where
      termi_css: "\<forall>i. \<Gamma>\<turnstile>(the (\<Gamma> (p i))) \<down> Normal (s i)" and
      step_css: "\<forall>i. \<Gamma>\<turnstile>([the (\<Gamma> (p i))],[],Normal (s i)) \<rightarrow>\<^sup>+
                         ([the (\<Gamma> (p (Suc i)))],css i,Normal (s (Suc i)))"
[PROOF STATE]
proof (prove)
using this:
\<exists>css. \<forall>i. \<Gamma>\<turnstile>the (\<Gamma> (p i)) \<down> Normal (s i) \<and> \<Gamma>\<turnstile> ([the (\<Gamma> (p i))], [], Normal (s i)) \<rightarrow>\<^sup>+ ([the (\<Gamma> (p (Suc i)))], css i, Normal (s (Suc i)))

goal (1 subgoal):
 1. (\<And>css. \<lbrakk>\<forall>i. \<Gamma>\<turnstile>the (\<Gamma> (p i)) \<down> Normal (s i); \<forall>i. \<Gamma>\<turnstile> ([the (\<Gamma> (p i))], [], Normal (s i)) \<rightarrow>\<^sup>+ ([the (\<Gamma> (p (Suc i)))], css i, Normal (s (Suc i)))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>i. \<Gamma>\<turnstile>the (\<Gamma> (p i)) \<down> Normal (s i)
\<forall>i. \<Gamma>\<turnstile> ([the (\<Gamma> (p i))], [], Normal (s i)) \<rightarrow>\<^sup>+ ([the (\<Gamma> (p (Suc i)))], css i, Normal (s (Suc i)))

goal (1 subgoal):
 1. False
[PROOF STEP]
define f where "f i = ([the (\<Gamma> (p i))], seq css i,Normal (s i)::('a,'c) xstate)" for i
[PROOF STATE]
proof (state)
this:
f ?i = ([the (\<Gamma> (p ?i))], seq css ?i, Normal (s ?i))

goal (1 subgoal):
 1. False
[PROOF STEP]
have "f 0 = ([the (\<Gamma> (p 0))],[],Normal (s 0))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f 0 = ([the (\<Gamma> (p 0))], [], Normal (s 0))
[PROOF STEP]
by (simp add: f_def)
[PROOF STATE]
proof (state)
this:
f 0 = ([the (\<Gamma> (p 0))], [], Normal (s 0))

goal (1 subgoal):
 1. False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f 0 = ([the (\<Gamma> (p 0))], [], Normal (s 0))

goal (1 subgoal):
 1. False
[PROOF STEP]
have "\<forall>i. \<Gamma>\<turnstile> (f i) \<rightarrow>\<^sup>+ (f (i+1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. \<Gamma>\<turnstile> f i \<rightarrow>\<^sup>+ f (i + 1)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. \<Gamma>\<turnstile> f i \<rightarrow>\<^sup>+ f (i + 1)
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. \<Gamma>\<turnstile> f i \<rightarrow>\<^sup>+ f (i + 1)
[PROOF STEP]
from step_css [rule_format, of i]
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> ([the (\<Gamma> (p i))], [], Normal (s i)) \<rightarrow>\<^sup>+ ([the (\<Gamma> (p (Suc i)))], css i, Normal (s (Suc i)))
[PROOF STEP]
have "\<Gamma>\<turnstile>([the (\<Gamma> (p i))], [], Normal (s i)) \<rightarrow>\<^sup>+
              ([the (\<Gamma> (p (Suc i)))], css i, Normal (s (Suc i)))"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> ([the (\<Gamma> (p i))], [], Normal (s i)) \<rightarrow>\<^sup>+ ([the (\<Gamma> (p (Suc i)))], css i, Normal (s (Suc i)))

goal (1 subgoal):
 1. \<Gamma>\<turnstile> ([the (\<Gamma> (p i))], [], Normal (s i)) \<rightarrow>\<^sup>+ ([the (\<Gamma> (p (Suc i)))], css i, Normal (s (Suc i)))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> ([the (\<Gamma> (p i))], [], Normal (s i)) \<rightarrow>\<^sup>+ ([the (\<Gamma> (p (Suc i)))], css i, Normal (s (Suc i)))

goal (1 subgoal):
 1. \<And>i. \<Gamma>\<turnstile> f i \<rightarrow>\<^sup>+ f (i + 1)
[PROOF STEP]
from app_css_steps [OF this,simplified]
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> ([the (\<Gamma> (p i))], ?xs, Normal (s i)) \<rightarrow>\<^sup>+ ([the (\<Gamma> (p (Suc i)))], css i @ ?xs, Normal (s (Suc i)))
[PROOF STEP]
have "\<Gamma>\<turnstile>([the (\<Gamma> (p i))], seq css i, Normal (s i)) \<rightarrow>\<^sup>+
              ([the (\<Gamma> (p (Suc i)))], css i@seq css i, Normal (s (Suc i)))"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> ([the (\<Gamma> (p i))], ?xs, Normal (s i)) \<rightarrow>\<^sup>+ ([the (\<Gamma> (p (Suc i)))], css i @ ?xs, Normal (s (Suc i)))

goal (1 subgoal):
 1. \<Gamma>\<turnstile> ([the (\<Gamma> (p i))], seq css i, Normal (s i)) \<rightarrow>\<^sup>+ ([the (\<Gamma> (p (Suc i)))], css i @ seq css i, Normal (s (Suc i)))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> ([the (\<Gamma> (p i))], seq css i, Normal (s i)) \<rightarrow>\<^sup>+ ([the (\<Gamma> (p (Suc i)))], css i @ seq css i, Normal (s (Suc i)))

goal (1 subgoal):
 1. \<And>i. \<Gamma>\<turnstile> f i \<rightarrow>\<^sup>+ f (i + 1)
[PROOF STEP]
thus "\<Gamma>\<turnstile> (f i) \<rightarrow>\<^sup>+ (f (i+1))"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> ([the (\<Gamma> (p i))], seq css i, Normal (s i)) \<rightarrow>\<^sup>+ ([the (\<Gamma> (p (Suc i)))], css i @ seq css i, Normal (s (Suc i)))

goal (1 subgoal):
 1. \<Gamma>\<turnstile> f i \<rightarrow>\<^sup>+ f (i + 1)
[PROOF STEP]
by (simp add: f_def)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> f i \<rightarrow>\<^sup>+ f (i + 1)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow>\<^sup>+ f (i + 1)

goal (1 subgoal):
 1. False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow>\<^sup>+ f (i + 1)

goal (1 subgoal):
 1. False
[PROOF STEP]
from termi_css [rule_format, of 0]
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile>the (\<Gamma> (p 0)) \<down> Normal (s 0)
[PROOF STEP]
have "\<not> (\<exists>f. (f 0 = ([the (\<Gamma> (p 0))],[],Normal (s 0)) \<and>
                 (\<forall>i. \<Gamma>\<turnstile>(f i) \<rightarrow>\<^sup>+ f(Suc i))))"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile>the (\<Gamma> (p 0)) \<down> Normal (s 0)

goal (1 subgoal):
 1. \<nexists>f. f 0 = ([the (\<Gamma> (p 0))], [], Normal (s 0)) \<and> (\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow>\<^sup>+ f (Suc i))
[PROOF STEP]
by (rule terminates_impl_no_inf_chain)
[PROOF STATE]
proof (state)
this:
\<nexists>f. f 0 = ([the (\<Gamma> (p 0))], [], Normal (s 0)) \<and> (\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow>\<^sup>+ f (Suc i))

goal (1 subgoal):
 1. False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
f 0 = ([the (\<Gamma> (p 0))], [], Normal (s 0))
\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow>\<^sup>+ f (i + 1)
\<nexists>f. f 0 = ([the (\<Gamma> (p 0))], [], Normal (s 0)) \<and> (\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow>\<^sup>+ f (Suc i))
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
f 0 = ([the (\<Gamma> (p 0))], [], Normal (s 0))
\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow>\<^sup>+ f (i + 1)
\<nexists>f. f 0 = ([the (\<Gamma> (p 0))], [], Normal (s 0)) \<and> (\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow>\<^sup>+ f (Suc i))

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem "wf (termi_call_steps \<Gamma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf (termi_call_steps \<Gamma>)
[PROOF STEP]
proof (simp only: termi_call_steps_def wf_iff_no_infinite_down_chain,
       clarify,simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. \<forall>i. (case f (Suc i) of (t, q) \<Rightarrow> \<lambda>(s, p). \<Gamma>\<turnstile>the (\<Gamma> p) \<down> Normal s \<and> (\<exists>css. \<Gamma>\<turnstile> ([the (\<Gamma> p)], [], Normal s) \<rightarrow>\<^sup>+ ([the (\<Gamma> q)], css, Normal t))) (f i) \<Longrightarrow> False
[PROOF STEP]
fix S
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. \<forall>i. (case f (Suc i) of (t, q) \<Rightarrow> \<lambda>(s, p). \<Gamma>\<turnstile>the (\<Gamma> p) \<down> Normal s \<and> (\<exists>css. \<Gamma>\<turnstile> ([the (\<Gamma> p)], [], Normal s) \<rightarrow>\<^sup>+ ([the (\<Gamma> q)], css, Normal t))) (f i) \<Longrightarrow> False
[PROOF STEP]
assume inf:
     "\<forall>i. (\<lambda>(t,q) (s,p). \<Gamma>\<turnstile>(the (\<Gamma> p)) \<down> Normal s \<and>
                 (\<exists>css. \<Gamma>\<turnstile>([the (\<Gamma> p)],[],Normal s) \<rightarrow>\<^sup>+ ([the (\<Gamma> q)],css,Normal t)))
           (S (Suc i)) (S i)"
[PROOF STATE]
proof (state)
this:
\<forall>i. (case S (Suc i) of (t, q) \<Rightarrow> \<lambda>(s, p). \<Gamma>\<turnstile>the (\<Gamma> p) \<down> Normal s \<and> (\<exists>css. \<Gamma>\<turnstile> ([the (\<Gamma> p)], [], Normal s) \<rightarrow>\<^sup>+ ([the (\<Gamma> q)], css, Normal t))) (S i)

goal (1 subgoal):
 1. \<And>f. \<forall>i. (case f (Suc i) of (t, q) \<Rightarrow> \<lambda>(s, p). \<Gamma>\<turnstile>the (\<Gamma> p) \<down> Normal s \<and> (\<exists>css. \<Gamma>\<turnstile> ([the (\<Gamma> p)], [], Normal s) \<rightarrow>\<^sup>+ ([the (\<Gamma> q)], css, Normal t))) (f i) \<Longrightarrow> False
[PROOF STEP]
obtain s p where "s = (\<lambda>i. fst (S i))" and "p = (\<lambda>i. snd (S i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s p. \<lbrakk>s = (\<lambda>i. fst (S i)); p = (\<lambda>i. snd (S i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s = (\<lambda>i. fst (S i))
p = (\<lambda>i. snd (S i))

goal (1 subgoal):
 1. \<And>f. \<forall>i. (case f (Suc i) of (t, q) \<Rightarrow> \<lambda>(s, p). \<Gamma>\<turnstile>the (\<Gamma> p) \<down> Normal s \<and> (\<exists>css. \<Gamma>\<turnstile> ([the (\<Gamma> p)], [], Normal s) \<rightarrow>\<^sup>+ ([the (\<Gamma> q)], css, Normal t))) (f i) \<Longrightarrow> False
[PROOF STEP]
with inf
[PROOF STATE]
proof (chain)
picking this:
\<forall>i. (case S (Suc i) of (t, q) \<Rightarrow> \<lambda>(s, p). \<Gamma>\<turnstile>the (\<Gamma> p) \<down> Normal s \<and> (\<exists>css. \<Gamma>\<turnstile> ([the (\<Gamma> p)], [], Normal s) \<rightarrow>\<^sup>+ ([the (\<Gamma> q)], css, Normal t))) (S i)
s = (\<lambda>i. fst (S i))
p = (\<lambda>i. snd (S i))
[PROOF STEP]
have inf':
     "\<forall>i. \<Gamma>\<turnstile>(the (\<Gamma> (p i))) \<down> Normal (s i) \<and>
                 (\<exists>css. \<Gamma>\<turnstile>([the (\<Gamma> (p i))],[],Normal (s i)) \<rightarrow>\<^sup>+
                           ([the (\<Gamma> (p (Suc i)))],css,Normal (s (Suc i))))"
[PROOF STATE]
proof (prove)
using this:
\<forall>i. (case S (Suc i) of (t, q) \<Rightarrow> \<lambda>(s, p). \<Gamma>\<turnstile>the (\<Gamma> p) \<down> Normal s \<and> (\<exists>css. \<Gamma>\<turnstile> ([the (\<Gamma> p)], [], Normal s) \<rightarrow>\<^sup>+ ([the (\<Gamma> q)], css, Normal t))) (S i)
s = (\<lambda>i. fst (S i))
p = (\<lambda>i. snd (S i))

goal (1 subgoal):
 1. \<forall>i. \<Gamma>\<turnstile>the (\<Gamma> (p i)) \<down> Normal (s i) \<and> (\<exists>css. \<Gamma>\<turnstile> ([the (\<Gamma> (p i))], [], Normal (s i)) \<rightarrow>\<^sup>+ ([the (\<Gamma> (p (Suc i)))], css, Normal (s (Suc i))))
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>i. (case S (Suc i) of (t, q) \<Rightarrow> \<lambda>(s, p). \<Gamma>\<turnstile>the (\<Gamma> p) \<down> Normal s \<and> (\<exists>css. \<Gamma>\<turnstile> ([the (\<Gamma> p)], [], Normal s) \<rightarrow>\<^sup>+ ([the (\<Gamma> q)], css, Normal t))) (S i); s = (\<lambda>i. fst (S i)); p = (\<lambda>i. snd (S i))\<rbrakk> \<Longrightarrow> \<forall>i. \<Gamma>\<turnstile>the (\<Gamma> (p i)) \<down> Normal (s i) \<and> (\<exists>css. \<Gamma>\<turnstile> ([the (\<Gamma> (p i))], [], Normal (s i)) \<rightarrow>\<^sup>+ ([the (\<Gamma> (p (Suc i)))], css, Normal (s (Suc i))))
[PROOF STEP]
apply (rule allI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>\<forall>i. (case S (Suc i) of (t, q) \<Rightarrow> \<lambda>(s, p). \<Gamma>\<turnstile>the (\<Gamma> p) \<down> Normal s \<and> (\<exists>css. \<Gamma>\<turnstile> ([the (\<Gamma> p)], [], Normal s) \<rightarrow>\<^sup>+ ([the (\<Gamma> q)], css, Normal t))) (S i); s = (\<lambda>i. fst (S i)); p = (\<lambda>i. snd (S i))\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>the (\<Gamma> (p i)) \<down> Normal (s i) \<and> (\<exists>css. \<Gamma>\<turnstile> ([the (\<Gamma> (p i))], [], Normal (s i)) \<rightarrow>\<^sup>+ ([the (\<Gamma> (p (Suc i)))], css, Normal (s (Suc i))))
[PROOF STEP]
apply (erule_tac x=i in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>s = (\<lambda>i. fst (S i)); p = (\<lambda>i. snd (S i)); (case S (Suc i) of (t, q) \<Rightarrow> \<lambda>(s, p). \<Gamma>\<turnstile>the (\<Gamma> p) \<down> Normal s \<and> (\<exists>css. \<Gamma>\<turnstile> ([the (\<Gamma> p)], [], Normal s) \<rightarrow>\<^sup>+ ([the (\<Gamma> q)], css, Normal t))) (S i)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>the (\<Gamma> (p i)) \<down> Normal (s i) \<and> (\<exists>css. \<Gamma>\<turnstile> ([the (\<Gamma> (p i))], [], Normal (s i)) \<rightarrow>\<^sup>+ ([the (\<Gamma> (p (Suc i)))], css, Normal (s (Suc i))))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<forall>i. \<Gamma>\<turnstile>the (\<Gamma> (p i)) \<down> Normal (s i) \<and> (\<exists>css. \<Gamma>\<turnstile> ([the (\<Gamma> (p i))], [], Normal (s i)) \<rightarrow>\<^sup>+ ([the (\<Gamma> (p (Suc i)))], css, Normal (s (Suc i))))

goal (1 subgoal):
 1. \<And>f. \<forall>i. (case f (Suc i) of (t, q) \<Rightarrow> \<lambda>(s, p). \<Gamma>\<turnstile>the (\<Gamma> p) \<down> Normal s \<and> (\<exists>css. \<Gamma>\<turnstile> ([the (\<Gamma> p)], [], Normal s) \<rightarrow>\<^sup>+ ([the (\<Gamma> q)], css, Normal t))) (f i) \<Longrightarrow> False
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. False
[PROOF STEP]
define CSS where "CSS i = (SOME css.
                      \<Gamma>\<turnstile>([the (\<Gamma> (p i))],[], Normal (s i)) \<rightarrow>\<^sup>+
                      ([the (\<Gamma> (p (i+1)))],css,Normal (s (i+1))))" for i
[PROOF STATE]
proof (state)
this:
CSS ?i = (SOME css. \<Gamma>\<turnstile> ([the (\<Gamma> (p ?i))], [], Normal (s ?i)) \<rightarrow>\<^sup>+ ([the (\<Gamma> (p (?i + 1)))], css, Normal (s (?i + 1))))

goal (1 subgoal):
 1. False
[PROOF STEP]
define f where "f i = ([the (\<Gamma> (p i))], seq CSS i,Normal (s i)::('a,'c) xstate)" for i
[PROOF STATE]
proof (state)
this:
f ?i = ([the (\<Gamma> (p ?i))], seq CSS ?i, Normal (s ?i))

goal (1 subgoal):
 1. False
[PROOF STEP]
have "f 0 = ([the (\<Gamma> (p 0))],[],Normal (s 0))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f 0 = ([the (\<Gamma> (p 0))], [], Normal (s 0))
[PROOF STEP]
by (simp add: f_def)
[PROOF STATE]
proof (state)
this:
f 0 = ([the (\<Gamma> (p 0))], [], Normal (s 0))

goal (1 subgoal):
 1. False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f 0 = ([the (\<Gamma> (p 0))], [], Normal (s 0))

goal (1 subgoal):
 1. False
[PROOF STEP]
have "\<forall>i. \<Gamma>\<turnstile> (f i) \<rightarrow>\<^sup>+ (f (i+1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. \<Gamma>\<turnstile> f i \<rightarrow>\<^sup>+ f (i + 1)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. \<Gamma>\<turnstile> f i \<rightarrow>\<^sup>+ f (i + 1)
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. \<Gamma>\<turnstile> f i \<rightarrow>\<^sup>+ f (i + 1)
[PROOF STEP]
from inf' [rule_format, of i]
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile>the (\<Gamma> (p i)) \<down> Normal (s i) \<and> (\<exists>css. \<Gamma>\<turnstile> ([the (\<Gamma> (p i))], [], Normal (s i)) \<rightarrow>\<^sup>+ ([the (\<Gamma> (p (Suc i)))], css, Normal (s (Suc i))))
[PROOF STEP]
obtain css where
         css: "\<Gamma>\<turnstile>([the (\<Gamma> (p i))],[],Normal (s i)) \<rightarrow>\<^sup>+
                ([the (\<Gamma> (p (i+1)))],css,Normal (s (i+1)))"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile>the (\<Gamma> (p i)) \<down> Normal (s i) \<and> (\<exists>css. \<Gamma>\<turnstile> ([the (\<Gamma> (p i))], [], Normal (s i)) \<rightarrow>\<^sup>+ ([the (\<Gamma> (p (Suc i)))], css, Normal (s (Suc i))))

goal (1 subgoal):
 1. (\<And>css. \<Gamma>\<turnstile> ([the (\<Gamma> (p i))], [], Normal (s i)) \<rightarrow>\<^sup>+ ([the (\<Gamma> (p (i + 1)))], css, Normal (s (i + 1))) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> ([the (\<Gamma> (p i))], [], Normal (s i)) \<rightarrow>\<^sup>+ ([the (\<Gamma> (p (i + 1)))], css, Normal (s (i + 1)))

goal (1 subgoal):
 1. \<And>i. \<Gamma>\<turnstile> f i \<rightarrow>\<^sup>+ f (i + 1)
[PROOF STEP]
hence "\<Gamma>\<turnstile>([the (\<Gamma> (p i))], seq CSS i, Normal (s i)) \<rightarrow>\<^sup>+
                  ([the (\<Gamma> (p (i+1)))], CSS i @ seq CSS i, Normal (s (i+1)))"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> ([the (\<Gamma> (p i))], [], Normal (s i)) \<rightarrow>\<^sup>+ ([the (\<Gamma> (p (i + 1)))], css, Normal (s (i + 1)))

goal (1 subgoal):
 1. \<Gamma>\<turnstile> ([the (\<Gamma> (p i))], seq CSS i, Normal (s i)) \<rightarrow>\<^sup>+ ([the (\<Gamma> (p (i + 1)))], CSS i @ seq CSS i, Normal (s (i + 1)))
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> ([the (\<Gamma> (p i))], [], Normal (s i)) \<rightarrow>\<^sup>+ ([the (\<Gamma> (p (i + 1)))], css, Normal (s (i + 1))) \<Longrightarrow> \<Gamma>\<turnstile> ([the (\<Gamma> (p i))], seq CSS i, Normal (s i)) \<rightarrow>\<^sup>+ ([the (\<Gamma> (p (i + 1)))], CSS i @ seq CSS i, Normal (s (i + 1)))
[PROOF STEP]
apply (unfold CSS_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> ([the (\<Gamma> (p i))], [], Normal (s i)) \<rightarrow>\<^sup>+ ([the (\<Gamma> (p (i + 1)))], css, Normal (s (i + 1))) \<Longrightarrow> \<Gamma>\<turnstile> ([the (\<Gamma> (p i))], seq (\<lambda>i. SOME css. \<Gamma>\<turnstile> ([the (\<Gamma> (p i))], [], Normal (s i)) \<rightarrow>\<^sup>+ ([the (\<Gamma> (p (i + 1)))], css, Normal (s (i + 1)))) i, Normal (s i)) \<rightarrow>\<^sup>+ ([the (\<Gamma> (p (i + 1)))], (SOME css. \<Gamma>\<turnstile> ([the (\<Gamma> (p i))], [], Normal (s i)) \<rightarrow>\<^sup>+ ([the (\<Gamma> (p (i + 1)))], css, Normal (s (i + 1)))) @ seq (\<lambda>i. SOME css. \<Gamma>\<turnstile> ([the (\<Gamma> (p i))], [], Normal (s i)) \<rightarrow>\<^sup>+ ([the (\<Gamma> (p (i + 1)))], css, Normal (s (i + 1)))) i, Normal (s (i + 1)))
[PROOF STEP]
apply (rule someI2
              [where P="\<lambda>css.
                    \<Gamma>\<turnstile>([the (\<Gamma> (p i))],[],Normal (s i))\<rightarrow>\<^sup>+
                         ([the (\<Gamma> (p (i+1)))],css, Normal (s (i+1)))"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<Gamma>\<turnstile> ([the (\<Gamma> (p i))], [], Normal (s i)) \<rightarrow>\<^sup>+ ([the (\<Gamma> (p (i + 1)))], css, Normal (s (i + 1))) \<Longrightarrow> \<Gamma>\<turnstile> ([the (\<Gamma> (p i))], [], Normal (s i)) \<rightarrow>\<^sup>+ ([the (\<Gamma> (p (i + 1)))], ?a1, Normal (s (i + 1)))
 2. \<And>x. \<lbrakk>\<Gamma>\<turnstile> ([the (\<Gamma> (p i))], [], Normal (s i)) \<rightarrow>\<^sup>+ ([the (\<Gamma> (p (i + 1)))], css, Normal (s (i + 1))); \<Gamma>\<turnstile> ([the (\<Gamma> (p i))], [], Normal (s i)) \<rightarrow>\<^sup>+ ([the (\<Gamma> (p (i + 1)))], x, Normal (s (i + 1)))\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> ([the (\<Gamma> (p i))], seq (\<lambda>i. SOME css. \<Gamma>\<turnstile> ([the (\<Gamma> (p i))], [], Normal (s i)) \<rightarrow>\<^sup>+ ([the (\<Gamma> (p (i + 1)))], css, Normal (s (i + 1)))) i, Normal (s i)) \<rightarrow>\<^sup>+ ([the (\<Gamma> (p (i + 1)))], x @ seq (\<lambda>i. SOME css. \<Gamma>\<turnstile> ([the (\<Gamma> (p i))], [], Normal (s i)) \<rightarrow>\<^sup>+ ([the (\<Gamma> (p (i + 1)))], css, Normal (s (i + 1)))) i, Normal (s (i + 1)))
[PROOF STEP]
apply (rule css)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<Gamma>\<turnstile> ([the (\<Gamma> (p i))], [], Normal (s i)) \<rightarrow>\<^sup>+ ([the (\<Gamma> (p (i + 1)))], css, Normal (s (i + 1))); \<Gamma>\<turnstile> ([the (\<Gamma> (p i))], [], Normal (s i)) \<rightarrow>\<^sup>+ ([the (\<Gamma> (p (i + 1)))], x, Normal (s (i + 1)))\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> ([the (\<Gamma> (p i))], seq (\<lambda>i. SOME css. \<Gamma>\<turnstile> ([the (\<Gamma> (p i))], [], Normal (s i)) \<rightarrow>\<^sup>+ ([the (\<Gamma> (p (i + 1)))], css, Normal (s (i + 1)))) i, Normal (s i)) \<rightarrow>\<^sup>+ ([the (\<Gamma> (p (i + 1)))], x @ seq (\<lambda>i. SOME css. \<Gamma>\<turnstile> ([the (\<Gamma> (p i))], [], Normal (s i)) \<rightarrow>\<^sup>+ ([the (\<Gamma> (p (i + 1)))], css, Normal (s (i + 1)))) i, Normal (s (i + 1)))
[PROOF STEP]
apply (fastforce dest: app_css_steps)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> ([the (\<Gamma> (p i))], seq CSS i, Normal (s i)) \<rightarrow>\<^sup>+ ([the (\<Gamma> (p (i + 1)))], CSS i @ seq CSS i, Normal (s (i + 1)))

goal (1 subgoal):
 1. \<And>i. \<Gamma>\<turnstile> f i \<rightarrow>\<^sup>+ f (i + 1)
[PROOF STEP]
thus "\<Gamma>\<turnstile> (f i) \<rightarrow>\<^sup>+ (f (i+1))"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> ([the (\<Gamma> (p i))], seq CSS i, Normal (s i)) \<rightarrow>\<^sup>+ ([the (\<Gamma> (p (i + 1)))], CSS i @ seq CSS i, Normal (s (i + 1)))

goal (1 subgoal):
 1. \<Gamma>\<turnstile> f i \<rightarrow>\<^sup>+ f (i + 1)
[PROOF STEP]
by (simp add: f_def)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> f i \<rightarrow>\<^sup>+ f (i + 1)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow>\<^sup>+ f (i + 1)

goal (1 subgoal):
 1. False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow>\<^sup>+ f (i + 1)

goal (1 subgoal):
 1. False
[PROOF STEP]
from inf' [rule_format, of 0]
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile>the (\<Gamma> (p 0)) \<down> Normal (s 0) \<and> (\<exists>css. \<Gamma>\<turnstile> ([the (\<Gamma> (p 0))], [], Normal (s 0)) \<rightarrow>\<^sup>+ ([the (\<Gamma> (p (Suc 0)))], css, Normal (s (Suc 0))))
[PROOF STEP]
have "\<Gamma>\<turnstile>the (\<Gamma> (p 0)) \<down> Normal (s 0)"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile>the (\<Gamma> (p 0)) \<down> Normal (s 0) \<and> (\<exists>css. \<Gamma>\<turnstile> ([the (\<Gamma> (p 0))], [], Normal (s 0)) \<rightarrow>\<^sup>+ ([the (\<Gamma> (p (Suc 0)))], css, Normal (s (Suc 0))))

goal (1 subgoal):
 1. \<Gamma>\<turnstile>the (\<Gamma> (p 0)) \<down> Normal (s 0)
[PROOF STEP]
by iprover
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>the (\<Gamma> (p 0)) \<down> Normal (s 0)

goal (1 subgoal):
 1. False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile>the (\<Gamma> (p 0)) \<down> Normal (s 0)
[PROOF STEP]
have "\<not> (\<exists>f. (f 0 = ([the (\<Gamma> (p 0))],[],Normal (s 0)) \<and>
                 (\<forall>i. \<Gamma>\<turnstile>(f i) \<rightarrow>\<^sup>+ f(Suc i))))"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile>the (\<Gamma> (p 0)) \<down> Normal (s 0)

goal (1 subgoal):
 1. \<nexists>f. f 0 = ([the (\<Gamma> (p 0))], [], Normal (s 0)) \<and> (\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow>\<^sup>+ f (Suc i))
[PROOF STEP]
by (rule terminates_impl_no_inf_chain)
[PROOF STATE]
proof (state)
this:
\<nexists>f. f 0 = ([the (\<Gamma> (p 0))], [], Normal (s 0)) \<and> (\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow>\<^sup>+ f (Suc i))

goal (1 subgoal):
 1. False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
f 0 = ([the (\<Gamma> (p 0))], [], Normal (s 0))
\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow>\<^sup>+ f (i + 1)
\<nexists>f. f 0 = ([the (\<Gamma> (p 0))], [], Normal (s 0)) \<and> (\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow>\<^sup>+ f (Suc i))
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
f 0 = ([the (\<Gamma> (p 0))], [], Normal (s 0))
\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow>\<^sup>+ f (i + 1)
\<nexists>f. f 0 = ([the (\<Gamma> (p 0))], [], Normal (s 0)) \<and> (\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow>\<^sup>+ f (Suc i))

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma not_inf_implies_wf: assumes not_inf: "\<not> inf \<Gamma> cs css s"
  shows "wf {(c2,c1). \<Gamma> \<turnstile> (cs,css,s) \<rightarrow>\<^sup>* c1 \<and> \<Gamma> \<turnstile> c1 \<rightarrow> c2}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf {(c2, c1). \<Gamma>\<turnstile> (cs, css, s) \<rightarrow>\<^sup>* c1 \<and> \<Gamma>\<turnstile> c1 \<rightarrow> c2}
[PROOF STEP]
proof (simp only: wf_iff_no_infinite_down_chain,clarify, simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. \<forall>i. \<Gamma>\<turnstile> (cs, css, s) \<rightarrow>\<^sup>* f i \<and> \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i) \<Longrightarrow> False
[PROOF STEP]
fix f
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. \<forall>i. \<Gamma>\<turnstile> (cs, css, s) \<rightarrow>\<^sup>* f i \<and> \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i) \<Longrightarrow> False
[PROOF STEP]
assume "\<forall>i. \<Gamma>\<turnstile>(cs, css, s) \<rightarrow>\<^sup>* f i \<and> \<Gamma>\<turnstile>f i \<rightarrow> f (Suc i)"
[PROOF STATE]
proof (state)
this:
\<forall>i. \<Gamma>\<turnstile> (cs, css, s) \<rightarrow>\<^sup>* f i \<and> \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)

goal (1 subgoal):
 1. \<And>f. \<forall>i. \<Gamma>\<turnstile> (cs, css, s) \<rightarrow>\<^sup>* f i \<and> \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i) \<Longrightarrow> False
[PROOF STEP]
hence "\<exists>f. f 0 = (cs, css, s) \<and> (\<forall>i. \<Gamma>\<turnstile>f i \<rightarrow> f (Suc i))"
[PROOF STATE]
proof (prove)
using this:
\<forall>i. \<Gamma>\<turnstile> (cs, css, s) \<rightarrow>\<^sup>* f i \<and> \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)

goal (1 subgoal):
 1. \<exists>f. f 0 = (cs, css, s) \<and> (\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i))
[PROOF STEP]
by (rule renumber [to_pred])
[PROOF STATE]
proof (state)
this:
\<exists>f. f 0 = (cs, css, s) \<and> (\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i))

goal (1 subgoal):
 1. \<And>f. \<forall>i. \<Gamma>\<turnstile> (cs, css, s) \<rightarrow>\<^sup>* f i \<and> \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i) \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<exists>f. f 0 = (cs, css, s) \<and> (\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i))

goal (1 subgoal):
 1. \<And>f. \<forall>i. \<Gamma>\<turnstile> (cs, css, s) \<rightarrow>\<^sup>* f i \<and> \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i) \<Longrightarrow> False
[PROOF STEP]
from not_inf
[PROOF STATE]
proof (chain)
picking this:
\<not> AlternativeSmallStep.inf \<Gamma> cs css s
[PROOF STEP]
have "\<not> (\<exists>f. f 0 = (cs, css, s) \<and> (\<forall>i. \<Gamma>\<turnstile>f i \<rightarrow> f (Suc i)))"
[PROOF STATE]
proof (prove)
using this:
\<not> AlternativeSmallStep.inf \<Gamma> cs css s

goal (1 subgoal):
 1. \<nexists>f. f 0 = (cs, css, s) \<and> (\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i))
[PROOF STEP]
by (unfold inf_def)
[PROOF STATE]
proof (state)
this:
\<nexists>f. f 0 = (cs, css, s) \<and> (\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i))

goal (1 subgoal):
 1. \<And>f. \<forall>i. \<Gamma>\<turnstile> (cs, css, s) \<rightarrow>\<^sup>* f i \<and> \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i) \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<exists>f. f 0 = (cs, css, s) \<and> (\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i))
\<nexists>f. f 0 = (cs, css, s) \<and> (\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i))
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<exists>f. f 0 = (cs, css, s) \<and> (\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i))
\<nexists>f. f 0 = (cs, css, s) \<and> (\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i))

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

goal:
No subgoals!
[PROOF STEP]
qed