[STATEMENT]
lemma (in inf) steps_hd_progress:
assumes f_0: "f 0 = (c#cs,css,s)"
assumes f_step: "\<forall>i. \<Gamma>\<turnstile> f(i) \<rightarrow> f(Suc i)"
assumes c_unfinished: "\<forall>i < k. \<not> (CS (f i) = cs \<and> CSS (f i) = css)"
shows "\<forall>i \<le> k. (\<exists>pcs pcss.
          (if pcss = [] then CSS (f i)=css \<and> CS (f i)=pcs@cs
           else CS (f i)=pcs  \<and>
                CSS (f i)= butlast pcss@
                           [(fst (last pcss)@cs,(snd (last pcss))@cs)]@
                           css))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i\<le>k. \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
using c_unfinished
[PROOF STATE]
proof (prove)
using this:
\<forall>i<k. \<not> (CS (f i) = cs \<and> CSS (f i) = css)

goal (1 subgoal):
 1. \<forall>i\<le>k. \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
proof (induct k)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>i<0. \<not> (CS (f i) = cs \<and> CSS (f i) = css) \<Longrightarrow> \<forall>i\<le>0. \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
 2. \<And>k. \<lbrakk>\<forall>i<k. \<not> (CS (f i) = cs \<and> CSS (f i) = css) \<Longrightarrow> \<forall>i\<le>k. \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css; \<forall>i<Suc k. \<not> (CS (f i) = cs \<and> CSS (f i) = css)\<rbrakk> \<Longrightarrow> \<forall>i\<le>Suc k. \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
\<forall>i<0. \<not> (CS (f i) = cs \<and> CSS (f i) = css)

goal (2 subgoals):
 1. \<forall>i<0. \<not> (CS (f i) = cs \<and> CSS (f i) = css) \<Longrightarrow> \<forall>i\<le>0. \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
 2. \<And>k. \<lbrakk>\<forall>i<k. \<not> (CS (f i) = cs \<and> CSS (f i) = css) \<Longrightarrow> \<forall>i\<le>k. \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css; \<forall>i<Suc k. \<not> (CS (f i) = cs \<and> CSS (f i) = css)\<rbrakk> \<Longrightarrow> \<forall>i\<le>Suc k. \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
with f_0
[PROOF STATE]
proof (chain)
picking this:
f 0 = (c # cs, css, s)
\<forall>i<0. \<not> (CS (f i) = cs \<and> CSS (f i) = css)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
f 0 = (c # cs, css, s)
\<forall>i<0. \<not> (CS (f i) = cs \<and> CSS (f i) = css)

goal (1 subgoal):
 1. \<forall>i\<le>0. \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
by (simp add: CSS_def CS_def)
[PROOF STATE]
proof (state)
this:
\<forall>i\<le>0. \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css

goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<forall>i<k. \<not> (CS (f i) = cs \<and> CSS (f i) = css) \<Longrightarrow> \<forall>i\<le>k. \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css; \<forall>i<Suc k. \<not> (CS (f i) = cs \<and> CSS (f i) = css)\<rbrakk> \<Longrightarrow> \<forall>i\<le>Suc k. \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<forall>i<k. \<not> (CS (f i) = cs \<and> CSS (f i) = css) \<Longrightarrow> \<forall>i\<le>k. \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css; \<forall>i<Suc k. \<not> (CS (f i) = cs \<and> CSS (f i) = css)\<rbrakk> \<Longrightarrow> \<forall>i\<le>Suc k. \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
\<forall>i<k. \<not> (CS (f i) = cs \<and> CSS (f i) = css) \<Longrightarrow> \<forall>i\<le>k. \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
\<forall>i<Suc k. \<not> (CS (f i) = cs \<and> CSS (f i) = css)

goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<forall>i<k. \<not> (CS (f i) = cs \<and> CSS (f i) = css) \<Longrightarrow> \<forall>i\<le>k. \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css; \<forall>i<Suc k. \<not> (CS (f i) = cs \<and> CSS (f i) = css)\<rbrakk> \<Longrightarrow> \<forall>i\<le>Suc k. \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
have c_unfinished: "\<forall>i<Suc k. \<not> (CS (f i) = cs \<and> CSS (f i) = css)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i<Suc k. \<not> (CS (f i) = cs \<and> CSS (f i) = css)
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
\<forall>i<Suc k. \<not> (CS (f i) = cs \<and> CSS (f i) = css)

goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<forall>i<k. \<not> (CS (f i) = cs \<and> CSS (f i) = css) \<Longrightarrow> \<forall>i\<le>k. \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css; \<forall>i<Suc k. \<not> (CS (f i) = cs \<and> CSS (f i) = css)\<rbrakk> \<Longrightarrow> \<forall>i\<le>Suc k. \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
hence c_unfinished': "\<forall>i< k. \<not> (CS (f i) = cs \<and> CSS (f i) = css)"
[PROOF STATE]
proof (prove)
using this:
\<forall>i<Suc k. \<not> (CS (f i) = cs \<and> CSS (f i) = css)

goal (1 subgoal):
 1. \<forall>i<k. \<not> (CS (f i) = cs \<and> CSS (f i) = css)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>i<k. \<not> (CS (f i) = cs \<and> CSS (f i) = css)

goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<forall>i<k. \<not> (CS (f i) = cs \<and> CSS (f i) = css) \<Longrightarrow> \<forall>i\<le>k. \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css; \<forall>i<Suc k. \<not> (CS (f i) = cs \<and> CSS (f i) = css)\<rbrakk> \<Longrightarrow> \<forall>i\<le>Suc k. \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i\<le>Suc k. \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
proof (clarify)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i \<le> Suc k \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i \<le> Suc k \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
assume i_le_Suc_k: "i \<le> Suc k"
[PROOF STATE]
proof (state)
this:
i \<le> Suc k

goal (1 subgoal):
 1. \<And>i. i \<le> Suc k \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
show "\<exists>pcs pcss.
          (if pcss = [] then CSS (f i)=css \<and> CS (f i)=pcs@cs
           else CS (f i)=pcs  \<and>
                CSS (f i)= butlast pcss@
                           [(fst (last pcss)@cs,(snd (last pcss))@cs)]@
                           css)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
proof (cases "i < Suc k")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i < Suc k \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
 2. \<not> i < Suc k \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
i < Suc k

goal (2 subgoals):
 1. i < Suc k \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
 2. \<not> i < Suc k \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
with Suc.hyps [OF c_unfinished', rule_format, of i] c_unfinished
[PROOF STATE]
proof (chain)
picking this:
i \<le> k \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
\<forall>i<Suc k. \<not> (CS (f i) = cs \<and> CSS (f i) = css)
i < Suc k
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i \<le> k \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
\<forall>i<Suc k. \<not> (CS (f i) = cs \<and> CSS (f i) = css)
i < Suc k

goal (1 subgoal):
 1. \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css

goal (1 subgoal):
 1. \<not> i < Suc k \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> i < Suc k \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> i < Suc k

goal (1 subgoal):
 1. \<not> i < Suc k \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
with i_le_Suc_k
[PROOF STATE]
proof (chain)
picking this:
i \<le> Suc k
\<not> i < Suc k
[PROOF STEP]
have eq_i_Suc_k: "i=Suc k"
[PROOF STATE]
proof (prove)
using this:
i \<le> Suc k
\<not> i < Suc k

goal (1 subgoal):
 1. i = Suc k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i = Suc k

goal (1 subgoal):
 1. \<not> i < Suc k \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
obtain cs' css' t' where
        f_Suc_k: "f (Suc k) = (cs', css', t')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>cs' css' t'. f (Suc k) = (cs', css', t') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases "f (Suc k)")
[PROOF STATE]
proof (state)
this:
f (Suc k) = (cs', css', t')

goal (1 subgoal):
 1. \<not> i < Suc k \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
obtain cs'' css'' t'' where
        f_k: "f k = (cs'',css'',t'')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>cs'' css'' t''. f k = (cs'', css'', t'') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases "f k")
[PROOF STATE]
proof (state)
this:
f k = (cs'', css'', t'')

goal (1 subgoal):
 1. \<not> i < Suc k \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
with Suc.hyps [OF c_unfinished',rule_format, of k]
[PROOF STATE]
proof (chain)
picking this:
k \<le> k \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f k) = css \<and> CS (f k) = pcs @ cs else CS (f k) = pcs \<and> CSS (f k) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
f k = (cs'', css'', t'')
[PROOF STEP]
obtain pcs pcss where
        pcs_pcss_k:
        "if pcss = [] then css'' = css \<and> cs'' = pcs @ cs
         else cs'' = pcs \<and>
              css'' = butlast pcss @
                           [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @
                           css"
[PROOF STATE]
proof (prove)
using this:
k \<le> k \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f k) = css \<and> CS (f k) = pcs @ cs else CS (f k) = pcs \<and> CSS (f k) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
f k = (cs'', css'', t'')

goal (1 subgoal):
 1. (\<And>pcss pcs. if pcss = [] then css'' = css \<and> cs'' = pcs @ cs else cs'' = pcs \<and> css'' = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: CSS_def CS_def cong: if_cong)
[PROOF STATE]
proof (state)
this:
if pcss = [] then css'' = css \<and> cs'' = pcs @ cs else cs'' = pcs \<and> css'' = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css

goal (1 subgoal):
 1. \<not> i < Suc k \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
from c_unfinished [rule_format, of k] f_k pcs_pcss_k
[PROOF STATE]
proof (chain)
picking this:
k < Suc k \<Longrightarrow> \<not> (CS (f k) = cs \<and> CSS (f k) = css)
f k = (cs'', css'', t'')
if pcss = [] then css'' = css \<and> cs'' = pcs @ cs else cs'' = pcs \<and> css'' = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
have pcs_pcss_empty: "\<not> (pcs = [] \<and> pcss = [])"
[PROOF STATE]
proof (prove)
using this:
k < Suc k \<Longrightarrow> \<not> (CS (f k) = cs \<and> CSS (f k) = css)
f k = (cs'', css'', t'')
if pcss = [] then css'' = css \<and> cs'' = pcs @ cs else cs'' = pcs \<and> css'' = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css

goal (1 subgoal):
 1. \<not> (pcs = [] \<and> pcss = [])
[PROOF STEP]
by (auto simp add: CS_def CSS_def S_def split: if_split_asm)
[PROOF STATE]
proof (state)
this:
\<not> (pcs = [] \<and> pcss = [])

goal (1 subgoal):
 1. \<not> i < Suc k \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
proof (cases "pcss = []")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. pcss = [] \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
 2. pcss \<noteq> [] \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
pcss = []

goal (2 subgoals):
 1. pcss = [] \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
 2. pcss \<noteq> [] \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
note pcss_Nil = this
[PROOF STATE]
proof (state)
this:
pcss = []

goal (2 subgoals):
 1. pcss = [] \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
 2. pcss \<noteq> [] \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
with pcs_pcss_k pcs_pcss_empty
[PROOF STATE]
proof (chain)
picking this:
if pcss = [] then css'' = css \<and> cs'' = pcs @ cs else cs'' = pcs \<and> css'' = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
\<not> (pcs = [] \<and> pcss = [])
pcss = []
[PROOF STEP]
obtain p ps where
          pcs_i: "pcs = p#ps" and
          css'': "css''=css" and
          cs'': "cs''=(p#ps)@cs"
[PROOF STATE]
proof (prove)
using this:
if pcss = [] then css'' = css \<and> cs'' = pcs @ cs else cs'' = pcs \<and> css'' = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
\<not> (pcs = [] \<and> pcss = [])
pcss = []

goal (1 subgoal):
 1. (\<And>p ps. \<lbrakk>pcs = p # ps; css'' = css; cs'' = (p # ps) @ cs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases "pcs") auto
[PROOF STATE]
proof (state)
this:
pcs = p # ps
css'' = css
cs'' = (p # ps) @ cs

goal (2 subgoals):
 1. pcss = [] \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
 2. pcss \<noteq> [] \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
with f_k
[PROOF STATE]
proof (chain)
picking this:
f k = (cs'', css'', t'')
pcs = p # ps
css'' = css
cs'' = (p # ps) @ cs
[PROOF STEP]
have "f k = (p#(ps@cs),css,t'')"
[PROOF STATE]
proof (prove)
using this:
f k = (cs'', css'', t'')
pcs = p # ps
css'' = css
cs'' = (p # ps) @ cs

goal (1 subgoal):
 1. f k = (p # ps @ cs, css, t'')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f k = (p # ps @ cs, css, t'')

goal (2 subgoals):
 1. pcss = [] \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
 2. pcss \<noteq> [] \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
with f_Suc_k f_step [rule_format, of k]
[PROOF STATE]
proof (chain)
picking this:
f (Suc k) = (cs', css', t')
\<Gamma>\<turnstile> f k \<rightarrow> f (Suc k)
f k = (p # ps @ cs, css, t'')
[PROOF STEP]
have step_css: "\<Gamma>\<turnstile> (p#(ps@cs),css,t'') \<rightarrow> (cs',css',t')"
[PROOF STATE]
proof (prove)
using this:
f (Suc k) = (cs', css', t')
\<Gamma>\<turnstile> f k \<rightarrow> f (Suc k)
f k = (p # ps @ cs, css, t'')

goal (1 subgoal):
 1. \<Gamma>\<turnstile> (p # ps @ cs, css, t'') \<rightarrow> (cs', css', t')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (p # ps @ cs, css, t'') \<rightarrow> (cs', css', t')

goal (2 subgoals):
 1. pcss = [] \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
 2. pcss \<noteq> [] \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
from step_Cons' [OF this, of p "ps@cs"]
[PROOF STATE]
proof (chain)
picking this:
p # ps @ cs = p # ps @ cs \<Longrightarrow> \<exists>css''. css' = css'' @ css \<and> (if css'' = [] then \<exists>p. cs' = p @ ps @ cs else \<exists>pnorm pabr. css'' = [(pnorm @ ps @ cs, pabr @ ps @ cs)])
[PROOF STEP]
obtain css''' where
          css''': "css' = css''' @ css"
          "if css''' = [] then \<exists>p. cs' = p @ ps @ cs
          else (\<exists>pnorm pabr. css'''=[(pnorm @ ps @ cs,pabr @ ps @ cs)])"
[PROOF STATE]
proof (prove)
using this:
p # ps @ cs = p # ps @ cs \<Longrightarrow> \<exists>css''. css' = css'' @ css \<and> (if css'' = [] then \<exists>p. cs' = p @ ps @ cs else \<exists>pnorm pabr. css'' = [(pnorm @ ps @ cs, pabr @ ps @ cs)])

goal (1 subgoal):
 1. (\<And>css'''. \<lbrakk>css' = css''' @ css; if css''' = [] then \<exists>p. cs' = p @ ps @ cs else \<exists>pnorm pabr. css''' = [(pnorm @ ps @ cs, pabr @ ps @ cs)]\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
css' = css''' @ css
if css''' = [] then \<exists>p. cs' = p @ ps @ cs else \<exists>pnorm pabr. css''' = [(pnorm @ ps @ cs, pabr @ ps @ cs)]

goal (2 subgoals):
 1. pcss = [] \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
 2. pcss \<noteq> [] \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
proof (cases "css''' = []")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. css''' = [] \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
 2. css''' \<noteq> [] \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
css''' = []

goal (2 subgoals):
 1. css''' = [] \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
 2. css''' \<noteq> [] \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
with css'''
[PROOF STATE]
proof (chain)
picking this:
css' = css''' @ css
if css''' = [] then \<exists>p. cs' = p @ ps @ cs else \<exists>pnorm pabr. css''' = [(pnorm @ ps @ cs, pabr @ ps @ cs)]
css''' = []
[PROOF STEP]
obtain p' where
            css': "css' = css" and
            cs': "cs' = p' @ ps @ cs"
[PROOF STATE]
proof (prove)
using this:
css' = css''' @ css
if css''' = [] then \<exists>p. cs' = p @ ps @ cs else \<exists>pnorm pabr. css''' = [(pnorm @ ps @ cs, pabr @ ps @ cs)]
css''' = []

goal (1 subgoal):
 1. (\<And>p'. \<lbrakk>css' = css; cs' = p' @ ps @ cs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
css' = css
cs' = p' @ ps @ cs

goal (2 subgoals):
 1. css''' = [] \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
 2. css''' \<noteq> [] \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
from css' cs' f_Suc_k
[PROOF STATE]
proof (chain)
picking this:
css' = css
cs' = p' @ ps @ cs
f (Suc k) = (cs', css', t')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
css' = css
cs' = p' @ ps @ cs
f (Suc k) = (cs', css', t')

goal (1 subgoal):
 1. \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
apply (rule_tac x="p'@ps" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>css' = css; cs' = p' @ ps @ cs; f (Suc k) = (cs', css', t')\<rbrakk> \<Longrightarrow> \<exists>pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = (p' @ ps) @ cs else CS (f i) = p' @ ps \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
apply (rule_tac x="[]" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>css' = css; cs' = p' @ ps @ cs; f (Suc k) = (cs', css', t')\<rbrakk> \<Longrightarrow> if [] = [] then CSS (f i) = css \<and> CS (f i) = (p' @ ps) @ cs else CS (f i) = p' @ ps \<and> CSS (f i) = butlast [] @ [(fst (last []) @ cs, snd (last []) @ cs)] @ css
[PROOF STEP]
apply (simp add: CSS_def CS_def eq_i_Suc_k)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css

goal (1 subgoal):
 1. css''' \<noteq> [] \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. css''' \<noteq> [] \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
css''' \<noteq> []

goal (1 subgoal):
 1. css''' \<noteq> [] \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
with css'''
[PROOF STATE]
proof (chain)
picking this:
css' = css''' @ css
if css''' = [] then \<exists>p. cs' = p @ ps @ cs else \<exists>pnorm pabr. css''' = [(pnorm @ ps @ cs, pabr @ ps @ cs)]
css''' \<noteq> []
[PROOF STEP]
obtain pnorm pabr where
            css': "css'=css'''@css"
            "css'''=[(pnorm @ ps @ cs,pabr @ ps @ cs)]"
[PROOF STATE]
proof (prove)
using this:
css' = css''' @ css
if css''' = [] then \<exists>p. cs' = p @ ps @ cs else \<exists>pnorm pabr. css''' = [(pnorm @ ps @ cs, pabr @ ps @ cs)]
css''' \<noteq> []

goal (1 subgoal):
 1. (\<And>pnorm pabr. \<lbrakk>css' = css''' @ css; css''' = [(pnorm @ ps @ cs, pabr @ ps @ cs)]\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
css' = css''' @ css
css''' = [(pnorm @ ps @ cs, pabr @ ps @ cs)]

goal (1 subgoal):
 1. css''' \<noteq> [] \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
with f_Suc_k eq_i_Suc_k
[PROOF STATE]
proof (chain)
picking this:
f (Suc k) = (cs', css', t')
i = Suc k
css' = css''' @ css
css''' = [(pnorm @ ps @ cs, pabr @ ps @ cs)]
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f (Suc k) = (cs', css', t')
i = Suc k
css' = css''' @ css
css''' = [(pnorm @ ps @ cs, pabr @ ps @ cs)]

goal (1 subgoal):
 1. \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
apply (rule_tac x="cs'" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f (Suc k) = (cs', css', t'); i = Suc k; css' = css''' @ css; css''' = [(pnorm @ ps @ cs, pabr @ ps @ cs)]\<rbrakk> \<Longrightarrow> \<exists>pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = cs' @ cs else CS (f i) = cs' \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
apply (rule_tac x="[(pnorm@ps, pabr@ps)]" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f (Suc k) = (cs', css', t'); i = Suc k; css' = css''' @ css; css''' = [(pnorm @ ps @ cs, pabr @ ps @ cs)]\<rbrakk> \<Longrightarrow> if [(pnorm @ ps, pabr @ ps)] = [] then CSS (f i) = css \<and> CS (f i) = cs' @ cs else CS (f i) = cs' \<and> CSS (f i) = butlast [(pnorm @ ps, pabr @ ps)] @ [(fst (last [(pnorm @ ps, pabr @ ps)]) @ cs, snd (last [(pnorm @ ps, pabr @ ps)]) @ cs)] @ css
[PROOF STEP]
by (simp add: CSS_def CS_def)
[PROOF STATE]
proof (state)
this:
\<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css

goal (1 subgoal):
 1. pcss \<noteq> [] \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pcss \<noteq> [] \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
pcss \<noteq> []

goal (1 subgoal):
 1. pcss \<noteq> [] \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
note pcss_k_not_Nil = this
[PROOF STATE]
proof (state)
this:
pcss \<noteq> []

goal (1 subgoal):
 1. pcss \<noteq> [] \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
with pcs_pcss_k
[PROOF STATE]
proof (chain)
picking this:
if pcss = [] then css'' = css \<and> cs'' = pcs @ cs else cs'' = pcs \<and> css'' = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
pcss \<noteq> []
[PROOF STEP]
obtain
          cs'': "cs''=pcs" and
          css'': "css''= butlast pcss@
                           [(fst (last pcss)@cs,(snd (last pcss))@cs)]@
                           css"
[PROOF STATE]
proof (prove)
using this:
if pcss = [] then css'' = css \<and> cs'' = pcs @ cs else cs'' = pcs \<and> css'' = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
pcss \<noteq> []

goal (1 subgoal):
 1. (\<lbrakk>cs'' = pcs; css'' = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cs'' = pcs
css'' = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css

goal (1 subgoal):
 1. pcss \<noteq> [] \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
from f_Suc_k f_k f_step [rule_format, of k]
[PROOF STATE]
proof (chain)
picking this:
f (Suc k) = (cs', css', t')
f k = (cs'', css'', t'')
\<Gamma>\<turnstile> f k \<rightarrow> f (Suc k)
[PROOF STEP]
have step_i_full: "\<Gamma>\<turnstile> (cs'',css'',t'') \<rightarrow> (cs',css',t')"
[PROOF STATE]
proof (prove)
using this:
f (Suc k) = (cs', css', t')
f k = (cs'', css'', t'')
\<Gamma>\<turnstile> f k \<rightarrow> f (Suc k)

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

goal (1 subgoal):
 1. pcss \<noteq> [] \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
proof (cases cs'')
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. cs'' = [] \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
 2. \<And>a list. cs'' = a # list \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
case (Cons c' cs)
[PROOF STATE]
proof (state)
this:
cs'' = c' # cs

goal (2 subgoals):
 1. cs'' = [] \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
 2. \<And>a list. cs'' = a # list \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
with step_Cons' [OF step_i_full]
[PROOF STATE]
proof (chain)
picking this:
cs'' = ?c # ?cs \<Longrightarrow> \<exists>css''a. css' = css''a @ css'' \<and> (if css''a = [] then \<exists>p. cs' = p @ ?cs else \<exists>pnorm pabr. css''a = [(pnorm @ ?cs, pabr @ ?cs)])
cs'' = c' # cs
[PROOF STEP]
obtain css''' where css': "css' = css'''@css''"
[PROOF STATE]
proof (prove)
using this:
cs'' = ?c # ?cs \<Longrightarrow> \<exists>css''a. css' = css''a @ css'' \<and> (if css''a = [] then \<exists>p. cs' = p @ ?cs else \<exists>pnorm pabr. css''a = [(pnorm @ ?cs, pabr @ ?cs)])
cs'' = c' # cs

goal (1 subgoal):
 1. (\<And>css'''. css' = css''' @ css'' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
css' = css''' @ css''

goal (2 subgoals):
 1. cs'' = [] \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
 2. \<And>a list. cs'' = a # list \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
with cs'' css'' f_Suc_k eq_i_Suc_k pcss_k_not_Nil
[PROOF STATE]
proof (chain)
picking this:
cs'' = pcs
css'' = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
f (Suc k) = (cs', css', t')
i = Suc k
pcss \<noteq> []
css' = css''' @ css''
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
cs'' = pcs
css'' = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
f (Suc k) = (cs', css', t')
i = Suc k
pcss \<noteq> []
css' = css''' @ css''

goal (1 subgoal):
 1. \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
apply (rule_tac x="cs'" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cs'' = pcs; css'' = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css; f (Suc k) = (cs', css', t'); i = Suc k; pcss \<noteq> []; css' = css''' @ css''\<rbrakk> \<Longrightarrow> \<exists>pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = cs' @ cs else CS (f i) = cs' \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
apply (rule_tac x="css'''@pcss" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cs'' = pcs; css'' = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css; f (Suc k) = (cs', css', t'); i = Suc k; pcss \<noteq> []; css' = css''' @ css''\<rbrakk> \<Longrightarrow> if css''' @ pcss = [] then CSS (f i) = css \<and> CS (f i) = cs' @ cs else CS (f i) = cs' \<and> CSS (f i) = butlast (css''' @ pcss) @ [(fst (last (css''' @ pcss)) @ cs, snd (last (css''' @ pcss)) @ cs)] @ css
[PROOF STEP]
by (clarsimp simp add: CSS_def CS_def butlast_append)
[PROOF STATE]
proof (state)
this:
\<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css

goal (1 subgoal):
 1. cs'' = [] \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cs'' = [] \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
cs'' = []

goal (1 subgoal):
 1. cs'' = [] \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
note cs''_Nil = this
[PROOF STATE]
proof (state)
this:
cs'' = []

goal (1 subgoal):
 1. cs'' = [] \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
proof (cases "butlast pcss")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. butlast pcss = [] \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
 2. \<And>a list. butlast pcss = a # list \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
case (Cons bpcs bpcss)
[PROOF STATE]
proof (state)
this:
butlast pcss = bpcs # bpcss

goal (2 subgoals):
 1. butlast pcss = [] \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
 2. \<And>a list. butlast pcss = a # list \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
with cs''_Nil step_i_full css''
[PROOF STATE]
proof (chain)
picking this:
cs'' = []
\<Gamma>\<turnstile> (cs'', css'', t'') \<rightarrow> (cs', css', t')
css'' = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
butlast pcss = bpcs # bpcss
[PROOF STEP]
have *: "\<Gamma>\<turnstile> ([],[hd css'']@tl css'',t'') \<rightarrow> (cs',css',t')"
[PROOF STATE]
proof (prove)
using this:
cs'' = []
\<Gamma>\<turnstile> (cs'', css'', t'') \<rightarrow> (cs', css', t')
css'' = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
butlast pcss = bpcs # bpcss

goal (1 subgoal):
 1. \<Gamma>\<turnstile> ([], [hd css''] @ tl css'', t'') \<rightarrow> (cs', css', t')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> ([], [hd css''] @ tl css'', t'') \<rightarrow> (cs', css', t')

goal (2 subgoals):
 1. butlast pcss = [] \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
 2. \<And>a list. butlast pcss = a # list \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> ([], [hd css''] @ tl css'', t'') \<rightarrow> (cs', css', t')

goal (2 subgoals):
 1. butlast pcss = [] \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
 2. \<And>a list. butlast pcss = a # list \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
from step_Nil [OF *]
[PROOF STATE]
proof (chain)
picking this:
[hd css''] \<noteq> [] \<Longrightarrow> css' = tl [hd css''] @ tl css'' \<and> (case t'' of Abrupt s' \<Rightarrow> cs' = snd (hd [hd css'']) \<and> t' = Normal s' | _ \<Rightarrow> cs' = fst (hd [hd css'']) \<and> t' = t'')
[PROOF STEP]
obtain css': "css'=tl css''" and
                   cs': "cs' = (case t'' of Abrupt s' \<Rightarrow> snd (hd css'')
                                 | _ \<Rightarrow> fst (hd css''))"
[PROOF STATE]
proof (prove)
using this:
[hd css''] \<noteq> [] \<Longrightarrow> css' = tl [hd css''] @ tl css'' \<and> (case t'' of Abrupt s' \<Rightarrow> cs' = snd (hd [hd css'']) \<and> t' = Normal s' | _ \<Rightarrow> cs' = fst (hd [hd css'']) \<and> t' = t'')

goal (1 subgoal):
 1. (\<lbrakk>css' = tl css''; cs' = (case t'' of Abrupt s' \<Rightarrow> snd (hd css'') | _ \<Rightarrow> fst (hd css''))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto split: xstate.splits)
[PROOF STATE]
proof (state)
this:
css' = tl css''
cs' = (case t'' of Abrupt s' \<Rightarrow> snd (hd css'') | _ \<Rightarrow> fst (hd css''))

goal (2 subgoals):
 1. butlast pcss = [] \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
 2. \<And>a list. butlast pcss = a # list \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
from css'' Cons pcss_k_not_Nil
[PROOF STATE]
proof (chain)
picking this:
css'' = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
butlast pcss = bpcs # bpcss
pcss \<noteq> []
[PROOF STEP]
have "hd css'' = hd pcss"
[PROOF STATE]
proof (prove)
using this:
css'' = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
butlast pcss = bpcs # bpcss
pcss \<noteq> []

goal (1 subgoal):
 1. hd css'' = hd pcss
[PROOF STEP]
by (auto simp add: neq_Nil_conv split: if_split_asm)
[PROOF STATE]
proof (state)
this:
hd css'' = hd pcss

goal (2 subgoals):
 1. butlast pcss = [] \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
 2. \<And>a list. butlast pcss = a # list \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
with css' cs' css'' cs''_Nil Cons pcss_k_not_Nil f_Suc_k eq_i_Suc_k
[PROOF STATE]
proof (chain)
picking this:
css' = tl css''
cs' = (case t'' of Abrupt s' \<Rightarrow> snd (hd css'') | _ \<Rightarrow> fst (hd css''))
css'' = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
cs'' = []
butlast pcss = bpcs # bpcss
pcss \<noteq> []
f (Suc k) = (cs', css', t')
i = Suc k
hd css'' = hd pcss
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
css' = tl css''
cs' = (case t'' of Abrupt s' \<Rightarrow> snd (hd css'') | _ \<Rightarrow> fst (hd css''))
css'' = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
cs'' = []
butlast pcss = bpcs # bpcss
pcss \<noteq> []
f (Suc k) = (cs', css', t')
i = Suc k
hd css'' = hd pcss

goal (1 subgoal):
 1. \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
apply (rule_tac x="cs'" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>css' = tl css''; cs' = (case t'' of Abrupt s' \<Rightarrow> snd (hd css'') | _ \<Rightarrow> fst (hd css'')); css'' = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css; cs'' = []; butlast pcss = bpcs # bpcss; pcss \<noteq> []; f (Suc k) = (cs', css', t'); i = Suc k; hd css'' = hd pcss\<rbrakk> \<Longrightarrow> \<exists>pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = cs' @ cs else CS (f i) = cs' \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
apply (rule_tac x="tl pcss" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>css' = tl css''; cs' = (case t'' of Abrupt s' \<Rightarrow> snd (hd css'') | _ \<Rightarrow> fst (hd css'')); css'' = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css; cs'' = []; butlast pcss = bpcs # bpcss; pcss \<noteq> []; f (Suc k) = (cs', css', t'); i = Suc k; hd css'' = hd pcss\<rbrakk> \<Longrightarrow> if tl pcss = [] then CSS (f i) = css \<and> CS (f i) = cs' @ cs else CS (f i) = cs' \<and> CSS (f i) = butlast (tl pcss) @ [(fst (last (tl pcss)) @ cs, snd (last (tl pcss)) @ cs)] @ css
[PROOF STEP]
apply (clarsimp split: xstate.splits
                       simp add: CS_def CSS_def neq_Nil_conv split: if_split_asm)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css

goal (1 subgoal):
 1. butlast pcss = [] \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. butlast pcss = [] \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
butlast pcss = []

goal (1 subgoal):
 1. butlast pcss = [] \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
with css'' pcss_k_not_Nil
[PROOF STATE]
proof (chain)
picking this:
css'' = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
pcss \<noteq> []
butlast pcss = []
[PROOF STEP]
obtain pnorm pabr
              where css'': "css''= [(pnorm@cs,pabr@cs)]@css" and
              pcss_k: "pcss = [(pnorm,pabr)]"
[PROOF STATE]
proof (prove)
using this:
css'' = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
pcss \<noteq> []
butlast pcss = []

goal (1 subgoal):
 1. (\<And>pnorm pabr. \<lbrakk>css'' = [(pnorm @ cs, pabr @ cs)] @ css; pcss = [(pnorm, pabr)]\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (force simp add: neq_Nil_conv split: if_split_asm)
[PROOF STATE]
proof (state)
this:
css'' = [(pnorm @ cs, pabr @ cs)] @ css
pcss = [(pnorm, pabr)]

goal (1 subgoal):
 1. butlast pcss = [] \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
with cs''_Nil step_i_full
[PROOF STATE]
proof (chain)
picking this:
cs'' = []
\<Gamma>\<turnstile> (cs'', css'', t'') \<rightarrow> (cs', css', t')
css'' = [(pnorm @ cs, pabr @ cs)] @ css
pcss = [(pnorm, pabr)]
[PROOF STEP]
have "\<Gamma>\<turnstile>([],[(pnorm@cs,pabr@cs)]@css,t'') \<rightarrow> (cs',css',t')"
[PROOF STATE]
proof (prove)
using this:
cs'' = []
\<Gamma>\<turnstile> (cs'', css'', t'') \<rightarrow> (cs', css', t')
css'' = [(pnorm @ cs, pabr @ cs)] @ css
pcss = [(pnorm, pabr)]

goal (1 subgoal):
 1. \<Gamma>\<turnstile> ([], [(pnorm @ cs, pabr @ cs)] @ css, t'') \<rightarrow> (cs', css', t')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> ([], [(pnorm @ cs, pabr @ cs)] @ css, t'') \<rightarrow> (cs', css', t')

goal (1 subgoal):
 1. butlast pcss = [] \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
from step_Nil [OF this]
[PROOF STATE]
proof (chain)
picking this:
[(pnorm @ cs, pabr @ cs)] \<noteq> [] \<Longrightarrow> css' = tl [(pnorm @ cs, pabr @ cs)] @ css \<and> (case t'' of Abrupt s' \<Rightarrow> cs' = snd (hd [(pnorm @ cs, pabr @ cs)]) \<and> t' = Normal s' | _ \<Rightarrow> cs' = fst (hd [(pnorm @ cs, pabr @ cs)]) \<and> t' = t'')
[PROOF STEP]
obtain
              css': "css'=css" and
              cs': "(case t'' of
              Abrupt s' \<Rightarrow> cs' = pabr @ cs \<and> t' = Normal s'
              | _ \<Rightarrow> cs' = pnorm @ cs \<and> t' = t'')"
[PROOF STATE]
proof (prove)
using this:
[(pnorm @ cs, pabr @ cs)] \<noteq> [] \<Longrightarrow> css' = tl [(pnorm @ cs, pabr @ cs)] @ css \<and> (case t'' of Abrupt s' \<Rightarrow> cs' = snd (hd [(pnorm @ cs, pabr @ cs)]) \<and> t' = Normal s' | _ \<Rightarrow> cs' = fst (hd [(pnorm @ cs, pabr @ cs)]) \<and> t' = t'')

goal (1 subgoal):
 1. (\<lbrakk>css' = css; case t'' of Abrupt s' \<Rightarrow> cs' = pabr @ cs \<and> t' = Normal s' | _ \<Rightarrow> cs' = pnorm @ cs \<and> t' = t''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (simp cong: xstate.case_cong)
[PROOF STATE]
proof (state)
this:
css' = css
case t'' of Abrupt s' \<Rightarrow> cs' = pabr @ cs \<and> t' = Normal s' | _ \<Rightarrow> cs' = pnorm @ cs \<and> t' = t''

goal (1 subgoal):
 1. butlast pcss = [] \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
let "?pcs_Suc_k " = "(case t'' of Abrupt s' \<Rightarrow> pabr | _ \<Rightarrow> pnorm)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. butlast pcss = [] \<Longrightarrow> \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
from css'' css' cs' pcss_k f_Suc_k eq_i_Suc_k
[PROOF STATE]
proof (chain)
picking this:
css'' = [(pnorm @ cs, pabr @ cs)] @ css
css' = css
case t'' of Abrupt s' \<Rightarrow> cs' = pabr @ cs \<and> t' = Normal s' | _ \<Rightarrow> cs' = pnorm @ cs \<and> t' = t''
pcss = [(pnorm, pabr)]
f (Suc k) = (cs', css', t')
i = Suc k
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
css'' = [(pnorm @ cs, pabr @ cs)] @ css
css' = css
case t'' of Abrupt s' \<Rightarrow> cs' = pabr @ cs \<and> t' = Normal s' | _ \<Rightarrow> cs' = pnorm @ cs \<and> t' = t''
pcss = [(pnorm, pabr)]
f (Suc k) = (cs', css', t')
i = Suc k

goal (1 subgoal):
 1. \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
apply (rule_tac x="?pcs_Suc_k" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>css'' = [(pnorm @ cs, pabr @ cs)] @ css; css' = css; case t'' of Abrupt s' \<Rightarrow> cs' = pabr @ cs \<and> t' = Normal s' | _ \<Rightarrow> cs' = pnorm @ cs \<and> t' = t''; pcss = [(pnorm, pabr)]; f (Suc k) = (cs', css', t'); i = Suc k\<rbrakk> \<Longrightarrow> \<exists>pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = (case t'' of Abrupt s' \<Rightarrow> pabr | _ \<Rightarrow> pnorm) @ cs else CS (f i) = (case t'' of Abrupt s' \<Rightarrow> pabr | _ \<Rightarrow> pnorm) \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
apply (rule_tac x="[]" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>css'' = [(pnorm @ cs, pabr @ cs)] @ css; css' = css; case t'' of Abrupt s' \<Rightarrow> cs' = pabr @ cs \<and> t' = Normal s' | _ \<Rightarrow> cs' = pnorm @ cs \<and> t' = t''; pcss = [(pnorm, pabr)]; f (Suc k) = (cs', css', t'); i = Suc k\<rbrakk> \<Longrightarrow> if [] = [] then CSS (f i) = css \<and> CS (f i) = (case t'' of Abrupt s' \<Rightarrow> pabr | _ \<Rightarrow> pnorm) @ cs else CS (f i) = (case t'' of Abrupt s' \<Rightarrow> pabr | _ \<Rightarrow> pnorm) \<and> CSS (f i) = butlast [] @ [(fst (last []) @ cs, snd (last []) @ cs)] @ css
[PROOF STEP]
apply (simp split: xstate.splits add: CS_def CSS_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>i\<le>Suc k. \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css

goal:
No subgoals!
[PROOF STEP]
qed


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

goal (1 subgoal):
 1. \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma skolemize1: "\<forall>x. P x \<longrightarrow> (\<exists>y. Q x y) \<Longrightarrow> \<exists>f.\<forall>x. P x \<longrightarrow> Q x (f x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. P x \<longrightarrow> (\<exists>y. Q x y) \<Longrightarrow> \<exists>f. \<forall>x. P x \<longrightarrow> Q x (f x)
[PROOF STEP]
by (rule choice) blast


[STATEMENT]
lemma skolemize2: "\<forall>x. P x \<longrightarrow> (\<exists>y z. Q x y z) \<Longrightarrow> \<exists>f g.\<forall>x. P x \<longrightarrow> Q x (f x) (g x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. P x \<longrightarrow> (\<exists>y z. Q x y z) \<Longrightarrow> \<exists>f g. \<forall>x. P x \<longrightarrow> Q x (f x) (g x)
[PROOF STEP]
apply (drule skolemize1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>f. \<forall>x. P x \<longrightarrow> (\<exists>z. Q x (f x) z) \<Longrightarrow> \<exists>f g. \<forall>x. P x \<longrightarrow> Q x (f x) (g x)
[PROOF STEP]
apply (erule exE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f. \<forall>x. P x \<longrightarrow> (\<exists>z. Q x (f x) z) \<Longrightarrow> \<exists>f g. \<forall>x. P x \<longrightarrow> Q x (f x) (g x)
[PROOF STEP]
apply (drule skolemize1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f. \<exists>fa. \<forall>x. P x \<longrightarrow> Q x (f x) (fa x) \<Longrightarrow> \<exists>f g. \<forall>x. P x \<longrightarrow> Q x (f x) (g x)
[PROOF STEP]
apply fast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
theorem (in inf) inf_cases:
  fixes c::"('s,'p,'f) com"
  assumes inf: "inf \<Gamma> (c#cs) css s"
  shows "inf \<Gamma> [c] [] s \<or> (\<exists>t. \<Gamma>\<turnstile>\<langle>c,s\<rangle> \<Rightarrow> t \<and> inf \<Gamma> cs css t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AlternativeSmallStep.inf \<Gamma> [c] [] s \<or> (\<exists>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<and> AlternativeSmallStep.inf \<Gamma> cs css t)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. AlternativeSmallStep.inf \<Gamma> [c] [] s \<or> (\<exists>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<and> AlternativeSmallStep.inf \<Gamma> cs css t)
[PROOF STEP]
from inf
[PROOF STATE]
proof (chain)
picking this:
AlternativeSmallStep.inf \<Gamma> (c # cs) css s
[PROOF STEP]
obtain f where
    f_0: "f 0 = (c#cs,css,s)" and
    f_step: "(\<forall>i. \<Gamma>\<turnstile>f i \<rightarrow> f (Suc i))"
[PROOF STATE]
proof (prove)
using this:
AlternativeSmallStep.inf \<Gamma> (c # cs) css s

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f 0 = (c # cs, css, s); \<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: inf_def)
[PROOF STATE]
proof (state)
this:
f 0 = (c # cs, css, s)
\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)

goal (1 subgoal):
 1. AlternativeSmallStep.inf \<Gamma> [c] [] s \<or> (\<exists>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<and> AlternativeSmallStep.inf \<Gamma> cs css t)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AlternativeSmallStep.inf \<Gamma> [c] [] s \<or> (\<exists>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<and> AlternativeSmallStep.inf \<Gamma> cs css t)
[PROOF STEP]
proof (cases "\<exists>i. CS (f i) = cs \<and> CSS (f i) = css")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>i. CS (f i) = cs \<and> CSS (f i) = css \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> [c] [] s \<or> (\<exists>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<and> AlternativeSmallStep.inf \<Gamma> cs css t)
 2. \<nexists>i. CS (f i) = cs \<and> CSS (f i) = css \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> [c] [] s \<or> (\<exists>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<and> AlternativeSmallStep.inf \<Gamma> cs css t)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<exists>i. CS (f i) = cs \<and> CSS (f i) = css

goal (2 subgoals):
 1. \<exists>i. CS (f i) = cs \<and> CSS (f i) = css \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> [c] [] s \<or> (\<exists>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<and> AlternativeSmallStep.inf \<Gamma> cs css t)
 2. \<nexists>i. CS (f i) = cs \<and> CSS (f i) = css \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> [c] [] s \<or> (\<exists>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<and> AlternativeSmallStep.inf \<Gamma> cs css t)
[PROOF STEP]
define k where "k = (LEAST i. CS (f i) = cs \<and> CSS (f i) = css)"
[PROOF STATE]
proof (state)
this:
k = (LEAST i. CS (f i) = cs \<and> CSS (f i) = css)

goal (2 subgoals):
 1. \<exists>i. CS (f i) = cs \<and> CSS (f i) = css \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> [c] [] s \<or> (\<exists>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<and> AlternativeSmallStep.inf \<Gamma> cs css t)
 2. \<nexists>i. CS (f i) = cs \<and> CSS (f i) = css \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> [c] [] s \<or> (\<exists>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<and> AlternativeSmallStep.inf \<Gamma> cs css t)
[PROOF STEP]
from True
[PROOF STATE]
proof (chain)
picking this:
\<exists>i. CS (f i) = cs \<and> CSS (f i) = css
[PROOF STEP]
obtain CS_f_k: "CS (f k) = cs" and CSS_f_k: "CSS (f k) = css"
[PROOF STATE]
proof (prove)
using this:
\<exists>i. CS (f i) = cs \<and> CSS (f i) = css

goal (1 subgoal):
 1. (\<lbrakk>CS (f k) = cs; CSS (f k) = css\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>CS (f k) = cs; CSS (f k) = css\<rbrakk> \<Longrightarrow> thesis; \<exists>i. CS (f i) = cs \<and> CSS (f i) = css\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (erule exE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>\<lbrakk>CS (f k) = cs; CSS (f k) = css\<rbrakk> \<Longrightarrow> thesis; CS (f i) = cs \<and> CSS (f i) = css\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (drule LeastI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>\<lbrakk>CS (f k) = cs; CSS (f k) = css\<rbrakk> \<Longrightarrow> thesis; CS (f (LEAST x. CS (f x) = cs \<and> CSS (f x) = css)) = cs \<and> CSS (f (LEAST x. CS (f x) = cs \<and> CSS (f x) = css)) = css\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (simp add: k_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
CS (f k) = cs
CSS (f k) = css

goal (2 subgoals):
 1. \<exists>i. CS (f i) = cs \<and> CSS (f i) = css \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> [c] [] s \<or> (\<exists>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<and> AlternativeSmallStep.inf \<Gamma> cs css t)
 2. \<nexists>i. CS (f i) = cs \<and> CSS (f i) = css \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> [c] [] s \<or> (\<exists>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<and> AlternativeSmallStep.inf \<Gamma> cs css t)
[PROOF STEP]
have less_k_prop: "\<forall>i<k. \<not> (CS (f i) = cs \<and> CSS (f i) = css)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i<k. \<not> (CS (f i) = cs \<and> CSS (f i) = css)
[PROOF STEP]
apply (intro allI impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. i < k \<Longrightarrow> \<not> (CS (f i) = cs \<and> CSS (f i) = css)
[PROOF STEP]
apply (unfold k_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. i < (LEAST i. CS (f i) = cs \<and> CSS (f i) = css) \<Longrightarrow> \<not> (CS (f i) = cs \<and> CSS (f i) = css)
[PROOF STEP]
apply (drule not_less_Least)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<not> (CS (f i) = cs \<and> CSS (f i) = css) \<Longrightarrow> \<not> (CS (f i) = cs \<and> CSS (f i) = css)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<forall>i<k. \<not> (CS (f i) = cs \<and> CSS (f i) = css)

goal (2 subgoals):
 1. \<exists>i. CS (f i) = cs \<and> CSS (f i) = css \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> [c] [] s \<or> (\<exists>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<and> AlternativeSmallStep.inf \<Gamma> cs css t)
 2. \<nexists>i. CS (f i) = cs \<and> CSS (f i) = css \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> [c] [] s \<or> (\<exists>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<and> AlternativeSmallStep.inf \<Gamma> cs css t)
[PROOF STEP]
have "\<Gamma>\<turnstile>([c], [], s) \<rightarrow>\<^sup>* ([],[],S (f k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> ([c], [], s) \<rightarrow>\<^sup>* ([], [], S (f k))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> ([c], [], s) \<rightarrow>\<^sup>* ([], [], S (f k))
[PROOF STEP]
have "\<forall>i\<le>k. \<exists>pcs pcss.
        (if pcss = [] then CSS (f i)=css \<and> CS (f i)=pcs@cs
           else CS (f i)=pcs  \<and>
                CSS (f i)= butlast pcss@
                           [(fst (last pcss)@cs,(snd (last pcss))@cs)]@
                           css)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i\<le>k. \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
by (rule steps_hd_progress
        [OF f_0 f_step, where k=k, OF less_k_prop])
[PROOF STATE]
proof (state)
this:
\<forall>i\<le>k. \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css

goal (1 subgoal):
 1. \<Gamma>\<turnstile> ([c], [], s) \<rightarrow>\<^sup>* ([], [], S (f k))
[PROOF STEP]
from skolemize2 [OF this]
[PROOF STATE]
proof (chain)
picking this:
\<exists>fa g. \<forall>x\<le>k. if g x = [] then CSS (f x) = css \<and> CS (f x) = fa x @ cs else CS (f x) = fa x \<and> CSS (f x) = butlast (g x) @ [(fst (last (g x)) @ cs, snd (last (g x)) @ cs)] @ css
[PROOF STEP]
obtain pcs pcss where
        pcs_pcss:
            "\<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)"
[PROOF STATE]
proof (prove)
using this:
\<exists>fa g. \<forall>x\<le>k. if g x = [] then CSS (f x) = css \<and> CS (f x) = fa x @ cs else CS (f x) = fa x \<and> CSS (f x) = butlast (g x) @ [(fst (last (g x)) @ cs, snd (last (g x)) @ cs)] @ css

goal (1 subgoal):
 1. (\<And>pcss pcs. \<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 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by iprover
[PROOF STATE]
proof (state)
this:
\<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

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

goal (1 subgoal):
 1. pcs k = [] &&& pcss k = []
[PROOF STEP]
by (auto simp add: CS_def CSS_def S_def split: if_split_asm)
[PROOF STATE]
proof (state)
this:
pcs k = []
pcss k = []

goal (1 subgoal):
 1. \<Gamma>\<turnstile> ([c], [], s) \<rightarrow>\<^sup>* ([], [], S (f k))
[PROOF STEP]
from pcs_pcss
[PROOF STATE]
proof (chain)
picking this:
\<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
[PROOF STEP]
have 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)"
[PROOF STATE]
proof (prove)
using this:
\<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

goal (1 subgoal):
 1. \<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
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<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

goal (1 subgoal):
 1. \<Gamma>\<turnstile> ([c], [], s) \<rightarrow>\<^sup>* ([], [], S (f k))
[PROOF STEP]
from steps_hd_drop_suffix_finite [OF f_0 f_step less_k_prop simul] finished
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> ([c], [], s) \<rightarrow>\<^sup>* (pcs k, pcss k, S (f k))
pcs k = []
pcss k = []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> ([c], [], s) \<rightarrow>\<^sup>* (pcs k, pcss k, S (f k))
pcs k = []
pcss k = []

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> ([c], [], s) \<rightarrow>\<^sup>* ([], [], S (f k))

goal (2 subgoals):
 1. \<exists>i. CS (f i) = cs \<and> CSS (f i) = css \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> [c] [] s \<or> (\<exists>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<and> AlternativeSmallStep.inf \<Gamma> cs css t)
 2. \<nexists>i. CS (f i) = cs \<and> CSS (f i) = css \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> [c] [] s \<or> (\<exists>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<and> AlternativeSmallStep.inf \<Gamma> cs css t)
[PROOF STEP]
hence "\<Gamma>\<turnstile>\<langle>c,s\<rangle> \<Rightarrow> S (f k)"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> ([c], [], s) \<rightarrow>\<^sup>* ([], [], S (f k))

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> S (f k)
[PROOF STEP]
by (rule steps_impl_exec)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> S (f k)

goal (2 subgoals):
 1. \<exists>i. CS (f i) = cs \<and> CSS (f i) = css \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> [c] [] s \<or> (\<exists>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<and> AlternativeSmallStep.inf \<Gamma> cs css t)
 2. \<nexists>i. CS (f i) = cs \<and> CSS (f i) = css \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> [c] [] s \<or> (\<exists>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<and> AlternativeSmallStep.inf \<Gamma> cs css t)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> S (f k)

goal (2 subgoals):
 1. \<exists>i. CS (f i) = cs \<and> CSS (f i) = css \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> [c] [] s \<or> (\<exists>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<and> AlternativeSmallStep.inf \<Gamma> cs css t)
 2. \<nexists>i. CS (f i) = cs \<and> CSS (f i) = css \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> [c] [] s \<or> (\<exists>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<and> AlternativeSmallStep.inf \<Gamma> cs css t)
[PROOF STEP]
from CS_f_k CSS_f_k f_step
[PROOF STATE]
proof (chain)
picking this:
CS (f k) = cs
CSS (f k) = css
\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)
[PROOF STEP]
have "inf \<Gamma> cs css (S (f k))"
[PROOF STATE]
proof (prove)
using this:
CS (f k) = cs
CSS (f k) = css
\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)

goal (1 subgoal):
 1. AlternativeSmallStep.inf \<Gamma> cs css (S (f k))
[PROOF STEP]
apply (simp add: inf_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>CS (f k) = cs; CSS (f k) = css; \<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> \<exists>fa. fa 0 = (cs, css, S (f k)) \<and> (\<forall>i. \<Gamma>\<turnstile> fa i \<rightarrow> fa (Suc i))
[PROOF STEP]
apply (rule_tac x="\<lambda>i. f (i + k)" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>CS (f k) = cs; CSS (f k) = css; \<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> f (0 + k) = (cs, css, S (f k)) \<and> (\<forall>i. \<Gamma>\<turnstile> f (i + k) \<rightarrow> f (Suc i + k))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>CS (f k) = cs; CSS (f k) = css; \<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> f k = (cs, css, S (f k))
[PROOF STEP]
apply (auto simp add: CS_def CSS_def S_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
AlternativeSmallStep.inf \<Gamma> cs css (S (f k))

goal (2 subgoals):
 1. \<exists>i. CS (f i) = cs \<and> CSS (f i) = css \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> [c] [] s \<or> (\<exists>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<and> AlternativeSmallStep.inf \<Gamma> cs css t)
 2. \<nexists>i. CS (f i) = cs \<and> CSS (f i) = css \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> [c] [] s \<or> (\<exists>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<and> AlternativeSmallStep.inf \<Gamma> cs css t)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> S (f k)
AlternativeSmallStep.inf \<Gamma> cs css (S (f k))
[PROOF STEP]
have "(\<exists>t. \<Gamma>\<turnstile>\<langle>c,s\<rangle> \<Rightarrow> t \<and> inf \<Gamma> cs css t)"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> S (f k)
AlternativeSmallStep.inf \<Gamma> cs css (S (f k))

goal (1 subgoal):
 1. \<exists>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<and> AlternativeSmallStep.inf \<Gamma> cs css t
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<and> AlternativeSmallStep.inf \<Gamma> cs css t

goal (2 subgoals):
 1. \<exists>i. CS (f i) = cs \<and> CSS (f i) = css \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> [c] [] s \<or> (\<exists>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<and> AlternativeSmallStep.inf \<Gamma> cs css t)
 2. \<nexists>i. CS (f i) = cs \<and> CSS (f i) = css \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> [c] [] s \<or> (\<exists>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<and> AlternativeSmallStep.inf \<Gamma> cs css t)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<and> AlternativeSmallStep.inf \<Gamma> cs css t

goal (1 subgoal):
 1. AlternativeSmallStep.inf \<Gamma> [c] [] s \<or> (\<exists>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<and> AlternativeSmallStep.inf \<Gamma> cs css t)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
AlternativeSmallStep.inf \<Gamma> [c] [] s \<or> (\<exists>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<and> AlternativeSmallStep.inf \<Gamma> cs css t)

goal (1 subgoal):
 1. \<nexists>i. CS (f i) = cs \<and> CSS (f i) = css \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> [c] [] s \<or> (\<exists>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<and> AlternativeSmallStep.inf \<Gamma> cs css t)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nexists>i. CS (f i) = cs \<and> CSS (f i) = css \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> [c] [] s \<or> (\<exists>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<and> AlternativeSmallStep.inf \<Gamma> cs css t)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<nexists>i. CS (f i) = cs \<and> CSS (f i) = css

goal (1 subgoal):
 1. \<nexists>i. CS (f i) = cs \<and> CSS (f i) = css \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> [c] [] s \<or> (\<exists>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<and> AlternativeSmallStep.inf \<Gamma> cs css t)
[PROOF STEP]
hence unfinished: "\<forall>i. \<not> ((CS (f i) = cs) \<and> (CSS (f i) = css))"
[PROOF STATE]
proof (prove)
using this:
\<nexists>i. CS (f i) = cs \<and> CSS (f i) = css

goal (1 subgoal):
 1. \<forall>i. \<not> (CS (f i) = cs \<and> CSS (f i) = css)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>i. \<not> (CS (f i) = cs \<and> CSS (f i) = css)

goal (1 subgoal):
 1. \<nexists>i. CS (f i) = cs \<and> CSS (f i) = css \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> [c] [] s \<or> (\<exists>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<and> AlternativeSmallStep.inf \<Gamma> cs css t)
[PROOF STEP]
from inf_progress [OF f_0 f_step this]
[PROOF STATE]
proof (chain)
picking this:
\<exists>pcs pcss. if pcss = [] then CSS (f ?i) = css \<and> CS (f ?i) = pcs @ cs else CS (f ?i) = pcs \<and> CSS (f ?i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
have "\<forall>i. \<exists>pcs pcss.
          (if pcss = [] then CSS (f i)=css \<and> CS (f i)=pcs@cs
           else CS (f i)=pcs  \<and>
                CSS (f i)= butlast pcss@
                           [(fst (last pcss)@cs,(snd (last pcss))@cs)]@
                           css)"
[PROOF STATE]
proof (prove)
using this:
\<exists>pcs pcss. if pcss = [] then CSS (f ?i) = css \<and> CS (f ?i) = pcs @ cs else CS (f ?i) = pcs \<and> CSS (f ?i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css

goal (1 subgoal):
 1. \<forall>i. \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>i. \<exists>pcs pcss. if pcss = [] then CSS (f i) = css \<and> CS (f i) = pcs @ cs else CS (f i) = pcs \<and> CSS (f i) = butlast pcss @ [(fst (last pcss) @ cs, snd (last pcss) @ cs)] @ css

goal (1 subgoal):
 1. \<nexists>i. CS (f i) = cs \<and> CSS (f i) = css \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> [c] [] s \<or> (\<exists>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<and> AlternativeSmallStep.inf \<Gamma> cs css t)
[PROOF STEP]
from skolemize2' [OF this]
[PROOF STATE]
proof (chain)
picking this:
\<exists>fa g. \<forall>x. if g x = [] then CSS (f x) = css \<and> CS (f x) = fa x @ cs else CS (f x) = fa x \<and> CSS (f x) = butlast (g x) @ [(fst (last (g x)) @ cs, snd (last (g x)) @ cs)] @ css
[PROOF STEP]
obtain pcs pcss where
      pcs_pcss: "\<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 STATE]
proof (prove)
using this:
\<exists>fa g. \<forall>x. if g x = [] then CSS (f x) = css \<and> CS (f x) = fa x @ cs else CS (f x) = fa x \<and> CSS (f x) = butlast (g x) @ [(fst (last (g x)) @ cs, snd (last (g x)) @ cs)] @ css

goal (1 subgoal):
 1. (\<And>pcss pcs. \<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 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by iprover
[PROOF STATE]
proof (state)
this:
\<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. \<nexists>i. CS (f i) = cs \<and> CSS (f i) = css \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> [c] [] s \<or> (\<exists>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<and> AlternativeSmallStep.inf \<Gamma> cs css t)
[PROOF STEP]
define g where "g i = (pcs i, pcss i, S (f i))" for i
[PROOF STATE]
proof (state)
this:
g ?i = (pcs ?i, pcss ?i, S (f ?i))

goal (1 subgoal):
 1. \<nexists>i. CS (f i) = cs \<and> CSS (f i) = css \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> [c] [] s \<or> (\<exists>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<and> AlternativeSmallStep.inf \<Gamma> cs css t)
[PROOF STEP]
from pcs_pcss [rule_format, of 0] f_0
[PROOF STATE]
proof (chain)
picking this:
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
f 0 = (c # cs, css, s)
[PROOF STEP]
have "g 0 = ([c],[],s)"
[PROOF STATE]
proof (prove)
using this:
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
f 0 = (c # cs, css, s)

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

goal (1 subgoal):
 1. \<nexists>i. CS (f i) = cs \<and> CSS (f i) = css \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> [c] [] s \<or> (\<exists>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<and> AlternativeSmallStep.inf \<Gamma> cs css t)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
g 0 = ([c], [], s)

goal (1 subgoal):
 1. \<nexists>i. CS (f i) = cs \<and> CSS (f i) = css \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> [c] [] s \<or> (\<exists>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<and> AlternativeSmallStep.inf \<Gamma> cs css t)
[PROOF STEP]
from steps_hd_drop_suffix_infinite [OF f_0 f_step unfinished pcs_pcss]
[PROOF STATE]
proof (chain)
picking this:
\<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. \<Gamma>\<turnstile>g i \<rightarrow> g (Suc i)"
[PROOF STATE]
proof (prove)
using this:
\<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. \<Gamma>\<turnstile> g i \<rightarrow> g (Suc i)
[PROOF STEP]
by (simp add: g_def)
[PROOF STATE]
proof (state)
this:
\<forall>i. \<Gamma>\<turnstile> g i \<rightarrow> g (Suc i)

goal (1 subgoal):
 1. \<nexists>i. CS (f i) = cs \<and> CSS (f i) = css \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> [c] [] s \<or> (\<exists>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<and> AlternativeSmallStep.inf \<Gamma> cs css t)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
g 0 = ([c], [], s)
\<forall>i. \<Gamma>\<turnstile> g i \<rightarrow> g (Suc i)
[PROOF STEP]
have "inf \<Gamma> [c] [] s"
[PROOF STATE]
proof (prove)
using this:
g 0 = ([c], [], s)
\<forall>i. \<Gamma>\<turnstile> g i \<rightarrow> g (Suc i)

goal (1 subgoal):
 1. AlternativeSmallStep.inf \<Gamma> [c] [] s
[PROOF STEP]
by (auto simp add: inf_def)
[PROOF STATE]
proof (state)
this:
AlternativeSmallStep.inf \<Gamma> [c] [] s

goal (1 subgoal):
 1. \<nexists>i. CS (f i) = cs \<and> CSS (f i) = css \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> [c] [] s \<or> (\<exists>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<and> AlternativeSmallStep.inf \<Gamma> cs css t)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
AlternativeSmallStep.inf \<Gamma> [c] [] s

goal (1 subgoal):
 1. AlternativeSmallStep.inf \<Gamma> [c] [] s \<or> (\<exists>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<and> AlternativeSmallStep.inf \<Gamma> cs css t)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
AlternativeSmallStep.inf \<Gamma> [c] [] s \<or> (\<exists>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<and> AlternativeSmallStep.inf \<Gamma> cs css t)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
AlternativeSmallStep.inf \<Gamma> [c] [] s \<or> (\<exists>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<and> AlternativeSmallStep.inf \<Gamma> cs css t)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma infE [consumes 1]:
  assumes inf: "inf \<Gamma> (c#cs) css s"
  assumes cases: "inf \<Gamma> [c] [] s \<Longrightarrow> P"
                 "\<And>t. \<lbrakk>\<Gamma>\<turnstile>\<langle>c,s\<rangle> \<Rightarrow> t; inf \<Gamma> cs css t\<rbrakk> \<Longrightarrow> P"
  shows P
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P
[PROOF STEP]
using inf cases
[PROOF STATE]
proof (prove)
using this:
AlternativeSmallStep.inf \<Gamma> (c # cs) css s
AlternativeSmallStep.inf \<Gamma> [c] [] s \<Longrightarrow> P
\<lbrakk>\<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> ?t; AlternativeSmallStep.inf \<Gamma> cs css ?t\<rbrakk> \<Longrightarrow> P

goal (1 subgoal):
 1. P
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>AlternativeSmallStep.inf \<Gamma> (c # cs) css s; AlternativeSmallStep.inf \<Gamma> [c] [] s \<Longrightarrow> P; \<And>t. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t; AlternativeSmallStep.inf \<Gamma> cs css t\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
apply (drule inf.inf_cases)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>AlternativeSmallStep.inf \<Gamma> [c] [] s \<Longrightarrow> P; \<And>t. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t; AlternativeSmallStep.inf \<Gamma> cs css t\<rbrakk> \<Longrightarrow> P; AlternativeSmallStep.inf \<Gamma> [c] [] s \<or> (\<exists>t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<and> AlternativeSmallStep.inf \<Gamma> cs css t)\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done