[STATEMENT]
lemma (in inf) steps_hd_drop_suffix:
assumes f_0: "f 0 = (c#cs,css,s)"
assumes f_step: "\<forall>i. \<Gamma>\<turnstile> f(i) \<rightarrow> f(Suc i)"
assumes not_finished: "\<forall>i < k. \<not> (CS (f i) = cs \<and> CSS (f i) = css)"
assumes simul: "\<forall>i\<le>k.
        (if pcss i = [] then CSS (f i)=css \<and> CS (f i)=pcs i@cs
                 else CS (f i)=pcs i \<and>
                      CSS (f i)= butlast (pcss i)@
                              [(fst (last (pcss i))@cs,(snd (last (pcss i)))@cs)]@
                              css)"
defines "p\<equiv>\<lambda>i. (pcs i, pcss i, S (f i))"
shows "\<forall>i<k. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i<k. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
using not_finished simul
[PROOF STATE]
proof (prove)
using this:
\<forall>i<k. \<not> (CS (f i) = cs \<and> CSS (f i) = css)
\<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<k. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
proof (induct k)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<forall>i<0. \<not> (CS (f i) = cs \<and> CSS (f i) = css); \<forall>i\<le>0. 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\<rbrakk> \<Longrightarrow> \<forall>i<0. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
 2. \<And>k. \<lbrakk>\<lbrakk>\<forall>i<k. \<not> (CS (f i) = cs \<and> CSS (f i) = css); \<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\<rbrakk> \<Longrightarrow> \<forall>i<k. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i); \<forall>i<Suc k. \<not> (CS (f i) = cs \<and> CSS (f i) = css); \<forall>i\<le>Suc 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\<rbrakk> \<Longrightarrow> \<forall>i<Suc k. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
\<forall>i<0. \<not> (CS (f i) = cs \<and> CSS (f i) = css)
\<forall>i\<le>0. 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 (2 subgoals):
 1. \<lbrakk>\<forall>i<0. \<not> (CS (f i) = cs \<and> CSS (f i) = css); \<forall>i\<le>0. 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\<rbrakk> \<Longrightarrow> \<forall>i<0. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
 2. \<And>k. \<lbrakk>\<lbrakk>\<forall>i<k. \<not> (CS (f i) = cs \<and> CSS (f i) = css); \<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\<rbrakk> \<Longrightarrow> \<forall>i<k. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i); \<forall>i<Suc k. \<not> (CS (f i) = cs \<and> CSS (f i) = css); \<forall>i\<le>Suc 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\<rbrakk> \<Longrightarrow> \<forall>i<Suc k. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>i<0. \<not> (CS (f i) = cs \<and> CSS (f i) = css)
\<forall>i\<le>0. 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<0. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>i<0. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)

goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<lbrakk>\<forall>i<k. \<not> (CS (f i) = cs \<and> CSS (f i) = css); \<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\<rbrakk> \<Longrightarrow> \<forall>i<k. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i); \<forall>i<Suc k. \<not> (CS (f i) = cs \<and> CSS (f i) = css); \<forall>i\<le>Suc 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\<rbrakk> \<Longrightarrow> \<forall>i<Suc k. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<lbrakk>\<forall>i<k. \<not> (CS (f i) = cs \<and> CSS (f i) = css); \<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\<rbrakk> \<Longrightarrow> \<forall>i<k. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i); \<forall>i<Suc k. \<not> (CS (f i) = cs \<and> CSS (f i) = css); \<forall>i\<le>Suc 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\<rbrakk> \<Longrightarrow> \<forall>i<Suc k. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<forall>i<k. \<not> (CS (f i) = cs \<and> CSS (f i) = css); \<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\<rbrakk> \<Longrightarrow> \<forall>i<k. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
\<forall>i<Suc k. \<not> (CS (f i) = cs \<and> CSS (f i) = css)
\<forall>i\<le>Suc 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. \<And>k. \<lbrakk>\<lbrakk>\<forall>i<k. \<not> (CS (f i) = cs \<and> CSS (f i) = css); \<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\<rbrakk> \<Longrightarrow> \<forall>i<k. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i); \<forall>i<Suc k. \<not> (CS (f i) = cs \<and> CSS (f i) = css); \<forall>i\<le>Suc 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\<rbrakk> \<Longrightarrow> \<forall>i<Suc k. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
have simul: "\<forall>i\<le>Suc 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)
goal (1 subgoal):
 1. \<forall>i\<le>Suc 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 fact
[PROOF STATE]
proof (state)
this:
\<forall>i\<le>Suc 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. \<And>k. \<lbrakk>\<lbrakk>\<forall>i<k. \<not> (CS (f i) = cs \<and> CSS (f i) = css); \<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\<rbrakk> \<Longrightarrow> \<forall>i<k. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i); \<forall>i<Suc k. \<not> (CS (f i) = cs \<and> CSS (f i) = css); \<forall>i\<le>Suc 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\<rbrakk> \<Longrightarrow> \<forall>i<Suc k. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
have not_finished': "\<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>\<lbrakk>\<forall>i<k. \<not> (CS (f i) = cs \<and> CSS (f i) = css); \<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\<rbrakk> \<Longrightarrow> \<forall>i<k. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i); \<forall>i<Suc k. \<not> (CS (f i) = cs \<and> CSS (f i) = css); \<forall>i\<le>Suc 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\<rbrakk> \<Longrightarrow> \<forall>i<Suc k. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
with simul
[PROOF STATE]
proof (chain)
picking this:
\<forall>i\<le>Suc 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
\<forall>i<Suc k. \<not> (CS (f i) = cs \<and> CSS (f i) = css)
[PROOF STEP]
have not_finished: "\<forall>i<Suc k. \<not> (pcs i = [] \<and> pcss i = [])"
[PROOF STATE]
proof (prove)
using this:
\<forall>i\<le>Suc 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
\<forall>i<Suc k. \<not> (CS (f i) = cs \<and> CSS (f i) = css)

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

goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<lbrakk>\<forall>i<k. \<not> (CS (f i) = cs \<and> CSS (f i) = css); \<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\<rbrakk> \<Longrightarrow> \<forall>i<k. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i); \<forall>i<Suc k. \<not> (CS (f i) = cs \<and> CSS (f i) = css); \<forall>i\<le>Suc 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\<rbrakk> \<Longrightarrow> \<forall>i<Suc k. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i<Suc k. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
proof (clarify)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i < Suc k \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i < Suc k \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
assume i_le_Suc_k: "i < Suc k"
[PROOF STATE]
proof (state)
this:
i < Suc k

goal (1 subgoal):
 1. \<And>i. i < Suc k \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
show "\<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
proof (cases "i < k")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i < k \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
 2. \<not> i < k \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
i < k

goal (2 subgoals):
 1. i < k \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
 2. \<not> i < k \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
with not_finished' simul Suc.hyps
[PROOF STATE]
proof (chain)
picking this:
\<forall>i<Suc k. \<not> (CS (f i) = cs \<and> CSS (f i) = css)
\<forall>i\<le>Suc 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
\<lbrakk>\<forall>i<k. \<not> (CS (f i) = cs \<and> CSS (f i) = css); \<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\<rbrakk> \<Longrightarrow> \<forall>i<k. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
i < k
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>i<Suc k. \<not> (CS (f i) = cs \<and> CSS (f i) = css)
\<forall>i\<le>Suc 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
\<lbrakk>\<forall>i<k. \<not> (CS (f i) = cs \<and> CSS (f i) = css); \<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\<rbrakk> \<Longrightarrow> \<forall>i<k. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
i < k

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

goal (1 subgoal):
 1. \<not> i < k \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> i < k \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> i < k

goal (1 subgoal):
 1. \<not> i < k \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
with i_le_Suc_k
[PROOF STATE]
proof (chain)
picking this:
i < Suc k
\<not> i < k
[PROOF STEP]
have eq_i_k: "i=k"
[PROOF STATE]
proof (prove)
using this:
i < Suc k
\<not> i < k

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

goal (1 subgoal):
 1. \<not> i < k \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
show "\<Gamma>\<turnstile>p i \<rightarrow> p (Suc i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
obtain cs' css' t' where
          f_Suc_i: "f (Suc i) = (cs', css', t')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>cs' css' t'. f (Suc i) = (cs', css', t') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases "f (Suc i)")
[PROOF STATE]
proof (state)
this:
f (Suc i) = (cs', css', t')

goal (1 subgoal):
 1. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
obtain cs'' css'' t'' where
          f_i: "f i = (cs'',css'',t'')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>cs'' css'' t''. f i = (cs'', css'', t'') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases "f i")
[PROOF STATE]
proof (state)
this:
f i = (cs'', css'', t'')

goal (1 subgoal):
 1. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
from not_finished eq_i_k
[PROOF STATE]
proof (chain)
picking this:
\<forall>i<Suc k. \<not> (pcs i = [] \<and> pcss i = [])
i = k
[PROOF STEP]
have pcs_pcss_not_Nil: "\<not> (pcs i = [] \<and> pcss i = [])"
[PROOF STATE]
proof (prove)
using this:
\<forall>i<Suc k. \<not> (pcs i = [] \<and> pcss i = [])
i = k

goal (1 subgoal):
 1. \<not> (pcs i = [] \<and> pcss i = [])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> (pcs i = [] \<and> pcss i = [])

goal (1 subgoal):
 1. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
from simul [rule_format, of i] i_le_Suc_k f_i
[PROOF STATE]
proof (chain)
picking this:
i \<le> Suc k \<Longrightarrow> 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
i < Suc k
f i = (cs'', css'', t'')
[PROOF STEP]
have pcs_pcss_i:
          "if pcss i = [] then css''=css \<and> cs''=pcs i@cs
           else cs''=pcs i \<and>
           css''= butlast (pcss i)@
                       [(fst (last (pcss i))@cs,(snd (last (pcss i)))@cs)]@
                       css"
[PROOF STATE]
proof (prove)
using this:
i \<le> Suc k \<Longrightarrow> 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
i < Suc k
f i = (cs'', css'', t'')

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

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

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

goal (1 subgoal):
 1. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
proof (cases "pcss i = []")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. pcss i = [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
 2. pcss i \<noteq> [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
pcss i = []

goal (2 subgoals):
 1. pcss i = [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
 2. pcss i \<noteq> [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
note pcss_Nil = this
[PROOF STATE]
proof (state)
this:
pcss i = []

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

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

goal (2 subgoals):
 1. pcss i = [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
 2. pcss i \<noteq> [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
with f_i
[PROOF STATE]
proof (chain)
picking this:
f i = (cs'', css'', t'')
pcs i = p # ps
css'' = css
cs'' = (p # ps) @ cs
[PROOF STEP]
have "f i = (p#(ps@cs),css,t'')"
[PROOF STATE]
proof (prove)
using this:
f i = (cs'', css'', t'')
pcs i = p # ps
css'' = css
cs'' = (p # ps) @ cs

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

goal (2 subgoals):
 1. pcss i = [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
 2. pcss i \<noteq> [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
with f_Suc_i f_step [rule_format, of i]
[PROOF STATE]
proof (chain)
picking this:
f (Suc i) = (cs', css', t')
\<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)
f i = (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 i) = (cs', css', t')
\<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)
f i = (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 i = [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
 2. pcss i \<noteq> [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[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 i = [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
 2. pcss i \<noteq> [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
proof (cases "css''' = []")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. css''' = [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
 2. css''' \<noteq> [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
css''' = []

goal (2 subgoals):
 1. css''' = [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
 2. css''' \<noteq> [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[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> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
 2. css''' \<noteq> [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
(*from cs' css' f_Suc_i f_i [rule_format, of "Suc k"]
                have p_ps_not_Nil: "p'@ps \<noteq> Nil"
                by auto*)
[PROOF STATE]
proof (state)
this:
css' = css
cs' = p' @ ps @ cs

goal (2 subgoals):
 1. css''' = [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
 2. css''' \<noteq> [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
from css' cs' step_css
[PROOF STATE]
proof (chain)
picking this:
css' = css
cs' = p' @ ps @ cs
\<Gamma>\<turnstile> (p # ps @ cs, css, t'') \<rightarrow> (cs', css', t')
[PROOF STEP]
have step: "\<Gamma>\<turnstile> (p#(ps@cs),css,t'') \<rightarrow> (p'@ps@cs,css,t')"
[PROOF STATE]
proof (prove)
using this:
css' = css
cs' = p' @ ps @ cs
\<Gamma>\<turnstile> (p # ps @ cs, css, t'') \<rightarrow> (cs', css', t')

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

goal (2 subgoals):
 1. css''' = [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
 2. css''' \<noteq> [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
hence "\<Gamma>\<turnstile> ((p#ps)@cs,css,t'') \<rightarrow> ((p'@ps)@cs,css,t')"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> (p # ps @ cs, css, t'') \<rightarrow> (p' @ ps @ cs, css, t')

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

goal (2 subgoals):
 1. css''' = [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
 2. css''' \<noteq> [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
from drop_suffix_css_step' [OF drop_suffix_same_css_step [OF this],
              where xs="css" and css="[]" and css'="[]"]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>p # ps \<noteq> []; ?css'xs = [] @ css; ?css'xs = [] @ css\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (p # ps, [], t'') \<rightarrow> (p' @ ps, [], t')
[PROOF STEP]
have  "\<Gamma>\<turnstile> (p#ps,[],t'') \<rightarrow> (p'@ps,[],t')"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>p # ps \<noteq> []; ?css'xs = [] @ css; ?css'xs = [] @ css\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (p # ps, [], t'') \<rightarrow> (p' @ ps, [], t')

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

goal (2 subgoals):
 1. css''' = [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
 2. css''' \<noteq> [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (p # ps, [], t'') \<rightarrow> (p' @ ps, [], t')

goal (2 subgoals):
 1. css''' = [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
 2. css''' \<noteq> [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
from css' cs' pcs_pcss_Suc_i
[PROOF STATE]
proof (chain)
picking this:
css' = css
cs' = p' @ ps @ cs
if pcss (Suc i) = [] then css' = css \<and> cs' = pcs (Suc i) @ cs else cs' = pcs (Suc i) \<and> css' = butlast (pcss (Suc i)) @ [(fst (last (pcss (Suc i))) @ cs, snd (last (pcss (Suc i))) @ cs)] @ css
[PROOF STEP]
obtain "pcs (Suc i) = p'@ps" and "pcss (Suc i) = []"
[PROOF STATE]
proof (prove)
using this:
css' = css
cs' = p' @ ps @ cs
if pcss (Suc i) = [] then css' = css \<and> cs' = pcs (Suc i) @ cs else cs' = pcs (Suc i) \<and> css' = butlast (pcss (Suc i)) @ [(fst (last (pcss (Suc i))) @ cs, snd (last (pcss (Suc i))) @ cs)] @ css

goal (1 subgoal):
 1. (\<lbrakk>pcs (Suc i) = p' @ ps; pcss (Suc i) = []\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (simp split: if_split_asm)
[PROOF STATE]
proof (state)
this:
pcs (Suc i) = p' @ ps
pcss (Suc i) = []

goal (2 subgoals):
 1. css''' = [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
 2. css''' \<noteq> [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> (p # ps, [], t'') \<rightarrow> (p' @ ps, [], t')
pcs (Suc i) = p' @ ps
pcss (Suc i) = []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> (p # ps, [], t'') \<rightarrow> (p' @ ps, [], t')
pcs (Suc i) = p' @ ps
pcss (Suc i) = []

goal (1 subgoal):
 1. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
using pcs_i pcss_Nil f_i f_Suc_i
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> (p # ps, [], t'') \<rightarrow> (p' @ ps, [], t')
pcs (Suc i) = p' @ ps
pcss (Suc i) = []
pcs i = p # ps
pcss i = []
f i = (cs'', css'', t'')
f (Suc i) = (cs', css', t')

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

goal (1 subgoal):
 1. css''' \<noteq> [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. css''' \<noteq> [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
css''' \<noteq> []

goal (1 subgoal):
 1. css''' \<noteq> [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[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> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
with css''' step_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)]
\<Gamma>\<turnstile> (p # ps @ cs, css, t'') \<rightarrow> (cs', css', t')
css' = css''' @ css
css''' = [(pnorm @ ps @ cs, pabr @ ps @ cs)]
[PROOF STEP]
have "\<Gamma>\<turnstile> (p#ps@cs,css,t'') \<rightarrow> (cs',[(pnorm@ps@cs,pabr@ps@cs)]@css,t')"
[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)]
\<Gamma>\<turnstile> (p # ps @ cs, css, t'') \<rightarrow> (cs', css', t')
css' = css''' @ css
css''' = [(pnorm @ ps @ cs, pabr @ ps @ cs)]

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

goal (1 subgoal):
 1. css''' \<noteq> [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> (p # ps @ cs, css, t'') \<rightarrow> (cs', [(pnorm @ ps @ cs, pabr @ ps @ cs)] @ css, t')
[PROOF STEP]
have "\<Gamma>\<turnstile>(p#ps, css, t'') \<rightarrow> (cs', [(pnorm@ps, pabr@ps)] @ css, t')"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> (p # ps @ cs, css, t'') \<rightarrow> (cs', [(pnorm @ ps @ cs, pabr @ ps @ cs)] @ css, t')

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

goal (1 subgoal):
 1. css''' \<noteq> [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
from drop_suffix_css_step' [OF this,
              where css="[]" and xs="css" and css'="[(pnorm@ps, pabr@ps)]"]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>css = [] @ css; [(pnorm @ ps, pabr @ ps)] @ css = [(pnorm @ ps, pabr @ ps)] @ css\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (p # ps, [], t'') \<rightarrow> (cs', [(pnorm @ ps, pabr @ ps)], t')
[PROOF STEP]
have "\<Gamma>\<turnstile> (p#ps,[],t'') \<rightarrow> (cs',[(pnorm@ps, pabr@ps)],t')"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>css = [] @ css; [(pnorm @ ps, pabr @ ps)] @ css = [(pnorm @ ps, pabr @ ps)] @ css\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (p # ps, [], t'') \<rightarrow> (cs', [(pnorm @ ps, pabr @ ps)], t')

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

goal (1 subgoal):
 1. css''' \<noteq> [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (p # ps, [], t'') \<rightarrow> (cs', [(pnorm @ ps, pabr @ ps)], t')

goal (1 subgoal):
 1. css''' \<noteq> [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
from css' pcs_pcss_Suc_i
[PROOF STATE]
proof (chain)
picking this:
css' = css''' @ css
css''' = [(pnorm @ ps @ cs, pabr @ ps @ cs)]
if pcss (Suc i) = [] then css' = css \<and> cs' = pcs (Suc i) @ cs else cs' = pcs (Suc i) \<and> css' = butlast (pcss (Suc i)) @ [(fst (last (pcss (Suc i))) @ cs, snd (last (pcss (Suc i))) @ cs)] @ css
[PROOF STEP]
obtain "pcs (Suc i) = cs'" "pcss (Suc i) = [(pnorm@ps, pabr@ps)]"
[PROOF STATE]
proof (prove)
using this:
css' = css''' @ css
css''' = [(pnorm @ ps @ cs, pabr @ ps @ cs)]
if pcss (Suc i) = [] then css' = css \<and> cs' = pcs (Suc i) @ cs else cs' = pcs (Suc i) \<and> css' = butlast (pcss (Suc i)) @ [(fst (last (pcss (Suc i))) @ cs, snd (last (pcss (Suc i))) @ cs)] @ css

goal (1 subgoal):
 1. (\<lbrakk>pcs (Suc i) = cs'; pcss (Suc i) = [(pnorm @ ps, pabr @ ps)]\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply (cases "pcss (Suc i)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>pcs (Suc i) = cs'; pcss (Suc i) = [(pnorm @ ps, pabr @ ps)]\<rbrakk> \<Longrightarrow> thesis; css' = css''' @ css; css''' = [(pnorm @ ps @ cs, pabr @ ps @ cs)]; if pcss (Suc i) = [] then css' = css \<and> cs' = pcs (Suc i) @ cs else cs' = pcs (Suc i) \<and> css' = butlast (pcss (Suc i)) @ [(fst (last (pcss (Suc i))) @ cs, snd (last (pcss (Suc i))) @ cs)] @ css; pcss (Suc i) = []\<rbrakk> \<Longrightarrow> thesis
 2. \<And>a list. \<lbrakk>\<lbrakk>pcs (Suc i) = cs'; pcss (Suc i) = [(pnorm @ ps, pabr @ ps)]\<rbrakk> \<Longrightarrow> thesis; css' = css''' @ css; css''' = [(pnorm @ ps @ cs, pabr @ ps @ cs)]; if pcss (Suc i) = [] then css' = css \<and> cs' = pcs (Suc i) @ cs else cs' = pcs (Suc i) \<and> css' = butlast (pcss (Suc i)) @ [(fst (last (pcss (Suc i))) @ cs, snd (last (pcss (Suc i))) @ cs)] @ css; pcss (Suc i) = a # list\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (auto split: if_split_asm)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
pcs (Suc i) = cs'
pcss (Suc i) = [(pnorm @ ps, pabr @ ps)]

goal (1 subgoal):
 1. css''' \<noteq> [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> (p # ps, [], t'') \<rightarrow> (cs', [(pnorm @ ps, pabr @ ps)], t')
pcs (Suc i) = cs'
pcss (Suc i) = [(pnorm @ ps, pabr @ ps)]
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> (p # ps, [], t'') \<rightarrow> (cs', [(pnorm @ ps, pabr @ ps)], t')
pcs (Suc i) = cs'
pcss (Suc i) = [(pnorm @ ps, pabr @ ps)]

goal (1 subgoal):
 1. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
using pcs_i pcss_Nil f_i f_Suc_i
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> (p # ps, [], t'') \<rightarrow> (cs', [(pnorm @ ps, pabr @ ps)], t')
pcs (Suc i) = cs'
pcss (Suc i) = [(pnorm @ ps, pabr @ ps)]
pcs i = p # ps
pcss i = []
f i = (cs'', css'', t'')
f (Suc i) = (cs', css', t')

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)

goal (1 subgoal):
 1. pcss i \<noteq> [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pcss i \<noteq> [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
pcss i \<noteq> []

goal (1 subgoal):
 1. pcss i \<noteq> [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
note pcss_i_not_Nil = this
[PROOF STATE]
proof (state)
this:
pcss i \<noteq> []

goal (1 subgoal):
 1. pcss i \<noteq> [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
with pcs_pcss_i
[PROOF STATE]
proof (chain)
picking this:
if pcss i = [] then css'' = css \<and> cs'' = pcs i @ cs else cs'' = pcs i \<and> css'' = butlast (pcss i) @ [(fst (last (pcss i)) @ cs, snd (last (pcss i)) @ cs)] @ css
pcss i \<noteq> []
[PROOF STEP]
obtain
            cs'': "cs''=pcs i" and
            css'': "css''= butlast (pcss i)@
                            [(fst (last (pcss i))@cs,(snd (last (pcss i)))@cs)]@
                            css"
[PROOF STATE]
proof (prove)
using this:
if pcss i = [] then css'' = css \<and> cs'' = pcs i @ cs else cs'' = pcs i \<and> css'' = butlast (pcss i) @ [(fst (last (pcss i)) @ cs, snd (last (pcss i)) @ cs)] @ css
pcss i \<noteq> []

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

goal (1 subgoal):
 1. pcss i \<noteq> [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
from f_Suc_i f_i f_step [rule_format, of i]
[PROOF STATE]
proof (chain)
picking this:
f (Suc i) = (cs', css', t')
f i = (cs'', css'', t'')
\<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)
[PROOF STEP]
have step_i_full: "\<Gamma>\<turnstile> (cs'',css'',t'') \<rightarrow> (cs',css',t')"
[PROOF STATE]
proof (prove)
using this:
f (Suc i) = (cs', css', t')
f i = (cs'', css'', t'')
\<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)

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 i \<noteq> [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
proof (cases cs'')
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. cs'' = [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
 2. \<And>a list. cs'' = a # list \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
case (Cons c' cs)
[PROOF STATE]
proof (state)
this:
cs'' = c' # cs

goal (2 subgoals):
 1. cs'' = [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
 2. \<And>a list. cs'' = a # list \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[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> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
 2. \<And>a list. cs'' = a # list \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
with step_i_full
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> (cs'', css'', t'') \<rightarrow> (cs', css', t')
css' = css''' @ css''
[PROOF STEP]
have "\<Gamma>\<turnstile> (cs'',css'',t'') \<rightarrow> (cs',css'''@css'',t')"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> (cs'', css'', t'') \<rightarrow> (cs', css', t')
css' = css''' @ css''

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

goal (2 subgoals):
 1. cs'' = [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
 2. \<And>a list. cs'' = a # list \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
from Cons_change_css_step [OF this, where xss="pcss i"] Cons cs''
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> (cs'', pcss i, t'') \<rightarrow> (cs', css''' @ pcss i, t')
cs'' = c' # cs
cs'' = pcs i
[PROOF STEP]
have "\<Gamma>\<turnstile> (pcs i, pcss i,t'') \<rightarrow> (cs',css'''@pcss i,t')"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> (cs'', pcss i, t'') \<rightarrow> (cs', css''' @ pcss i, t')
cs'' = c' # cs
cs'' = pcs i

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

goal (2 subgoals):
 1. cs'' = [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
 2. \<And>a list. cs'' = a # list \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (pcs i, pcss i, t'') \<rightarrow> (cs', css''' @ pcss i, t')

goal (2 subgoals):
 1. cs'' = [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
 2. \<And>a list. cs'' = a # list \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
from cs'' css'' css' False pcs_pcss_Suc_i
[PROOF STATE]
proof (chain)
picking this:
cs'' = pcs i
css'' = butlast (pcss i) @ [(fst (last (pcss i)) @ cs, snd (last (pcss i)) @ cs)] @ css
css' = css''' @ css''
pcss i \<noteq> []
if pcss (Suc i) = [] then css' = css \<and> cs' = pcs (Suc i) @ cs else cs' = pcs (Suc i) \<and> css' = butlast (pcss (Suc i)) @ [(fst (last (pcss (Suc i))) @ cs, snd (last (pcss (Suc i))) @ cs)] @ css
[PROOF STEP]
obtain "pcs (Suc i) = cs'" "pcss (Suc i) = css'''@pcss i"
[PROOF STATE]
proof (prove)
using this:
cs'' = pcs i
css'' = butlast (pcss i) @ [(fst (last (pcss i)) @ cs, snd (last (pcss i)) @ cs)] @ css
css' = css''' @ css''
pcss i \<noteq> []
if pcss (Suc i) = [] then css' = css \<and> cs' = pcs (Suc i) @ cs else cs' = pcs (Suc i) \<and> css' = butlast (pcss (Suc i)) @ [(fst (last (pcss (Suc i))) @ cs, snd (last (pcss (Suc i))) @ cs)] @ css

goal (1 subgoal):
 1. (\<lbrakk>pcs (Suc i) = cs'; pcss (Suc i) = css''' @ pcss i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply (auto  split: if_split_asm)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pcss (Suc i) = css''' @ pcss i \<Longrightarrow> thesis; cs'' = pcs i; css'' = butlast (pcss i) @ (fst (last (pcss i)) @ cs, snd (last (pcss i)) @ cs) # css; pcss i \<noteq> []; pcss (Suc i) \<noteq> []; butlast (pcss (Suc i)) = css''' @ butlast (pcss i); cs' = pcs (Suc i); css' = css''' @ butlast (pcss i) @ (fst (last (pcss i)) @ cs, snd (last (pcss i)) @ cs) # css; fst (last (pcss (Suc i))) = fst (last (pcss i)); snd (last (pcss (Suc i))) = snd (last (pcss i))\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (drule (4) last_butlast_app)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pcss (Suc i) = css''' @ pcss i \<Longrightarrow> thesis; cs'' = pcs i; css'' = butlast (pcss i) @ (fst (last (pcss i)) @ cs, snd (last (pcss i)) @ cs) # css; pcss i \<noteq> []; pcss (Suc i) \<noteq> []; cs' = pcs (Suc i); css' = css''' @ butlast (pcss i) @ (fst (last (pcss i)) @ cs, snd (last (pcss i)) @ cs) # css; fst (last (pcss (Suc i))) = fst (last (pcss i)); snd (last (pcss (Suc i))) = snd (last (pcss i)); pcss (Suc i) = css''' @ pcss i\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
pcs (Suc i) = cs'
pcss (Suc i) = css''' @ pcss i

goal (2 subgoals):
 1. cs'' = [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
 2. \<And>a list. cs'' = a # list \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> (pcs i, pcss i, t'') \<rightarrow> (cs', css''' @ pcss i, t')
pcs (Suc i) = cs'
pcss (Suc i) = css''' @ pcss i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> (pcs i, pcss i, t'') \<rightarrow> (cs', css''' @ pcss i, t')
pcs (Suc i) = cs'
pcss (Suc i) = css''' @ pcss i

goal (1 subgoal):
 1. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
using f_i f_Suc_i
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> (pcs i, pcss i, t'') \<rightarrow> (cs', css''' @ pcss i, t')
pcs (Suc i) = cs'
pcss (Suc i) = css''' @ pcss i
f i = (cs'', css'', t'')
f (Suc i) = (cs', css', t')

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

goal (1 subgoal):
 1. cs'' = [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cs'' = [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
cs'' = []

goal (1 subgoal):
 1. cs'' = [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
note cs''_Nil = this
[PROOF STATE]
proof (state)
this:
cs'' = []

goal (1 subgoal):
 1. cs'' = [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
proof (cases "butlast (pcss i)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. butlast (pcss i) = [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
 2. \<And>a list. butlast (pcss i) = a # list \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
case (Cons bpcs bpcss)
[PROOF STATE]
proof (state)
this:
butlast (pcss i) = bpcs # bpcss

goal (2 subgoals):
 1. butlast (pcss i) = [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
 2. \<And>a list. butlast (pcss i) = a # list \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[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 i) @ [(fst (last (pcss i)) @ cs, snd (last (pcss i)) @ cs)] @ css
butlast (pcss i) = 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 i) @ [(fst (last (pcss i)) @ cs, snd (last (pcss i)) @ cs)] @ css
butlast (pcss i) = 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 i) = [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
 2. \<And>a list. butlast (pcss i) = a # list \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[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 i) = [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
 2. \<And>a list. butlast (pcss i) = a # list \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[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]
have css': "css'=tl 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. css' = tl css''
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
css' = tl css''

goal (2 subgoals):
 1. butlast (pcss i) = [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
 2. \<And>a list. butlast (pcss i) = a # list \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> ([], [hd css''] @ tl css'', t'') \<rightarrow> (cs', css', t')
css' = tl css''
[PROOF STEP]
have
                step_i_full: "\<Gamma>\<turnstile> ([],[hd css'']@tl css'',t'') \<rightarrow> (cs',tl css'',t')"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> ([], [hd css''] @ tl css'', t'') \<rightarrow> (cs', css', t')
css' = tl css''

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

goal (2 subgoals):
 1. butlast (pcss i) = [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
 2. \<And>a list. butlast (pcss i) = a # list \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
from css'' Cons pcss_i_not_Nil
[PROOF STATE]
proof (chain)
picking this:
css'' = butlast (pcss i) @ [(fst (last (pcss i)) @ cs, snd (last (pcss i)) @ cs)] @ css
butlast (pcss i) = bpcs # bpcss
pcss i \<noteq> []
[PROOF STEP]
have "hd css'' = hd (pcss i)"
[PROOF STATE]
proof (prove)
using this:
css'' = butlast (pcss i) @ [(fst (last (pcss i)) @ cs, snd (last (pcss i)) @ cs)] @ css
butlast (pcss i) = bpcs # bpcss
pcss i \<noteq> []

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

goal (2 subgoals):
 1. butlast (pcss i) = [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
 2. \<And>a list. butlast (pcss i) = a # list \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
with cs'' cs''_Nil
                Nil_change_css_step [where ass="[hd css'']" and
                css="tl css''" and ass'="[]" and
                xss="tl (pcss i)", simplified, OF step_i_full [simplified]]
[PROOF STATE]
proof (chain)
picking this:
cs'' = pcs i
cs'' = []
\<Gamma>\<turnstile> ([], hd css'' # tl (pcss i), t'') \<rightarrow> (cs', tl (pcss i), t')
hd css'' = hd (pcss i)
[PROOF STEP]
have "\<Gamma>\<turnstile> (pcs i,[hd (pcss i)]@tl (pcss i),t'') \<rightarrow> (cs',tl (pcss i),t')"
[PROOF STATE]
proof (prove)
using this:
cs'' = pcs i
cs'' = []
\<Gamma>\<turnstile> ([], hd css'' # tl (pcss i), t'') \<rightarrow> (cs', tl (pcss i), t')
hd css'' = hd (pcss i)

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

goal (2 subgoals):
 1. butlast (pcss i) = [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
 2. \<And>a list. butlast (pcss i) = a # list \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
with pcss_i_not_Nil
[PROOF STATE]
proof (chain)
picking this:
pcss i \<noteq> []
\<Gamma>\<turnstile> (pcs i, [hd (pcss i)] @ tl (pcss i), t'') \<rightarrow> (cs', tl (pcss i), t')
[PROOF STEP]
have "\<Gamma>\<turnstile> (pcs i,pcss i,t'') \<rightarrow> (cs',tl (pcss i),t')"
[PROOF STATE]
proof (prove)
using this:
pcss i \<noteq> []
\<Gamma>\<turnstile> (pcs i, [hd (pcss i)] @ tl (pcss i), t'') \<rightarrow> (cs', tl (pcss i), t')

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

goal (2 subgoals):
 1. butlast (pcss i) = [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
 2. \<And>a list. butlast (pcss i) = a # list \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (pcs i, pcss i, t'') \<rightarrow> (cs', tl (pcss i), t')

goal (2 subgoals):
 1. butlast (pcss i) = [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
 2. \<And>a list. butlast (pcss i) = a # list \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
from css' css'' cs''_Nil Cons pcss_i_not_Nil pcs_pcss_Suc_i
[PROOF STATE]
proof (chain)
picking this:
css' = tl css''
css'' = butlast (pcss i) @ [(fst (last (pcss i)) @ cs, snd (last (pcss i)) @ cs)] @ css
cs'' = []
butlast (pcss i) = bpcs # bpcss
pcss i \<noteq> []
if pcss (Suc i) = [] then css' = css \<and> cs' = pcs (Suc i) @ cs else cs' = pcs (Suc i) \<and> css' = butlast (pcss (Suc i)) @ [(fst (last (pcss (Suc i))) @ cs, snd (last (pcss (Suc i))) @ cs)] @ css
[PROOF STEP]
obtain "pcs (Suc i) = cs'" "pcss (Suc i) = tl (pcss i)"
[PROOF STATE]
proof (prove)
using this:
css' = tl css''
css'' = butlast (pcss i) @ [(fst (last (pcss i)) @ cs, snd (last (pcss i)) @ cs)] @ css
cs'' = []
butlast (pcss i) = bpcs # bpcss
pcss i \<noteq> []
if pcss (Suc i) = [] then css' = css \<and> cs' = pcs (Suc i) @ cs else cs' = pcs (Suc i) \<and> css' = butlast (pcss (Suc i)) @ [(fst (last (pcss (Suc i))) @ cs, snd (last (pcss (Suc i))) @ cs)] @ css

goal (1 subgoal):
 1. (\<lbrakk>pcs (Suc i) = cs'; pcss (Suc i) = tl (pcss i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply (clarsimp  split: if_split_asm)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pcss (Suc i) = tl (pcss i) \<Longrightarrow> thesis; css'' = bpcs # butlast (pcss (Suc i)) @ (fst (last (pcss i)) @ cs, snd (last (pcss i)) @ cs) # css; cs'' = []; butlast (pcss i) = bpcs # butlast (pcss (Suc i)); pcss i \<noteq> []; pcss (Suc i) \<noteq> []; bpcss = butlast (pcss (Suc i)); cs' = pcs (Suc i); css' = butlast (pcss (Suc i)) @ (fst (last (pcss i)) @ cs, snd (last (pcss i)) @ cs) # css; fst (last (pcss (Suc i))) = fst (last (pcss i)); snd (last (pcss (Suc i))) = snd (last (pcss i))\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (drule (4) last_butlast_tl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pcss (Suc i) = tl (pcss i) \<Longrightarrow> thesis; css'' = bpcs # butlast (pcss (Suc i)) @ (fst (last (pcss i)) @ cs, snd (last (pcss i)) @ cs) # css; cs'' = []; pcss i \<noteq> []; pcss (Suc i) \<noteq> []; bpcss = butlast (pcss (Suc i)); cs' = pcs (Suc i); css' = butlast (pcss (Suc i)) @ (fst (last (pcss i)) @ cs, snd (last (pcss i)) @ cs) # css; fst (last (pcss (Suc i))) = fst (last (pcss i)); snd (last (pcss (Suc i))) = snd (last (pcss i)); pcss (Suc i) = tl (pcss i)\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
pcs (Suc i) = cs'
pcss (Suc i) = tl (pcss i)

goal (2 subgoals):
 1. butlast (pcss i) = [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
 2. \<And>a list. butlast (pcss i) = a # list \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> (pcs i, pcss i, t'') \<rightarrow> (cs', tl (pcss i), t')
pcs (Suc i) = cs'
pcss (Suc i) = tl (pcss i)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> (pcs i, pcss i, t'') \<rightarrow> (cs', tl (pcss i), t')
pcs (Suc i) = cs'
pcss (Suc i) = tl (pcss i)

goal (1 subgoal):
 1. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
using f_i f_Suc_i
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> (pcs i, pcss i, t'') \<rightarrow> (cs', tl (pcss i), t')
pcs (Suc i) = cs'
pcss (Suc i) = tl (pcss i)
f i = (cs'', css'', t'')
f (Suc i) = (cs', css', t')

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

goal (1 subgoal):
 1. butlast (pcss i) = [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. butlast (pcss i) = [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
butlast (pcss i) = []

goal (1 subgoal):
 1. butlast (pcss i) = [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
with css'' pcss_i_not_Nil
[PROOF STATE]
proof (chain)
picking this:
css'' = butlast (pcss i) @ [(fst (last (pcss i)) @ cs, snd (last (pcss i)) @ cs)] @ css
pcss i \<noteq> []
butlast (pcss i) = []
[PROOF STEP]
obtain pnorm pabr
                where css'': "css''= [(pnorm@cs,pabr@cs)]@css" and
                pcss_i: "pcss i = [(pnorm,pabr)]"
[PROOF STATE]
proof (prove)
using this:
css'' = butlast (pcss i) @ [(fst (last (pcss i)) @ cs, snd (last (pcss i)) @ cs)] @ css
pcss i \<noteq> []
butlast (pcss i) = []

goal (1 subgoal):
 1. (\<And>pnorm pabr. \<lbrakk>css'' = [(pnorm @ cs, pabr @ cs)] @ css; pcss i = [(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 i = [(pnorm, pabr)]

goal (1 subgoal):
 1. butlast (pcss i) = [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[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 i = [(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 i = [(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 i) = [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[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 i) = [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
let "?pcs_Suc_i " = "(case t'' of Abrupt s' \<Rightarrow> pabr | _ \<Rightarrow> pnorm)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. butlast (pcss i) = [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
from cs'
[PROOF STATE]
proof (chain)
picking this:
case t'' of Abrupt s' \<Rightarrow> cs' = pabr @ cs \<and> t' = Normal s' | _ \<Rightarrow> cs' = pnorm @ cs \<and> t' = t''
[PROOF STEP]
have "\<Gamma>\<turnstile>([],[(pnorm,pabr)],t'') \<rightarrow> (?pcs_Suc_i,[],t')"
[PROOF STATE]
proof (prove)
using this:
case t'' of Abrupt s' \<Rightarrow> cs' = pabr @ cs \<and> t' = Normal s' | _ \<Rightarrow> cs' = pnorm @ cs \<and> t' = t''

goal (1 subgoal):
 1. \<Gamma>\<turnstile> ([], [(pnorm, pabr)], t'') \<rightarrow> (case t'' of Abrupt s' \<Rightarrow> pabr | _ \<Rightarrow> pnorm, [], t')
[PROOF STEP]
by (auto intro: step.intros split: xstate.splits)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> ([], [(pnorm, pabr)], t'') \<rightarrow> (case t'' of Abrupt s' \<Rightarrow> pabr | _ \<Rightarrow> pnorm, [], t')

goal (1 subgoal):
 1. butlast (pcss i) = [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> ([], [(pnorm, pabr)], t'') \<rightarrow> (case t'' of Abrupt s' \<Rightarrow> pabr | _ \<Rightarrow> pnorm, [], t')

goal (1 subgoal):
 1. butlast (pcss i) = [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
from css'' css' cs' pcss_i pcs_pcss_Suc_i
[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 i = [(pnorm, pabr)]
if pcss (Suc i) = [] then css' = css \<and> cs' = pcs (Suc i) @ cs else cs' = pcs (Suc i) \<and> css' = butlast (pcss (Suc i)) @ [(fst (last (pcss (Suc i))) @ cs, snd (last (pcss (Suc i))) @ cs)] @ css
[PROOF STEP]
obtain "pcs (Suc i) = ?pcs_Suc_i" "pcss (Suc i) = []"
[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 i = [(pnorm, pabr)]
if pcss (Suc i) = [] then css' = css \<and> cs' = pcs (Suc i) @ cs else cs' = pcs (Suc i) \<and> css' = butlast (pcss (Suc i)) @ [(fst (last (pcss (Suc i))) @ cs, snd (last (pcss (Suc i))) @ cs)] @ css

goal (1 subgoal):
 1. (\<lbrakk>pcs (Suc i) = (case t'' of Abrupt s' \<Rightarrow> pabr | _ \<Rightarrow> pnorm); pcss (Suc i) = []\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (simp split: if_split_asm xstate.splits)
[PROOF STATE]
proof (state)
this:
pcs (Suc i) = (case t'' of Abrupt s' \<Rightarrow> pabr | _ \<Rightarrow> pnorm)
pcss (Suc i) = []

goal (1 subgoal):
 1. butlast (pcss i) = [] \<Longrightarrow> \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> ([], [(pnorm, pabr)], t'') \<rightarrow> (case t'' of Abrupt s' \<Rightarrow> pabr | _ \<Rightarrow> pnorm, [], t')
pcs (Suc i) = (case t'' of Abrupt s' \<Rightarrow> pabr | _ \<Rightarrow> pnorm)
pcss (Suc i) = []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> ([], [(pnorm, pabr)], t'') \<rightarrow> (case t'' of Abrupt s' \<Rightarrow> pabr | _ \<Rightarrow> pnorm, [], t')
pcs (Suc i) = (case t'' of Abrupt s' \<Rightarrow> pabr | _ \<Rightarrow> pnorm)
pcss (Suc i) = []

goal (1 subgoal):
 1. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)
[PROOF STEP]
using pcss_i cs'' cs''_Nil f_i f_Suc_i
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> ([], [(pnorm, pabr)], t'') \<rightarrow> (case t'' of Abrupt s' \<Rightarrow> pabr | _ \<Rightarrow> pnorm, [], t')
pcs (Suc i) = (case t'' of Abrupt s' \<Rightarrow> pabr | _ \<Rightarrow> pnorm)
pcss (Suc i) = []
pcss i = [(pnorm, pabr)]
cs'' = pcs i
cs'' = []
f i = (cs'', css'', t'')
f (Suc i) = (cs', css', t')

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>i<Suc k. \<Gamma>\<turnstile> p i \<rightarrow> p (Suc i)

goal:
No subgoals!
[PROOF STEP]
qed


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


[STATEMENT]
lemma unfold_fold_1:
  "isotone f \<Longrightarrow> has_least_prefixpoint f \<Longrightarrow> apx.has_least_fixpoint f \<Longrightarrow> f(x) \<le> x \<Longrightarrow> \<kappa> f \<le> x \<squnion> L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isotone f; has_least_prefixpoint f; order.has_least_fixpoint (\<sqsubseteq>) f; f x \<le> x\<rbrakk> \<Longrightarrow> \<kappa> f \<le> x \<squnion> L
[PROOF STEP]
by (metis sup_left_isotone apx_def has_least_fixpoint_def is_least_prefixpoint_def least_prefixpoint_char least_prefixpoint_fixpoint order_trans pmu_mu kappa_apx_below_mu)


[STATEMENT]
lemma max_Var_floatariths_lessI: "i < max_Var_floatarith (fas ! j) \<Longrightarrow> j < length fas \<Longrightarrow> i < max_Var_floatariths fas"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i < max_Var_floatarith (fas ! j); j < length fas\<rbrakk> \<Longrightarrow> i < max_Var_floatariths fas
[PROOF STEP]
by (metis leD le_trans less_le max_Var_floatarith_le_max_Var_floatariths nth_mem)


[STATEMENT]
lemma isFDERIV_max_Var_congI: "isFDERIV n xs fas ws"
  if f: "isFDERIV n xs fas vs" and c: "(\<And>i. i < max_Var_floatariths fas \<Longrightarrow> vs ! i = ws ! i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isFDERIV n xs fas ws
[PROOF STEP]
using c f
[PROOF STATE]
proof (prove)
using this:
?i < max_Var_floatariths fas \<Longrightarrow> vs ! ?i = ws ! ?i
isFDERIV n xs fas vs

goal (1 subgoal):
 1. isFDERIV n xs fas ws
[PROOF STEP]
by (auto simp: isFDERIV_def max_Var_floatariths_lessI
      intro!: isFDERIV_I isDERIV_max_Var_floatarithI[OF isFDERIV_isDERIV_D[OF f]])


[STATEMENT]
lemma interpret_floatarith_FDERIV_floatariths:
  assumes iD: "isFDERIV DIM('a) [0..<DIM('a)] fas (list_of_eucl x)"
  assumes m: "max_Var_floatariths fas \<le> DIM('a)"
  assumes [simp]: "length fas = DIM('a)"
  shows "((\<lambda>x::'a::executable_euclidean_space.
    eucl_of_list
      (interpret_floatariths fas (list_of_eucl x))::'a) has_derivative
        (\<lambda>d. eucl_of_list (interpret_floatariths
         (FDERIV_floatariths fas [0..<DIM('a)] (map Var [DIM('a)..<2*DIM('a)]))
         (list_of_eucl x @ list_of_eucl d)))) (at x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. einterpret fas (list_of_eucl x)) has_derivative (\<lambda>d. einterpret (FDERIV_floatariths fas [0..<DIM('a)] (map Var [DIM('a)..<2 * DIM('a)])) (list_of_eucl x @ list_of_eucl d))) (at x)
[PROOF STEP]
using interpret_floatarith_FDERIV_floatariths_append[where ramsch=Nil, simplified, OF assms]
[PROOF STATE]
proof (prove)
using this:
((\<lambda>x. einterpret fas (list_of_eucl x)) has_derivative (\<lambda>d. einterpret (FDERIV_floatariths fas [0..<DIM('a)] (map Var [DIM('a)..<2 * DIM('a)])) (list_of_eucl x @ list_of_eucl d))) (at x)

goal (1 subgoal):
 1. ((\<lambda>x. einterpret fas (list_of_eucl x)) has_derivative (\<lambda>d. einterpret (FDERIV_floatariths fas [0..<DIM('a)] (map Var [DIM('a)..<2 * DIM('a)])) (list_of_eucl x @ list_of_eucl d))) (at x)
[PROOF STEP]
by simp


[STATEMENT]
lemma path_one_edge[simp]:
  "task1_1.path v1 v2 pth \<longleftrightarrow>
    (v1 = 0 \<and> v2 = 1 \<and> pth = [((0,Reg A),(1,plain_ant A))] \<or>
    pth = [] \<and> v1 = v2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. task1_1.path v1 v2 pth = (v1 = 0 \<and> v2 = 1 \<and> pth = [((0, Reg A), 1, plain_ant A)] \<or> pth = [] \<and> v1 = v2)
[PROOF STEP]
apply (cases pth)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. pth = [] \<Longrightarrow> task1_1.path v1 v2 pth = (v1 = 0 \<and> v2 = 1 \<and> pth = [((0, Reg A), 1, plain_ant A)] \<or> pth = [] \<and> v1 = v2)
 2. \<And>a list. pth = a # list \<Longrightarrow> task1_1.path v1 v2 pth = (v1 = 0 \<and> v2 = 1 \<and> pth = [((0, Reg A), 1, plain_ant A)] \<or> pth = [] \<and> v1 = v2)
[PROOF STEP]
apply (auto simp add: task1_1.path_cons_simp')
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>list. \<lbrakk>pth = ((0, Reg A), 1, plain_ant A) # list; task1_1.path 1 v2 list; v1 = 0\<rbrakk> \<Longrightarrow> v2 = 1
 2. \<And>list. \<lbrakk>pth = ((0, Reg A), 1, plain_ant A) # list; task1_1.path 1 v2 list; v1 = 0\<rbrakk> \<Longrightarrow> list = []
[PROOF STEP]
apply (rename_tac list, case_tac list, auto simp add: task1_1.path_cons_simp')+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma phase_zero [simp]: "phase 0 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. phase 0 = 0
[PROOF STEP]
by (simp add: phase_def)


[STATEMENT]
lemma fast_exp_7681_to_mod_ring:
"fast_exp_7681 x e = to_int_mod_ring ((of_int_mod_ring x :: fin7681 mod_ring)^e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fast_exp_7681 x e = to_int_mod_ring (of_int_mod_ring x ^ e)
[PROOF STEP]
proof (induct e arbitrary: x rule: fast_exp_7681.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x xa. fast_exp_7681 xa 0 = to_int_mod_ring (of_int_mod_ring xa ^ 0)
 2. \<And>x e xa. (\<And>x. fast_exp_7681 x e = to_int_mod_ring (of_int_mod_ring x ^ e)) \<Longrightarrow> fast_exp_7681 xa (Suc e) = to_int_mod_ring (of_int_mod_ring xa ^ Suc e)
[PROOF STEP]
case (2 x e)
[PROOF STATE]
proof (state)
this:
fast_exp_7681 ?x e = to_int_mod_ring (of_int_mod_ring ?x ^ e)

goal (2 subgoals):
 1. \<And>x xa. fast_exp_7681 xa 0 = to_int_mod_ring (of_int_mod_ring xa ^ 0)
 2. \<And>x e xa. (\<And>x. fast_exp_7681 x e = to_int_mod_ring (of_int_mod_ring x ^ e)) \<Longrightarrow> fast_exp_7681 xa (Suc e) = to_int_mod_ring (of_int_mod_ring xa ^ Suc e)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fast_exp_7681 ?x e = to_int_mod_ring (of_int_mod_ring ?x ^ e)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
fast_exp_7681 ?x e = to_int_mod_ring (of_int_mod_ring ?x ^ e)

goal (1 subgoal):
 1. fast_exp_7681 x (Suc e) = to_int_mod_ring (of_int_mod_ring x ^ Suc e)
[PROOF STEP]
by (metis Suc_inject fast_exp_7681.elims kyber7681.CARD_a kyber7681.of_int_mod_ring_mult
    nat.discI of_int_mod_ring.rep_eq of_int_mod_ring_to_int_mod_ring power_Suc
    to_int_mod_ring.rep_eq)
[PROOF STATE]
proof (state)
this:
fast_exp_7681 x (Suc e) = to_int_mod_ring (of_int_mod_ring x ^ Suc e)

goal (1 subgoal):
 1. \<And>x xa. fast_exp_7681 xa 0 = to_int_mod_ring (of_int_mod_ring xa ^ 0)
[PROOF STEP]
qed auto


[STATEMENT]
lemma mpoly_coeff_times_0: "coeff (p * q) 0 = coeff p 0 * coeff q 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MPoly_Type.coeff (p * q) 0 = MPoly_Type.coeff p 0 * MPoly_Type.coeff q 0
[PROOF STEP]
by (simp add: coeff_mpoly_times prod_fun_nat_0)


[STATEMENT]
lemma mpoly_map_vars_smult [simp]: "mpoly_map_vars f (smult c p) = smult c (mpoly_map_vars f p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mpoly_map_vars f (MPoly_Type.smult c p) = MPoly_Type.smult c (mpoly_map_vars f p)
[PROOF STEP]
by transfer (simp add: permutep_smult)


[STATEMENT]
lemma mpoly_map_vars_mult [simp]: "mpoly_map_vars f (p * q) = mpoly_map_vars f p * mpoly_map_vars f q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mpoly_map_vars f (p * q) = mpoly_map_vars f p * mpoly_map_vars f q
[PROOF STEP]
by transfer simp


[STATEMENT]
lemma lookup_sym_mpoly_aux:
  "Poly_Mapping.lookup (sym_mpoly_aux X k) mon =
     (if finite X \<and> (\<exists>Y. Y \<subseteq> X \<and> card Y = k \<and> mon = monom_of_set Y) then 1 else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup (sym_mpoly_aux X k) mon = (if finite X \<and> (\<exists>Y\<subseteq>X. card Y = k \<and> mon = monom_of_set Y) then 1::'a else (0::'a))
[PROOF STEP]
by transfer' simp