[STATEMENT]
theorem assumes wf:"wwf_prog P"
shows red_preserves_lconf:
  "P,E \<turnstile> \<langle>e,(h,l)\<rangle> \<rightarrow> \<langle>e',(h',l')\<rangle> \<Longrightarrow>
  (\<And>T. \<lbrakk> P,E,h \<turnstile> e:T; P,h \<turnstile> l (:\<le>)\<^sub>w E; P \<turnstile> E \<surd> \<rbrakk> \<Longrightarrow> P,h' \<turnstile> l' (:\<le>)\<^sub>w E)"
and reds_preserves_lconf:
  "P,E \<turnstile> \<langle>es,(h,l)\<rangle> [\<rightarrow>] \<langle>es',(h',l')\<rangle> \<Longrightarrow>
  (\<And>Ts. \<lbrakk> P,E,h \<turnstile> es[:]Ts; P,h \<turnstile> l (:\<le>)\<^sub>w E; P \<turnstile> E \<surd> \<rbrakk> \<Longrightarrow> P,h' \<turnstile> l' (:\<le>)\<^sub>w E)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P,E \<turnstile> \<langle>e,(h, l)\<rangle> \<rightarrow> \<langle>e',(h', l')\<rangle> \<Longrightarrow> (\<And>T. \<lbrakk>P,E,h \<turnstile> e : T; P,h \<turnstile> l (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,h' \<turnstile> l' (:\<le>)\<^sub>w E)) &&& (P,E \<turnstile> \<langle>es,(h, l)\<rangle> [\<rightarrow>] \<langle>es',(h', l')\<rangle> \<Longrightarrow> (\<And>Ts. \<lbrakk>P,E,h \<turnstile> es [:] Ts; P,h \<turnstile> l (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,h' \<turnstile> l' (:\<le>)\<^sub>w E))
[PROOF STEP]
proof(induct rule:red_reds_inducts)
[PROOF STATE]
proof (state)
goal (61 subgoals):
 1. \<And>h a h' C E l T. \<lbrakk>new_Addr h = \<lfloor>a\<rfloor>; h' = h(a \<mapsto> (C, Collect (init_obj P C))); P,E,h \<turnstile> new C : T; P,h \<turnstile> l (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,h' \<turnstile> l (:\<le>)\<^sub>w E
 2. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P,h \<turnstile> l (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,h \<turnstile> l (:\<le>)\<^sub>w E
 3. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 4. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 5. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 6. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 7. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 8. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> Cast C e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 9. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 10. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
A total of 61 subgoals...
[PROOF STEP]
case RedNew
[PROOF STATE]
proof (state)
this:
new_Addr h_ = \<lfloor>a_\<rfloor>
h'_ = h_(a_ \<mapsto> (C_, Collect (init_obj P C_)))
P,E_,h_ \<turnstile> new C_ : T
P,h_ \<turnstile> l_ (:\<le>)\<^sub>w E_
P \<turnstile> E_ \<surd>

goal (61 subgoals):
 1. \<And>h a h' C E l T. \<lbrakk>new_Addr h = \<lfloor>a\<rfloor>; h' = h(a \<mapsto> (C, Collect (init_obj P C))); P,E,h \<turnstile> new C : T; P,h \<turnstile> l (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,h' \<turnstile> l (:\<le>)\<^sub>w E
 2. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P,h \<turnstile> l (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,h \<turnstile> l (:\<le>)\<^sub>w E
 3. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 4. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 5. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 6. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 7. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 8. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> Cast C e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 9. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 10. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
A total of 61 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
new_Addr h_ = \<lfloor>a_\<rfloor>
h'_ = h_(a_ \<mapsto> (C_, Collect (init_obj P C_)))
P,E_,h_ \<turnstile> new C_ : T
P,h_ \<turnstile> l_ (:\<le>)\<^sub>w E_
P \<turnstile> E_ \<surd>

goal (1 subgoal):
 1. P,h'_ \<turnstile> l_ (:\<le>)\<^sub>w E_
[PROOF STEP]
by(fast intro:lconf_hext red_hext_incr[OF red_reds.RedNew])
[PROOF STATE]
proof (state)
this:
P,h'_ \<turnstile> l_ (:\<le>)\<^sub>w E_

goal (60 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P,h \<turnstile> l (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,h \<turnstile> l (:\<le>)\<^sub>w E
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> Cast C e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
A total of 60 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (60 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P,h \<turnstile> l (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,h \<turnstile> l (:\<le>)\<^sub>w E
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> Cast C e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
A total of 60 subgoals...
[PROOF STEP]
case (RedLAss E V T v v' h l T')
[PROOF STATE]
proof (state)
this:
E V = \<lfloor>T\<rfloor>
P \<turnstile> T casts v to v'
P,E,h \<turnstile> V:=Val v : T'
P,h \<turnstile> l (:\<le>)\<^sub>w E
P \<turnstile> E \<surd>

goal (60 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P,h \<turnstile> l (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,h \<turnstile> l (:\<le>)\<^sub>w E
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> Cast C e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
A total of 60 subgoals...
[PROOF STEP]
have casts:"P \<turnstile> T casts v to v'" and env:"E V = Some T"
    and wt:"P,E,h \<turnstile> V:=Val v : T'" and lconf:"P,h \<turnstile> l (:\<le>)\<^sub>w E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P \<turnstile> T casts v to v'  &&& E V = \<lfloor>T\<rfloor>) &&& P,E,h \<turnstile> V:=Val v : T' &&& P,h \<turnstile> l (:\<le>)\<^sub>w E
[PROOF STEP]
by fact+
[PROOF STATE]
proof (state)
this:
P \<turnstile> T casts v to v'
E V = \<lfloor>T\<rfloor>
P,E,h \<turnstile> V:=Val v : T'
P,h \<turnstile> l (:\<le>)\<^sub>w E

goal (60 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P,h \<turnstile> l (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,h \<turnstile> l (:\<le>)\<^sub>w E
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> Cast C e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
A total of 60 subgoals...
[PROOF STEP]
from wt env
[PROOF STATE]
proof (chain)
picking this:
P,E,h \<turnstile> V:=Val v : T'
E V = \<lfloor>T\<rfloor>
[PROOF STEP]
have eq:"T = T'"
[PROOF STATE]
proof (prove)
using this:
P,E,h \<turnstile> V:=Val v : T'
E V = \<lfloor>T\<rfloor>

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

goal (60 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P,h \<turnstile> l (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,h \<turnstile> l (:\<le>)\<^sub>w E
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> Cast C e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
A total of 60 subgoals...
[PROOF STEP]
with casts wt wf
[PROOF STATE]
proof (chain)
picking this:
P \<turnstile> T casts v to v'
P,E,h \<turnstile> V:=Val v : T'
wwf_prog P
T = T'
[PROOF STEP]
have conf:"P,h \<turnstile> v' :\<le> T'"
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> T casts v to v'
P,E,h \<turnstile> V:=Val v : T'
wwf_prog P
T = T'

goal (1 subgoal):
 1. P,h \<turnstile> v' :\<le> T'
[PROOF STEP]
by(auto intro:casts_conf)
[PROOF STATE]
proof (state)
this:
P,h \<turnstile> v' :\<le> T'

goal (60 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P,h \<turnstile> l (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,h \<turnstile> l (:\<le>)\<^sub>w E
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> Cast C e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
A total of 60 subgoals...
[PROOF STEP]
with lconf env eq
[PROOF STATE]
proof (chain)
picking this:
P,h \<turnstile> l (:\<le>)\<^sub>w E
E V = \<lfloor>T\<rfloor>
T = T'
P,h \<turnstile> v' :\<le> T'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
P,h \<turnstile> l (:\<le>)\<^sub>w E
E V = \<lfloor>T\<rfloor>
T = T'
P,h \<turnstile> v' :\<le> T'

goal (1 subgoal):
 1. P,h \<turnstile> l(V \<mapsto> v') (:\<le>)\<^sub>w E
[PROOF STEP]
by (simp del:fun_upd_apply)(erule lconf_upd,simp_all)
[PROOF STATE]
proof (state)
this:
P,h \<turnstile> l(V \<mapsto> v') (:\<le>)\<^sub>w E

goal (59 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P,h \<turnstile> l (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,h \<turnstile> l (:\<le>)\<^sub>w E
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> Cast C e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
A total of 59 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (59 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P,h \<turnstile> l (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,h \<turnstile> l (:\<le>)\<^sub>w E
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> Cast C e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
A total of 59 subgoals...
[PROOF STEP]
case RedFAss
[PROOF STATE]
proof (state)
this:
h_ a_ = \<lfloor>(D_, S_)\<rfloor>
P \<turnstile> last Cs'_ has least F_:T_ via Cs_
P \<turnstile> T_ casts v_ to v'_
Ds_ = Cs'_ @\<^sub>p Cs_
(Ds_, fs_) \<in> S_
P,E_,h_ \<turnstile> ref (a_, Cs'_)\<bullet>F_{Cs_} := Val v_ : T
P,h_ \<turnstile> l_ (:\<le>)\<^sub>w E_
P \<turnstile> E_ \<surd>

goal (59 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P,h \<turnstile> l (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,h \<turnstile> l (:\<le>)\<^sub>w E
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> Cast C e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
A total of 59 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
h_ a_ = \<lfloor>(D_, S_)\<rfloor>
P \<turnstile> last Cs'_ has least F_:T_ via Cs_
P \<turnstile> T_ casts v_ to v'_
Ds_ = Cs'_ @\<^sub>p Cs_
(Ds_, fs_) \<in> S_
P,E_,h_ \<turnstile> ref (a_, Cs'_)\<bullet>F_{Cs_} := Val v_ : T
P,h_ \<turnstile> l_ (:\<le>)\<^sub>w E_
P \<turnstile> E_ \<surd>

goal (1 subgoal):
 1. P,h_(a_ \<mapsto> (D_, insert (Ds_, fs_(F_ \<mapsto> v'_)) (S_ - {(Ds_, fs_)}))) \<turnstile> l_ (:\<le>)\<^sub>w E_
[PROOF STEP]
by(auto intro:lconf_hext red_hext_incr[OF red_reds.RedFAss]
         simp del:fun_upd_apply)
[PROOF STATE]
proof (state)
this:
P,h_(a_ \<mapsto> (D_, insert (Ds_, fs_(F_ \<mapsto> v'_)) (S_ - {(Ds_, fs_)}))) \<turnstile> l_ (:\<le>)\<^sub>w E_

goal (58 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P,h \<turnstile> l (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,h \<turnstile> l (:\<le>)\<^sub>w E
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> Cast C e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
A total of 58 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (58 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P,h \<turnstile> l (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,h \<turnstile> l (:\<le>)\<^sub>w E
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> Cast C e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
A total of 58 subgoals...
[PROOF STEP]
case (BlockRedNone E V T e h l e' h' l' T')
[PROOF STATE]
proof (state)
this:
P,E(V \<mapsto> T) \<turnstile> \<langle>e,(h, l(V := None))\<rangle> \<rightarrow> \<langle>e',(h', l')\<rangle>
\<lbrakk>P,E(V \<mapsto> T),h \<turnstile> e : ?T; P,h \<turnstile> l(V := None) (:\<le>)\<^sub>w E(V \<mapsto> T); P \<turnstile> E(V \<mapsto> T) \<surd>\<rbrakk> \<Longrightarrow> P,h' \<turnstile> l' (:\<le>)\<^sub>w E(V \<mapsto> T)
l' V = None
\<not> assigned V e
P,E,h \<turnstile> {V:T; e} : T'
P,h \<turnstile> l (:\<le>)\<^sub>w E
P \<turnstile> E \<surd>

goal (58 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P,h \<turnstile> l (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,h \<turnstile> l (:\<le>)\<^sub>w E
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> Cast C e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
A total of 58 subgoals...
[PROOF STEP]
have red:"P,E(V \<mapsto> T) \<turnstile> \<langle>e,(h, l(V := None))\<rangle> \<rightarrow> \<langle>e',(h', l')\<rangle>"
    and IH: "\<And>T''. \<lbrakk> P,E(V \<mapsto> T),h \<turnstile> e : T''; P,h \<turnstile> l(V:=None) (:\<le>)\<^sub>w E(V \<mapsto> T);
                      envconf P (E(V \<mapsto> T)) \<rbrakk>
                   \<Longrightarrow> P,h' \<turnstile> l' (:\<le>)\<^sub>w E(V \<mapsto> T)"
    and lconf: "P,h \<turnstile> l (:\<le>)\<^sub>w E" and wte: "P,E,h \<turnstile> {V:T; e} : T'"
    and envconf:"envconf P E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P,E(V \<mapsto> T) \<turnstile> \<langle>e,(h, l(V := None))\<rangle> \<rightarrow> \<langle>e',(h', l')\<rangle> &&& (\<And>T''. \<lbrakk>P,E(V \<mapsto> T),h \<turnstile> e : T''; P,h \<turnstile> l(V := None) (:\<le>)\<^sub>w E(V \<mapsto> T); P \<turnstile> E(V \<mapsto> T) \<surd>\<rbrakk> \<Longrightarrow> P,h' \<turnstile> l' (:\<le>)\<^sub>w E(V \<mapsto> T))) &&& P,h \<turnstile> l (:\<le>)\<^sub>w E &&& P,E,h \<turnstile> {V:T; e} : T' &&& P \<turnstile> E \<surd>
[PROOF STEP]
by fact+
[PROOF STATE]
proof (state)
this:
P,E(V \<mapsto> T) \<turnstile> \<langle>e,(h, l(V := None))\<rangle> \<rightarrow> \<langle>e',(h', l')\<rangle>
\<lbrakk>P,E(V \<mapsto> T),h \<turnstile> e : ?T''; P,h \<turnstile> l(V := None) (:\<le>)\<^sub>w E(V \<mapsto> T); P \<turnstile> E(V \<mapsto> T) \<surd>\<rbrakk> \<Longrightarrow> P,h' \<turnstile> l' (:\<le>)\<^sub>w E(V \<mapsto> T)
P,h \<turnstile> l (:\<le>)\<^sub>w E
P,E,h \<turnstile> {V:T; e} : T'
P \<turnstile> E \<surd>

goal (58 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P,h \<turnstile> l (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,h \<turnstile> l (:\<le>)\<^sub>w E
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> Cast C e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
A total of 58 subgoals...
[PROOF STEP]
from lconf_hext[OF lconf red_hext_incr[OF red]]
[PROOF STATE]
proof (chain)
picking this:
P,h' \<turnstile> l (:\<le>)\<^sub>w E
[PROOF STEP]
have lconf':"P,h' \<turnstile> l (:\<le>)\<^sub>w E"
[PROOF STATE]
proof (prove)
using this:
P,h' \<turnstile> l (:\<le>)\<^sub>w E

goal (1 subgoal):
 1. P,h' \<turnstile> l (:\<le>)\<^sub>w E
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
P,h' \<turnstile> l (:\<le>)\<^sub>w E

goal (58 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P,h \<turnstile> l (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,h \<turnstile> l (:\<le>)\<^sub>w E
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> Cast C e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
A total of 58 subgoals...
[PROOF STEP]
from wte
[PROOF STATE]
proof (chain)
picking this:
P,E,h \<turnstile> {V:T; e} : T'
[PROOF STEP]
have wte':"P,E(V\<mapsto>T),h \<turnstile> e : T'" and type:"is_type P T"
[PROOF STATE]
proof (prove)
using this:
P,E,h \<turnstile> {V:T; e} : T'

goal (1 subgoal):
 1. P,E(V \<mapsto> T),h \<turnstile> e : T' &&& is_type P T
[PROOF STEP]
by (auto elim:WTrt.cases)
[PROOF STATE]
proof (state)
this:
P,E(V \<mapsto> T),h \<turnstile> e : T'
is_type P T

goal (58 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P,h \<turnstile> l (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,h \<turnstile> l (:\<le>)\<^sub>w E
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> Cast C e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
A total of 58 subgoals...
[PROOF STEP]
from envconf type
[PROOF STATE]
proof (chain)
picking this:
P \<turnstile> E \<surd>
is_type P T
[PROOF STEP]
have envconf':"envconf P (E(V \<mapsto> T))"
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> E \<surd>
is_type P T

goal (1 subgoal):
 1. P \<turnstile> E(V \<mapsto> T) \<surd>
[PROOF STEP]
by(auto simp:envconf_def)
[PROOF STATE]
proof (state)
this:
P \<turnstile> E(V \<mapsto> T) \<surd>

goal (58 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P,h \<turnstile> l (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,h \<turnstile> l (:\<le>)\<^sub>w E
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> Cast C e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
A total of 58 subgoals...
[PROOF STEP]
from lconf
[PROOF STATE]
proof (chain)
picking this:
P,h \<turnstile> l (:\<le>)\<^sub>w E
[PROOF STEP]
have "P,h \<turnstile> (l(V := None)) (:\<le>)\<^sub>w E(V\<mapsto>T)"
[PROOF STATE]
proof (prove)
using this:
P,h \<turnstile> l (:\<le>)\<^sub>w E

goal (1 subgoal):
 1. P,h \<turnstile> l(V := None) (:\<le>)\<^sub>w E(V \<mapsto> T)
[PROOF STEP]
by (simp add:lconf_def fun_upd_apply)
[PROOF STATE]
proof (state)
this:
P,h \<turnstile> l(V := None) (:\<le>)\<^sub>w E(V \<mapsto> T)

goal (58 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P,h \<turnstile> l (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,h \<turnstile> l (:\<le>)\<^sub>w E
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> Cast C e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
A total of 58 subgoals...
[PROOF STEP]
from IH[OF wte' this envconf']
[PROOF STATE]
proof (chain)
picking this:
P,h' \<turnstile> l' (:\<le>)\<^sub>w E(V \<mapsto> T)
[PROOF STEP]
have "P,h' \<turnstile> l' (:\<le>)\<^sub>w E(V\<mapsto>T)"
[PROOF STATE]
proof (prove)
using this:
P,h' \<turnstile> l' (:\<le>)\<^sub>w E(V \<mapsto> T)

goal (1 subgoal):
 1. P,h' \<turnstile> l' (:\<le>)\<^sub>w E(V \<mapsto> T)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
P,h' \<turnstile> l' (:\<le>)\<^sub>w E(V \<mapsto> T)

goal (58 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P,h \<turnstile> l (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,h \<turnstile> l (:\<le>)\<^sub>w E
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> Cast C e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
A total of 58 subgoals...
[PROOF STEP]
with lconf'
[PROOF STATE]
proof (chain)
picking this:
P,h' \<turnstile> l (:\<le>)\<^sub>w E
P,h' \<turnstile> l' (:\<le>)\<^sub>w E(V \<mapsto> T)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
P,h' \<turnstile> l (:\<le>)\<^sub>w E
P,h' \<turnstile> l' (:\<le>)\<^sub>w E(V \<mapsto> T)

goal (1 subgoal):
 1. P,h' \<turnstile> l'(V := l V) (:\<le>)\<^sub>w E
[PROOF STEP]
by (fastforce simp:lconf_def fun_upd_apply split:if_split_asm)
[PROOF STATE]
proof (state)
this:
P,h' \<turnstile> l'(V := l V) (:\<le>)\<^sub>w E

goal (57 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P,h \<turnstile> l (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,h \<turnstile> l (:\<le>)\<^sub>w E
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> Cast C e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
A total of 57 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (57 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P,h \<turnstile> l (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,h \<turnstile> l (:\<le>)\<^sub>w E
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> Cast C e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
A total of 57 subgoals...
[PROOF STEP]
case (BlockRedSome E V T e h l e' h' l' v T')
[PROOF STATE]
proof (state)
this:
P,E(V \<mapsto> T) \<turnstile> \<langle>e,(h, l(V := None))\<rangle> \<rightarrow> \<langle>e',(h', l')\<rangle>
\<lbrakk>P,E(V \<mapsto> T),h \<turnstile> e : ?T; P,h \<turnstile> l(V := None) (:\<le>)\<^sub>w E(V \<mapsto> T); P \<turnstile> E(V \<mapsto> T) \<surd>\<rbrakk> \<Longrightarrow> P,h' \<turnstile> l' (:\<le>)\<^sub>w E(V \<mapsto> T)
l' V = \<lfloor>v\<rfloor>
\<not> assigned V e
P,E,h \<turnstile> {V:T; e} : T'
P,h \<turnstile> l (:\<le>)\<^sub>w E
P \<turnstile> E \<surd>

goal (57 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P,h \<turnstile> l (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,h \<turnstile> l (:\<le>)\<^sub>w E
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> Cast C e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
A total of 57 subgoals...
[PROOF STEP]
have red:"P,E(V \<mapsto> T) \<turnstile> \<langle>e,(h, l(V := None))\<rangle> \<rightarrow> \<langle>e',(h', l')\<rangle>"
    and IH: "\<And>T''. \<lbrakk> P,E(V \<mapsto> T),h \<turnstile> e : T''; P,h \<turnstile> l(V:=None) (:\<le>)\<^sub>w E(V \<mapsto> T);
                      envconf P (E(V \<mapsto> T)) \<rbrakk>
                   \<Longrightarrow> P,h' \<turnstile> l' (:\<le>)\<^sub>w E(V \<mapsto> T)"
    and lconf: "P,h \<turnstile> l (:\<le>)\<^sub>w E" and wte: "P,E,h \<turnstile> {V:T; e} : T'"
    and envconf:"envconf P E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P,E(V \<mapsto> T) \<turnstile> \<langle>e,(h, l(V := None))\<rangle> \<rightarrow> \<langle>e',(h', l')\<rangle> &&& (\<And>T''. \<lbrakk>P,E(V \<mapsto> T),h \<turnstile> e : T''; P,h \<turnstile> l(V := None) (:\<le>)\<^sub>w E(V \<mapsto> T); P \<turnstile> E(V \<mapsto> T) \<surd>\<rbrakk> \<Longrightarrow> P,h' \<turnstile> l' (:\<le>)\<^sub>w E(V \<mapsto> T))) &&& P,h \<turnstile> l (:\<le>)\<^sub>w E &&& P,E,h \<turnstile> {V:T; e} : T' &&& P \<turnstile> E \<surd>
[PROOF STEP]
by fact+
[PROOF STATE]
proof (state)
this:
P,E(V \<mapsto> T) \<turnstile> \<langle>e,(h, l(V := None))\<rangle> \<rightarrow> \<langle>e',(h', l')\<rangle>
\<lbrakk>P,E(V \<mapsto> T),h \<turnstile> e : ?T''; P,h \<turnstile> l(V := None) (:\<le>)\<^sub>w E(V \<mapsto> T); P \<turnstile> E(V \<mapsto> T) \<surd>\<rbrakk> \<Longrightarrow> P,h' \<turnstile> l' (:\<le>)\<^sub>w E(V \<mapsto> T)
P,h \<turnstile> l (:\<le>)\<^sub>w E
P,E,h \<turnstile> {V:T; e} : T'
P \<turnstile> E \<surd>

goal (57 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P,h \<turnstile> l (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,h \<turnstile> l (:\<le>)\<^sub>w E
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> Cast C e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
A total of 57 subgoals...
[PROOF STEP]
from lconf_hext[OF lconf red_hext_incr[OF red]]
[PROOF STATE]
proof (chain)
picking this:
P,h' \<turnstile> l (:\<le>)\<^sub>w E
[PROOF STEP]
have lconf':"P,h' \<turnstile> l (:\<le>)\<^sub>w E"
[PROOF STATE]
proof (prove)
using this:
P,h' \<turnstile> l (:\<le>)\<^sub>w E

goal (1 subgoal):
 1. P,h' \<turnstile> l (:\<le>)\<^sub>w E
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
P,h' \<turnstile> l (:\<le>)\<^sub>w E

goal (57 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P,h \<turnstile> l (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,h \<turnstile> l (:\<le>)\<^sub>w E
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> Cast C e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
A total of 57 subgoals...
[PROOF STEP]
from wte
[PROOF STATE]
proof (chain)
picking this:
P,E,h \<turnstile> {V:T; e} : T'
[PROOF STEP]
have wte':"P,E(V\<mapsto>T),h \<turnstile> e : T'" and type:"is_type P T"
[PROOF STATE]
proof (prove)
using this:
P,E,h \<turnstile> {V:T; e} : T'

goal (1 subgoal):
 1. P,E(V \<mapsto> T),h \<turnstile> e : T' &&& is_type P T
[PROOF STEP]
by (auto elim:WTrt.cases)
[PROOF STATE]
proof (state)
this:
P,E(V \<mapsto> T),h \<turnstile> e : T'
is_type P T

goal (57 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P,h \<turnstile> l (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,h \<turnstile> l (:\<le>)\<^sub>w E
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> Cast C e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
A total of 57 subgoals...
[PROOF STEP]
from envconf type
[PROOF STATE]
proof (chain)
picking this:
P \<turnstile> E \<surd>
is_type P T
[PROOF STEP]
have envconf':"envconf P (E(V \<mapsto> T))"
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> E \<surd>
is_type P T

goal (1 subgoal):
 1. P \<turnstile> E(V \<mapsto> T) \<surd>
[PROOF STEP]
by(auto simp:envconf_def)
[PROOF STATE]
proof (state)
this:
P \<turnstile> E(V \<mapsto> T) \<surd>

goal (57 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P,h \<turnstile> l (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,h \<turnstile> l (:\<le>)\<^sub>w E
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> Cast C e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
A total of 57 subgoals...
[PROOF STEP]
from lconf
[PROOF STATE]
proof (chain)
picking this:
P,h \<turnstile> l (:\<le>)\<^sub>w E
[PROOF STEP]
have "P,h \<turnstile> (l(V := None)) (:\<le>)\<^sub>w E(V\<mapsto>T)"
[PROOF STATE]
proof (prove)
using this:
P,h \<turnstile> l (:\<le>)\<^sub>w E

goal (1 subgoal):
 1. P,h \<turnstile> l(V := None) (:\<le>)\<^sub>w E(V \<mapsto> T)
[PROOF STEP]
by (simp add:lconf_def fun_upd_apply)
[PROOF STATE]
proof (state)
this:
P,h \<turnstile> l(V := None) (:\<le>)\<^sub>w E(V \<mapsto> T)

goal (57 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P,h \<turnstile> l (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,h \<turnstile> l (:\<le>)\<^sub>w E
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> Cast C e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
A total of 57 subgoals...
[PROOF STEP]
from IH[OF wte' this envconf']
[PROOF STATE]
proof (chain)
picking this:
P,h' \<turnstile> l' (:\<le>)\<^sub>w E(V \<mapsto> T)
[PROOF STEP]
have "P,h' \<turnstile> l' (:\<le>)\<^sub>w E(V\<mapsto>T)"
[PROOF STATE]
proof (prove)
using this:
P,h' \<turnstile> l' (:\<le>)\<^sub>w E(V \<mapsto> T)

goal (1 subgoal):
 1. P,h' \<turnstile> l' (:\<le>)\<^sub>w E(V \<mapsto> T)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
P,h' \<turnstile> l' (:\<le>)\<^sub>w E(V \<mapsto> T)

goal (57 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P,h \<turnstile> l (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,h \<turnstile> l (:\<le>)\<^sub>w E
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> Cast C e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
A total of 57 subgoals...
[PROOF STEP]
with lconf'
[PROOF STATE]
proof (chain)
picking this:
P,h' \<turnstile> l (:\<le>)\<^sub>w E
P,h' \<turnstile> l' (:\<le>)\<^sub>w E(V \<mapsto> T)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
P,h' \<turnstile> l (:\<le>)\<^sub>w E
P,h' \<turnstile> l' (:\<le>)\<^sub>w E(V \<mapsto> T)

goal (1 subgoal):
 1. P,h' \<turnstile> l'(V := l V) (:\<le>)\<^sub>w E
[PROOF STEP]
by (fastforce simp:lconf_def fun_upd_apply split:if_split_asm)
[PROOF STATE]
proof (state)
this:
P,h' \<turnstile> l'(V := l V) (:\<le>)\<^sub>w E

goal (56 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P,h \<turnstile> l (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,h \<turnstile> l (:\<le>)\<^sub>w E
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> Cast C e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
A total of 56 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (56 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P,h \<turnstile> l (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,h \<turnstile> l (:\<le>)\<^sub>w E
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> Cast C e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
A total of 56 subgoals...
[PROOF STEP]
case (InitBlockRed E V T e h l v' e' h' l' v'' v T')
[PROOF STATE]
proof (state)
this:
P,E(V \<mapsto> T) \<turnstile> \<langle>e,(h, l(V \<mapsto> v'))\<rangle> \<rightarrow> \<langle>e',(h', l')\<rangle>
\<lbrakk>P,E(V \<mapsto> T),h \<turnstile> e : ?T; P,h \<turnstile> l(V \<mapsto> v') (:\<le>)\<^sub>w E(V \<mapsto> T); P \<turnstile> E(V \<mapsto> T) \<surd>\<rbrakk> \<Longrightarrow> P,h' \<turnstile> l' (:\<le>)\<^sub>w E(V \<mapsto> T)
l' V = \<lfloor>v''\<rfloor>
P \<turnstile> T casts v to v'
P,E,h \<turnstile> {V:T; V:=Val v;; e} : T'
P,h \<turnstile> l (:\<le>)\<^sub>w E
P \<turnstile> E \<surd>

goal (56 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P,h \<turnstile> l (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,h \<turnstile> l (:\<le>)\<^sub>w E
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> Cast C e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
A total of 56 subgoals...
[PROOF STEP]
have red: "P,E(V \<mapsto> T) \<turnstile> \<langle>e, (h, l(V\<mapsto>v'))\<rangle> \<rightarrow> \<langle>e',(h', l')\<rangle>"
     and IH: "\<And>T''. \<lbrakk> P,E(V \<mapsto> T),h \<turnstile> e : T''; P,h \<turnstile> l(V \<mapsto> v') (:\<le>)\<^sub>w E(V \<mapsto> T);
                       envconf P (E(V \<mapsto> T)) \<rbrakk>
                   \<Longrightarrow> P,h' \<turnstile> l' (:\<le>)\<^sub>w E(V \<mapsto> T)"
    and lconf:"P,h \<turnstile> l (:\<le>)\<^sub>w E" and l':"l' V = Some v''"
    and wte:"P,E,h \<turnstile> {V:T; V:=Val v;; e} : T'"
    and casts:"P \<turnstile> T casts v to v'" and envconf:"envconf P E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P,E(V \<mapsto> T) \<turnstile> \<langle>e,(h, l(V \<mapsto> v'))\<rangle> \<rightarrow> \<langle>e',(h', l')\<rangle> &&& (\<And>T''. \<lbrakk>P,E(V \<mapsto> T),h \<turnstile> e : T''; P,h \<turnstile> l(V \<mapsto> v') (:\<le>)\<^sub>w E(V \<mapsto> T); P \<turnstile> E(V \<mapsto> T) \<surd>\<rbrakk> \<Longrightarrow> P,h' \<turnstile> l' (:\<le>)\<^sub>w E(V \<mapsto> T)) &&& P,h \<turnstile> l (:\<le>)\<^sub>w E) &&& (l' V = \<lfloor>v''\<rfloor> &&& P,E,h \<turnstile> {V:T; V:=Val v;; e} : T') &&& P \<turnstile> T casts v to v'  &&& P \<turnstile> E \<surd>
[PROOF STEP]
by fact+
[PROOF STATE]
proof (state)
this:
P,E(V \<mapsto> T) \<turnstile> \<langle>e,(h, l(V \<mapsto> v'))\<rangle> \<rightarrow> \<langle>e',(h', l')\<rangle>
\<lbrakk>P,E(V \<mapsto> T),h \<turnstile> e : ?T''; P,h \<turnstile> l(V \<mapsto> v') (:\<le>)\<^sub>w E(V \<mapsto> T); P \<turnstile> E(V \<mapsto> T) \<surd>\<rbrakk> \<Longrightarrow> P,h' \<turnstile> l' (:\<le>)\<^sub>w E(V \<mapsto> T)
P,h \<turnstile> l (:\<le>)\<^sub>w E
l' V = \<lfloor>v''\<rfloor>
P,E,h \<turnstile> {V:T; V:=Val v;; e} : T'
P \<turnstile> T casts v to v'
P \<turnstile> E \<surd>

goal (56 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P,h \<turnstile> l (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,h \<turnstile> l (:\<le>)\<^sub>w E
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> Cast C e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
A total of 56 subgoals...
[PROOF STEP]
from lconf_hext[OF lconf red_hext_incr[OF red]]
[PROOF STATE]
proof (chain)
picking this:
P,h' \<turnstile> l (:\<le>)\<^sub>w E
[PROOF STEP]
have lconf':"P,h' \<turnstile> l (:\<le>)\<^sub>w E"
[PROOF STATE]
proof (prove)
using this:
P,h' \<turnstile> l (:\<le>)\<^sub>w E

goal (1 subgoal):
 1. P,h' \<turnstile> l (:\<le>)\<^sub>w E
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
P,h' \<turnstile> l (:\<le>)\<^sub>w E

goal (56 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P,h \<turnstile> l (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,h \<turnstile> l (:\<le>)\<^sub>w E
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> Cast C e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
A total of 56 subgoals...
[PROOF STEP]
from wte
[PROOF STATE]
proof (chain)
picking this:
P,E,h \<turnstile> {V:T; V:=Val v;; e} : T'
[PROOF STEP]
obtain T'' where wte':"P,E(V\<mapsto>T),h \<turnstile> e : T'"
    and wt:"P,E(V \<mapsto> T),h \<turnstile> V:=Val v : T''"
    and type:"is_type P T"
[PROOF STATE]
proof (prove)
using this:
P,E,h \<turnstile> {V:T; V:=Val v;; e} : T'

goal (1 subgoal):
 1. (\<And>T''. \<lbrakk>P,E(V \<mapsto> T),h \<turnstile> e : T'; P,E(V \<mapsto> T),h \<turnstile> V:=Val v : T''; is_type P T\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto elim:WTrt.cases)
[PROOF STATE]
proof (state)
this:
P,E(V \<mapsto> T),h \<turnstile> e : T'
P,E(V \<mapsto> T),h \<turnstile> V:=Val v : T''
is_type P T

goal (56 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P,h \<turnstile> l (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,h \<turnstile> l (:\<le>)\<^sub>w E
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> Cast C e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
A total of 56 subgoals...
[PROOF STEP]
from envconf type
[PROOF STATE]
proof (chain)
picking this:
P \<turnstile> E \<surd>
is_type P T
[PROOF STEP]
have envconf':"envconf P (E(V \<mapsto> T))"
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> E \<surd>
is_type P T

goal (1 subgoal):
 1. P \<turnstile> E(V \<mapsto> T) \<surd>
[PROOF STEP]
by(auto simp:envconf_def)
[PROOF STATE]
proof (state)
this:
P \<turnstile> E(V \<mapsto> T) \<surd>

goal (56 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P,h \<turnstile> l (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,h \<turnstile> l (:\<le>)\<^sub>w E
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> Cast C e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
A total of 56 subgoals...
[PROOF STEP]
from wt
[PROOF STATE]
proof (chain)
picking this:
P,E(V \<mapsto> T),h \<turnstile> V:=Val v : T''
[PROOF STEP]
have "T'' = T"
[PROOF STATE]
proof (prove)
using this:
P,E(V \<mapsto> T),h \<turnstile> V:=Val v : T''

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

goal (56 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P,h \<turnstile> l (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,h \<turnstile> l (:\<le>)\<^sub>w E
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> Cast C e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
A total of 56 subgoals...
[PROOF STEP]
with wf casts wt
[PROOF STATE]
proof (chain)
picking this:
wwf_prog P
P \<turnstile> T casts v to v'
P,E(V \<mapsto> T),h \<turnstile> V:=Val v : T''
T'' = T
[PROOF STEP]
have "P,h \<turnstile> v' :\<le> T"
[PROOF STATE]
proof (prove)
using this:
wwf_prog P
P \<turnstile> T casts v to v'
P,E(V \<mapsto> T),h \<turnstile> V:=Val v : T''
T'' = T

goal (1 subgoal):
 1. P,h \<turnstile> v' :\<le> T
[PROOF STEP]
by(auto intro:casts_conf)
[PROOF STATE]
proof (state)
this:
P,h \<turnstile> v' :\<le> T

goal (56 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P,h \<turnstile> l (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,h \<turnstile> l (:\<le>)\<^sub>w E
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> Cast C e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
A total of 56 subgoals...
[PROOF STEP]
with lconf
[PROOF STATE]
proof (chain)
picking this:
P,h \<turnstile> l (:\<le>)\<^sub>w E
P,h \<turnstile> v' :\<le> T
[PROOF STEP]
have "P,h \<turnstile> l(V \<mapsto> v') (:\<le>)\<^sub>w E(V\<mapsto>T)"
[PROOF STATE]
proof (prove)
using this:
P,h \<turnstile> l (:\<le>)\<^sub>w E
P,h \<turnstile> v' :\<le> T

goal (1 subgoal):
 1. P,h \<turnstile> l(V \<mapsto> v') (:\<le>)\<^sub>w E(V \<mapsto> T)
[PROOF STEP]
by -(rule lconf_upd2)
[PROOF STATE]
proof (state)
this:
P,h \<turnstile> l(V \<mapsto> v') (:\<le>)\<^sub>w E(V \<mapsto> T)

goal (56 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P,h \<turnstile> l (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,h \<turnstile> l (:\<le>)\<^sub>w E
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> Cast C e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
A total of 56 subgoals...
[PROOF STEP]
from IH[OF wte' this envconf']
[PROOF STATE]
proof (chain)
picking this:
P,h' \<turnstile> l' (:\<le>)\<^sub>w E(V \<mapsto> T)
[PROOF STEP]
have "P,h' \<turnstile> l' (:\<le>)\<^sub>w E(V \<mapsto> T)"
[PROOF STATE]
proof (prove)
using this:
P,h' \<turnstile> l' (:\<le>)\<^sub>w E(V \<mapsto> T)

goal (1 subgoal):
 1. P,h' \<turnstile> l' (:\<le>)\<^sub>w E(V \<mapsto> T)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
P,h' \<turnstile> l' (:\<le>)\<^sub>w E(V \<mapsto> T)

goal (56 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P,h \<turnstile> l (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,h \<turnstile> l (:\<le>)\<^sub>w E
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> Cast C e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
A total of 56 subgoals...
[PROOF STEP]
with lconf'
[PROOF STATE]
proof (chain)
picking this:
P,h' \<turnstile> l (:\<le>)\<^sub>w E
P,h' \<turnstile> l' (:\<le>)\<^sub>w E(V \<mapsto> T)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
P,h' \<turnstile> l (:\<le>)\<^sub>w E
P,h' \<turnstile> l' (:\<le>)\<^sub>w E(V \<mapsto> T)

goal (1 subgoal):
 1. P,h' \<turnstile> l'(V := l V) (:\<le>)\<^sub>w E
[PROOF STEP]
by (fastforce simp:lconf_def fun_upd_apply split:if_split_asm)
[PROOF STATE]
proof (state)
this:
P,h' \<turnstile> l'(V := l V) (:\<le>)\<^sub>w E

goal (55 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P,h \<turnstile> l (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,h \<turnstile> l (:\<le>)\<^sub>w E
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> Cast C e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
A total of 55 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (55 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P,h \<turnstile> l (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,h \<turnstile> l (:\<le>)\<^sub>w E
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> Cast C e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
A total of 55 subgoals...
[PROOF STEP]
case (CallObj E e h l e' h' l' Copt M es)
[PROOF STATE]
proof (state)
this:
P,E \<turnstile> \<langle>e,(h, l)\<rangle> \<rightarrow> \<langle>e',(h', l')\<rangle>
\<lbrakk>P,E,h \<turnstile> e : ?T; P,h \<turnstile> l (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,h' \<turnstile> l' (:\<le>)\<^sub>w E
P,E,h \<turnstile> Call e Copt M es : T
P,h \<turnstile> l (:\<le>)\<^sub>w E
P \<turnstile> E \<surd>

goal (55 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P,h \<turnstile> l (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,h \<turnstile> l (:\<le>)\<^sub>w E
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> Cast C e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
A total of 55 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
P,E \<turnstile> \<langle>e,(h, l)\<rangle> \<rightarrow> \<langle>e',(h', l')\<rangle>
\<lbrakk>P,E,h \<turnstile> e : ?T; P,h \<turnstile> l (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,h' \<turnstile> l' (:\<le>)\<^sub>w E
P,E,h \<turnstile> Call e Copt M es : T
P,h \<turnstile> l (:\<le>)\<^sub>w E
P \<turnstile> E \<surd>

goal (1 subgoal):
 1. P,h' \<turnstile> l' (:\<le>)\<^sub>w E
[PROOF STEP]
by (cases Copt) auto
[PROOF STATE]
proof (state)
this:
P,h' \<turnstile> l' (:\<le>)\<^sub>w E

goal (54 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P,h \<turnstile> l (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,h \<turnstile> l (:\<le>)\<^sub>w E
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> Cast C e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
A total of 54 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (54 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P,h \<turnstile> l (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,h \<turnstile> l (:\<le>)\<^sub>w E
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> Cast C e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
A total of 54 subgoals...
[PROOF STEP]
case (CallParams E es h l es' h' l' v Copt M)
[PROOF STATE]
proof (state)
this:
P,E \<turnstile> \<langle>es,(h, l)\<rangle> [\<rightarrow>] \<langle>es',(h', l')\<rangle>
\<lbrakk>P,E,h \<turnstile> es [:] ?Ts; P,h \<turnstile> l (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,h' \<turnstile> l' (:\<le>)\<^sub>w E
P,E,h \<turnstile> Call (Val v) Copt M es : T
P,h \<turnstile> l (:\<le>)\<^sub>w E
P \<turnstile> E \<surd>

goal (54 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P,h \<turnstile> l (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,h \<turnstile> l (:\<le>)\<^sub>w E
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> Cast C e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
A total of 54 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
P,E \<turnstile> \<langle>es,(h, l)\<rangle> [\<rightarrow>] \<langle>es',(h', l')\<rangle>
\<lbrakk>P,E,h \<turnstile> es [:] ?Ts; P,h \<turnstile> l (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,h' \<turnstile> l' (:\<le>)\<^sub>w E
P,E,h \<turnstile> Call (Val v) Copt M es : T
P,h \<turnstile> l (:\<le>)\<^sub>w E
P \<turnstile> E \<surd>

goal (1 subgoal):
 1. P,h' \<turnstile> l' (:\<le>)\<^sub>w E
[PROOF STEP]
by (cases Copt) auto
[PROOF STATE]
proof (state)
this:
P,h' \<turnstile> l' (:\<le>)\<^sub>w E

goal (53 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P,h \<turnstile> l (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,h \<turnstile> l (:\<le>)\<^sub>w E
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> Cast C e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
A total of 53 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (53 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P,h \<turnstile> l (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,h \<turnstile> l (:\<le>)\<^sub>w E
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> Cast C e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
A total of 53 subgoals...
[PROOF STEP]
case (RedCallNull E Copt M vs h l)
[PROOF STATE]
proof (state)
this:
P,E,h \<turnstile> Call null Copt M (map Val vs) : T
P,h \<turnstile> l (:\<le>)\<^sub>w E
P \<turnstile> E \<surd>

goal (53 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P,h \<turnstile> l (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,h \<turnstile> l (:\<le>)\<^sub>w E
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> Cast C e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
A total of 53 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
P,E,h \<turnstile> Call null Copt M (map Val vs) : T
P,h \<turnstile> l (:\<le>)\<^sub>w E
P \<turnstile> E \<surd>

goal (1 subgoal):
 1. P,h \<turnstile> l (:\<le>)\<^sub>w E
[PROOF STEP]
by (cases Copt) auto
[PROOF STATE]
proof (state)
this:
P,h \<turnstile> l (:\<le>)\<^sub>w E

goal (52 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P,h \<turnstile> l (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,h \<turnstile> l (:\<le>)\<^sub>w E
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E; P,E,a \<turnstile> Cast C e : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> ba (:\<le>)\<^sub>w E
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P,a \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,a \<turnstile> b (:\<le>)\<^sub>w E
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P,aa \<turnstile> b (:\<le>)\<^sub>w E; P \<turnstile> E \<surd>\<rbrakk> \<Longrightarrow> P,aa \<turnstile> b (:\<le>)\<^sub>w E
A total of 52 subgoals...
[PROOF STEP]
qed auto