[STATEMENT]
lemma lemma_2:
  assumes "\<Gamma> : e \<Down>\<^bsub>L\<^esub> \<Delta> : z"
  and     "fv (\<Gamma>, e, S) \<subseteq> set L \<union> domA \<Gamma>"
  shows "(\<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Delta>, z, S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Delta>, z, S)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<Gamma> : e \<Down>\<^bsub>L\<^esub> \<Delta> : z
fv (\<Gamma>, e, S) \<subseteq> set L \<union> domA \<Gamma>

goal (1 subgoal):
 1. (\<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Delta>, z, S)
[PROOF STEP]
proof(induction arbitrary: S  rule:reds.induct)
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>\<Gamma> x e L S. fv (\<Gamma>, Lam [x]. e, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, Lam [x]. e, S) \<Rightarrow>\<^sup>* (\<Gamma>, Lam [x]. e, S)
 2. \<And>y \<Gamma> e x L \<Delta> \<Theta> z e' S. \<lbrakk>atom y \<sharp> (\<Gamma>, e, x, L, \<Delta>, \<Theta>, z); \<Gamma> : e \<Down>\<^bsub>L\<^esub> \<Delta> : Lam [y]. e'; \<And>S. fv (\<Gamma>, e, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Delta>, Lam [y]. e', S); \<Delta> : e'[y::=x] \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta>, e'[y::=x], S) \<subseteq> set L \<union> domA \<Delta> \<Longrightarrow> (\<Delta>, e'[y::=x], S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, App e x, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, App e x, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
 3. \<And>\<Gamma> x e L \<Delta> z S. \<lbrakk>map_of \<Gamma> x = Some e; delete x \<Gamma> : e \<Down>\<^bsub>x # L\<^esub> \<Delta> : z; \<And>S. fv (delete x \<Gamma>, e, S) \<subseteq> set (x # L) \<union> domA (delete x \<Gamma>) \<Longrightarrow> (delete x \<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Delta>, z, S); fv (\<Gamma>, Var x, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Var x, S) \<Rightarrow>\<^sup>* ((x, z) # \<Delta>, z, S)
 4. \<And>\<Delta> \<Gamma> L body \<Theta> z S. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta> @ \<Gamma>, body, S) \<subseteq> set L \<union> domA (\<Delta> @ \<Gamma>) \<Longrightarrow> (\<Delta> @ \<Gamma>, body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, Terms.Let \<Delta> body, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Terms.Let \<Delta> body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
 5. \<And>\<Gamma> b L S. fv (\<Gamma>, Bool b, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, Bool b, S) \<Rightarrow>\<^sup>* (\<Gamma>, Bool b, S)
 6. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z S. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; \<And>S. fv (\<Gamma>, scrut, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, scrut, S) \<Rightarrow>\<^sup>* (\<Delta>, Bool b, S); \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<subseteq> set L \<union> domA \<Delta> \<Longrightarrow> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
[PROOF STEP]
case (Lambda \<Gamma> x e L)
[PROOF STATE]
proof (state)
this:
fv (\<Gamma>, Lam [x]. e, S) \<subseteq> set L \<union> domA \<Gamma>

goal (6 subgoals):
 1. \<And>\<Gamma> x e L S. fv (\<Gamma>, Lam [x]. e, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, Lam [x]. e, S) \<Rightarrow>\<^sup>* (\<Gamma>, Lam [x]. e, S)
 2. \<And>y \<Gamma> e x L \<Delta> \<Theta> z e' S. \<lbrakk>atom y \<sharp> (\<Gamma>, e, x, L, \<Delta>, \<Theta>, z); \<Gamma> : e \<Down>\<^bsub>L\<^esub> \<Delta> : Lam [y]. e'; \<And>S. fv (\<Gamma>, e, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Delta>, Lam [y]. e', S); \<Delta> : e'[y::=x] \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta>, e'[y::=x], S) \<subseteq> set L \<union> domA \<Delta> \<Longrightarrow> (\<Delta>, e'[y::=x], S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, App e x, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, App e x, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
 3. \<And>\<Gamma> x e L \<Delta> z S. \<lbrakk>map_of \<Gamma> x = Some e; delete x \<Gamma> : e \<Down>\<^bsub>x # L\<^esub> \<Delta> : z; \<And>S. fv (delete x \<Gamma>, e, S) \<subseteq> set (x # L) \<union> domA (delete x \<Gamma>) \<Longrightarrow> (delete x \<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Delta>, z, S); fv (\<Gamma>, Var x, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Var x, S) \<Rightarrow>\<^sup>* ((x, z) # \<Delta>, z, S)
 4. \<And>\<Delta> \<Gamma> L body \<Theta> z S. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta> @ \<Gamma>, body, S) \<subseteq> set L \<union> domA (\<Delta> @ \<Gamma>) \<Longrightarrow> (\<Delta> @ \<Gamma>, body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, Terms.Let \<Delta> body, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Terms.Let \<Delta> body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
 5. \<And>\<Gamma> b L S. fv (\<Gamma>, Bool b, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, Bool b, S) \<Rightarrow>\<^sup>* (\<Gamma>, Bool b, S)
 6. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z S. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; \<And>S. fv (\<Gamma>, scrut, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, scrut, S) \<Rightarrow>\<^sup>* (\<Delta>, Bool b, S); \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<subseteq> set L \<union> domA \<Delta> \<Longrightarrow> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Gamma>, Lam [x]. e, S) \<Rightarrow>\<^sup>* (\<Gamma>, Lam [x]. e, S)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(\<Gamma>, Lam [x]. e, S) \<Rightarrow>\<^sup>* (\<Gamma>, Lam [x]. e, S)

goal (5 subgoals):
 1. \<And>y \<Gamma> e x L \<Delta> \<Theta> z e' S. \<lbrakk>atom y \<sharp> (\<Gamma>, e, x, L, \<Delta>, \<Theta>, z); \<Gamma> : e \<Down>\<^bsub>L\<^esub> \<Delta> : Lam [y]. e'; \<And>S. fv (\<Gamma>, e, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Delta>, Lam [y]. e', S); \<Delta> : e'[y::=x] \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta>, e'[y::=x], S) \<subseteq> set L \<union> domA \<Delta> \<Longrightarrow> (\<Delta>, e'[y::=x], S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, App e x, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, App e x, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
 2. \<And>\<Gamma> x e L \<Delta> z S. \<lbrakk>map_of \<Gamma> x = Some e; delete x \<Gamma> : e \<Down>\<^bsub>x # L\<^esub> \<Delta> : z; \<And>S. fv (delete x \<Gamma>, e, S) \<subseteq> set (x # L) \<union> domA (delete x \<Gamma>) \<Longrightarrow> (delete x \<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Delta>, z, S); fv (\<Gamma>, Var x, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Var x, S) \<Rightarrow>\<^sup>* ((x, z) # \<Delta>, z, S)
 3. \<And>\<Delta> \<Gamma> L body \<Theta> z S. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta> @ \<Gamma>, body, S) \<subseteq> set L \<union> domA (\<Delta> @ \<Gamma>) \<Longrightarrow> (\<Delta> @ \<Gamma>, body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, Terms.Let \<Delta> body, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Terms.Let \<Delta> body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
 4. \<And>\<Gamma> b L S. fv (\<Gamma>, Bool b, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, Bool b, S) \<Rightarrow>\<^sup>* (\<Gamma>, Bool b, S)
 5. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z S. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; \<And>S. fv (\<Gamma>, scrut, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, scrut, S) \<Rightarrow>\<^sup>* (\<Delta>, Bool b, S); \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<subseteq> set L \<union> domA \<Delta> \<Longrightarrow> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>y \<Gamma> e x L \<Delta> \<Theta> z e' S. \<lbrakk>atom y \<sharp> (\<Gamma>, e, x, L, \<Delta>, \<Theta>, z); \<Gamma> : e \<Down>\<^bsub>L\<^esub> \<Delta> : Lam [y]. e'; \<And>S. fv (\<Gamma>, e, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Delta>, Lam [y]. e', S); \<Delta> : e'[y::=x] \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta>, e'[y::=x], S) \<subseteq> set L \<union> domA \<Delta> \<Longrightarrow> (\<Delta>, e'[y::=x], S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, App e x, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, App e x, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
 2. \<And>\<Gamma> x e L \<Delta> z S. \<lbrakk>map_of \<Gamma> x = Some e; delete x \<Gamma> : e \<Down>\<^bsub>x # L\<^esub> \<Delta> : z; \<And>S. fv (delete x \<Gamma>, e, S) \<subseteq> set (x # L) \<union> domA (delete x \<Gamma>) \<Longrightarrow> (delete x \<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Delta>, z, S); fv (\<Gamma>, Var x, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Var x, S) \<Rightarrow>\<^sup>* ((x, z) # \<Delta>, z, S)
 3. \<And>\<Delta> \<Gamma> L body \<Theta> z S. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta> @ \<Gamma>, body, S) \<subseteq> set L \<union> domA (\<Delta> @ \<Gamma>) \<Longrightarrow> (\<Delta> @ \<Gamma>, body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, Terms.Let \<Delta> body, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Terms.Let \<Delta> body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
 4. \<And>\<Gamma> b L S. fv (\<Gamma>, Bool b, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, Bool b, S) \<Rightarrow>\<^sup>* (\<Gamma>, Bool b, S)
 5. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z S. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; \<And>S. fv (\<Gamma>, scrut, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, scrut, S) \<Rightarrow>\<^sup>* (\<Delta>, Bool b, S); \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<subseteq> set L \<union> domA \<Delta> \<Longrightarrow> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
[PROOF STEP]
case (Application y \<Gamma> e x L \<Delta> \<Theta> z e')
[PROOF STATE]
proof (state)
this:
atom y \<sharp> (\<Gamma>, e, x, L, \<Delta>, \<Theta>, z)
\<Gamma> : e \<Down>\<^bsub>L\<^esub> \<Delta> : Lam [y]. e'
\<Delta> : e'[y::=x] \<Down>\<^bsub>L\<^esub> \<Theta> : z
fv (\<Gamma>, e, ?S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, e, ?S) \<Rightarrow>\<^sup>* (\<Delta>, Lam [y]. e', ?S)
fv (\<Delta>, e'[y::=x], ?S) \<subseteq> set L \<union> domA \<Delta> \<Longrightarrow> (\<Delta>, e'[y::=x], ?S) \<Rightarrow>\<^sup>* (\<Theta>, z, ?S)
fv (\<Gamma>, App e x, S) \<subseteq> set L \<union> domA \<Gamma>

goal (5 subgoals):
 1. \<And>y \<Gamma> e x L \<Delta> \<Theta> z e' S. \<lbrakk>atom y \<sharp> (\<Gamma>, e, x, L, \<Delta>, \<Theta>, z); \<Gamma> : e \<Down>\<^bsub>L\<^esub> \<Delta> : Lam [y]. e'; \<And>S. fv (\<Gamma>, e, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Delta>, Lam [y]. e', S); \<Delta> : e'[y::=x] \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta>, e'[y::=x], S) \<subseteq> set L \<union> domA \<Delta> \<Longrightarrow> (\<Delta>, e'[y::=x], S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, App e x, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, App e x, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
 2. \<And>\<Gamma> x e L \<Delta> z S. \<lbrakk>map_of \<Gamma> x = Some e; delete x \<Gamma> : e \<Down>\<^bsub>x # L\<^esub> \<Delta> : z; \<And>S. fv (delete x \<Gamma>, e, S) \<subseteq> set (x # L) \<union> domA (delete x \<Gamma>) \<Longrightarrow> (delete x \<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Delta>, z, S); fv (\<Gamma>, Var x, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Var x, S) \<Rightarrow>\<^sup>* ((x, z) # \<Delta>, z, S)
 3. \<And>\<Delta> \<Gamma> L body \<Theta> z S. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta> @ \<Gamma>, body, S) \<subseteq> set L \<union> domA (\<Delta> @ \<Gamma>) \<Longrightarrow> (\<Delta> @ \<Gamma>, body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, Terms.Let \<Delta> body, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Terms.Let \<Delta> body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
 4. \<And>\<Gamma> b L S. fv (\<Gamma>, Bool b, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, Bool b, S) \<Rightarrow>\<^sup>* (\<Gamma>, Bool b, S)
 5. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z S. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; \<And>S. fv (\<Gamma>, scrut, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, scrut, S) \<Rightarrow>\<^sup>* (\<Delta>, Bool b, S); \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<subseteq> set L \<union> domA \<Delta> \<Longrightarrow> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
[PROOF STEP]
from \<open>fv (\<Gamma>, App e x, S) \<subseteq> set L \<union> domA \<Gamma>\<close>
[PROOF STATE]
proof (chain)
picking this:
fv (\<Gamma>, App e x, S) \<subseteq> set L \<union> domA \<Gamma>
[PROOF STEP]
have prem1: "fv (\<Gamma>, e, Arg x # S) \<subseteq> set L \<union> domA \<Gamma>"
[PROOF STATE]
proof (prove)
using this:
fv (\<Gamma>, App e x, S) \<subseteq> set L \<union> domA \<Gamma>

goal (1 subgoal):
 1. fv (\<Gamma>, e, Arg x # S) \<subseteq> set L \<union> domA \<Gamma>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fv (\<Gamma>, e, Arg x # S) \<subseteq> set L \<union> domA \<Gamma>

goal (5 subgoals):
 1. \<And>y \<Gamma> e x L \<Delta> \<Theta> z e' S. \<lbrakk>atom y \<sharp> (\<Gamma>, e, x, L, \<Delta>, \<Theta>, z); \<Gamma> : e \<Down>\<^bsub>L\<^esub> \<Delta> : Lam [y]. e'; \<And>S. fv (\<Gamma>, e, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Delta>, Lam [y]. e', S); \<Delta> : e'[y::=x] \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta>, e'[y::=x], S) \<subseteq> set L \<union> domA \<Delta> \<Longrightarrow> (\<Delta>, e'[y::=x], S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, App e x, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, App e x, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
 2. \<And>\<Gamma> x e L \<Delta> z S. \<lbrakk>map_of \<Gamma> x = Some e; delete x \<Gamma> : e \<Down>\<^bsub>x # L\<^esub> \<Delta> : z; \<And>S. fv (delete x \<Gamma>, e, S) \<subseteq> set (x # L) \<union> domA (delete x \<Gamma>) \<Longrightarrow> (delete x \<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Delta>, z, S); fv (\<Gamma>, Var x, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Var x, S) \<Rightarrow>\<^sup>* ((x, z) # \<Delta>, z, S)
 3. \<And>\<Delta> \<Gamma> L body \<Theta> z S. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta> @ \<Gamma>, body, S) \<subseteq> set L \<union> domA (\<Delta> @ \<Gamma>) \<Longrightarrow> (\<Delta> @ \<Gamma>, body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, Terms.Let \<Delta> body, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Terms.Let \<Delta> body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
 4. \<And>\<Gamma> b L S. fv (\<Gamma>, Bool b, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, Bool b, S) \<Rightarrow>\<^sup>* (\<Gamma>, Bool b, S)
 5. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z S. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; \<And>S. fv (\<Gamma>, scrut, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, scrut, S) \<Rightarrow>\<^sup>* (\<Delta>, Bool b, S); \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<subseteq> set L \<union> domA \<Delta> \<Longrightarrow> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
[PROOF STEP]
from prem1 reds_pres_closed[OF \<open>\<Gamma> : e \<Down>\<^bsub>L\<^esub> \<Delta> : Lam [y]. e'\<close>] reds_doesnt_forget[OF \<open>\<Gamma> : e \<Down>\<^bsub>L\<^esub> \<Delta> : Lam [y]. e'\<close>]
[PROOF STATE]
proof (chain)
picking this:
fv (\<Gamma>, e, Arg x # S) \<subseteq> set L \<union> domA \<Gamma>
fv (\<Gamma>, e) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> fv (\<Delta>, Lam [y]. e') \<subseteq> set L \<union> domA \<Delta>
domA \<Gamma> \<subseteq> domA \<Delta>
[PROOF STEP]
have prem2: "fv (\<Delta>, e'[y::=x], S) \<subseteq> set L \<union> domA \<Delta>"
[PROOF STATE]
proof (prove)
using this:
fv (\<Gamma>, e, Arg x # S) \<subseteq> set L \<union> domA \<Gamma>
fv (\<Gamma>, e) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> fv (\<Delta>, Lam [y]. e') \<subseteq> set L \<union> domA \<Delta>
domA \<Gamma> \<subseteq> domA \<Delta>

goal (1 subgoal):
 1. fv (\<Delta>, e'[y::=x], S) \<subseteq> set L \<union> domA \<Delta>
[PROOF STEP]
by (auto simp add: fv_subst_eq)
[PROOF STATE]
proof (state)
this:
fv (\<Delta>, e'[y::=x], S) \<subseteq> set L \<union> domA \<Delta>

goal (5 subgoals):
 1. \<And>y \<Gamma> e x L \<Delta> \<Theta> z e' S. \<lbrakk>atom y \<sharp> (\<Gamma>, e, x, L, \<Delta>, \<Theta>, z); \<Gamma> : e \<Down>\<^bsub>L\<^esub> \<Delta> : Lam [y]. e'; \<And>S. fv (\<Gamma>, e, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Delta>, Lam [y]. e', S); \<Delta> : e'[y::=x] \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta>, e'[y::=x], S) \<subseteq> set L \<union> domA \<Delta> \<Longrightarrow> (\<Delta>, e'[y::=x], S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, App e x, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, App e x, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
 2. \<And>\<Gamma> x e L \<Delta> z S. \<lbrakk>map_of \<Gamma> x = Some e; delete x \<Gamma> : e \<Down>\<^bsub>x # L\<^esub> \<Delta> : z; \<And>S. fv (delete x \<Gamma>, e, S) \<subseteq> set (x # L) \<union> domA (delete x \<Gamma>) \<Longrightarrow> (delete x \<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Delta>, z, S); fv (\<Gamma>, Var x, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Var x, S) \<Rightarrow>\<^sup>* ((x, z) # \<Delta>, z, S)
 3. \<And>\<Delta> \<Gamma> L body \<Theta> z S. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta> @ \<Gamma>, body, S) \<subseteq> set L \<union> domA (\<Delta> @ \<Gamma>) \<Longrightarrow> (\<Delta> @ \<Gamma>, body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, Terms.Let \<Delta> body, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Terms.Let \<Delta> body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
 4. \<And>\<Gamma> b L S. fv (\<Gamma>, Bool b, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, Bool b, S) \<Rightarrow>\<^sup>* (\<Gamma>, Bool b, S)
 5. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z S. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; \<And>S. fv (\<Gamma>, scrut, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, scrut, S) \<Rightarrow>\<^sup>* (\<Delta>, Bool b, S); \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<subseteq> set L \<union> domA \<Delta> \<Longrightarrow> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
[PROOF STEP]
have "(\<Gamma>, App e x, S) \<Rightarrow> (\<Gamma>, e, Arg x # S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Gamma>, App e x, S) \<Rightarrow> (\<Gamma>, e, Arg x # S)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(\<Gamma>, App e x, S) \<Rightarrow> (\<Gamma>, e, Arg x # S)

goal (5 subgoals):
 1. \<And>y \<Gamma> e x L \<Delta> \<Theta> z e' S. \<lbrakk>atom y \<sharp> (\<Gamma>, e, x, L, \<Delta>, \<Theta>, z); \<Gamma> : e \<Down>\<^bsub>L\<^esub> \<Delta> : Lam [y]. e'; \<And>S. fv (\<Gamma>, e, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Delta>, Lam [y]. e', S); \<Delta> : e'[y::=x] \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta>, e'[y::=x], S) \<subseteq> set L \<union> domA \<Delta> \<Longrightarrow> (\<Delta>, e'[y::=x], S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, App e x, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, App e x, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
 2. \<And>\<Gamma> x e L \<Delta> z S. \<lbrakk>map_of \<Gamma> x = Some e; delete x \<Gamma> : e \<Down>\<^bsub>x # L\<^esub> \<Delta> : z; \<And>S. fv (delete x \<Gamma>, e, S) \<subseteq> set (x # L) \<union> domA (delete x \<Gamma>) \<Longrightarrow> (delete x \<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Delta>, z, S); fv (\<Gamma>, Var x, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Var x, S) \<Rightarrow>\<^sup>* ((x, z) # \<Delta>, z, S)
 3. \<And>\<Delta> \<Gamma> L body \<Theta> z S. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta> @ \<Gamma>, body, S) \<subseteq> set L \<union> domA (\<Delta> @ \<Gamma>) \<Longrightarrow> (\<Delta> @ \<Gamma>, body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, Terms.Let \<Delta> body, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Terms.Let \<Delta> body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
 4. \<And>\<Gamma> b L S. fv (\<Gamma>, Bool b, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, Bool b, S) \<Rightarrow>\<^sup>* (\<Gamma>, Bool b, S)
 5. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z S. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; \<And>S. fv (\<Gamma>, scrut, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, scrut, S) \<Rightarrow>\<^sup>* (\<Delta>, Bool b, S); \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<subseteq> set L \<union> domA \<Delta> \<Longrightarrow> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Gamma>, App e x, S) \<Rightarrow> (\<Gamma>, e, Arg x # S)

goal (5 subgoals):
 1. \<And>y \<Gamma> e x L \<Delta> \<Theta> z e' S. \<lbrakk>atom y \<sharp> (\<Gamma>, e, x, L, \<Delta>, \<Theta>, z); \<Gamma> : e \<Down>\<^bsub>L\<^esub> \<Delta> : Lam [y]. e'; \<And>S. fv (\<Gamma>, e, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Delta>, Lam [y]. e', S); \<Delta> : e'[y::=x] \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta>, e'[y::=x], S) \<subseteq> set L \<union> domA \<Delta> \<Longrightarrow> (\<Delta>, e'[y::=x], S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, App e x, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, App e x, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
 2. \<And>\<Gamma> x e L \<Delta> z S. \<lbrakk>map_of \<Gamma> x = Some e; delete x \<Gamma> : e \<Down>\<^bsub>x # L\<^esub> \<Delta> : z; \<And>S. fv (delete x \<Gamma>, e, S) \<subseteq> set (x # L) \<union> domA (delete x \<Gamma>) \<Longrightarrow> (delete x \<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Delta>, z, S); fv (\<Gamma>, Var x, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Var x, S) \<Rightarrow>\<^sup>* ((x, z) # \<Delta>, z, S)
 3. \<And>\<Delta> \<Gamma> L body \<Theta> z S. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta> @ \<Gamma>, body, S) \<subseteq> set L \<union> domA (\<Delta> @ \<Gamma>) \<Longrightarrow> (\<Delta> @ \<Gamma>, body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, Terms.Let \<Delta> body, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Terms.Let \<Delta> body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
 4. \<And>\<Gamma> b L S. fv (\<Gamma>, Bool b, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, Bool b, S) \<Rightarrow>\<^sup>* (\<Gamma>, Bool b, S)
 5. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z S. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; \<And>S. fv (\<Gamma>, scrut, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, scrut, S) \<Rightarrow>\<^sup>* (\<Delta>, Bool b, S); \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<subseteq> set L \<union> domA \<Delta> \<Longrightarrow> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
[PROOF STEP]
have "\<dots> \<Rightarrow>\<^sup>* (\<Delta>, Lam [y]. e', Arg x# S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Gamma>, e, Arg x # S) \<Rightarrow>\<^sup>* (\<Delta>, Lam [y]. e', Arg x # S)
[PROOF STEP]
by (rule Application.IH(1)[OF prem1])
[PROOF STATE]
proof (state)
this:
(\<Gamma>, e, Arg x # S) \<Rightarrow>\<^sup>* (\<Delta>, Lam [y]. e', Arg x # S)

goal (5 subgoals):
 1. \<And>y \<Gamma> e x L \<Delta> \<Theta> z e' S. \<lbrakk>atom y \<sharp> (\<Gamma>, e, x, L, \<Delta>, \<Theta>, z); \<Gamma> : e \<Down>\<^bsub>L\<^esub> \<Delta> : Lam [y]. e'; \<And>S. fv (\<Gamma>, e, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Delta>, Lam [y]. e', S); \<Delta> : e'[y::=x] \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta>, e'[y::=x], S) \<subseteq> set L \<union> domA \<Delta> \<Longrightarrow> (\<Delta>, e'[y::=x], S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, App e x, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, App e x, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
 2. \<And>\<Gamma> x e L \<Delta> z S. \<lbrakk>map_of \<Gamma> x = Some e; delete x \<Gamma> : e \<Down>\<^bsub>x # L\<^esub> \<Delta> : z; \<And>S. fv (delete x \<Gamma>, e, S) \<subseteq> set (x # L) \<union> domA (delete x \<Gamma>) \<Longrightarrow> (delete x \<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Delta>, z, S); fv (\<Gamma>, Var x, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Var x, S) \<Rightarrow>\<^sup>* ((x, z) # \<Delta>, z, S)
 3. \<And>\<Delta> \<Gamma> L body \<Theta> z S. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta> @ \<Gamma>, body, S) \<subseteq> set L \<union> domA (\<Delta> @ \<Gamma>) \<Longrightarrow> (\<Delta> @ \<Gamma>, body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, Terms.Let \<Delta> body, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Terms.Let \<Delta> body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
 4. \<And>\<Gamma> b L S. fv (\<Gamma>, Bool b, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, Bool b, S) \<Rightarrow>\<^sup>* (\<Gamma>, Bool b, S)
 5. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z S. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; \<And>S. fv (\<Gamma>, scrut, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, scrut, S) \<Rightarrow>\<^sup>* (\<Delta>, Bool b, S); \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<subseteq> set L \<union> domA \<Delta> \<Longrightarrow> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Gamma>, e, Arg x # S) \<Rightarrow>\<^sup>* (\<Delta>, Lam [y]. e', Arg x # S)

goal (5 subgoals):
 1. \<And>y \<Gamma> e x L \<Delta> \<Theta> z e' S. \<lbrakk>atom y \<sharp> (\<Gamma>, e, x, L, \<Delta>, \<Theta>, z); \<Gamma> : e \<Down>\<^bsub>L\<^esub> \<Delta> : Lam [y]. e'; \<And>S. fv (\<Gamma>, e, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Delta>, Lam [y]. e', S); \<Delta> : e'[y::=x] \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta>, e'[y::=x], S) \<subseteq> set L \<union> domA \<Delta> \<Longrightarrow> (\<Delta>, e'[y::=x], S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, App e x, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, App e x, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
 2. \<And>\<Gamma> x e L \<Delta> z S. \<lbrakk>map_of \<Gamma> x = Some e; delete x \<Gamma> : e \<Down>\<^bsub>x # L\<^esub> \<Delta> : z; \<And>S. fv (delete x \<Gamma>, e, S) \<subseteq> set (x # L) \<union> domA (delete x \<Gamma>) \<Longrightarrow> (delete x \<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Delta>, z, S); fv (\<Gamma>, Var x, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Var x, S) \<Rightarrow>\<^sup>* ((x, z) # \<Delta>, z, S)
 3. \<And>\<Delta> \<Gamma> L body \<Theta> z S. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta> @ \<Gamma>, body, S) \<subseteq> set L \<union> domA (\<Delta> @ \<Gamma>) \<Longrightarrow> (\<Delta> @ \<Gamma>, body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, Terms.Let \<Delta> body, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Terms.Let \<Delta> body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
 4. \<And>\<Gamma> b L S. fv (\<Gamma>, Bool b, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, Bool b, S) \<Rightarrow>\<^sup>* (\<Gamma>, Bool b, S)
 5. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z S. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; \<And>S. fv (\<Gamma>, scrut, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, scrut, S) \<Rightarrow>\<^sup>* (\<Delta>, Bool b, S); \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<subseteq> set L \<union> domA \<Delta> \<Longrightarrow> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
[PROOF STEP]
have "\<dots> \<Rightarrow> (\<Delta>, e'[y ::= x], S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Delta>, Lam [y]. e', Arg x # S) \<Rightarrow> (\<Delta>, e'[y::=x], S)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(\<Delta>, Lam [y]. e', Arg x # S) \<Rightarrow> (\<Delta>, e'[y::=x], S)

goal (5 subgoals):
 1. \<And>y \<Gamma> e x L \<Delta> \<Theta> z e' S. \<lbrakk>atom y \<sharp> (\<Gamma>, e, x, L, \<Delta>, \<Theta>, z); \<Gamma> : e \<Down>\<^bsub>L\<^esub> \<Delta> : Lam [y]. e'; \<And>S. fv (\<Gamma>, e, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Delta>, Lam [y]. e', S); \<Delta> : e'[y::=x] \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta>, e'[y::=x], S) \<subseteq> set L \<union> domA \<Delta> \<Longrightarrow> (\<Delta>, e'[y::=x], S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, App e x, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, App e x, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
 2. \<And>\<Gamma> x e L \<Delta> z S. \<lbrakk>map_of \<Gamma> x = Some e; delete x \<Gamma> : e \<Down>\<^bsub>x # L\<^esub> \<Delta> : z; \<And>S. fv (delete x \<Gamma>, e, S) \<subseteq> set (x # L) \<union> domA (delete x \<Gamma>) \<Longrightarrow> (delete x \<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Delta>, z, S); fv (\<Gamma>, Var x, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Var x, S) \<Rightarrow>\<^sup>* ((x, z) # \<Delta>, z, S)
 3. \<And>\<Delta> \<Gamma> L body \<Theta> z S. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta> @ \<Gamma>, body, S) \<subseteq> set L \<union> domA (\<Delta> @ \<Gamma>) \<Longrightarrow> (\<Delta> @ \<Gamma>, body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, Terms.Let \<Delta> body, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Terms.Let \<Delta> body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
 4. \<And>\<Gamma> b L S. fv (\<Gamma>, Bool b, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, Bool b, S) \<Rightarrow>\<^sup>* (\<Gamma>, Bool b, S)
 5. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z S. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; \<And>S. fv (\<Gamma>, scrut, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, scrut, S) \<Rightarrow>\<^sup>* (\<Delta>, Bool b, S); \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<subseteq> set L \<union> domA \<Delta> \<Longrightarrow> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Delta>, Lam [y]. e', Arg x # S) \<Rightarrow> (\<Delta>, e'[y::=x], S)

goal (5 subgoals):
 1. \<And>y \<Gamma> e x L \<Delta> \<Theta> z e' S. \<lbrakk>atom y \<sharp> (\<Gamma>, e, x, L, \<Delta>, \<Theta>, z); \<Gamma> : e \<Down>\<^bsub>L\<^esub> \<Delta> : Lam [y]. e'; \<And>S. fv (\<Gamma>, e, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Delta>, Lam [y]. e', S); \<Delta> : e'[y::=x] \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta>, e'[y::=x], S) \<subseteq> set L \<union> domA \<Delta> \<Longrightarrow> (\<Delta>, e'[y::=x], S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, App e x, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, App e x, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
 2. \<And>\<Gamma> x e L \<Delta> z S. \<lbrakk>map_of \<Gamma> x = Some e; delete x \<Gamma> : e \<Down>\<^bsub>x # L\<^esub> \<Delta> : z; \<And>S. fv (delete x \<Gamma>, e, S) \<subseteq> set (x # L) \<union> domA (delete x \<Gamma>) \<Longrightarrow> (delete x \<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Delta>, z, S); fv (\<Gamma>, Var x, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Var x, S) \<Rightarrow>\<^sup>* ((x, z) # \<Delta>, z, S)
 3. \<And>\<Delta> \<Gamma> L body \<Theta> z S. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta> @ \<Gamma>, body, S) \<subseteq> set L \<union> domA (\<Delta> @ \<Gamma>) \<Longrightarrow> (\<Delta> @ \<Gamma>, body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, Terms.Let \<Delta> body, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Terms.Let \<Delta> body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
 4. \<And>\<Gamma> b L S. fv (\<Gamma>, Bool b, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, Bool b, S) \<Rightarrow>\<^sup>* (\<Gamma>, Bool b, S)
 5. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z S. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; \<And>S. fv (\<Gamma>, scrut, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, scrut, S) \<Rightarrow>\<^sup>* (\<Delta>, Bool b, S); \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<subseteq> set L \<union> domA \<Delta> \<Longrightarrow> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
[PROOF STEP]
have "\<dots> \<Rightarrow>\<^sup>* (\<Theta>, z, S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Delta>, e'[y::=x], S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
[PROOF STEP]
by (rule Application.IH(2)[OF prem2])
[PROOF STATE]
proof (state)
this:
(\<Delta>, e'[y::=x], S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)

goal (5 subgoals):
 1. \<And>y \<Gamma> e x L \<Delta> \<Theta> z e' S. \<lbrakk>atom y \<sharp> (\<Gamma>, e, x, L, \<Delta>, \<Theta>, z); \<Gamma> : e \<Down>\<^bsub>L\<^esub> \<Delta> : Lam [y]. e'; \<And>S. fv (\<Gamma>, e, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Delta>, Lam [y]. e', S); \<Delta> : e'[y::=x] \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta>, e'[y::=x], S) \<subseteq> set L \<union> domA \<Delta> \<Longrightarrow> (\<Delta>, e'[y::=x], S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, App e x, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, App e x, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
 2. \<And>\<Gamma> x e L \<Delta> z S. \<lbrakk>map_of \<Gamma> x = Some e; delete x \<Gamma> : e \<Down>\<^bsub>x # L\<^esub> \<Delta> : z; \<And>S. fv (delete x \<Gamma>, e, S) \<subseteq> set (x # L) \<union> domA (delete x \<Gamma>) \<Longrightarrow> (delete x \<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Delta>, z, S); fv (\<Gamma>, Var x, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Var x, S) \<Rightarrow>\<^sup>* ((x, z) # \<Delta>, z, S)
 3. \<And>\<Delta> \<Gamma> L body \<Theta> z S. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta> @ \<Gamma>, body, S) \<subseteq> set L \<union> domA (\<Delta> @ \<Gamma>) \<Longrightarrow> (\<Delta> @ \<Gamma>, body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, Terms.Let \<Delta> body, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Terms.Let \<Delta> body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
 4. \<And>\<Gamma> b L S. fv (\<Gamma>, Bool b, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, Bool b, S) \<Rightarrow>\<^sup>* (\<Gamma>, Bool b, S)
 5. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z S. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; \<And>S. fv (\<Gamma>, scrut, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, scrut, S) \<Rightarrow>\<^sup>* (\<Delta>, Bool b, S); \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<subseteq> set L \<union> domA \<Delta> \<Longrightarrow> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Gamma>, App e x, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(\<Gamma>, App e x, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)

goal (1 subgoal):
 1. (\<Gamma>, App e x, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<Gamma>, App e x, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)

goal (4 subgoals):
 1. \<And>\<Gamma> x e L \<Delta> z S. \<lbrakk>map_of \<Gamma> x = Some e; delete x \<Gamma> : e \<Down>\<^bsub>x # L\<^esub> \<Delta> : z; \<And>S. fv (delete x \<Gamma>, e, S) \<subseteq> set (x # L) \<union> domA (delete x \<Gamma>) \<Longrightarrow> (delete x \<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Delta>, z, S); fv (\<Gamma>, Var x, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Var x, S) \<Rightarrow>\<^sup>* ((x, z) # \<Delta>, z, S)
 2. \<And>\<Delta> \<Gamma> L body \<Theta> z S. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta> @ \<Gamma>, body, S) \<subseteq> set L \<union> domA (\<Delta> @ \<Gamma>) \<Longrightarrow> (\<Delta> @ \<Gamma>, body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, Terms.Let \<Delta> body, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Terms.Let \<Delta> body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
 3. \<And>\<Gamma> b L S. fv (\<Gamma>, Bool b, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, Bool b, S) \<Rightarrow>\<^sup>* (\<Gamma>, Bool b, S)
 4. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z S. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; \<And>S. fv (\<Gamma>, scrut, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, scrut, S) \<Rightarrow>\<^sup>* (\<Delta>, Bool b, S); \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<subseteq> set L \<union> domA \<Delta> \<Longrightarrow> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>\<Gamma> x e L \<Delta> z S. \<lbrakk>map_of \<Gamma> x = Some e; delete x \<Gamma> : e \<Down>\<^bsub>x # L\<^esub> \<Delta> : z; \<And>S. fv (delete x \<Gamma>, e, S) \<subseteq> set (x # L) \<union> domA (delete x \<Gamma>) \<Longrightarrow> (delete x \<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Delta>, z, S); fv (\<Gamma>, Var x, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Var x, S) \<Rightarrow>\<^sup>* ((x, z) # \<Delta>, z, S)
 2. \<And>\<Delta> \<Gamma> L body \<Theta> z S. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta> @ \<Gamma>, body, S) \<subseteq> set L \<union> domA (\<Delta> @ \<Gamma>) \<Longrightarrow> (\<Delta> @ \<Gamma>, body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, Terms.Let \<Delta> body, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Terms.Let \<Delta> body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
 3. \<And>\<Gamma> b L S. fv (\<Gamma>, Bool b, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, Bool b, S) \<Rightarrow>\<^sup>* (\<Gamma>, Bool b, S)
 4. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z S. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; \<And>S. fv (\<Gamma>, scrut, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, scrut, S) \<Rightarrow>\<^sup>* (\<Delta>, Bool b, S); \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<subseteq> set L \<union> domA \<Delta> \<Longrightarrow> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
[PROOF STEP]
case (Variable \<Gamma> x e L \<Delta> z S)
[PROOF STATE]
proof (state)
this:
map_of \<Gamma> x = Some e
delete x \<Gamma> : e \<Down>\<^bsub>x # L\<^esub> \<Delta> : z
fv (delete x \<Gamma>, e, ?S) \<subseteq> set (x # L) \<union> domA (delete x \<Gamma>) \<Longrightarrow> (delete x \<Gamma>, e, ?S) \<Rightarrow>\<^sup>* (\<Delta>, z, ?S)
fv (\<Gamma>, Var x, S) \<subseteq> set L \<union> domA \<Gamma>

goal (4 subgoals):
 1. \<And>\<Gamma> x e L \<Delta> z S. \<lbrakk>map_of \<Gamma> x = Some e; delete x \<Gamma> : e \<Down>\<^bsub>x # L\<^esub> \<Delta> : z; \<And>S. fv (delete x \<Gamma>, e, S) \<subseteq> set (x # L) \<union> domA (delete x \<Gamma>) \<Longrightarrow> (delete x \<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Delta>, z, S); fv (\<Gamma>, Var x, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Var x, S) \<Rightarrow>\<^sup>* ((x, z) # \<Delta>, z, S)
 2. \<And>\<Delta> \<Gamma> L body \<Theta> z S. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta> @ \<Gamma>, body, S) \<subseteq> set L \<union> domA (\<Delta> @ \<Gamma>) \<Longrightarrow> (\<Delta> @ \<Gamma>, body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, Terms.Let \<Delta> body, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Terms.Let \<Delta> body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
 3. \<And>\<Gamma> b L S. fv (\<Gamma>, Bool b, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, Bool b, S) \<Rightarrow>\<^sup>* (\<Gamma>, Bool b, S)
 4. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z S. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; \<And>S. fv (\<Gamma>, scrut, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, scrut, S) \<Rightarrow>\<^sup>* (\<Delta>, Bool b, S); \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<subseteq> set L \<union> domA \<Delta> \<Longrightarrow> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
[PROOF STEP]
from Variable(2)
[PROOF STATE]
proof (chain)
picking this:
delete x \<Gamma> : e \<Down>\<^bsub>x # L\<^esub> \<Delta> : z
[PROOF STEP]
have "isVal z"
[PROOF STATE]
proof (prove)
using this:
delete x \<Gamma> : e \<Down>\<^bsub>x # L\<^esub> \<Delta> : z

goal (1 subgoal):
 1. isVal z
[PROOF STEP]
by (rule result_evaluated)
[PROOF STATE]
proof (state)
this:
isVal z

goal (4 subgoals):
 1. \<And>\<Gamma> x e L \<Delta> z S. \<lbrakk>map_of \<Gamma> x = Some e; delete x \<Gamma> : e \<Down>\<^bsub>x # L\<^esub> \<Delta> : z; \<And>S. fv (delete x \<Gamma>, e, S) \<subseteq> set (x # L) \<union> domA (delete x \<Gamma>) \<Longrightarrow> (delete x \<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Delta>, z, S); fv (\<Gamma>, Var x, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Var x, S) \<Rightarrow>\<^sup>* ((x, z) # \<Delta>, z, S)
 2. \<And>\<Delta> \<Gamma> L body \<Theta> z S. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta> @ \<Gamma>, body, S) \<subseteq> set L \<union> domA (\<Delta> @ \<Gamma>) \<Longrightarrow> (\<Delta> @ \<Gamma>, body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, Terms.Let \<Delta> body, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Terms.Let \<Delta> body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
 3. \<And>\<Gamma> b L S. fv (\<Gamma>, Bool b, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, Bool b, S) \<Rightarrow>\<^sup>* (\<Gamma>, Bool b, S)
 4. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z S. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; \<And>S. fv (\<Gamma>, scrut, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, scrut, S) \<Rightarrow>\<^sup>* (\<Delta>, Bool b, S); \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<subseteq> set L \<union> domA \<Delta> \<Longrightarrow> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
[PROOF STEP]
have "x \<notin> domA \<Delta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<notin> domA \<Delta>
[PROOF STEP]
by (rule reds_avoids_live[OF Variable(2), where x = x]) simp_all
[PROOF STATE]
proof (state)
this:
x \<notin> domA \<Delta>

goal (4 subgoals):
 1. \<And>\<Gamma> x e L \<Delta> z S. \<lbrakk>map_of \<Gamma> x = Some e; delete x \<Gamma> : e \<Down>\<^bsub>x # L\<^esub> \<Delta> : z; \<And>S. fv (delete x \<Gamma>, e, S) \<subseteq> set (x # L) \<union> domA (delete x \<Gamma>) \<Longrightarrow> (delete x \<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Delta>, z, S); fv (\<Gamma>, Var x, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Var x, S) \<Rightarrow>\<^sup>* ((x, z) # \<Delta>, z, S)
 2. \<And>\<Delta> \<Gamma> L body \<Theta> z S. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta> @ \<Gamma>, body, S) \<subseteq> set L \<union> domA (\<Delta> @ \<Gamma>) \<Longrightarrow> (\<Delta> @ \<Gamma>, body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, Terms.Let \<Delta> body, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Terms.Let \<Delta> body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
 3. \<And>\<Gamma> b L S. fv (\<Gamma>, Bool b, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, Bool b, S) \<Rightarrow>\<^sup>* (\<Gamma>, Bool b, S)
 4. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z S. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; \<And>S. fv (\<Gamma>, scrut, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, scrut, S) \<Rightarrow>\<^sup>* (\<Delta>, Bool b, S); \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<subseteq> set L \<union> domA \<Delta> \<Longrightarrow> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
[PROOF STEP]
from \<open>fv (\<Gamma>, Var x, S) \<subseteq> set L \<union> domA \<Gamma>\<close>
[PROOF STATE]
proof (chain)
picking this:
fv (\<Gamma>, Var x, S) \<subseteq> set L \<union> domA \<Gamma>
[PROOF STEP]
have prem: "fv (delete x \<Gamma>, e, Upd x # S) \<subseteq> set (x#L) \<union> domA (delete x \<Gamma>)"
[PROOF STATE]
proof (prove)
using this:
fv (\<Gamma>, Var x, S) \<subseteq> set L \<union> domA \<Gamma>

goal (1 subgoal):
 1. fv (delete x \<Gamma>, e, Upd x # S) \<subseteq> set (x # L) \<union> domA (delete x \<Gamma>)
[PROOF STEP]
by (auto dest: subsetD[OF fv_delete_subset] subsetD[OF map_of_Some_fv_subset[OF \<open>map_of \<Gamma> x = Some e\<close>]])
[PROOF STATE]
proof (state)
this:
fv (delete x \<Gamma>, e, Upd x # S) \<subseteq> set (x # L) \<union> domA (delete x \<Gamma>)

goal (4 subgoals):
 1. \<And>\<Gamma> x e L \<Delta> z S. \<lbrakk>map_of \<Gamma> x = Some e; delete x \<Gamma> : e \<Down>\<^bsub>x # L\<^esub> \<Delta> : z; \<And>S. fv (delete x \<Gamma>, e, S) \<subseteq> set (x # L) \<union> domA (delete x \<Gamma>) \<Longrightarrow> (delete x \<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Delta>, z, S); fv (\<Gamma>, Var x, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Var x, S) \<Rightarrow>\<^sup>* ((x, z) # \<Delta>, z, S)
 2. \<And>\<Delta> \<Gamma> L body \<Theta> z S. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta> @ \<Gamma>, body, S) \<subseteq> set L \<union> domA (\<Delta> @ \<Gamma>) \<Longrightarrow> (\<Delta> @ \<Gamma>, body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, Terms.Let \<Delta> body, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Terms.Let \<Delta> body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
 3. \<And>\<Gamma> b L S. fv (\<Gamma>, Bool b, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, Bool b, S) \<Rightarrow>\<^sup>* (\<Gamma>, Bool b, S)
 4. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z S. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; \<And>S. fv (\<Gamma>, scrut, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, scrut, S) \<Rightarrow>\<^sup>* (\<Delta>, Bool b, S); \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<subseteq> set L \<union> domA \<Delta> \<Longrightarrow> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
[PROOF STEP]
from \<open>map_of \<Gamma> x = Some e\<close>
[PROOF STATE]
proof (chain)
picking this:
map_of \<Gamma> x = Some e
[PROOF STEP]
have "(\<Gamma>, Var x, S) \<Rightarrow> (delete x \<Gamma>, e, Upd x # S)"
[PROOF STATE]
proof (prove)
using this:
map_of \<Gamma> x = Some e

goal (1 subgoal):
 1. (\<Gamma>, Var x, S) \<Rightarrow> (delete x \<Gamma>, e, Upd x # S)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(\<Gamma>, Var x, S) \<Rightarrow> (delete x \<Gamma>, e, Upd x # S)

goal (4 subgoals):
 1. \<And>\<Gamma> x e L \<Delta> z S. \<lbrakk>map_of \<Gamma> x = Some e; delete x \<Gamma> : e \<Down>\<^bsub>x # L\<^esub> \<Delta> : z; \<And>S. fv (delete x \<Gamma>, e, S) \<subseteq> set (x # L) \<union> domA (delete x \<Gamma>) \<Longrightarrow> (delete x \<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Delta>, z, S); fv (\<Gamma>, Var x, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Var x, S) \<Rightarrow>\<^sup>* ((x, z) # \<Delta>, z, S)
 2. \<And>\<Delta> \<Gamma> L body \<Theta> z S. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta> @ \<Gamma>, body, S) \<subseteq> set L \<union> domA (\<Delta> @ \<Gamma>) \<Longrightarrow> (\<Delta> @ \<Gamma>, body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, Terms.Let \<Delta> body, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Terms.Let \<Delta> body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
 3. \<And>\<Gamma> b L S. fv (\<Gamma>, Bool b, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, Bool b, S) \<Rightarrow>\<^sup>* (\<Gamma>, Bool b, S)
 4. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z S. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; \<And>S. fv (\<Gamma>, scrut, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, scrut, S) \<Rightarrow>\<^sup>* (\<Delta>, Bool b, S); \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<subseteq> set L \<union> domA \<Delta> \<Longrightarrow> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Gamma>, Var x, S) \<Rightarrow> (delete x \<Gamma>, e, Upd x # S)

goal (4 subgoals):
 1. \<And>\<Gamma> x e L \<Delta> z S. \<lbrakk>map_of \<Gamma> x = Some e; delete x \<Gamma> : e \<Down>\<^bsub>x # L\<^esub> \<Delta> : z; \<And>S. fv (delete x \<Gamma>, e, S) \<subseteq> set (x # L) \<union> domA (delete x \<Gamma>) \<Longrightarrow> (delete x \<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Delta>, z, S); fv (\<Gamma>, Var x, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Var x, S) \<Rightarrow>\<^sup>* ((x, z) # \<Delta>, z, S)
 2. \<And>\<Delta> \<Gamma> L body \<Theta> z S. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta> @ \<Gamma>, body, S) \<subseteq> set L \<union> domA (\<Delta> @ \<Gamma>) \<Longrightarrow> (\<Delta> @ \<Gamma>, body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, Terms.Let \<Delta> body, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Terms.Let \<Delta> body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
 3. \<And>\<Gamma> b L S. fv (\<Gamma>, Bool b, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, Bool b, S) \<Rightarrow>\<^sup>* (\<Gamma>, Bool b, S)
 4. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z S. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; \<And>S. fv (\<Gamma>, scrut, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, scrut, S) \<Rightarrow>\<^sup>* (\<Delta>, Bool b, S); \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<subseteq> set L \<union> domA \<Delta> \<Longrightarrow> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
[PROOF STEP]
have "\<dots> \<Rightarrow>\<^sup>* (\<Delta>, z, Upd x # S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (delete x \<Gamma>, e, Upd x # S) \<Rightarrow>\<^sup>* (\<Delta>, z, Upd x # S)
[PROOF STEP]
by (rule Variable.IH[OF prem])
[PROOF STATE]
proof (state)
this:
(delete x \<Gamma>, e, Upd x # S) \<Rightarrow>\<^sup>* (\<Delta>, z, Upd x # S)

goal (4 subgoals):
 1. \<And>\<Gamma> x e L \<Delta> z S. \<lbrakk>map_of \<Gamma> x = Some e; delete x \<Gamma> : e \<Down>\<^bsub>x # L\<^esub> \<Delta> : z; \<And>S. fv (delete x \<Gamma>, e, S) \<subseteq> set (x # L) \<union> domA (delete x \<Gamma>) \<Longrightarrow> (delete x \<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Delta>, z, S); fv (\<Gamma>, Var x, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Var x, S) \<Rightarrow>\<^sup>* ((x, z) # \<Delta>, z, S)
 2. \<And>\<Delta> \<Gamma> L body \<Theta> z S. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta> @ \<Gamma>, body, S) \<subseteq> set L \<union> domA (\<Delta> @ \<Gamma>) \<Longrightarrow> (\<Delta> @ \<Gamma>, body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, Terms.Let \<Delta> body, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Terms.Let \<Delta> body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
 3. \<And>\<Gamma> b L S. fv (\<Gamma>, Bool b, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, Bool b, S) \<Rightarrow>\<^sup>* (\<Gamma>, Bool b, S)
 4. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z S. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; \<And>S. fv (\<Gamma>, scrut, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, scrut, S) \<Rightarrow>\<^sup>* (\<Delta>, Bool b, S); \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<subseteq> set L \<union> domA \<Delta> \<Longrightarrow> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(delete x \<Gamma>, e, Upd x # S) \<Rightarrow>\<^sup>* (\<Delta>, z, Upd x # S)

goal (4 subgoals):
 1. \<And>\<Gamma> x e L \<Delta> z S. \<lbrakk>map_of \<Gamma> x = Some e; delete x \<Gamma> : e \<Down>\<^bsub>x # L\<^esub> \<Delta> : z; \<And>S. fv (delete x \<Gamma>, e, S) \<subseteq> set (x # L) \<union> domA (delete x \<Gamma>) \<Longrightarrow> (delete x \<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Delta>, z, S); fv (\<Gamma>, Var x, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Var x, S) \<Rightarrow>\<^sup>* ((x, z) # \<Delta>, z, S)
 2. \<And>\<Delta> \<Gamma> L body \<Theta> z S. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta> @ \<Gamma>, body, S) \<subseteq> set L \<union> domA (\<Delta> @ \<Gamma>) \<Longrightarrow> (\<Delta> @ \<Gamma>, body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, Terms.Let \<Delta> body, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Terms.Let \<Delta> body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
 3. \<And>\<Gamma> b L S. fv (\<Gamma>, Bool b, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, Bool b, S) \<Rightarrow>\<^sup>* (\<Gamma>, Bool b, S)
 4. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z S. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; \<And>S. fv (\<Gamma>, scrut, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, scrut, S) \<Rightarrow>\<^sup>* (\<Delta>, Bool b, S); \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<subseteq> set L \<union> domA \<Delta> \<Longrightarrow> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
[PROOF STEP]
have "\<dots> \<Rightarrow> ((x,z)#\<Delta>, z, S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Delta>, z, Upd x # S) \<Rightarrow> ((x, z) # \<Delta>, z, S)
[PROOF STEP]
using \<open>x \<notin> domA \<Delta>\<close> \<open>isVal z\<close>
[PROOF STATE]
proof (prove)
using this:
x \<notin> domA \<Delta>
isVal z

goal (1 subgoal):
 1. (\<Delta>, z, Upd x # S) \<Rightarrow> ((x, z) # \<Delta>, z, S)
[PROOF STEP]
by (rule var\<^sub>2)
[PROOF STATE]
proof (state)
this:
(\<Delta>, z, Upd x # S) \<Rightarrow> ((x, z) # \<Delta>, z, S)

goal (4 subgoals):
 1. \<And>\<Gamma> x e L \<Delta> z S. \<lbrakk>map_of \<Gamma> x = Some e; delete x \<Gamma> : e \<Down>\<^bsub>x # L\<^esub> \<Delta> : z; \<And>S. fv (delete x \<Gamma>, e, S) \<subseteq> set (x # L) \<union> domA (delete x \<Gamma>) \<Longrightarrow> (delete x \<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Delta>, z, S); fv (\<Gamma>, Var x, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Var x, S) \<Rightarrow>\<^sup>* ((x, z) # \<Delta>, z, S)
 2. \<And>\<Delta> \<Gamma> L body \<Theta> z S. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta> @ \<Gamma>, body, S) \<subseteq> set L \<union> domA (\<Delta> @ \<Gamma>) \<Longrightarrow> (\<Delta> @ \<Gamma>, body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, Terms.Let \<Delta> body, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Terms.Let \<Delta> body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
 3. \<And>\<Gamma> b L S. fv (\<Gamma>, Bool b, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, Bool b, S) \<Rightarrow>\<^sup>* (\<Gamma>, Bool b, S)
 4. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z S. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; \<And>S. fv (\<Gamma>, scrut, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, scrut, S) \<Rightarrow>\<^sup>* (\<Delta>, Bool b, S); \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<subseteq> set L \<union> domA \<Delta> \<Longrightarrow> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Gamma>, Var x, S) \<Rightarrow>\<^sup>* ((x, z) # \<Delta>, z, S)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(\<Gamma>, Var x, S) \<Rightarrow>\<^sup>* ((x, z) # \<Delta>, z, S)

goal (1 subgoal):
 1. (\<Gamma>, Var x, S) \<Rightarrow>\<^sup>* ((x, z) # \<Delta>, z, S)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<Gamma>, Var x, S) \<Rightarrow>\<^sup>* ((x, z) # \<Delta>, z, S)

goal (3 subgoals):
 1. \<And>\<Delta> \<Gamma> L body \<Theta> z S. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta> @ \<Gamma>, body, S) \<subseteq> set L \<union> domA (\<Delta> @ \<Gamma>) \<Longrightarrow> (\<Delta> @ \<Gamma>, body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, Terms.Let \<Delta> body, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Terms.Let \<Delta> body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
 2. \<And>\<Gamma> b L S. fv (\<Gamma>, Bool b, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, Bool b, S) \<Rightarrow>\<^sup>* (\<Gamma>, Bool b, S)
 3. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z S. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; \<And>S. fv (\<Gamma>, scrut, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, scrut, S) \<Rightarrow>\<^sup>* (\<Delta>, Bool b, S); \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<subseteq> set L \<union> domA \<Delta> \<Longrightarrow> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>\<Delta> \<Gamma> L body \<Theta> z S. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta> @ \<Gamma>, body, S) \<subseteq> set L \<union> domA (\<Delta> @ \<Gamma>) \<Longrightarrow> (\<Delta> @ \<Gamma>, body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, Terms.Let \<Delta> body, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Terms.Let \<Delta> body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
 2. \<And>\<Gamma> b L S. fv (\<Gamma>, Bool b, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, Bool b, S) \<Rightarrow>\<^sup>* (\<Gamma>, Bool b, S)
 3. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z S. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; \<And>S. fv (\<Gamma>, scrut, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, scrut, S) \<Rightarrow>\<^sup>* (\<Delta>, Bool b, S); \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<subseteq> set L \<union> domA \<Delta> \<Longrightarrow> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
[PROOF STEP]
case (Bool \<Gamma> b L S)
[PROOF STATE]
proof (state)
this:
fv (\<Gamma>, Bool b, S) \<subseteq> set L \<union> domA \<Gamma>

goal (3 subgoals):
 1. \<And>\<Delta> \<Gamma> L body \<Theta> z S. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta> @ \<Gamma>, body, S) \<subseteq> set L \<union> domA (\<Delta> @ \<Gamma>) \<Longrightarrow> (\<Delta> @ \<Gamma>, body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, Terms.Let \<Delta> body, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Terms.Let \<Delta> body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
 2. \<And>\<Gamma> b L S. fv (\<Gamma>, Bool b, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, Bool b, S) \<Rightarrow>\<^sup>* (\<Gamma>, Bool b, S)
 3. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z S. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; \<And>S. fv (\<Gamma>, scrut, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, scrut, S) \<Rightarrow>\<^sup>* (\<Delta>, Bool b, S); \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<subseteq> set L \<union> domA \<Delta> \<Longrightarrow> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Gamma>, Bool b, S) \<Rightarrow>\<^sup>* (\<Gamma>, Bool b, S)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(\<Gamma>, Bool b, S) \<Rightarrow>\<^sup>* (\<Gamma>, Bool b, S)

goal (2 subgoals):
 1. \<And>\<Delta> \<Gamma> L body \<Theta> z S. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta> @ \<Gamma>, body, S) \<subseteq> set L \<union> domA (\<Delta> @ \<Gamma>) \<Longrightarrow> (\<Delta> @ \<Gamma>, body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, Terms.Let \<Delta> body, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Terms.Let \<Delta> body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
 2. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z S. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; \<And>S. fv (\<Gamma>, scrut, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, scrut, S) \<Rightarrow>\<^sup>* (\<Delta>, Bool b, S); \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<subseteq> set L \<union> domA \<Delta> \<Longrightarrow> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<Delta> \<Gamma> L body \<Theta> z S. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta> @ \<Gamma>, body, S) \<subseteq> set L \<union> domA (\<Delta> @ \<Gamma>) \<Longrightarrow> (\<Delta> @ \<Gamma>, body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, Terms.Let \<Delta> body, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Terms.Let \<Delta> body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
 2. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z S. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; \<And>S. fv (\<Gamma>, scrut, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, scrut, S) \<Rightarrow>\<^sup>* (\<Delta>, Bool b, S); \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<subseteq> set L \<union> domA \<Delta> \<Longrightarrow> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
[PROOF STEP]
case (IfThenElse \<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z S)
[PROOF STATE]
proof (state)
this:
\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b
\<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z
fv (\<Gamma>, scrut, ?S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, scrut, ?S) \<Rightarrow>\<^sup>* (\<Delta>, Bool b, ?S)
fv (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, ?S) \<subseteq> set L \<union> domA \<Delta> \<Longrightarrow> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, ?S) \<Rightarrow>\<^sup>* (\<Theta>, z, ?S)
fv (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<subseteq> set L \<union> domA \<Gamma>

goal (2 subgoals):
 1. \<And>\<Delta> \<Gamma> L body \<Theta> z S. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta> @ \<Gamma>, body, S) \<subseteq> set L \<union> domA (\<Delta> @ \<Gamma>) \<Longrightarrow> (\<Delta> @ \<Gamma>, body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, Terms.Let \<Delta> body, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Terms.Let \<Delta> body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
 2. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z S. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; \<And>S. fv (\<Gamma>, scrut, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, scrut, S) \<Rightarrow>\<^sup>* (\<Delta>, Bool b, S); \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<subseteq> set L \<union> domA \<Delta> \<Longrightarrow> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
[PROOF STEP]
have "(\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<Rightarrow> (\<Gamma>, scrut, Alts e\<^sub>1 e\<^sub>2 #S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<Rightarrow> (\<Gamma>, scrut, Alts e\<^sub>1 e\<^sub>2 # S)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<Rightarrow> (\<Gamma>, scrut, Alts e\<^sub>1 e\<^sub>2 # S)

goal (2 subgoals):
 1. \<And>\<Delta> \<Gamma> L body \<Theta> z S. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta> @ \<Gamma>, body, S) \<subseteq> set L \<union> domA (\<Delta> @ \<Gamma>) \<Longrightarrow> (\<Delta> @ \<Gamma>, body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, Terms.Let \<Delta> body, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Terms.Let \<Delta> body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
 2. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z S. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; \<And>S. fv (\<Gamma>, scrut, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, scrut, S) \<Rightarrow>\<^sup>* (\<Delta>, Bool b, S); \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<subseteq> set L \<union> domA \<Delta> \<Longrightarrow> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<Rightarrow> (\<Gamma>, scrut, Alts e\<^sub>1 e\<^sub>2 # S)

goal (2 subgoals):
 1. \<And>\<Delta> \<Gamma> L body \<Theta> z S. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta> @ \<Gamma>, body, S) \<subseteq> set L \<union> domA (\<Delta> @ \<Gamma>) \<Longrightarrow> (\<Delta> @ \<Gamma>, body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, Terms.Let \<Delta> body, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Terms.Let \<Delta> body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
 2. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z S. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; \<And>S. fv (\<Gamma>, scrut, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, scrut, S) \<Rightarrow>\<^sup>* (\<Delta>, Bool b, S); \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<subseteq> set L \<union> domA \<Delta> \<Longrightarrow> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
[PROOF STEP]
from IfThenElse.prems
[PROOF STATE]
proof (chain)
picking this:
fv (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<subseteq> set L \<union> domA \<Gamma>
[PROOF STEP]
have prem1: "fv (\<Gamma>, scrut, Alts e\<^sub>1 e\<^sub>2 #S) \<subseteq> set L \<union> domA \<Gamma>"
[PROOF STATE]
proof (prove)
using this:
fv (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<subseteq> set L \<union> domA \<Gamma>

goal (1 subgoal):
 1. fv (\<Gamma>, scrut, Alts e\<^sub>1 e\<^sub>2 # S) \<subseteq> set L \<union> domA \<Gamma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fv (\<Gamma>, scrut, Alts e\<^sub>1 e\<^sub>2 # S) \<subseteq> set L \<union> domA \<Gamma>

goal (2 subgoals):
 1. \<And>\<Delta> \<Gamma> L body \<Theta> z S. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta> @ \<Gamma>, body, S) \<subseteq> set L \<union> domA (\<Delta> @ \<Gamma>) \<Longrightarrow> (\<Delta> @ \<Gamma>, body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, Terms.Let \<Delta> body, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Terms.Let \<Delta> body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
 2. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z S. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; \<And>S. fv (\<Gamma>, scrut, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, scrut, S) \<Rightarrow>\<^sup>* (\<Delta>, Bool b, S); \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<subseteq> set L \<union> domA \<Delta> \<Longrightarrow> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
[PROOF STEP]
hence "(\<Gamma>, scrut, Alts e\<^sub>1 e\<^sub>2 #S) \<Rightarrow>\<^sup>* (\<Delta>, Bool b, Alts e\<^sub>1 e\<^sub>2 #S)"
[PROOF STATE]
proof (prove)
using this:
fv (\<Gamma>, scrut, Alts e\<^sub>1 e\<^sub>2 # S) \<subseteq> set L \<union> domA \<Gamma>

goal (1 subgoal):
 1. (\<Gamma>, scrut, Alts e\<^sub>1 e\<^sub>2 # S) \<Rightarrow>\<^sup>* (\<Delta>, Bool b, Alts e\<^sub>1 e\<^sub>2 # S)
[PROOF STEP]
by (rule IfThenElse.IH)
[PROOF STATE]
proof (state)
this:
(\<Gamma>, scrut, Alts e\<^sub>1 e\<^sub>2 # S) \<Rightarrow>\<^sup>* (\<Delta>, Bool b, Alts e\<^sub>1 e\<^sub>2 # S)

goal (2 subgoals):
 1. \<And>\<Delta> \<Gamma> L body \<Theta> z S. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta> @ \<Gamma>, body, S) \<subseteq> set L \<union> domA (\<Delta> @ \<Gamma>) \<Longrightarrow> (\<Delta> @ \<Gamma>, body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, Terms.Let \<Delta> body, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Terms.Let \<Delta> body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
 2. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z S. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; \<And>S. fv (\<Gamma>, scrut, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, scrut, S) \<Rightarrow>\<^sup>* (\<Delta>, Bool b, S); \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<subseteq> set L \<union> domA \<Delta> \<Longrightarrow> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Gamma>, scrut, Alts e\<^sub>1 e\<^sub>2 # S) \<Rightarrow>\<^sup>* (\<Delta>, Bool b, Alts e\<^sub>1 e\<^sub>2 # S)

goal (2 subgoals):
 1. \<And>\<Delta> \<Gamma> L body \<Theta> z S. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta> @ \<Gamma>, body, S) \<subseteq> set L \<union> domA (\<Delta> @ \<Gamma>) \<Longrightarrow> (\<Delta> @ \<Gamma>, body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, Terms.Let \<Delta> body, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Terms.Let \<Delta> body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
 2. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z S. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; \<And>S. fv (\<Gamma>, scrut, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, scrut, S) \<Rightarrow>\<^sup>* (\<Delta>, Bool b, S); \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<subseteq> set L \<union> domA \<Delta> \<Longrightarrow> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
[PROOF STEP]
have "(\<Delta>, Bool b, Alts e\<^sub>1 e\<^sub>2 #S) \<Rightarrow> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Delta>, Bool b, Alts e\<^sub>1 e\<^sub>2 # S) \<Rightarrow> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(\<Delta>, Bool b, Alts e\<^sub>1 e\<^sub>2 # S) \<Rightarrow> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S)

goal (2 subgoals):
 1. \<And>\<Delta> \<Gamma> L body \<Theta> z S. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta> @ \<Gamma>, body, S) \<subseteq> set L \<union> domA (\<Delta> @ \<Gamma>) \<Longrightarrow> (\<Delta> @ \<Gamma>, body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, Terms.Let \<Delta> body, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Terms.Let \<Delta> body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
 2. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z S. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; \<And>S. fv (\<Gamma>, scrut, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, scrut, S) \<Rightarrow>\<^sup>* (\<Delta>, Bool b, S); \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<subseteq> set L \<union> domA \<Delta> \<Longrightarrow> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Delta>, Bool b, Alts e\<^sub>1 e\<^sub>2 # S) \<Rightarrow> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S)

goal (2 subgoals):
 1. \<And>\<Delta> \<Gamma> L body \<Theta> z S. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta> @ \<Gamma>, body, S) \<subseteq> set L \<union> domA (\<Delta> @ \<Gamma>) \<Longrightarrow> (\<Delta> @ \<Gamma>, body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, Terms.Let \<Delta> body, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Terms.Let \<Delta> body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
 2. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z S. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; \<And>S. fv (\<Gamma>, scrut, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, scrut, S) \<Rightarrow>\<^sup>* (\<Delta>, Bool b, S); \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<subseteq> set L \<union> domA \<Delta> \<Longrightarrow> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
[PROOF STEP]
from prem1 reds_pres_closed[OF IfThenElse(1)] reds_doesnt_forget[OF IfThenElse(1)]
[PROOF STATE]
proof (chain)
picking this:
fv (\<Gamma>, scrut, Alts e\<^sub>1 e\<^sub>2 # S) \<subseteq> set L \<union> domA \<Gamma>
fv (\<Gamma>, scrut) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> fv (\<Delta>, Bool b) \<subseteq> set L \<union> domA \<Delta>
domA \<Gamma> \<subseteq> domA \<Delta>
[PROOF STEP]
have prem2: "fv (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<subseteq> set L \<union> domA \<Delta>"
[PROOF STATE]
proof (prove)
using this:
fv (\<Gamma>, scrut, Alts e\<^sub>1 e\<^sub>2 # S) \<subseteq> set L \<union> domA \<Gamma>
fv (\<Gamma>, scrut) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> fv (\<Delta>, Bool b) \<subseteq> set L \<union> domA \<Delta>
domA \<Gamma> \<subseteq> domA \<Delta>

goal (1 subgoal):
 1. fv (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<subseteq> set L \<union> domA \<Delta>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fv (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<subseteq> set L \<union> domA \<Delta>

goal (2 subgoals):
 1. \<And>\<Delta> \<Gamma> L body \<Theta> z S. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta> @ \<Gamma>, body, S) \<subseteq> set L \<union> domA (\<Delta> @ \<Gamma>) \<Longrightarrow> (\<Delta> @ \<Gamma>, body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, Terms.Let \<Delta> body, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Terms.Let \<Delta> body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
 2. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z S. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; \<And>S. fv (\<Gamma>, scrut, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, scrut, S) \<Rightarrow>\<^sup>* (\<Delta>, Bool b, S); \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<subseteq> set L \<union> domA \<Delta> \<Longrightarrow> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
[PROOF STEP]
hence "(\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)"
[PROOF STATE]
proof (prove)
using this:
fv (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<subseteq> set L \<union> domA \<Delta>

goal (1 subgoal):
 1. (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
[PROOF STEP]
by (rule IfThenElse.IH(2))
[PROOF STATE]
proof (state)
this:
(\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)

goal (2 subgoals):
 1. \<And>\<Delta> \<Gamma> L body \<Theta> z S. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta> @ \<Gamma>, body, S) \<subseteq> set L \<union> domA (\<Delta> @ \<Gamma>) \<Longrightarrow> (\<Delta> @ \<Gamma>, body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, Terms.Let \<Delta> body, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Terms.Let \<Delta> body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
 2. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z S. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; \<And>S. fv (\<Gamma>, scrut, S) \<subseteq> set L \<union> domA \<Gamma> \<Longrightarrow> (\<Gamma>, scrut, S) \<Rightarrow>\<^sup>* (\<Delta>, Bool b, S); \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<subseteq> set L \<union> domA \<Delta> \<Longrightarrow> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)

goal (1 subgoal):
 1. (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)

goal (1 subgoal):
 1. \<And>\<Delta> \<Gamma> L body \<Theta> z S. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta> @ \<Gamma>, body, S) \<subseteq> set L \<union> domA (\<Delta> @ \<Gamma>) \<Longrightarrow> (\<Delta> @ \<Gamma>, body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, Terms.Let \<Delta> body, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Terms.Let \<Delta> body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<Delta> \<Gamma> L body \<Theta> z S. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta> @ \<Gamma>, body, S) \<subseteq> set L \<union> domA (\<Delta> @ \<Gamma>) \<Longrightarrow> (\<Delta> @ \<Gamma>, body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, Terms.Let \<Delta> body, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Terms.Let \<Delta> body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
[PROOF STEP]
case (Let as \<Gamma> L body \<Delta> z S)
[PROOF STATE]
proof (state)
this:
atom ` domA as \<sharp>* (\<Gamma>, L)
as @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Delta> : z
fv (as @ \<Gamma>, body, ?S) \<subseteq> set L \<union> domA (as @ \<Gamma>) \<Longrightarrow> (as @ \<Gamma>, body, ?S) \<Rightarrow>\<^sup>* (\<Delta>, z, ?S)
fv (\<Gamma>, Terms.Let as body, S) \<subseteq> set L \<union> domA \<Gamma>

goal (1 subgoal):
 1. \<And>\<Delta> \<Gamma> L body \<Theta> z S. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta> @ \<Gamma>, body, S) \<subseteq> set L \<union> domA (\<Delta> @ \<Gamma>) \<Longrightarrow> (\<Delta> @ \<Gamma>, body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, Terms.Let \<Delta> body, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Terms.Let \<Delta> body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
[PROOF STEP]
from Let(4)
[PROOF STATE]
proof (chain)
picking this:
fv (\<Gamma>, Terms.Let as body, S) \<subseteq> set L \<union> domA \<Gamma>
[PROOF STEP]
have prem: "fv (as @ \<Gamma>, body, S) \<subseteq> set L \<union> domA (as @ \<Gamma>)"
[PROOF STATE]
proof (prove)
using this:
fv (\<Gamma>, Terms.Let as body, S) \<subseteq> set L \<union> domA \<Gamma>

goal (1 subgoal):
 1. fv (as @ \<Gamma>, body, S) \<subseteq> set L \<union> domA (as @ \<Gamma>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fv (as @ \<Gamma>, body, S) \<subseteq> set L \<union> domA (as @ \<Gamma>)

goal (1 subgoal):
 1. \<And>\<Delta> \<Gamma> L body \<Theta> z S. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta> @ \<Gamma>, body, S) \<subseteq> set L \<union> domA (\<Delta> @ \<Gamma>) \<Longrightarrow> (\<Delta> @ \<Gamma>, body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, Terms.Let \<Delta> body, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Terms.Let \<Delta> body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
[PROOF STEP]
from Let(1)
[PROOF STATE]
proof (chain)
picking this:
atom ` domA as \<sharp>* (\<Gamma>, L)
[PROOF STEP]
have "atom ` domA as \<sharp>* \<Gamma>"
[PROOF STATE]
proof (prove)
using this:
atom ` domA as \<sharp>* (\<Gamma>, L)

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

goal (1 subgoal):
 1. \<And>\<Delta> \<Gamma> L body \<Theta> z S. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta> @ \<Gamma>, body, S) \<subseteq> set L \<union> domA (\<Delta> @ \<Gamma>) \<Longrightarrow> (\<Delta> @ \<Gamma>, body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, Terms.Let \<Delta> body, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Terms.Let \<Delta> body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
atom ` domA as \<sharp>* \<Gamma>

goal (1 subgoal):
 1. \<And>\<Delta> \<Gamma> L body \<Theta> z S. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta> @ \<Gamma>, body, S) \<subseteq> set L \<union> domA (\<Delta> @ \<Gamma>) \<Longrightarrow> (\<Delta> @ \<Gamma>, body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, Terms.Let \<Delta> body, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Terms.Let \<Delta> body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
[PROOF STEP]
from Let(1)
[PROOF STATE]
proof (chain)
picking this:
atom ` domA as \<sharp>* (\<Gamma>, L)
[PROOF STEP]
have "domA as \<inter> fv (\<Gamma>, L) = {}"
[PROOF STATE]
proof (prove)
using this:
atom ` domA as \<sharp>* (\<Gamma>, L)

goal (1 subgoal):
 1. domA as \<inter> fv (\<Gamma>, L) = {}
[PROOF STEP]
by (rule fresh_distinct_fv)
[PROOF STATE]
proof (state)
this:
domA as \<inter> fv (\<Gamma>, L) = {}

goal (1 subgoal):
 1. \<And>\<Delta> \<Gamma> L body \<Theta> z S. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta> @ \<Gamma>, body, S) \<subseteq> set L \<union> domA (\<Delta> @ \<Gamma>) \<Longrightarrow> (\<Delta> @ \<Gamma>, body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, Terms.Let \<Delta> body, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Terms.Let \<Delta> body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
[PROOF STEP]
hence "domA as \<inter> (set L \<union> domA \<Gamma>) = {}"
[PROOF STATE]
proof (prove)
using this:
domA as \<inter> fv (\<Gamma>, L) = {}

goal (1 subgoal):
 1. domA as \<inter> (set L \<union> domA \<Gamma>) = {}
[PROOF STEP]
by (auto dest: subsetD[OF domA_fv_subset])
[PROOF STATE]
proof (state)
this:
domA as \<inter> (set L \<union> domA \<Gamma>) = {}

goal (1 subgoal):
 1. \<And>\<Delta> \<Gamma> L body \<Theta> z S. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta> @ \<Gamma>, body, S) \<subseteq> set L \<union> domA (\<Delta> @ \<Gamma>) \<Longrightarrow> (\<Delta> @ \<Gamma>, body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, Terms.Let \<Delta> body, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Terms.Let \<Delta> body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
[PROOF STEP]
with Let(4)
[PROOF STATE]
proof (chain)
picking this:
fv (\<Gamma>, Terms.Let as body, S) \<subseteq> set L \<union> domA \<Gamma>
domA as \<inter> (set L \<union> domA \<Gamma>) = {}
[PROOF STEP]
have "domA as \<inter> fv S = {}"
[PROOF STATE]
proof (prove)
using this:
fv (\<Gamma>, Terms.Let as body, S) \<subseteq> set L \<union> domA \<Gamma>
domA as \<inter> (set L \<union> domA \<Gamma>) = {}

goal (1 subgoal):
 1. domA as \<inter> fv S = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
domA as \<inter> fv S = {}

goal (1 subgoal):
 1. \<And>\<Delta> \<Gamma> L body \<Theta> z S. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta> @ \<Gamma>, body, S) \<subseteq> set L \<union> domA (\<Delta> @ \<Gamma>) \<Longrightarrow> (\<Delta> @ \<Gamma>, body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, Terms.Let \<Delta> body, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Terms.Let \<Delta> body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
[PROOF STEP]
hence "atom ` domA as \<sharp>* S"
[PROOF STATE]
proof (prove)
using this:
domA as \<inter> fv S = {}

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

goal (1 subgoal):
 1. \<And>\<Delta> \<Gamma> L body \<Theta> z S. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta> @ \<Gamma>, body, S) \<subseteq> set L \<union> domA (\<Delta> @ \<Gamma>) \<Longrightarrow> (\<Delta> @ \<Gamma>, body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, Terms.Let \<Delta> body, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Terms.Let \<Delta> body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
atom ` domA as \<sharp>* \<Gamma>
atom ` domA as \<sharp>* S
[PROOF STEP]
have "(\<Gamma>, Terms.Let as body, S) \<Rightarrow> (as@\<Gamma>, body, S)"
[PROOF STATE]
proof (prove)
using this:
atom ` domA as \<sharp>* \<Gamma>
atom ` domA as \<sharp>* S

goal (1 subgoal):
 1. (\<Gamma>, Terms.Let as body, S) \<Rightarrow> (as @ \<Gamma>, body, S)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(\<Gamma>, Terms.Let as body, S) \<Rightarrow> (as @ \<Gamma>, body, S)

goal (1 subgoal):
 1. \<And>\<Delta> \<Gamma> L body \<Theta> z S. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta> @ \<Gamma>, body, S) \<subseteq> set L \<union> domA (\<Delta> @ \<Gamma>) \<Longrightarrow> (\<Delta> @ \<Gamma>, body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, Terms.Let \<Delta> body, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Terms.Let \<Delta> body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Gamma>, Terms.Let as body, S) \<Rightarrow> (as @ \<Gamma>, body, S)

goal (1 subgoal):
 1. \<And>\<Delta> \<Gamma> L body \<Theta> z S. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta> @ \<Gamma>, body, S) \<subseteq> set L \<union> domA (\<Delta> @ \<Gamma>) \<Longrightarrow> (\<Delta> @ \<Gamma>, body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, Terms.Let \<Delta> body, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Terms.Let \<Delta> body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
[PROOF STEP]
have "\<dots> \<Rightarrow>\<^sup>* (\<Delta>, z, S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (as @ \<Gamma>, body, S) \<Rightarrow>\<^sup>* (\<Delta>, z, S)
[PROOF STEP]
by (rule Let.IH[OF prem])
[PROOF STATE]
proof (state)
this:
(as @ \<Gamma>, body, S) \<Rightarrow>\<^sup>* (\<Delta>, z, S)

goal (1 subgoal):
 1. \<And>\<Delta> \<Gamma> L body \<Theta> z S. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; \<And>S. fv (\<Delta> @ \<Gamma>, body, S) \<subseteq> set L \<union> domA (\<Delta> @ \<Gamma>) \<Longrightarrow> (\<Delta> @ \<Gamma>, body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S); fv (\<Gamma>, Terms.Let \<Delta> body, S) \<subseteq> set L \<union> domA \<Gamma>\<rbrakk> \<Longrightarrow> (\<Gamma>, Terms.Let \<Delta> body, S) \<Rightarrow>\<^sup>* (\<Theta>, z, S)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Gamma>, Terms.Let as body, S) \<Rightarrow>\<^sup>* (\<Delta>, z, S)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(\<Gamma>, Terms.Let as body, S) \<Rightarrow>\<^sup>* (\<Delta>, z, S)

goal (1 subgoal):
 1. (\<Gamma>, Terms.Let as body, S) \<Rightarrow>\<^sup>* (\<Delta>, z, S)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<Gamma>, Terms.Let as body, S) \<Rightarrow>\<^sup>* (\<Delta>, z, S)

goal:
No subgoals!
[PROOF STEP]
qed