[STATEMENT]
lemma steps_preserves_terminations:
  assumes steps: "\<Gamma>\<turnstile>(cs,css,s) \<rightarrow>\<^sup>* (cs',css',t)"
  shows "\<Gamma>\<turnstile>cs,css\<Down>s \<Longrightarrow> \<Gamma>\<turnstile>cs',css'\<Down>t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>cs,css \<Down> s \<Longrightarrow> \<Gamma>\<turnstile>cs',css' \<Down> t
[PROOF STEP]
using steps
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> (cs, css, s) \<rightarrow>\<^sup>* (cs', css', t)

goal (1 subgoal):
 1. \<Gamma>\<turnstile>cs,css \<Down> s \<Longrightarrow> \<Gamma>\<turnstile>cs',css' \<Down> t
[PROOF STEP]
proof (induct rule: rtrancl_induct3 [consumes 1])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<Gamma>\<turnstile>cs,css \<Down> s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> s
 2. \<And>a aa b ab ac ba. \<lbrakk>\<Gamma>\<turnstile> (cs, css, s) \<rightarrow>\<^sup>* (a, aa, b); \<Gamma>\<turnstile> (a, aa, b) \<rightarrow> (ab, ac, ba); \<Gamma>\<turnstile>cs,css \<Down> s \<Longrightarrow> \<Gamma>\<turnstile>a,aa \<Down> b; \<Gamma>\<turnstile>cs,css \<Down> s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>ab,ac \<Down> ba
[PROOF STEP]
assume  "\<Gamma>\<turnstile>cs,css\<Down>s"
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>cs,css \<Down> s

goal (2 subgoals):
 1. \<Gamma>\<turnstile>cs,css \<Down> s \<Longrightarrow> \<Gamma>\<turnstile>cs,css \<Down> s
 2. \<And>a aa b ab ac ba. \<lbrakk>\<Gamma>\<turnstile> (cs, css, s) \<rightarrow>\<^sup>* (a, aa, b); \<Gamma>\<turnstile> (a, aa, b) \<rightarrow> (ab, ac, ba); \<Gamma>\<turnstile>cs,css \<Down> s \<Longrightarrow> \<Gamma>\<turnstile>a,aa \<Down> b; \<Gamma>\<turnstile>cs,css \<Down> s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>ab,ac \<Down> ba
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile>cs,css \<Down> s
[PROOF STEP]
show "\<Gamma>\<turnstile>cs,css\<Down>s"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile>cs,css \<Down> s

goal (1 subgoal):
 1. \<Gamma>\<turnstile>cs,css \<Down> s
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>cs,css \<Down> s

goal (1 subgoal):
 1. \<And>a aa b ab ac ba. \<lbrakk>\<Gamma>\<turnstile> (cs, css, s) \<rightarrow>\<^sup>* (a, aa, b); \<Gamma>\<turnstile> (a, aa, b) \<rightarrow> (ab, ac, ba); \<Gamma>\<turnstile>cs,css \<Down> s \<Longrightarrow> \<Gamma>\<turnstile>a,aa \<Down> b; \<Gamma>\<turnstile>cs,css \<Down> s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>ab,ac \<Down> ba
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a aa b ab ac ba. \<lbrakk>\<Gamma>\<turnstile> (cs, css, s) \<rightarrow>\<^sup>* (a, aa, b); \<Gamma>\<turnstile> (a, aa, b) \<rightarrow> (ab, ac, ba); \<Gamma>\<turnstile>cs,css \<Down> s \<Longrightarrow> \<Gamma>\<turnstile>a,aa \<Down> b; \<Gamma>\<turnstile>cs,css \<Down> s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>ab,ac \<Down> ba
[PROOF STEP]
fix cs'' css'' w cs' css' t
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a aa b ab ac ba. \<lbrakk>\<Gamma>\<turnstile> (cs, css, s) \<rightarrow>\<^sup>* (a, aa, b); \<Gamma>\<turnstile> (a, aa, b) \<rightarrow> (ab, ac, ba); \<Gamma>\<turnstile>cs,css \<Down> s \<Longrightarrow> \<Gamma>\<turnstile>a,aa \<Down> b; \<Gamma>\<turnstile>cs,css \<Down> s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>ab,ac \<Down> ba
[PROOF STEP]
assume "\<Gamma>\<turnstile>(cs'',css'', w) \<rightarrow> (cs',css', t)" "\<Gamma>\<turnstile>cs,css\<Down>s \<Longrightarrow> \<Gamma>\<turnstile>cs'',css''\<Down>w"
         "\<Gamma>\<turnstile>cs,css\<Down>s"
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (cs'', css'', w) \<rightarrow> (cs', css', t)
\<Gamma>\<turnstile>cs,css \<Down> s \<Longrightarrow> \<Gamma>\<turnstile>cs'',css'' \<Down> w
\<Gamma>\<turnstile>cs,css \<Down> s

goal (1 subgoal):
 1. \<And>a aa b ab ac ba. \<lbrakk>\<Gamma>\<turnstile> (cs, css, s) \<rightarrow>\<^sup>* (a, aa, b); \<Gamma>\<turnstile> (a, aa, b) \<rightarrow> (ab, ac, ba); \<Gamma>\<turnstile>cs,css \<Down> s \<Longrightarrow> \<Gamma>\<turnstile>a,aa \<Down> b; \<Gamma>\<turnstile>cs,css \<Down> s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>ab,ac \<Down> ba
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> (cs'', css'', w) \<rightarrow> (cs', css', t)
\<Gamma>\<turnstile>cs,css \<Down> s \<Longrightarrow> \<Gamma>\<turnstile>cs'',css'' \<Down> w
\<Gamma>\<turnstile>cs,css \<Down> s
[PROOF STEP]
show "\<Gamma>\<turnstile>cs',css'\<Down>t"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> (cs'', css'', w) \<rightarrow> (cs', css', t)
\<Gamma>\<turnstile>cs,css \<Down> s \<Longrightarrow> \<Gamma>\<turnstile>cs'',css'' \<Down> w
\<Gamma>\<turnstile>cs,css \<Down> s

goal (1 subgoal):
 1. \<Gamma>\<turnstile>cs',css' \<Down> t
[PROOF STEP]
by (blast dest: step_preserves_terminations)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>cs',css' \<Down> t

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem steps_preserves_termination:
  assumes steps: "\<Gamma>\<turnstile>([c],[],s) \<rightarrow>\<^sup>* (c'#cs',css',t)"
  assumes term_c: "\<Gamma>\<turnstile>c\<down>s"
  shows "\<Gamma>\<turnstile>c'\<down>t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>c' \<down> t
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>c' \<down> t
[PROOF STEP]
from term_c
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile>c \<down> s
[PROOF STEP]
have "\<Gamma>\<turnstile>[c],[]\<Down>s"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile>c \<down> s

goal (1 subgoal):
 1. \<Gamma>\<turnstile>[c],[] \<Down> s
[PROOF STEP]
by (auto intro: terminatess.intros)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>[c],[] \<Down> s

goal (1 subgoal):
 1. \<Gamma>\<turnstile>c' \<down> t
[PROOF STEP]
from steps this
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> ([c], [], s) \<rightarrow>\<^sup>* (c' # cs', css', t)
\<Gamma>\<turnstile>[c],[] \<Down> s
[PROOF STEP]
have "\<Gamma>\<turnstile>c'#cs',css'\<Down>t"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> ([c], [], s) \<rightarrow>\<^sup>* (c' # cs', css', t)
\<Gamma>\<turnstile>[c],[] \<Down> s

goal (1 subgoal):
 1. \<Gamma>\<turnstile>c' # cs',css' \<Down> t
[PROOF STEP]
by (rule steps_preserves_terminations)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>c' # cs',css' \<Down> t

goal (1 subgoal):
 1. \<Gamma>\<turnstile>c' \<down> t
[PROOF STEP]
thus "\<Gamma>\<turnstile>c'\<down>t"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile>c' # cs',css' \<Down> t

goal (1 subgoal):
 1. \<Gamma>\<turnstile>c' \<down> t
[PROOF STEP]
by (auto elim: terminatess_elim_cases)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile>c' \<down> t

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma renumber':
  assumes f: "\<forall>i. (a,f i) \<in> r\<^sup>* \<and> (f i,f(Suc i)) \<in> r"
  assumes a_b: "(a,b) \<in> r\<^sup>*"
  shows "b = f 0 \<Longrightarrow> (\<exists>f. f 0 = a \<and> (\<forall>i. (f i, f(Suc i)) \<in> r))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b = f 0 \<Longrightarrow> \<exists>f. f 0 = a \<and> (\<forall>i. (f i, f (Suc i)) \<in> r)
[PROOF STEP]
using a_b
[PROOF STATE]
proof (prove)
using this:
(a, b) \<in> r\<^sup>*

goal (1 subgoal):
 1. b = f 0 \<Longrightarrow> \<exists>f. f 0 = a \<and> (\<forall>i. (f i, f (Suc i)) \<in> r)
[PROOF STEP]
proof (induct rule: converse_rtrancl_induct [consumes 1])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. b = f 0 \<Longrightarrow> \<exists>f. f 0 = b \<and> (\<forall>i. (f i, f (Suc i)) \<in> r)
 2. \<And>y z. \<lbrakk>(y, z) \<in> r; (z, b) \<in> r\<^sup>*; b = f 0 \<Longrightarrow> \<exists>f. f 0 = z \<and> (\<forall>i. (f i, f (Suc i)) \<in> r); b = f 0\<rbrakk> \<Longrightarrow> \<exists>f. f 0 = y \<and> (\<forall>i. (f i, f (Suc i)) \<in> r)
[PROOF STEP]
assume "b = f 0"
[PROOF STATE]
proof (state)
this:
b = f 0

goal (2 subgoals):
 1. b = f 0 \<Longrightarrow> \<exists>f. f 0 = b \<and> (\<forall>i. (f i, f (Suc i)) \<in> r)
 2. \<And>y z. \<lbrakk>(y, z) \<in> r; (z, b) \<in> r\<^sup>*; b = f 0 \<Longrightarrow> \<exists>f. f 0 = z \<and> (\<forall>i. (f i, f (Suc i)) \<in> r); b = f 0\<rbrakk> \<Longrightarrow> \<exists>f. f 0 = y \<and> (\<forall>i. (f i, f (Suc i)) \<in> r)
[PROOF STEP]
with f
[PROOF STATE]
proof (chain)
picking this:
\<forall>i. (a, f i) \<in> r\<^sup>* \<and> (f i, f (Suc i)) \<in> r
b = f 0
[PROOF STEP]
show "\<exists>f. f 0 = b \<and> (\<forall>i. (f i, f (Suc i)) \<in> r)"
[PROOF STATE]
proof (prove)
using this:
\<forall>i. (a, f i) \<in> r\<^sup>* \<and> (f i, f (Suc i)) \<in> r
b = f 0

goal (1 subgoal):
 1. \<exists>f. f 0 = b \<and> (\<forall>i. (f i, f (Suc i)) \<in> r)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>f. f 0 = b \<and> (\<forall>i. (f i, f (Suc i)) \<in> r)

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(y, z) \<in> r; (z, b) \<in> r\<^sup>*; b = f 0 \<Longrightarrow> \<exists>f. f 0 = z \<and> (\<forall>i. (f i, f (Suc i)) \<in> r); b = f 0\<rbrakk> \<Longrightarrow> \<exists>f. f 0 = y \<and> (\<forall>i. (f i, f (Suc i)) \<in> r)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(y, z) \<in> r; (z, b) \<in> r\<^sup>*; b = f 0 \<Longrightarrow> \<exists>f. f 0 = z \<and> (\<forall>i. (f i, f (Suc i)) \<in> r); b = f 0\<rbrakk> \<Longrightarrow> \<exists>f. f 0 = y \<and> (\<forall>i. (f i, f (Suc i)) \<in> r)
[PROOF STEP]
fix a z
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(y, z) \<in> r; (z, b) \<in> r\<^sup>*; b = f 0 \<Longrightarrow> \<exists>f. f 0 = z \<and> (\<forall>i. (f i, f (Suc i)) \<in> r); b = f 0\<rbrakk> \<Longrightarrow> \<exists>f. f 0 = y \<and> (\<forall>i. (f i, f (Suc i)) \<in> r)
[PROOF STEP]
assume a_z: "(a, z) \<in> r" and "(z, b) \<in> r\<^sup>*"
[PROOF STATE]
proof (state)
this:
(a, z) \<in> r
(z, b) \<in> r\<^sup>*

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(y, z) \<in> r; (z, b) \<in> r\<^sup>*; b = f 0 \<Longrightarrow> \<exists>f. f 0 = z \<and> (\<forall>i. (f i, f (Suc i)) \<in> r); b = f 0\<rbrakk> \<Longrightarrow> \<exists>f. f 0 = y \<and> (\<forall>i. (f i, f (Suc i)) \<in> r)
[PROOF STEP]
assume "b = f 0 \<Longrightarrow> \<exists>f. f 0 = z \<and> (\<forall>i. (f i, f (Suc i)) \<in> r)"
         "b = f 0"
[PROOF STATE]
proof (state)
this:
b = f 0 \<Longrightarrow> \<exists>f. f 0 = z \<and> (\<forall>i. (f i, f (Suc i)) \<in> r)
b = f 0

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(y, z) \<in> r; (z, b) \<in> r\<^sup>*; b = f 0 \<Longrightarrow> \<exists>f. f 0 = z \<and> (\<forall>i. (f i, f (Suc i)) \<in> r); b = f 0\<rbrakk> \<Longrightarrow> \<exists>f. f 0 = y \<and> (\<forall>i. (f i, f (Suc i)) \<in> r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b = f 0 \<Longrightarrow> \<exists>f. f 0 = z \<and> (\<forall>i. (f i, f (Suc i)) \<in> r)
b = f 0
[PROOF STEP]
obtain f where f0: "f 0 = z" and seq: "\<forall>i. (f i, f (Suc i)) \<in> r"
[PROOF STATE]
proof (prove)
using this:
b = f 0 \<Longrightarrow> \<exists>f. f 0 = z \<and> (\<forall>i. (f i, f (Suc i)) \<in> r)
b = f 0

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f 0 = z; \<forall>i. (f i, f (Suc i)) \<in> r\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by iprover
[PROOF STATE]
proof (state)
this:
f 0 = z
\<forall>i. (f i, f (Suc i)) \<in> r

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(y, z) \<in> r; (z, b) \<in> r\<^sup>*; b = f 0 \<Longrightarrow> \<exists>f. f 0 = z \<and> (\<forall>i. (f i, f (Suc i)) \<in> r); b = f 0\<rbrakk> \<Longrightarrow> \<exists>f. f 0 = y \<and> (\<forall>i. (f i, f (Suc i)) \<in> r)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
f 0 = z
\<forall>i. (f i, f (Suc i)) \<in> r

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(y, z) \<in> r; (z, b) \<in> r\<^sup>*; b = f 0 \<Longrightarrow> \<exists>f. f 0 = z \<and> (\<forall>i. (f i, f (Suc i)) \<in> r); b = f 0\<rbrakk> \<Longrightarrow> \<exists>f. f 0 = y \<and> (\<forall>i. (f i, f (Suc i)) \<in> r)
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(y, z) \<in> r; (z, b) \<in> r\<^sup>*; b = f 0 \<Longrightarrow> \<exists>f. f 0 = z \<and> (\<forall>i. (f i, f (Suc i)) \<in> r); b = f 0\<rbrakk> \<Longrightarrow> \<exists>f. f 0 = y \<and> (\<forall>i. (f i, f (Suc i)) \<in> r)
[PROOF STEP]
have "((\<lambda>i. case i of 0 \<Rightarrow> a | Suc i \<Rightarrow> f i) i, f i) \<in> r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case i of 0 \<Rightarrow> a | Suc i \<Rightarrow> f i, f i) \<in> r
[PROOF STEP]
using seq a_z f0
[PROOF STATE]
proof (prove)
using this:
\<forall>i. (f i, f (Suc i)) \<in> r
(a, z) \<in> r
f 0 = z

goal (1 subgoal):
 1. (case i of 0 \<Rightarrow> a | Suc i \<Rightarrow> f i, f i) \<in> r
[PROOF STEP]
by (cases i) auto
[PROOF STATE]
proof (state)
this:
(case i of 0 \<Rightarrow> a | Suc i \<Rightarrow> f i, f i) \<in> r

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(y, z) \<in> r; (z, b) \<in> r\<^sup>*; b = f 0 \<Longrightarrow> \<exists>f. f 0 = z \<and> (\<forall>i. (f i, f (Suc i)) \<in> r); b = f 0\<rbrakk> \<Longrightarrow> \<exists>f. f 0 = y \<and> (\<forall>i. (f i, f (Suc i)) \<in> r)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(case ?i2 of 0 \<Rightarrow> a | Suc i \<Rightarrow> f i, f ?i2) \<in> r

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(y, z) \<in> r; (z, b) \<in> r\<^sup>*; b = f 0 \<Longrightarrow> \<exists>f. f 0 = z \<and> (\<forall>i. (f i, f (Suc i)) \<in> r); b = f 0\<rbrakk> \<Longrightarrow> \<exists>f. f 0 = y \<and> (\<forall>i. (f i, f (Suc i)) \<in> r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(case ?i2 of 0 \<Rightarrow> a | Suc i \<Rightarrow> f i, f ?i2) \<in> r
[PROOF STEP]
show "\<exists>f. f 0 = a \<and> (\<forall>i. (f i, f (Suc i)) \<in> r)"
[PROOF STATE]
proof (prove)
using this:
(case ?i2 of 0 \<Rightarrow> a | Suc i \<Rightarrow> f i, f ?i2) \<in> r

goal (1 subgoal):
 1. \<exists>f. f 0 = a \<and> (\<forall>i. (f i, f (Suc i)) \<in> r)
[PROOF STEP]
by - (rule exI [where x="\<lambda>i. case i of 0 \<Rightarrow> a | Suc i \<Rightarrow> f i"],simp)
[PROOF STATE]
proof (state)
this:
\<exists>f. f 0 = a \<and> (\<forall>i. (f i, f (Suc i)) \<in> r)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma renumber:
 "\<forall>i. (a,f i) \<in> r\<^sup>* \<and> (f i,f(Suc i)) \<in> r
 \<Longrightarrow> \<exists>f. f 0 = a \<and> (\<forall>i. (f i, f(Suc i)) \<in> r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. (a, f i) \<in> r\<^sup>* \<and> (f i, f (Suc i)) \<in> r \<Longrightarrow> \<exists>f. f 0 = a \<and> (\<forall>i. (f i, f (Suc i)) \<in> r)
[PROOF STEP]
by(blast dest:renumber')


[STATEMENT]
lemma not_inf_Fault':
  assumes enum_step: "\<forall>i. \<Gamma>\<turnstile>f i \<rightarrow> f (Suc i)"
  shows "\<And>k cs. f k = (cs,css,Fault m) \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k cs. f k = (cs, css, Fault m) \<Longrightarrow> False
[PROOF STEP]
proof (induct css)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>k cs. f k = (cs, [], Fault m) \<Longrightarrow> False
 2. \<And>a css k cs. \<lbrakk>\<And>k cs. f k = (cs, css, Fault m) \<Longrightarrow> False; f k = (cs, a # css, Fault m)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
f k = (cs, [], Fault m)

goal (2 subgoals):
 1. \<And>k cs. f k = (cs, [], Fault m) \<Longrightarrow> False
 2. \<And>a css k cs. \<lbrakk>\<And>k cs. f k = (cs, css, Fault m) \<Longrightarrow> False; f k = (cs, a # css, Fault m)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have f_k: "f k = (cs,[],Fault m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f k = (cs, [], Fault m)
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
f k = (cs, [], Fault m)

goal (2 subgoals):
 1. \<And>k cs. f k = (cs, [], Fault m) \<Longrightarrow> False
 2. \<And>a css k cs. \<lbrakk>\<And>k cs. f k = (cs, css, Fault m) \<Longrightarrow> False; f k = (cs, a # css, Fault m)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "\<And>k. f k = (cs,[],Fault m) \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. f k = (cs, [], Fault m) \<Longrightarrow> False
[PROOF STEP]
proof (induct cs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>k. f k = ([], [], Fault m) \<Longrightarrow> False
 2. \<And>a cs k. \<lbrakk>\<And>k. f k = (cs, [], Fault m) \<Longrightarrow> False; f k = (a # cs, [], Fault m)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
f k = ([], [], Fault m)

goal (2 subgoals):
 1. \<And>k. f k = ([], [], Fault m) \<Longrightarrow> False
 2. \<And>a cs k. \<lbrakk>\<And>k. f k = (cs, [], Fault m) \<Longrightarrow> False; f k = (a # cs, [], Fault m)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "f k = ([], [], Fault m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f k = ([], [], Fault m)
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
f k = ([], [], Fault m)

goal (2 subgoals):
 1. \<And>k. f k = ([], [], Fault m) \<Longrightarrow> False
 2. \<And>a cs k. \<lbrakk>\<And>k. f k = (cs, [], Fault m) \<Longrightarrow> False; f k = (a # cs, [], Fault m)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f k = ([], [], Fault m)

goal (2 subgoals):
 1. \<And>k. f k = ([], [], Fault m) \<Longrightarrow> False
 2. \<And>a cs k. \<lbrakk>\<And>k. f k = (cs, [], Fault m) \<Longrightarrow> False; f k = (a # cs, [], Fault m)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from enum_step
[PROOF STATE]
proof (chain)
picking this:
\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)
[PROOF STEP]
have "\<Gamma>\<turnstile>f k \<rightarrow> f (Suc k)"
[PROOF STATE]
proof (prove)
using this:
\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)

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

goal (2 subgoals):
 1. \<And>k. f k = ([], [], Fault m) \<Longrightarrow> False
 2. \<And>a cs k. \<lbrakk>\<And>k. f k = (cs, [], Fault m) \<Longrightarrow> False; f k = (a # cs, [], Fault m)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
f k = ([], [], Fault m)
\<Gamma>\<turnstile> f k \<rightarrow> f (Suc k)
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
f k = ([], [], Fault m)
\<Gamma>\<turnstile> f k \<rightarrow> f (Suc k)

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

goal (1 subgoal):
 1. \<And>a cs k. \<lbrakk>\<And>k. f k = (cs, [], Fault m) \<Longrightarrow> False; f k = (a # cs, [], Fault m)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a cs k. \<lbrakk>\<And>k. f k = (cs, [], Fault m) \<Longrightarrow> False; f k = (a # cs, [], Fault m)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
case (Cons c cs)
[PROOF STATE]
proof (state)
this:
f ?k = (cs, [], Fault m) \<Longrightarrow> False
f k = (c # cs, [], Fault m)

goal (1 subgoal):
 1. \<And>a cs k. \<lbrakk>\<And>k. f k = (cs, [], Fault m) \<Longrightarrow> False; f k = (a # cs, [], Fault m)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have fk: "f k = (c # cs, [], Fault m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f k = (c # cs, [], Fault m)
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
f k = (c # cs, [], Fault m)

goal (1 subgoal):
 1. \<And>a cs k. \<lbrakk>\<And>k. f k = (cs, [], Fault m) \<Longrightarrow> False; f k = (a # cs, [], Fault m)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from enum_step
[PROOF STATE]
proof (chain)
picking this:
\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)
[PROOF STEP]
have "\<Gamma>\<turnstile>f k \<rightarrow> f (Suc k)"
[PROOF STATE]
proof (prove)
using this:
\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)

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

goal (1 subgoal):
 1. \<And>a cs k. \<lbrakk>\<And>k. f k = (cs, [], Fault m) \<Longrightarrow> False; f k = (a # cs, [], Fault m)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with fk
[PROOF STATE]
proof (chain)
picking this:
f k = (c # cs, [], Fault m)
\<Gamma>\<turnstile> f k \<rightarrow> f (Suc k)
[PROOF STEP]
have "f (Suc k) = (cs,[],Fault m)"
[PROOF STATE]
proof (prove)
using this:
f k = (c # cs, [], Fault m)
\<Gamma>\<turnstile> f k \<rightarrow> f (Suc k)

goal (1 subgoal):
 1. f (Suc k) = (cs, [], Fault m)
[PROOF STEP]
by (fastforce elim: step_elim_cases)
[PROOF STATE]
proof (state)
this:
f (Suc k) = (cs, [], Fault m)

goal (1 subgoal):
 1. \<And>a cs k. \<lbrakk>\<And>k. f k = (cs, [], Fault m) \<Longrightarrow> False; f k = (a # cs, [], Fault m)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with enum_step Cons.hyps
[PROOF STATE]
proof (chain)
picking this:
\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)
f ?k = (cs, [], Fault m) \<Longrightarrow> False
f (Suc k) = (cs, [], Fault m)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)
f ?k = (cs, [], Fault m) \<Longrightarrow> False
f (Suc k) = (cs, [], Fault m)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f ?k = (cs, [], Fault m) \<Longrightarrow> False

goal (2 subgoals):
 1. \<And>k cs. f k = (cs, [], Fault m) \<Longrightarrow> False
 2. \<And>a css k cs. \<lbrakk>\<And>k cs. f k = (cs, css, Fault m) \<Longrightarrow> False; f k = (cs, a # css, Fault m)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from this f_k
[PROOF STATE]
proof (chain)
picking this:
f ?k = (cs, [], Fault m) \<Longrightarrow> False
f k = (cs, [], Fault m)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
f ?k = (cs, [], Fault m) \<Longrightarrow> False
f k = (cs, [], Fault m)

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

goal (1 subgoal):
 1. \<And>a css k cs. \<lbrakk>\<And>k cs. f k = (cs, css, Fault m) \<Longrightarrow> False; f k = (cs, a # css, Fault m)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a css k cs. \<lbrakk>\<And>k cs. f k = (cs, css, Fault m) \<Longrightarrow> False; f k = (cs, a # css, Fault m)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
case (Cons ds css)
[PROOF STATE]
proof (state)
this:
f ?k = (?cs, css, Fault m) \<Longrightarrow> False
f k = (cs, ds # css, Fault m)

goal (1 subgoal):
 1. \<And>a css k cs. \<lbrakk>\<And>k cs. f k = (cs, css, Fault m) \<Longrightarrow> False; f k = (cs, a # css, Fault m)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f ?k = (?cs, css, Fault m) \<Longrightarrow> False
f k = (cs, ds # css, Fault m)
[PROOF STEP]
obtain nrms abrs where ds: "ds=(nrms,abrs)"
[PROOF STATE]
proof (prove)
using this:
f ?k = (?cs, css, Fault m) \<Longrightarrow> False
f k = (cs, ds # css, Fault m)

goal (1 subgoal):
 1. (\<And>nrms abrs. ds = (nrms, abrs) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases ds) auto
[PROOF STATE]
proof (state)
this:
ds = (nrms, abrs)

goal (1 subgoal):
 1. \<And>a css k cs. \<lbrakk>\<And>k cs. f k = (cs, css, Fault m) \<Longrightarrow> False; f k = (cs, a # css, Fault m)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have hyp: "\<And>k cs. f k = (cs,css,Fault m) \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k cs. f k = (cs, css, Fault m) \<Longrightarrow> False
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
f ?k = (?cs, css, Fault m) \<Longrightarrow> False

goal (1 subgoal):
 1. \<And>a css k cs. \<lbrakk>\<And>k cs. f k = (cs, css, Fault m) \<Longrightarrow> False; f k = (cs, a # css, Fault m)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "\<And>k. f k = (cs,(nrms,abrs)#css,Fault m) \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. f k = (cs, (nrms, abrs) # css, Fault m) \<Longrightarrow> False
[PROOF STEP]
proof (induct cs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>k. f k = ([], (nrms, abrs) # css, Fault m) \<Longrightarrow> False
 2. \<And>a cs k. \<lbrakk>\<And>k. f k = (cs, (nrms, abrs) # css, Fault m) \<Longrightarrow> False; f k = (a # cs, (nrms, abrs) # css, Fault m)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
f k = ([], (nrms, abrs) # css, Fault m)

goal (2 subgoals):
 1. \<And>k. f k = ([], (nrms, abrs) # css, Fault m) \<Longrightarrow> False
 2. \<And>a cs k. \<lbrakk>\<And>k. f k = (cs, (nrms, abrs) # css, Fault m) \<Longrightarrow> False; f k = (a # cs, (nrms, abrs) # css, Fault m)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have fk: "f k = ([], (nrms, abrs) # css, Fault m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f k = ([], (nrms, abrs) # css, Fault m)
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
f k = ([], (nrms, abrs) # css, Fault m)

goal (2 subgoals):
 1. \<And>k. f k = ([], (nrms, abrs) # css, Fault m) \<Longrightarrow> False
 2. \<And>a cs k. \<lbrakk>\<And>k. f k = (cs, (nrms, abrs) # css, Fault m) \<Longrightarrow> False; f k = (a # cs, (nrms, abrs) # css, Fault m)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from enum_step
[PROOF STATE]
proof (chain)
picking this:
\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)
[PROOF STEP]
have "\<Gamma>\<turnstile>f k \<rightarrow> f (Suc k)"
[PROOF STATE]
proof (prove)
using this:
\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)

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

goal (2 subgoals):
 1. \<And>k. f k = ([], (nrms, abrs) # css, Fault m) \<Longrightarrow> False
 2. \<And>a cs k. \<lbrakk>\<And>k. f k = (cs, (nrms, abrs) # css, Fault m) \<Longrightarrow> False; f k = (a # cs, (nrms, abrs) # css, Fault m)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with fk
[PROOF STATE]
proof (chain)
picking this:
f k = ([], (nrms, abrs) # css, Fault m)
\<Gamma>\<turnstile> f k \<rightarrow> f (Suc k)
[PROOF STEP]
have "f (Suc k) = (nrms,css,Fault m)"
[PROOF STATE]
proof (prove)
using this:
f k = ([], (nrms, abrs) # css, Fault m)
\<Gamma>\<turnstile> f k \<rightarrow> f (Suc k)

goal (1 subgoal):
 1. f (Suc k) = (nrms, css, Fault m)
[PROOF STEP]
by (fastforce elim: step_elim_cases)
[PROOF STATE]
proof (state)
this:
f (Suc k) = (nrms, css, Fault m)

goal (2 subgoals):
 1. \<And>k. f k = ([], (nrms, abrs) # css, Fault m) \<Longrightarrow> False
 2. \<And>a cs k. \<lbrakk>\<And>k. f k = (cs, (nrms, abrs) # css, Fault m) \<Longrightarrow> False; f k = (a # cs, (nrms, abrs) # css, Fault m)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
f (Suc k) = (nrms, css, Fault m)

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

goal (1 subgoal):
 1. \<And>a cs k. \<lbrakk>\<And>k. f k = (cs, (nrms, abrs) # css, Fault m) \<Longrightarrow> False; f k = (a # cs, (nrms, abrs) # css, Fault m)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a cs k. \<lbrakk>\<And>k. f k = (cs, (nrms, abrs) # css, Fault m) \<Longrightarrow> False; f k = (a # cs, (nrms, abrs) # css, Fault m)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
case (Cons c cs)
[PROOF STATE]
proof (state)
this:
f ?k = (cs, (nrms, abrs) # css, Fault m) \<Longrightarrow> False
f k = (c # cs, (nrms, abrs) # css, Fault m)

goal (1 subgoal):
 1. \<And>a cs k. \<lbrakk>\<And>k. f k = (cs, (nrms, abrs) # css, Fault m) \<Longrightarrow> False; f k = (a # cs, (nrms, abrs) # css, Fault m)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have fk: "f k = (c#cs, (nrms, abrs) # css, Fault m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f k = (c # cs, (nrms, abrs) # css, Fault m)
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
f k = (c # cs, (nrms, abrs) # css, Fault m)

goal (1 subgoal):
 1. \<And>a cs k. \<lbrakk>\<And>k. f k = (cs, (nrms, abrs) # css, Fault m) \<Longrightarrow> False; f k = (a # cs, (nrms, abrs) # css, Fault m)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have hyp1: "\<And>k. f k = (cs, (nrms, abrs) # css, Fault m) \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. f k = (cs, (nrms, abrs) # css, Fault m) \<Longrightarrow> False
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
f ?k = (cs, (nrms, abrs) # css, Fault m) \<Longrightarrow> False

goal (1 subgoal):
 1. \<And>a cs k. \<lbrakk>\<And>k. f k = (cs, (nrms, abrs) # css, Fault m) \<Longrightarrow> False; f k = (a # cs, (nrms, abrs) # css, Fault m)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from enum_step
[PROOF STATE]
proof (chain)
picking this:
\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)
[PROOF STEP]
have "\<Gamma>\<turnstile>f k \<rightarrow> f (Suc k)"
[PROOF STATE]
proof (prove)
using this:
\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)

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

goal (1 subgoal):
 1. \<And>a cs k. \<lbrakk>\<And>k. f k = (cs, (nrms, abrs) # css, Fault m) \<Longrightarrow> False; f k = (a # cs, (nrms, abrs) # css, Fault m)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with fk
[PROOF STATE]
proof (chain)
picking this:
f k = (c # cs, (nrms, abrs) # css, Fault m)
\<Gamma>\<turnstile> f k \<rightarrow> f (Suc k)
[PROOF STEP]
have "f (Suc k) = (cs,(nrms,abrs)#css,Fault m)"
[PROOF STATE]
proof (prove)
using this:
f k = (c # cs, (nrms, abrs) # css, Fault m)
\<Gamma>\<turnstile> f k \<rightarrow> f (Suc k)

goal (1 subgoal):
 1. f (Suc k) = (cs, (nrms, abrs) # css, Fault m)
[PROOF STEP]
by (fastforce elim: step_elim_cases)
[PROOF STATE]
proof (state)
this:
f (Suc k) = (cs, (nrms, abrs) # css, Fault m)

goal (1 subgoal):
 1. \<And>a cs k. \<lbrakk>\<And>k. f k = (cs, (nrms, abrs) # css, Fault m) \<Longrightarrow> False; f k = (a # cs, (nrms, abrs) # css, Fault m)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
f (Suc k) = (cs, (nrms, abrs) # css, Fault m)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f ?k = (cs, (nrms, abrs) # css, Fault m) \<Longrightarrow> False

goal (1 subgoal):
 1. \<And>a css k cs. \<lbrakk>\<And>k cs. f k = (cs, css, Fault m) \<Longrightarrow> False; f k = (cs, a # css, Fault m)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with ds Cons.prems
[PROOF STATE]
proof (chain)
picking this:
ds = (nrms, abrs)
f k = (cs, ds # css, Fault m)
f ?k = (cs, (nrms, abrs) # css, Fault m) \<Longrightarrow> False
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
ds = (nrms, abrs)
f k = (cs, ds # css, Fault m)
f ?k = (cs, (nrms, abrs) # css, Fault m) \<Longrightarrow> False

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma not_inf_Fault:
  "\<not> inf \<Gamma> cs css (Fault m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> AlternativeSmallStep.inf \<Gamma> cs css (Fault m)
[PROOF STEP]
apply (rule not_infI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f. \<lbrakk>f 0 = (cs, css, Fault m); \<And>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (rule_tac f=f in not_inf_Fault' )
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>f. \<lbrakk>f 0 = (cs, css, Fault m); \<And>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> \<forall>i. ?\<Gamma>2 f\<turnstile> f i \<rightarrow> f (Suc i)
 2. \<And>f. \<lbrakk>f 0 = (cs, css, Fault m); \<And>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> f (?k2 f) = (?cs2 f, ?css2 f, Fault (?m2 f))
[PROOF STEP]
by auto


[STATEMENT]
lemma not_inf_Stuck':
  assumes enum_step: "\<forall>i. \<Gamma>\<turnstile>f i \<rightarrow> f (Suc i)"
  shows "\<And>k cs. f k = (cs,css,Stuck) \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k cs. f k = (cs, css, Stuck) \<Longrightarrow> False
[PROOF STEP]
proof (induct css)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>k cs. f k = (cs, [], Stuck) \<Longrightarrow> False
 2. \<And>a css k cs. \<lbrakk>\<And>k cs. f k = (cs, css, Stuck) \<Longrightarrow> False; f k = (cs, a # css, Stuck)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
f k = (cs, [], Stuck)

goal (2 subgoals):
 1. \<And>k cs. f k = (cs, [], Stuck) \<Longrightarrow> False
 2. \<And>a css k cs. \<lbrakk>\<And>k cs. f k = (cs, css, Stuck) \<Longrightarrow> False; f k = (cs, a # css, Stuck)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have f_k: "f k = (cs,[],Stuck)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f k = (cs, [], Stuck)
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
f k = (cs, [], Stuck)

goal (2 subgoals):
 1. \<And>k cs. f k = (cs, [], Stuck) \<Longrightarrow> False
 2. \<And>a css k cs. \<lbrakk>\<And>k cs. f k = (cs, css, Stuck) \<Longrightarrow> False; f k = (cs, a # css, Stuck)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "\<And>k. f k = (cs,[],Stuck) \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. f k = (cs, [], Stuck) \<Longrightarrow> False
[PROOF STEP]
proof (induct cs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>k. f k = ([], [], Stuck) \<Longrightarrow> False
 2. \<And>a cs k. \<lbrakk>\<And>k. f k = (cs, [], Stuck) \<Longrightarrow> False; f k = (a # cs, [], Stuck)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
f k = ([], [], Stuck)

goal (2 subgoals):
 1. \<And>k. f k = ([], [], Stuck) \<Longrightarrow> False
 2. \<And>a cs k. \<lbrakk>\<And>k. f k = (cs, [], Stuck) \<Longrightarrow> False; f k = (a # cs, [], Stuck)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "f k = ([], [], Stuck)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f k = ([], [], Stuck)
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
f k = ([], [], Stuck)

goal (2 subgoals):
 1. \<And>k. f k = ([], [], Stuck) \<Longrightarrow> False
 2. \<And>a cs k. \<lbrakk>\<And>k. f k = (cs, [], Stuck) \<Longrightarrow> False; f k = (a # cs, [], Stuck)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f k = ([], [], Stuck)

goal (2 subgoals):
 1. \<And>k. f k = ([], [], Stuck) \<Longrightarrow> False
 2. \<And>a cs k. \<lbrakk>\<And>k. f k = (cs, [], Stuck) \<Longrightarrow> False; f k = (a # cs, [], Stuck)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from enum_step
[PROOF STATE]
proof (chain)
picking this:
\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)
[PROOF STEP]
have "\<Gamma>\<turnstile>f k \<rightarrow> f (Suc k)"
[PROOF STATE]
proof (prove)
using this:
\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)

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

goal (2 subgoals):
 1. \<And>k. f k = ([], [], Stuck) \<Longrightarrow> False
 2. \<And>a cs k. \<lbrakk>\<And>k. f k = (cs, [], Stuck) \<Longrightarrow> False; f k = (a # cs, [], Stuck)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
f k = ([], [], Stuck)
\<Gamma>\<turnstile> f k \<rightarrow> f (Suc k)
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
f k = ([], [], Stuck)
\<Gamma>\<turnstile> f k \<rightarrow> f (Suc k)

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

goal (1 subgoal):
 1. \<And>a cs k. \<lbrakk>\<And>k. f k = (cs, [], Stuck) \<Longrightarrow> False; f k = (a # cs, [], Stuck)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a cs k. \<lbrakk>\<And>k. f k = (cs, [], Stuck) \<Longrightarrow> False; f k = (a # cs, [], Stuck)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
case (Cons c cs)
[PROOF STATE]
proof (state)
this:
f ?k = (cs, [], Stuck) \<Longrightarrow> False
f k = (c # cs, [], Stuck)

goal (1 subgoal):
 1. \<And>a cs k. \<lbrakk>\<And>k. f k = (cs, [], Stuck) \<Longrightarrow> False; f k = (a # cs, [], Stuck)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have fk: "f k = (c # cs, [], Stuck)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f k = (c # cs, [], Stuck)
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
f k = (c # cs, [], Stuck)

goal (1 subgoal):
 1. \<And>a cs k. \<lbrakk>\<And>k. f k = (cs, [], Stuck) \<Longrightarrow> False; f k = (a # cs, [], Stuck)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from enum_step
[PROOF STATE]
proof (chain)
picking this:
\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)
[PROOF STEP]
have "\<Gamma>\<turnstile>f k \<rightarrow> f (Suc k)"
[PROOF STATE]
proof (prove)
using this:
\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)

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

goal (1 subgoal):
 1. \<And>a cs k. \<lbrakk>\<And>k. f k = (cs, [], Stuck) \<Longrightarrow> False; f k = (a # cs, [], Stuck)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with fk
[PROOF STATE]
proof (chain)
picking this:
f k = (c # cs, [], Stuck)
\<Gamma>\<turnstile> f k \<rightarrow> f (Suc k)
[PROOF STEP]
have "f (Suc k) = (cs,[],Stuck)"
[PROOF STATE]
proof (prove)
using this:
f k = (c # cs, [], Stuck)
\<Gamma>\<turnstile> f k \<rightarrow> f (Suc k)

goal (1 subgoal):
 1. f (Suc k) = (cs, [], Stuck)
[PROOF STEP]
by (fastforce elim: step_elim_cases)
[PROOF STATE]
proof (state)
this:
f (Suc k) = (cs, [], Stuck)

goal (1 subgoal):
 1. \<And>a cs k. \<lbrakk>\<And>k. f k = (cs, [], Stuck) \<Longrightarrow> False; f k = (a # cs, [], Stuck)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with enum_step Cons.hyps
[PROOF STATE]
proof (chain)
picking this:
\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)
f ?k = (cs, [], Stuck) \<Longrightarrow> False
f (Suc k) = (cs, [], Stuck)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)
f ?k = (cs, [], Stuck) \<Longrightarrow> False
f (Suc k) = (cs, [], Stuck)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f ?k = (cs, [], Stuck) \<Longrightarrow> False

goal (2 subgoals):
 1. \<And>k cs. f k = (cs, [], Stuck) \<Longrightarrow> False
 2. \<And>a css k cs. \<lbrakk>\<And>k cs. f k = (cs, css, Stuck) \<Longrightarrow> False; f k = (cs, a # css, Stuck)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from this f_k
[PROOF STATE]
proof (chain)
picking this:
f ?k = (cs, [], Stuck) \<Longrightarrow> False
f k = (cs, [], Stuck)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
f ?k = (cs, [], Stuck) \<Longrightarrow> False
f k = (cs, [], Stuck)

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

goal (1 subgoal):
 1. \<And>a css k cs. \<lbrakk>\<And>k cs. f k = (cs, css, Stuck) \<Longrightarrow> False; f k = (cs, a # css, Stuck)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a css k cs. \<lbrakk>\<And>k cs. f k = (cs, css, Stuck) \<Longrightarrow> False; f k = (cs, a # css, Stuck)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
case (Cons ds css)
[PROOF STATE]
proof (state)
this:
f ?k = (?cs, css, Stuck) \<Longrightarrow> False
f k = (cs, ds # css, Stuck)

goal (1 subgoal):
 1. \<And>a css k cs. \<lbrakk>\<And>k cs. f k = (cs, css, Stuck) \<Longrightarrow> False; f k = (cs, a # css, Stuck)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f ?k = (?cs, css, Stuck) \<Longrightarrow> False
f k = (cs, ds # css, Stuck)
[PROOF STEP]
obtain nrms abrs where ds: "ds=(nrms,abrs)"
[PROOF STATE]
proof (prove)
using this:
f ?k = (?cs, css, Stuck) \<Longrightarrow> False
f k = (cs, ds # css, Stuck)

goal (1 subgoal):
 1. (\<And>nrms abrs. ds = (nrms, abrs) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases ds) auto
[PROOF STATE]
proof (state)
this:
ds = (nrms, abrs)

goal (1 subgoal):
 1. \<And>a css k cs. \<lbrakk>\<And>k cs. f k = (cs, css, Stuck) \<Longrightarrow> False; f k = (cs, a # css, Stuck)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have hyp: "\<And>k cs. f k = (cs,css,Stuck) \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k cs. f k = (cs, css, Stuck) \<Longrightarrow> False
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
f ?k = (?cs, css, Stuck) \<Longrightarrow> False

goal (1 subgoal):
 1. \<And>a css k cs. \<lbrakk>\<And>k cs. f k = (cs, css, Stuck) \<Longrightarrow> False; f k = (cs, a # css, Stuck)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "\<And>k. f k = (cs,(nrms,abrs)#css,Stuck) \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. f k = (cs, (nrms, abrs) # css, Stuck) \<Longrightarrow> False
[PROOF STEP]
proof (induct cs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>k. f k = ([], (nrms, abrs) # css, Stuck) \<Longrightarrow> False
 2. \<And>a cs k. \<lbrakk>\<And>k. f k = (cs, (nrms, abrs) # css, Stuck) \<Longrightarrow> False; f k = (a # cs, (nrms, abrs) # css, Stuck)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
f k = ([], (nrms, abrs) # css, Stuck)

goal (2 subgoals):
 1. \<And>k. f k = ([], (nrms, abrs) # css, Stuck) \<Longrightarrow> False
 2. \<And>a cs k. \<lbrakk>\<And>k. f k = (cs, (nrms, abrs) # css, Stuck) \<Longrightarrow> False; f k = (a # cs, (nrms, abrs) # css, Stuck)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have fk: "f k = ([], (nrms, abrs) # css, Stuck)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f k = ([], (nrms, abrs) # css, Stuck)
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
f k = ([], (nrms, abrs) # css, Stuck)

goal (2 subgoals):
 1. \<And>k. f k = ([], (nrms, abrs) # css, Stuck) \<Longrightarrow> False
 2. \<And>a cs k. \<lbrakk>\<And>k. f k = (cs, (nrms, abrs) # css, Stuck) \<Longrightarrow> False; f k = (a # cs, (nrms, abrs) # css, Stuck)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from enum_step
[PROOF STATE]
proof (chain)
picking this:
\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)
[PROOF STEP]
have "\<Gamma>\<turnstile>f k \<rightarrow> f (Suc k)"
[PROOF STATE]
proof (prove)
using this:
\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)

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

goal (2 subgoals):
 1. \<And>k. f k = ([], (nrms, abrs) # css, Stuck) \<Longrightarrow> False
 2. \<And>a cs k. \<lbrakk>\<And>k. f k = (cs, (nrms, abrs) # css, Stuck) \<Longrightarrow> False; f k = (a # cs, (nrms, abrs) # css, Stuck)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with fk
[PROOF STATE]
proof (chain)
picking this:
f k = ([], (nrms, abrs) # css, Stuck)
\<Gamma>\<turnstile> f k \<rightarrow> f (Suc k)
[PROOF STEP]
have "f (Suc k) = (nrms,css,Stuck)"
[PROOF STATE]
proof (prove)
using this:
f k = ([], (nrms, abrs) # css, Stuck)
\<Gamma>\<turnstile> f k \<rightarrow> f (Suc k)

goal (1 subgoal):
 1. f (Suc k) = (nrms, css, Stuck)
[PROOF STEP]
by (fastforce elim: step_elim_cases)
[PROOF STATE]
proof (state)
this:
f (Suc k) = (nrms, css, Stuck)

goal (2 subgoals):
 1. \<And>k. f k = ([], (nrms, abrs) # css, Stuck) \<Longrightarrow> False
 2. \<And>a cs k. \<lbrakk>\<And>k. f k = (cs, (nrms, abrs) # css, Stuck) \<Longrightarrow> False; f k = (a # cs, (nrms, abrs) # css, Stuck)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
f (Suc k) = (nrms, css, Stuck)

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

goal (1 subgoal):
 1. \<And>a cs k. \<lbrakk>\<And>k. f k = (cs, (nrms, abrs) # css, Stuck) \<Longrightarrow> False; f k = (a # cs, (nrms, abrs) # css, Stuck)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a cs k. \<lbrakk>\<And>k. f k = (cs, (nrms, abrs) # css, Stuck) \<Longrightarrow> False; f k = (a # cs, (nrms, abrs) # css, Stuck)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
case (Cons c cs)
[PROOF STATE]
proof (state)
this:
f ?k = (cs, (nrms, abrs) # css, Stuck) \<Longrightarrow> False
f k = (c # cs, (nrms, abrs) # css, Stuck)

goal (1 subgoal):
 1. \<And>a cs k. \<lbrakk>\<And>k. f k = (cs, (nrms, abrs) # css, Stuck) \<Longrightarrow> False; f k = (a # cs, (nrms, abrs) # css, Stuck)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have fk: "f k = (c#cs, (nrms, abrs) # css, Stuck)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f k = (c # cs, (nrms, abrs) # css, Stuck)
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
f k = (c # cs, (nrms, abrs) # css, Stuck)

goal (1 subgoal):
 1. \<And>a cs k. \<lbrakk>\<And>k. f k = (cs, (nrms, abrs) # css, Stuck) \<Longrightarrow> False; f k = (a # cs, (nrms, abrs) # css, Stuck)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have hyp1: "\<And>k. f k = (cs, (nrms, abrs) # css, Stuck) \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. f k = (cs, (nrms, abrs) # css, Stuck) \<Longrightarrow> False
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
f ?k = (cs, (nrms, abrs) # css, Stuck) \<Longrightarrow> False

goal (1 subgoal):
 1. \<And>a cs k. \<lbrakk>\<And>k. f k = (cs, (nrms, abrs) # css, Stuck) \<Longrightarrow> False; f k = (a # cs, (nrms, abrs) # css, Stuck)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from enum_step
[PROOF STATE]
proof (chain)
picking this:
\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)
[PROOF STEP]
have "\<Gamma>\<turnstile>f k \<rightarrow> f (Suc k)"
[PROOF STATE]
proof (prove)
using this:
\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)

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

goal (1 subgoal):
 1. \<And>a cs k. \<lbrakk>\<And>k. f k = (cs, (nrms, abrs) # css, Stuck) \<Longrightarrow> False; f k = (a # cs, (nrms, abrs) # css, Stuck)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with fk
[PROOF STATE]
proof (chain)
picking this:
f k = (c # cs, (nrms, abrs) # css, Stuck)
\<Gamma>\<turnstile> f k \<rightarrow> f (Suc k)
[PROOF STEP]
have "f (Suc k) = (cs,(nrms,abrs)#css,Stuck)"
[PROOF STATE]
proof (prove)
using this:
f k = (c # cs, (nrms, abrs) # css, Stuck)
\<Gamma>\<turnstile> f k \<rightarrow> f (Suc k)

goal (1 subgoal):
 1. f (Suc k) = (cs, (nrms, abrs) # css, Stuck)
[PROOF STEP]
by (fastforce elim: step_elim_cases)
[PROOF STATE]
proof (state)
this:
f (Suc k) = (cs, (nrms, abrs) # css, Stuck)

goal (1 subgoal):
 1. \<And>a cs k. \<lbrakk>\<And>k. f k = (cs, (nrms, abrs) # css, Stuck) \<Longrightarrow> False; f k = (a # cs, (nrms, abrs) # css, Stuck)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
f (Suc k) = (cs, (nrms, abrs) # css, Stuck)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f ?k = (cs, (nrms, abrs) # css, Stuck) \<Longrightarrow> False

goal (1 subgoal):
 1. \<And>a css k cs. \<lbrakk>\<And>k cs. f k = (cs, css, Stuck) \<Longrightarrow> False; f k = (cs, a # css, Stuck)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with ds Cons.prems
[PROOF STATE]
proof (chain)
picking this:
ds = (nrms, abrs)
f k = (cs, ds # css, Stuck)
f ?k = (cs, (nrms, abrs) # css, Stuck) \<Longrightarrow> False
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
ds = (nrms, abrs)
f k = (cs, ds # css, Stuck)
f ?k = (cs, (nrms, abrs) # css, Stuck) \<Longrightarrow> False

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma not_inf_Stuck:
  "\<not> inf \<Gamma> cs css Stuck"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> AlternativeSmallStep.inf \<Gamma> cs css Stuck
[PROOF STEP]
apply (rule not_infI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f. \<lbrakk>f 0 = (cs, css, Stuck); \<And>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (rule_tac f=f in not_inf_Stuck')
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>f. \<lbrakk>f 0 = (cs, css, Stuck); \<And>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> \<forall>i. ?\<Gamma>2 f\<turnstile> f i \<rightarrow> f (Suc i)
 2. \<And>f. \<lbrakk>f 0 = (cs, css, Stuck); \<And>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> f (?k2 f) = (?cs2 f, ?css2 f, Stuck)
[PROOF STEP]
by auto


[STATEMENT]
lemma last_butlast_app:
assumes butlast: "butlast as = xs @ butlast bs"
assumes not_Nil: "bs \<noteq> []" "as \<noteq> []"
assumes last: "fst (last as) = fst (last bs)" "snd (last as) = snd (last bs)"
shows "as = xs @ bs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. as = xs @ bs
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. as = xs @ bs
[PROOF STEP]
from last
[PROOF STATE]
proof (chain)
picking this:
fst (last as) = fst (last bs)
snd (last as) = snd (last bs)
[PROOF STEP]
have "last as = last bs"
[PROOF STATE]
proof (prove)
using this:
fst (last as) = fst (last bs)
snd (last as) = snd (last bs)

goal (1 subgoal):
 1. last as = last bs
[PROOF STEP]
by (cases "last as",cases "last bs") simp
[PROOF STATE]
proof (state)
this:
last as = last bs

goal (1 subgoal):
 1. as = xs @ bs
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
last as = last bs

goal (1 subgoal):
 1. as = xs @ bs
[PROOF STEP]
from not_Nil
[PROOF STATE]
proof (chain)
picking this:
bs \<noteq> []
as \<noteq> []
[PROOF STEP]
have "as = butlast as @ [last as]" "bs = butlast bs @ [last bs]"
[PROOF STATE]
proof (prove)
using this:
bs \<noteq> []
as \<noteq> []

goal (1 subgoal):
 1. as = butlast as @ [last as] &&& bs = butlast bs @ [last bs]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
as = butlast as @ [last as]
bs = butlast bs @ [last bs]

goal (1 subgoal):
 1. as = xs @ bs
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
last as = last bs
as = butlast as @ [last as]
bs = butlast bs @ [last bs]
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
last as = last bs
as = butlast as @ [last as]
bs = butlast bs @ [last bs]

goal (1 subgoal):
 1. as = xs @ bs
[PROOF STEP]
using butlast
[PROOF STATE]
proof (prove)
using this:
last as = last bs
as = butlast as @ [last as]
bs = butlast bs @ [last bs]
butlast as = xs @ butlast bs

goal (1 subgoal):
 1. as = xs @ bs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
as = xs @ bs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma last_butlast_tl:
assumes butlast: "butlast bs = x # butlast as"
assumes not_Nil: "bs \<noteq> []" "as \<noteq> []"
assumes last: "fst (last as) = fst (last bs)" "snd (last as) = snd (last bs)"
shows "as = tl bs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. as = tl bs
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. as = tl bs
[PROOF STEP]
from last
[PROOF STATE]
proof (chain)
picking this:
fst (last as) = fst (last bs)
snd (last as) = snd (last bs)
[PROOF STEP]
have "last as = last bs"
[PROOF STATE]
proof (prove)
using this:
fst (last as) = fst (last bs)
snd (last as) = snd (last bs)

goal (1 subgoal):
 1. last as = last bs
[PROOF STEP]
by (cases "last as",cases "last bs") simp
[PROOF STATE]
proof (state)
this:
last as = last bs

goal (1 subgoal):
 1. as = tl bs
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
last as = last bs

goal (1 subgoal):
 1. as = tl bs
[PROOF STEP]
from not_Nil
[PROOF STATE]
proof (chain)
picking this:
bs \<noteq> []
as \<noteq> []
[PROOF STEP]
have "as = butlast as @ [last as]" "bs = butlast bs @ [last bs]"
[PROOF STATE]
proof (prove)
using this:
bs \<noteq> []
as \<noteq> []

goal (1 subgoal):
 1. as = butlast as @ [last as] &&& bs = butlast bs @ [last bs]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
as = butlast as @ [last as]
bs = butlast bs @ [last bs]

goal (1 subgoal):
 1. as = tl bs
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
last as = last bs
as = butlast as @ [last as]
bs = butlast bs @ [last bs]
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
last as = last bs
as = butlast as @ [last as]
bs = butlast bs @ [last bs]

goal (1 subgoal):
 1. as = tl bs
[PROOF STEP]
using butlast
[PROOF STATE]
proof (prove)
using this:
last as = last bs
as = butlast as @ [last as]
bs = butlast bs @ [last bs]
butlast bs = x # butlast as

goal (1 subgoal):
 1. as = tl bs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
as = tl bs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma k_steps_to_rtrancl:
  assumes steps: "\<forall>i<k. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)"
  shows "\<Gamma>\<turnstile>p 0\<rightarrow>\<^sup>* p k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> p 0 \<rightarrow>\<^sup>* p k
[PROOF STEP]
using steps
[PROOF STATE]
proof (prove)
using this:
\<forall>i<k. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)

goal (1 subgoal):
 1. \<Gamma>\<turnstile> p 0 \<rightarrow>\<^sup>* p k
[PROOF STEP]
proof (induct k)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>i<0. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i) \<Longrightarrow> \<Gamma>\<turnstile> p 0 \<rightarrow>\<^sup>* p 0
 2. \<And>k. \<lbrakk>\<forall>i<k. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i) \<Longrightarrow> \<Gamma>\<turnstile> p 0 \<rightarrow>\<^sup>* p k; \<forall>i<Suc k. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> p 0 \<rightarrow>\<^sup>* p (Suc k)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
\<forall>i<0. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)

goal (2 subgoals):
 1. \<forall>i<0. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i) \<Longrightarrow> \<Gamma>\<turnstile> p 0 \<rightarrow>\<^sup>* p 0
 2. \<And>k. \<lbrakk>\<forall>i<k. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i) \<Longrightarrow> \<Gamma>\<turnstile> p 0 \<rightarrow>\<^sup>* p k; \<forall>i<Suc k. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> p 0 \<rightarrow>\<^sup>* p (Suc k)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>i<0. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)

goal (1 subgoal):
 1. \<Gamma>\<turnstile> p 0 \<rightarrow>\<^sup>* p 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> p 0 \<rightarrow>\<^sup>* p 0

goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<forall>i<k. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i) \<Longrightarrow> \<Gamma>\<turnstile> p 0 \<rightarrow>\<^sup>* p k; \<forall>i<Suc k. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> p 0 \<rightarrow>\<^sup>* p (Suc k)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<forall>i<k. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i) \<Longrightarrow> \<Gamma>\<turnstile> p 0 \<rightarrow>\<^sup>* p k; \<forall>i<Suc k. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> p 0 \<rightarrow>\<^sup>* p (Suc k)
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
\<forall>i<k. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i) \<Longrightarrow> \<Gamma>\<turnstile> p 0 \<rightarrow>\<^sup>* p k
\<forall>i<Suc k. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)

goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<forall>i<k. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i) \<Longrightarrow> \<Gamma>\<turnstile> p 0 \<rightarrow>\<^sup>* p k; \<forall>i<Suc k. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> p 0 \<rightarrow>\<^sup>* p (Suc k)
[PROOF STEP]
have "\<forall>i<Suc k. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i<Suc k. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
\<forall>i<Suc k. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)

goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<forall>i<k. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i) \<Longrightarrow> \<Gamma>\<turnstile> p 0 \<rightarrow>\<^sup>* p k; \<forall>i<Suc k. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> p 0 \<rightarrow>\<^sup>* p (Suc k)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>i<Suc k. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
obtain
  step_le_k: "\<forall>i<k. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)" and step_k: "\<Gamma>\<turnstile> p k \<rightarrow> p (Suc k)"
[PROOF STATE]
proof (prove)
using this:
\<forall>i<Suc k. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)

goal (1 subgoal):
 1. (\<lbrakk>\<forall>i<k. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i); \<Gamma>\<turnstile> p k \<rightarrow> p (Suc k)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>i<k. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
\<Gamma>\<turnstile> p k \<rightarrow> p (Suc k)

goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<forall>i<k. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i) \<Longrightarrow> \<Gamma>\<turnstile> p 0 \<rightarrow>\<^sup>* p k; \<forall>i<Suc k. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> p 0 \<rightarrow>\<^sup>* p (Suc k)
[PROOF STEP]
from Suc.hyps [OF step_le_k]
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> p 0 \<rightarrow>\<^sup>* p k
[PROOF STEP]
have "\<Gamma>\<turnstile> p 0 \<rightarrow>\<^sup>* p k"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> p 0 \<rightarrow>\<^sup>* p k

goal (1 subgoal):
 1. \<Gamma>\<turnstile> p 0 \<rightarrow>\<^sup>* p k
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> p 0 \<rightarrow>\<^sup>* p k

goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<forall>i<k. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i) \<Longrightarrow> \<Gamma>\<turnstile> p 0 \<rightarrow>\<^sup>* p k; \<forall>i<Suc k. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> p 0 \<rightarrow>\<^sup>* p (Suc k)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> p 0 \<rightarrow>\<^sup>* p k

goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<forall>i<k. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i) \<Longrightarrow> \<Gamma>\<turnstile> p 0 \<rightarrow>\<^sup>* p k; \<forall>i<Suc k. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> p 0 \<rightarrow>\<^sup>* p (Suc k)
[PROOF STEP]
note step_k
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> p k \<rightarrow> p (Suc k)

goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<forall>i<k. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i) \<Longrightarrow> \<Gamma>\<turnstile> p 0 \<rightarrow>\<^sup>* p k; \<forall>i<Suc k. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> p 0 \<rightarrow>\<^sup>* p (Suc k)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> p 0 \<rightarrow>\<^sup>* p (Suc k)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> p 0 \<rightarrow>\<^sup>* p (Suc k)

goal (1 subgoal):
 1. \<Gamma>\<turnstile> p 0 \<rightarrow>\<^sup>* p (Suc k)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> p 0 \<rightarrow>\<^sup>* p (Suc k)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in inf) steps_hd_drop_suffix_finite:
assumes f_0: "f 0 = (c#cs,css,s)"
assumes f_step: "\<forall>i. \<Gamma>\<turnstile> f(i) \<rightarrow> f(Suc i)"
assumes not_finished: "\<forall>i < k. \<not> (CS (f i) = cs \<and> CSS (f i) = css)"
assumes simul: "\<forall>i\<le>k.
        (if pcss i = [] then CSS (f i)=css \<and> CS (f i)=pcs i@cs
                 else CS (f i)=pcs i \<and>
                      CSS (f i)= butlast (pcss i)@
                              [(fst (last (pcss i))@cs,(snd (last (pcss i)))@cs)]@
                              css)"
shows "\<Gamma>\<turnstile>([c],[],s) \<rightarrow>\<^sup>* (pcs k, pcss k, S (f k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> ([c], [], s) \<rightarrow>\<^sup>* (pcs k, pcss k, S (f k))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> ([c], [], s) \<rightarrow>\<^sup>* (pcs k, pcss k, S (f k))
[PROOF STEP]
from steps_hd_drop_suffix [OF f_0 f_step not_finished simul]
[PROOF STATE]
proof (chain)
picking this:
\<forall>i<k. \<Gamma>\<turnstile> (pcs i, pcss i, S (f i)) \<rightarrow> (pcs (Suc i), pcss (Suc i), S (f (Suc i)))
[PROOF STEP]
have "\<forall>i<k. \<Gamma>\<turnstile> (pcs i, pcss i, S (f i)) \<rightarrow>
                  (pcs (Suc i), pcss (Suc i), S (f (Suc i)))"
[PROOF STATE]
proof (prove)
using this:
\<forall>i<k. \<Gamma>\<turnstile> (pcs i, pcss i, S (f i)) \<rightarrow> (pcs (Suc i), pcss (Suc i), S (f (Suc i)))

goal (1 subgoal):
 1. \<forall>i<k. \<Gamma>\<turnstile> (pcs i, pcss i, S (f i)) \<rightarrow> (pcs (Suc i), pcss (Suc i), S (f (Suc i)))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<forall>i<k. \<Gamma>\<turnstile> (pcs i, pcss i, S (f i)) \<rightarrow> (pcs (Suc i), pcss (Suc i), S (f (Suc i)))

goal (1 subgoal):
 1. \<Gamma>\<turnstile> ([c], [], s) \<rightarrow>\<^sup>* (pcs k, pcss k, S (f k))
[PROOF STEP]
from k_steps_to_rtrancl [OF this]
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> (pcs 0, pcss 0, S (f 0)) \<rightarrow>\<^sup>* (pcs k, pcss k, S (f k))
[PROOF STEP]
have "\<Gamma>\<turnstile> (pcs 0, pcss 0, S (f 0)) \<rightarrow>\<^sup>* (pcs k, pcss k, S (f k))"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> (pcs 0, pcss 0, S (f 0)) \<rightarrow>\<^sup>* (pcs k, pcss k, S (f k))

goal (1 subgoal):
 1. \<Gamma>\<turnstile> (pcs 0, pcss 0, S (f 0)) \<rightarrow>\<^sup>* (pcs k, pcss k, S (f k))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (pcs 0, pcss 0, S (f 0)) \<rightarrow>\<^sup>* (pcs k, pcss k, S (f k))

goal (1 subgoal):
 1. \<Gamma>\<turnstile> ([c], [], s) \<rightarrow>\<^sup>* (pcs k, pcss k, S (f k))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (pcs 0, pcss 0, S (f 0)) \<rightarrow>\<^sup>* (pcs k, pcss k, S (f k))

goal (1 subgoal):
 1. \<Gamma>\<turnstile> ([c], [], s) \<rightarrow>\<^sup>* (pcs k, pcss k, S (f k))
[PROOF STEP]
from f_0 simul [rule_format, of 0]
[PROOF STATE]
proof (chain)
picking this:
f 0 = (c # cs, css, s)
0 \<le> k \<Longrightarrow> if pcss 0 = [] then CSS (f 0) = css \<and> CS (f 0) = pcs 0 @ cs else CS (f 0) = pcs 0 \<and> CSS (f 0) = butlast (pcss 0) @ [(fst (last (pcss 0)) @ cs, snd (last (pcss 0)) @ cs)] @ css
[PROOF STEP]
have "(pcs 0, pcss 0, S (f 0)) = ([c],[],s)"
[PROOF STATE]
proof (prove)
using this:
f 0 = (c # cs, css, s)
0 \<le> k \<Longrightarrow> if pcss 0 = [] then CSS (f 0) = css \<and> CS (f 0) = pcs 0 @ cs else CS (f 0) = pcs 0 \<and> CSS (f 0) = butlast (pcss 0) @ [(fst (last (pcss 0)) @ cs, snd (last (pcss 0)) @ cs)] @ css

goal (1 subgoal):
 1. (pcs 0, pcss 0, S (f 0)) = ([c], [], s)
[PROOF STEP]
by (auto split: if_split_asm simp add: CS_def CSS_def S_def)
[PROOF STATE]
proof (state)
this:
(pcs 0, pcss 0, S (f 0)) = ([c], [], s)

goal (1 subgoal):
 1. \<Gamma>\<turnstile> ([c], [], s) \<rightarrow>\<^sup>* (pcs k, pcss k, S (f k))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> (pcs 0, pcss 0, S (f 0)) \<rightarrow>\<^sup>* (pcs k, pcss k, S (f k))
(pcs 0, pcss 0, S (f 0)) = ([c], [], s)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> (pcs 0, pcss 0, S (f 0)) \<rightarrow>\<^sup>* (pcs k, pcss k, S (f k))
(pcs 0, pcss 0, S (f 0)) = ([c], [], s)

goal (1 subgoal):
 1. \<Gamma>\<turnstile> ([c], [], s) \<rightarrow>\<^sup>* (pcs k, pcss k, S (f k))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> ([c], [], s) \<rightarrow>\<^sup>* (pcs k, pcss k, S (f k))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in inf) steps_hd_drop_suffix_infinite:
assumes f_0: "f 0 = (c#cs,css,s)"
assumes f_step: "\<forall>i. \<Gamma>\<turnstile> f(i) \<rightarrow> f(Suc i)"
assumes not_finished: "\<forall>i. \<not> (CS (f i) = cs \<and> CSS (f i) = css)"
(*assumes not_finished: "\<forall>i. \<not> (pcs i = [] \<and> pcss i = [])"*)
assumes simul: "\<forall>i.
        (if pcss i = [] then CSS (f i)=css \<and> CS (f i)=pcs i@cs
                 else CS (f i)=pcs i \<and>
                      CSS (f i)= butlast (pcss i)@
                              [(fst (last (pcss i))@cs,(snd (last (pcss i)))@cs)]@
                              css)"
defines "p\<equiv>\<lambda>i. (pcs i, pcss i, S (f i))"
shows "\<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
from steps_hd_drop_suffix [OF f_0 f_step, of "Suc i" pcss pcs] not_finished simul
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<forall>ia<Suc i. \<not> (CS (f ia) = cs \<and> CSS (f ia) = css); \<forall>ia\<le>Suc i. if pcss ia = [] then CSS (f ia) = css \<and> CS (f ia) = pcs ia @ cs else CS (f ia) = pcs ia \<and> CSS (f ia) = butlast (pcss ia) @ [(fst (last (pcss ia)) @ cs, snd (last (pcss ia)) @ cs)] @ css\<rbrakk> \<Longrightarrow> \<forall>ia<Suc i. \<Gamma>\<turnstile> (pcs ia, pcss ia, S (f ia)) \<rightarrow> (pcs (Suc ia), pcss (Suc ia), S (f (Suc ia)))
\<forall>i. \<not> (CS (f i) = cs \<and> CSS (f i) = css)
\<forall>i. if pcss i = [] then CSS (f i) = css \<and> CS (f i) = pcs i @ cs else CS (f i) = pcs i \<and> CSS (f i) = butlast (pcss i) @ [(fst (last (pcss i)) @ cs, snd (last (pcss i)) @ cs)] @ css
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<forall>ia<Suc i. \<not> (CS (f ia) = cs \<and> CSS (f ia) = css); \<forall>ia\<le>Suc i. if pcss ia = [] then CSS (f ia) = css \<and> CS (f ia) = pcs ia @ cs else CS (f ia) = pcs ia \<and> CSS (f ia) = butlast (pcss ia) @ [(fst (last (pcss ia)) @ cs, snd (last (pcss ia)) @ cs)] @ css\<rbrakk> \<Longrightarrow> \<forall>ia<Suc i. \<Gamma>\<turnstile> (pcs ia, pcss ia, S (f ia)) \<rightarrow> (pcs (Suc ia), pcss (Suc ia), S (f (Suc ia)))
\<forall>i. \<not> (CS (f i) = cs \<and> CSS (f i) = css)
\<forall>i. if pcss i = [] then CSS (f i) = css \<and> CS (f i) = pcs i @ cs else CS (f i) = pcs i \<and> CSS (f i) = butlast (pcss i) @ [(fst (last (pcss i)) @ cs, snd (last (pcss i)) @ cs)] @ css

goal (1 subgoal):
 1. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
by (auto simp add: p_def)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)

goal:
No subgoals!
[PROOF STEP]
qed