[STATEMENT]
lemma conf_trace_induct_final[consumes 1, case_names trace_nil trace_cons]:
  "(\<Gamma>, e, S) \<Rightarrow>\<^sup>*\<^bsub>T\<^esub> final \<Longrightarrow> (\<And> \<Gamma> e S. final = (\<Gamma>, e, S) \<Longrightarrow> P \<Gamma> e S [] (\<Gamma>, e, S)) \<Longrightarrow> (\<And>\<Gamma> e S T \<Gamma>' e' S'. (\<Gamma>', e', S') \<Rightarrow>\<^sup>*\<^bsub>T\<^esub> final \<Longrightarrow> P \<Gamma>' e' S' T final \<Longrightarrow> (\<Gamma>, e, S) \<Rightarrow> (\<Gamma>', e', S') \<Longrightarrow> P \<Gamma> e S ((\<Gamma>', e', S') # T) final) \<Longrightarrow> P \<Gamma> e S T final"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<Gamma>, e, S) \<Rightarrow>\<^sup>*\<^bsub>T\<^esub> final; \<And>\<Gamma> e S. final = (\<Gamma>, e, S) \<Longrightarrow> P \<Gamma> e S [] (\<Gamma>, e, S); \<And>\<Gamma> e S T \<Gamma>' e' S'. \<lbrakk>(\<Gamma>', e', S') \<Rightarrow>\<^sup>*\<^bsub>T\<^esub> final; P \<Gamma>' e' S' T final; (\<Gamma>, e, S) \<Rightarrow> (\<Gamma>', e', S')\<rbrakk> \<Longrightarrow> P \<Gamma> e S ((\<Gamma>', e', S') # T) final\<rbrakk> \<Longrightarrow> P \<Gamma> e S T final
[PROOF STEP]
by (induction "(\<Gamma>, e, S)" T final arbitrary: \<Gamma> e S rule: trace_induct_final) auto


[STATEMENT]
lemma isVal_stops:
  assumes "isVal e"
  assumes "(\<Gamma>, e, S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^esub> (\<Delta>, z, S)"
  shows "T=[]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T = []
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
isVal e
(\<Gamma>, e, S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^esub> (\<Delta>, z, S)

goal (1 subgoal):
 1. T = []
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isVal e; (\<Gamma>, e, S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^esub> (\<Delta>, z, S)\<rbrakk> \<Longrightarrow> T = []
[PROOF STEP]
apply (erule balE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isVal e; (\<Gamma>, e, S) \<Rightarrow>\<^sup>*\<^bsub>T\<^esub> (\<Delta>, z, S); \<forall>c'\<in>set T. stack (\<Gamma>, e, S) \<lesssim> stack c'; stack (\<Delta>, z, S) = stack (\<Gamma>, e, S)\<rbrakk> \<Longrightarrow> T = []
[PROOF STEP]
apply (erule trace.cases)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>final. \<lbrakk>isVal e; \<forall>c'\<in>set T. stack (\<Gamma>, e, S) \<lesssim> stack c'; stack (\<Delta>, z, S) = stack (\<Gamma>, e, S); (\<Gamma>, e, S) = final; T = []; (\<Delta>, z, S) = final\<rbrakk> \<Longrightarrow> T = []
 2. \<And>conf' Ta final conf. \<lbrakk>isVal e; \<forall>c'\<in>set T. stack (\<Gamma>, e, S) \<lesssim> stack c'; stack (\<Delta>, z, S) = stack (\<Gamma>, e, S); (\<Gamma>, e, S) = conf; T = conf' # Ta; (\<Delta>, z, S) = final; conf' \<Rightarrow>\<^sup>*\<^bsub>Ta\<^esub> final; conf \<Rightarrow> conf'\<rbrakk> \<Longrightarrow> T = []
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>conf' Ta final conf. \<lbrakk>isVal e; \<forall>c'\<in>set T. stack (\<Gamma>, e, S) \<lesssim> stack c'; stack (\<Delta>, z, S) = stack (\<Gamma>, e, S); (\<Gamma>, e, S) = conf; T = conf' # Ta; (\<Delta>, z, S) = final; conf' \<Rightarrow>\<^sup>*\<^bsub>Ta\<^esub> final; conf \<Rightarrow> conf'\<rbrakk> \<Longrightarrow> T = []
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa b Ta. \<lbrakk>isVal e; T = (a, aa, b) # Ta; (a, aa, b) \<Rightarrow>\<^sup>*\<^bsub>Ta\<^esub> (\<Delta>, z, S); (\<Gamma>, e, S) \<Rightarrow> (a, aa, b); S \<lesssim> b; \<forall>c'\<in>set Ta. S \<lesssim> stack c'\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (auto elim!: step.cases)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Ball_subst[simp]:
  "(\<forall>p\<in>set (\<Gamma>[y::h=x]). f p) \<longleftrightarrow> (\<forall>p\<in>set \<Gamma>. case p of (z,e) \<Rightarrow> f (z, e[y::=x]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>p\<in>set \<Gamma>[y::h=x]. f p) = (\<forall>p\<in>set \<Gamma>. case p of (z, e) \<Rightarrow> f (z, e[y::=x]))
[PROOF STEP]
by (induction \<Gamma>) auto


[STATEMENT]
lemma lemma_3:
  assumes "(\<Gamma>, e, S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^esub> (\<Delta>, z, S)"
  assumes "isVal z"
  shows "\<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(\<Gamma>, e, S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^esub> (\<Delta>, z, S)
isVal z

goal (1 subgoal):
 1. \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
proof(induction T arbitrary: \<Gamma> e S \<Delta> z rule: measure_induct_rule[where f = length])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x \<Gamma> e S \<Delta> z. \<lbrakk>\<And>y \<Gamma> e S \<Delta> z. \<lbrakk>length y < length x; (\<Gamma>, e, S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>y\<^esub> (\<Delta>, z, S); isVal z\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z; (\<Gamma>, e, S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>x\<^esub> (\<Delta>, z, S); isVal z\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
case (less T \<Gamma> e S \<Delta> z)
[PROOF STATE]
proof (state)
this:
\<lbrakk>length ?y < length T; (?\<Gamma>, ?e, ?S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>?y\<^esub> (?\<Delta>, ?z, ?S); isVal ?z\<rbrakk> \<Longrightarrow> ?\<Gamma> : ?e \<Down>\<^bsub>upds_list ?S\<^esub> ?\<Delta> : ?z
(\<Gamma>, e, S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^esub> (\<Delta>, z, S)
isVal z

goal (1 subgoal):
 1. \<And>x \<Gamma> e S \<Delta> z. \<lbrakk>\<And>y \<Gamma> e S \<Delta> z. \<lbrakk>length y < length x; (\<Gamma>, e, S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>y\<^esub> (\<Delta>, z, S); isVal z\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z; (\<Gamma>, e, S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>x\<^esub> (\<Delta>, z, S); isVal z\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
from \<open>(\<Gamma>, e, S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^esub> (\<Delta>, z, S)\<close>
[PROOF STATE]
proof (chain)
picking this:
(\<Gamma>, e, S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^esub> (\<Delta>, z, S)
[PROOF STEP]
have "(\<Gamma>, e, S) \<Rightarrow>\<^sup>*\<^bsub>T\<^esub> (\<Delta>, z, S)" and "\<forall> c'\<in>set T. S \<lesssim> stack c'"
[PROOF STATE]
proof (prove)
using this:
(\<Gamma>, e, S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^esub> (\<Delta>, z, S)

goal (1 subgoal):
 1. (\<Gamma>, e, S) \<Rightarrow>\<^sup>*\<^bsub>T\<^esub> (\<Delta>, z, S) &&& \<forall>c'\<in>set T. S \<lesssim> stack c'
[PROOF STEP]
unfolding bal.simps
[PROOF STATE]
proof (prove)
using this:
\<exists>c T c'. (\<Gamma>, e, S) = c \<and> T = T \<and> (\<Delta>, z, S) = c' \<and> c \<Rightarrow>\<^sup>*\<^bsub>T\<^esub> c' \<and> (\<forall>c'\<in>set T. stack c \<lesssim> stack c') \<and> stack c' = stack c

goal (1 subgoal):
 1. (\<Gamma>, e, S) \<Rightarrow>\<^sup>*\<^bsub>T\<^esub> (\<Delta>, z, S) &&& \<forall>c'\<in>set T. S \<lesssim> stack c'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Gamma>, e, S) \<Rightarrow>\<^sup>*\<^bsub>T\<^esub> (\<Delta>, z, S)
\<forall>c'\<in>set T. S \<lesssim> stack c'

goal (1 subgoal):
 1. \<And>x \<Gamma> e S \<Delta> z. \<lbrakk>\<And>y \<Gamma> e S \<Delta> z. \<lbrakk>length y < length x; (\<Gamma>, e, S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>y\<^esub> (\<Delta>, z, S); isVal z\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z; (\<Gamma>, e, S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>x\<^esub> (\<Delta>, z, S); isVal z\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
from this(1)
[PROOF STATE]
proof (chain)
picking this:
(\<Gamma>, e, S) \<Rightarrow>\<^sup>*\<^bsub>T\<^esub> (\<Delta>, z, S)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(\<Gamma>, e, S) \<Rightarrow>\<^sup>*\<^bsub>T\<^esub> (\<Delta>, z, S)

goal (1 subgoal):
 1. \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
proof(cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>T = []; \<Delta> = \<Gamma>; z = e\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 2. \<And>conf' T. \<lbrakk>T = conf' # T; conf' \<Rightarrow>\<^sup>*\<^bsub>T\<^esub> (\<Delta>, z, S); (\<Gamma>, e, S) \<Rightarrow> conf'\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
case trace_nil
[PROOF STATE]
proof (state)
this:
T = []
\<Delta> = \<Gamma>
z = e

goal (2 subgoals):
 1. \<lbrakk>T = []; \<Delta> = \<Gamma>; z = e\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 2. \<And>conf' T. \<lbrakk>T = conf' # T; conf' \<Rightarrow>\<^sup>*\<^bsub>T\<^esub> (\<Delta>, z, S); (\<Gamma>, e, S) \<Rightarrow> conf'\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
from \<open>isVal z\<close>  trace_nil
[PROOF STATE]
proof (chain)
picking this:
isVal z
T = []
\<Delta> = \<Gamma>
z = e
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
isVal z
T = []
\<Delta> = \<Gamma>
z = e

goal (1 subgoal):
 1. \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
by (auto intro: reds_isValI)
[PROOF STATE]
proof (state)
this:
\<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z

goal (1 subgoal):
 1. \<And>conf' T. \<lbrakk>T = conf' # T; conf' \<Rightarrow>\<^sup>*\<^bsub>T\<^esub> (\<Delta>, z, S); (\<Gamma>, e, S) \<Rightarrow> conf'\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>conf' T. \<lbrakk>T = conf' # T; conf' \<Rightarrow>\<^sup>*\<^bsub>T\<^esub> (\<Delta>, z, S); (\<Gamma>, e, S) \<Rightarrow> conf'\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
case (trace_cons conf' T')
[PROOF STATE]
proof (state)
this:
T = conf' # T'
conf' \<Rightarrow>\<^sup>*\<^bsub>T'\<^esub> (\<Delta>, z, S)
(\<Gamma>, e, S) \<Rightarrow> conf'

goal (1 subgoal):
 1. \<And>conf' T. \<lbrakk>T = conf' # T; conf' \<Rightarrow>\<^sup>*\<^bsub>T\<^esub> (\<Delta>, z, S); (\<Gamma>, e, S) \<Rightarrow> conf'\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
from \<open>T = conf' # T'\<close> and \<open>\<forall> c'\<in>set T. S \<lesssim> stack c'\<close>
[PROOF STATE]
proof (chain)
picking this:
T = conf' # T'
\<forall>c'\<in>set T. S \<lesssim> stack c'
[PROOF STEP]
have "S \<lesssim> stack conf'"
[PROOF STATE]
proof (prove)
using this:
T = conf' # T'
\<forall>c'\<in>set T. S \<lesssim> stack c'

goal (1 subgoal):
 1. S \<lesssim> stack conf'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
S \<lesssim> stack conf'

goal (1 subgoal):
 1. \<And>conf' T. \<lbrakk>T = conf' # T; conf' \<Rightarrow>\<^sup>*\<^bsub>T\<^esub> (\<Delta>, z, S); (\<Gamma>, e, S) \<Rightarrow> conf'\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
from \<open>(\<Gamma>, e, S) \<Rightarrow> conf'\<close>
[PROOF STATE]
proof (chain)
picking this:
(\<Gamma>, e, S) \<Rightarrow> conf'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Gamma>, e, S) \<Rightarrow> conf'

goal (1 subgoal):
 1. \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
proof(cases)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>e x. \<lbrakk>e = App e x; conf' = (\<Gamma>, e, Arg x # S)\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 2. \<And>y e x S. \<lbrakk>e = Lam [y]. e; S = Arg x # S; conf' = (\<Gamma>, e[y::=x], S)\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 3. \<And>x e. \<lbrakk>e = Var x; conf' = (delete x \<Gamma>, e, Upd x # S); map_of \<Gamma> x = Some e\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 4. \<And>x S. \<lbrakk>S = Upd x # S; conf' = ((x, e) # \<Gamma>, e, S); x \<notin> domA \<Gamma>; isVal e\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 5. \<And>\<Delta> e. \<lbrakk>e = Terms.Let \<Delta> e; conf' = (\<Delta> @ \<Gamma>, e, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 6. \<And>scrut e1 e2. \<lbrakk>e = (scrut ? e1 : e2); conf' = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 7. \<And>b e1 e2 S. \<lbrakk>e = Bool b; S = Alts e1 e2 # S; conf' = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
case (app\<^sub>1 e x)
[PROOF STATE]
proof (state)
this:
ea__ = App e x
conf' = (\<Gamma>, e, Arg x # S)

goal (7 subgoals):
 1. \<And>e x. \<lbrakk>ea__ = App e x; conf' = (\<Gamma>, e, Arg x # S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 2. \<And>y e x S. \<lbrakk>ea__ = Lam [y]. e; S = Arg x # S; conf' = (\<Gamma>, e[y::=x], S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 3. \<And>x e. \<lbrakk>ea__ = Var x; conf' = (delete x \<Gamma>, e, Upd x # S); map_of \<Gamma> x = Some e\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 4. \<And>x S. \<lbrakk>S = Upd x # S; conf' = ((x, ea__) # \<Gamma>, ea__, S); x \<notin> domA \<Gamma>; isVal ea__\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 5. \<And>\<Delta> e. \<lbrakk>ea__ = Terms.Let \<Delta> e; conf' = (\<Delta> @ \<Gamma>, e, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 6. \<And>scrut e1 e2. \<lbrakk>ea__ = (scrut ? e1 : e2); conf' = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 7. \<And>b e1 e2 S. \<lbrakk>ea__ = Bool b; S = Alts e1 e2 # S; conf' = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
obtain T\<^sub>1 c\<^sub>3 c\<^sub>4 T\<^sub>2
      where "T' = T\<^sub>1 @ c\<^sub>4 # T\<^sub>2" and prem1: "(\<Gamma>, e, Arg x # S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^sub>1\<^esub> c\<^sub>3" and "c\<^sub>3 \<Rightarrow> c\<^sub>4" and prem2: " c\<^sub>4 \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^sub>2\<^esub> (\<Delta>, z, S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>T\<^sub>1 c\<^sub>4 T\<^sub>2 c\<^sub>3. \<lbrakk>T' = T\<^sub>1 @ c\<^sub>4 # T\<^sub>2; (\<Gamma>, e, Arg x # S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^sub>1\<^esub> c\<^sub>3; c\<^sub>3 \<Rightarrow> c\<^sub>4; c\<^sub>4 \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^sub>2\<^esub> (\<Delta>, z, S)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule bal_consE[OF  \<open>bal _ T _\<close>[unfolded app\<^sub>1 trace_cons]]) (simp, rule)
[PROOF STATE]
proof (state)
this:
T' = T\<^sub>1 @ c\<^sub>4 # T\<^sub>2
(\<Gamma>, e, Arg x # S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^sub>1\<^esub> c\<^sub>3
c\<^sub>3 \<Rightarrow> c\<^sub>4
c\<^sub>4 \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^sub>2\<^esub> (\<Delta>, z, S)

goal (7 subgoals):
 1. \<And>e x. \<lbrakk>ea__ = App e x; conf' = (\<Gamma>, e, Arg x # S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 2. \<And>y e x S. \<lbrakk>ea__ = Lam [y]. e; S = Arg x # S; conf' = (\<Gamma>, e[y::=x], S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 3. \<And>x e. \<lbrakk>ea__ = Var x; conf' = (delete x \<Gamma>, e, Upd x # S); map_of \<Gamma> x = Some e\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 4. \<And>x S. \<lbrakk>S = Upd x # S; conf' = ((x, ea__) # \<Gamma>, ea__, S); x \<notin> domA \<Gamma>; isVal ea__\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 5. \<And>\<Delta> e. \<lbrakk>ea__ = Terms.Let \<Delta> e; conf' = (\<Delta> @ \<Gamma>, e, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 6. \<And>scrut e1 e2. \<lbrakk>ea__ = (scrut ? e1 : e2); conf' = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 7. \<And>b e1 e2 S. \<lbrakk>ea__ = Bool b; S = Alts e1 e2 # S; conf' = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
from \<open>T = _\<close> \<open>T' = _\<close>
[PROOF STATE]
proof (chain)
picking this:
T = conf' # T'
T' = T\<^sub>1 @ c\<^sub>4 # T\<^sub>2
[PROOF STEP]
have "length T\<^sub>1 < length T" and "length T\<^sub>2 < length T"
[PROOF STATE]
proof (prove)
using this:
T = conf' # T'
T' = T\<^sub>1 @ c\<^sub>4 # T\<^sub>2

goal (1 subgoal):
 1. length T\<^sub>1 < length T &&& length T\<^sub>2 < length T
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length T\<^sub>1 < length T
length T\<^sub>2 < length T

goal (7 subgoals):
 1. \<And>e x. \<lbrakk>ea__ = App e x; conf' = (\<Gamma>, e, Arg x # S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 2. \<And>y e x S. \<lbrakk>ea__ = Lam [y]. e; S = Arg x # S; conf' = (\<Gamma>, e[y::=x], S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 3. \<And>x e. \<lbrakk>ea__ = Var x; conf' = (delete x \<Gamma>, e, Upd x # S); map_of \<Gamma> x = Some e\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 4. \<And>x S. \<lbrakk>S = Upd x # S; conf' = ((x, ea__) # \<Gamma>, ea__, S); x \<notin> domA \<Gamma>; isVal ea__\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 5. \<And>\<Delta> e. \<lbrakk>ea__ = Terms.Let \<Delta> e; conf' = (\<Delta> @ \<Gamma>, e, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 6. \<And>scrut e1 e2. \<lbrakk>ea__ = (scrut ? e1 : e2); conf' = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 7. \<And>b e1 e2 S. \<lbrakk>ea__ = Bool b; S = Alts e1 e2 # S; conf' = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
from prem1
[PROOF STATE]
proof (chain)
picking this:
(\<Gamma>, e, Arg x # S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^sub>1\<^esub> c\<^sub>3
[PROOF STEP]
have "stack c\<^sub>3 =  Arg x # S"
[PROOF STATE]
proof (prove)
using this:
(\<Gamma>, e, Arg x # S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^sub>1\<^esub> c\<^sub>3

goal (1 subgoal):
 1. stack c\<^sub>3 = Arg x # S
[PROOF STEP]
by (auto dest:  bal_stackD)
[PROOF STATE]
proof (state)
this:
stack c\<^sub>3 = Arg x # S

goal (7 subgoals):
 1. \<And>e x. \<lbrakk>ea__ = App e x; conf' = (\<Gamma>, e, Arg x # S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 2. \<And>y e x S. \<lbrakk>ea__ = Lam [y]. e; S = Arg x # S; conf' = (\<Gamma>, e[y::=x], S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 3. \<And>x e. \<lbrakk>ea__ = Var x; conf' = (delete x \<Gamma>, e, Upd x # S); map_of \<Gamma> x = Some e\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 4. \<And>x S. \<lbrakk>S = Upd x # S; conf' = ((x, ea__) # \<Gamma>, ea__, S); x \<notin> domA \<Gamma>; isVal ea__\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 5. \<And>\<Delta> e. \<lbrakk>ea__ = Terms.Let \<Delta> e; conf' = (\<Delta> @ \<Gamma>, e, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 6. \<And>scrut e1 e2. \<lbrakk>ea__ = (scrut ? e1 : e2); conf' = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 7. \<And>b e1 e2 S. \<lbrakk>ea__ = Bool b; S = Alts e1 e2 # S; conf' = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
stack c\<^sub>3 = Arg x # S

goal (7 subgoals):
 1. \<And>e x. \<lbrakk>ea__ = App e x; conf' = (\<Gamma>, e, Arg x # S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 2. \<And>y e x S. \<lbrakk>ea__ = Lam [y]. e; S = Arg x # S; conf' = (\<Gamma>, e[y::=x], S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 3. \<And>x e. \<lbrakk>ea__ = Var x; conf' = (delete x \<Gamma>, e, Upd x # S); map_of \<Gamma> x = Some e\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 4. \<And>x S. \<lbrakk>S = Upd x # S; conf' = ((x, ea__) # \<Gamma>, ea__, S); x \<notin> domA \<Gamma>; isVal ea__\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 5. \<And>\<Delta> e. \<lbrakk>ea__ = Terms.Let \<Delta> e; conf' = (\<Delta> @ \<Gamma>, e, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 6. \<And>scrut e1 e2. \<lbrakk>ea__ = (scrut ? e1 : e2); conf' = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 7. \<And>b e1 e2 S. \<lbrakk>ea__ = Bool b; S = Alts e1 e2 # S; conf' = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
from prem2
[PROOF STATE]
proof (chain)
picking this:
c\<^sub>4 \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^sub>2\<^esub> (\<Delta>, z, S)
[PROOF STEP]
have "stack c\<^sub>4 = S"
[PROOF STATE]
proof (prove)
using this:
c\<^sub>4 \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^sub>2\<^esub> (\<Delta>, z, S)

goal (1 subgoal):
 1. stack c\<^sub>4 = S
[PROOF STEP]
by (auto dest: bal_stackD)
[PROOF STATE]
proof (state)
this:
stack c\<^sub>4 = S

goal (7 subgoals):
 1. \<And>e x. \<lbrakk>ea__ = App e x; conf' = (\<Gamma>, e, Arg x # S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 2. \<And>y e x S. \<lbrakk>ea__ = Lam [y]. e; S = Arg x # S; conf' = (\<Gamma>, e[y::=x], S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 3. \<And>x e. \<lbrakk>ea__ = Var x; conf' = (delete x \<Gamma>, e, Upd x # S); map_of \<Gamma> x = Some e\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 4. \<And>x S. \<lbrakk>S = Upd x # S; conf' = ((x, ea__) # \<Gamma>, ea__, S); x \<notin> domA \<Gamma>; isVal ea__\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 5. \<And>\<Delta> e. \<lbrakk>ea__ = Terms.Let \<Delta> e; conf' = (\<Delta> @ \<Gamma>, e, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 6. \<And>scrut e1 e2. \<lbrakk>ea__ = (scrut ? e1 : e2); conf' = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 7. \<And>b e1 e2 S. \<lbrakk>ea__ = Bool b; S = Alts e1 e2 # S; conf' = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
stack c\<^sub>4 = S

goal (7 subgoals):
 1. \<And>e x. \<lbrakk>ea__ = App e x; conf' = (\<Gamma>, e, Arg x # S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 2. \<And>y e x S. \<lbrakk>ea__ = Lam [y]. e; S = Arg x # S; conf' = (\<Gamma>, e[y::=x], S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 3. \<And>x e. \<lbrakk>ea__ = Var x; conf' = (delete x \<Gamma>, e, Upd x # S); map_of \<Gamma> x = Some e\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 4. \<And>x S. \<lbrakk>S = Upd x # S; conf' = ((x, ea__) # \<Gamma>, ea__, S); x \<notin> domA \<Gamma>; isVal ea__\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 5. \<And>\<Delta> e. \<lbrakk>ea__ = Terms.Let \<Delta> e; conf' = (\<Delta> @ \<Gamma>, e, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 6. \<And>scrut e1 e2. \<lbrakk>ea__ = (scrut ? e1 : e2); conf' = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 7. \<And>b e1 e2 S. \<lbrakk>ea__ = Bool b; S = Alts e1 e2 # S; conf' = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
note \<open>c\<^sub>3 \<Rightarrow> c\<^sub>4\<close>
[PROOF STATE]
proof (state)
this:
c\<^sub>3 \<Rightarrow> c\<^sub>4

goal (7 subgoals):
 1. \<And>e x. \<lbrakk>ea__ = App e x; conf' = (\<Gamma>, e, Arg x # S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 2. \<And>y e x S. \<lbrakk>ea__ = Lam [y]. e; S = Arg x # S; conf' = (\<Gamma>, e[y::=x], S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 3. \<And>x e. \<lbrakk>ea__ = Var x; conf' = (delete x \<Gamma>, e, Upd x # S); map_of \<Gamma> x = Some e\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 4. \<And>x S. \<lbrakk>S = Upd x # S; conf' = ((x, ea__) # \<Gamma>, ea__, S); x \<notin> domA \<Gamma>; isVal ea__\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 5. \<And>\<Delta> e. \<lbrakk>ea__ = Terms.Let \<Delta> e; conf' = (\<Delta> @ \<Gamma>, e, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 6. \<And>scrut e1 e2. \<lbrakk>ea__ = (scrut ? e1 : e2); conf' = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 7. \<And>b e1 e2 S. \<lbrakk>ea__ = Bool b; S = Alts e1 e2 # S; conf' = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
stack c\<^sub>3 = Arg x # S
stack c\<^sub>4 = S
c\<^sub>3 \<Rightarrow> c\<^sub>4
[PROOF STEP]
obtain \<Delta>' y e' where "c\<^sub>3 = (\<Delta>', Lam [y]. e', Arg x # S)" and "c\<^sub>4 = (\<Delta>', e'[y ::= x], S)"
[PROOF STATE]
proof (prove)
using this:
stack c\<^sub>3 = Arg x # S
stack c\<^sub>4 = S
c\<^sub>3 \<Rightarrow> c\<^sub>4

goal (1 subgoal):
 1. (\<And>\<Delta>' y e'. \<lbrakk>c\<^sub>3 = (\<Delta>', Lam [y]. e', Arg x # S); c\<^sub>4 = (\<Delta>', e'[y::=x], S)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto elim!: step.cases simp del: exp_assn.eq_iff)
[PROOF STATE]
proof (state)
this:
c\<^sub>3 = (\<Delta>', Lam [y]. e', Arg x # S)
c\<^sub>4 = (\<Delta>', e'[y::=x], S)

goal (7 subgoals):
 1. \<And>e x. \<lbrakk>ea__ = App e x; conf' = (\<Gamma>, e, Arg x # S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 2. \<And>y e x S. \<lbrakk>ea__ = Lam [y]. e; S = Arg x # S; conf' = (\<Gamma>, e[y::=x], S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 3. \<And>x e. \<lbrakk>ea__ = Var x; conf' = (delete x \<Gamma>, e, Upd x # S); map_of \<Gamma> x = Some e\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 4. \<And>x S. \<lbrakk>S = Upd x # S; conf' = ((x, ea__) # \<Gamma>, ea__, S); x \<notin> domA \<Gamma>; isVal ea__\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 5. \<And>\<Delta> e. \<lbrakk>ea__ = Terms.Let \<Delta> e; conf' = (\<Delta> @ \<Gamma>, e, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 6. \<And>scrut e1 e2. \<lbrakk>ea__ = (scrut ? e1 : e2); conf' = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 7. \<And>b e1 e2 S. \<lbrakk>ea__ = Bool b; S = Alts e1 e2 # S; conf' = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
from less(1)[OF \<open>length T\<^sub>1 < length T\<close> prem1[unfolded \<open>c\<^sub>3 = _\<close> \<open>c\<^sub>4 = _\<close>]]
[PROOF STATE]
proof (chain)
picking this:
isVal (Lam [y]. e') \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list (Arg x # S)\<^esub> \<Delta>' : Lam [y]. e'
[PROOF STEP]
have "\<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta>' : Lam [y]. e'"
[PROOF STATE]
proof (prove)
using this:
isVal (Lam [y]. e') \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list (Arg x # S)\<^esub> \<Delta>' : Lam [y]. e'

goal (1 subgoal):
 1. \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta>' : Lam [y]. e'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta>' : Lam [y]. e'

goal (7 subgoals):
 1. \<And>e x. \<lbrakk>ea__ = App e x; conf' = (\<Gamma>, e, Arg x # S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 2. \<And>y e x S. \<lbrakk>ea__ = Lam [y]. e; S = Arg x # S; conf' = (\<Gamma>, e[y::=x], S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 3. \<And>x e. \<lbrakk>ea__ = Var x; conf' = (delete x \<Gamma>, e, Upd x # S); map_of \<Gamma> x = Some e\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 4. \<And>x S. \<lbrakk>S = Upd x # S; conf' = ((x, ea__) # \<Gamma>, ea__, S); x \<notin> domA \<Gamma>; isVal ea__\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 5. \<And>\<Delta> e. \<lbrakk>ea__ = Terms.Let \<Delta> e; conf' = (\<Delta> @ \<Gamma>, e, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 6. \<And>scrut e1 e2. \<lbrakk>ea__ = (scrut ? e1 : e2); conf' = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 7. \<And>b e1 e2 S. \<lbrakk>ea__ = Bool b; S = Alts e1 e2 # S; conf' = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta>' : Lam [y]. e'

goal (7 subgoals):
 1. \<And>e x. \<lbrakk>ea__ = App e x; conf' = (\<Gamma>, e, Arg x # S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 2. \<And>y e x S. \<lbrakk>ea__ = Lam [y]. e; S = Arg x # S; conf' = (\<Gamma>, e[y::=x], S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 3. \<And>x e. \<lbrakk>ea__ = Var x; conf' = (delete x \<Gamma>, e, Upd x # S); map_of \<Gamma> x = Some e\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 4. \<And>x S. \<lbrakk>S = Upd x # S; conf' = ((x, ea__) # \<Gamma>, ea__, S); x \<notin> domA \<Gamma>; isVal ea__\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 5. \<And>\<Delta> e. \<lbrakk>ea__ = Terms.Let \<Delta> e; conf' = (\<Delta> @ \<Gamma>, e, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 6. \<And>scrut e1 e2. \<lbrakk>ea__ = (scrut ? e1 : e2); conf' = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 7. \<And>b e1 e2 S. \<lbrakk>ea__ = Bool b; S = Alts e1 e2 # S; conf' = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
from less(1)[OF \<open>length T\<^sub>2 < length T\<close> prem2[unfolded \<open>c\<^sub>3 = _\<close> \<open>c\<^sub>4 = _\<close>] \<open>isVal z\<close>]
[PROOF STATE]
proof (chain)
picking this:
\<Delta>' : e'[y::=x] \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
have "\<Delta>' : e'[y::=x] \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z"
[PROOF STATE]
proof (prove)
using this:
\<Delta>' : e'[y::=x] \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z

goal (1 subgoal):
 1. \<Delta>' : e'[y::=x] \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Delta>' : e'[y::=x] \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z

goal (7 subgoals):
 1. \<And>e x. \<lbrakk>ea__ = App e x; conf' = (\<Gamma>, e, Arg x # S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 2. \<And>y e x S. \<lbrakk>ea__ = Lam [y]. e; S = Arg x # S; conf' = (\<Gamma>, e[y::=x], S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 3. \<And>x e. \<lbrakk>ea__ = Var x; conf' = (delete x \<Gamma>, e, Upd x # S); map_of \<Gamma> x = Some e\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 4. \<And>x S. \<lbrakk>S = Upd x # S; conf' = ((x, ea__) # \<Gamma>, ea__, S); x \<notin> domA \<Gamma>; isVal ea__\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 5. \<And>\<Delta> e. \<lbrakk>ea__ = Terms.Let \<Delta> e; conf' = (\<Delta> @ \<Gamma>, e, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 6. \<And>scrut e1 e2. \<lbrakk>ea__ = (scrut ? e1 : e2); conf' = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 7. \<And>b e1 e2 S. \<lbrakk>ea__ = Bool b; S = Alts e1 e2 # S; conf' = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta>' : Lam [y]. e'
\<Delta>' : e'[y::=x] \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta>' : Lam [y]. e'
\<Delta>' : e'[y::=x] \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z

goal (1 subgoal):
 1. \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
unfolding app\<^sub>1
[PROOF STATE]
proof (prove)
using this:
\<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta>' : Lam [y]. e'
\<Delta>' : e'[y::=x] \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z

goal (1 subgoal):
 1. \<Gamma> : App e x \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
by (rule reds_ApplicationI)
[PROOF STATE]
proof (state)
this:
\<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z

goal (6 subgoals):
 1. \<And>y e x S. \<lbrakk>ea__ = Lam [y]. e; S = Arg x # S; conf' = (\<Gamma>, e[y::=x], S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 2. \<And>x e. \<lbrakk>ea__ = Var x; conf' = (delete x \<Gamma>, e, Upd x # S); map_of \<Gamma> x = Some e\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 3. \<And>x S. \<lbrakk>S = Upd x # S; conf' = ((x, ea__) # \<Gamma>, ea__, S); x \<notin> domA \<Gamma>; isVal ea__\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 4. \<And>\<Delta> e. \<lbrakk>ea__ = Terms.Let \<Delta> e; conf' = (\<Delta> @ \<Gamma>, e, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 5. \<And>scrut e1 e2. \<lbrakk>ea__ = (scrut ? e1 : e2); conf' = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 6. \<And>b e1 e2 S. \<lbrakk>ea__ = Bool b; S = Alts e1 e2 # S; conf' = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>y e x S. \<lbrakk>e = Lam [y]. e; S = Arg x # S; conf' = (\<Gamma>, e[y::=x], S)\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 2. \<And>x e. \<lbrakk>e = Var x; conf' = (delete x \<Gamma>, e, Upd x # S); map_of \<Gamma> x = Some e\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 3. \<And>x S. \<lbrakk>S = Upd x # S; conf' = ((x, e) # \<Gamma>, e, S); x \<notin> domA \<Gamma>; isVal e\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 4. \<And>\<Delta> e. \<lbrakk>e = Terms.Let \<Delta> e; conf' = (\<Delta> @ \<Gamma>, e, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 5. \<And>scrut e1 e2. \<lbrakk>e = (scrut ? e1 : e2); conf' = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 6. \<And>b e1 e2 S. \<lbrakk>e = Bool b; S = Alts e1 e2 # S; conf' = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
case (app\<^sub>2 y e x S')
[PROOF STATE]
proof (state)
this:
ea__ = Lam [y]. e
S = Arg x # S'
conf' = (\<Gamma>, e[y::=x], S')

goal (6 subgoals):
 1. \<And>y e x S. \<lbrakk>ea__ = Lam [y]. e; S = Arg x # S; conf' = (\<Gamma>, e[y::=x], S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 2. \<And>x e. \<lbrakk>ea__ = Var x; conf' = (delete x \<Gamma>, e, Upd x # S); map_of \<Gamma> x = Some e\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 3. \<And>x S. \<lbrakk>S = Upd x # S; conf' = ((x, ea__) # \<Gamma>, ea__, S); x \<notin> domA \<Gamma>; isVal ea__\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 4. \<And>\<Delta> e. \<lbrakk>ea__ = Terms.Let \<Delta> e; conf' = (\<Delta> @ \<Gamma>, e, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 5. \<And>scrut e1 e2. \<lbrakk>ea__ = (scrut ? e1 : e2); conf' = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 6. \<And>b e1 e2 S. \<lbrakk>ea__ = Bool b; S = Alts e1 e2 # S; conf' = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
from \<open>conf' =_\<close> \<open>S = _ # S'\<close> \<open>S \<lesssim> stack conf'\<close>
[PROOF STATE]
proof (chain)
picking this:
conf' = (\<Gamma>, e[y::=x], S')
S = Arg x # S'
S \<lesssim> stack conf'
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
conf' = (\<Gamma>, e[y::=x], S')
S = Arg x # S'
S \<lesssim> stack conf'

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

goal (6 subgoals):
 1. \<And>y e x S. \<lbrakk>ea__ = Lam [y]. e; S = Arg x # S; conf' = (\<Gamma>, e[y::=x], S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 2. \<And>x e. \<lbrakk>ea__ = Var x; conf' = (delete x \<Gamma>, e, Upd x # S); map_of \<Gamma> x = Some e\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 3. \<And>x S. \<lbrakk>S = Upd x # S; conf' = ((x, ea__) # \<Gamma>, ea__, S); x \<notin> domA \<Gamma>; isVal ea__\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 4. \<And>\<Delta> e. \<lbrakk>ea__ = Terms.Let \<Delta> e; conf' = (\<Delta> @ \<Gamma>, e, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 5. \<And>scrut e1 e2. \<lbrakk>ea__ = (scrut ? e1 : e2); conf' = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 6. \<And>b e1 e2 S. \<lbrakk>ea__ = Bool b; S = Alts e1 e2 # S; conf' = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z

goal (5 subgoals):
 1. \<And>x e. \<lbrakk>ea__ = Var x; conf' = (delete x \<Gamma>, e, Upd x # S); map_of \<Gamma> x = Some e\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 2. \<And>x S. \<lbrakk>S = Upd x # S; conf' = ((x, ea__) # \<Gamma>, ea__, S); x \<notin> domA \<Gamma>; isVal ea__\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 3. \<And>\<Delta> e. \<lbrakk>ea__ = Terms.Let \<Delta> e; conf' = (\<Delta> @ \<Gamma>, e, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 4. \<And>scrut e1 e2. \<lbrakk>ea__ = (scrut ? e1 : e2); conf' = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 5. \<And>b e1 e2 S. \<lbrakk>ea__ = Bool b; S = Alts e1 e2 # S; conf' = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>x e. \<lbrakk>e = Var x; conf' = (delete x \<Gamma>, e, Upd x # S); map_of \<Gamma> x = Some e\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 2. \<And>x S. \<lbrakk>S = Upd x # S; conf' = ((x, e) # \<Gamma>, e, S); x \<notin> domA \<Gamma>; isVal e\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 3. \<And>\<Delta> e. \<lbrakk>e = Terms.Let \<Delta> e; conf' = (\<Delta> @ \<Gamma>, e, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 4. \<And>scrut e1 e2. \<lbrakk>e = (scrut ? e1 : e2); conf' = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 5. \<And>b e1 e2 S. \<lbrakk>e = Bool b; S = Alts e1 e2 # S; conf' = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
case (var\<^sub>1 x e)
[PROOF STATE]
proof (state)
this:
ea__ = Var x
conf' = (delete x \<Gamma>, e, Upd x # S)
map_of \<Gamma> x = Some e

goal (5 subgoals):
 1. \<And>x e. \<lbrakk>ea__ = Var x; conf' = (delete x \<Gamma>, e, Upd x # S); map_of \<Gamma> x = Some e\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 2. \<And>x S. \<lbrakk>S = Upd x # S; conf' = ((x, ea__) # \<Gamma>, ea__, S); x \<notin> domA \<Gamma>; isVal ea__\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 3. \<And>\<Delta> e. \<lbrakk>ea__ = Terms.Let \<Delta> e; conf' = (\<Delta> @ \<Gamma>, e, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 4. \<And>scrut e1 e2. \<lbrakk>ea__ = (scrut ? e1 : e2); conf' = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 5. \<And>b e1 e2 S. \<lbrakk>ea__ = Bool b; S = Alts e1 e2 # S; conf' = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
obtain T\<^sub>1 c\<^sub>3 c\<^sub>4 T\<^sub>2
      where "T' = T\<^sub>1 @ c\<^sub>4 # T\<^sub>2" and prem1: "(delete x \<Gamma>, e, Upd x # S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^sub>1\<^esub> c\<^sub>3" and "c\<^sub>3 \<Rightarrow> c\<^sub>4" and prem2: "c\<^sub>4 \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^sub>2\<^esub> (\<Delta>, z, S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>T\<^sub>1 c\<^sub>4 T\<^sub>2 c\<^sub>3. \<lbrakk>T' = T\<^sub>1 @ c\<^sub>4 # T\<^sub>2; (delete x \<Gamma>, e, Upd x # S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^sub>1\<^esub> c\<^sub>3; c\<^sub>3 \<Rightarrow> c\<^sub>4; c\<^sub>4 \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^sub>2\<^esub> (\<Delta>, z, S)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule bal_consE[OF  \<open>bal _ T _\<close>[unfolded var\<^sub>1 trace_cons]]) (simp, rule)
[PROOF STATE]
proof (state)
this:
T' = T\<^sub>1 @ c\<^sub>4 # T\<^sub>2
(delete x \<Gamma>, e, Upd x # S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^sub>1\<^esub> c\<^sub>3
c\<^sub>3 \<Rightarrow> c\<^sub>4
c\<^sub>4 \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^sub>2\<^esub> (\<Delta>, z, S)

goal (5 subgoals):
 1. \<And>x e. \<lbrakk>ea__ = Var x; conf' = (delete x \<Gamma>, e, Upd x # S); map_of \<Gamma> x = Some e\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 2. \<And>x S. \<lbrakk>S = Upd x # S; conf' = ((x, ea__) # \<Gamma>, ea__, S); x \<notin> domA \<Gamma>; isVal ea__\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 3. \<And>\<Delta> e. \<lbrakk>ea__ = Terms.Let \<Delta> e; conf' = (\<Delta> @ \<Gamma>, e, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 4. \<And>scrut e1 e2. \<lbrakk>ea__ = (scrut ? e1 : e2); conf' = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 5. \<And>b e1 e2 S. \<lbrakk>ea__ = Bool b; S = Alts e1 e2 # S; conf' = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
from \<open>T = _\<close> \<open>T' = _\<close>
[PROOF STATE]
proof (chain)
picking this:
T = conf' # T'
T' = T\<^sub>1 @ c\<^sub>4 # T\<^sub>2
[PROOF STEP]
have "length T\<^sub>1 < length T" and "length T\<^sub>2 < length T"
[PROOF STATE]
proof (prove)
using this:
T = conf' # T'
T' = T\<^sub>1 @ c\<^sub>4 # T\<^sub>2

goal (1 subgoal):
 1. length T\<^sub>1 < length T &&& length T\<^sub>2 < length T
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length T\<^sub>1 < length T
length T\<^sub>2 < length T

goal (5 subgoals):
 1. \<And>x e. \<lbrakk>ea__ = Var x; conf' = (delete x \<Gamma>, e, Upd x # S); map_of \<Gamma> x = Some e\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 2. \<And>x S. \<lbrakk>S = Upd x # S; conf' = ((x, ea__) # \<Gamma>, ea__, S); x \<notin> domA \<Gamma>; isVal ea__\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 3. \<And>\<Delta> e. \<lbrakk>ea__ = Terms.Let \<Delta> e; conf' = (\<Delta> @ \<Gamma>, e, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 4. \<And>scrut e1 e2. \<lbrakk>ea__ = (scrut ? e1 : e2); conf' = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 5. \<And>b e1 e2 S. \<lbrakk>ea__ = Bool b; S = Alts e1 e2 # S; conf' = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
from prem1
[PROOF STATE]
proof (chain)
picking this:
(delete x \<Gamma>, e, Upd x # S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^sub>1\<^esub> c\<^sub>3
[PROOF STEP]
have "stack c\<^sub>3 = Upd x # S"
[PROOF STATE]
proof (prove)
using this:
(delete x \<Gamma>, e, Upd x # S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^sub>1\<^esub> c\<^sub>3

goal (1 subgoal):
 1. stack c\<^sub>3 = Upd x # S
[PROOF STEP]
by (auto dest:  bal_stackD)
[PROOF STATE]
proof (state)
this:
stack c\<^sub>3 = Upd x # S

goal (5 subgoals):
 1. \<And>x e. \<lbrakk>ea__ = Var x; conf' = (delete x \<Gamma>, e, Upd x # S); map_of \<Gamma> x = Some e\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 2. \<And>x S. \<lbrakk>S = Upd x # S; conf' = ((x, ea__) # \<Gamma>, ea__, S); x \<notin> domA \<Gamma>; isVal ea__\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 3. \<And>\<Delta> e. \<lbrakk>ea__ = Terms.Let \<Delta> e; conf' = (\<Delta> @ \<Gamma>, e, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 4. \<And>scrut e1 e2. \<lbrakk>ea__ = (scrut ? e1 : e2); conf' = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 5. \<And>b e1 e2 S. \<lbrakk>ea__ = Bool b; S = Alts e1 e2 # S; conf' = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
stack c\<^sub>3 = Upd x # S

goal (5 subgoals):
 1. \<And>x e. \<lbrakk>ea__ = Var x; conf' = (delete x \<Gamma>, e, Upd x # S); map_of \<Gamma> x = Some e\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 2. \<And>x S. \<lbrakk>S = Upd x # S; conf' = ((x, ea__) # \<Gamma>, ea__, S); x \<notin> domA \<Gamma>; isVal ea__\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 3. \<And>\<Delta> e. \<lbrakk>ea__ = Terms.Let \<Delta> e; conf' = (\<Delta> @ \<Gamma>, e, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 4. \<And>scrut e1 e2. \<lbrakk>ea__ = (scrut ? e1 : e2); conf' = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 5. \<And>b e1 e2 S. \<lbrakk>ea__ = Bool b; S = Alts e1 e2 # S; conf' = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
from prem2
[PROOF STATE]
proof (chain)
picking this:
c\<^sub>4 \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^sub>2\<^esub> (\<Delta>, z, S)
[PROOF STEP]
have "stack c\<^sub>4 = S"
[PROOF STATE]
proof (prove)
using this:
c\<^sub>4 \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^sub>2\<^esub> (\<Delta>, z, S)

goal (1 subgoal):
 1. stack c\<^sub>4 = S
[PROOF STEP]
by (auto dest: bal_stackD)
[PROOF STATE]
proof (state)
this:
stack c\<^sub>4 = S

goal (5 subgoals):
 1. \<And>x e. \<lbrakk>ea__ = Var x; conf' = (delete x \<Gamma>, e, Upd x # S); map_of \<Gamma> x = Some e\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 2. \<And>x S. \<lbrakk>S = Upd x # S; conf' = ((x, ea__) # \<Gamma>, ea__, S); x \<notin> domA \<Gamma>; isVal ea__\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 3. \<And>\<Delta> e. \<lbrakk>ea__ = Terms.Let \<Delta> e; conf' = (\<Delta> @ \<Gamma>, e, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 4. \<And>scrut e1 e2. \<lbrakk>ea__ = (scrut ? e1 : e2); conf' = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 5. \<And>b e1 e2 S. \<lbrakk>ea__ = Bool b; S = Alts e1 e2 # S; conf' = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
stack c\<^sub>4 = S

goal (5 subgoals):
 1. \<And>x e. \<lbrakk>ea__ = Var x; conf' = (delete x \<Gamma>, e, Upd x # S); map_of \<Gamma> x = Some e\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 2. \<And>x S. \<lbrakk>S = Upd x # S; conf' = ((x, ea__) # \<Gamma>, ea__, S); x \<notin> domA \<Gamma>; isVal ea__\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 3. \<And>\<Delta> e. \<lbrakk>ea__ = Terms.Let \<Delta> e; conf' = (\<Delta> @ \<Gamma>, e, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 4. \<And>scrut e1 e2. \<lbrakk>ea__ = (scrut ? e1 : e2); conf' = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 5. \<And>b e1 e2 S. \<lbrakk>ea__ = Bool b; S = Alts e1 e2 # S; conf' = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
note \<open>c\<^sub>3 \<Rightarrow> c\<^sub>4\<close>
[PROOF STATE]
proof (state)
this:
c\<^sub>3 \<Rightarrow> c\<^sub>4

goal (5 subgoals):
 1. \<And>x e. \<lbrakk>ea__ = Var x; conf' = (delete x \<Gamma>, e, Upd x # S); map_of \<Gamma> x = Some e\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 2. \<And>x S. \<lbrakk>S = Upd x # S; conf' = ((x, ea__) # \<Gamma>, ea__, S); x \<notin> domA \<Gamma>; isVal ea__\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 3. \<And>\<Delta> e. \<lbrakk>ea__ = Terms.Let \<Delta> e; conf' = (\<Delta> @ \<Gamma>, e, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 4. \<And>scrut e1 e2. \<lbrakk>ea__ = (scrut ? e1 : e2); conf' = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 5. \<And>b e1 e2 S. \<lbrakk>ea__ = Bool b; S = Alts e1 e2 # S; conf' = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
stack c\<^sub>3 = Upd x # S
stack c\<^sub>4 = S
c\<^sub>3 \<Rightarrow> c\<^sub>4
[PROOF STEP]
obtain \<Delta>' z' where "c\<^sub>3 = (\<Delta>', z', Upd x # S)" and "c\<^sub>4 = ((x,z')#\<Delta>', z', S)" and "isVal z'"
[PROOF STATE]
proof (prove)
using this:
stack c\<^sub>3 = Upd x # S
stack c\<^sub>4 = S
c\<^sub>3 \<Rightarrow> c\<^sub>4

goal (1 subgoal):
 1. (\<And>\<Delta>' z'. \<lbrakk>c\<^sub>3 = (\<Delta>', z', Upd x # S); c\<^sub>4 = ((x, z') # \<Delta>', z', S); isVal z'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto elim!: step.cases simp del: exp_assn.eq_iff)
[PROOF STATE]
proof (state)
this:
c\<^sub>3 = (\<Delta>', z', Upd x # S)
c\<^sub>4 = ((x, z') # \<Delta>', z', S)
isVal z'

goal (5 subgoals):
 1. \<And>x e. \<lbrakk>ea__ = Var x; conf' = (delete x \<Gamma>, e, Upd x # S); map_of \<Gamma> x = Some e\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 2. \<And>x S. \<lbrakk>S = Upd x # S; conf' = ((x, ea__) # \<Gamma>, ea__, S); x \<notin> domA \<Gamma>; isVal ea__\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 3. \<And>\<Delta> e. \<lbrakk>ea__ = Terms.Let \<Delta> e; conf' = (\<Delta> @ \<Gamma>, e, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 4. \<And>scrut e1 e2. \<lbrakk>ea__ = (scrut ? e1 : e2); conf' = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 5. \<And>b e1 e2 S. \<lbrakk>ea__ = Bool b; S = Alts e1 e2 # S; conf' = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
from \<open>isVal z'\<close> and prem2[unfolded \<open>c\<^sub>4 = _\<close>]
[PROOF STATE]
proof (chain)
picking this:
isVal z'
((x, z') # \<Delta>', z', S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^sub>2\<^esub> (\<Delta>, z, S)
[PROOF STEP]
have "T\<^sub>2 = []"
[PROOF STATE]
proof (prove)
using this:
isVal z'
((x, z') # \<Delta>', z', S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^sub>2\<^esub> (\<Delta>, z, S)

goal (1 subgoal):
 1. T\<^sub>2 = []
[PROOF STEP]
by (rule isVal_stops)
[PROOF STATE]
proof (state)
this:
T\<^sub>2 = []

goal (5 subgoals):
 1. \<And>x e. \<lbrakk>ea__ = Var x; conf' = (delete x \<Gamma>, e, Upd x # S); map_of \<Gamma> x = Some e\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 2. \<And>x S. \<lbrakk>S = Upd x # S; conf' = ((x, ea__) # \<Gamma>, ea__, S); x \<notin> domA \<Gamma>; isVal ea__\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 3. \<And>\<Delta> e. \<lbrakk>ea__ = Terms.Let \<Delta> e; conf' = (\<Delta> @ \<Gamma>, e, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 4. \<And>scrut e1 e2. \<lbrakk>ea__ = (scrut ? e1 : e2); conf' = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 5. \<And>b e1 e2 S. \<lbrakk>ea__ = Bool b; S = Alts e1 e2 # S; conf' = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
with prem2 \<open>c\<^sub>4 = _\<close>
[PROOF STATE]
proof (chain)
picking this:
c\<^sub>4 \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^sub>2\<^esub> (\<Delta>, z, S)
c\<^sub>4 = ((x, z') # \<Delta>', z', S)
T\<^sub>2 = []
[PROOF STEP]
have "z' = z" and "\<Delta> = (x,z)#\<Delta>'"
[PROOF STATE]
proof (prove)
using this:
c\<^sub>4 \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^sub>2\<^esub> (\<Delta>, z, S)
c\<^sub>4 = ((x, z') # \<Delta>', z', S)
T\<^sub>2 = []

goal (1 subgoal):
 1. z' = z &&& \<Delta> = (x, z) # \<Delta>'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z' = z
\<Delta> = (x, z) # \<Delta>'

goal (5 subgoals):
 1. \<And>x e. \<lbrakk>ea__ = Var x; conf' = (delete x \<Gamma>, e, Upd x # S); map_of \<Gamma> x = Some e\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 2. \<And>x S. \<lbrakk>S = Upd x # S; conf' = ((x, ea__) # \<Gamma>, ea__, S); x \<notin> domA \<Gamma>; isVal ea__\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 3. \<And>\<Delta> e. \<lbrakk>ea__ = Terms.Let \<Delta> e; conf' = (\<Delta> @ \<Gamma>, e, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 4. \<And>scrut e1 e2. \<lbrakk>ea__ = (scrut ? e1 : e2); conf' = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 5. \<And>b e1 e2 S. \<lbrakk>ea__ = Bool b; S = Alts e1 e2 # S; conf' = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
from less(1)[OF \<open>length T\<^sub>1 < length T\<close> prem1[unfolded \<open>c\<^sub>3 = _\<close> \<open>c\<^sub>4 = _\<close>  \<open>z' = _\<close>]  \<open>isVal z\<close>]
[PROOF STATE]
proof (chain)
picking this:
delete x \<Gamma> : e \<Down>\<^bsub>upds_list (Upd x # S)\<^esub> \<Delta>' : z
[PROOF STEP]
have "delete x \<Gamma> : e \<Down>\<^bsub>x # upds_list S\<^esub> \<Delta>' : z"
[PROOF STATE]
proof (prove)
using this:
delete x \<Gamma> : e \<Down>\<^bsub>upds_list (Upd x # S)\<^esub> \<Delta>' : z

goal (1 subgoal):
 1. delete x \<Gamma> : e \<Down>\<^bsub>x # upds_list S\<^esub> \<Delta>' : z
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
delete x \<Gamma> : e \<Down>\<^bsub>x # upds_list S\<^esub> \<Delta>' : z

goal (5 subgoals):
 1. \<And>x e. \<lbrakk>ea__ = Var x; conf' = (delete x \<Gamma>, e, Upd x # S); map_of \<Gamma> x = Some e\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 2. \<And>x S. \<lbrakk>S = Upd x # S; conf' = ((x, ea__) # \<Gamma>, ea__, S); x \<notin> domA \<Gamma>; isVal ea__\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 3. \<And>\<Delta> e. \<lbrakk>ea__ = Terms.Let \<Delta> e; conf' = (\<Delta> @ \<Gamma>, e, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 4. \<And>scrut e1 e2. \<lbrakk>ea__ = (scrut ? e1 : e2); conf' = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 5. \<And>b e1 e2 S. \<lbrakk>ea__ = Bool b; S = Alts e1 e2 # S; conf' = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
with \<open>map_of _ _ = _\<close>
[PROOF STATE]
proof (chain)
picking this:
map_of \<Gamma> x = Some e
delete x \<Gamma> : e \<Down>\<^bsub>x # upds_list S\<^esub> \<Delta>' : z
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
map_of \<Gamma> x = Some e
delete x \<Gamma> : e \<Down>\<^bsub>x # upds_list S\<^esub> \<Delta>' : z

goal (1 subgoal):
 1. \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
unfolding var\<^sub>1(1) \<open>\<Delta> = _\<close>
[PROOF STATE]
proof (prove)
using this:
map_of \<Gamma> x = Some e
delete x \<Gamma> : e \<Down>\<^bsub>x # upds_list S\<^esub> \<Delta>' : z

goal (1 subgoal):
 1. \<Gamma> : Var x \<Down>\<^bsub>upds_list S\<^esub> (x, z) # \<Delta>' : z
[PROOF STEP]
by rule
[PROOF STATE]
proof (state)
this:
\<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z

goal (4 subgoals):
 1. \<And>x S. \<lbrakk>S = Upd x # S; conf' = ((x, ea__) # \<Gamma>, ea__, S); x \<notin> domA \<Gamma>; isVal ea__\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 2. \<And>\<Delta> e. \<lbrakk>ea__ = Terms.Let \<Delta> e; conf' = (\<Delta> @ \<Gamma>, e, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 3. \<And>scrut e1 e2. \<lbrakk>ea__ = (scrut ? e1 : e2); conf' = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 4. \<And>b e1 e2 S. \<lbrakk>ea__ = Bool b; S = Alts e1 e2 # S; conf' = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x S. \<lbrakk>S = Upd x # S; conf' = ((x, e) # \<Gamma>, e, S); x \<notin> domA \<Gamma>; isVal e\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 2. \<And>\<Delta> e. \<lbrakk>e = Terms.Let \<Delta> e; conf' = (\<Delta> @ \<Gamma>, e, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 3. \<And>scrut e1 e2. \<lbrakk>e = (scrut ? e1 : e2); conf' = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 4. \<And>b e1 e2 S. \<lbrakk>e = Bool b; S = Alts e1 e2 # S; conf' = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
case (var\<^sub>2 x S')
[PROOF STATE]
proof (state)
this:
S = Upd x # S'
conf' = ((x, e) # \<Gamma>, e, S')
x \<notin> domA \<Gamma>
isVal e

goal (4 subgoals):
 1. \<And>x S. \<lbrakk>S = Upd x # S; conf' = ((x, e) # \<Gamma>, e, S); x \<notin> domA \<Gamma>; isVal e\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 2. \<And>\<Delta> e. \<lbrakk>e = Terms.Let \<Delta> e; conf' = (\<Delta> @ \<Gamma>, e, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 3. \<And>scrut e1 e2. \<lbrakk>e = (scrut ? e1 : e2); conf' = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 4. \<And>b e1 e2 S. \<lbrakk>e = Bool b; S = Alts e1 e2 # S; conf' = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
from \<open>conf' = _\<close> \<open>S = _ # S'\<close> \<open>S \<lesssim> stack conf'\<close>
[PROOF STATE]
proof (chain)
picking this:
conf' = ((x, e) # \<Gamma>, e, S')
S = Upd x # S'
S \<lesssim> stack conf'
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
conf' = ((x, e) # \<Gamma>, e, S')
S = Upd x # S'
S \<lesssim> stack conf'

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

goal (4 subgoals):
 1. \<And>x S. \<lbrakk>S = Upd x # S; conf' = ((x, e) # \<Gamma>, e, S); x \<notin> domA \<Gamma>; isVal e\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 2. \<And>\<Delta> e. \<lbrakk>e = Terms.Let \<Delta> e; conf' = (\<Delta> @ \<Gamma>, e, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 3. \<And>scrut e1 e2. \<lbrakk>e = (scrut ? e1 : e2); conf' = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 4. \<And>b e1 e2 S. \<lbrakk>e = Bool b; S = Alts e1 e2 # S; conf' = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z

goal (3 subgoals):
 1. \<And>\<Delta> e. \<lbrakk>e = Terms.Let \<Delta> e; conf' = (\<Delta> @ \<Gamma>, e, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 2. \<And>scrut e1 e2. \<lbrakk>e = (scrut ? e1 : e2); conf' = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 3. \<And>b e1 e2 S. \<lbrakk>e = Bool b; S = Alts e1 e2 # S; conf' = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>\<Delta> e. \<lbrakk>e = Terms.Let \<Delta> e; conf' = (\<Delta> @ \<Gamma>, e, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 2. \<And>scrut e1 e2. \<lbrakk>e = (scrut ? e1 : e2); conf' = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 3. \<And>b e1 e2 S. \<lbrakk>e = Bool b; S = Alts e1 e2 # S; conf' = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
case (if\<^sub>1 scrut  e\<^sub>1 e\<^sub>2)
[PROOF STATE]
proof (state)
this:
e = (scrut ? e\<^sub>1 : e\<^sub>2)
conf' = (\<Gamma>, scrut, Alts e\<^sub>1 e\<^sub>2 # S)

goal (3 subgoals):
 1. \<And>\<Delta> e. \<lbrakk>e = Terms.Let \<Delta> e; conf' = (\<Delta> @ \<Gamma>, e, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 2. \<And>scrut e1 e2. \<lbrakk>e = (scrut ? e1 : e2); conf' = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 3. \<And>b e1 e2 S. \<lbrakk>e = Bool b; S = Alts e1 e2 # S; conf' = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
obtain T\<^sub>1 c\<^sub>3 c\<^sub>4 T\<^sub>2
      where "T' = T\<^sub>1 @ c\<^sub>4 # T\<^sub>2" and prem1: "(\<Gamma>, scrut, Alts e\<^sub>1 e\<^sub>2 # S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^sub>1\<^esub> c\<^sub>3" and "c\<^sub>3 \<Rightarrow> c\<^sub>4" and prem2: "c\<^sub>4 \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^sub>2\<^esub> (\<Delta>, z, S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>T\<^sub>1 c\<^sub>4 T\<^sub>2 c\<^sub>3. \<lbrakk>T' = T\<^sub>1 @ c\<^sub>4 # T\<^sub>2; (\<Gamma>, scrut, Alts e\<^sub>1 e\<^sub>2 # S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^sub>1\<^esub> c\<^sub>3; c\<^sub>3 \<Rightarrow> c\<^sub>4; c\<^sub>4 \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^sub>2\<^esub> (\<Delta>, z, S)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule bal_consE[OF  \<open>bal _ T _\<close>[unfolded if\<^sub>1 trace_cons]])  (simp, rule)
[PROOF STATE]
proof (state)
this:
T' = T\<^sub>1 @ c\<^sub>4 # T\<^sub>2
(\<Gamma>, scrut, Alts e\<^sub>1 e\<^sub>2 # S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^sub>1\<^esub> c\<^sub>3
c\<^sub>3 \<Rightarrow> c\<^sub>4
c\<^sub>4 \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^sub>2\<^esub> (\<Delta>, z, S)

goal (3 subgoals):
 1. \<And>\<Delta> e. \<lbrakk>e = Terms.Let \<Delta> e; conf' = (\<Delta> @ \<Gamma>, e, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 2. \<And>scrut e1 e2. \<lbrakk>e = (scrut ? e1 : e2); conf' = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 3. \<And>b e1 e2 S. \<lbrakk>e = Bool b; S = Alts e1 e2 # S; conf' = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
from \<open>T = _\<close> \<open>T' = _\<close>
[PROOF STATE]
proof (chain)
picking this:
T = conf' # T'
T' = T\<^sub>1 @ c\<^sub>4 # T\<^sub>2
[PROOF STEP]
have "length T\<^sub>1 < length T" and "length T\<^sub>2 < length T"
[PROOF STATE]
proof (prove)
using this:
T = conf' # T'
T' = T\<^sub>1 @ c\<^sub>4 # T\<^sub>2

goal (1 subgoal):
 1. length T\<^sub>1 < length T &&& length T\<^sub>2 < length T
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length T\<^sub>1 < length T
length T\<^sub>2 < length T

goal (3 subgoals):
 1. \<And>\<Delta> e. \<lbrakk>e = Terms.Let \<Delta> e; conf' = (\<Delta> @ \<Gamma>, e, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 2. \<And>scrut e1 e2. \<lbrakk>e = (scrut ? e1 : e2); conf' = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 3. \<And>b e1 e2 S. \<lbrakk>e = Bool b; S = Alts e1 e2 # S; conf' = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
from prem1
[PROOF STATE]
proof (chain)
picking this:
(\<Gamma>, scrut, Alts e\<^sub>1 e\<^sub>2 # S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^sub>1\<^esub> c\<^sub>3
[PROOF STEP]
have "stack c\<^sub>3 = Alts e\<^sub>1 e\<^sub>2 # S"
[PROOF STATE]
proof (prove)
using this:
(\<Gamma>, scrut, Alts e\<^sub>1 e\<^sub>2 # S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^sub>1\<^esub> c\<^sub>3

goal (1 subgoal):
 1. stack c\<^sub>3 = Alts e\<^sub>1 e\<^sub>2 # S
[PROOF STEP]
by (auto dest:  bal_stackD)
[PROOF STATE]
proof (state)
this:
stack c\<^sub>3 = Alts e\<^sub>1 e\<^sub>2 # S

goal (3 subgoals):
 1. \<And>\<Delta> e. \<lbrakk>e = Terms.Let \<Delta> e; conf' = (\<Delta> @ \<Gamma>, e, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 2. \<And>scrut e1 e2. \<lbrakk>e = (scrut ? e1 : e2); conf' = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 3. \<And>b e1 e2 S. \<lbrakk>e = Bool b; S = Alts e1 e2 # S; conf' = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
stack c\<^sub>3 = Alts e\<^sub>1 e\<^sub>2 # S

goal (3 subgoals):
 1. \<And>\<Delta> e. \<lbrakk>e = Terms.Let \<Delta> e; conf' = (\<Delta> @ \<Gamma>, e, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 2. \<And>scrut e1 e2. \<lbrakk>e = (scrut ? e1 : e2); conf' = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 3. \<And>b e1 e2 S. \<lbrakk>e = Bool b; S = Alts e1 e2 # S; conf' = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
from prem2
[PROOF STATE]
proof (chain)
picking this:
c\<^sub>4 \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^sub>2\<^esub> (\<Delta>, z, S)
[PROOF STEP]
have "stack c\<^sub>4 = S"
[PROOF STATE]
proof (prove)
using this:
c\<^sub>4 \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T\<^sub>2\<^esub> (\<Delta>, z, S)

goal (1 subgoal):
 1. stack c\<^sub>4 = S
[PROOF STEP]
by (auto dest: bal_stackD)
[PROOF STATE]
proof (state)
this:
stack c\<^sub>4 = S

goal (3 subgoals):
 1. \<And>\<Delta> e. \<lbrakk>e = Terms.Let \<Delta> e; conf' = (\<Delta> @ \<Gamma>, e, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 2. \<And>scrut e1 e2. \<lbrakk>e = (scrut ? e1 : e2); conf' = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 3. \<And>b e1 e2 S. \<lbrakk>e = Bool b; S = Alts e1 e2 # S; conf' = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
stack c\<^sub>4 = S

goal (3 subgoals):
 1. \<And>\<Delta> e. \<lbrakk>e = Terms.Let \<Delta> e; conf' = (\<Delta> @ \<Gamma>, e, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 2. \<And>scrut e1 e2. \<lbrakk>e = (scrut ? e1 : e2); conf' = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 3. \<And>b e1 e2 S. \<lbrakk>e = Bool b; S = Alts e1 e2 # S; conf' = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
note \<open>c\<^sub>3 \<Rightarrow> c\<^sub>4\<close>
[PROOF STATE]
proof (state)
this:
c\<^sub>3 \<Rightarrow> c\<^sub>4

goal (3 subgoals):
 1. \<And>\<Delta> e. \<lbrakk>e = Terms.Let \<Delta> e; conf' = (\<Delta> @ \<Gamma>, e, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 2. \<And>scrut e1 e2. \<lbrakk>e = (scrut ? e1 : e2); conf' = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 3. \<And>b e1 e2 S. \<lbrakk>e = Bool b; S = Alts e1 e2 # S; conf' = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
stack c\<^sub>3 = Alts e\<^sub>1 e\<^sub>2 # S
stack c\<^sub>4 = S
c\<^sub>3 \<Rightarrow> c\<^sub>4
[PROOF STEP]
obtain \<Delta>' b where "c\<^sub>3 = (\<Delta>', Bool b, Alts e\<^sub>1 e\<^sub>2 # S)" and "c\<^sub>4 = (\<Delta>', (if b then e\<^sub>1 else e\<^sub>2), S)"
[PROOF STATE]
proof (prove)
using this:
stack c\<^sub>3 = Alts e\<^sub>1 e\<^sub>2 # S
stack c\<^sub>4 = S
c\<^sub>3 \<Rightarrow> c\<^sub>4

goal (1 subgoal):
 1. (\<And>\<Delta>' b. \<lbrakk>c\<^sub>3 = (\<Delta>', Bool b, Alts e\<^sub>1 e\<^sub>2 # S); c\<^sub>4 = (\<Delta>', if b then e\<^sub>1 else e\<^sub>2, S)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto elim!: step.cases simp del: exp_assn.eq_iff)
[PROOF STATE]
proof (state)
this:
c\<^sub>3 = (\<Delta>', Bool b, Alts e\<^sub>1 e\<^sub>2 # S)
c\<^sub>4 = (\<Delta>', if b then e\<^sub>1 else e\<^sub>2, S)

goal (3 subgoals):
 1. \<And>\<Delta> e. \<lbrakk>e = Terms.Let \<Delta> e; conf' = (\<Delta> @ \<Gamma>, e, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 2. \<And>scrut e1 e2. \<lbrakk>e = (scrut ? e1 : e2); conf' = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 3. \<And>b e1 e2 S. \<lbrakk>e = Bool b; S = Alts e1 e2 # S; conf' = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
from less(1)[OF \<open>length T\<^sub>1 < length T\<close> prem1[unfolded \<open>c\<^sub>3 = _\<close> \<open>c\<^sub>4 = _\<close> ] isVal_Bool]
[PROOF STATE]
proof (chain)
picking this:
\<Gamma> : scrut \<Down>\<^bsub>upds_list (Alts e\<^sub>1 e\<^sub>2 # S)\<^esub> \<Delta>' : Bool b
[PROOF STEP]
have "\<Gamma> : scrut \<Down>\<^bsub>upds_list S\<^esub> \<Delta>' : Bool b"
[PROOF STATE]
proof (prove)
using this:
\<Gamma> : scrut \<Down>\<^bsub>upds_list (Alts e\<^sub>1 e\<^sub>2 # S)\<^esub> \<Delta>' : Bool b

goal (1 subgoal):
 1. \<Gamma> : scrut \<Down>\<^bsub>upds_list S\<^esub> \<Delta>' : Bool b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Gamma> : scrut \<Down>\<^bsub>upds_list S\<^esub> \<Delta>' : Bool b

goal (3 subgoals):
 1. \<And>\<Delta> e. \<lbrakk>e = Terms.Let \<Delta> e; conf' = (\<Delta> @ \<Gamma>, e, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 2. \<And>scrut e1 e2. \<lbrakk>e = (scrut ? e1 : e2); conf' = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 3. \<And>b e1 e2 S. \<lbrakk>e = Bool b; S = Alts e1 e2 # S; conf' = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Gamma> : scrut \<Down>\<^bsub>upds_list S\<^esub> \<Delta>' : Bool b

goal (3 subgoals):
 1. \<And>\<Delta> e. \<lbrakk>e = Terms.Let \<Delta> e; conf' = (\<Delta> @ \<Gamma>, e, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 2. \<And>scrut e1 e2. \<lbrakk>e = (scrut ? e1 : e2); conf' = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 3. \<And>b e1 e2 S. \<lbrakk>e = Bool b; S = Alts e1 e2 # S; conf' = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
from less(1)[OF \<open>length T\<^sub>2 < length T\<close> prem2[unfolded \<open>c\<^sub>4 = _\<close>] \<open>isVal z\<close>]
[PROOF STATE]
proof (chain)
picking this:
\<Delta>' : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
have "\<Delta>' : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z"
[PROOF STATE]
proof (prove)
using this:
\<Delta>' : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z

goal (1 subgoal):
 1. \<Delta>' : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<Delta>' : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z

goal (3 subgoals):
 1. \<And>\<Delta> e. \<lbrakk>e = Terms.Let \<Delta> e; conf' = (\<Delta> @ \<Gamma>, e, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 2. \<And>scrut e1 e2. \<lbrakk>e = (scrut ? e1 : e2); conf' = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 3. \<And>b e1 e2 S. \<lbrakk>e = Bool b; S = Alts e1 e2 # S; conf' = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Gamma> : scrut \<Down>\<^bsub>upds_list S\<^esub> \<Delta>' : Bool b
\<Delta>' : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Gamma> : scrut \<Down>\<^bsub>upds_list S\<^esub> \<Delta>' : Bool b
\<Delta>' : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z

goal (1 subgoal):
 1. \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
unfolding if\<^sub>1
[PROOF STATE]
proof (prove)
using this:
\<Gamma> : scrut \<Down>\<^bsub>upds_list S\<^esub> \<Delta>' : Bool b
\<Delta>' : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z

goal (1 subgoal):
 1. \<Gamma> : (scrut ? e\<^sub>1 : e\<^sub>2) \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
by (rule reds.IfThenElse)
[PROOF STATE]
proof (state)
this:
\<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z

goal (2 subgoals):
 1. \<And>\<Delta> e. \<lbrakk>e = Terms.Let \<Delta> e; conf' = (\<Delta> @ \<Gamma>, e, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 2. \<And>b e1 e2 S. \<lbrakk>e = Bool b; S = Alts e1 e2 # S; conf' = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<Delta> e. \<lbrakk>e = Terms.Let \<Delta> e; conf' = (\<Delta> @ \<Gamma>, e, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 2. \<And>b e1 e2 S. \<lbrakk>e = Bool b; S = Alts e1 e2 # S; conf' = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
case (if\<^sub>2 b e1 e2 S')
[PROOF STATE]
proof (state)
this:
e = Bool b
S = Alts e1 e2 # S'
conf' = (\<Gamma>, if b then e1 else e2, S')

goal (2 subgoals):
 1. \<And>\<Delta> e. \<lbrakk>e = Terms.Let \<Delta> e; conf' = (\<Delta> @ \<Gamma>, e, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 2. \<And>b e1 e2 S. \<lbrakk>e = Bool b; S = Alts e1 e2 # S; conf' = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
from \<open>conf' = _\<close> \<open>S = _ # S'\<close> \<open>S \<lesssim> stack conf'\<close>
[PROOF STATE]
proof (chain)
picking this:
conf' = (\<Gamma>, if b then e1 else e2, S')
S = Alts e1 e2 # S'
S \<lesssim> stack conf'
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
conf' = (\<Gamma>, if b then e1 else e2, S')
S = Alts e1 e2 # S'
S \<lesssim> stack conf'

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

goal (2 subgoals):
 1. \<And>\<Delta> e. \<lbrakk>e = Terms.Let \<Delta> e; conf' = (\<Delta> @ \<Gamma>, e, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
 2. \<And>b e1 e2 S. \<lbrakk>e = Bool b; S = Alts e1 e2 # S; conf' = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z

goal (1 subgoal):
 1. \<And>\<Delta> e. \<lbrakk>e = Terms.Let \<Delta> e; conf' = (\<Delta> @ \<Gamma>, e, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<Delta> e. \<lbrakk>e = Terms.Let \<Delta> e; conf' = (\<Delta> @ \<Gamma>, e, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
case (let\<^sub>1 as e)
[PROOF STATE]
proof (state)
this:
ea__ = Terms.Let as e
conf' = (as @ \<Gamma>, e, S)
atom ` domA as \<sharp>* \<Gamma>
atom ` domA as \<sharp>* S

goal (1 subgoal):
 1. \<And>\<Delta> e. \<lbrakk>ea__ = Terms.Let \<Delta> e; conf' = (\<Delta> @ \<Gamma>, e, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
from \<open>T = conf' # T'\<close>
[PROOF STATE]
proof (chain)
picking this:
T = conf' # T'
[PROOF STEP]
have "length T' < length T"
[PROOF STATE]
proof (prove)
using this:
T = conf' # T'

goal (1 subgoal):
 1. length T' < length T
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length T' < length T

goal (1 subgoal):
 1. \<And>\<Delta> e. \<lbrakk>ea__ = Terms.Let \<Delta> e; conf' = (\<Delta> @ \<Gamma>, e, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
length T' < length T

goal (1 subgoal):
 1. \<And>\<Delta> e. \<lbrakk>ea__ = Terms.Let \<Delta> e; conf' = (\<Delta> @ \<Gamma>, e, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
have "(as @ \<Gamma>, e, S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T'\<^esub> (\<Delta>, z, S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (as @ \<Gamma>, e, S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T'\<^esub> (\<Delta>, z, S)
[PROOF STEP]
using trace_cons \<open>conf' = _\<close>  \<open>\<forall> c'\<in>set T. S \<lesssim> stack c'\<close>
[PROOF STATE]
proof (prove)
using this:
T = conf' # T'
conf' \<Rightarrow>\<^sup>*\<^bsub>T'\<^esub> (\<Delta>, z, S)
(\<Gamma>, ea__, S) \<Rightarrow> conf'
conf' = (as @ \<Gamma>, e, S)
\<forall>c'\<in>set T. S \<lesssim> stack c'

goal (1 subgoal):
 1. (as @ \<Gamma>, e, S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T'\<^esub> (\<Delta>, z, S)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(as @ \<Gamma>, e, S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T'\<^esub> (\<Delta>, z, S)

goal (1 subgoal):
 1. \<And>\<Delta> e. \<lbrakk>ea__ = Terms.Let \<Delta> e; conf' = (\<Delta> @ \<Gamma>, e, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(as @ \<Gamma>, e, S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T'\<^esub> (\<Delta>, z, S)

goal (1 subgoal):
 1. \<And>\<Delta> e. \<lbrakk>ea__ = Terms.Let \<Delta> e; conf' = (\<Delta> @ \<Gamma>, e, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
note \<open>isVal z\<close>
[PROOF STATE]
proof (state)
this:
isVal z

goal (1 subgoal):
 1. \<And>\<Delta> e. \<lbrakk>ea__ = Terms.Let \<Delta> e; conf' = (\<Delta> @ \<Gamma>, e, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
length T' < length T
(as @ \<Gamma>, e, S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T'\<^esub> (\<Delta>, z, S)
isVal z
[PROOF STEP]
have "as @ \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z"
[PROOF STATE]
proof (prove)
using this:
length T' < length T
(as @ \<Gamma>, e, S) \<Rightarrow>\<^sup>b\<^sup>*\<^bsub>T'\<^esub> (\<Delta>, z, S)
isVal z

goal (1 subgoal):
 1. as @ \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
by (rule less)
[PROOF STATE]
proof (state)
this:
as @ \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z

goal (1 subgoal):
 1. \<And>\<Delta> e. \<lbrakk>ea__ = Terms.Let \<Delta> e; conf' = (\<Delta> @ \<Gamma>, e, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
as @ \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z

goal (1 subgoal):
 1. \<And>\<Delta> e. \<lbrakk>ea__ = Terms.Let \<Delta> e; conf' = (\<Delta> @ \<Gamma>, e, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
from \<open>atom ` domA as \<sharp>* \<Gamma>\<close>  \<open>atom ` domA as \<sharp>* S\<close>
[PROOF STATE]
proof (chain)
picking this:
atom ` domA as \<sharp>* \<Gamma>
atom ` domA as \<sharp>* S
[PROOF STEP]
have "atom ` domA as \<sharp>* (\<Gamma>, upds_list S)"
[PROOF STATE]
proof (prove)
using this:
atom ` domA as \<sharp>* \<Gamma>
atom ` domA as \<sharp>* S

goal (1 subgoal):
 1. atom ` domA as \<sharp>* (\<Gamma>, upds_list S)
[PROOF STEP]
by (auto simp add: fresh_star_Pair)
[PROOF STATE]
proof (state)
this:
atom ` domA as \<sharp>* (\<Gamma>, upds_list S)

goal (1 subgoal):
 1. \<And>\<Delta> e. \<lbrakk>ea__ = Terms.Let \<Delta> e; conf' = (\<Delta> @ \<Gamma>, e, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
as @ \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
atom ` domA as \<sharp>* (\<Gamma>, upds_list S)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
as @ \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
atom ` domA as \<sharp>* (\<Gamma>, upds_list S)

goal (1 subgoal):
 1. \<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
unfolding let\<^sub>1
[PROOF STATE]
proof (prove)
using this:
as @ \<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
atom ` domA as \<sharp>* (\<Gamma>, upds_list S)

goal (1 subgoal):
 1. \<Gamma> : Terms.Let as e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z
[PROOF STEP]
by (rule reds.Let[rotated])
[PROOF STATE]
proof (state)
this:
\<Gamma> : ea__ \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Gamma> : e \<Down>\<^bsub>upds_list S\<^esub> \<Delta> : z

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dummy_stack_extended:
  "set S \<subseteq>  Dummy ` UNIV \<Longrightarrow> x \<notin> Dummy ` UNIV \<Longrightarrow> (S \<lesssim> x # S') \<longleftrightarrow>  S \<lesssim> S'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>set S \<subseteq> range Dummy; x \<notin> range Dummy\<rbrakk> \<Longrightarrow> (S \<lesssim> x # S') = (S \<lesssim> S')
[PROOF STEP]
apply (auto simp add: extends_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>S''. \<lbrakk>set S \<subseteq> range Dummy; x \<notin> range Dummy; x # S' = S'' @ S\<rbrakk> \<Longrightarrow> \<exists>S''. S' = S'' @ S
[PROOF STEP]
apply (case_tac S'')
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>S''. \<lbrakk>set S \<subseteq> range Dummy; x \<notin> range Dummy; x # S' = S'' @ S; S'' = []\<rbrakk> \<Longrightarrow> \<exists>S''. S' = S'' @ S
 2. \<And>S'' a list. \<lbrakk>set S \<subseteq> range Dummy; x \<notin> range Dummy; x # S' = S'' @ S; S'' = a # list\<rbrakk> \<Longrightarrow> \<exists>S''. S' = S'' @ S
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done