[STATEMENT]
lemma sestoftUnGCstep:
  assumes "to_gc_conf r c \<Rightarrow>\<^sub>G d"
  assumes "heap_upds_ok_conf c"
  assumes "closed c"
  and "r_ok r c"
  shows   "\<exists> r' c'. c \<Rightarrow>\<^sup>* c' \<and> d = to_gc_conf r' c' \<and> r_ok r' c'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>r' c'. c \<Rightarrow>\<^sup>* c' \<and> d = to_gc_conf r' c' \<and> r_ok r' c'
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>r' c'. c \<Rightarrow>\<^sup>* c' \<and> d = to_gc_conf r' c' \<and> r_ok r' c'
[PROOF STEP]
obtain \<Gamma> e S where "c = (\<Gamma>, e, S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<Gamma> e S. c = (\<Gamma>, e, S) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases c) auto
[PROOF STATE]
proof (state)
this:
c = (\<Gamma>, e, S)

goal (1 subgoal):
 1. \<exists>r' c'. c \<Rightarrow>\<^sup>* c' \<and> d = to_gc_conf r' c' \<and> r_ok r' c'
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
to_gc_conf r c \<Rightarrow>\<^sub>G d
heap_upds_ok_conf c
closed c
r_ok r c
c = (\<Gamma>, e, S)
[PROOF STEP]
have "heap_upds_ok (\<Gamma>,S)" and "closed (\<Gamma>, e, S)" and "r_ok r (\<Gamma>, e, S)"
[PROOF STATE]
proof (prove)
using this:
to_gc_conf r c \<Rightarrow>\<^sub>G d
heap_upds_ok_conf c
closed c
r_ok r c
c = (\<Gamma>, e, S)

goal (1 subgoal):
 1. heap_upds_ok (\<Gamma>, S) &&& closed (\<Gamma>, e, S) &&& r_ok r (\<Gamma>, e, S)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
heap_upds_ok (\<Gamma>, S)
closed (\<Gamma>, e, S)
r_ok r (\<Gamma>, e, S)

goal (1 subgoal):
 1. \<exists>r' c'. c \<Rightarrow>\<^sup>* c' \<and> d = to_gc_conf r' c' \<and> r_ok r' c'
[PROOF STEP]
from sestoftUnGCStack[OF this(1)]
[PROOF STATE]
proof (chain)
picking this:
(\<And>\<Gamma>' S'. \<lbrakk>(\<Gamma>, ?e, S) \<Rightarrow>\<^sup>* (\<Gamma>', ?e, S'); to_gc_conf ?r (\<Gamma>, ?e, S) = to_gc_conf ?r (\<Gamma>', ?e, S'); \<not> isVal ?e \<or> safe_hd S' = safe_hd (restr_stack (- set ?r) S')\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
[PROOF STEP]
obtain \<Gamma>' S' where
    "(\<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Gamma>', e, S')"
    and *: "to_gc_conf r (\<Gamma>, e, S) = to_gc_conf r (\<Gamma>', e, S')"
    and disj: "\<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S')"
[PROOF STATE]
proof (prove)
using this:
(\<And>\<Gamma>' S'. \<lbrakk>(\<Gamma>, ?e, S) \<Rightarrow>\<^sup>* (\<Gamma>', ?e, S'); to_gc_conf ?r (\<Gamma>, ?e, S) = to_gc_conf ?r (\<Gamma>', ?e, S'); \<not> isVal ?e \<or> safe_hd S' = safe_hd (restr_stack (- set ?r) S')\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>\<Gamma>' S'. \<lbrakk>(\<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Gamma>', e, S'); to_gc_conf r (\<Gamma>, e, S) = to_gc_conf r (\<Gamma>', e, S'); \<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(\<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Gamma>', e, S')
to_gc_conf r (\<Gamma>, e, S) = to_gc_conf r (\<Gamma>', e, S')
\<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S')

goal (1 subgoal):
 1. \<exists>r' c'. c \<Rightarrow>\<^sup>* c' \<and> d = to_gc_conf r' c' \<and> r_ok r' c'
[PROOF STEP]
from invariant_starE[OF \<open>_ \<Rightarrow>\<^sup>* _\<close> heap_upds_ok_invariant]  \<open>heap_upds_ok (\<Gamma>,S)\<close>
[PROOF STATE]
proof (chain)
picking this:
heap_upds_ok_conf (\<Gamma>, e, S) \<Longrightarrow> heap_upds_ok_conf (\<Gamma>', e, S')
heap_upds_ok (\<Gamma>, S)
[PROOF STEP]
have "heap_upds_ok (\<Gamma>', S')"
[PROOF STATE]
proof (prove)
using this:
heap_upds_ok_conf (\<Gamma>, e, S) \<Longrightarrow> heap_upds_ok_conf (\<Gamma>', e, S')
heap_upds_ok (\<Gamma>, S)

goal (1 subgoal):
 1. heap_upds_ok (\<Gamma>', S')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
heap_upds_ok (\<Gamma>', S')

goal (1 subgoal):
 1. \<exists>r' c'. c \<Rightarrow>\<^sup>* c' \<and> d = to_gc_conf r' c' \<and> r_ok r' c'
[PROOF STEP]
from invariant_starE[OF \<open>_ \<Rightarrow>\<^sup>* _\<close> closed_invariant  \<open>closed (\<Gamma>, e, S)\<close> ]
[PROOF STATE]
proof (chain)
picking this:
closed (\<Gamma>', e, S')
[PROOF STEP]
have "closed (\<Gamma>', e, S')"
[PROOF STATE]
proof (prove)
using this:
closed (\<Gamma>', e, S')

goal (1 subgoal):
 1. closed (\<Gamma>', e, S')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
closed (\<Gamma>', e, S')

goal (1 subgoal):
 1. \<exists>r' c'. c \<Rightarrow>\<^sup>* c' \<and> d = to_gc_conf r' c' \<and> r_ok r' c'
[PROOF STEP]
from invariant_starE[OF \<open>_ \<Rightarrow>\<^sup>* _\<close> subset_bound_invariant \<open>r_ok r (\<Gamma>, e, S)\<close> ]
[PROOF STATE]
proof (chain)
picking this:
r_ok r (\<Gamma>', e, S')
[PROOF STEP]
have "r_ok r (\<Gamma>', e, S')"
[PROOF STATE]
proof (prove)
using this:
r_ok r (\<Gamma>', e, S')

goal (1 subgoal):
 1. r_ok r (\<Gamma>', e, S')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r_ok r (\<Gamma>', e, S')

goal (1 subgoal):
 1. \<exists>r' c'. c \<Rightarrow>\<^sup>* c' \<and> d = to_gc_conf r' c' \<and> r_ok r' c'
[PROOF STEP]
from assms(1)[unfolded \<open>c =_ \<close> *]
[PROOF STATE]
proof (chain)
picking this:
to_gc_conf r (\<Gamma>', e, S') \<Rightarrow>\<^sub>G d
[PROOF STEP]
have "\<exists> r' \<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow>\<^sup>* (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r' (\<Gamma>'', e'', S'') \<and> r_ok r' (\<Gamma>'', e'', S'')"
[PROOF STATE]
proof (prove)
using this:
to_gc_conf r (\<Gamma>', e, S') \<Rightarrow>\<^sub>G d

goal (1 subgoal):
 1. \<exists>r' \<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow>\<^sup>* (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r' (\<Gamma>'', e'', S'') \<and> r_ok r' (\<Gamma>'', e'', S'')
[PROOF STEP]
proof(cases rule: gc_step.cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. to_gc_conf r (\<Gamma>', e, S') \<Rightarrow> d \<Longrightarrow> \<exists>r' \<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow>\<^sup>* (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r' (\<Gamma>'', e'', S'') \<and> r_ok r' (\<Gamma>'', e'', S'')
 2. \<And>\<Gamma> ea x S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, ea, Upd x # S); d = (\<Gamma>, ea, S @ [Dummy x])\<rbrakk> \<Longrightarrow> \<exists>r' \<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow>\<^sup>* (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r' (\<Gamma>'', e'', S'') \<and> r_ok r' (\<Gamma>'', e'', S'')
[PROOF STEP]
case normal
[PROOF STATE]
proof (state)
this:
to_gc_conf r (\<Gamma>', e, S') \<Rightarrow> d

goal (2 subgoals):
 1. to_gc_conf r (\<Gamma>', e, S') \<Rightarrow> d \<Longrightarrow> \<exists>r' \<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow>\<^sup>* (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r' (\<Gamma>'', e'', S'') \<and> r_ok r' (\<Gamma>'', e'', S'')
 2. \<And>\<Gamma> ea x S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, ea, Upd x # S); d = (\<Gamma>, ea, S @ [Dummy x])\<rbrakk> \<Longrightarrow> \<exists>r' \<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow>\<^sup>* (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r' (\<Gamma>'', e'', S'') \<and> r_ok r' (\<Gamma>'', e'', S'')
[PROOF STEP]
hence "\<exists> \<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')"
[PROOF STATE]
proof (prove)
using this:
to_gc_conf r (\<Gamma>', e, S') \<Rightarrow> d

goal (1 subgoal):
 1. \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
[PROOF STEP]
proof(cases rule: step.cases)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>\<Gamma> ea x S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, App ea x, S); d = (\<Gamma>, ea, Arg x # S)\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
 2. \<And>\<Gamma> y ea x S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, Lam [y]. ea, Arg x # S); d = (\<Gamma>, ea[y::=x], S)\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
 3. \<And>\<Gamma> x ea S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, Var x, S); d = (delete x \<Gamma>, ea, Upd x # S); map_of \<Gamma> x = Some ea\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
 4. \<And>x \<Gamma> ea S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, ea, Upd x # S); d = ((x, ea) # \<Gamma>, ea, S); x \<notin> domA \<Gamma>; isVal ea\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
 5. \<And>\<Delta> \<Gamma> S ea. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, Let \<Delta> ea, S); d = (\<Delta> @ \<Gamma>, ea, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
 6. \<And>\<Gamma> scrut e1 e2 S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, scrut ? e1 : e2, S); d = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
 7. \<And>\<Gamma> b e1 e2 S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, Bool b, Alts e1 e2 # S); d = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
[PROOF STEP]
case app\<^sub>1
[PROOF STATE]
proof (state)
this:
to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>_, App e_ x_, S_)
d = (\<Gamma>_, e_, Arg x_ # S_)

goal (7 subgoals):
 1. \<And>\<Gamma> ea x S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, App ea x, S); d = (\<Gamma>, ea, Arg x # S)\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
 2. \<And>\<Gamma> y ea x S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, Lam [y]. ea, Arg x # S); d = (\<Gamma>, ea[y::=x], S)\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
 3. \<And>\<Gamma> x ea S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, Var x, S); d = (delete x \<Gamma>, ea, Upd x # S); map_of \<Gamma> x = Some ea\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
 4. \<And>x \<Gamma> ea S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, ea, Upd x # S); d = ((x, ea) # \<Gamma>, ea, S); x \<notin> domA \<Gamma>; isVal ea\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
 5. \<And>\<Delta> \<Gamma> S ea. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, Let \<Delta> ea, S); d = (\<Delta> @ \<Gamma>, ea, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
 6. \<And>\<Gamma> scrut e1 e2 S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, scrut ? e1 : e2, S); d = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
 7. \<And>\<Gamma> b e1 e2 S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, Bool b, Alts e1 e2 # S); d = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>_, App e_ x_, S_)
d = (\<Gamma>_, e_, Arg x_ # S_)

goal (1 subgoal):
 1. \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>d = (restrictA (- set r) \<Gamma>', e_, Arg x_ # restr_stack (- set r) S' @ map Dummy (rev r)); \<Gamma>_ = restrictA (- set r) \<Gamma>'; e = App e_ x_; S_ = restr_stack (- set r) S' @ map Dummy (rev r)\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' S''. (\<Gamma>', App e_ x_, S') \<Rightarrow> (\<Gamma>'', e_, S'') \<and> restrictA (- set r) \<Gamma>' = restrictA (- set r) \<Gamma>'' \<and> Arg x_ # restr_stack (- set r) S' = restr_stack (- set r) S''
[PROOF STEP]
apply (intro exI conjI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>d = (restrictA (- set r) \<Gamma>', e_, Arg x_ # restr_stack (- set r) S' @ map Dummy (rev r)); \<Gamma>_ = restrictA (- set r) \<Gamma>'; e = App e_ x_; S_ = restr_stack (- set r) S' @ map Dummy (rev r)\<rbrakk> \<Longrightarrow> (\<Gamma>', App e_ x_, S') \<Rightarrow> (?\<Gamma>''11, e_, ?S''12)
 2. \<lbrakk>d = (restrictA (- set r) \<Gamma>', e_, Arg x_ # restr_stack (- set r) S' @ map Dummy (rev r)); \<Gamma>_ = restrictA (- set r) \<Gamma>'; e = App e_ x_; S_ = restr_stack (- set r) S' @ map Dummy (rev r)\<rbrakk> \<Longrightarrow> restrictA (- set r) \<Gamma>' = restrictA (- set r) ?\<Gamma>''11
 3. \<lbrakk>d = (restrictA (- set r) \<Gamma>', e_, Arg x_ # restr_stack (- set r) S' @ map Dummy (rev r)); \<Gamma>_ = restrictA (- set r) \<Gamma>'; e = App e_ x_; S_ = restr_stack (- set r) S' @ map Dummy (rev r)\<rbrakk> \<Longrightarrow> Arg x_ # restr_stack (- set r) S' = restr_stack (- set r) ?S''12
[PROOF STEP]
apply (rule  step.intros)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>d = (restrictA (- set r) \<Gamma>', e_, Arg x_ # restr_stack (- set r) S' @ map Dummy (rev r)); \<Gamma>_ = restrictA (- set r) \<Gamma>'; e = App e_ x_; S_ = restr_stack (- set r) S' @ map Dummy (rev r)\<rbrakk> \<Longrightarrow> restrictA (- set r) \<Gamma>' = restrictA (- set r) \<Gamma>'
 2. \<lbrakk>d = (restrictA (- set r) \<Gamma>', e_, Arg x_ # restr_stack (- set r) S' @ map Dummy (rev r)); \<Gamma>_ = restrictA (- set r) \<Gamma>'; e = App e_ x_; S_ = restr_stack (- set r) S' @ map Dummy (rev r)\<rbrakk> \<Longrightarrow> Arg x_ # restr_stack (- set r) S' = restr_stack (- set r) (Arg x_ # S')
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')

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

goal (6 subgoals):
 1. \<And>\<Gamma> y ea x S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, Lam [y]. ea, Arg x # S); d = (\<Gamma>, ea[y::=x], S)\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
 2. \<And>\<Gamma> x ea S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, Var x, S); d = (delete x \<Gamma>, ea, Upd x # S); map_of \<Gamma> x = Some ea\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
 3. \<And>x \<Gamma> ea S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, ea, Upd x # S); d = ((x, ea) # \<Gamma>, ea, S); x \<notin> domA \<Gamma>; isVal ea\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
 4. \<And>\<Delta> \<Gamma> S ea. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, Let \<Delta> ea, S); d = (\<Delta> @ \<Gamma>, ea, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
 5. \<And>\<Gamma> scrut e1 e2 S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, scrut ? e1 : e2, S); d = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
 6. \<And>\<Gamma> b e1 e2 S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, Bool b, Alts e1 e2 # S); d = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, Lam [y]. ea, Arg x # S)
d = (\<Gamma>, ea[y::=x], S)

goal (1 subgoal):
 1. \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
[PROOF STEP]
using disj
[PROOF STATE]
proof (prove)
using this:
to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, Lam [y]. ea, Arg x # S)
d = (\<Gamma>, ea[y::=x], S)
\<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S')

goal (1 subgoal):
 1. \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
[PROOF STEP]
apply (cases S')
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, Lam [y]. ea, Arg x # S); d = (\<Gamma>, ea[y::=x], S); \<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S'); S' = []\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
 2. \<And>a list. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, Lam [y]. ea, Arg x # S); d = (\<Gamma>, ea[y::=x], S); \<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S'); S' = a # list\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>list. \<lbrakk>d = (restrictA (- set r) \<Gamma>', ea[y::=x], restr_stack (- set r) list @ map Dummy (rev r)); S' = Arg x # list; \<Gamma> = restrictA (- set r) \<Gamma>'; e = Lam [y]. ea; S = restr_stack (- set r) list @ map Dummy (rev r)\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' S''. (\<Gamma>', Lam [y]. ea, Arg x # list) \<Rightarrow> (\<Gamma>'', ea[y::=x], S'') \<and> restrictA (- set r) \<Gamma>' = restrictA (- set r) \<Gamma>'' \<and> restr_stack (- set r) list = restr_stack (- set r) S''
[PROOF STEP]
apply (intro exI conjI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>list. \<lbrakk>d = (restrictA (- set r) \<Gamma>', ea[y::=x], restr_stack (- set r) list @ map Dummy (rev r)); S' = Arg x # list; \<Gamma> = restrictA (- set r) \<Gamma>'; e = Lam [y]. ea; S = restr_stack (- set r) list @ map Dummy (rev r)\<rbrakk> \<Longrightarrow> (\<Gamma>', Lam [y]. ea, Arg x # list) \<Rightarrow> (?\<Gamma>''27 list, ea[y::=x], ?S''28 list)
 2. \<And>list. \<lbrakk>d = (restrictA (- set r) \<Gamma>', ea[y::=x], restr_stack (- set r) list @ map Dummy (rev r)); S' = Arg x # list; \<Gamma> = restrictA (- set r) \<Gamma>'; e = Lam [y]. ea; S = restr_stack (- set r) list @ map Dummy (rev r)\<rbrakk> \<Longrightarrow> restrictA (- set r) \<Gamma>' = restrictA (- set r) (?\<Gamma>''27 list)
 3. \<And>list. \<lbrakk>d = (restrictA (- set r) \<Gamma>', ea[y::=x], restr_stack (- set r) list @ map Dummy (rev r)); S' = Arg x # list; \<Gamma> = restrictA (- set r) \<Gamma>'; e = Lam [y]. ea; S = restr_stack (- set r) list @ map Dummy (rev r)\<rbrakk> \<Longrightarrow> restr_stack (- set r) list = restr_stack (- set r) (?S''28 list)
[PROOF STEP]
apply (rule step.intros)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>list. \<lbrakk>d = (restrictA (- set r) \<Gamma>', ea[y::=x], restr_stack (- set r) list @ map Dummy (rev r)); S' = Arg x # list; \<Gamma> = restrictA (- set r) \<Gamma>'; e = Lam [y]. ea; S = restr_stack (- set r) list @ map Dummy (rev r)\<rbrakk> \<Longrightarrow> restrictA (- set r) \<Gamma>' = restrictA (- set r) \<Gamma>'
 2. \<And>list. \<lbrakk>d = (restrictA (- set r) \<Gamma>', ea[y::=x], restr_stack (- set r) list @ map Dummy (rev r)); S' = Arg x # list; \<Gamma> = restrictA (- set r) \<Gamma>'; e = Lam [y]. ea; S = restr_stack (- set r) list @ map Dummy (rev r)\<rbrakk> \<Longrightarrow> restr_stack (- set r) list = restr_stack (- set r) list
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')

goal (5 subgoals):
 1. \<And>\<Gamma> x ea S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, Var x, S); d = (delete x \<Gamma>, ea, Upd x # S); map_of \<Gamma> x = Some ea\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
 2. \<And>x \<Gamma> ea S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, ea, Upd x # S); d = ((x, ea) # \<Gamma>, ea, S); x \<notin> domA \<Gamma>; isVal ea\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
 3. \<And>\<Delta> \<Gamma> S ea. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, Let \<Delta> ea, S); d = (\<Delta> @ \<Gamma>, ea, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
 4. \<And>\<Gamma> scrut e1 e2 S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, scrut ? e1 : e2, S); d = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
 5. \<And>\<Gamma> b e1 e2 S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, Bool b, Alts e1 e2 # S); d = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>\<Gamma> x ea S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, Var x, S); d = (delete x \<Gamma>, ea, Upd x # S); map_of \<Gamma> x = Some ea\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
 2. \<And>x \<Gamma> ea S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, ea, Upd x # S); d = ((x, ea) # \<Gamma>, ea, S); x \<notin> domA \<Gamma>; isVal ea\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
 3. \<And>\<Delta> \<Gamma> S ea. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, Let \<Delta> ea, S); d = (\<Delta> @ \<Gamma>, ea, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
 4. \<And>\<Gamma> scrut e1 e2 S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, scrut ? e1 : e2, S); d = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
 5. \<And>\<Gamma> b e1 e2 S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, Bool b, Alts e1 e2 # S); d = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
[PROOF STEP]
case var\<^sub>1
[PROOF STATE]
proof (state)
this:
to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>_, Var x_, S_)
d = (delete x_ \<Gamma>_, e_, Upd x_ # S_)
map_of \<Gamma>_ x_ = Some e_

goal (5 subgoals):
 1. \<And>\<Gamma> x ea S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, Var x, S); d = (delete x \<Gamma>, ea, Upd x # S); map_of \<Gamma> x = Some ea\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
 2. \<And>x \<Gamma> ea S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, ea, Upd x # S); d = ((x, ea) # \<Gamma>, ea, S); x \<notin> domA \<Gamma>; isVal ea\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
 3. \<And>\<Delta> \<Gamma> S ea. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, Let \<Delta> ea, S); d = (\<Delta> @ \<Gamma>, ea, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
 4. \<And>\<Gamma> scrut e1 e2 S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, scrut ? e1 : e2, S); d = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
 5. \<And>\<Gamma> b e1 e2 S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, Bool b, Alts e1 e2 # S); d = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>_, Var x_, S_)
d = (delete x_ \<Gamma>_, e_, Upd x_ # S_)
map_of \<Gamma>_ x_ = Some e_

goal (1 subgoal):
 1. \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>d = (restrictA (- set r - {x_}) \<Gamma>', e_, Upd x_ # restr_stack (- set r) S' @ map Dummy (rev r)); map_of \<Gamma>' x_ = Some e_; \<Gamma>_ = restrictA (- set r) \<Gamma>'; e = Var x_; S_ = restr_stack (- set r) S' @ map Dummy (rev r); x_ \<notin> set r\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' S''. (\<Gamma>', Var x_, S') \<Rightarrow> (\<Gamma>'', e_, S'') \<and> restrictA (- set r - {x_}) \<Gamma>' = restrictA (- set r) \<Gamma>'' \<and> Upd x_ # restr_stack (- set r) S' = restr_stack (- set r) S''
[PROOF STEP]
apply (intro  exI conjI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>d = (restrictA (- set r - {x_}) \<Gamma>', e_, Upd x_ # restr_stack (- set r) S' @ map Dummy (rev r)); map_of \<Gamma>' x_ = Some e_; \<Gamma>_ = restrictA (- set r) \<Gamma>'; e = Var x_; S_ = restr_stack (- set r) S' @ map Dummy (rev r); x_ \<notin> set r\<rbrakk> \<Longrightarrow> (\<Gamma>', Var x_, S') \<Rightarrow> (?\<Gamma>''18, e_, ?S''19)
 2. \<lbrakk>d = (restrictA (- set r - {x_}) \<Gamma>', e_, Upd x_ # restr_stack (- set r) S' @ map Dummy (rev r)); map_of \<Gamma>' x_ = Some e_; \<Gamma>_ = restrictA (- set r) \<Gamma>'; e = Var x_; S_ = restr_stack (- set r) S' @ map Dummy (rev r); x_ \<notin> set r\<rbrakk> \<Longrightarrow> restrictA (- set r - {x_}) \<Gamma>' = restrictA (- set r) ?\<Gamma>''18
 3. \<lbrakk>d = (restrictA (- set r - {x_}) \<Gamma>', e_, Upd x_ # restr_stack (- set r) S' @ map Dummy (rev r)); map_of \<Gamma>' x_ = Some e_; \<Gamma>_ = restrictA (- set r) \<Gamma>'; e = Var x_; S_ = restr_stack (- set r) S' @ map Dummy (rev r); x_ \<notin> set r\<rbrakk> \<Longrightarrow> Upd x_ # restr_stack (- set r) S' = restr_stack (- set r) ?S''19
[PROOF STEP]
apply (rule step.intros)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>d = (restrictA (- set r - {x_}) \<Gamma>', e_, Upd x_ # restr_stack (- set r) S' @ map Dummy (rev r)); map_of \<Gamma>' x_ = Some e_; \<Gamma>_ = restrictA (- set r) \<Gamma>'; e = Var x_; S_ = restr_stack (- set r) S' @ map Dummy (rev r); x_ \<notin> set r\<rbrakk> \<Longrightarrow> map_of \<Gamma>' x_ = Some e_
 2. \<lbrakk>d = (restrictA (- set r - {x_}) \<Gamma>', e_, Upd x_ # restr_stack (- set r) S' @ map Dummy (rev r)); map_of \<Gamma>' x_ = Some e_; \<Gamma>_ = restrictA (- set r) \<Gamma>'; e = Var x_; S_ = restr_stack (- set r) S' @ map Dummy (rev r); x_ \<notin> set r\<rbrakk> \<Longrightarrow> restrictA (- set r - {x_}) \<Gamma>' = restrictA (- set r) (delete x_ \<Gamma>')
 3. \<lbrakk>d = (restrictA (- set r - {x_}) \<Gamma>', e_, Upd x_ # restr_stack (- set r) S' @ map Dummy (rev r)); map_of \<Gamma>' x_ = Some e_; \<Gamma>_ = restrictA (- set r) \<Gamma>'; e = Var x_; S_ = restr_stack (- set r) S' @ map Dummy (rev r); x_ \<notin> set r\<rbrakk> \<Longrightarrow> Upd x_ # restr_stack (- set r) S' = restr_stack (- set r) (Upd x_ # S')
[PROOF STEP]
apply (auto simp add: restr_delete_twist)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')

goal (4 subgoals):
 1. \<And>x \<Gamma> ea S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, ea, Upd x # S); d = ((x, ea) # \<Gamma>, ea, S); x \<notin> domA \<Gamma>; isVal ea\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
 2. \<And>\<Delta> \<Gamma> S ea. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, Let \<Delta> ea, S); d = (\<Delta> @ \<Gamma>, ea, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
 3. \<And>\<Gamma> scrut e1 e2 S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, scrut ? e1 : e2, S); d = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
 4. \<And>\<Gamma> b e1 e2 S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, Bool b, Alts e1 e2 # S); d = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x \<Gamma> ea S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, ea, Upd x # S); d = ((x, ea) # \<Gamma>, ea, S); x \<notin> domA \<Gamma>; isVal ea\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
 2. \<And>\<Delta> \<Gamma> S ea. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, Let \<Delta> ea, S); d = (\<Delta> @ \<Gamma>, ea, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
 3. \<And>\<Gamma> scrut e1 e2 S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, scrut ? e1 : e2, S); d = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
 4. \<And>\<Gamma> b e1 e2 S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, Bool b, Alts e1 e2 # S); d = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
[PROOF STEP]
case var\<^sub>2
[PROOF STATE]
proof (state)
this:
to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>_, e_, Upd x_ # S_)
d = ((x_, e_) # \<Gamma>_, e_, S_)
x_ \<notin> domA \<Gamma>_
isVal e_

goal (4 subgoals):
 1. \<And>x \<Gamma> ea S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, ea, Upd x # S); d = ((x, ea) # \<Gamma>, ea, S); x \<notin> domA \<Gamma>; isVal ea\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
 2. \<And>\<Delta> \<Gamma> S ea. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, Let \<Delta> ea, S); d = (\<Delta> @ \<Gamma>, ea, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
 3. \<And>\<Gamma> scrut e1 e2 S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, scrut ? e1 : e2, S); d = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
 4. \<And>\<Gamma> b e1 e2 S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, Bool b, Alts e1 e2 # S); d = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>_, e_, Upd x_ # S_)
d = ((x_, e_) # \<Gamma>_, e_, S_)
x_ \<notin> domA \<Gamma>_
isVal e_

goal (1 subgoal):
 1. \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
[PROOF STEP]
using disj
[PROOF STATE]
proof (prove)
using this:
to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>_, e_, Upd x_ # S_)
d = ((x_, e_) # \<Gamma>_, e_, S_)
x_ \<notin> domA \<Gamma>_
isVal e_
\<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S')

goal (1 subgoal):
 1. \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
[PROOF STEP]
apply (cases S')
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>_, e_, Upd x_ # S_); d = ((x_, e_) # \<Gamma>_, e_, S_); x_ \<notin> domA \<Gamma>_; isVal e_; \<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S'); S' = []\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
 2. \<And>a list. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>_, e_, Upd x_ # S_); d = ((x_, e_) # \<Gamma>_, e_, S_); x_ \<notin> domA \<Gamma>_; isVal e_; \<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S'); S' = a # list\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>list. \<lbrakk>d = ((x_, e_) # restrictA (- set r) \<Gamma>', e_, restr_stack (- set r) list @ map Dummy (rev r)); isVal e_; (if x_ \<notin> set r then Upd x_ # restr_stack (- set r) list else restr_stack (- set r) list) = Upd x_ # restr_stack (- set r) list; S' = Upd x_ # list; \<Gamma>_ = restrictA (- set r) \<Gamma>'; e = e_; S_ = restr_stack (- set r) list @ map Dummy (rev r); x_ \<notin> domA \<Gamma>'\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' S''. (\<Gamma>', e_, Upd x_ # list) \<Rightarrow> (\<Gamma>'', e_, S'') \<and> (x_, e_) # restrictA (- set r) \<Gamma>' = restrictA (- set r) \<Gamma>'' \<and> restr_stack (- set r) list = restr_stack (- set r) S''
[PROOF STEP]
apply (intro exI conjI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>list. \<lbrakk>d = ((x_, e_) # restrictA (- set r) \<Gamma>', e_, restr_stack (- set r) list @ map Dummy (rev r)); isVal e_; (if x_ \<notin> set r then Upd x_ # restr_stack (- set r) list else restr_stack (- set r) list) = Upd x_ # restr_stack (- set r) list; S' = Upd x_ # list; \<Gamma>_ = restrictA (- set r) \<Gamma>'; e = e_; S_ = restr_stack (- set r) list @ map Dummy (rev r); x_ \<notin> domA \<Gamma>'\<rbrakk> \<Longrightarrow> (\<Gamma>', e_, Upd x_ # list) \<Rightarrow> (?\<Gamma>''29 list, e_, ?S''30 list)
 2. \<And>list. \<lbrakk>d = ((x_, e_) # restrictA (- set r) \<Gamma>', e_, restr_stack (- set r) list @ map Dummy (rev r)); isVal e_; (if x_ \<notin> set r then Upd x_ # restr_stack (- set r) list else restr_stack (- set r) list) = Upd x_ # restr_stack (- set r) list; S' = Upd x_ # list; \<Gamma>_ = restrictA (- set r) \<Gamma>'; e = e_; S_ = restr_stack (- set r) list @ map Dummy (rev r); x_ \<notin> domA \<Gamma>'\<rbrakk> \<Longrightarrow> (x_, e_) # restrictA (- set r) \<Gamma>' = restrictA (- set r) (?\<Gamma>''29 list)
 3. \<And>list. \<lbrakk>d = ((x_, e_) # restrictA (- set r) \<Gamma>', e_, restr_stack (- set r) list @ map Dummy (rev r)); isVal e_; (if x_ \<notin> set r then Upd x_ # restr_stack (- set r) list else restr_stack (- set r) list) = Upd x_ # restr_stack (- set r) list; S' = Upd x_ # list; \<Gamma>_ = restrictA (- set r) \<Gamma>'; e = e_; S_ = restr_stack (- set r) list @ map Dummy (rev r); x_ \<notin> domA \<Gamma>'\<rbrakk> \<Longrightarrow> restr_stack (- set r) list = restr_stack (- set r) (?S''30 list)
[PROOF STEP]
apply (rule step.intros)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>list. \<lbrakk>d = ((x_, e_) # restrictA (- set r) \<Gamma>', e_, restr_stack (- set r) list @ map Dummy (rev r)); isVal e_; (if x_ \<notin> set r then Upd x_ # restr_stack (- set r) list else restr_stack (- set r) list) = Upd x_ # restr_stack (- set r) list; S' = Upd x_ # list; \<Gamma>_ = restrictA (- set r) \<Gamma>'; e = e_; S_ = restr_stack (- set r) list @ map Dummy (rev r); x_ \<notin> domA \<Gamma>'\<rbrakk> \<Longrightarrow> x_ \<notin> domA \<Gamma>'
 2. \<And>list. \<lbrakk>d = ((x_, e_) # restrictA (- set r) \<Gamma>', e_, restr_stack (- set r) list @ map Dummy (rev r)); isVal e_; (if x_ \<notin> set r then Upd x_ # restr_stack (- set r) list else restr_stack (- set r) list) = Upd x_ # restr_stack (- set r) list; S' = Upd x_ # list; \<Gamma>_ = restrictA (- set r) \<Gamma>'; e = e_; S_ = restr_stack (- set r) list @ map Dummy (rev r); x_ \<notin> domA \<Gamma>'\<rbrakk> \<Longrightarrow> isVal e_
 3. \<And>list. \<lbrakk>d = ((x_, e_) # restrictA (- set r) \<Gamma>', e_, restr_stack (- set r) list @ map Dummy (rev r)); isVal e_; (if x_ \<notin> set r then Upd x_ # restr_stack (- set r) list else restr_stack (- set r) list) = Upd x_ # restr_stack (- set r) list; S' = Upd x_ # list; \<Gamma>_ = restrictA (- set r) \<Gamma>'; e = e_; S_ = restr_stack (- set r) list @ map Dummy (rev r); x_ \<notin> domA \<Gamma>'\<rbrakk> \<Longrightarrow> (x_, e_) # restrictA (- set r) \<Gamma>' = restrictA (- set r) ((x_, e_) # \<Gamma>')
 4. \<And>list. \<lbrakk>d = ((x_, e_) # restrictA (- set r) \<Gamma>', e_, restr_stack (- set r) list @ map Dummy (rev r)); isVal e_; (if x_ \<notin> set r then Upd x_ # restr_stack (- set r) list else restr_stack (- set r) list) = Upd x_ # restr_stack (- set r) list; S' = Upd x_ # list; \<Gamma>_ = restrictA (- set r) \<Gamma>'; e = e_; S_ = restr_stack (- set r) list @ map Dummy (rev r); x_ \<notin> domA \<Gamma>'\<rbrakk> \<Longrightarrow> restr_stack (- set r) list = restr_stack (- set r) list
[PROOF STEP]
apply (auto split: if_splits dest: Upd_eq_restr_stackD2)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')

goal (3 subgoals):
 1. \<And>\<Delta> \<Gamma> S ea. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, Let \<Delta> ea, S); d = (\<Delta> @ \<Gamma>, ea, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
 2. \<And>\<Gamma> scrut e1 e2 S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, scrut ? e1 : e2, S); d = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
 3. \<And>\<Gamma> b e1 e2 S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, Bool b, Alts e1 e2 # S); d = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>\<Delta> \<Gamma> S ea. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, Let \<Delta> ea, S); d = (\<Delta> @ \<Gamma>, ea, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
 2. \<And>\<Gamma> scrut e1 e2 S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, scrut ? e1 : e2, S); d = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
 3. \<And>\<Gamma> b e1 e2 S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, Bool b, Alts e1 e2 # S); d = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
[PROOF STEP]
case (let\<^sub>1 \<Delta>'' \<Gamma>'' S'' e')
[PROOF STATE]
proof (state)
this:
to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>'', Let \<Delta>'' e', S'')
d = (\<Delta>'' @ \<Gamma>'', e', S'')
atom ` domA \<Delta>'' \<sharp>* \<Gamma>''
atom ` domA \<Delta>'' \<sharp>* S''

goal (3 subgoals):
 1. \<And>\<Delta> \<Gamma> S ea. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, Let \<Delta> ea, S); d = (\<Delta> @ \<Gamma>, ea, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
 2. \<And>\<Gamma> scrut e1 e2 S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, scrut ? e1 : e2, S); d = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
 3. \<And>\<Gamma> b e1 e2 S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, Bool b, Alts e1 e2 # S); d = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
[PROOF STEP]
from \<open>closed (\<Gamma>', e, S')\<close> let\<^sub>1
[PROOF STATE]
proof (chain)
picking this:
closed (\<Gamma>', e, S')
to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>'', Let \<Delta>'' e', S'')
d = (\<Delta>'' @ \<Gamma>'', e', S'')
atom ` domA \<Delta>'' \<sharp>* \<Gamma>''
atom ` domA \<Delta>'' \<sharp>* S''
[PROOF STEP]
have "closed (\<Gamma>', Let \<Delta>'' e', S')"
[PROOF STATE]
proof (prove)
using this:
closed (\<Gamma>', e, S')
to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>'', Let \<Delta>'' e', S'')
d = (\<Delta>'' @ \<Gamma>'', e', S'')
atom ` domA \<Delta>'' \<sharp>* \<Gamma>''
atom ` domA \<Delta>'' \<sharp>* S''

goal (1 subgoal):
 1. closed (\<Gamma>', Let \<Delta>'' e', S')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
closed (\<Gamma>', Let \<Delta>'' e', S')

goal (3 subgoals):
 1. \<And>\<Delta> \<Gamma> S ea. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, Let \<Delta> ea, S); d = (\<Delta> @ \<Gamma>, ea, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
 2. \<And>\<Gamma> scrut e1 e2 S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, scrut ? e1 : e2, S); d = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
 3. \<And>\<Gamma> b e1 e2 S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, Bool b, Alts e1 e2 # S); d = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
[PROOF STEP]
from fresh_distinct[OF let\<^sub>1(3)] fresh_distinct_fv[OF let\<^sub>1(4)]
[PROOF STATE]
proof (chain)
picking this:
domA \<Delta>'' \<inter> domA \<Gamma>'' = {}
domA \<Delta>'' \<inter> fv S'' = {}
[PROOF STEP]
have "domA \<Delta>'' \<inter> domA \<Gamma>'' = {}" and "domA \<Delta>'' \<inter> upds S'' = {}"  and "domA \<Delta>'' \<inter> dummies S'' = {}"
[PROOF STATE]
proof (prove)
using this:
domA \<Delta>'' \<inter> domA \<Gamma>'' = {}
domA \<Delta>'' \<inter> fv S'' = {}

goal (1 subgoal):
 1. domA \<Delta>'' \<inter> domA \<Gamma>'' = {} &&& domA \<Delta>'' \<inter> upds S'' = {} &&& domA \<Delta>'' \<inter> dummies S'' = {}
[PROOF STEP]
by (auto dest: subsetD[OF ups_fv_subset] subsetD[OF dummies_fv_subset])
[PROOF STATE]
proof (state)
this:
domA \<Delta>'' \<inter> domA \<Gamma>'' = {}
domA \<Delta>'' \<inter> upds S'' = {}
domA \<Delta>'' \<inter> dummies S'' = {}

goal (3 subgoals):
 1. \<And>\<Delta> \<Gamma> S ea. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, Let \<Delta> ea, S); d = (\<Delta> @ \<Gamma>, ea, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
 2. \<And>\<Gamma> scrut e1 e2 S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, scrut ? e1 : e2, S); d = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
 3. \<And>\<Gamma> b e1 e2 S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, Bool b, Alts e1 e2 # S); d = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
domA \<Delta>'' \<inter> domA \<Gamma>'' = {}
domA \<Delta>'' \<inter> upds S'' = {}
domA \<Delta>'' \<inter> dummies S'' = {}

goal (3 subgoals):
 1. \<And>\<Delta> \<Gamma> S ea. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, Let \<Delta> ea, S); d = (\<Delta> @ \<Gamma>, ea, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
 2. \<And>\<Gamma> scrut e1 e2 S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, scrut ? e1 : e2, S); d = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
 3. \<And>\<Gamma> b e1 e2 S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, Bool b, Alts e1 e2 # S); d = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
[PROOF STEP]
from let\<^sub>1(1)
[PROOF STATE]
proof (chain)
picking this:
to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>'', Let \<Delta>'' e', S'')
[PROOF STEP]
have "domA \<Gamma>' \<union> upds S' \<subseteq> domA \<Gamma>'' \<union> upds S'' \<union> dummies S''"
[PROOF STATE]
proof (prove)
using this:
to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>'', Let \<Delta>'' e', S'')

goal (1 subgoal):
 1. domA \<Gamma>' \<union> upds S' \<subseteq> domA \<Gamma>'' \<union> upds S'' \<union> dummies S''
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
domA \<Gamma>' \<union> upds S' \<subseteq> domA \<Gamma>'' \<union> upds S'' \<union> dummies S''

goal (3 subgoals):
 1. \<And>\<Delta> \<Gamma> S ea. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, Let \<Delta> ea, S); d = (\<Delta> @ \<Gamma>, ea, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
 2. \<And>\<Gamma> scrut e1 e2 S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, scrut ? e1 : e2, S); d = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
 3. \<And>\<Gamma> b e1 e2 S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, Bool b, Alts e1 e2 # S); d = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
domA \<Delta>'' \<inter> domA \<Gamma>'' = {}
domA \<Delta>'' \<inter> upds S'' = {}
domA \<Delta>'' \<inter> dummies S'' = {}
domA \<Gamma>' \<union> upds S' \<subseteq> domA \<Gamma>'' \<union> upds S'' \<union> dummies S''
[PROOF STEP]
have disj: "domA \<Delta>'' \<inter> domA \<Gamma>' = {}" "domA \<Delta>'' \<inter> upds S' = {}"
[PROOF STATE]
proof (prove)
using this:
domA \<Delta>'' \<inter> domA \<Gamma>'' = {}
domA \<Delta>'' \<inter> upds S'' = {}
domA \<Delta>'' \<inter> dummies S'' = {}
domA \<Gamma>' \<union> upds S' \<subseteq> domA \<Gamma>'' \<union> upds S'' \<union> dummies S''

goal (1 subgoal):
 1. domA \<Delta>'' \<inter> domA \<Gamma>' = {} &&& domA \<Delta>'' \<inter> upds S' = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
domA \<Delta>'' \<inter> domA \<Gamma>' = {}
domA \<Delta>'' \<inter> upds S' = {}

goal (3 subgoals):
 1. \<And>\<Delta> \<Gamma> S ea. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, Let \<Delta> ea, S); d = (\<Delta> @ \<Gamma>, ea, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
 2. \<And>\<Gamma> scrut e1 e2 S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, scrut ? e1 : e2, S); d = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
 3. \<And>\<Gamma> b e1 e2 S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, Bool b, Alts e1 e2 # S); d = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
[PROOF STEP]
from \<open>domA \<Delta>'' \<inter> dummies S'' = {}\<close> let\<^sub>1(1)
[PROOF STATE]
proof (chain)
picking this:
domA \<Delta>'' \<inter> dummies S'' = {}
to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>'', Let \<Delta>'' e', S'')
[PROOF STEP]
have "domA \<Delta>'' \<inter> set r = {}"
[PROOF STATE]
proof (prove)
using this:
domA \<Delta>'' \<inter> dummies S'' = {}
to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>'', Let \<Delta>'' e', S'')

goal (1 subgoal):
 1. domA \<Delta>'' \<inter> set r = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
domA \<Delta>'' \<inter> set r = {}

goal (3 subgoals):
 1. \<And>\<Delta> \<Gamma> S ea. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, Let \<Delta> ea, S); d = (\<Delta> @ \<Gamma>, ea, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
 2. \<And>\<Gamma> scrut e1 e2 S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, scrut ? e1 : e2, S); d = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
 3. \<And>\<Gamma> b e1 e2 S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, Bool b, Alts e1 e2 # S); d = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
[PROOF STEP]
hence [simp]: "restrictA (- set r) \<Delta>'' = \<Delta>''"
[PROOF STATE]
proof (prove)
using this:
domA \<Delta>'' \<inter> set r = {}

goal (1 subgoal):
 1. restrictA (- set r) \<Delta>'' = \<Delta>''
[PROOF STEP]
by (auto intro: restrictA_noop)
[PROOF STATE]
proof (state)
this:
restrictA (- set r) \<Delta>'' = \<Delta>''

goal (3 subgoals):
 1. \<And>\<Delta> \<Gamma> S ea. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, Let \<Delta> ea, S); d = (\<Delta> @ \<Gamma>, ea, S); atom ` domA \<Delta> \<sharp>* \<Gamma>; atom ` domA \<Delta> \<sharp>* S\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
 2. \<And>\<Gamma> scrut e1 e2 S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, scrut ? e1 : e2, S); d = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
 3. \<And>\<Gamma> b e1 e2 S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, Bool b, Alts e1 e2 # S); d = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
[PROOF STEP]
from let\<^sub>1(1-3)
[PROOF STATE]
proof (chain)
picking this:
to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>'', Let \<Delta>'' e', S'')
d = (\<Delta>'' @ \<Gamma>'', e', S'')
atom ` domA \<Delta>'' \<sharp>* \<Gamma>''
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>'', Let \<Delta>'' e', S'')
d = (\<Delta>'' @ \<Gamma>'', e', S'')
atom ` domA \<Delta>'' \<sharp>* \<Gamma>''

goal (1 subgoal):
 1. \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>d = (\<Delta>'' @ restrictA (- set r) \<Gamma>', e', restr_stack (- set r) S' @ map Dummy (rev r)); atom ` domA \<Delta>'' \<sharp>* restrictA (- set r) \<Gamma>'; \<Gamma>'' = restrictA (- set r) \<Gamma>'; e = Let \<Delta>'' e'; S'' = restr_stack (- set r) S' @ map Dummy (rev r)\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' S''. (\<Gamma>', Let \<Delta>'' e', S') \<Rightarrow> (\<Gamma>'', e', S'') \<and> \<Delta>'' @ restrictA (- set r) \<Gamma>' = restrictA (- set r) \<Gamma>'' \<and> restr_stack (- set r) S' = restr_stack (- set r) S''
[PROOF STEP]
apply (intro  exI[where x = "r"] exI[where x = "\<Delta>'' @ \<Gamma>'"] exI[where x = "S'"] conjI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>d = (\<Delta>'' @ restrictA (- set r) \<Gamma>', e', restr_stack (- set r) S' @ map Dummy (rev r)); atom ` domA \<Delta>'' \<sharp>* restrictA (- set r) \<Gamma>'; \<Gamma>'' = restrictA (- set r) \<Gamma>'; e = Let \<Delta>'' e'; S'' = restr_stack (- set r) S' @ map Dummy (rev r)\<rbrakk> \<Longrightarrow> (\<Gamma>', Let \<Delta>'' e', S') \<Rightarrow> (\<Delta>'' @ \<Gamma>', e', S')
 2. \<lbrakk>d = (\<Delta>'' @ restrictA (- set r) \<Gamma>', e', restr_stack (- set r) S' @ map Dummy (rev r)); atom ` domA \<Delta>'' \<sharp>* restrictA (- set r) \<Gamma>'; \<Gamma>'' = restrictA (- set r) \<Gamma>'; e = Let \<Delta>'' e'; S'' = restr_stack (- set r) S' @ map Dummy (rev r)\<rbrakk> \<Longrightarrow> \<Delta>'' @ restrictA (- set r) \<Gamma>' = restrictA (- set r) (\<Delta>'' @ \<Gamma>')
 3. \<lbrakk>d = (\<Delta>'' @ restrictA (- set r) \<Gamma>', e', restr_stack (- set r) S' @ map Dummy (rev r)); atom ` domA \<Delta>'' \<sharp>* restrictA (- set r) \<Gamma>'; \<Gamma>'' = restrictA (- set r) \<Gamma>'; e = Let \<Delta>'' e'; S'' = restr_stack (- set r) S' @ map Dummy (rev r)\<rbrakk> \<Longrightarrow> restr_stack (- set r) S' = restr_stack (- set r) S'
[PROOF STEP]
apply (rule let\<^sub>1_closed[OF \<open>closed (\<Gamma>', Let \<Delta>'' e', S')\<close> disj])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>d = (\<Delta>'' @ restrictA (- set r) \<Gamma>', e', restr_stack (- set r) S' @ map Dummy (rev r)); atom ` domA \<Delta>'' \<sharp>* restrictA (- set r) \<Gamma>'; \<Gamma>'' = restrictA (- set r) \<Gamma>'; e = Let \<Delta>'' e'; S'' = restr_stack (- set r) S' @ map Dummy (rev r)\<rbrakk> \<Longrightarrow> \<Delta>'' @ restrictA (- set r) \<Gamma>' = restrictA (- set r) (\<Delta>'' @ \<Gamma>')
 2. \<lbrakk>d = (\<Delta>'' @ restrictA (- set r) \<Gamma>', e', restr_stack (- set r) S' @ map Dummy (rev r)); atom ` domA \<Delta>'' \<sharp>* restrictA (- set r) \<Gamma>'; \<Gamma>'' = restrictA (- set r) \<Gamma>'; e = Let \<Delta>'' e'; S'' = restr_stack (- set r) S' @ map Dummy (rev r)\<rbrakk> \<Longrightarrow> restr_stack (- set r) S' = restr_stack (- set r) S'
[PROOF STEP]
apply (auto simp add: restrictA_append)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')

goal (2 subgoals):
 1. \<And>\<Gamma> scrut e1 e2 S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, scrut ? e1 : e2, S); d = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
 2. \<And>\<Gamma> b e1 e2 S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, Bool b, Alts e1 e2 # S); d = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<Gamma> scrut e1 e2 S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, scrut ? e1 : e2, S); d = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
 2. \<And>\<Gamma> b e1 e2 S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, Bool b, Alts e1 e2 # S); d = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
[PROOF STEP]
case if\<^sub>1
[PROOF STATE]
proof (state)
this:
to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>_, scrut_ ? e1_ : e2_, S_)
d = (\<Gamma>_, scrut_, Alts e1_ e2_ # S_)

goal (2 subgoals):
 1. \<And>\<Gamma> scrut e1 e2 S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, scrut ? e1 : e2, S); d = (\<Gamma>, scrut, Alts e1 e2 # S)\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
 2. \<And>\<Gamma> b e1 e2 S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, Bool b, Alts e1 e2 # S); d = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>_, scrut_ ? e1_ : e2_, S_)
d = (\<Gamma>_, scrut_, Alts e1_ e2_ # S_)

goal (1 subgoal):
 1. \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>d = (restrictA (- set r) \<Gamma>', scrut_, Alts e1_ e2_ # restr_stack (- set r) S' @ map Dummy (rev r)); \<Gamma>_ = restrictA (- set r) \<Gamma>'; e = (scrut_ ? e1_ : e2_); S_ = restr_stack (- set r) S' @ map Dummy (rev r)\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' S''. (\<Gamma>', scrut_ ? e1_ : e2_, S') \<Rightarrow> (\<Gamma>'', scrut_, S'') \<and> restrictA (- set r) \<Gamma>' = restrictA (- set r) \<Gamma>'' \<and> Alts e1_ e2_ # restr_stack (- set r) S' = restr_stack (- set r) S''
[PROOF STEP]
apply (intro exI[where x = "0::perm"] exI conjI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>d = (restrictA (- set r) \<Gamma>', scrut_, Alts e1_ e2_ # restr_stack (- set r) S' @ map Dummy (rev r)); \<Gamma>_ = restrictA (- set r) \<Gamma>'; e = (scrut_ ? e1_ : e2_); S_ = restr_stack (- set r) S' @ map Dummy (rev r)\<rbrakk> \<Longrightarrow> (\<Gamma>', scrut_ ? e1_ : e2_, S') \<Rightarrow> (?\<Gamma>''11, scrut_, ?S''12)
 2. \<lbrakk>d = (restrictA (- set r) \<Gamma>', scrut_, Alts e1_ e2_ # restr_stack (- set r) S' @ map Dummy (rev r)); \<Gamma>_ = restrictA (- set r) \<Gamma>'; e = (scrut_ ? e1_ : e2_); S_ = restr_stack (- set r) S' @ map Dummy (rev r)\<rbrakk> \<Longrightarrow> restrictA (- set r) \<Gamma>' = restrictA (- set r) ?\<Gamma>''11
 3. \<lbrakk>d = (restrictA (- set r) \<Gamma>', scrut_, Alts e1_ e2_ # restr_stack (- set r) S' @ map Dummy (rev r)); \<Gamma>_ = restrictA (- set r) \<Gamma>'; e = (scrut_ ? e1_ : e2_); S_ = restr_stack (- set r) S' @ map Dummy (rev r)\<rbrakk> \<Longrightarrow> Alts e1_ e2_ # restr_stack (- set r) S' = restr_stack (- set r) ?S''12
[PROOF STEP]
unfolding permute_zero
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>d = (restrictA (- set r) \<Gamma>', scrut_, Alts e1_ e2_ # restr_stack (- set r) S' @ map Dummy (rev r)); \<Gamma>_ = restrictA (- set r) \<Gamma>'; e = (scrut_ ? e1_ : e2_); S_ = restr_stack (- set r) S' @ map Dummy (rev r)\<rbrakk> \<Longrightarrow> (\<Gamma>', scrut_ ? e1_ : e2_, S') \<Rightarrow> (?\<Gamma>''11, scrut_, ?S''12)
 2. \<lbrakk>d = (restrictA (- set r) \<Gamma>', scrut_, Alts e1_ e2_ # restr_stack (- set r) S' @ map Dummy (rev r)); \<Gamma>_ = restrictA (- set r) \<Gamma>'; e = (scrut_ ? e1_ : e2_); S_ = restr_stack (- set r) S' @ map Dummy (rev r)\<rbrakk> \<Longrightarrow> restrictA (- set r) \<Gamma>' = restrictA (- set r) ?\<Gamma>''11
 3. \<lbrakk>d = (restrictA (- set r) \<Gamma>', scrut_, Alts e1_ e2_ # restr_stack (- set r) S' @ map Dummy (rev r)); \<Gamma>_ = restrictA (- set r) \<Gamma>'; e = (scrut_ ? e1_ : e2_); S_ = restr_stack (- set r) S' @ map Dummy (rev r)\<rbrakk> \<Longrightarrow> Alts e1_ e2_ # restr_stack (- set r) S' = restr_stack (- set r) ?S''12
[PROOF STEP]
apply (rule step.intros)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>d = (restrictA (- set r) \<Gamma>', scrut_, Alts e1_ e2_ # restr_stack (- set r) S' @ map Dummy (rev r)); \<Gamma>_ = restrictA (- set r) \<Gamma>'; e = (scrut_ ? e1_ : e2_); S_ = restr_stack (- set r) S' @ map Dummy (rev r)\<rbrakk> \<Longrightarrow> restrictA (- set r) \<Gamma>' = restrictA (- set r) \<Gamma>'
 2. \<lbrakk>d = (restrictA (- set r) \<Gamma>', scrut_, Alts e1_ e2_ # restr_stack (- set r) S' @ map Dummy (rev r)); \<Gamma>_ = restrictA (- set r) \<Gamma>'; e = (scrut_ ? e1_ : e2_); S_ = restr_stack (- set r) S' @ map Dummy (rev r)\<rbrakk> \<Longrightarrow> Alts e1_ e2_ # restr_stack (- set r) S' = restr_stack (- set r) (Alts e1_ e2_ # S')
[PROOF STEP]
apply (auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')

goal (1 subgoal):
 1. \<And>\<Gamma> b e1 e2 S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, Bool b, Alts e1 e2 # S); d = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<Gamma> b e1 e2 S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, Bool b, Alts e1 e2 # S); d = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
[PROOF STEP]
case if\<^sub>2
[PROOF STATE]
proof (state)
this:
to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>_, Bool b_, Alts e1_ e2_ # S_)
d = (\<Gamma>_, if b_ then e1_ else e2_, S_)

goal (1 subgoal):
 1. \<And>\<Gamma> b e1 e2 S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, Bool b, Alts e1 e2 # S); d = (\<Gamma>, if b then e1 else e2, S)\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>_, Bool b_, Alts e1_ e2_ # S_)
d = (\<Gamma>_, if b_ then e1_ else e2_, S_)

goal (1 subgoal):
 1. \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
[PROOF STEP]
using disj
[PROOF STATE]
proof (prove)
using this:
to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>_, Bool b_, Alts e1_ e2_ # S_)
d = (\<Gamma>_, if b_ then e1_ else e2_, S_)
\<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S')

goal (1 subgoal):
 1. \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
[PROOF STEP]
apply (cases S')
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>_, Bool b_, Alts e1_ e2_ # S_); d = (\<Gamma>_, if b_ then e1_ else e2_, S_); \<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S'); S' = []\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
 2. \<And>a list. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>_, Bool b_, Alts e1_ e2_ # S_); d = (\<Gamma>_, if b_ then e1_ else e2_, S_); \<not> isVal e \<or> safe_hd S' = safe_hd (restr_stack (- set r) S'); S' = a # list\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>list. \<lbrakk>d = (restrictA (- set r) \<Gamma>', e1_, restr_stack (- set r) list @ map Dummy (rev r)); S' = Alts e1_ e2_ # list; \<Gamma>_ = restrictA (- set r) \<Gamma>'; e = Bool True; S_ = restr_stack (- set r) list @ map Dummy (rev r); b_\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' S''. (\<Gamma>', Bool True, Alts e1_ e2_ # list) \<Rightarrow> (\<Gamma>'', e1_, S'') \<and> restrictA (- set r) \<Gamma>' = restrictA (- set r) \<Gamma>'' \<and> restr_stack (- set r) list = restr_stack (- set r) S''
 2. \<And>list. \<lbrakk>d = (restrictA (- set r) \<Gamma>', e2_, restr_stack (- set r) list @ map Dummy (rev r)); S' = Alts e1_ e2_ # list; \<Gamma>_ = restrictA (- set r) \<Gamma>'; e = Bool False; S_ = restr_stack (- set r) list @ map Dummy (rev r); \<not> b_\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' S''. (\<Gamma>', Bool False, Alts e1_ e2_ # list) \<Rightarrow> (\<Gamma>'', e2_, S'') \<and> restrictA (- set r) \<Gamma>' = restrictA (- set r) \<Gamma>'' \<and> restr_stack (- set r) list = restr_stack (- set r) S''
[PROOF STEP]
apply (intro exI exI conjI)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>list. \<lbrakk>d = (restrictA (- set r) \<Gamma>', e1_, restr_stack (- set r) list @ map Dummy (rev r)); S' = Alts e1_ e2_ # list; \<Gamma>_ = restrictA (- set r) \<Gamma>'; e = Bool True; S_ = restr_stack (- set r) list @ map Dummy (rev r); b_\<rbrakk> \<Longrightarrow> (\<Gamma>', Bool True, Alts e1_ e2_ # list) \<Rightarrow> (?\<Gamma>''34 list, e1_, ?S''35 list)
 2. \<And>list. \<lbrakk>d = (restrictA (- set r) \<Gamma>', e1_, restr_stack (- set r) list @ map Dummy (rev r)); S' = Alts e1_ e2_ # list; \<Gamma>_ = restrictA (- set r) \<Gamma>'; e = Bool True; S_ = restr_stack (- set r) list @ map Dummy (rev r); b_\<rbrakk> \<Longrightarrow> restrictA (- set r) \<Gamma>' = restrictA (- set r) (?\<Gamma>''34 list)
 3. \<And>list. \<lbrakk>d = (restrictA (- set r) \<Gamma>', e1_, restr_stack (- set r) list @ map Dummy (rev r)); S' = Alts e1_ e2_ # list; \<Gamma>_ = restrictA (- set r) \<Gamma>'; e = Bool True; S_ = restr_stack (- set r) list @ map Dummy (rev r); b_\<rbrakk> \<Longrightarrow> restr_stack (- set r) list = restr_stack (- set r) (?S''35 list)
 4. \<And>list. \<lbrakk>d = (restrictA (- set r) \<Gamma>', e2_, restr_stack (- set r) list @ map Dummy (rev r)); S' = Alts e1_ e2_ # list; \<Gamma>_ = restrictA (- set r) \<Gamma>'; e = Bool False; S_ = restr_stack (- set r) list @ map Dummy (rev r); \<not> b_\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' S''. (\<Gamma>', Bool False, Alts e1_ e2_ # list) \<Rightarrow> (\<Gamma>'', e2_, S'') \<and> restrictA (- set r) \<Gamma>' = restrictA (- set r) \<Gamma>'' \<and> restr_stack (- set r) list = restr_stack (- set r) S''
[PROOF STEP]
apply (rule step.if\<^sub>2[where b = True, simplified] step.if\<^sub>2[where b = False, simplified])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>list. \<lbrakk>d = (restrictA (- set r) \<Gamma>', e1_, restr_stack (- set r) list @ map Dummy (rev r)); S' = Alts e1_ e2_ # list; \<Gamma>_ = restrictA (- set r) \<Gamma>'; e = Bool True; S_ = restr_stack (- set r) list @ map Dummy (rev r); b_\<rbrakk> \<Longrightarrow> restrictA (- set r) \<Gamma>' = restrictA (- set r) \<Gamma>'
 2. \<And>list. \<lbrakk>d = (restrictA (- set r) \<Gamma>', e1_, restr_stack (- set r) list @ map Dummy (rev r)); S' = Alts e1_ e2_ # list; \<Gamma>_ = restrictA (- set r) \<Gamma>'; e = Bool True; S_ = restr_stack (- set r) list @ map Dummy (rev r); b_\<rbrakk> \<Longrightarrow> restr_stack (- set r) list = restr_stack (- set r) list
 3. \<And>list. \<lbrakk>d = (restrictA (- set r) \<Gamma>', e2_, restr_stack (- set r) list @ map Dummy (rev r)); S' = Alts e1_ e2_ # list; \<Gamma>_ = restrictA (- set r) \<Gamma>'; e = Bool False; S_ = restr_stack (- set r) list @ map Dummy (rev r); \<not> b_\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' S''. (\<Gamma>', Bool False, Alts e1_ e2_ # list) \<Rightarrow> (\<Gamma>'', e2_, S'') \<and> restrictA (- set r) \<Gamma>' = restrictA (- set r) \<Gamma>'' \<and> restr_stack (- set r) list = restr_stack (- set r) S''
[PROOF STEP]
apply (auto split: if_splits dest: Upd_eq_restr_stackD2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>list. \<lbrakk>d = (restrictA (- set r) \<Gamma>', e2_, restr_stack (- set r) list @ map Dummy (rev r)); S' = Alts e1_ e2_ # list; \<Gamma>_ = restrictA (- set r) \<Gamma>'; e = Bool False; S_ = restr_stack (- set r) list @ map Dummy (rev r); \<not> b_\<rbrakk> \<Longrightarrow> \<exists>\<Gamma>'' S''. (\<Gamma>', Bool False, Alts e1_ e2_ # list) \<Rightarrow> (\<Gamma>'', e2_, S'') \<and> restrictA (- set r) \<Gamma>' = restrictA (- set r) \<Gamma>'' \<and> restr_stack (- set r) list = restr_stack (- set r) S''
[PROOF STEP]
apply (intro exI conjI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>list. \<lbrakk>d = (restrictA (- set r) \<Gamma>', e2_, restr_stack (- set r) list @ map Dummy (rev r)); S' = Alts e1_ e2_ # list; \<Gamma>_ = restrictA (- set r) \<Gamma>'; e = Bool False; S_ = restr_stack (- set r) list @ map Dummy (rev r); \<not> b_\<rbrakk> \<Longrightarrow> (\<Gamma>', Bool False, Alts e1_ e2_ # list) \<Rightarrow> (?\<Gamma>''39 list, e2_, ?S''40 list)
 2. \<And>list. \<lbrakk>d = (restrictA (- set r) \<Gamma>', e2_, restr_stack (- set r) list @ map Dummy (rev r)); S' = Alts e1_ e2_ # list; \<Gamma>_ = restrictA (- set r) \<Gamma>'; e = Bool False; S_ = restr_stack (- set r) list @ map Dummy (rev r); \<not> b_\<rbrakk> \<Longrightarrow> restrictA (- set r) \<Gamma>' = restrictA (- set r) (?\<Gamma>''39 list)
 3. \<And>list. \<lbrakk>d = (restrictA (- set r) \<Gamma>', e2_, restr_stack (- set r) list @ map Dummy (rev r)); S' = Alts e1_ e2_ # list; \<Gamma>_ = restrictA (- set r) \<Gamma>'; e = Bool False; S_ = restr_stack (- set r) list @ map Dummy (rev r); \<not> b_\<rbrakk> \<Longrightarrow> restr_stack (- set r) list = restr_stack (- set r) (?S''40 list)
[PROOF STEP]
apply (rule step.if\<^sub>2[where b = True, simplified] step.if\<^sub>2[where b = False, simplified])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>list. \<lbrakk>d = (restrictA (- set r) \<Gamma>', e2_, restr_stack (- set r) list @ map Dummy (rev r)); S' = Alts e1_ e2_ # list; \<Gamma>_ = restrictA (- set r) \<Gamma>'; e = Bool False; S_ = restr_stack (- set r) list @ map Dummy (rev r); \<not> b_\<rbrakk> \<Longrightarrow> restrictA (- set r) \<Gamma>' = restrictA (- set r) \<Gamma>'
 2. \<And>list. \<lbrakk>d = (restrictA (- set r) \<Gamma>', e2_, restr_stack (- set r) list @ map Dummy (rev r)); S' = Alts e1_ e2_ # list; \<Gamma>_ = restrictA (- set r) \<Gamma>'; e = Bool False; S_ = restr_stack (- set r) list @ map Dummy (rev r); \<not> b_\<rbrakk> \<Longrightarrow> restr_stack (- set r) list = restr_stack (- set r) list
[PROOF STEP]
apply (auto split: if_splits dest: Upd_eq_restr_stackD2)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')

goal (2 subgoals):
 1. to_gc_conf r (\<Gamma>', e, S') \<Rightarrow> d \<Longrightarrow> \<exists>r' \<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow>\<^sup>* (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r' (\<Gamma>'', e'', S'') \<and> r_ok r' (\<Gamma>'', e'', S'')
 2. \<And>\<Gamma> ea x S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, ea, Upd x # S); d = (\<Gamma>, ea, S @ [Dummy x])\<rbrakk> \<Longrightarrow> \<exists>r' \<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow>\<^sup>* (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r' (\<Gamma>'', e'', S'') \<and> r_ok r' (\<Gamma>'', e'', S'')
[PROOF STEP]
with invariantE[OF subset_bound_invariant _ \<open>r_ok r (\<Gamma>', e, S')\<close>]
[PROOF STATE]
proof (chain)
picking this:
(\<Gamma>', e, S') \<Rightarrow> ?y \<Longrightarrow> r_ok r ?y
\<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Gamma>', e, S') \<Rightarrow> ?y \<Longrightarrow> r_ok r ?y
\<exists>\<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow> (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r (\<Gamma>'', e'', S'')

goal (1 subgoal):
 1. \<exists>r' \<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow>\<^sup>* (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r' (\<Gamma>'', e'', S'') \<and> r_ok r' (\<Gamma>'', e'', S'')
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>r' \<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow>\<^sup>* (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r' (\<Gamma>'', e'', S'') \<and> r_ok r' (\<Gamma>'', e'', S'')

goal (1 subgoal):
 1. \<And>\<Gamma> ea x S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, ea, Upd x # S); d = (\<Gamma>, ea, S @ [Dummy x])\<rbrakk> \<Longrightarrow> \<exists>r' \<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow>\<^sup>* (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r' (\<Gamma>'', e'', S'') \<and> r_ok r' (\<Gamma>'', e'', S'')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<Gamma> ea x S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, ea, Upd x # S); d = (\<Gamma>, ea, S @ [Dummy x])\<rbrakk> \<Longrightarrow> \<exists>r' \<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow>\<^sup>* (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r' (\<Gamma>'', e'', S'') \<and> r_ok r' (\<Gamma>'', e'', S'')
[PROOF STEP]
case (dropUpd \<Gamma>'' e'' x S'')
[PROOF STATE]
proof (state)
this:
to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>'', e'', Upd x # S'')
d = (\<Gamma>'', e'', S'' @ [Dummy x])

goal (1 subgoal):
 1. \<And>\<Gamma> ea x S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, ea, Upd x # S); d = (\<Gamma>, ea, S @ [Dummy x])\<rbrakk> \<Longrightarrow> \<exists>r' \<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow>\<^sup>* (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r' (\<Gamma>'', e'', S'') \<and> r_ok r' (\<Gamma>'', e'', S'')
[PROOF STEP]
from \<open>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>'', e'', Upd x # S'')\<close>
[PROOF STATE]
proof (chain)
picking this:
to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>'', e'', Upd x # S'')
[PROOF STEP]
have "x \<notin> set r"
[PROOF STATE]
proof (prove)
using this:
to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>'', e'', Upd x # S'')

goal (1 subgoal):
 1. x \<notin> set r
[PROOF STEP]
by (auto dest!: arg_cong[where f = upds])
[PROOF STATE]
proof (state)
this:
x \<notin> set r

goal (1 subgoal):
 1. \<And>\<Gamma> ea x S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, ea, Upd x # S); d = (\<Gamma>, ea, S @ [Dummy x])\<rbrakk> \<Longrightarrow> \<exists>r' \<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow>\<^sup>* (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r' (\<Gamma>'', e'', S'') \<and> r_ok r' (\<Gamma>'', e'', S'')
[PROOF STEP]
from \<open>heap_upds_ok (\<Gamma>', S')\<close> and \<open>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>'', e'', Upd x # S'')\<close>
[PROOF STATE]
proof (chain)
picking this:
heap_upds_ok (\<Gamma>', S')
to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>'', e'', Upd x # S'')
[PROOF STEP]
have "heap_upds_ok (\<Gamma>'', Upd x # S'')"
[PROOF STATE]
proof (prove)
using this:
heap_upds_ok (\<Gamma>', S')
to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>'', e'', Upd x # S'')

goal (1 subgoal):
 1. heap_upds_ok (\<Gamma>'', Upd x # S'')
[PROOF STEP]
by (rule heap_upd_ok_to_gc_conf)
[PROOF STATE]
proof (state)
this:
heap_upds_ok (\<Gamma>'', Upd x # S'')

goal (1 subgoal):
 1. \<And>\<Gamma> ea x S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, ea, Upd x # S); d = (\<Gamma>, ea, S @ [Dummy x])\<rbrakk> \<Longrightarrow> \<exists>r' \<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow>\<^sup>* (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r' (\<Gamma>'', e'', S'') \<and> r_ok r' (\<Gamma>'', e'', S'')
[PROOF STEP]
hence [simp]: "x \<notin> domA \<Gamma>''" "x \<notin> upds S''"
[PROOF STATE]
proof (prove)
using this:
heap_upds_ok (\<Gamma>'', Upd x # S'')

goal (1 subgoal):
 1. x \<notin> domA \<Gamma>'' &&& x \<notin> upds S''
[PROOF STEP]
by (auto dest: heap_upds_ok_upd)
[PROOF STATE]
proof (state)
this:
x \<notin> domA \<Gamma>''
x \<notin> upds S''

goal (1 subgoal):
 1. \<And>\<Gamma> ea x S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, ea, Upd x # S); d = (\<Gamma>, ea, S @ [Dummy x])\<rbrakk> \<Longrightarrow> \<exists>r' \<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow>\<^sup>* (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r' (\<Gamma>'', e'', S'') \<and> r_ok r' (\<Gamma>'', e'', S'')
[PROOF STEP]
have "to_gc_conf (x # r) (\<Gamma>', e, S') = to_gc_conf ([x]@ r) (\<Gamma>', e, S')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_gc_conf (x # r) (\<Gamma>', e, S') = to_gc_conf ([x] @ r) (\<Gamma>', e, S')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
to_gc_conf (x # r) (\<Gamma>', e, S') = to_gc_conf ([x] @ r) (\<Gamma>', e, S')

goal (1 subgoal):
 1. \<And>\<Gamma> ea x S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, ea, Upd x # S); d = (\<Gamma>, ea, S @ [Dummy x])\<rbrakk> \<Longrightarrow> \<exists>r' \<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow>\<^sup>* (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r' (\<Gamma>'', e'', S'') \<and> r_ok r' (\<Gamma>'', e'', S'')
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
to_gc_conf (x # r) (\<Gamma>', e, S') = to_gc_conf ([x] @ r) (\<Gamma>', e, S')

goal (1 subgoal):
 1. \<And>\<Gamma> ea x S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, ea, Upd x # S); d = (\<Gamma>, ea, S @ [Dummy x])\<rbrakk> \<Longrightarrow> \<exists>r' \<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow>\<^sup>* (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r' (\<Gamma>'', e'', S'') \<and> r_ok r' (\<Gamma>'', e'', S'')
[PROOF STEP]
have "\<dots> = to_gc_conf [x] (to_gc_conf r (\<Gamma>', e, S'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_gc_conf ([x] @ r) (\<Gamma>', e, S') = to_gc_conf [x] (to_gc_conf r (\<Gamma>', e, S'))
[PROOF STEP]
by (rule to_gc_conf_append)
[PROOF STATE]
proof (state)
this:
to_gc_conf ([x] @ r) (\<Gamma>', e, S') = to_gc_conf [x] (to_gc_conf r (\<Gamma>', e, S'))

goal (1 subgoal):
 1. \<And>\<Gamma> ea x S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, ea, Upd x # S); d = (\<Gamma>, ea, S @ [Dummy x])\<rbrakk> \<Longrightarrow> \<exists>r' \<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow>\<^sup>* (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r' (\<Gamma>'', e'', S'') \<and> r_ok r' (\<Gamma>'', e'', S'')
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
to_gc_conf ([x] @ r) (\<Gamma>', e, S') = to_gc_conf [x] (to_gc_conf r (\<Gamma>', e, S'))

goal (1 subgoal):
 1. \<And>\<Gamma> ea x S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, ea, Upd x # S); d = (\<Gamma>, ea, S @ [Dummy x])\<rbrakk> \<Longrightarrow> \<exists>r' \<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow>\<^sup>* (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r' (\<Gamma>'', e'', S'') \<and> r_ok r' (\<Gamma>'', e'', S'')
[PROOF STEP]
have "\<dots> = to_gc_conf [x] (\<Gamma>'', e'', Upd x # S'')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_gc_conf [x] (to_gc_conf r (\<Gamma>', e, S')) = to_gc_conf [x] (\<Gamma>'', e'', Upd x # S'')
[PROOF STEP]
unfolding \<open>to_gc_conf r (\<Gamma>', e, S') = _\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_gc_conf [x] (\<Gamma>'', e'', Upd x # S'') = to_gc_conf [x] (\<Gamma>'', e'', Upd x # S'')
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
to_gc_conf [x] (to_gc_conf r (\<Gamma>', e, S')) = to_gc_conf [x] (\<Gamma>'', e'', Upd x # S'')

goal (1 subgoal):
 1. \<And>\<Gamma> ea x S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, ea, Upd x # S); d = (\<Gamma>, ea, S @ [Dummy x])\<rbrakk> \<Longrightarrow> \<exists>r' \<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow>\<^sup>* (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r' (\<Gamma>'', e'', S'') \<and> r_ok r' (\<Gamma>'', e'', S'')
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
to_gc_conf [x] (to_gc_conf r (\<Gamma>', e, S')) = to_gc_conf [x] (\<Gamma>'', e'', Upd x # S'')

goal (1 subgoal):
 1. \<And>\<Gamma> ea x S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, ea, Upd x # S); d = (\<Gamma>, ea, S @ [Dummy x])\<rbrakk> \<Longrightarrow> \<exists>r' \<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow>\<^sup>* (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r' (\<Gamma>'', e'', S'') \<and> r_ok r' (\<Gamma>'', e'', S'')
[PROOF STEP]
have "\<dots> = (\<Gamma>'', e'', S''@[Dummy x])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_gc_conf [x] (\<Gamma>'', e'', Upd x # S'') = (\<Gamma>'', e'', S'' @ [Dummy x])
[PROOF STEP]
by (auto intro: restrictA_noop)
[PROOF STATE]
proof (state)
this:
to_gc_conf [x] (\<Gamma>'', e'', Upd x # S'') = (\<Gamma>'', e'', S'' @ [Dummy x])

goal (1 subgoal):
 1. \<And>\<Gamma> ea x S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, ea, Upd x # S); d = (\<Gamma>, ea, S @ [Dummy x])\<rbrakk> \<Longrightarrow> \<exists>r' \<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow>\<^sup>* (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r' (\<Gamma>'', e'', S'') \<and> r_ok r' (\<Gamma>'', e'', S'')
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
to_gc_conf [x] (\<Gamma>'', e'', Upd x # S'') = (\<Gamma>'', e'', S'' @ [Dummy x])

goal (1 subgoal):
 1. \<And>\<Gamma> ea x S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, ea, Upd x # S); d = (\<Gamma>, ea, S @ [Dummy x])\<rbrakk> \<Longrightarrow> \<exists>r' \<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow>\<^sup>* (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r' (\<Gamma>'', e'', S'') \<and> r_ok r' (\<Gamma>'', e'', S'')
[PROOF STEP]
have "\<dots> = d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Gamma>'', e'', S'' @ [Dummy x]) = d
[PROOF STEP]
using \<open> d= _\<close>
[PROOF STATE]
proof (prove)
using this:
d = (\<Gamma>'', e'', S'' @ [Dummy x])

goal (1 subgoal):
 1. (\<Gamma>'', e'', S'' @ [Dummy x]) = d
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Gamma>'', e'', S'' @ [Dummy x]) = d

goal (1 subgoal):
 1. \<And>\<Gamma> ea x S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, ea, Upd x # S); d = (\<Gamma>, ea, S @ [Dummy x])\<rbrakk> \<Longrightarrow> \<exists>r' \<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow>\<^sup>* (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r' (\<Gamma>'', e'', S'') \<and> r_ok r' (\<Gamma>'', e'', S'')
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
to_gc_conf (x # r) (\<Gamma>', e, S') = d
[PROOF STEP]
have "to_gc_conf (x # r) (\<Gamma>', e, S') = d"
[PROOF STATE]
proof (prove)
using this:
to_gc_conf (x # r) (\<Gamma>', e, S') = d

goal (1 subgoal):
 1. to_gc_conf (x # r) (\<Gamma>', e, S') = d
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
to_gc_conf (x # r) (\<Gamma>', e, S') = d

goal (1 subgoal):
 1. \<And>\<Gamma> ea x S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, ea, Upd x # S); d = (\<Gamma>, ea, S @ [Dummy x])\<rbrakk> \<Longrightarrow> \<exists>r' \<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow>\<^sup>* (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r' (\<Gamma>'', e'', S'') \<and> r_ok r' (\<Gamma>'', e'', S'')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
to_gc_conf (x # r) (\<Gamma>', e, S') = d

goal (1 subgoal):
 1. \<And>\<Gamma> ea x S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, ea, Upd x # S); d = (\<Gamma>, ea, S @ [Dummy x])\<rbrakk> \<Longrightarrow> \<exists>r' \<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow>\<^sup>* (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r' (\<Gamma>'', e'', S'') \<and> r_ok r' (\<Gamma>'', e'', S'')
[PROOF STEP]
from \<open>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>'', e'', Upd x # S'')\<close>
[PROOF STATE]
proof (chain)
picking this:
to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>'', e'', Upd x # S'')
[PROOF STEP]
have "x \<in> upds S'"
[PROOF STATE]
proof (prove)
using this:
to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>'', e'', Upd x # S'')

goal (1 subgoal):
 1. x \<in> upds S'
[PROOF STEP]
by (auto dest!: arg_cong[where f = upds])
[PROOF STATE]
proof (state)
this:
x \<in> upds S'

goal (1 subgoal):
 1. \<And>\<Gamma> ea x S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, ea, Upd x # S); d = (\<Gamma>, ea, S @ [Dummy x])\<rbrakk> \<Longrightarrow> \<exists>r' \<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow>\<^sup>* (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r' (\<Gamma>'', e'', S'') \<and> r_ok r' (\<Gamma>'', e'', S'')
[PROOF STEP]
with \<open>r_ok r (\<Gamma>', e, S')\<close>
[PROOF STATE]
proof (chain)
picking this:
r_ok r (\<Gamma>', e, S')
x \<in> upds S'
[PROOF STEP]
have "r_ok (x # r) (\<Gamma>', e, S')"
[PROOF STATE]
proof (prove)
using this:
r_ok r (\<Gamma>', e, S')
x \<in> upds S'

goal (1 subgoal):
 1. r_ok (x # r) (\<Gamma>', e, S')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r_ok (x # r) (\<Gamma>', e, S')

goal (1 subgoal):
 1. \<And>\<Gamma> ea x S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, ea, Upd x # S); d = (\<Gamma>, ea, S @ [Dummy x])\<rbrakk> \<Longrightarrow> \<exists>r' \<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow>\<^sup>* (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r' (\<Gamma>'', e'', S'') \<and> r_ok r' (\<Gamma>'', e'', S'')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
r_ok (x # r) (\<Gamma>', e, S')

goal (1 subgoal):
 1. \<And>\<Gamma> ea x S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, ea, Upd x # S); d = (\<Gamma>, ea, S @ [Dummy x])\<rbrakk> \<Longrightarrow> \<exists>r' \<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow>\<^sup>* (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r' (\<Gamma>'', e'', S'') \<and> r_ok r' (\<Gamma>'', e'', S'')
[PROOF STEP]
note \<open>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>'', e'', Upd x # S'')\<close>
[PROOF STATE]
proof (state)
this:
to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>'', e'', Upd x # S'')

goal (1 subgoal):
 1. \<And>\<Gamma> ea x S. \<lbrakk>to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>, ea, Upd x # S); d = (\<Gamma>, ea, S @ [Dummy x])\<rbrakk> \<Longrightarrow> \<exists>r' \<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow>\<^sup>* (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r' (\<Gamma>'', e'', S'') \<and> r_ok r' (\<Gamma>'', e'', S'')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
to_gc_conf (x # r) (\<Gamma>', e, S') = d
r_ok (x # r) (\<Gamma>', e, S')
to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>'', e'', Upd x # S'')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
to_gc_conf (x # r) (\<Gamma>', e, S') = d
r_ok (x # r) (\<Gamma>', e, S')
to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>'', e'', Upd x # S'')

goal (1 subgoal):
 1. \<exists>r' \<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow>\<^sup>* (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r' (\<Gamma>'', e'', S'') \<and> r_ok r' (\<Gamma>'', e'', S'')
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>r' \<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow>\<^sup>* (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r' (\<Gamma>'', e'', S'') \<and> r_ok r' (\<Gamma>'', e'', S'')

goal:
No subgoals!
[PROOF STEP]
(*
  next
    case (drop x \<Gamma>'' e'' S'')
    from `to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>'', e'', S'')` and `x \<in> domA \<Gamma>''`
    have "x \<notin> set r" by auto

    from `heap_upds_ok (\<Gamma>', S')` and  `to_gc_conf r (\<Gamma>', e, S') = (\<Gamma>'', e'', S'')`
    have "heap_upds_ok (\<Gamma>'', S'')" by (rule heap_upd_ok_to_gc_conf)
    with `x \<in> domA \<Gamma>''`
    have [simp]: "x \<notin> upds S''" by (metis heap_upds_okE)

    have "to_gc_conf (x # r) (\<Gamma>', e, S') = to_gc_conf ([x]@ r) (\<Gamma>', e, S')" by simp
    also have "\<dots> = to_gc_conf [x] (to_gc_conf r (\<Gamma>', e, S'))" by (rule to_gc_conf_append)
    also have "\<dots> = to_gc_conf [x] (\<Gamma>'', e'', S'')" unfolding `to_gc_conf r (\<Gamma>', e, S') = _`..
    also have "\<dots> = (delete x \<Gamma>'', e'', S''@[Dummy x])" by (auto  simp add: delete_restrictA_conv)
    also have "\<dots> = d" using ` d= _` by simp
    finally have "to_gc_conf (x # r) (\<Gamma>', e, S') = d".
    moreover
    from `to_gc_conf r (\<Gamma>', e, S') = _` `x \<in> domA \<Gamma>''`
    have "x \<in> domA \<Gamma>'" by auto
    with `r_ok r (\<Gamma>', e, S')`
    have "r_ok (x # r) (\<Gamma>', e, S')" by auto
    moreover
    note `to_gc_conf r (\<Gamma>', e, S') = _`
    ultimately
    show ?thesis by fastforce
*)
[PROOF STATE]
proof (state)
this:
\<exists>r' \<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow>\<^sup>* (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r' (\<Gamma>'', e'', S'') \<and> r_ok r' (\<Gamma>'', e'', S'')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>r' \<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow>\<^sup>* (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r' (\<Gamma>'', e'', S'') \<and> r_ok r' (\<Gamma>'', e'', S'')

goal (1 subgoal):
 1. \<exists>r' c'. c \<Rightarrow>\<^sup>* c' \<and> d = to_gc_conf r' c' \<and> r_ok r' c'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>r' \<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow>\<^sup>* (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r' (\<Gamma>'', e'', S'') \<and> r_ok r' (\<Gamma>'', e'', S'')
[PROOF STEP]
obtain r' \<Gamma>'' e'' S''
    where "(\<Gamma>', e, S') \<Rightarrow>\<^sup>* (\<Gamma>'', e'', S'')"
    and "d = to_gc_conf r' (\<Gamma>'', e'', S'')"
    and "r_ok r' (\<Gamma>'', e'', S'')"
[PROOF STATE]
proof (prove)
using this:
\<exists>r' \<Gamma>'' e'' S''. (\<Gamma>', e, S') \<Rightarrow>\<^sup>* (\<Gamma>'', e'', S'') \<and> d = to_gc_conf r' (\<Gamma>'', e'', S'') \<and> r_ok r' (\<Gamma>'', e'', S'')

goal (1 subgoal):
 1. (\<And>\<Gamma>'' e'' S'' r'. \<lbrakk>(\<Gamma>', e, S') \<Rightarrow>\<^sup>* (\<Gamma>'', e'', S''); d = to_gc_conf r' (\<Gamma>'', e'', S''); r_ok r' (\<Gamma>'', e'', S'')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(\<Gamma>', e, S') \<Rightarrow>\<^sup>* (\<Gamma>'', e'', S'')
d = to_gc_conf r' (\<Gamma>'', e'', S'')
r_ok r' (\<Gamma>'', e'', S'')

goal (1 subgoal):
 1. \<exists>r' c'. c \<Rightarrow>\<^sup>* c' \<and> d = to_gc_conf r' c' \<and> r_ok r' c'
[PROOF STEP]
from  \<open>(\<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Gamma>', e, S')\<close> and \<open>(\<Gamma>', e, S') \<Rightarrow>\<^sup>* (\<Gamma>'', e'', S'')\<close>
[PROOF STATE]
proof (chain)
picking this:
(\<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Gamma>', e, S')
(\<Gamma>', e, S') \<Rightarrow>\<^sup>* (\<Gamma>'', e'', S'')
[PROOF STEP]
have "(\<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Gamma>'', e'', S'')"
[PROOF STATE]
proof (prove)
using this:
(\<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Gamma>', e, S')
(\<Gamma>', e, S') \<Rightarrow>\<^sup>* (\<Gamma>'', e'', S'')

goal (1 subgoal):
 1. (\<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Gamma>'', e'', S'')
[PROOF STEP]
by (rule rtranclp_trans)
[PROOF STATE]
proof (state)
this:
(\<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Gamma>'', e'', S'')

goal (1 subgoal):
 1. \<exists>r' c'. c \<Rightarrow>\<^sup>* c' \<and> d = to_gc_conf r' c' \<and> r_ok r' c'
[PROOF STEP]
with \<open>d = _\<close> \<open>r_ok r' _\<close>
[PROOF STATE]
proof (chain)
picking this:
d = to_gc_conf r' (\<Gamma>'', e'', S'')
r_ok r' (\<Gamma>'', e'', S'')
(\<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Gamma>'', e'', S'')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
d = to_gc_conf r' (\<Gamma>'', e'', S'')
r_ok r' (\<Gamma>'', e'', S'')
(\<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Gamma>'', e'', S'')

goal (1 subgoal):
 1. \<exists>r' c'. c \<Rightarrow>\<^sup>* c' \<and> d = to_gc_conf r' c' \<and> r_ok r' c'
[PROOF STEP]
unfolding \<open>c = _\<close>
[PROOF STATE]
proof (prove)
using this:
d = to_gc_conf r' (\<Gamma>'', e'', S'')
r_ok r' (\<Gamma>'', e'', S'')
(\<Gamma>, e, S) \<Rightarrow>\<^sup>* (\<Gamma>'', e'', S'')

goal (1 subgoal):
 1. \<exists>r' c'. (\<Gamma>, e, S) \<Rightarrow>\<^sup>* c' \<and> d = to_gc_conf r' c' \<and> r_ok r' c'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>r' c'. c \<Rightarrow>\<^sup>* c' \<and> d = to_gc_conf r' c' \<and> r_ok r' c'

goal:
No subgoals!
[PROOF STEP]
qed