[STATEMENT]
lemma Fault_app_steps: "\<Gamma>\<turnstile>(cs@xs,css,Fault f) \<rightarrow>\<^sup>* (xs,css,Fault f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> (cs @ xs, css, Fault f) \<rightarrow>\<^sup>* (xs, css, Fault f)
[PROOF STEP]
proof (induct cs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<Gamma>\<turnstile> ([] @ xs, css, Fault f) \<rightarrow>\<^sup>* (xs, css, Fault f)
 2. \<And>a cs. \<Gamma>\<turnstile> (cs @ xs, css, Fault f) \<rightarrow>\<^sup>* (xs, css, Fault f) \<Longrightarrow> \<Gamma>\<turnstile> ((a # cs) @ xs, css, Fault f) \<rightarrow>\<^sup>* (xs, css, Fault f)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<Gamma>\<turnstile> ([] @ xs, css, Fault f) \<rightarrow>\<^sup>* (xs, css, Fault f)
 2. \<And>a cs. \<Gamma>\<turnstile> (cs @ xs, css, Fault f) \<rightarrow>\<^sup>* (xs, css, Fault f) \<Longrightarrow> \<Gamma>\<turnstile> ((a # cs) @ xs, css, Fault f) \<rightarrow>\<^sup>* (xs, css, Fault f)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> ([] @ xs, css, Fault f) \<rightarrow>\<^sup>* (xs, css, Fault f)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> ([] @ xs, css, Fault f) \<rightarrow>\<^sup>* (xs, css, Fault f)

goal (1 subgoal):
 1. \<And>a cs. \<Gamma>\<turnstile> (cs @ xs, css, Fault f) \<rightarrow>\<^sup>* (xs, css, Fault f) \<Longrightarrow> \<Gamma>\<turnstile> ((a # cs) @ xs, css, Fault f) \<rightarrow>\<^sup>* (xs, css, Fault f)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a cs. \<Gamma>\<turnstile> (cs @ xs, css, Fault f) \<rightarrow>\<^sup>* (xs, css, Fault f) \<Longrightarrow> \<Gamma>\<turnstile> ((a # cs) @ xs, css, Fault f) \<rightarrow>\<^sup>* (xs, css, Fault f)
[PROOF STEP]
case (Cons c cs)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (cs @ xs, css, Fault f) \<rightarrow>\<^sup>* (xs, css, Fault f)

goal (1 subgoal):
 1. \<And>a cs. \<Gamma>\<turnstile> (cs @ xs, css, Fault f) \<rightarrow>\<^sup>* (xs, css, Fault f) \<Longrightarrow> \<Gamma>\<turnstile> ((a # cs) @ xs, css, Fault f) \<rightarrow>\<^sup>* (xs, css, Fault f)
[PROOF STEP]
have "\<Gamma>\<turnstile>(c#cs@xs, css, Fault f) \<rightarrow>\<^sup>* (xs, css, Fault f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> (c # cs @ xs, css, Fault f) \<rightarrow>\<^sup>* (xs, css, Fault f)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> (c # cs @ xs, css, Fault f) \<rightarrow>\<^sup>* (xs, css, Fault f)
[PROOF STEP]
have "\<Gamma>\<turnstile>(c#cs@xs, css, Fault f) \<rightarrow> (cs@xs, css, Fault f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> (c # cs @ xs, css, Fault f) \<rightarrow> (cs @ xs, css, Fault f)
[PROOF STEP]
by (rule step.FaultProp)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (c # cs @ xs, css, Fault f) \<rightarrow> (cs @ xs, css, Fault f)

goal (1 subgoal):
 1. \<Gamma>\<turnstile> (c # cs @ xs, css, Fault f) \<rightarrow>\<^sup>* (xs, css, Fault f)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (c # cs @ xs, css, Fault f) \<rightarrow> (cs @ xs, css, Fault f)

goal (1 subgoal):
 1. \<Gamma>\<turnstile> (c # cs @ xs, css, Fault f) \<rightarrow>\<^sup>* (xs, css, Fault f)
[PROOF STEP]
have "\<Gamma>\<turnstile>(cs@xs, css, Fault f) \<rightarrow>\<^sup>* (xs, css, Fault f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> (cs @ xs, css, Fault f) \<rightarrow>\<^sup>* (xs, css, Fault f)
[PROOF STEP]
by (rule Cons.hyps)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (cs @ xs, css, Fault f) \<rightarrow>\<^sup>* (xs, css, Fault f)

goal (1 subgoal):
 1. \<Gamma>\<turnstile> (c # cs @ xs, css, Fault f) \<rightarrow>\<^sup>* (xs, css, Fault f)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> (c # cs @ xs, css, Fault f) \<rightarrow>\<^sup>* (xs, css, Fault f)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> (c # cs @ xs, css, Fault f) \<rightarrow>\<^sup>* (xs, css, Fault f)

goal (1 subgoal):
 1. \<Gamma>\<turnstile> (c # cs @ xs, css, Fault f) \<rightarrow>\<^sup>* (xs, css, Fault f)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (c # cs @ xs, css, Fault f) \<rightarrow>\<^sup>* (xs, css, Fault f)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (c # cs @ xs, css, Fault f) \<rightarrow>\<^sup>* (xs, css, Fault f)

goal (1 subgoal):
 1. \<And>a cs. \<Gamma>\<turnstile> (cs @ xs, css, Fault f) \<rightarrow>\<^sup>* (xs, css, Fault f) \<Longrightarrow> \<Gamma>\<turnstile> ((a # cs) @ xs, css, Fault f) \<rightarrow>\<^sup>* (xs, css, Fault f)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> (c # cs @ xs, css, Fault f) \<rightarrow>\<^sup>* (xs, css, Fault f)

goal (1 subgoal):
 1. \<Gamma>\<turnstile> ((c # cs) @ xs, css, Fault f) \<rightarrow>\<^sup>* (xs, css, Fault f)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> ((c # cs) @ xs, css, Fault f) \<rightarrow>\<^sup>* (xs, css, Fault f)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Stuck_app_steps: "\<Gamma>\<turnstile>(cs@xs,css,Stuck) \<rightarrow>\<^sup>* (xs,css,Stuck)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> (cs @ xs, css, Stuck) \<rightarrow>\<^sup>* (xs, css, Stuck)
[PROOF STEP]
proof (induct cs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<Gamma>\<turnstile> ([] @ xs, css, Stuck) \<rightarrow>\<^sup>* (xs, css, Stuck)
 2. \<And>a cs. \<Gamma>\<turnstile> (cs @ xs, css, Stuck) \<rightarrow>\<^sup>* (xs, css, Stuck) \<Longrightarrow> \<Gamma>\<turnstile> ((a # cs) @ xs, css, Stuck) \<rightarrow>\<^sup>* (xs, css, Stuck)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<Gamma>\<turnstile> ([] @ xs, css, Stuck) \<rightarrow>\<^sup>* (xs, css, Stuck)
 2. \<And>a cs. \<Gamma>\<turnstile> (cs @ xs, css, Stuck) \<rightarrow>\<^sup>* (xs, css, Stuck) \<Longrightarrow> \<Gamma>\<turnstile> ((a # cs) @ xs, css, Stuck) \<rightarrow>\<^sup>* (xs, css, Stuck)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> ([] @ xs, css, Stuck) \<rightarrow>\<^sup>* (xs, css, Stuck)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> ([] @ xs, css, Stuck) \<rightarrow>\<^sup>* (xs, css, Stuck)

goal (1 subgoal):
 1. \<And>a cs. \<Gamma>\<turnstile> (cs @ xs, css, Stuck) \<rightarrow>\<^sup>* (xs, css, Stuck) \<Longrightarrow> \<Gamma>\<turnstile> ((a # cs) @ xs, css, Stuck) \<rightarrow>\<^sup>* (xs, css, Stuck)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a cs. \<Gamma>\<turnstile> (cs @ xs, css, Stuck) \<rightarrow>\<^sup>* (xs, css, Stuck) \<Longrightarrow> \<Gamma>\<turnstile> ((a # cs) @ xs, css, Stuck) \<rightarrow>\<^sup>* (xs, css, Stuck)
[PROOF STEP]
case (Cons c cs)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (cs @ xs, css, Stuck) \<rightarrow>\<^sup>* (xs, css, Stuck)

goal (1 subgoal):
 1. \<And>a cs. \<Gamma>\<turnstile> (cs @ xs, css, Stuck) \<rightarrow>\<^sup>* (xs, css, Stuck) \<Longrightarrow> \<Gamma>\<turnstile> ((a # cs) @ xs, css, Stuck) \<rightarrow>\<^sup>* (xs, css, Stuck)
[PROOF STEP]
have "\<Gamma>\<turnstile>(c#cs@xs, css, Stuck) \<rightarrow>\<^sup>* (xs, css, Stuck)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> (c # cs @ xs, css, Stuck) \<rightarrow>\<^sup>* (xs, css, Stuck)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> (c # cs @ xs, css, Stuck) \<rightarrow>\<^sup>* (xs, css, Stuck)
[PROOF STEP]
have "\<Gamma>\<turnstile>(c#cs@xs, css, Stuck) \<rightarrow> (cs@xs, css, Stuck)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> (c # cs @ xs, css, Stuck) \<rightarrow> (cs @ xs, css, Stuck)
[PROOF STEP]
by (rule step.StuckProp)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (c # cs @ xs, css, Stuck) \<rightarrow> (cs @ xs, css, Stuck)

goal (1 subgoal):
 1. \<Gamma>\<turnstile> (c # cs @ xs, css, Stuck) \<rightarrow>\<^sup>* (xs, css, Stuck)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (c # cs @ xs, css, Stuck) \<rightarrow> (cs @ xs, css, Stuck)

goal (1 subgoal):
 1. \<Gamma>\<turnstile> (c # cs @ xs, css, Stuck) \<rightarrow>\<^sup>* (xs, css, Stuck)
[PROOF STEP]
have "\<Gamma>\<turnstile>(cs@xs, css, Stuck) \<rightarrow>\<^sup>* (xs, css, Stuck)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> (cs @ xs, css, Stuck) \<rightarrow>\<^sup>* (xs, css, Stuck)
[PROOF STEP]
by (rule Cons.hyps)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (cs @ xs, css, Stuck) \<rightarrow>\<^sup>* (xs, css, Stuck)

goal (1 subgoal):
 1. \<Gamma>\<turnstile> (c # cs @ xs, css, Stuck) \<rightarrow>\<^sup>* (xs, css, Stuck)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> (c # cs @ xs, css, Stuck) \<rightarrow>\<^sup>* (xs, css, Stuck)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> (c # cs @ xs, css, Stuck) \<rightarrow>\<^sup>* (xs, css, Stuck)

goal (1 subgoal):
 1. \<Gamma>\<turnstile> (c # cs @ xs, css, Stuck) \<rightarrow>\<^sup>* (xs, css, Stuck)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (c # cs @ xs, css, Stuck) \<rightarrow>\<^sup>* (xs, css, Stuck)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (c # cs @ xs, css, Stuck) \<rightarrow>\<^sup>* (xs, css, Stuck)

goal (1 subgoal):
 1. \<And>a cs. \<Gamma>\<turnstile> (cs @ xs, css, Stuck) \<rightarrow>\<^sup>* (xs, css, Stuck) \<Longrightarrow> \<Gamma>\<turnstile> ((a # cs) @ xs, css, Stuck) \<rightarrow>\<^sup>* (xs, css, Stuck)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> (c # cs @ xs, css, Stuck) \<rightarrow>\<^sup>* (xs, css, Stuck)

goal (1 subgoal):
 1. \<Gamma>\<turnstile> ((c # cs) @ xs, css, Stuck) \<rightarrow>\<^sup>* (xs, css, Stuck)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> ((c # cs) @ xs, css, Stuck) \<rightarrow>\<^sup>* (xs, css, Stuck)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma app_step:
  assumes step: "\<Gamma>\<turnstile>(cs,css,s) \<rightarrow> (cs',css',t)"
  shows "css=css' \<Longrightarrow> \<Gamma>\<turnstile>(cs@xs,css,s) \<rightarrow> (cs'@xs,css',t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. css = css' \<Longrightarrow> \<Gamma>\<turnstile> (cs @ xs, css, s) \<rightarrow> (cs' @ xs, css', t)
[PROOF STEP]
using step
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> (cs, css, s) \<rightarrow> (cs', css', t)

goal (1 subgoal):
 1. css = css' \<Longrightarrow> \<Gamma>\<turnstile> (cs @ xs, css, s) \<rightarrow> (cs' @ xs, css', t)
[PROOF STEP]
apply induct
[PROOF STATE]
proof (prove)
goal (23 subgoals):
 1. \<And>cs css s. css = css \<Longrightarrow> \<Gamma>\<turnstile> ((Skip # cs) @ xs, css, Normal s) \<rightarrow> (cs @ xs, css, Normal s)
 2. \<And>s g f c cs css. \<lbrakk>s \<in> g; css = css\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> ((Guard f g c # cs) @ xs, css, Normal s) \<rightarrow> ((c # cs) @ xs, css, Normal s)
 3. \<And>s g f c cs css. \<lbrakk>s \<notin> g; css = css\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> ((Guard f g c # cs) @ xs, css, Normal s) \<rightarrow> (cs @ xs, css, Fault f)
 4. \<And>c cs css f. css = css \<Longrightarrow> \<Gamma>\<turnstile> ((c # cs) @ xs, css, Fault f) \<rightarrow> (cs @ xs, css, Fault f)
 5. \<And>nrms abrs css f. (nrms, abrs) # css = css \<Longrightarrow> \<Gamma>\<turnstile> ([] @ xs, (nrms, abrs) # css, Fault f) \<rightarrow> (nrms @ xs, css, Fault f)
 6. \<And>c cs css s. css = css \<Longrightarrow> \<Gamma>\<turnstile> ((c # cs) @ xs, css, Abrupt s) \<rightarrow> (cs @ xs, css, Abrupt s)
 7. \<And>nrms abrs css s. (nrms, abrs) # css = css \<Longrightarrow> \<Gamma>\<turnstile> ([] @ xs, (nrms, abrs) # css, Normal s) \<rightarrow> (nrms @ xs, css, Normal s)
 8. \<And>nrms abrs css s. (nrms, abrs) # css = css \<Longrightarrow> \<Gamma>\<turnstile> ([] @ xs, (nrms, abrs) # css, Abrupt s) \<rightarrow> (abrs @ xs, css, Normal s)
 9. \<And>f cs css s. css = css \<Longrightarrow> \<Gamma>\<turnstile> ((Basic f # cs) @ xs, css, Normal s) \<rightarrow> (cs @ xs, css, Normal (f s))
 10. \<And>s t r cs css. \<lbrakk>(s, t) \<in> r; css = css\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> ((Spec r # cs) @ xs, css, Normal s) \<rightarrow> (cs @ xs, css, Normal t)
A total of 23 subgoals...
[PROOF STEP]
apply (simp_all del: fun_upd_apply,(blast intro: step.intros)+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma app_css_step:
  assumes step: "\<Gamma>\<turnstile>(cs,css,s) \<rightarrow> (cs',css',t)"
  shows "\<Gamma>\<turnstile>(cs,css@xs,s) \<rightarrow> (cs',css'@xs,t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> (cs, css @ xs, s) \<rightarrow> (cs', css' @ xs, t)
[PROOF STEP]
using step
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> (cs, css, s) \<rightarrow> (cs', css', t)

goal (1 subgoal):
 1. \<Gamma>\<turnstile> (cs, css @ xs, s) \<rightarrow> (cs', css' @ xs, t)
[PROOF STEP]
apply induct
[PROOF STATE]
proof (prove)
goal (23 subgoals):
 1. \<And>cs css s. \<Gamma>\<turnstile> (Skip # cs, css @ xs, Normal s) \<rightarrow> (cs, css @ xs, Normal s)
 2. \<And>s g f c cs css. s \<in> g \<Longrightarrow> \<Gamma>\<turnstile> (Guard f g c # cs, css @ xs, Normal s) \<rightarrow> (c # cs, css @ xs, Normal s)
 3. \<And>s g f c cs css. s \<notin> g \<Longrightarrow> \<Gamma>\<turnstile> (Guard f g c # cs, css @ xs, Normal s) \<rightarrow> (cs, css @ xs, Fault f)
 4. \<And>c cs css f. \<Gamma>\<turnstile> (c # cs, css @ xs, Fault f) \<rightarrow> (cs, css @ xs, Fault f)
 5. \<And>nrms abrs css f. \<Gamma>\<turnstile> ([], ((nrms, abrs) # css) @ xs, Fault f) \<rightarrow> (nrms, css @ xs, Fault f)
 6. \<And>c cs css s. \<Gamma>\<turnstile> (c # cs, css @ xs, Abrupt s) \<rightarrow> (cs, css @ xs, Abrupt s)
 7. \<And>nrms abrs css s. \<Gamma>\<turnstile> ([], ((nrms, abrs) # css) @ xs, Normal s) \<rightarrow> (nrms, css @ xs, Normal s)
 8. \<And>nrms abrs css s. \<Gamma>\<turnstile> ([], ((nrms, abrs) # css) @ xs, Abrupt s) \<rightarrow> (abrs, css @ xs, Normal s)
 9. \<And>f cs css s. \<Gamma>\<turnstile> (Basic f # cs, css @ xs, Normal s) \<rightarrow> (cs, css @ xs, Normal (f s))
 10. \<And>s t r cs css. (s, t) \<in> r \<Longrightarrow> \<Gamma>\<turnstile> (Spec r # cs, css @ xs, Normal s) \<rightarrow> (cs, css @ xs, Normal t)
A total of 23 subgoals...
[PROOF STEP]
apply (simp_all del: fun_upd_apply,(blast intro: step.intros)+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma app_css_steps:
  assumes step: "\<Gamma>\<turnstile>(cs,css,s) \<rightarrow>\<^sup>+ (cs',css',t)"
  shows "\<Gamma>\<turnstile>(cs,css@xs,s) \<rightarrow>\<^sup>+ (cs',css'@xs,t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> (cs, css @ xs, s) \<rightarrow>\<^sup>+ (cs', css' @ xs, t)
[PROOF STEP]
apply(rule trancl_induct3 [OF step])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a aa b. \<Gamma>\<turnstile> (cs, css, s) \<rightarrow> (a, aa, b) \<Longrightarrow> \<Gamma>\<turnstile> (cs, css @ xs, s) \<rightarrow>\<^sup>+ (a, aa @ xs, b)
 2. \<And>a aa b ab ac ba. \<lbrakk>\<Gamma>\<turnstile> (cs, css, s) \<rightarrow>\<^sup>+ (a, aa, b); \<Gamma>\<turnstile> (a, aa, b) \<rightarrow> (ab, ac, ba); \<Gamma>\<turnstile> (cs, css @ xs, s) \<rightarrow>\<^sup>+ (a, aa @ xs, b)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (cs, css @ xs, s) \<rightarrow>\<^sup>+ (ab, ac @ xs, ba)
[PROOF STEP]
apply (rule app_css_step [THEN tranclp.r_into_trancl [of "step \<Gamma>"]],assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa b ab ac ba. \<lbrakk>\<Gamma>\<turnstile> (cs, css, s) \<rightarrow>\<^sup>+ (a, aa, b); \<Gamma>\<turnstile> (a, aa, b) \<rightarrow> (ab, ac, ba); \<Gamma>\<turnstile> (cs, css @ xs, s) \<rightarrow>\<^sup>+ (a, aa @ xs, b)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (cs, css @ xs, s) \<rightarrow>\<^sup>+ (ab, ac @ xs, ba)
[PROOF STEP]
apply(blast intro:app_css_step tranclp_trans)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma step_Cons':
  assumes step: "\<Gamma>\<turnstile>(ccs,css,s) \<rightarrow> (cs',css',t)"
  shows
  "\<And>c cs. ccs=c#cs \<Longrightarrow> \<exists>css''. css'=css''@css \<and>
      (if css''=[] then \<exists>p. cs'=p@cs
       else (\<exists>pnorm pabr. css''=[(pnorm@cs,pabr@cs)]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c cs. ccs = c # cs \<Longrightarrow> \<exists>css''. css' = css'' @ css \<and> (if css'' = [] then \<exists>p. cs' = p @ cs else \<exists>pnorm pabr. css'' = [(pnorm @ cs, pabr @ cs)])
[PROOF STEP]
using step
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> (ccs, css, s) \<rightarrow> (cs', css', t)

goal (1 subgoal):
 1. \<And>c cs. ccs = c # cs \<Longrightarrow> \<exists>css''. css' = css'' @ css \<and> (if css'' = [] then \<exists>p. cs' = p @ cs else \<exists>pnorm pabr. css'' = [(pnorm @ cs, pabr @ cs)])
[PROOF STEP]
by induct force+


[STATEMENT]
lemma step_Cons:
  assumes step: "\<Gamma>\<turnstile>(c#cs,css,s) \<rightarrow> (cs',css',t)"
  shows "\<exists>pcss. css'=pcss@css \<and>
         (if pcss=[] then \<exists>ps. cs'=ps@cs
          else (\<exists>pcs_normal pcs_abrupt. pcss=[(pcs_normal@cs,pcs_abrupt@cs)]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>pcss. css' = pcss @ css \<and> (if pcss = [] then \<exists>ps. cs' = ps @ cs else \<exists>pcs_normal pcs_abrupt. pcss = [(pcs_normal @ cs, pcs_abrupt @ cs)])
[PROOF STEP]
using step_Cons' [OF step]
[PROOF STATE]
proof (prove)
using this:
c # cs = ?c # ?cs \<Longrightarrow> \<exists>css''. css' = css'' @ css \<and> (if css'' = [] then \<exists>p. cs' = p @ ?cs else \<exists>pnorm pabr. css'' = [(pnorm @ ?cs, pabr @ ?cs)])

goal (1 subgoal):
 1. \<exists>pcss. css' = pcss @ css \<and> (if pcss = [] then \<exists>ps. cs' = ps @ cs else \<exists>pcs_normal pcs_abrupt. pcss = [(pcs_normal @ cs, pcs_abrupt @ cs)])
[PROOF STEP]
by blast


[STATEMENT]
lemma step_Nil':
  assumes step: "\<Gamma>\<turnstile>(cs,asscss,s) \<rightarrow> (cs',css',t)"
  shows
  "\<And>ass. \<lbrakk>cs=[]; asscss=ass@css; ass\<noteq>Nil\<rbrakk> \<Longrightarrow>
          css'=tl ass@css \<and>
          (case s of
             Abrupt s' \<Rightarrow> cs'=snd (hd ass) \<and> t=Normal s'
           |  _ \<Rightarrow> cs'=fst (hd ass) \<and> t=s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ass. \<lbrakk>cs = []; asscss = ass @ css; ass \<noteq> []\<rbrakk> \<Longrightarrow> css' = tl ass @ css \<and> (case s of Abrupt s' \<Rightarrow> cs' = snd (hd ass) \<and> t = Normal s' | _ \<Rightarrow> cs' = fst (hd ass) \<and> t = s)
[PROOF STEP]
using step
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> (cs, asscss, s) \<rightarrow> (cs', css', t)

goal (1 subgoal):
 1. \<And>ass. \<lbrakk>cs = []; asscss = ass @ css; ass \<noteq> []\<rbrakk> \<Longrightarrow> css' = tl ass @ css \<and> (case s of Abrupt s' \<Rightarrow> cs' = snd (hd ass) \<and> t = Normal s' | _ \<Rightarrow> cs' = fst (hd ass) \<and> t = s)
[PROOF STEP]
by (induct) (fastforce simp add: neq_Nil_conv)+


[STATEMENT]
lemma step_Nil:
  assumes step: "\<Gamma>\<turnstile>([],ass@css,s) \<rightarrow> (cs',css',t)"
  assumes ass_not_Nil: "ass\<noteq>[]"
  shows "css'=tl ass@css \<and>
          (case s of
             Abrupt s' \<Rightarrow> cs'=snd (hd ass) \<and> t=Normal s'
           |  _ \<Rightarrow> cs'=fst (hd ass) \<and> t=s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. css' = tl ass @ css \<and> (case s of Abrupt s' \<Rightarrow> cs' = snd (hd ass) \<and> t = Normal s' | _ \<Rightarrow> cs' = fst (hd ass) \<and> t = s)
[PROOF STEP]
using step_Nil' [OF step _ _ ass_not_Nil]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>[] = []; ass @ css = ass @ ?css\<rbrakk> \<Longrightarrow> css' = tl ass @ ?css \<and> (case s of Abrupt s' \<Rightarrow> cs' = snd (hd ass) \<and> t = Normal s' | _ \<Rightarrow> cs' = fst (hd ass) \<and> t = s)

goal (1 subgoal):
 1. css' = tl ass @ css \<and> (case s of Abrupt s' \<Rightarrow> cs' = snd (hd ass) \<and> t = Normal s' | _ \<Rightarrow> cs' = fst (hd ass) \<and> t = s)
[PROOF STEP]
by simp


[STATEMENT]
lemma step_Nil'':
  assumes step: "\<Gamma>\<turnstile>([],(pcs_normal,pcs_abrupt)#pcss@css,s) \<rightarrow> (cs',pcss@css,t)"
  shows "(case s of
             Abrupt s' \<Rightarrow> cs'=pcs_abrupt \<and> t=Normal s'
           |  _ \<Rightarrow> cs'=pcs_normal \<and> t=s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. case s of Abrupt s' \<Rightarrow> cs' = pcs_abrupt \<and> t = Normal s' | _ \<Rightarrow> cs' = pcs_normal \<and> t = s
[PROOF STEP]
using step_Nil' [OF step, where ass ="(pcs_normal,pcs_abrupt)#pcss" and css="css"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>[] = []; (pcs_normal, pcs_abrupt) # pcss @ css = ((pcs_normal, pcs_abrupt) # pcss) @ css; (pcs_normal, pcs_abrupt) # pcss \<noteq> []\<rbrakk> \<Longrightarrow> pcss @ css = tl ((pcs_normal, pcs_abrupt) # pcss) @ css \<and> (case s of Abrupt s' \<Rightarrow> cs' = snd (hd ((pcs_normal, pcs_abrupt) # pcss)) \<and> t = Normal s' | _ \<Rightarrow> cs' = fst (hd ((pcs_normal, pcs_abrupt) # pcss)) \<and> t = s)

goal (1 subgoal):
 1. case s of Abrupt s' \<Rightarrow> cs' = pcs_abrupt \<and> t = Normal s' | _ \<Rightarrow> cs' = pcs_normal \<and> t = s
[PROOF STEP]
by (auto split: xstate.splits)


[STATEMENT]
lemma drop_suffix_css_step':
assumes step: "\<Gamma>\<turnstile>(cs,cssxs,s) \<rightarrow> (cs',css'xs,t)"
shows "\<And>css css' xs. \<lbrakk>cssxs = css@xs; css'xs=css'@xs\<rbrakk>
     \<Longrightarrow> \<Gamma>\<turnstile>(cs,css,s) \<rightarrow> (cs',css',t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>css css' xs. \<lbrakk>cssxs = css @ xs; css'xs = css' @ xs\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (cs, css, s) \<rightarrow> (cs', css', t)
[PROOF STEP]
using step
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> (cs, cssxs, s) \<rightarrow> (cs', css'xs, t)

goal (1 subgoal):
 1. \<And>css css' xs. \<lbrakk>cssxs = css @ xs; css'xs = css' @ xs\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (cs, css, s) \<rightarrow> (cs', css', t)
[PROOF STEP]
apply induct
[PROOF STATE]
proof (prove)
goal (23 subgoals):
 1. \<And>cs css s cssa css' xs. \<lbrakk>css = cssa @ xs; css = css' @ xs\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Skip # cs, cssa, Normal s) \<rightarrow> (cs, css', Normal s)
 2. \<And>s g f c cs css cssa css' xs. \<lbrakk>s \<in> g; css = cssa @ xs; css = css' @ xs\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Guard f g c # cs, cssa, Normal s) \<rightarrow> (c # cs, css', Normal s)
 3. \<And>s g f c cs css cssa css' xs. \<lbrakk>s \<notin> g; css = cssa @ xs; css = css' @ xs\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Guard f g c # cs, cssa, Normal s) \<rightarrow> (cs, css', Fault f)
 4. \<And>c cs css f cssa css' xs. \<lbrakk>css = cssa @ xs; css = css' @ xs\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (c # cs, cssa, Fault f) \<rightarrow> (cs, css', Fault f)
 5. \<And>nrms abrs css f cssa css' xs. \<lbrakk>(nrms, abrs) # css = cssa @ xs; css = css' @ xs\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> ([], cssa, Fault f) \<rightarrow> (nrms, css', Fault f)
 6. \<And>c cs css s cssa css' xs. \<lbrakk>css = cssa @ xs; css = css' @ xs\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (c # cs, cssa, Abrupt s) \<rightarrow> (cs, css', Abrupt s)
 7. \<And>nrms abrs css s cssa css' xs. \<lbrakk>(nrms, abrs) # css = cssa @ xs; css = css' @ xs\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> ([], cssa, Normal s) \<rightarrow> (nrms, css', Normal s)
 8. \<And>nrms abrs css s cssa css' xs. \<lbrakk>(nrms, abrs) # css = cssa @ xs; css = css' @ xs\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> ([], cssa, Abrupt s) \<rightarrow> (abrs, css', Normal s)
 9. \<And>f cs css s cssa css' xs. \<lbrakk>css = cssa @ xs; css = css' @ xs\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Basic f # cs, cssa, Normal s) \<rightarrow> (cs, css', Normal (f s))
 10. \<And>s t r cs css cssa css' xs. \<lbrakk>(s, t) \<in> r; css = cssa @ xs; css = css' @ xs\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (Spec r # cs, cssa, Normal s) \<rightarrow> (cs, css', Normal t)
A total of 23 subgoals...
[PROOF STEP]
apply (fastforce intro: step.intros)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma drop_suffix_css_step:
assumes step: "\<Gamma>\<turnstile>(cs,pcss@css,s) \<rightarrow> (cs',pcss'@css,t)"
shows "\<Gamma>\<turnstile>(cs,pcss,s) \<rightarrow> (cs',pcss',t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> (cs, pcss, s) \<rightarrow> (cs', pcss', t)
[PROOF STEP]
using step
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> (cs, pcss @ css, s) \<rightarrow> (cs', pcss' @ css, t)

goal (1 subgoal):
 1. \<Gamma>\<turnstile> (cs, pcss, s) \<rightarrow> (cs', pcss', t)
[PROOF STEP]
by (blast intro: drop_suffix_css_step')


[STATEMENT]
lemma drop_suffix_hd_css_step':
  assumes step: "\<Gamma>\<turnstile> (pcs,css,s) \<rightarrow> (cs',css'css,t)"
  shows "\<And>p ps cs pnorm pabr. \<lbrakk>pcs=p#ps@cs; css'css=(pnorm@cs,pabr@cs)#css\<rbrakk>
         \<Longrightarrow> \<Gamma>\<turnstile> (p#ps,css,s) \<rightarrow> (cs',(pnorm,pabr)#css,t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p ps cs pnorm pabr. \<lbrakk>pcs = p # ps @ cs; css'css = (pnorm @ cs, pabr @ cs) # css\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (p # ps, css, s) \<rightarrow> (cs', (pnorm, pabr) # css, t)
[PROOF STEP]
using step
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> (pcs, css, s) \<rightarrow> (cs', css'css, t)

goal (1 subgoal):
 1. \<And>p ps cs pnorm pabr. \<lbrakk>pcs = p # ps @ cs; css'css = (pnorm @ cs, pabr @ cs) # css\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (p # ps, css, s) \<rightarrow> (cs', (pnorm, pabr) # css, t)
[PROOF STEP]
by induct (force intro: step.intros)+


[STATEMENT]
lemma drop_suffix_hd_css_step'':
  assumes step: "\<Gamma>\<turnstile> (p#ps@cs,css,s) \<rightarrow> (cs',(pnorm@cs,pabr@cs)#css,t)"
  shows  "\<Gamma>\<turnstile> (p#ps,css,s) \<rightarrow> (cs',(pnorm,pabr)#css,t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> (p # ps, css, s) \<rightarrow> (cs', (pnorm, pabr) # css, t)
[PROOF STEP]
using drop_suffix_hd_css_step' [OF step]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>p # ps @ cs = ?p # ?ps @ ?cs; (pnorm @ cs, pabr @ cs) # css = (?pnorm @ ?cs, ?pabr @ ?cs) # css\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?p # ?ps, css, s) \<rightarrow> (cs', (?pnorm, ?pabr) # css, t)

goal (1 subgoal):
 1. \<Gamma>\<turnstile> (p # ps, css, s) \<rightarrow> (cs', (pnorm, pabr) # css, t)
[PROOF STEP]
by auto


[STATEMENT]
lemma drop_suffix_hd_css_step:
  assumes step: "\<Gamma>\<turnstile> (p#ps@cs,css,s) \<rightarrow> (cs',[(pnorm@ps@cs,pabr@ps@cs)]@css,t)"
  shows  "\<Gamma>\<turnstile> (p#ps,css,s) \<rightarrow> (cs',[(pnorm@ps,pabr@ps)]@css,t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> (p # ps, css, s) \<rightarrow> (cs', [(pnorm @ ps, pabr @ ps)] @ css, t)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> (p # ps, css, s) \<rightarrow> (cs', [(pnorm @ ps, pabr @ ps)] @ css, t)
[PROOF STEP]
from step drop_suffix_hd_css_step'' [of _ p ps cs css s cs' "pnorm@ps" "pabr@ps" t]
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> (p # ps @ cs, css, s) \<rightarrow> (cs', [(pnorm @ ps @ cs, pabr @ ps @ cs)] @ css, t)
?\<Gamma>\<turnstile> (p # ps @ cs, css, s) \<rightarrow> (cs', ((pnorm @ ps) @ cs, (pabr @ ps) @ cs) # css, t) \<Longrightarrow> ?\<Gamma>\<turnstile> (p # ps, css, s) \<rightarrow> (cs', (pnorm @ ps, pabr @ ps) # css, t)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> (p # ps @ cs, css, s) \<rightarrow> (cs', [(pnorm @ ps @ cs, pabr @ ps @ cs)] @ css, t)
?\<Gamma>\<turnstile> (p # ps @ cs, css, s) \<rightarrow> (cs', ((pnorm @ ps) @ cs, (pabr @ ps) @ cs) # css, t) \<Longrightarrow> ?\<Gamma>\<turnstile> (p # ps, css, s) \<rightarrow> (cs', (pnorm @ ps, pabr @ ps) # css, t)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma drop_suffix':
  assumes step: "\<Gamma>\<turnstile>(csxs,css,s) \<rightarrow> (cs'xs,css',t)"
  shows "\<And>xs cs cs'. \<lbrakk>css=css'; csxs=cs@xs; cs'xs = cs'@xs; cs\<noteq>[] \<rbrakk>
         \<Longrightarrow> \<Gamma>\<turnstile>(cs,css,s) \<rightarrow> (cs',css,t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs cs cs'. \<lbrakk>css = css'; csxs = cs @ xs; cs'xs = cs' @ xs; cs \<noteq> []\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (cs, css, s) \<rightarrow> (cs', css, t)
[PROOF STEP]
using step
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> (csxs, css, s) \<rightarrow> (cs'xs, css', t)

goal (1 subgoal):
 1. \<And>xs cs cs'. \<lbrakk>css = css'; csxs = cs @ xs; cs'xs = cs' @ xs; cs \<noteq> []\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (cs, css, s) \<rightarrow> (cs', css, t)
[PROOF STEP]
apply induct
[PROOF STATE]
proof (prove)
goal (23 subgoals):
 1. \<And>cs css s xs csa cs'. \<lbrakk>css = css; Skip # cs = csa @ xs; cs = cs' @ xs; csa \<noteq> []\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (csa, css, Normal s) \<rightarrow> (cs', css, Normal s)
 2. \<And>s g f c cs css xs csa cs'. \<lbrakk>s \<in> g; css = css; Guard f g c # cs = csa @ xs; c # cs = cs' @ xs; csa \<noteq> []\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (csa, css, Normal s) \<rightarrow> (cs', css, Normal s)
 3. \<And>s g f c cs css xs csa cs'. \<lbrakk>s \<notin> g; css = css; Guard f g c # cs = csa @ xs; cs = cs' @ xs; csa \<noteq> []\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (csa, css, Normal s) \<rightarrow> (cs', css, Fault f)
 4. \<And>c cs css f xs csa cs'. \<lbrakk>css = css; c # cs = csa @ xs; cs = cs' @ xs; csa \<noteq> []\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (csa, css, Fault f) \<rightarrow> (cs', css, Fault f)
 5. \<And>nrms abrs css f xs cs cs'. \<lbrakk>(nrms, abrs) # css = css; [] = cs @ xs; nrms = cs' @ xs; cs \<noteq> []\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (cs, (nrms, abrs) # css, Fault f) \<rightarrow> (cs', (nrms, abrs) # css, Fault f)
 6. \<And>c cs css s xs csa cs'. \<lbrakk>css = css; c # cs = csa @ xs; cs = cs' @ xs; csa \<noteq> []\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (csa, css, Abrupt s) \<rightarrow> (cs', css, Abrupt s)
 7. \<And>nrms abrs css s xs cs cs'. \<lbrakk>(nrms, abrs) # css = css; [] = cs @ xs; nrms = cs' @ xs; cs \<noteq> []\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (cs, (nrms, abrs) # css, Normal s) \<rightarrow> (cs', (nrms, abrs) # css, Normal s)
 8. \<And>nrms abrs css s xs cs cs'. \<lbrakk>(nrms, abrs) # css = css; [] = cs @ xs; abrs = cs' @ xs; cs \<noteq> []\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (cs, (nrms, abrs) # css, Abrupt s) \<rightarrow> (cs', (nrms, abrs) # css, Normal s)
 9. \<And>f cs css s xs csa cs'. \<lbrakk>css = css; Basic f # cs = csa @ xs; cs = cs' @ xs; csa \<noteq> []\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (csa, css, Normal s) \<rightarrow> (cs', css, Normal (f s))
 10. \<And>s t r cs css xs csa cs'. \<lbrakk>(s, t) \<in> r; css = css; Spec r # cs = csa @ xs; cs = cs' @ xs; csa \<noteq> []\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (csa, css, Normal s) \<rightarrow> (cs', css, Normal t)
A total of 23 subgoals...
[PROOF STEP]
apply (fastforce intro: step.intros simp add: neq_Nil_conv)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma drop_suffix:
  assumes step: "\<Gamma>\<turnstile>(c#cs@xs,css,s) \<rightarrow> (cs'@xs,css,t)"
  shows "\<Gamma>\<turnstile>(c#cs,css,s) \<rightarrow> (cs',css,t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> (c # cs, css, s) \<rightarrow> (cs', css, t)
[PROOF STEP]
by(rule drop_suffix' [OF step _ _ _]) auto


[STATEMENT]
lemma drop_suffix_same_css_step:
  assumes step: "\<Gamma>\<turnstile>(cs@xs,css,s) \<rightarrow> (cs'@xs,css,t)"
  assumes not_Nil: "cs\<noteq>[]"
  shows "\<Gamma>\<turnstile>(cs,xss,s) \<rightarrow> (cs',xss,t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> (cs, xss, s) \<rightarrow> (cs', xss, t)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> (cs, xss, s) \<rightarrow> (cs', xss, t)
[PROOF STEP]
from drop_suffix' [OF step _ _ _ not_Nil]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>css = css; cs @ xs = cs @ ?xs; cs' @ xs = ?cs' @ ?xs\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (cs, css, s) \<rightarrow> (?cs', css, t)
[PROOF STEP]
have "\<Gamma>\<turnstile>(cs,css,s) \<rightarrow> (cs',css,t)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>css = css; cs @ xs = cs @ ?xs; cs' @ xs = ?cs' @ ?xs\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (cs, css, s) \<rightarrow> (?cs', css, t)

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

goal (1 subgoal):
 1. \<Gamma>\<turnstile> (cs, xss, s) \<rightarrow> (cs', xss, t)
[PROOF STEP]
with drop_suffix_css_step [of _ cs "[]" css s cs' "[]" t]
[PROOF STATE]
proof (chain)
picking this:
?\<Gamma>\<turnstile> (cs, [] @ css, s) \<rightarrow> (cs', [] @ css, t) \<Longrightarrow> ?\<Gamma>\<turnstile> (cs, [], s) \<rightarrow> (cs', [], t)
\<Gamma>\<turnstile> (cs, css, s) \<rightarrow> (cs', css, t)
[PROOF STEP]
have "\<Gamma>\<turnstile> (cs, [], s) \<rightarrow> (cs', [], t)"
[PROOF STATE]
proof (prove)
using this:
?\<Gamma>\<turnstile> (cs, [] @ css, s) \<rightarrow> (cs', [] @ css, t) \<Longrightarrow> ?\<Gamma>\<turnstile> (cs, [], s) \<rightarrow> (cs', [], t)
\<Gamma>\<turnstile> (cs, css, s) \<rightarrow> (cs', css, t)

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

goal (1 subgoal):
 1. \<Gamma>\<turnstile> (cs, xss, s) \<rightarrow> (cs', xss, t)
[PROOF STEP]
from app_css_step [OF this]
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> (cs, [] @ ?xs, s) \<rightarrow> (cs', [] @ ?xs, t)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> (cs, [] @ ?xs, s) \<rightarrow> (cs', [] @ ?xs, t)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Cons_change_css_step:
  assumes step: "\<Gamma>\<turnstile> (cs,css,s) \<rightarrow> (cs',css'@css,t)"
  shows "\<Gamma>\<turnstile> (cs,xss,s) \<rightarrow> (cs',css'@xss,t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> (cs, xss, s) \<rightarrow> (cs', css' @ xss, t)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> (cs, xss, s) \<rightarrow> (cs', css' @ xss, t)
[PROOF STEP]
from step
    drop_suffix_css_step [where cs=cs and pcss="[]" and css=css and s=s
                             and cs'=cs' and pcss'=css' and t=t]
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> (cs, css, s) \<rightarrow> (cs', css' @ css, t)
?\<Gamma>\<turnstile> (cs, [] @ css, s) \<rightarrow> (cs', css' @ css, t) \<Longrightarrow> ?\<Gamma>\<turnstile> (cs, [], s) \<rightarrow> (cs', css', t)
[PROOF STEP]
have "\<Gamma>\<turnstile> (cs, [], s) \<rightarrow> (cs', css', t)"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> (cs, css, s) \<rightarrow> (cs', css' @ css, t)
?\<Gamma>\<turnstile> (cs, [] @ css, s) \<rightarrow> (cs', css' @ css, t) \<Longrightarrow> ?\<Gamma>\<turnstile> (cs, [], s) \<rightarrow> (cs', css', t)

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

goal (1 subgoal):
 1. \<Gamma>\<turnstile> (cs, xss, s) \<rightarrow> (cs', css' @ xss, t)
[PROOF STEP]
from app_css_step [where xs=xss, OF this]
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> (cs, [] @ xss, s) \<rightarrow> (cs', css' @ xss, t)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> (cs, [] @ xss, s) \<rightarrow> (cs', css' @ xss, t)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Nil_change_css_step:
  assumes step: "\<Gamma>\<turnstile>([],ass@css,s) \<rightarrow> (cs',ass'@css,t)"
  assumes ass_not_Nil: "ass\<noteq>[]"
  shows "\<Gamma>\<turnstile>([],ass@xss,s) \<rightarrow> (cs',ass'@xss,t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> ([], ass @ xss, s) \<rightarrow> (cs', ass' @ xss, t)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> ([], ass @ xss, s) \<rightarrow> (cs', ass' @ xss, t)
[PROOF STEP]
from step drop_suffix_css_step [of _ "[]" ass css s cs' ass' t]
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> ([], ass @ css, s) \<rightarrow> (cs', ass' @ css, t)
?\<Gamma>\<turnstile> ([], ass @ css, s) \<rightarrow> (cs', ass' @ css, t) \<Longrightarrow> ?\<Gamma>\<turnstile> ([], ass, s) \<rightarrow> (cs', ass', t)
[PROOF STEP]
have "\<Gamma>\<turnstile> ([], ass, s) \<rightarrow> (cs', ass', t)"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> ([], ass @ css, s) \<rightarrow> (cs', ass' @ css, t)
?\<Gamma>\<turnstile> ([], ass @ css, s) \<rightarrow> (cs', ass' @ css, t) \<Longrightarrow> ?\<Gamma>\<turnstile> ([], ass, s) \<rightarrow> (cs', ass', t)

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

goal (1 subgoal):
 1. \<Gamma>\<turnstile> ([], ass @ xss, s) \<rightarrow> (cs', ass' @ xss, t)
[PROOF STEP]
from app_css_step [where xs=xss, OF this]
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> ([], ass @ xss, s) \<rightarrow> (cs', ass' @ xss, t)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> ([], ass @ xss, s) \<rightarrow> (cs', ass' @ xss, t)

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

goal:
No subgoals!
[PROOF STEP]
qed