[STATEMENT]
lemma red_lA_incr: "extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle> \<Longrightarrow> \<lfloor>dom (lcl s)\<rfloor> \<squnion> \ e \<sqsubseteq>  \<lfloor>dom (lcl s')\<rfloor> \<squnion> \ e'"
  and reds_lA_incr: "extTA,P,t \<turnstile> \<langle>es,s\<rangle> [-ta\<rightarrow>] \<langle>es',s'\<rangle> \<Longrightarrow> \<lfloor>dom (lcl s)\<rfloor> \<squnion> \s es \<sqsubseteq>  \<lfloor>dom (lcl s')\<rfloor> \<squnion> \s es'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle> \<Longrightarrow> \<lfloor>dom (lcl s)\<rfloor> \<squnion> \ e \<sqsubseteq> \<lfloor>dom (lcl s')\<rfloor> \<squnion> \ e') &&& (extTA,P,t \<turnstile> \<langle>es,s\<rangle> [-ta\<rightarrow>] \<langle>es',s'\<rangle> \<Longrightarrow> \<lfloor>dom (lcl s)\<rfloor> \<squnion> \s es \<sqsubseteq> \<lfloor>dom (lcl s')\<rfloor> \<squnion> \s es')
[PROOF STEP]
apply(induct rule:red_reds.inducts)
[PROOF STATE]
proof (prove)
goal (98 subgoals):
 1. \<And>h' a h C l. (h', a) \<in> allocate h (Class_type C) \<Longrightarrow> \<lfloor>dom (lcl (h, l))\<rfloor> \<squnion> \ (new C) \<sqsubseteq> \<lfloor>dom (lcl (h', l))\<rfloor> \<squnion> \ (addr a)
 2. \<And>h C l. allocate h (Class_type C) = {} \<Longrightarrow> \<lfloor>dom (lcl (h, l))\<rfloor> \<squnion> \ (new C) \<sqsubseteq> \<lfloor>dom (lcl (h, l))\<rfloor> \<squnion> \ (Throw (addr_of_sys_xcpt OutOfMemory))
 3. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<lfloor>dom (lcl s)\<rfloor> \<squnion> \ e \<sqsubseteq> \<lfloor>dom (lcl s')\<rfloor> \<squnion> \ e'\<rbrakk> \<Longrightarrow> \<lfloor>dom (lcl s)\<rfloor> \<squnion> \ (newA T\<lfloor>e\<rceil>) \<sqsubseteq> \<lfloor>dom (lcl s')\<rfloor> \<squnion> \ (newA T\<lfloor>e'\<rceil>)
 4. \<And>i h' a h T l. \<lbrakk>0 \<le>s i; (h', a) \<in> allocate h (Array_type T (nat (sint i)))\<rbrakk> \<Longrightarrow> \<lfloor>dom (lcl (h, l))\<rfloor> \<squnion> \ (newA T\<lfloor>Val (Intg i)\<rceil>) \<sqsubseteq> \<lfloor>dom (lcl (h', l))\<rfloor> \<squnion> \ (addr a)
 5. \<And>i T s. i <s 0 \<Longrightarrow> \<lfloor>dom (lcl s)\<rfloor> \<squnion> \ (newA T\<lfloor>Val (Intg i)\<rceil>) \<sqsubseteq> \<lfloor>dom (lcl s)\<rfloor> \<squnion> \ (Throw (addr_of_sys_xcpt NegativeArraySize))
 6. \<And>i h T l. \<lbrakk>0 \<le>s i; allocate h (Array_type T (nat (sint i))) = {}\<rbrakk> \<Longrightarrow> \<lfloor>dom (lcl (h, l))\<rfloor> \<squnion> \ (newA T\<lfloor>Val (Intg i)\<rceil>) \<sqsubseteq> \<lfloor>dom (lcl (h, l))\<rfloor> \<squnion> \ (Throw (addr_of_sys_xcpt OutOfMemory))
 7. \<And>e s ta e' s' C. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<lfloor>dom (lcl s)\<rfloor> \<squnion> \ e \<sqsubseteq> \<lfloor>dom (lcl s')\<rfloor> \<squnion> \ e'\<rbrakk> \<Longrightarrow> \<lfloor>dom (lcl s)\<rfloor> \<squnion> \ (Cast C e) \<sqsubseteq> \<lfloor>dom (lcl s')\<rfloor> \<squnion> \ (Cast C e')
 8. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T\<rbrakk> \<Longrightarrow> \<lfloor>dom (lcl s)\<rfloor> \<squnion> \ (Cast T (Val v)) \<sqsubseteq> \<lfloor>dom (lcl s)\<rfloor> \<squnion> \ (Val v)
 9. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T\<rbrakk> \<Longrightarrow> \<lfloor>dom (lcl s)\<rfloor> \<squnion> \ (Cast T (Val v)) \<sqsubseteq> \<lfloor>dom (lcl s)\<rfloor> \<squnion> \ (Throw (addr_of_sys_xcpt ClassCast))
 10. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<lfloor>dom (lcl s)\<rfloor> \<squnion> \ e \<sqsubseteq> \<lfloor>dom (lcl s')\<rfloor> \<squnion> \ e'\<rbrakk> \<Longrightarrow> \<lfloor>dom (lcl s)\<rfloor> \<squnion> \ (e instanceof T) \<sqsubseteq> \<lfloor>dom (lcl s')\<rfloor> \<squnion> \ (e' instanceof T)
A total of 98 subgoals...
[PROOF STEP]
apply(simp_all del:fun_upd_apply add:hyperset_defs)
[PROOF STATE]
proof (prove)
goal (25 subgoals):
 1. \<And>e s ta e' s' e2 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e2 = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2)
 2. \<And>e s ta e' s' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<and> x2c \<subseteq> dom (lcl s') \<union> x2a
 3. \<And>e s ta e' s' V x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> dom (lcl s) \<subseteq> insert V (dom (lcl s') \<union> x2a) \<and> x2c \<subseteq> insert V (dom (lcl s') \<union> x2a)
 4. \<And>a s ta a' s' i x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>a,s\<rangle> -ta\<rightarrow> \<langle>a',s'\<rangle>; \ a' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ a = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ i = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2)
 5. \<And>i s ta i' s' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>i,s\<rangle> -ta\<rightarrow> \<langle>i',s'\<rangle>; \ i' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ i = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<and> x2c \<subseteq> dom (lcl s') \<union> x2a
 6. \<And>a s ta a' s' i e x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>a,s\<rangle> -ta\<rightarrow> \<langle>a',s'\<rangle>; \ a' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ a = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ i = \<lfloor>x2\<rfloor> \<longrightarrow> (\<forall>x2b. \ e = \<lfloor>x2b\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2b \<union> (x2a \<union> x2)) \<and> x2b \<subseteq> dom (lcl s') \<union> (x2b \<union> (x2a \<union> x2)) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2b \<union> (x2a \<union> x2)) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2b \<union> (x2a \<union> x2)))
 7. \<And>i s ta i' s' e x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>i,s\<rangle> -ta\<rightarrow> \<langle>i',s'\<rangle>; \ i' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ i = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2 \<union> x2a) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2 \<union> x2a) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2 \<union> x2a)
 8. \<And>e s ta e' s' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<and> x2c \<subseteq> dom (lcl s') \<union> x2a
 9. \<And>e s ta e' s' e2 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e2 = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2)
 10. \<And>e s ta e' s' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<and> x2c \<subseteq> dom (lcl s') \<union> x2a
A total of 25 subgoals...
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (24 subgoals):
 1. \<And>e s ta e' s' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<and> x2c \<subseteq> dom (lcl s') \<union> x2a
 2. \<And>e s ta e' s' V x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> dom (lcl s) \<subseteq> insert V (dom (lcl s') \<union> x2a) \<and> x2c \<subseteq> insert V (dom (lcl s') \<union> x2a)
 3. \<And>a s ta a' s' i x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>a,s\<rangle> -ta\<rightarrow> \<langle>a',s'\<rangle>; \ a' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ a = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ i = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2)
 4. \<And>i s ta i' s' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>i,s\<rangle> -ta\<rightarrow> \<langle>i',s'\<rangle>; \ i' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ i = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<and> x2c \<subseteq> dom (lcl s') \<union> x2a
 5. \<And>a s ta a' s' i e x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>a,s\<rangle> -ta\<rightarrow> \<langle>a',s'\<rangle>; \ a' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ a = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ i = \<lfloor>x2\<rfloor> \<longrightarrow> (\<forall>x2b. \ e = \<lfloor>x2b\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2b \<union> (x2a \<union> x2)) \<and> x2b \<subseteq> dom (lcl s') \<union> (x2b \<union> (x2a \<union> x2)) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2b \<union> (x2a \<union> x2)) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2b \<union> (x2a \<union> x2)))
 6. \<And>i s ta i' s' e x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>i,s\<rangle> -ta\<rightarrow> \<langle>i',s'\<rangle>; \ i' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ i = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2 \<union> x2a) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2 \<union> x2a) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2 \<union> x2a)
 7. \<And>e s ta e' s' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<and> x2c \<subseteq> dom (lcl s') \<union> x2a
 8. \<And>e s ta e' s' e2 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e2 = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2)
 9. \<And>e s ta e' s' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<and> x2c \<subseteq> dom (lcl s') \<union> x2a
 10. \<And>e s ta e' s' e2 e3 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e2 = \<lfloor>x2\<rfloor> \<longrightarrow> (\<forall>x2b. \ e3 = \<lfloor>x2b\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2b \<union> (x2a \<union> x2)) \<and> x2b \<subseteq> dom (lcl s') \<union> (x2b \<union> (x2a \<union> x2)) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2b \<union> (x2a \<union> x2)) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2b \<union> (x2a \<union> x2)))
A total of 24 subgoals...
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (23 subgoals):
 1. \<And>e s ta e' s' V x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> dom (lcl s) \<subseteq> insert V (dom (lcl s') \<union> x2a) \<and> x2c \<subseteq> insert V (dom (lcl s') \<union> x2a)
 2. \<And>a s ta a' s' i x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>a,s\<rangle> -ta\<rightarrow> \<langle>a',s'\<rangle>; \ a' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ a = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ i = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2)
 3. \<And>i s ta i' s' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>i,s\<rangle> -ta\<rightarrow> \<langle>i',s'\<rangle>; \ i' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ i = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<and> x2c \<subseteq> dom (lcl s') \<union> x2a
 4. \<And>a s ta a' s' i e x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>a,s\<rangle> -ta\<rightarrow> \<langle>a',s'\<rangle>; \ a' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ a = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ i = \<lfloor>x2\<rfloor> \<longrightarrow> (\<forall>x2b. \ e = \<lfloor>x2b\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2b \<union> (x2a \<union> x2)) \<and> x2b \<subseteq> dom (lcl s') \<union> (x2b \<union> (x2a \<union> x2)) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2b \<union> (x2a \<union> x2)) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2b \<union> (x2a \<union> x2)))
 5. \<And>i s ta i' s' e x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>i,s\<rangle> -ta\<rightarrow> \<langle>i',s'\<rangle>; \ i' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ i = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2 \<union> x2a) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2 \<union> x2a) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2 \<union> x2a)
 6. \<And>e s ta e' s' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<and> x2c \<subseteq> dom (lcl s') \<union> x2a
 7. \<And>e s ta e' s' e2 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e2 = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2)
 8. \<And>e s ta e' s' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<and> x2c \<subseteq> dom (lcl s') \<union> x2a
 9. \<And>e s ta e' s' e2 e3 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e2 = \<lfloor>x2\<rfloor> \<longrightarrow> (\<forall>x2b. \ e3 = \<lfloor>x2b\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2b \<union> (x2a \<union> x2)) \<and> x2b \<subseteq> dom (lcl s') \<union> (x2b \<union> (x2a \<union> x2)) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2b \<union> (x2a \<union> x2)) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2b \<union> (x2a \<union> x2)))
 10. \<And>e s ta e' s' e3 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e3 = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2 \<union> x2a) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2 \<union> x2a) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2 \<union> x2a)
A total of 23 subgoals...
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (22 subgoals):
 1. \<And>a s ta a' s' i x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>a,s\<rangle> -ta\<rightarrow> \<langle>a',s'\<rangle>; \ a' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ a = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ i = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2)
 2. \<And>i s ta i' s' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>i,s\<rangle> -ta\<rightarrow> \<langle>i',s'\<rangle>; \ i' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ i = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<and> x2c \<subseteq> dom (lcl s') \<union> x2a
 3. \<And>a s ta a' s' i e x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>a,s\<rangle> -ta\<rightarrow> \<langle>a',s'\<rangle>; \ a' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ a = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ i = \<lfloor>x2\<rfloor> \<longrightarrow> (\<forall>x2b. \ e = \<lfloor>x2b\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2b \<union> (x2a \<union> x2)) \<and> x2b \<subseteq> dom (lcl s') \<union> (x2b \<union> (x2a \<union> x2)) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2b \<union> (x2a \<union> x2)) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2b \<union> (x2a \<union> x2)))
 4. \<And>i s ta i' s' e x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>i,s\<rangle> -ta\<rightarrow> \<langle>i',s'\<rangle>; \ i' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ i = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2 \<union> x2a) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2 \<union> x2a) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2 \<union> x2a)
 5. \<And>e s ta e' s' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<and> x2c \<subseteq> dom (lcl s') \<union> x2a
 6. \<And>e s ta e' s' e2 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e2 = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2)
 7. \<And>e s ta e' s' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<and> x2c \<subseteq> dom (lcl s') \<union> x2a
 8. \<And>e s ta e' s' e2 e3 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e2 = \<lfloor>x2\<rfloor> \<longrightarrow> (\<forall>x2b. \ e3 = \<lfloor>x2b\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2b \<union> (x2a \<union> x2)) \<and> x2b \<subseteq> dom (lcl s') \<union> (x2b \<union> (x2a \<union> x2)) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2b \<union> (x2a \<union> x2)) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2b \<union> (x2a \<union> x2)))
 9. \<And>e s ta e' s' e3 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e3 = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2 \<union> x2a) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2 \<union> x2a) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2 \<union> x2a)
 10. \<And>e s ta e' s' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<and> x2c \<subseteq> dom (lcl s') \<union> x2a
A total of 22 subgoals...
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (21 subgoals):
 1. \<And>i s ta i' s' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>i,s\<rangle> -ta\<rightarrow> \<langle>i',s'\<rangle>; \ i' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ i = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<and> x2c \<subseteq> dom (lcl s') \<union> x2a
 2. \<And>a s ta a' s' i e x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>a,s\<rangle> -ta\<rightarrow> \<langle>a',s'\<rangle>; \ a' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ a = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ i = \<lfloor>x2\<rfloor> \<longrightarrow> (\<forall>x2b. \ e = \<lfloor>x2b\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2b \<union> (x2a \<union> x2)) \<and> x2b \<subseteq> dom (lcl s') \<union> (x2b \<union> (x2a \<union> x2)) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2b \<union> (x2a \<union> x2)) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2b \<union> (x2a \<union> x2)))
 3. \<And>i s ta i' s' e x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>i,s\<rangle> -ta\<rightarrow> \<langle>i',s'\<rangle>; \ i' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ i = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2 \<union> x2a) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2 \<union> x2a) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2 \<union> x2a)
 4. \<And>e s ta e' s' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<and> x2c \<subseteq> dom (lcl s') \<union> x2a
 5. \<And>e s ta e' s' e2 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e2 = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2)
 6. \<And>e s ta e' s' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<and> x2c \<subseteq> dom (lcl s') \<union> x2a
 7. \<And>e s ta e' s' e2 e3 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e2 = \<lfloor>x2\<rfloor> \<longrightarrow> (\<forall>x2b. \ e3 = \<lfloor>x2b\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2b \<union> (x2a \<union> x2)) \<and> x2b \<subseteq> dom (lcl s') \<union> (x2b \<union> (x2a \<union> x2)) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2b \<union> (x2a \<union> x2)) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2b \<union> (x2a \<union> x2)))
 8. \<And>e s ta e' s' e3 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e3 = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2 \<union> x2a) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2 \<union> x2a) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2 \<union> x2a)
 9. \<And>e s ta e' s' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<and> x2c \<subseteq> dom (lcl s') \<union> x2a
 10. \<And>e s ta e' s' es x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \s es = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2)
A total of 21 subgoals...
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (20 subgoals):
 1. \<And>a s ta a' s' i e x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>a,s\<rangle> -ta\<rightarrow> \<langle>a',s'\<rangle>; \ a' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ a = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ i = \<lfloor>x2\<rfloor> \<longrightarrow> (\<forall>x2b. \ e = \<lfloor>x2b\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2b \<union> (x2a \<union> x2)) \<and> x2b \<subseteq> dom (lcl s') \<union> (x2b \<union> (x2a \<union> x2)) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2b \<union> (x2a \<union> x2)) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2b \<union> (x2a \<union> x2)))
 2. \<And>i s ta i' s' e x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>i,s\<rangle> -ta\<rightarrow> \<langle>i',s'\<rangle>; \ i' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ i = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2 \<union> x2a) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2 \<union> x2a) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2 \<union> x2a)
 3. \<And>e s ta e' s' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<and> x2c \<subseteq> dom (lcl s') \<union> x2a
 4. \<And>e s ta e' s' e2 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e2 = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2)
 5. \<And>e s ta e' s' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<and> x2c \<subseteq> dom (lcl s') \<union> x2a
 6. \<And>e s ta e' s' e2 e3 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e2 = \<lfloor>x2\<rfloor> \<longrightarrow> (\<forall>x2b. \ e3 = \<lfloor>x2b\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2b \<union> (x2a \<union> x2)) \<and> x2b \<subseteq> dom (lcl s') \<union> (x2b \<union> (x2a \<union> x2)) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2b \<union> (x2a \<union> x2)) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2b \<union> (x2a \<union> x2)))
 7. \<And>e s ta e' s' e3 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e3 = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2 \<union> x2a) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2 \<union> x2a) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2 \<union> x2a)
 8. \<And>e s ta e' s' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<and> x2c \<subseteq> dom (lcl s') \<union> x2a
 9. \<And>e s ta e' s' es x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \s es = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2)
 10. \<And>es s ta es' s' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>es,s\<rangle> [-ta\<rightarrow>] \<langle>es',s'\<rangle>; \s es' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \s es = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<and> x2c \<subseteq> dom (lcl s') \<union> x2a
A total of 20 subgoals...
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (19 subgoals):
 1. \<And>i s ta i' s' e x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>i,s\<rangle> -ta\<rightarrow> \<langle>i',s'\<rangle>; \ i' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ i = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2 \<union> x2a) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2 \<union> x2a) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2 \<union> x2a)
 2. \<And>e s ta e' s' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<and> x2c \<subseteq> dom (lcl s') \<union> x2a
 3. \<And>e s ta e' s' e2 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e2 = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2)
 4. \<And>e s ta e' s' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<and> x2c \<subseteq> dom (lcl s') \<union> x2a
 5. \<And>e s ta e' s' e2 e3 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e2 = \<lfloor>x2\<rfloor> \<longrightarrow> (\<forall>x2b. \ e3 = \<lfloor>x2b\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2b \<union> (x2a \<union> x2)) \<and> x2b \<subseteq> dom (lcl s') \<union> (x2b \<union> (x2a \<union> x2)) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2b \<union> (x2a \<union> x2)) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2b \<union> (x2a \<union> x2)))
 6. \<And>e s ta e' s' e3 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e3 = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2 \<union> x2a) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2 \<union> x2a) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2 \<union> x2a)
 7. \<And>e s ta e' s' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<and> x2c \<subseteq> dom (lcl s') \<union> x2a
 8. \<And>e s ta e' s' es x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \s es = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2)
 9. \<And>es s ta es' s' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>es,s\<rangle> [-ta\<rightarrow>] \<langle>es',s'\<rangle>; \s es' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \s es = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<and> x2c \<subseteq> dom (lcl s') \<union> x2a
 10. \<And>e h l V vo ta e' h' l' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,(h, l(V := vo))\<rangle> -ta\<rightarrow> \<langle>e',(h', l')\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom l' = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> (if vo = None then dom l - {V} else insert V (dom l)) = x2b\<rbrakk> \<Longrightarrow> (l V = None \<longrightarrow> dom l \<subseteq> x2a - {V} \<union> (dom l' - {V}) \<and> x2c - {V} \<subseteq> x2a - {V} \<union> (dom l' - {V})) \<and> ((\<exists>y. l V = \<lfloor>y\<rfloor>) \<longrightarrow> dom l \<subseteq> insert V (x2a - {V} \<union> dom l') \<and> x2c - {V} \<subseteq> insert V (x2a - {V} \<union> dom l'))
A total of 19 subgoals...
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (18 subgoals):
 1. \<And>e s ta e' s' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<and> x2c \<subseteq> dom (lcl s') \<union> x2a
 2. \<And>e s ta e' s' e2 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e2 = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2)
 3. \<And>e s ta e' s' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<and> x2c \<subseteq> dom (lcl s') \<union> x2a
 4. \<And>e s ta e' s' e2 e3 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e2 = \<lfloor>x2\<rfloor> \<longrightarrow> (\<forall>x2b. \ e3 = \<lfloor>x2b\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2b \<union> (x2a \<union> x2)) \<and> x2b \<subseteq> dom (lcl s') \<union> (x2b \<union> (x2a \<union> x2)) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2b \<union> (x2a \<union> x2)) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2b \<union> (x2a \<union> x2)))
 5. \<And>e s ta e' s' e3 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e3 = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2 \<union> x2a) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2 \<union> x2a) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2 \<union> x2a)
 6. \<And>e s ta e' s' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<and> x2c \<subseteq> dom (lcl s') \<union> x2a
 7. \<And>e s ta e' s' es x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \s es = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2)
 8. \<And>es s ta es' s' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>es,s\<rangle> [-ta\<rightarrow>] \<langle>es',s'\<rangle>; \s es' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \s es = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<and> x2c \<subseteq> dom (lcl s') \<union> x2a
 9. \<And>e h l V vo ta e' h' l' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,(h, l(V := vo))\<rangle> -ta\<rightarrow> \<langle>e',(h', l')\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom l' = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> (if vo = None then dom l - {V} else insert V (dom l)) = x2b\<rbrakk> \<Longrightarrow> (l V = None \<longrightarrow> dom l \<subseteq> x2a - {V} \<union> (dom l' - {V}) \<and> x2c - {V} \<subseteq> x2a - {V} \<union> (dom l' - {V})) \<and> ((\<exists>y. l V = \<lfloor>y\<rfloor>) \<longrightarrow> dom l \<subseteq> insert V (x2a - {V} \<union> dom l') \<and> x2c - {V} \<subseteq> insert V (x2a - {V} \<union> dom l'))
 10. \<And>o' s ta o'' s' e x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>o',s\<rangle> -ta\<rightarrow> \<langle>o'',s'\<rangle>; \ o'' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ o' = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2)
A total of 18 subgoals...
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (17 subgoals):
 1. \<And>e s ta e' s' e2 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e2 = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2)
 2. \<And>e s ta e' s' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<and> x2c \<subseteq> dom (lcl s') \<union> x2a
 3. \<And>e s ta e' s' e2 e3 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e2 = \<lfloor>x2\<rfloor> \<longrightarrow> (\<forall>x2b. \ e3 = \<lfloor>x2b\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2b \<union> (x2a \<union> x2)) \<and> x2b \<subseteq> dom (lcl s') \<union> (x2b \<union> (x2a \<union> x2)) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2b \<union> (x2a \<union> x2)) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2b \<union> (x2a \<union> x2)))
 4. \<And>e s ta e' s' e3 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e3 = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2 \<union> x2a) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2 \<union> x2a) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2 \<union> x2a)
 5. \<And>e s ta e' s' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<and> x2c \<subseteq> dom (lcl s') \<union> x2a
 6. \<And>e s ta e' s' es x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \s es = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2)
 7. \<And>es s ta es' s' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>es,s\<rangle> [-ta\<rightarrow>] \<langle>es',s'\<rangle>; \s es' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \s es = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<and> x2c \<subseteq> dom (lcl s') \<union> x2a
 8. \<And>e h l V vo ta e' h' l' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,(h, l(V := vo))\<rangle> -ta\<rightarrow> \<langle>e',(h', l')\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom l' = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> (if vo = None then dom l - {V} else insert V (dom l)) = x2b\<rbrakk> \<Longrightarrow> (l V = None \<longrightarrow> dom l \<subseteq> x2a - {V} \<union> (dom l' - {V}) \<and> x2c - {V} \<subseteq> x2a - {V} \<union> (dom l' - {V})) \<and> ((\<exists>y. l V = \<lfloor>y\<rfloor>) \<longrightarrow> dom l \<subseteq> insert V (x2a - {V} \<union> dom l') \<and> x2c - {V} \<subseteq> insert V (x2a - {V} \<union> dom l'))
 9. \<And>o' s ta o'' s' e x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>o',s\<rangle> -ta\<rightarrow> \<langle>o'',s'\<rangle>; \ o'' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ o' = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2)
 10. \<And>e s ta e' s' e2 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e2 = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2)
A total of 17 subgoals...
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (16 subgoals):
 1. \<And>e s ta e' s' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<and> x2c \<subseteq> dom (lcl s') \<union> x2a
 2. \<And>e s ta e' s' e2 e3 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e2 = \<lfloor>x2\<rfloor> \<longrightarrow> (\<forall>x2b. \ e3 = \<lfloor>x2b\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2b \<union> (x2a \<union> x2)) \<and> x2b \<subseteq> dom (lcl s') \<union> (x2b \<union> (x2a \<union> x2)) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2b \<union> (x2a \<union> x2)) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2b \<union> (x2a \<union> x2)))
 3. \<And>e s ta e' s' e3 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e3 = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2 \<union> x2a) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2 \<union> x2a) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2 \<union> x2a)
 4. \<And>e s ta e' s' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<and> x2c \<subseteq> dom (lcl s') \<union> x2a
 5. \<And>e s ta e' s' es x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \s es = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2)
 6. \<And>es s ta es' s' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>es,s\<rangle> [-ta\<rightarrow>] \<langle>es',s'\<rangle>; \s es' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \s es = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<and> x2c \<subseteq> dom (lcl s') \<union> x2a
 7. \<And>e h l V vo ta e' h' l' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,(h, l(V := vo))\<rangle> -ta\<rightarrow> \<langle>e',(h', l')\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom l' = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> (if vo = None then dom l - {V} else insert V (dom l)) = x2b\<rbrakk> \<Longrightarrow> (l V = None \<longrightarrow> dom l \<subseteq> x2a - {V} \<union> (dom l' - {V}) \<and> x2c - {V} \<subseteq> x2a - {V} \<union> (dom l' - {V})) \<and> ((\<exists>y. l V = \<lfloor>y\<rfloor>) \<longrightarrow> dom l \<subseteq> insert V (x2a - {V} \<union> dom l') \<and> x2c - {V} \<subseteq> insert V (x2a - {V} \<union> dom l'))
 8. \<And>o' s ta o'' s' e x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>o',s\<rangle> -ta\<rightarrow> \<langle>o'',s'\<rangle>; \ o'' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ o' = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2)
 9. \<And>e s ta e' s' e2 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e2 = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2)
 10. \<And>b s ta b' s' e1 e2 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>b,s\<rangle> -ta\<rightarrow> \<langle>b',s'\<rangle>; \ b' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ b = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. (\ e2 = None \<longrightarrow> x2c = x2 \<longrightarrow> (\<forall>x2b. \ e1 = \<lfloor>x2b\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2b) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2b) \<and> x2b \<subseteq> dom (lcl s') \<union> (x2a \<union> x2b))) \<and> (\<forall>x2b. \ e2 = \<lfloor>x2b\<rfloor> \<longrightarrow> x2c = x2 \<longrightarrow> (\ e1 = None \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2b) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2b) \<and> x2b \<subseteq> dom (lcl s') \<union> (x2a \<union> x2b)) \<and> (\<forall>x2c. \ e1 = \<lfloor>x2c\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2c \<inter> x2b) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2c \<inter> x2b) \<and> x2c \<inter> x2b \<subseteq> dom (lcl s') \<union> (x2a \<union> x2c \<inter> x2b)))
A total of 16 subgoals...
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (15 subgoals):
 1. \<And>e s ta e' s' e2 e3 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e2 = \<lfloor>x2\<rfloor> \<longrightarrow> (\<forall>x2b. \ e3 = \<lfloor>x2b\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2b \<union> (x2a \<union> x2)) \<and> x2b \<subseteq> dom (lcl s') \<union> (x2b \<union> (x2a \<union> x2)) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2b \<union> (x2a \<union> x2)) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2b \<union> (x2a \<union> x2)))
 2. \<And>e s ta e' s' e3 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e3 = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2 \<union> x2a) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2 \<union> x2a) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2 \<union> x2a)
 3. \<And>e s ta e' s' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<and> x2c \<subseteq> dom (lcl s') \<union> x2a
 4. \<And>e s ta e' s' es x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \s es = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2)
 5. \<And>es s ta es' s' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>es,s\<rangle> [-ta\<rightarrow>] \<langle>es',s'\<rangle>; \s es' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \s es = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<and> x2c \<subseteq> dom (lcl s') \<union> x2a
 6. \<And>e h l V vo ta e' h' l' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,(h, l(V := vo))\<rangle> -ta\<rightarrow> \<langle>e',(h', l')\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom l' = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> (if vo = None then dom l - {V} else insert V (dom l)) = x2b\<rbrakk> \<Longrightarrow> (l V = None \<longrightarrow> dom l \<subseteq> x2a - {V} \<union> (dom l' - {V}) \<and> x2c - {V} \<subseteq> x2a - {V} \<union> (dom l' - {V})) \<and> ((\<exists>y. l V = \<lfloor>y\<rfloor>) \<longrightarrow> dom l \<subseteq> insert V (x2a - {V} \<union> dom l') \<and> x2c - {V} \<subseteq> insert V (x2a - {V} \<union> dom l'))
 7. \<And>o' s ta o'' s' e x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>o',s\<rangle> -ta\<rightarrow> \<langle>o'',s'\<rangle>; \ o'' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ o' = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2)
 8. \<And>e s ta e' s' e2 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e2 = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2)
 9. \<And>b s ta b' s' e1 e2 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>b,s\<rangle> -ta\<rightarrow> \<langle>b',s'\<rangle>; \ b' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ b = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. (\ e2 = None \<longrightarrow> x2c = x2 \<longrightarrow> (\<forall>x2b. \ e1 = \<lfloor>x2b\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2b) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2b) \<and> x2b \<subseteq> dom (lcl s') \<union> (x2a \<union> x2b))) \<and> (\<forall>x2b. \ e2 = \<lfloor>x2b\<rfloor> \<longrightarrow> x2c = x2 \<longrightarrow> (\ e1 = None \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2b) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2b) \<and> x2b \<subseteq> dom (lcl s') \<union> (x2a \<union> x2b)) \<and> (\<forall>x2c. \ e1 = \<lfloor>x2c\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2c \<inter> x2b) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2c \<inter> x2b) \<and> x2c \<inter> x2b \<subseteq> dom (lcl s') \<union> (x2a \<union> x2c \<inter> x2b)))
 10. \<And>e1 e2 s. \<forall>x2 x2a. \ e2 = \<lfloor>x2a\<rfloor> \<longrightarrow> \ e1 = \<lfloor>x2\<rfloor> \<longrightarrow> x2 \<inter> x2a \<subseteq> x2 \<union> dom (lcl s)
A total of 15 subgoals...
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (14 subgoals):
 1. \<And>e s ta e' s' e3 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e3 = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2 \<union> x2a) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2 \<union> x2a) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2 \<union> x2a)
 2. \<And>e s ta e' s' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<and> x2c \<subseteq> dom (lcl s') \<union> x2a
 3. \<And>e s ta e' s' es x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \s es = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2)
 4. \<And>es s ta es' s' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>es,s\<rangle> [-ta\<rightarrow>] \<langle>es',s'\<rangle>; \s es' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \s es = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<and> x2c \<subseteq> dom (lcl s') \<union> x2a
 5. \<And>e h l V vo ta e' h' l' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,(h, l(V := vo))\<rangle> -ta\<rightarrow> \<langle>e',(h', l')\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom l' = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> (if vo = None then dom l - {V} else insert V (dom l)) = x2b\<rbrakk> \<Longrightarrow> (l V = None \<longrightarrow> dom l \<subseteq> x2a - {V} \<union> (dom l' - {V}) \<and> x2c - {V} \<subseteq> x2a - {V} \<union> (dom l' - {V})) \<and> ((\<exists>y. l V = \<lfloor>y\<rfloor>) \<longrightarrow> dom l \<subseteq> insert V (x2a - {V} \<union> dom l') \<and> x2c - {V} \<subseteq> insert V (x2a - {V} \<union> dom l'))
 6. \<And>o' s ta o'' s' e x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>o',s\<rangle> -ta\<rightarrow> \<langle>o'',s'\<rangle>; \ o'' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ o' = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2)
 7. \<And>e s ta e' s' e2 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e2 = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2)
 8. \<And>b s ta b' s' e1 e2 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>b,s\<rangle> -ta\<rightarrow> \<langle>b',s'\<rangle>; \ b' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ b = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. (\ e2 = None \<longrightarrow> x2c = x2 \<longrightarrow> (\<forall>x2b. \ e1 = \<lfloor>x2b\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2b) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2b) \<and> x2b \<subseteq> dom (lcl s') \<union> (x2a \<union> x2b))) \<and> (\<forall>x2b. \ e2 = \<lfloor>x2b\<rfloor> \<longrightarrow> x2c = x2 \<longrightarrow> (\ e1 = None \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2b) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2b) \<and> x2b \<subseteq> dom (lcl s') \<union> (x2a \<union> x2b)) \<and> (\<forall>x2c. \ e1 = \<lfloor>x2c\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2c \<inter> x2b) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2c \<inter> x2b) \<and> x2c \<inter> x2b \<subseteq> dom (lcl s') \<union> (x2a \<union> x2c \<inter> x2b)))
 9. \<And>e1 e2 s. \<forall>x2 x2a. \ e2 = \<lfloor>x2a\<rfloor> \<longrightarrow> \ e1 = \<lfloor>x2\<rfloor> \<longrightarrow> x2 \<inter> x2a \<subseteq> x2 \<union> dom (lcl s)
 10. \<And>e1 e2 s. \<forall>x2 x2a. \ e2 = \<lfloor>x2a\<rfloor> \<longrightarrow> \ e1 = \<lfloor>x2\<rfloor> \<longrightarrow> x2 \<inter> x2a \<subseteq> x2a \<union> dom (lcl s)
A total of 14 subgoals...
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (13 subgoals):
 1. \<And>e s ta e' s' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<and> x2c \<subseteq> dom (lcl s') \<union> x2a
 2. \<And>e s ta e' s' es x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \s es = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2)
 3. \<And>es s ta es' s' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>es,s\<rangle> [-ta\<rightarrow>] \<langle>es',s'\<rangle>; \s es' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \s es = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<and> x2c \<subseteq> dom (lcl s') \<union> x2a
 4. \<And>e h l V vo ta e' h' l' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,(h, l(V := vo))\<rangle> -ta\<rightarrow> \<langle>e',(h', l')\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom l' = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> (if vo = None then dom l - {V} else insert V (dom l)) = x2b\<rbrakk> \<Longrightarrow> (l V = None \<longrightarrow> dom l \<subseteq> x2a - {V} \<union> (dom l' - {V}) \<and> x2c - {V} \<subseteq> x2a - {V} \<union> (dom l' - {V})) \<and> ((\<exists>y. l V = \<lfloor>y\<rfloor>) \<longrightarrow> dom l \<subseteq> insert V (x2a - {V} \<union> dom l') \<and> x2c - {V} \<subseteq> insert V (x2a - {V} \<union> dom l'))
 5. \<And>o' s ta o'' s' e x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>o',s\<rangle> -ta\<rightarrow> \<langle>o'',s'\<rangle>; \ o'' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ o' = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2)
 6. \<And>e s ta e' s' e2 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e2 = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2)
 7. \<And>b s ta b' s' e1 e2 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>b,s\<rangle> -ta\<rightarrow> \<langle>b',s'\<rangle>; \ b' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ b = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. (\ e2 = None \<longrightarrow> x2c = x2 \<longrightarrow> (\<forall>x2b. \ e1 = \<lfloor>x2b\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2b) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2b) \<and> x2b \<subseteq> dom (lcl s') \<union> (x2a \<union> x2b))) \<and> (\<forall>x2b. \ e2 = \<lfloor>x2b\<rfloor> \<longrightarrow> x2c = x2 \<longrightarrow> (\ e1 = None \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2b) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2b) \<and> x2b \<subseteq> dom (lcl s') \<union> (x2a \<union> x2b)) \<and> (\<forall>x2c. \ e1 = \<lfloor>x2c\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2c \<inter> x2b) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2c \<inter> x2b) \<and> x2c \<inter> x2b \<subseteq> dom (lcl s') \<union> (x2a \<union> x2c \<inter> x2b)))
 8. \<And>e1 e2 s. \<forall>x2 x2a. \ e2 = \<lfloor>x2a\<rfloor> \<longrightarrow> \ e1 = \<lfloor>x2\<rfloor> \<longrightarrow> x2 \<inter> x2a \<subseteq> x2 \<union> dom (lcl s)
 9. \<And>e1 e2 s. \<forall>x2 x2a. \ e2 = \<lfloor>x2a\<rfloor> \<longrightarrow> \ e1 = \<lfloor>x2\<rfloor> \<longrightarrow> x2 \<inter> x2a \<subseteq> x2a \<union> dom (lcl s)
 10. \<And>e s ta e' s' V e2. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = None\<rbrakk> \<Longrightarrow> (\ e = None \<longrightarrow> (\<forall>x2. \ e2 = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2 - {V}))) \<and> (\<forall>x2. \ e = \<lfloor>x2\<rfloor> \<longrightarrow> (\<forall>x2a. \ e2 = \<lfloor>x2a\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a - {V}) \<and> x2 \<inter> (x2a - {V}) \<subseteq> dom (lcl s') \<union> (x2a - {V})))
A total of 13 subgoals...
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (12 subgoals):
 1. \<And>e s ta e' s' es x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \s es = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2)
 2. \<And>es s ta es' s' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>es,s\<rangle> [-ta\<rightarrow>] \<langle>es',s'\<rangle>; \s es' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \s es = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<and> x2c \<subseteq> dom (lcl s') \<union> x2a
 3. \<And>e h l V vo ta e' h' l' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,(h, l(V := vo))\<rangle> -ta\<rightarrow> \<langle>e',(h', l')\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom l' = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> (if vo = None then dom l - {V} else insert V (dom l)) = x2b\<rbrakk> \<Longrightarrow> (l V = None \<longrightarrow> dom l \<subseteq> x2a - {V} \<union> (dom l' - {V}) \<and> x2c - {V} \<subseteq> x2a - {V} \<union> (dom l' - {V})) \<and> ((\<exists>y. l V = \<lfloor>y\<rfloor>) \<longrightarrow> dom l \<subseteq> insert V (x2a - {V} \<union> dom l') \<and> x2c - {V} \<subseteq> insert V (x2a - {V} \<union> dom l'))
 4. \<And>o' s ta o'' s' e x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>o',s\<rangle> -ta\<rightarrow> \<langle>o'',s'\<rangle>; \ o'' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ o' = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2)
 5. \<And>e s ta e' s' e2 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e2 = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2)
 6. \<And>b s ta b' s' e1 e2 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>b,s\<rangle> -ta\<rightarrow> \<langle>b',s'\<rangle>; \ b' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ b = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. (\ e2 = None \<longrightarrow> x2c = x2 \<longrightarrow> (\<forall>x2b. \ e1 = \<lfloor>x2b\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2b) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2b) \<and> x2b \<subseteq> dom (lcl s') \<union> (x2a \<union> x2b))) \<and> (\<forall>x2b. \ e2 = \<lfloor>x2b\<rfloor> \<longrightarrow> x2c = x2 \<longrightarrow> (\ e1 = None \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2b) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2b) \<and> x2b \<subseteq> dom (lcl s') \<union> (x2a \<union> x2b)) \<and> (\<forall>x2c. \ e1 = \<lfloor>x2c\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2c \<inter> x2b) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2c \<inter> x2b) \<and> x2c \<inter> x2b \<subseteq> dom (lcl s') \<union> (x2a \<union> x2c \<inter> x2b)))
 7. \<And>e1 e2 s. \<forall>x2 x2a. \ e2 = \<lfloor>x2a\<rfloor> \<longrightarrow> \ e1 = \<lfloor>x2\<rfloor> \<longrightarrow> x2 \<inter> x2a \<subseteq> x2 \<union> dom (lcl s)
 8. \<And>e1 e2 s. \<forall>x2 x2a. \ e2 = \<lfloor>x2a\<rfloor> \<longrightarrow> \ e1 = \<lfloor>x2\<rfloor> \<longrightarrow> x2 \<inter> x2a \<subseteq> x2a \<union> dom (lcl s)
 9. \<And>e s ta e' s' V e2. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = None\<rbrakk> \<Longrightarrow> (\ e = None \<longrightarrow> (\<forall>x2. \ e2 = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2 - {V}))) \<and> (\<forall>x2. \ e = \<lfloor>x2\<rfloor> \<longrightarrow> (\<forall>x2a. \ e2 = \<lfloor>x2a\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a - {V}) \<and> x2 \<inter> (x2a - {V}) \<subseteq> dom (lcl s') \<union> (x2a - {V})))
 10. \<And>e s ta e' s' V e2 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> (\ e2 = None \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<and> x2c \<subseteq> dom (lcl s') \<union> x2a) \<and> (\<forall>x2. \ e2 = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<inter> (x2 - {V}) \<and> x2c \<inter> (x2 - {V}) \<subseteq> dom (lcl s') \<union> x2a \<inter> (x2 - {V}))
A total of 12 subgoals...
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (11 subgoals):
 1. \<And>es s ta es' s' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>es,s\<rangle> [-ta\<rightarrow>] \<langle>es',s'\<rangle>; \s es' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \s es = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<and> x2c \<subseteq> dom (lcl s') \<union> x2a
 2. \<And>e h l V vo ta e' h' l' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,(h, l(V := vo))\<rangle> -ta\<rightarrow> \<langle>e',(h', l')\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom l' = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> (if vo = None then dom l - {V} else insert V (dom l)) = x2b\<rbrakk> \<Longrightarrow> (l V = None \<longrightarrow> dom l \<subseteq> x2a - {V} \<union> (dom l' - {V}) \<and> x2c - {V} \<subseteq> x2a - {V} \<union> (dom l' - {V})) \<and> ((\<exists>y. l V = \<lfloor>y\<rfloor>) \<longrightarrow> dom l \<subseteq> insert V (x2a - {V} \<union> dom l') \<and> x2c - {V} \<subseteq> insert V (x2a - {V} \<union> dom l'))
 3. \<And>o' s ta o'' s' e x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>o',s\<rangle> -ta\<rightarrow> \<langle>o'',s'\<rangle>; \ o'' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ o' = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2)
 4. \<And>e s ta e' s' e2 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e2 = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2)
 5. \<And>b s ta b' s' e1 e2 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>b,s\<rangle> -ta\<rightarrow> \<langle>b',s'\<rangle>; \ b' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ b = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. (\ e2 = None \<longrightarrow> x2c = x2 \<longrightarrow> (\<forall>x2b. \ e1 = \<lfloor>x2b\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2b) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2b) \<and> x2b \<subseteq> dom (lcl s') \<union> (x2a \<union> x2b))) \<and> (\<forall>x2b. \ e2 = \<lfloor>x2b\<rfloor> \<longrightarrow> x2c = x2 \<longrightarrow> (\ e1 = None \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2b) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2b) \<and> x2b \<subseteq> dom (lcl s') \<union> (x2a \<union> x2b)) \<and> (\<forall>x2c. \ e1 = \<lfloor>x2c\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2c \<inter> x2b) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2c \<inter> x2b) \<and> x2c \<inter> x2b \<subseteq> dom (lcl s') \<union> (x2a \<union> x2c \<inter> x2b)))
 6. \<And>e1 e2 s. \<forall>x2 x2a. \ e2 = \<lfloor>x2a\<rfloor> \<longrightarrow> \ e1 = \<lfloor>x2\<rfloor> \<longrightarrow> x2 \<inter> x2a \<subseteq> x2 \<union> dom (lcl s)
 7. \<And>e1 e2 s. \<forall>x2 x2a. \ e2 = \<lfloor>x2a\<rfloor> \<longrightarrow> \ e1 = \<lfloor>x2\<rfloor> \<longrightarrow> x2 \<inter> x2a \<subseteq> x2a \<union> dom (lcl s)
 8. \<And>e s ta e' s' V e2. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = None\<rbrakk> \<Longrightarrow> (\ e = None \<longrightarrow> (\<forall>x2. \ e2 = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2 - {V}))) \<and> (\<forall>x2. \ e = \<lfloor>x2\<rfloor> \<longrightarrow> (\<forall>x2a. \ e2 = \<lfloor>x2a\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a - {V}) \<and> x2 \<inter> (x2a - {V}) \<subseteq> dom (lcl s') \<union> (x2a - {V})))
 9. \<And>e s ta e' s' V e2 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> (\ e2 = None \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<and> x2c \<subseteq> dom (lcl s') \<union> x2a) \<and> (\<forall>x2. \ e2 = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<inter> (x2 - {V}) \<and> x2c \<inter> (x2 - {V}) \<subseteq> dom (lcl s') \<union> x2a \<inter> (x2 - {V}))
 10. \<And>e s ta e' s' es x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \s es = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2)
A total of 11 subgoals...
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (10 subgoals):
 1. \<And>e h l V vo ta e' h' l' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,(h, l(V := vo))\<rangle> -ta\<rightarrow> \<langle>e',(h', l')\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom l' = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> (if vo = None then dom l - {V} else insert V (dom l)) = x2b\<rbrakk> \<Longrightarrow> (l V = None \<longrightarrow> dom l \<subseteq> x2a - {V} \<union> (dom l' - {V}) \<and> x2c - {V} \<subseteq> x2a - {V} \<union> (dom l' - {V})) \<and> ((\<exists>y. l V = \<lfloor>y\<rfloor>) \<longrightarrow> dom l \<subseteq> insert V (x2a - {V} \<union> dom l') \<and> x2c - {V} \<subseteq> insert V (x2a - {V} \<union> dom l'))
 2. \<And>o' s ta o'' s' e x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>o',s\<rangle> -ta\<rightarrow> \<langle>o'',s'\<rangle>; \ o'' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ o' = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2)
 3. \<And>e s ta e' s' e2 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e2 = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2)
 4. \<And>b s ta b' s' e1 e2 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>b,s\<rangle> -ta\<rightarrow> \<langle>b',s'\<rangle>; \ b' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ b = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. (\ e2 = None \<longrightarrow> x2c = x2 \<longrightarrow> (\<forall>x2b. \ e1 = \<lfloor>x2b\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2b) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2b) \<and> x2b \<subseteq> dom (lcl s') \<union> (x2a \<union> x2b))) \<and> (\<forall>x2b. \ e2 = \<lfloor>x2b\<rfloor> \<longrightarrow> x2c = x2 \<longrightarrow> (\ e1 = None \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2b) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2b) \<and> x2b \<subseteq> dom (lcl s') \<union> (x2a \<union> x2b)) \<and> (\<forall>x2c. \ e1 = \<lfloor>x2c\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2c \<inter> x2b) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2c \<inter> x2b) \<and> x2c \<inter> x2b \<subseteq> dom (lcl s') \<union> (x2a \<union> x2c \<inter> x2b)))
 5. \<And>e1 e2 s. \<forall>x2 x2a. \ e2 = \<lfloor>x2a\<rfloor> \<longrightarrow> \ e1 = \<lfloor>x2\<rfloor> \<longrightarrow> x2 \<inter> x2a \<subseteq> x2 \<union> dom (lcl s)
 6. \<And>e1 e2 s. \<forall>x2 x2a. \ e2 = \<lfloor>x2a\<rfloor> \<longrightarrow> \ e1 = \<lfloor>x2\<rfloor> \<longrightarrow> x2 \<inter> x2a \<subseteq> x2a \<union> dom (lcl s)
 7. \<And>e s ta e' s' V e2. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = None\<rbrakk> \<Longrightarrow> (\ e = None \<longrightarrow> (\<forall>x2. \ e2 = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2 - {V}))) \<and> (\<forall>x2. \ e = \<lfloor>x2\<rfloor> \<longrightarrow> (\<forall>x2a. \ e2 = \<lfloor>x2a\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a - {V}) \<and> x2 \<inter> (x2a - {V}) \<subseteq> dom (lcl s') \<union> (x2a - {V})))
 8. \<And>e s ta e' s' V e2 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> (\ e2 = None \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<and> x2c \<subseteq> dom (lcl s') \<union> x2a) \<and> (\<forall>x2. \ e2 = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<inter> (x2 - {V}) \<and> x2c \<inter> (x2 - {V}) \<subseteq> dom (lcl s') \<union> x2a \<inter> (x2 - {V}))
 9. \<And>e s ta e' s' es x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \s es = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2)
 10. \<And>es s ta es' s' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>es,s\<rangle> [-ta\<rightarrow>] \<langle>es',s'\<rangle>; \s es' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \s es = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<and> x2c \<subseteq> dom (lcl s') \<union> x2a
[PROOF STEP]
apply(force split: if_split_asm)
[PROOF STATE]
proof (prove)
goal (9 subgoals):
 1. \<And>o' s ta o'' s' e x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>o',s\<rangle> -ta\<rightarrow> \<langle>o'',s'\<rangle>; \ o'' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ o' = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2)
 2. \<And>e s ta e' s' e2 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e2 = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2)
 3. \<And>b s ta b' s' e1 e2 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>b,s\<rangle> -ta\<rightarrow> \<langle>b',s'\<rangle>; \ b' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ b = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. (\ e2 = None \<longrightarrow> x2c = x2 \<longrightarrow> (\<forall>x2b. \ e1 = \<lfloor>x2b\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2b) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2b) \<and> x2b \<subseteq> dom (lcl s') \<union> (x2a \<union> x2b))) \<and> (\<forall>x2b. \ e2 = \<lfloor>x2b\<rfloor> \<longrightarrow> x2c = x2 \<longrightarrow> (\ e1 = None \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2b) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2b) \<and> x2b \<subseteq> dom (lcl s') \<union> (x2a \<union> x2b)) \<and> (\<forall>x2c. \ e1 = \<lfloor>x2c\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2c \<inter> x2b) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2c \<inter> x2b) \<and> x2c \<inter> x2b \<subseteq> dom (lcl s') \<union> (x2a \<union> x2c \<inter> x2b)))
 4. \<And>e1 e2 s. \<forall>x2 x2a. \ e2 = \<lfloor>x2a\<rfloor> \<longrightarrow> \ e1 = \<lfloor>x2\<rfloor> \<longrightarrow> x2 \<inter> x2a \<subseteq> x2 \<union> dom (lcl s)
 5. \<And>e1 e2 s. \<forall>x2 x2a. \ e2 = \<lfloor>x2a\<rfloor> \<longrightarrow> \ e1 = \<lfloor>x2\<rfloor> \<longrightarrow> x2 \<inter> x2a \<subseteq> x2a \<union> dom (lcl s)
 6. \<And>e s ta e' s' V e2. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = None\<rbrakk> \<Longrightarrow> (\ e = None \<longrightarrow> (\<forall>x2. \ e2 = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2 - {V}))) \<and> (\<forall>x2. \ e = \<lfloor>x2\<rfloor> \<longrightarrow> (\<forall>x2a. \ e2 = \<lfloor>x2a\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a - {V}) \<and> x2 \<inter> (x2a - {V}) \<subseteq> dom (lcl s') \<union> (x2a - {V})))
 7. \<And>e s ta e' s' V e2 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> (\ e2 = None \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<and> x2c \<subseteq> dom (lcl s') \<union> x2a) \<and> (\<forall>x2. \ e2 = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<inter> (x2 - {V}) \<and> x2c \<inter> (x2 - {V}) \<subseteq> dom (lcl s') \<union> x2a \<inter> (x2 - {V}))
 8. \<And>e s ta e' s' es x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \s es = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2)
 9. \<And>es s ta es' s' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>es,s\<rangle> [-ta\<rightarrow>] \<langle>es',s'\<rangle>; \s es' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \s es = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<and> x2c \<subseteq> dom (lcl s') \<union> x2a
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>e s ta e' s' e2 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \ e2 = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2)
 2. \<And>b s ta b' s' e1 e2 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>b,s\<rangle> -ta\<rightarrow> \<langle>b',s'\<rangle>; \ b' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ b = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. (\ e2 = None \<longrightarrow> x2c = x2 \<longrightarrow> (\<forall>x2b. \ e1 = \<lfloor>x2b\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2b) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2b) \<and> x2b \<subseteq> dom (lcl s') \<union> (x2a \<union> x2b))) \<and> (\<forall>x2b. \ e2 = \<lfloor>x2b\<rfloor> \<longrightarrow> x2c = x2 \<longrightarrow> (\ e1 = None \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2b) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2b) \<and> x2b \<subseteq> dom (lcl s') \<union> (x2a \<union> x2b)) \<and> (\<forall>x2c. \ e1 = \<lfloor>x2c\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2c \<inter> x2b) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2c \<inter> x2b) \<and> x2c \<inter> x2b \<subseteq> dom (lcl s') \<union> (x2a \<union> x2c \<inter> x2b)))
 3. \<And>e1 e2 s. \<forall>x2 x2a. \ e2 = \<lfloor>x2a\<rfloor> \<longrightarrow> \ e1 = \<lfloor>x2\<rfloor> \<longrightarrow> x2 \<inter> x2a \<subseteq> x2 \<union> dom (lcl s)
 4. \<And>e1 e2 s. \<forall>x2 x2a. \ e2 = \<lfloor>x2a\<rfloor> \<longrightarrow> \ e1 = \<lfloor>x2\<rfloor> \<longrightarrow> x2 \<inter> x2a \<subseteq> x2a \<union> dom (lcl s)
 5. \<And>e s ta e' s' V e2. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = None\<rbrakk> \<Longrightarrow> (\ e = None \<longrightarrow> (\<forall>x2. \ e2 = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2 - {V}))) \<and> (\<forall>x2. \ e = \<lfloor>x2\<rfloor> \<longrightarrow> (\<forall>x2a. \ e2 = \<lfloor>x2a\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a - {V}) \<and> x2 \<inter> (x2a - {V}) \<subseteq> dom (lcl s') \<union> (x2a - {V})))
 6. \<And>e s ta e' s' V e2 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> (\ e2 = None \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<and> x2c \<subseteq> dom (lcl s') \<union> x2a) \<and> (\<forall>x2. \ e2 = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<inter> (x2 - {V}) \<and> x2c \<inter> (x2 - {V}) \<subseteq> dom (lcl s') \<union> x2a \<inter> (x2 - {V}))
 7. \<And>e s ta e' s' es x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \s es = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2)
 8. \<And>es s ta es' s' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>es,s\<rangle> [-ta\<rightarrow>] \<langle>es',s'\<rangle>; \s es' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \s es = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<and> x2c \<subseteq> dom (lcl s') \<union> x2a
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>b s ta b' s' e1 e2 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>b,s\<rangle> -ta\<rightarrow> \<langle>b',s'\<rangle>; \ b' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ b = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. (\ e2 = None \<longrightarrow> x2c = x2 \<longrightarrow> (\<forall>x2b. \ e1 = \<lfloor>x2b\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2b) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2b) \<and> x2b \<subseteq> dom (lcl s') \<union> (x2a \<union> x2b))) \<and> (\<forall>x2b. \ e2 = \<lfloor>x2b\<rfloor> \<longrightarrow> x2c = x2 \<longrightarrow> (\ e1 = None \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2b) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2b) \<and> x2b \<subseteq> dom (lcl s') \<union> (x2a \<union> x2b)) \<and> (\<forall>x2c. \ e1 = \<lfloor>x2c\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2c \<inter> x2b) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2c \<inter> x2b) \<and> x2c \<inter> x2b \<subseteq> dom (lcl s') \<union> (x2a \<union> x2c \<inter> x2b)))
 2. \<And>e1 e2 s. \<forall>x2 x2a. \ e2 = \<lfloor>x2a\<rfloor> \<longrightarrow> \ e1 = \<lfloor>x2\<rfloor> \<longrightarrow> x2 \<inter> x2a \<subseteq> x2 \<union> dom (lcl s)
 3. \<And>e1 e2 s. \<forall>x2 x2a. \ e2 = \<lfloor>x2a\<rfloor> \<longrightarrow> \ e1 = \<lfloor>x2\<rfloor> \<longrightarrow> x2 \<inter> x2a \<subseteq> x2a \<union> dom (lcl s)
 4. \<And>e s ta e' s' V e2. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = None\<rbrakk> \<Longrightarrow> (\ e = None \<longrightarrow> (\<forall>x2. \ e2 = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2 - {V}))) \<and> (\<forall>x2. \ e = \<lfloor>x2\<rfloor> \<longrightarrow> (\<forall>x2a. \ e2 = \<lfloor>x2a\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a - {V}) \<and> x2 \<inter> (x2a - {V}) \<subseteq> dom (lcl s') \<union> (x2a - {V})))
 5. \<And>e s ta e' s' V e2 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> (\ e2 = None \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<and> x2c \<subseteq> dom (lcl s') \<union> x2a) \<and> (\<forall>x2. \ e2 = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<inter> (x2 - {V}) \<and> x2c \<inter> (x2 - {V}) \<subseteq> dom (lcl s') \<union> x2a \<inter> (x2 - {V}))
 6. \<And>e s ta e' s' es x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \s es = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2)
 7. \<And>es s ta es' s' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>es,s\<rangle> [-ta\<rightarrow>] \<langle>es',s'\<rangle>; \s es' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \s es = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<and> x2c \<subseteq> dom (lcl s') \<union> x2a
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>e1 e2 s. \<forall>x2 x2a. \ e2 = \<lfloor>x2a\<rfloor> \<longrightarrow> \ e1 = \<lfloor>x2\<rfloor> \<longrightarrow> x2 \<inter> x2a \<subseteq> x2 \<union> dom (lcl s)
 2. \<And>e1 e2 s. \<forall>x2 x2a. \ e2 = \<lfloor>x2a\<rfloor> \<longrightarrow> \ e1 = \<lfloor>x2\<rfloor> \<longrightarrow> x2 \<inter> x2a \<subseteq> x2a \<union> dom (lcl s)
 3. \<And>e s ta e' s' V e2. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = None\<rbrakk> \<Longrightarrow> (\ e = None \<longrightarrow> (\<forall>x2. \ e2 = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2 - {V}))) \<and> (\<forall>x2. \ e = \<lfloor>x2\<rfloor> \<longrightarrow> (\<forall>x2a. \ e2 = \<lfloor>x2a\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a - {V}) \<and> x2 \<inter> (x2a - {V}) \<subseteq> dom (lcl s') \<union> (x2a - {V})))
 4. \<And>e s ta e' s' V e2 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> (\ e2 = None \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<and> x2c \<subseteq> dom (lcl s') \<union> x2a) \<and> (\<forall>x2. \ e2 = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<inter> (x2 - {V}) \<and> x2c \<inter> (x2 - {V}) \<subseteq> dom (lcl s') \<union> x2a \<inter> (x2 - {V}))
 5. \<And>e s ta e' s' es x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \s es = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2)
 6. \<And>es s ta es' s' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>es,s\<rangle> [-ta\<rightarrow>] \<langle>es',s'\<rangle>; \s es' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \s es = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<and> x2c \<subseteq> dom (lcl s') \<union> x2a
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>e1 e2 s. \<forall>x2 x2a. \ e2 = \<lfloor>x2a\<rfloor> \<longrightarrow> \ e1 = \<lfloor>x2\<rfloor> \<longrightarrow> x2 \<inter> x2a \<subseteq> x2a \<union> dom (lcl s)
 2. \<And>e s ta e' s' V e2. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = None\<rbrakk> \<Longrightarrow> (\ e = None \<longrightarrow> (\<forall>x2. \ e2 = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2 - {V}))) \<and> (\<forall>x2. \ e = \<lfloor>x2\<rfloor> \<longrightarrow> (\<forall>x2a. \ e2 = \<lfloor>x2a\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a - {V}) \<and> x2 \<inter> (x2a - {V}) \<subseteq> dom (lcl s') \<union> (x2a - {V})))
 3. \<And>e s ta e' s' V e2 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> (\ e2 = None \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<and> x2c \<subseteq> dom (lcl s') \<union> x2a) \<and> (\<forall>x2. \ e2 = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<inter> (x2 - {V}) \<and> x2c \<inter> (x2 - {V}) \<subseteq> dom (lcl s') \<union> x2a \<inter> (x2 - {V}))
 4. \<And>e s ta e' s' es x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \s es = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2)
 5. \<And>es s ta es' s' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>es,s\<rangle> [-ta\<rightarrow>] \<langle>es',s'\<rangle>; \s es' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \s es = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<and> x2c \<subseteq> dom (lcl s') \<union> x2a
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>e s ta e' s' V e2. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = None\<rbrakk> \<Longrightarrow> (\ e = None \<longrightarrow> (\<forall>x2. \ e2 = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2 - {V}))) \<and> (\<forall>x2. \ e = \<lfloor>x2\<rfloor> \<longrightarrow> (\<forall>x2a. \ e2 = \<lfloor>x2a\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a - {V}) \<and> x2 \<inter> (x2a - {V}) \<subseteq> dom (lcl s') \<union> (x2a - {V})))
 2. \<And>e s ta e' s' V e2 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> (\ e2 = None \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<and> x2c \<subseteq> dom (lcl s') \<union> x2a) \<and> (\<forall>x2. \ e2 = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<inter> (x2 - {V}) \<and> x2c \<inter> (x2 - {V}) \<subseteq> dom (lcl s') \<union> x2a \<inter> (x2 - {V}))
 3. \<And>e s ta e' s' es x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \s es = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2)
 4. \<And>es s ta es' s' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>es,s\<rangle> [-ta\<rightarrow>] \<langle>es',s'\<rangle>; \s es' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \s es = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<and> x2c \<subseteq> dom (lcl s') \<union> x2a
[PROOF STEP]
apply(blast dest: red_lcl_incr)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>e s ta e' s' V e2 x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> (\ e2 = None \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<and> x2c \<subseteq> dom (lcl s') \<union> x2a) \<and> (\<forall>x2. \ e2 = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<inter> (x2 - {V}) \<and> x2c \<inter> (x2 - {V}) \<subseteq> dom (lcl s') \<union> x2a \<inter> (x2 - {V}))
 2. \<And>e s ta e' s' es x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \s es = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2)
 3. \<And>es s ta es' s' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>es,s\<rangle> [-ta\<rightarrow>] \<langle>es',s'\<rangle>; \s es' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \s es = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<and> x2c \<subseteq> dom (lcl s') \<union> x2a
[PROOF STEP]
apply(blast dest: red_lcl_incr)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>e s ta e' s' es x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \ e' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \ e = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> \<forall>x2. \s es = \<lfloor>x2\<rfloor> \<longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2c \<subseteq> dom (lcl s') \<union> (x2a \<union> x2) \<and> x2 \<subseteq> dom (lcl s') \<union> (x2a \<union> x2)
 2. \<And>es s ta es' s' x2 x2a x2b x2c. \<lbrakk>x2b \<subseteq> x2; extTA,P,t \<turnstile> \<langle>es,s\<rangle> [-ta\<rightarrow>] \<langle>es',s'\<rangle>; \s es' = \<lfloor>x2a\<rfloor>; x2a \<union> dom (lcl s') = x2; \s es = \<lfloor>x2c\<rfloor>; x2c \<union> dom (lcl s) = x2b\<rbrakk> \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s') \<union> x2a \<and> x2c \<subseteq> dom (lcl s') \<union> x2a
[PROOF STEP]
by blast+