[STATEMENT]
lemma [iff]: "\<And>A. \<lbrakk> length Vs = length Ts; length vs = length Ts\<rbrakk> \<Longrightarrow>
 \<D> (blocks (Vs,Ts,vs,e)) A = \<D> e (A \<squnion> \<lfloor>set Vs\<rfloor>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>A. \<lbrakk>length Vs = length Ts; length vs = length Ts\<rbrakk> \<Longrightarrow> \<D> (blocks (Vs, Ts, vs, e)) A = \<D> e (A \<squnion> \<lfloor>set Vs\<rfloor>)
[PROOF STEP]
apply(induct Vs Ts vs e rule:blocks_old_induct)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>aj ak al A. \<lbrakk>length [] = length []; length (aj # ak) = length []\<rbrakk> \<Longrightarrow> \<D> (blocks ([], [], aj # ak, al)) A = \<D> al (A \<squnion> \<lfloor>set []\<rfloor>)
 2. \<And>ad ae a b A. \<lbrakk>length [] = length (ad # ae); length a = length (ad # ae)\<rbrakk> \<Longrightarrow> \<D> (blocks ([], ad # ae, a, b)) A = \<D> b (A \<squnion> \<lfloor>set []\<rfloor>)
 3. \<And>V Vs a b A. \<lbrakk>length (V # Vs) = length []; length a = length []\<rbrakk> \<Longrightarrow> \<D> (blocks (V # Vs, [], a, b)) A = \<D> b (A \<squnion> \<lfloor>set (V # Vs)\<rfloor>)
 4. \<And>V Vs T Ts aw A. \<lbrakk>length (V # Vs) = length (T # Ts); length [] = length (T # Ts)\<rbrakk> \<Longrightarrow> \<D> (blocks (V # Vs, T # Ts, [], aw)) A = \<D> aw (A \<squnion> \<lfloor>set (V # Vs)\<rfloor>)
 5. \<And>V Vs T Ts v vs e A. \<lbrakk>\<And>A. \<lbrakk>length Vs = length Ts; length vs = length Ts\<rbrakk> \<Longrightarrow> \<D> (blocks (Vs, Ts, vs, e)) A = \<D> e (A \<squnion> \<lfloor>set Vs\<rfloor>); length (V # Vs) = length (T # Ts); length (v # vs) = length (T # Ts)\<rbrakk> \<Longrightarrow> \<D> (blocks (V # Vs, T # Ts, v # vs, e)) A = \<D> e (A \<squnion> \<lfloor>set (V # Vs)\<rfloor>)
 6. \<And>e A. \<lbrakk>length [] = length []; length [] = length []\<rbrakk> \<Longrightarrow> \<D> (blocks ([], [], [], e)) A = \<D> e (A \<squnion> \<lfloor>set []\<rfloor>)
[PROOF STEP]
apply(simp_all add:hyperset_defs)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma red_lA_incr: "P,E \<turnstile> \<langle>e,(h,l)\<rangle> \<rightarrow> \<langle>e',(h',l')\<rangle> \<Longrightarrow> \<lfloor>dom l\<rfloor> \<squnion> \ e \<sqsubseteq>  \<lfloor>dom l'\<rfloor> \<squnion> \ e'"
  and reds_lA_incr: "P,E \<turnstile> \<langle>es,(h,l)\<rangle> [\<rightarrow>] \<langle>es',(h',l')\<rangle> \<Longrightarrow> \<lfloor>dom l\<rfloor> \<squnion> \s es \<sqsubseteq>  \<lfloor>dom l'\<rfloor> \<squnion> \s es'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P,E \<turnstile> \<langle>e,(h, l)\<rangle> \<rightarrow> \<langle>e',(h', l')\<rangle> \<Longrightarrow> \<lfloor>dom l\<rfloor> \<squnion> \ e \<sqsubseteq> \<lfloor>dom l'\<rfloor> \<squnion> \ e') &&& (P,E \<turnstile> \<langle>es,(h, l)\<rangle> [\<rightarrow>] \<langle>es',(h', l')\<rangle> \<Longrightarrow> \<lfloor>dom l\<rfloor> \<squnion> \s es \<sqsubseteq> \<lfloor>dom l'\<rfloor> \<squnion> \s es')
[PROOF STEP]
apply (induct rule:red_reds_inducts)
[PROOF STATE]
proof (prove)
goal (61 subgoals):
 1. \<And>h a h' C E l. \<lbrakk>new_Addr h = \<lfloor>a\<rfloor>; h' = h(a \<mapsto> (C, Collect (init_obj P C)))\<rbrakk> \<Longrightarrow> \<lfloor>dom l\<rfloor> \<squnion> \ (new C) \<sqsubseteq> \<lfloor>dom l\<rfloor> \<squnion> \ (ref (a, [C]))
 2. \<And>h E C l. new_Addr h = None \<Longrightarrow> \<lfloor>dom l\<rfloor> \<squnion> \ (new C) \<sqsubseteq> \<lfloor>dom l\<rfloor> \<squnion> \ (Throw (addr_of_sys_xcpt OutOfMemory, [OutOfMemory]))
 3. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<lfloor>dom b\<rfloor> \<squnion> \ e \<sqsubseteq> \<lfloor>dom ba\<rfloor> \<squnion> \ e'\<rbrakk> \<Longrightarrow> \<lfloor>dom b\<rfloor> \<squnion> \ (\<lparr>C\<rparr>e) \<sqsubseteq> \<lfloor>dom ba\<rfloor> \<squnion> \ (\<lparr>C\<rparr>e')
 4. \<And>E C a b. \<lfloor>dom b\<rfloor> \<squnion> \ (\<lparr>C\<rparr>null) \<sqsubseteq> \<lfloor>dom b\<rfloor> \<squnion> \ null
 5. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'\<rbrakk> \<Longrightarrow> \<lfloor>dom b\<rfloor> \<squnion> \ (\<lparr>C\<rparr>ref (a, Cs)) \<sqsubseteq> \<lfloor>dom b\<rfloor> \<squnion> \ (ref (a, Ds))
 6. \<And>E C a Cs Cs' aa b. \<lfloor>dom b\<rfloor> \<squnion> \ (\<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs')) \<sqsubseteq> \<lfloor>dom b\<rfloor> \<squnion> \ (ref (a, Cs @ [C]))
 7. \<And>C Cs E a aa b. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*\<rbrakk> \<Longrightarrow> \<lfloor>dom b\<rfloor> \<squnion> \ (\<lparr>C\<rparr>ref (a, Cs)) \<sqsubseteq> \<lfloor>dom b\<rfloor> \<squnion> \ (Throw (addr_of_sys_xcpt ClassCast, [ClassCast]))
 8. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<lfloor>dom b\<rfloor> \<squnion> \ e \<sqsubseteq> \<lfloor>dom ba\<rfloor> \<squnion> \ e'\<rbrakk> \<Longrightarrow> \<lfloor>dom b\<rfloor> \<squnion> \ (Cast C e) \<sqsubseteq> \<lfloor>dom ba\<rfloor> \<squnion> \ (Cast C e')
 9. \<And>E C a b. \<lfloor>dom b\<rfloor> \<squnion> \ (Cast C null) \<sqsubseteq> \<lfloor>dom b\<rfloor> \<squnion> \ null
 10. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'\<rbrakk> \<Longrightarrow> \<lfloor>dom b\<rfloor> \<squnion> \ (Cast C (ref (a, Cs))) \<sqsubseteq> \<lfloor>dom b\<rfloor> \<squnion> \ (ref (a, Ds))
A total of 61 subgoals...
[PROOF STEP]
apply (simp_all del: fun_upd_apply add: hyperset_defs)
[PROOF STATE]
proof (prove)
goal (16 subgoals):
 1. \<And>E e a b e' aa ba e\<^sub>2 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; dom ba \<union> x2a = x2; \ e = \<lfloor>x2c\<rfloor>; dom b \<union> x2c = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e\<^sub>2 = \<lfloor>x2\<rfloor> \<longrightarrow> dom b \<subseteq> dom ba \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom ba \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom ba \<union> (x2a \<union> x2)
 2. \<And>E e a b e' aa ba x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; dom ba \<union> x2a = x2; \ e = \<lfloor>x2c\<rfloor>; dom b \<union> x2c = x2b\<rbrakk> \<Longrightarrow> dom b \<subseteq> x2 \<and> x2c \<subseteq> x2
 3. \<And>E e a b e' aa ba V x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; dom ba \<union> x2a = x2; \ e = \<lfloor>x2c\<rfloor>; dom b \<union> x2c = x2b\<rbrakk> \<Longrightarrow> dom b \<subseteq> insert V x2 \<and> x2c \<subseteq> insert V x2
 4. \<And>E e a b e' aa ba e\<^sub>2 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; dom ba \<union> x2a = x2; \ e = \<lfloor>x2c\<rfloor>; dom b \<union> x2c = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e\<^sub>2 = \<lfloor>x2\<rfloor> \<longrightarrow> dom b \<subseteq> dom ba \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom ba \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom ba \<union> (x2a \<union> x2)
 5. \<And>E e a b e' aa ba x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; dom ba \<union> x2a = x2; \ e = \<lfloor>x2c\<rfloor>; dom b \<union> x2c = x2b\<rbrakk> \<Longrightarrow> dom b \<subseteq> x2 \<and> x2c \<subseteq> x2
 6. \<And>E e a b e' aa ba es x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; dom ba \<union> x2a = x2; \ e = \<lfloor>x2c\<rfloor>; dom b \<union> x2c = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \s es = \<lfloor>x2\<rfloor> \<longrightarrow> dom b \<subseteq> dom ba \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom ba \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom ba \<union> (x2a \<union> x2)
 7. \<And>E es a b es' aa ba x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; P,E \<turnstile> \<langle>es,(a, b)\<rangle> [\<rightarrow>] \<langle>es',(aa, ba)\<rangle>; \s es' = \<lfloor>x2a\<rfloor>; dom ba \<union> x2a = x2; \s es = \<lfloor>x2c\<rfloor>; dom b \<union> x2c = x2b\<rbrakk> \<Longrightarrow> dom b \<subseteq> x2 \<and> x2c \<subseteq> x2
 8. \<And>E V T e h l e' h' l' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; l' V = None; \<not> assigned V e; P,E(V \<mapsto> T) \<turnstile> \<langle>e,(h, l(V := None))\<rangle> \<rightarrow> \<langle>e',(h', l')\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; dom l' \<union> x2a = x2; \ e = \<lfloor>x2c\<rfloor>; dom l - {V} \<union> x2c = x2b\<rbrakk> \<Longrightarrow> (l V = None \<longrightarrow> dom l \<subseteq> dom l' - {V} \<union> (x2a - {V}) \<and> x2c - {V} \<subseteq> dom l' - {V} \<union> (x2a - {V})) \<and> ((\<exists>y. l V = \<lfloor>y\<rfloor>) \<longrightarrow> dom l \<subseteq> insert V (dom l' \<union> (x2a - {V})) \<and> x2c - {V} \<subseteq> insert V (dom l' \<union> (x2a - {V})))
 9. \<And>E V T e h l e' h' l' v x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; l' V = \<lfloor>v\<rfloor>; \<not> assigned V e; P,E(V \<mapsto> T) \<turnstile> \<langle>e,(h, l(V := None))\<rangle> \<rightarrow> \<langle>e',(h', l')\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; dom l' \<union> x2a = x2; \ e = \<lfloor>x2c\<rfloor>; dom l - {V} \<union> x2c = x2b\<rbrakk> \<Longrightarrow> (l V = None \<longrightarrow> dom l \<subseteq> dom l' - {V} \<union> (x2a - {V}) \<and> x2c - {V} \<subseteq> dom l' - {V} \<union> (x2a - {V})) \<and> ((\<exists>y. l V = \<lfloor>y\<rfloor>) \<longrightarrow> dom l \<subseteq> insert V (dom l' \<union> (x2a - {V})) \<and> x2c - {V} \<subseteq> insert V (dom l' \<union> (x2a - {V})))
 10. \<And>E V T e h l v' e' h' l' v'' v x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; l' V = \<lfloor>v''\<rfloor>; P \<turnstile> T casts v to v' ; P,E(V \<mapsto> T) \<turnstile> \<langle>e,(h, l(V \<mapsto> v'))\<rangle> \<rightarrow> \<langle>e',(h', l')\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; dom l' \<union> x2a = x2; \ e = \<lfloor>x2c\<rfloor>; insert V (dom l \<union> x2c) = x2b\<rbrakk> \<Longrightarrow> (l V = None \<longrightarrow> dom l \<subseteq> dom l' - {V} \<union> (x2a - {V}) \<and> x2c - {V} \<subseteq> dom l' - {V} \<union> (x2a - {V})) \<and> ((\<exists>y. l V = \<lfloor>y\<rfloor>) \<longrightarrow> dom l \<subseteq> insert V (dom l' \<union> (x2a - {V})) \<and> x2c - {V} \<subseteq> insert V (dom l' \<union> (x2a - {V})))
A total of 16 subgoals...
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (15 subgoals):
 1. \<And>E e a b e' aa ba x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; dom ba \<union> x2a = x2; \ e = \<lfloor>x2c\<rfloor>; dom b \<union> x2c = x2b\<rbrakk> \<Longrightarrow> dom b \<subseteq> x2 \<and> x2c \<subseteq> x2
 2. \<And>E e a b e' aa ba V x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; dom ba \<union> x2a = x2; \ e = \<lfloor>x2c\<rfloor>; dom b \<union> x2c = x2b\<rbrakk> \<Longrightarrow> dom b \<subseteq> insert V x2 \<and> x2c \<subseteq> insert V x2
 3. \<And>E e a b e' aa ba e\<^sub>2 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; dom ba \<union> x2a = x2; \ e = \<lfloor>x2c\<rfloor>; dom b \<union> x2c = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e\<^sub>2 = \<lfloor>x2\<rfloor> \<longrightarrow> dom b \<subseteq> dom ba \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom ba \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom ba \<union> (x2a \<union> x2)
 4. \<And>E e a b e' aa ba x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; dom ba \<union> x2a = x2; \ e = \<lfloor>x2c\<rfloor>; dom b \<union> x2c = x2b\<rbrakk> \<Longrightarrow> dom b \<subseteq> x2 \<and> x2c \<subseteq> x2
 5. \<And>E e a b e' aa ba es x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; dom ba \<union> x2a = x2; \ e = \<lfloor>x2c\<rfloor>; dom b \<union> x2c = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \s es = \<lfloor>x2\<rfloor> \<longrightarrow> dom b \<subseteq> dom ba \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom ba \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom ba \<union> (x2a \<union> x2)
 6. \<And>E es a b es' aa ba x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; P,E \<turnstile> \<langle>es,(a, b)\<rangle> [\<rightarrow>] \<langle>es',(aa, ba)\<rangle>; \s es' = \<lfloor>x2a\<rfloor>; dom ba \<union> x2a = x2; \s es = \<lfloor>x2c\<rfloor>; dom b \<union> x2c = x2b\<rbrakk> \<Longrightarrow> dom b \<subseteq> x2 \<and> x2c \<subseteq> x2
 7. \<And>E V T e h l e' h' l' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; l' V = None; \<not> assigned V e; P,E(V \<mapsto> T) \<turnstile> \<langle>e,(h, l(V := None))\<rangle> \<rightarrow> \<langle>e',(h', l')\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; dom l' \<union> x2a = x2; \ e = \<lfloor>x2c\<rfloor>; dom l - {V} \<union> x2c = x2b\<rbrakk> \<Longrightarrow> (l V = None \<longrightarrow> dom l \<subseteq> dom l' - {V} \<union> (x2a - {V}) \<and> x2c - {V} \<subseteq> dom l' - {V} \<union> (x2a - {V})) \<and> ((\<exists>y. l V = \<lfloor>y\<rfloor>) \<longrightarrow> dom l \<subseteq> insert V (dom l' \<union> (x2a - {V})) \<and> x2c - {V} \<subseteq> insert V (dom l' \<union> (x2a - {V})))
 8. \<And>E V T e h l e' h' l' v x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; l' V = \<lfloor>v\<rfloor>; \<not> assigned V e; P,E(V \<mapsto> T) \<turnstile> \<langle>e,(h, l(V := None))\<rangle> \<rightarrow> \<langle>e',(h', l')\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; dom l' \<union> x2a = x2; \ e = \<lfloor>x2c\<rfloor>; dom l - {V} \<union> x2c = x2b\<rbrakk> \<Longrightarrow> (l V = None \<longrightarrow> dom l \<subseteq> dom l' - {V} \<union> (x2a - {V}) \<and> x2c - {V} \<subseteq> dom l' - {V} \<union> (x2a - {V})) \<and> ((\<exists>y. l V = \<lfloor>y\<rfloor>) \<longrightarrow> dom l \<subseteq> insert V (dom l' \<union> (x2a - {V})) \<and> x2c - {V} \<subseteq> insert V (dom l' \<union> (x2a - {V})))
 9. \<And>E V T e h l v' e' h' l' v'' v x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; l' V = \<lfloor>v''\<rfloor>; P \<turnstile> T casts v to v' ; P,E(V \<mapsto> T) \<turnstile> \<langle>e,(h, l(V \<mapsto> v'))\<rangle> \<rightarrow> \<langle>e',(h', l')\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; dom l' \<union> x2a = x2; \ e = \<lfloor>x2c\<rfloor>; insert V (dom l \<union> x2c) = x2b\<rbrakk> \<Longrightarrow> (l V = None \<longrightarrow> dom l \<subseteq> dom l' - {V} \<union> (x2a - {V}) \<and> x2c - {V} \<subseteq> dom l' - {V} \<union> (x2a - {V})) \<and> ((\<exists>y. l V = \<lfloor>y\<rfloor>) \<longrightarrow> dom l \<subseteq> insert V (dom l' \<union> (x2a - {V})) \<and> x2c - {V} \<subseteq> insert V (dom l' \<union> (x2a - {V})))
 10. \<And>E e a b e' aa ba e\<^sub>2 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; dom ba \<union> x2a = x2; \ e = \<lfloor>x2c\<rfloor>; dom b \<union> x2c = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e\<^sub>2 = \<lfloor>x2\<rfloor> \<longrightarrow> dom b \<subseteq> dom ba \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom ba \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom ba \<union> (x2a \<union> x2)
A total of 15 subgoals...
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (14 subgoals):
 1. \<And>E e a b e' aa ba V x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; dom ba \<union> x2a = x2; \ e = \<lfloor>x2c\<rfloor>; dom b \<union> x2c = x2b\<rbrakk> \<Longrightarrow> dom b \<subseteq> insert V x2 \<and> x2c \<subseteq> insert V x2
 2. \<And>E e a b e' aa ba e\<^sub>2 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; dom ba \<union> x2a = x2; \ e = \<lfloor>x2c\<rfloor>; dom b \<union> x2c = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e\<^sub>2 = \<lfloor>x2\<rfloor> \<longrightarrow> dom b \<subseteq> dom ba \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom ba \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom ba \<union> (x2a \<union> x2)
 3. \<And>E e a b e' aa ba x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; dom ba \<union> x2a = x2; \ e = \<lfloor>x2c\<rfloor>; dom b \<union> x2c = x2b\<rbrakk> \<Longrightarrow> dom b \<subseteq> x2 \<and> x2c \<subseteq> x2
 4. \<And>E e a b e' aa ba es x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; dom ba \<union> x2a = x2; \ e = \<lfloor>x2c\<rfloor>; dom b \<union> x2c = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \s es = \<lfloor>x2\<rfloor> \<longrightarrow> dom b \<subseteq> dom ba \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom ba \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom ba \<union> (x2a \<union> x2)
 5. \<And>E es a b es' aa ba x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; P,E \<turnstile> \<langle>es,(a, b)\<rangle> [\<rightarrow>] \<langle>es',(aa, ba)\<rangle>; \s es' = \<lfloor>x2a\<rfloor>; dom ba \<union> x2a = x2; \s es = \<lfloor>x2c\<rfloor>; dom b \<union> x2c = x2b\<rbrakk> \<Longrightarrow> dom b \<subseteq> x2 \<and> x2c \<subseteq> x2
 6. \<And>E V T e h l e' h' l' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; l' V = None; \<not> assigned V e; P,E(V \<mapsto> T) \<turnstile> \<langle>e,(h, l(V := None))\<rangle> \<rightarrow> \<langle>e',(h', l')\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; dom l' \<union> x2a = x2; \ e = \<lfloor>x2c\<rfloor>; dom l - {V} \<union> x2c = x2b\<rbrakk> \<Longrightarrow> (l V = None \<longrightarrow> dom l \<subseteq> dom l' - {V} \<union> (x2a - {V}) \<and> x2c - {V} \<subseteq> dom l' - {V} \<union> (x2a - {V})) \<and> ((\<exists>y. l V = \<lfloor>y\<rfloor>) \<longrightarrow> dom l \<subseteq> insert V (dom l' \<union> (x2a - {V})) \<and> x2c - {V} \<subseteq> insert V (dom l' \<union> (x2a - {V})))
 7. \<And>E V T e h l e' h' l' v x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; l' V = \<lfloor>v\<rfloor>; \<not> assigned V e; P,E(V \<mapsto> T) \<turnstile> \<langle>e,(h, l(V := None))\<rangle> \<rightarrow> \<langle>e',(h', l')\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; dom l' \<union> x2a = x2; \ e = \<lfloor>x2c\<rfloor>; dom l - {V} \<union> x2c = x2b\<rbrakk> \<Longrightarrow> (l V = None \<longrightarrow> dom l \<subseteq> dom l' - {V} \<union> (x2a - {V}) \<and> x2c - {V} \<subseteq> dom l' - {V} \<union> (x2a - {V})) \<and> ((\<exists>y. l V = \<lfloor>y\<rfloor>) \<longrightarrow> dom l \<subseteq> insert V (dom l' \<union> (x2a - {V})) \<and> x2c - {V} \<subseteq> insert V (dom l' \<union> (x2a - {V})))
 8. \<And>E V T e h l v' e' h' l' v'' v x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; l' V = \<lfloor>v''\<rfloor>; P \<turnstile> T casts v to v' ; P,E(V \<mapsto> T) \<turnstile> \<langle>e,(h, l(V \<mapsto> v'))\<rangle> \<rightarrow> \<langle>e',(h', l')\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; dom l' \<union> x2a = x2; \ e = \<lfloor>x2c\<rfloor>; insert V (dom l \<union> x2c) = x2b\<rbrakk> \<Longrightarrow> (l V = None \<longrightarrow> dom l \<subseteq> dom l' - {V} \<union> (x2a - {V}) \<and> x2c - {V} \<subseteq> dom l' - {V} \<union> (x2a - {V})) \<and> ((\<exists>y. l V = \<lfloor>y\<rfloor>) \<longrightarrow> dom l \<subseteq> insert V (dom l' \<union> (x2a - {V})) \<and> x2c - {V} \<subseteq> insert V (dom l' \<union> (x2a - {V})))
 9. \<And>E e a b e' aa ba e\<^sub>2 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; dom ba \<union> x2a = x2; \ e = \<lfloor>x2c\<rfloor>; dom b \<union> x2c = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e\<^sub>2 = \<lfloor>x2\<rfloor> \<longrightarrow> dom b \<subseteq> dom ba \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom ba \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom ba \<union> (x2a \<union> x2)
 10. \<And>E e a b e' aa ba e\<^sub>1 e\<^sub>2 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; dom ba \<union> x2a = x2; \ e = \<lfloor>x2c\<rfloor>; dom b \<union> x2c = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. (\ e\<^sub>2 = None \<longrightarrow> x2c = x2 \<longrightarrow> (\<forall>x2b. \ e\<^sub>1 = \<lfloor>x2b\<rfloor> \<longrightarrow> dom b \<subseteq> dom ba \<union> (x2a \<union> x2b) \<and> x2 \<subseteq> dom ba \<union> (x2a \<union> x2b) \<and> x2b \<subseteq> dom ba \<union> (x2a \<union> x2b))) \<and> (\<forall>x2b. \ e\<^sub>2 = \<lfloor>x2b\<rfloor> \<longrightarrow> x2c = x2 \<longrightarrow> (\ e\<^sub>1 = None \<longrightarrow> dom b \<subseteq> dom ba \<union> (x2a \<union> x2b) \<and> x2 \<subseteq> dom ba \<union> (x2a \<union> x2b) \<and> x2b \<subseteq> dom ba \<union> (x2a \<union> x2b)) \<and> (\<forall>x2c. \ e\<^sub>1 = \<lfloor>x2c\<rfloor> \<longrightarrow> dom b \<subseteq> dom ba \<union> (x2a \<union> x2c \<inter> x2b) \<and> x2 \<subseteq> dom ba \<union> (x2a \<union> x2c \<inter> x2b) \<and> x2c \<inter> x2b \<subseteq> dom ba \<union> (x2a \<union> x2c \<inter> x2b)))
A total of 14 subgoals...
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (13 subgoals):
 1. \<And>E e a b e' aa ba e\<^sub>2 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; dom ba \<union> x2a = x2; \ e = \<lfloor>x2c\<rfloor>; dom b \<union> x2c = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e\<^sub>2 = \<lfloor>x2\<rfloor> \<longrightarrow> dom b \<subseteq> dom ba \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom ba \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom ba \<union> (x2a \<union> x2)
 2. \<And>E e a b e' aa ba x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; dom ba \<union> x2a = x2; \ e = \<lfloor>x2c\<rfloor>; dom b \<union> x2c = x2b\<rbrakk> \<Longrightarrow> dom b \<subseteq> x2 \<and> x2c \<subseteq> x2
 3. \<And>E e a b e' aa ba es x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; dom ba \<union> x2a = x2; \ e = \<lfloor>x2c\<rfloor>; dom b \<union> x2c = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \s es = \<lfloor>x2\<rfloor> \<longrightarrow> dom b \<subseteq> dom ba \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom ba \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom ba \<union> (x2a \<union> x2)
 4. \<And>E es a b es' aa ba x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; P,E \<turnstile> \<langle>es,(a, b)\<rangle> [\<rightarrow>] \<langle>es',(aa, ba)\<rangle>; \s es' = \<lfloor>x2a\<rfloor>; dom ba \<union> x2a = x2; \s es = \<lfloor>x2c\<rfloor>; dom b \<union> x2c = x2b\<rbrakk> \<Longrightarrow> dom b \<subseteq> x2 \<and> x2c \<subseteq> x2
 5. \<And>E V T e h l e' h' l' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; l' V = None; \<not> assigned V e; P,E(V \<mapsto> T) \<turnstile> \<langle>e,(h, l(V := None))\<rangle> \<rightarrow> \<langle>e',(h', l')\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; dom l' \<union> x2a = x2; \ e = \<lfloor>x2c\<rfloor>; dom l - {V} \<union> x2c = x2b\<rbrakk> \<Longrightarrow> (l V = None \<longrightarrow> dom l \<subseteq> dom l' - {V} \<union> (x2a - {V}) \<and> x2c - {V} \<subseteq> dom l' - {V} \<union> (x2a - {V})) \<and> ((\<exists>y. l V = \<lfloor>y\<rfloor>) \<longrightarrow> dom l \<subseteq> insert V (dom l' \<union> (x2a - {V})) \<and> x2c - {V} \<subseteq> insert V (dom l' \<union> (x2a - {V})))
 6. \<And>E V T e h l e' h' l' v x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; l' V = \<lfloor>v\<rfloor>; \<not> assigned V e; P,E(V \<mapsto> T) \<turnstile> \<langle>e,(h, l(V := None))\<rangle> \<rightarrow> \<langle>e',(h', l')\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; dom l' \<union> x2a = x2; \ e = \<lfloor>x2c\<rfloor>; dom l - {V} \<union> x2c = x2b\<rbrakk> \<Longrightarrow> (l V = None \<longrightarrow> dom l \<subseteq> dom l' - {V} \<union> (x2a - {V}) \<and> x2c - {V} \<subseteq> dom l' - {V} \<union> (x2a - {V})) \<and> ((\<exists>y. l V = \<lfloor>y\<rfloor>) \<longrightarrow> dom l \<subseteq> insert V (dom l' \<union> (x2a - {V})) \<and> x2c - {V} \<subseteq> insert V (dom l' \<union> (x2a - {V})))
 7. \<And>E V T e h l v' e' h' l' v'' v x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; l' V = \<lfloor>v''\<rfloor>; P \<turnstile> T casts v to v' ; P,E(V \<mapsto> T) \<turnstile> \<langle>e,(h, l(V \<mapsto> v'))\<rangle> \<rightarrow> \<langle>e',(h', l')\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; dom l' \<union> x2a = x2; \ e = \<lfloor>x2c\<rfloor>; insert V (dom l \<union> x2c) = x2b\<rbrakk> \<Longrightarrow> (l V = None \<longrightarrow> dom l \<subseteq> dom l' - {V} \<union> (x2a - {V}) \<and> x2c - {V} \<subseteq> dom l' - {V} \<union> (x2a - {V})) \<and> ((\<exists>y. l V = \<lfloor>y\<rfloor>) \<longrightarrow> dom l \<subseteq> insert V (dom l' \<union> (x2a - {V})) \<and> x2c - {V} \<subseteq> insert V (dom l' \<union> (x2a - {V})))
 8. \<And>E e a b e' aa ba e\<^sub>2 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; dom ba \<union> x2a = x2; \ e = \<lfloor>x2c\<rfloor>; dom b \<union> x2c = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e\<^sub>2 = \<lfloor>x2\<rfloor> \<longrightarrow> dom b \<subseteq> dom ba \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom ba \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom ba \<union> (x2a \<union> x2)
 9. \<And>E e a b e' aa ba e\<^sub>1 e\<^sub>2 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; dom ba \<union> x2a = x2; \ e = \<lfloor>x2c\<rfloor>; dom b \<union> x2c = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. (\ e\<^sub>2 = None \<longrightarrow> x2c = x2 \<longrightarrow> (\<forall>x2b. \ e\<^sub>1 = \<lfloor>x2b\<rfloor> \<longrightarrow> dom b \<subseteq> dom ba \<union> (x2a \<union> x2b) \<and> x2 \<subseteq> dom ba \<union> (x2a \<union> x2b) \<and> x2b \<subseteq> dom ba \<union> (x2a \<union> x2b))) \<and> (\<forall>x2b. \ e\<^sub>2 = \<lfloor>x2b\<rfloor> \<longrightarrow> x2c = x2 \<longrightarrow> (\ e\<^sub>1 = None \<longrightarrow> dom b \<subseteq> dom ba \<union> (x2a \<union> x2b) \<and> x2 \<subseteq> dom ba \<union> (x2a \<union> x2b) \<and> x2b \<subseteq> dom ba \<union> (x2a \<union> x2b)) \<and> (\<forall>x2c. \ e\<^sub>1 = \<lfloor>x2c\<rfloor> \<longrightarrow> dom b \<subseteq> dom ba \<union> (x2a \<union> x2c \<inter> x2b) \<and> x2 \<subseteq> dom ba \<union> (x2a \<union> x2c \<inter> x2b) \<and> x2c \<inter> x2b \<subseteq> dom ba \<union> (x2a \<union> x2c \<inter> x2b)))
 10. \<And>e\<^sub>1 e\<^sub>2 b. \<forall>x2 x2a. \ e\<^sub>2 = \<lfloor>x2a\<rfloor> \<longrightarrow> \ e\<^sub>1 = \<lfloor>x2\<rfloor> \<longrightarrow> x2 \<inter> x2a \<subseteq> dom b \<union> x2
A total of 13 subgoals...
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (12 subgoals):
 1. \<And>E e a b e' aa ba x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; dom ba \<union> x2a = x2; \ e = \<lfloor>x2c\<rfloor>; dom b \<union> x2c = x2b\<rbrakk> \<Longrightarrow> dom b \<subseteq> x2 \<and> x2c \<subseteq> x2
 2. \<And>E e a b e' aa ba es x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; dom ba \<union> x2a = x2; \ e = \<lfloor>x2c\<rfloor>; dom b \<union> x2c = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \s es = \<lfloor>x2\<rfloor> \<longrightarrow> dom b \<subseteq> dom ba \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom ba \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom ba \<union> (x2a \<union> x2)
 3. \<And>E es a b es' aa ba x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; P,E \<turnstile> \<langle>es,(a, b)\<rangle> [\<rightarrow>] \<langle>es',(aa, ba)\<rangle>; \s es' = \<lfloor>x2a\<rfloor>; dom ba \<union> x2a = x2; \s es = \<lfloor>x2c\<rfloor>; dom b \<union> x2c = x2b\<rbrakk> \<Longrightarrow> dom b \<subseteq> x2 \<and> x2c \<subseteq> x2
 4. \<And>E V T e h l e' h' l' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; l' V = None; \<not> assigned V e; P,E(V \<mapsto> T) \<turnstile> \<langle>e,(h, l(V := None))\<rangle> \<rightarrow> \<langle>e',(h', l')\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; dom l' \<union> x2a = x2; \ e = \<lfloor>x2c\<rfloor>; dom l - {V} \<union> x2c = x2b\<rbrakk> \<Longrightarrow> (l V = None \<longrightarrow> dom l \<subseteq> dom l' - {V} \<union> (x2a - {V}) \<and> x2c - {V} \<subseteq> dom l' - {V} \<union> (x2a - {V})) \<and> ((\<exists>y. l V = \<lfloor>y\<rfloor>) \<longrightarrow> dom l \<subseteq> insert V (dom l' \<union> (x2a - {V})) \<and> x2c - {V} \<subseteq> insert V (dom l' \<union> (x2a - {V})))
 5. \<And>E V T e h l e' h' l' v x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; l' V = \<lfloor>v\<rfloor>; \<not> assigned V e; P,E(V \<mapsto> T) \<turnstile> \<langle>e,(h, l(V := None))\<rangle> \<rightarrow> \<langle>e',(h', l')\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; dom l' \<union> x2a = x2; \ e = \<lfloor>x2c\<rfloor>; dom l - {V} \<union> x2c = x2b\<rbrakk> \<Longrightarrow> (l V = None \<longrightarrow> dom l \<subseteq> dom l' - {V} \<union> (x2a - {V}) \<and> x2c - {V} \<subseteq> dom l' - {V} \<union> (x2a - {V})) \<and> ((\<exists>y. l V = \<lfloor>y\<rfloor>) \<longrightarrow> dom l \<subseteq> insert V (dom l' \<union> (x2a - {V})) \<and> x2c - {V} \<subseteq> insert V (dom l' \<union> (x2a - {V})))
 6. \<And>E V T e h l v' e' h' l' v'' v x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; l' V = \<lfloor>v''\<rfloor>; P \<turnstile> T casts v to v' ; P,E(V \<mapsto> T) \<turnstile> \<langle>e,(h, l(V \<mapsto> v'))\<rangle> \<rightarrow> \<langle>e',(h', l')\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; dom l' \<union> x2a = x2; \ e = \<lfloor>x2c\<rfloor>; insert V (dom l \<union> x2c) = x2b\<rbrakk> \<Longrightarrow> (l V = None \<longrightarrow> dom l \<subseteq> dom l' - {V} \<union> (x2a - {V}) \<and> x2c - {V} \<subseteq> dom l' - {V} \<union> (x2a - {V})) \<and> ((\<exists>y. l V = \<lfloor>y\<rfloor>) \<longrightarrow> dom l \<subseteq> insert V (dom l' \<union> (x2a - {V})) \<and> x2c - {V} \<subseteq> insert V (dom l' \<union> (x2a - {V})))
 7. \<And>E e a b e' aa ba e\<^sub>2 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; dom ba \<union> x2a = x2; \ e = \<lfloor>x2c\<rfloor>; dom b \<union> x2c = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e\<^sub>2 = \<lfloor>x2\<rfloor> \<longrightarrow> dom b \<subseteq> dom ba \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom ba \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom ba \<union> (x2a \<union> x2)
 8. \<And>E e a b e' aa ba e\<^sub>1 e\<^sub>2 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; dom ba \<union> x2a = x2; \ e = \<lfloor>x2c\<rfloor>; dom b \<union> x2c = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. (\ e\<^sub>2 = None \<longrightarrow> x2c = x2 \<longrightarrow> (\<forall>x2b. \ e\<^sub>1 = \<lfloor>x2b\<rfloor> \<longrightarrow> dom b \<subseteq> dom ba \<union> (x2a \<union> x2b) \<and> x2 \<subseteq> dom ba \<union> (x2a \<union> x2b) \<and> x2b \<subseteq> dom ba \<union> (x2a \<union> x2b))) \<and> (\<forall>x2b. \ e\<^sub>2 = \<lfloor>x2b\<rfloor> \<longrightarrow> x2c = x2 \<longrightarrow> (\ e\<^sub>1 = None \<longrightarrow> dom b \<subseteq> dom ba \<union> (x2a \<union> x2b) \<and> x2 \<subseteq> dom ba \<union> (x2a \<union> x2b) \<and> x2b \<subseteq> dom ba \<union> (x2a \<union> x2b)) \<and> (\<forall>x2c. \ e\<^sub>1 = \<lfloor>x2c\<rfloor> \<longrightarrow> dom b \<subseteq> dom ba \<union> (x2a \<union> x2c \<inter> x2b) \<and> x2 \<subseteq> dom ba \<union> (x2a \<union> x2c \<inter> x2b) \<and> x2c \<inter> x2b \<subseteq> dom ba \<union> (x2a \<union> x2c \<inter> x2b)))
 9. \<And>e\<^sub>1 e\<^sub>2 b. \<forall>x2 x2a. \ e\<^sub>2 = \<lfloor>x2a\<rfloor> \<longrightarrow> \ e\<^sub>1 = \<lfloor>x2\<rfloor> \<longrightarrow> x2 \<inter> x2a \<subseteq> dom b \<union> x2
 10. \<And>e\<^sub>1 e\<^sub>2 b. \<forall>x2 x2a. \ e\<^sub>2 = \<lfloor>x2a\<rfloor> \<longrightarrow> \ e\<^sub>1 = \<lfloor>x2\<rfloor> \<longrightarrow> x2 \<inter> x2a \<subseteq> dom b \<union> x2a
A total of 12 subgoals...
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (11 subgoals):
 1. \<And>E e a b e' aa ba es x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; dom ba \<union> x2a = x2; \ e = \<lfloor>x2c\<rfloor>; dom b \<union> x2c = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \s es = \<lfloor>x2\<rfloor> \<longrightarrow> dom b \<subseteq> dom ba \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom ba \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom ba \<union> (x2a \<union> x2)
 2. \<And>E es a b es' aa ba x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; P,E \<turnstile> \<langle>es,(a, b)\<rangle> [\<rightarrow>] \<langle>es',(aa, ba)\<rangle>; \s es' = \<lfloor>x2a\<rfloor>; dom ba \<union> x2a = x2; \s es = \<lfloor>x2c\<rfloor>; dom b \<union> x2c = x2b\<rbrakk> \<Longrightarrow> dom b \<subseteq> x2 \<and> x2c \<subseteq> x2
 3. \<And>E V T e h l e' h' l' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; l' V = None; \<not> assigned V e; P,E(V \<mapsto> T) \<turnstile> \<langle>e,(h, l(V := None))\<rangle> \<rightarrow> \<langle>e',(h', l')\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; dom l' \<union> x2a = x2; \ e = \<lfloor>x2c\<rfloor>; dom l - {V} \<union> x2c = x2b\<rbrakk> \<Longrightarrow> (l V = None \<longrightarrow> dom l \<subseteq> dom l' - {V} \<union> (x2a - {V}) \<and> x2c - {V} \<subseteq> dom l' - {V} \<union> (x2a - {V})) \<and> ((\<exists>y. l V = \<lfloor>y\<rfloor>) \<longrightarrow> dom l \<subseteq> insert V (dom l' \<union> (x2a - {V})) \<and> x2c - {V} \<subseteq> insert V (dom l' \<union> (x2a - {V})))
 4. \<And>E V T e h l e' h' l' v x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; l' V = \<lfloor>v\<rfloor>; \<not> assigned V e; P,E(V \<mapsto> T) \<turnstile> \<langle>e,(h, l(V := None))\<rangle> \<rightarrow> \<langle>e',(h', l')\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; dom l' \<union> x2a = x2; \ e = \<lfloor>x2c\<rfloor>; dom l - {V} \<union> x2c = x2b\<rbrakk> \<Longrightarrow> (l V = None \<longrightarrow> dom l \<subseteq> dom l' - {V} \<union> (x2a - {V}) \<and> x2c - {V} \<subseteq> dom l' - {V} \<union> (x2a - {V})) \<and> ((\<exists>y. l V = \<lfloor>y\<rfloor>) \<longrightarrow> dom l \<subseteq> insert V (dom l' \<union> (x2a - {V})) \<and> x2c - {V} \<subseteq> insert V (dom l' \<union> (x2a - {V})))
 5. \<And>E V T e h l v' e' h' l' v'' v x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; l' V = \<lfloor>v''\<rfloor>; P \<turnstile> T casts v to v' ; P,E(V \<mapsto> T) \<turnstile> \<langle>e,(h, l(V \<mapsto> v'))\<rangle> \<rightarrow> \<langle>e',(h', l')\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; dom l' \<union> x2a = x2; \ e = \<lfloor>x2c\<rfloor>; insert V (dom l \<union> x2c) = x2b\<rbrakk> \<Longrightarrow> (l V = None \<longrightarrow> dom l \<subseteq> dom l' - {V} \<union> (x2a - {V}) \<and> x2c - {V} \<subseteq> dom l' - {V} \<union> (x2a - {V})) \<and> ((\<exists>y. l V = \<lfloor>y\<rfloor>) \<longrightarrow> dom l \<subseteq> insert V (dom l' \<union> (x2a - {V})) \<and> x2c - {V} \<subseteq> insert V (dom l' \<union> (x2a - {V})))
 6. \<And>E e a b e' aa ba e\<^sub>2 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; dom ba \<union> x2a = x2; \ e = \<lfloor>x2c\<rfloor>; dom b \<union> x2c = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e\<^sub>2 = \<lfloor>x2\<rfloor> \<longrightarrow> dom b \<subseteq> dom ba \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom ba \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom ba \<union> (x2a \<union> x2)
 7. \<And>E e a b e' aa ba e\<^sub>1 e\<^sub>2 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; dom ba \<union> x2a = x2; \ e = \<lfloor>x2c\<rfloor>; dom b \<union> x2c = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. (\ e\<^sub>2 = None \<longrightarrow> x2c = x2 \<longrightarrow> (\<forall>x2b. \ e\<^sub>1 = \<lfloor>x2b\<rfloor> \<longrightarrow> dom b \<subseteq> dom ba \<union> (x2a \<union> x2b) \<and> x2 \<subseteq> dom ba \<union> (x2a \<union> x2b) \<and> x2b \<subseteq> dom ba \<union> (x2a \<union> x2b))) \<and> (\<forall>x2b. \ e\<^sub>2 = \<lfloor>x2b\<rfloor> \<longrightarrow> x2c = x2 \<longrightarrow> (\ e\<^sub>1 = None \<longrightarrow> dom b \<subseteq> dom ba \<union> (x2a \<union> x2b) \<and> x2 \<subseteq> dom ba \<union> (x2a \<union> x2b) \<and> x2b \<subseteq> dom ba \<union> (x2a \<union> x2b)) \<and> (\<forall>x2c. \ e\<^sub>1 = \<lfloor>x2c\<rfloor> \<longrightarrow> dom b \<subseteq> dom ba \<union> (x2a \<union> x2c \<inter> x2b) \<and> x2 \<subseteq> dom ba \<union> (x2a \<union> x2c \<inter> x2b) \<and> x2c \<inter> x2b \<subseteq> dom ba \<union> (x2a \<union> x2c \<inter> x2b)))
 8. \<And>e\<^sub>1 e\<^sub>2 b. \<forall>x2 x2a. \ e\<^sub>2 = \<lfloor>x2a\<rfloor> \<longrightarrow> \ e\<^sub>1 = \<lfloor>x2\<rfloor> \<longrightarrow> x2 \<inter> x2a \<subseteq> dom b \<union> x2
 9. \<And>e\<^sub>1 e\<^sub>2 b. \<forall>x2 x2a. \ e\<^sub>2 = \<lfloor>x2a\<rfloor> \<longrightarrow> \ e\<^sub>1 = \<lfloor>x2\<rfloor> \<longrightarrow> x2 \<inter> x2a \<subseteq> dom b \<union> x2a
 10. \<And>E e a b e' aa ba es x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; dom ba \<union> x2a = x2; \ e = \<lfloor>x2c\<rfloor>; dom b \<union> x2c = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \s es = \<lfloor>x2\<rfloor> \<longrightarrow> dom b \<subseteq> dom ba \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom ba \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom ba \<union> (x2a \<union> x2)
A total of 11 subgoals...
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (10 subgoals):
 1. \<And>E es a b es' aa ba x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; P,E \<turnstile> \<langle>es,(a, b)\<rangle> [\<rightarrow>] \<langle>es',(aa, ba)\<rangle>; \s es' = \<lfloor>x2a\<rfloor>; dom ba \<union> x2a = x2; \s es = \<lfloor>x2c\<rfloor>; dom b \<union> x2c = x2b\<rbrakk> \<Longrightarrow> dom b \<subseteq> x2 \<and> x2c \<subseteq> x2
 2. \<And>E V T e h l e' h' l' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; l' V = None; \<not> assigned V e; P,E(V \<mapsto> T) \<turnstile> \<langle>e,(h, l(V := None))\<rangle> \<rightarrow> \<langle>e',(h', l')\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; dom l' \<union> x2a = x2; \ e = \<lfloor>x2c\<rfloor>; dom l - {V} \<union> x2c = x2b\<rbrakk> \<Longrightarrow> (l V = None \<longrightarrow> dom l \<subseteq> dom l' - {V} \<union> (x2a - {V}) \<and> x2c - {V} \<subseteq> dom l' - {V} \<union> (x2a - {V})) \<and> ((\<exists>y. l V = \<lfloor>y\<rfloor>) \<longrightarrow> dom l \<subseteq> insert V (dom l' \<union> (x2a - {V})) \<and> x2c - {V} \<subseteq> insert V (dom l' \<union> (x2a - {V})))
 3. \<And>E V T e h l e' h' l' v x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; l' V = \<lfloor>v\<rfloor>; \<not> assigned V e; P,E(V \<mapsto> T) \<turnstile> \<langle>e,(h, l(V := None))\<rangle> \<rightarrow> \<langle>e',(h', l')\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; dom l' \<union> x2a = x2; \ e = \<lfloor>x2c\<rfloor>; dom l - {V} \<union> x2c = x2b\<rbrakk> \<Longrightarrow> (l V = None \<longrightarrow> dom l \<subseteq> dom l' - {V} \<union> (x2a - {V}) \<and> x2c - {V} \<subseteq> dom l' - {V} \<union> (x2a - {V})) \<and> ((\<exists>y. l V = \<lfloor>y\<rfloor>) \<longrightarrow> dom l \<subseteq> insert V (dom l' \<union> (x2a - {V})) \<and> x2c - {V} \<subseteq> insert V (dom l' \<union> (x2a - {V})))
 4. \<And>E V T e h l v' e' h' l' v'' v x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; l' V = \<lfloor>v''\<rfloor>; P \<turnstile> T casts v to v' ; P,E(V \<mapsto> T) \<turnstile> \<langle>e,(h, l(V \<mapsto> v'))\<rangle> \<rightarrow> \<langle>e',(h', l')\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; dom l' \<union> x2a = x2; \ e = \<lfloor>x2c\<rfloor>; insert V (dom l \<union> x2c) = x2b\<rbrakk> \<Longrightarrow> (l V = None \<longrightarrow> dom l \<subseteq> dom l' - {V} \<union> (x2a - {V}) \<and> x2c - {V} \<subseteq> dom l' - {V} \<union> (x2a - {V})) \<and> ((\<exists>y. l V = \<lfloor>y\<rfloor>) \<longrightarrow> dom l \<subseteq> insert V (dom l' \<union> (x2a - {V})) \<and> x2c - {V} \<subseteq> insert V (dom l' \<union> (x2a - {V})))
 5. \<And>E e a b e' aa ba e\<^sub>2 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; dom ba \<union> x2a = x2; \ e = \<lfloor>x2c\<rfloor>; dom b \<union> x2c = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e\<^sub>2 = \<lfloor>x2\<rfloor> \<longrightarrow> dom b \<subseteq> dom ba \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom ba \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom ba \<union> (x2a \<union> x2)
 6. \<And>E e a b e' aa ba e\<^sub>1 e\<^sub>2 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; dom ba \<union> x2a = x2; \ e = \<lfloor>x2c\<rfloor>; dom b \<union> x2c = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. (\ e\<^sub>2 = None \<longrightarrow> x2c = x2 \<longrightarrow> (\<forall>x2b. \ e\<^sub>1 = \<lfloor>x2b\<rfloor> \<longrightarrow> dom b \<subseteq> dom ba \<union> (x2a \<union> x2b) \<and> x2 \<subseteq> dom ba \<union> (x2a \<union> x2b) \<and> x2b \<subseteq> dom ba \<union> (x2a \<union> x2b))) \<and> (\<forall>x2b. \ e\<^sub>2 = \<lfloor>x2b\<rfloor> \<longrightarrow> x2c = x2 \<longrightarrow> (\ e\<^sub>1 = None \<longrightarrow> dom b \<subseteq> dom ba \<union> (x2a \<union> x2b) \<and> x2 \<subseteq> dom ba \<union> (x2a \<union> x2b) \<and> x2b \<subseteq> dom ba \<union> (x2a \<union> x2b)) \<and> (\<forall>x2c. \ e\<^sub>1 = \<lfloor>x2c\<rfloor> \<longrightarrow> dom b \<subseteq> dom ba \<union> (x2a \<union> x2c \<inter> x2b) \<and> x2 \<subseteq> dom ba \<union> (x2a \<union> x2c \<inter> x2b) \<and> x2c \<inter> x2b \<subseteq> dom ba \<union> (x2a \<union> x2c \<inter> x2b)))
 7. \<And>e\<^sub>1 e\<^sub>2 b. \<forall>x2 x2a. \ e\<^sub>2 = \<lfloor>x2a\<rfloor> \<longrightarrow> \ e\<^sub>1 = \<lfloor>x2\<rfloor> \<longrightarrow> x2 \<inter> x2a \<subseteq> dom b \<union> x2
 8. \<And>e\<^sub>1 e\<^sub>2 b. \<forall>x2 x2a. \ e\<^sub>2 = \<lfloor>x2a\<rfloor> \<longrightarrow> \ e\<^sub>1 = \<lfloor>x2\<rfloor> \<longrightarrow> x2 \<inter> x2a \<subseteq> dom b \<union> x2a
 9. \<And>E e a b e' aa ba es x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; dom ba \<union> x2a = x2; \ e = \<lfloor>x2c\<rfloor>; dom b \<union> x2c = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \s es = \<lfloor>x2\<rfloor> \<longrightarrow> dom b \<subseteq> dom ba \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom ba \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom ba \<union> (x2a \<union> x2)
 10. \<And>E es a b es' aa ba x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; P,E \<turnstile> \<langle>es,(a, b)\<rangle> [\<rightarrow>] \<langle>es',(aa, ba)\<rangle>; \s es' = \<lfloor>x2a\<rfloor>; dom ba \<union> x2a = x2; \s es = \<lfloor>x2c\<rfloor>; dom b \<union> x2c = x2b\<rbrakk> \<Longrightarrow> dom b \<subseteq> x2 \<and> x2c \<subseteq> x2
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (9 subgoals):
 1. \<And>E V T e h l e' h' l' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; l' V = None; \<not> assigned V e; P,E(V \<mapsto> T) \<turnstile> \<langle>e,(h, l(V := None))\<rangle> \<rightarrow> \<langle>e',(h', l')\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; dom l' \<union> x2a = x2; \ e = \<lfloor>x2c\<rfloor>; dom l - {V} \<union> x2c = x2b\<rbrakk> \<Longrightarrow> (l V = None \<longrightarrow> dom l \<subseteq> dom l' - {V} \<union> (x2a - {V}) \<and> x2c - {V} \<subseteq> dom l' - {V} \<union> (x2a - {V})) \<and> ((\<exists>y. l V = \<lfloor>y\<rfloor>) \<longrightarrow> dom l \<subseteq> insert V (dom l' \<union> (x2a - {V})) \<and> x2c - {V} \<subseteq> insert V (dom l' \<union> (x2a - {V})))
 2. \<And>E V T e h l e' h' l' v x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; l' V = \<lfloor>v\<rfloor>; \<not> assigned V e; P,E(V \<mapsto> T) \<turnstile> \<langle>e,(h, l(V := None))\<rangle> \<rightarrow> \<langle>e',(h', l')\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; dom l' \<union> x2a = x2; \ e = \<lfloor>x2c\<rfloor>; dom l - {V} \<union> x2c = x2b\<rbrakk> \<Longrightarrow> (l V = None \<longrightarrow> dom l \<subseteq> dom l' - {V} \<union> (x2a - {V}) \<and> x2c - {V} \<subseteq> dom l' - {V} \<union> (x2a - {V})) \<and> ((\<exists>y. l V = \<lfloor>y\<rfloor>) \<longrightarrow> dom l \<subseteq> insert V (dom l' \<union> (x2a - {V})) \<and> x2c - {V} \<subseteq> insert V (dom l' \<union> (x2a - {V})))
 3. \<And>E V T e h l v' e' h' l' v'' v x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; l' V = \<lfloor>v''\<rfloor>; P \<turnstile> T casts v to v' ; P,E(V \<mapsto> T) \<turnstile> \<langle>e,(h, l(V \<mapsto> v'))\<rangle> \<rightarrow> \<langle>e',(h', l')\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; dom l' \<union> x2a = x2; \ e = \<lfloor>x2c\<rfloor>; insert V (dom l \<union> x2c) = x2b\<rbrakk> \<Longrightarrow> (l V = None \<longrightarrow> dom l \<subseteq> dom l' - {V} \<union> (x2a - {V}) \<and> x2c - {V} \<subseteq> dom l' - {V} \<union> (x2a - {V})) \<and> ((\<exists>y. l V = \<lfloor>y\<rfloor>) \<longrightarrow> dom l \<subseteq> insert V (dom l' \<union> (x2a - {V})) \<and> x2c - {V} \<subseteq> insert V (dom l' \<union> (x2a - {V})))
 4. \<And>E e a b e' aa ba e\<^sub>2 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; dom ba \<union> x2a = x2; \ e = \<lfloor>x2c\<rfloor>; dom b \<union> x2c = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e\<^sub>2 = \<lfloor>x2\<rfloor> \<longrightarrow> dom b \<subseteq> dom ba \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom ba \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom ba \<union> (x2a \<union> x2)
 5. \<And>E e a b e' aa ba e\<^sub>1 e\<^sub>2 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; dom ba \<union> x2a = x2; \ e = \<lfloor>x2c\<rfloor>; dom b \<union> x2c = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. (\ e\<^sub>2 = None \<longrightarrow> x2c = x2 \<longrightarrow> (\<forall>x2b. \ e\<^sub>1 = \<lfloor>x2b\<rfloor> \<longrightarrow> dom b \<subseteq> dom ba \<union> (x2a \<union> x2b) \<and> x2 \<subseteq> dom ba \<union> (x2a \<union> x2b) \<and> x2b \<subseteq> dom ba \<union> (x2a \<union> x2b))) \<and> (\<forall>x2b. \ e\<^sub>2 = \<lfloor>x2b\<rfloor> \<longrightarrow> x2c = x2 \<longrightarrow> (\ e\<^sub>1 = None \<longrightarrow> dom b \<subseteq> dom ba \<union> (x2a \<union> x2b) \<and> x2 \<subseteq> dom ba \<union> (x2a \<union> x2b) \<and> x2b \<subseteq> dom ba \<union> (x2a \<union> x2b)) \<and> (\<forall>x2c. \ e\<^sub>1 = \<lfloor>x2c\<rfloor> \<longrightarrow> dom b \<subseteq> dom ba \<union> (x2a \<union> x2c \<inter> x2b) \<and> x2 \<subseteq> dom ba \<union> (x2a \<union> x2c \<inter> x2b) \<and> x2c \<inter> x2b \<subseteq> dom ba \<union> (x2a \<union> x2c \<inter> x2b)))
 6. \<And>e\<^sub>1 e\<^sub>2 b. \<forall>x2 x2a. \ e\<^sub>2 = \<lfloor>x2a\<rfloor> \<longrightarrow> \ e\<^sub>1 = \<lfloor>x2\<rfloor> \<longrightarrow> x2 \<inter> x2a \<subseteq> dom b \<union> x2
 7. \<And>e\<^sub>1 e\<^sub>2 b. \<forall>x2 x2a. \ e\<^sub>2 = \<lfloor>x2a\<rfloor> \<longrightarrow> \ e\<^sub>1 = \<lfloor>x2\<rfloor> \<longrightarrow> x2 \<inter> x2a \<subseteq> dom b \<union> x2a
 8. \<And>E e a b e' aa ba es x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; dom ba \<union> x2a = x2; \ e = \<lfloor>x2c\<rfloor>; dom b \<union> x2c = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \s es = \<lfloor>x2\<rfloor> \<longrightarrow> dom b \<subseteq> dom ba \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom ba \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom ba \<union> (x2a \<union> x2)
 9. \<And>E es a b es' aa ba x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; P,E \<turnstile> \<langle>es,(a, b)\<rangle> [\<rightarrow>] \<langle>es',(aa, ba)\<rangle>; \s es' = \<lfloor>x2a\<rfloor>; dom ba \<union> x2a = x2; \s es = \<lfloor>x2c\<rfloor>; dom b \<union> x2c = x2b\<rbrakk> \<Longrightarrow> dom b \<subseteq> x2 \<and> x2c \<subseteq> x2
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done