[STATEMENT]
lemma A_compE\<^sub>1:
      "\<And>A Vs. \<lbrakk> \ e = \<lfloor>A\<rfloor>; fv e \<subseteq> set Vs \<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs e) = \<lfloor>last_index Vs ` A\<rfloor>"
and "\<And>A Vs. \<lbrakk> \s es = \<lfloor>A\<rfloor>; fvs es \<subseteq> set Vs \<rbrakk> \<Longrightarrow> \s (compEs\<^sub>1 Vs es) = \<lfloor>last_index Vs ` A\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>A Vs. \<lbrakk>\ e = \<lfloor>A\<rfloor>; fv e \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs e) = \<lfloor>last_index Vs ` A\<rfloor>) &&& (\<And>A Vs. \<lbrakk>\<A>s es = \<lfloor>A\<rfloor>; fvs es \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A>s (compEs\<^sub>1 Vs es) = \<lfloor>last_index Vs ` A\<rfloor>)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>A Vs. \<lbrakk>\ e = \<lfloor>A\<rfloor>; fv e \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs e) = \<lfloor>last_index Vs ` A\<rfloor>) &&& (\<And>A Vs. \<lbrakk>\<A>s es = \<lfloor>A\<rfloor>; fvs es \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A>s (compEs\<^sub>1 Vs es) = \<lfloor>last_index Vs ` A\<rfloor>)
[PROOF STEP]
proof(induct e and es rule: fv.induct fvs.induct)
[PROOF STATE]
proof (state)
goal (17 subgoals):
 1. \<And>x A Vs. \<lbrakk>\ (new x) = \<lfloor>A\<rfloor>; fv (new x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (new x)) = \<lfloor>last_index Vs ` A\<rfloor>
 2. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (Cast x1 x2) = \<lfloor>A\<rfloor>; fv (Cast x1 x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (Cast x1 x2)) = \<lfloor>last_index Vs ` A\<rfloor>
 3. \<And>x A Vs. \<lbrakk>\ (Val x) = \<lfloor>A\<rfloor>; fv (Val x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (Val x)) = \<lfloor>last_index Vs ` A\<rfloor>
 4. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x3 = \<lfloor>A\<rfloor>; fv x3 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x3) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1 \<guillemotleft>x2\<guillemotright> x3) = \<lfloor>A\<rfloor>; fv (x1 \<guillemotleft>x2\<guillemotright> x3) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1 \<guillemotleft>x2\<guillemotright> x3)) = \<lfloor>last_index Vs ` A\<rfloor>
 5. \<And>x A Vs. \<lbrakk>\ (Var x) = \<lfloor>A\<rfloor>; fv (Var x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (Var x)) = \<lfloor>last_index Vs ` A\<rfloor>
 6. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (x1:=x2) = \<lfloor>A\<rfloor>; fv (x1:=x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (x1:=x2)) = \<lfloor>last_index Vs ` A\<rfloor>
 7. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (x1\<bullet>x2{x3}) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2{x3}) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (x1\<bullet>x2{x3})) = \<lfloor>last_index Vs ` A\<rfloor>
 8. \<And>x1 x2 x3 x4 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x4 = \<lfloor>A\<rfloor>; fv x4 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x4) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1\<bullet>x2{x3} := x4) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2{x3} := x4) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1\<bullet>x2{x3} := x4)) = \<lfloor>last_index Vs ` A\<rfloor>
 9. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A>s x3 = \<lfloor>A\<rfloor>; fvs x3 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A>s (compEs\<^sub>1 Vs x3) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1\<bullet>x2(x3)) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2(x3)) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1\<bullet>x2(x3))) = \<lfloor>last_index Vs ` A\<rfloor>
 10. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x3 = \<lfloor>A\<rfloor>; fv x3 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x3) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> {x1:x2; x3} = \<lfloor>A\<rfloor>; fv {x1:x2; x3} \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs {x1:x2; x3}) = \<lfloor>last_index Vs ` A\<rfloor>
A total of 17 subgoals...
[PROOF STEP]
case (Block V' T e)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\ e = \<lfloor>?A\<rfloor>; fv e \<subseteq> set ?Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 ?Vs e) = \<lfloor>last_index ?Vs ` ?A\<rfloor>
\ {V':T; e} = \<lfloor>A\<rfloor>
fv {V':T; e} \<subseteq> set Vs

goal (17 subgoals):
 1. \<And>x A Vs. \<lbrakk>\ (new x) = \<lfloor>A\<rfloor>; fv (new x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (new x)) = \<lfloor>last_index Vs ` A\<rfloor>
 2. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (Cast x1 x2) = \<lfloor>A\<rfloor>; fv (Cast x1 x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (Cast x1 x2)) = \<lfloor>last_index Vs ` A\<rfloor>
 3. \<And>x A Vs. \<lbrakk>\ (Val x) = \<lfloor>A\<rfloor>; fv (Val x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (Val x)) = \<lfloor>last_index Vs ` A\<rfloor>
 4. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x3 = \<lfloor>A\<rfloor>; fv x3 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x3) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1 \<guillemotleft>x2\<guillemotright> x3) = \<lfloor>A\<rfloor>; fv (x1 \<guillemotleft>x2\<guillemotright> x3) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1 \<guillemotleft>x2\<guillemotright> x3)) = \<lfloor>last_index Vs ` A\<rfloor>
 5. \<And>x A Vs. \<lbrakk>\ (Var x) = \<lfloor>A\<rfloor>; fv (Var x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (Var x)) = \<lfloor>last_index Vs ` A\<rfloor>
 6. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (x1:=x2) = \<lfloor>A\<rfloor>; fv (x1:=x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (x1:=x2)) = \<lfloor>last_index Vs ` A\<rfloor>
 7. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (x1\<bullet>x2{x3}) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2{x3}) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (x1\<bullet>x2{x3})) = \<lfloor>last_index Vs ` A\<rfloor>
 8. \<And>x1 x2 x3 x4 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x4 = \<lfloor>A\<rfloor>; fv x4 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x4) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1\<bullet>x2{x3} := x4) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2{x3} := x4) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1\<bullet>x2{x3} := x4)) = \<lfloor>last_index Vs ` A\<rfloor>
 9. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A>s x3 = \<lfloor>A\<rfloor>; fvs x3 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A>s (compEs\<^sub>1 Vs x3) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1\<bullet>x2(x3)) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2(x3)) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1\<bullet>x2(x3))) = \<lfloor>last_index Vs ` A\<rfloor>
 10. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x3 = \<lfloor>A\<rfloor>; fv x3 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x3) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> {x1:x2; x3} = \<lfloor>A\<rfloor>; fv {x1:x2; x3} \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs {x1:x2; x3}) = \<lfloor>last_index Vs ` A\<rfloor>
A total of 17 subgoals...
[PROOF STEP]
hence "fv e \<subseteq> set (Vs@[V'])"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\ e = \<lfloor>?A\<rfloor>; fv e \<subseteq> set ?Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 ?Vs e) = \<lfloor>last_index ?Vs ` ?A\<rfloor>
\ {V':T; e} = \<lfloor>A\<rfloor>
fv {V':T; e} \<subseteq> set Vs

goal (1 subgoal):
 1. fv e \<subseteq> set (Vs @ [V'])
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
fv e \<subseteq> set (Vs @ [V'])

goal (17 subgoals):
 1. \<And>x A Vs. \<lbrakk>\ (new x) = \<lfloor>A\<rfloor>; fv (new x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (new x)) = \<lfloor>last_index Vs ` A\<rfloor>
 2. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (Cast x1 x2) = \<lfloor>A\<rfloor>; fv (Cast x1 x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (Cast x1 x2)) = \<lfloor>last_index Vs ` A\<rfloor>
 3. \<And>x A Vs. \<lbrakk>\ (Val x) = \<lfloor>A\<rfloor>; fv (Val x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (Val x)) = \<lfloor>last_index Vs ` A\<rfloor>
 4. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x3 = \<lfloor>A\<rfloor>; fv x3 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x3) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1 \<guillemotleft>x2\<guillemotright> x3) = \<lfloor>A\<rfloor>; fv (x1 \<guillemotleft>x2\<guillemotright> x3) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1 \<guillemotleft>x2\<guillemotright> x3)) = \<lfloor>last_index Vs ` A\<rfloor>
 5. \<And>x A Vs. \<lbrakk>\ (Var x) = \<lfloor>A\<rfloor>; fv (Var x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (Var x)) = \<lfloor>last_index Vs ` A\<rfloor>
 6. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (x1:=x2) = \<lfloor>A\<rfloor>; fv (x1:=x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (x1:=x2)) = \<lfloor>last_index Vs ` A\<rfloor>
 7. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (x1\<bullet>x2{x3}) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2{x3}) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (x1\<bullet>x2{x3})) = \<lfloor>last_index Vs ` A\<rfloor>
 8. \<And>x1 x2 x3 x4 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x4 = \<lfloor>A\<rfloor>; fv x4 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x4) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1\<bullet>x2{x3} := x4) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2{x3} := x4) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1\<bullet>x2{x3} := x4)) = \<lfloor>last_index Vs ` A\<rfloor>
 9. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A>s x3 = \<lfloor>A\<rfloor>; fvs x3 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A>s (compEs\<^sub>1 Vs x3) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1\<bullet>x2(x3)) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2(x3)) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1\<bullet>x2(x3))) = \<lfloor>last_index Vs ` A\<rfloor>
 10. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x3 = \<lfloor>A\<rfloor>; fv x3 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x3) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> {x1:x2; x3} = \<lfloor>A\<rfloor>; fv {x1:x2; x3} \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs {x1:x2; x3}) = \<lfloor>last_index Vs ` A\<rfloor>
A total of 17 subgoals...
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
fv e \<subseteq> set (Vs @ [V'])

goal (17 subgoals):
 1. \<And>x A Vs. \<lbrakk>\ (new x) = \<lfloor>A\<rfloor>; fv (new x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (new x)) = \<lfloor>last_index Vs ` A\<rfloor>
 2. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (Cast x1 x2) = \<lfloor>A\<rfloor>; fv (Cast x1 x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (Cast x1 x2)) = \<lfloor>last_index Vs ` A\<rfloor>
 3. \<And>x A Vs. \<lbrakk>\ (Val x) = \<lfloor>A\<rfloor>; fv (Val x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (Val x)) = \<lfloor>last_index Vs ` A\<rfloor>
 4. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x3 = \<lfloor>A\<rfloor>; fv x3 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x3) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1 \<guillemotleft>x2\<guillemotright> x3) = \<lfloor>A\<rfloor>; fv (x1 \<guillemotleft>x2\<guillemotright> x3) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1 \<guillemotleft>x2\<guillemotright> x3)) = \<lfloor>last_index Vs ` A\<rfloor>
 5. \<And>x A Vs. \<lbrakk>\ (Var x) = \<lfloor>A\<rfloor>; fv (Var x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (Var x)) = \<lfloor>last_index Vs ` A\<rfloor>
 6. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (x1:=x2) = \<lfloor>A\<rfloor>; fv (x1:=x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (x1:=x2)) = \<lfloor>last_index Vs ` A\<rfloor>
 7. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (x1\<bullet>x2{x3}) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2{x3}) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (x1\<bullet>x2{x3})) = \<lfloor>last_index Vs ` A\<rfloor>
 8. \<And>x1 x2 x3 x4 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x4 = \<lfloor>A\<rfloor>; fv x4 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x4) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1\<bullet>x2{x3} := x4) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2{x3} := x4) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1\<bullet>x2{x3} := x4)) = \<lfloor>last_index Vs ` A\<rfloor>
 9. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A>s x3 = \<lfloor>A\<rfloor>; fvs x3 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A>s (compEs\<^sub>1 Vs x3) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1\<bullet>x2(x3)) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2(x3)) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1\<bullet>x2(x3))) = \<lfloor>last_index Vs ` A\<rfloor>
 10. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x3 = \<lfloor>A\<rfloor>; fv x3 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x3) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> {x1:x2; x3} = \<lfloor>A\<rfloor>; fv {x1:x2; x3} \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs {x1:x2; x3}) = \<lfloor>last_index Vs ` A\<rfloor>
A total of 17 subgoals...
[PROOF STEP]
obtain B where "\ e = \<lfloor>B\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>B. \ e = \<lfloor>B\<rfloor> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using Block.prems
[PROOF STATE]
proof (prove)
using this:
\ {V':T; e} = \<lfloor>A\<rfloor>
fv {V':T; e} \<subseteq> set Vs

goal (1 subgoal):
 1. (\<And>B. \ e = \<lfloor>B\<rfloor> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(simp add: hyperset_defs)
[PROOF STATE]
proof (state)
this:
\ e = \<lfloor>B\<rfloor>

goal (17 subgoals):
 1. \<And>x A Vs. \<lbrakk>\ (new x) = \<lfloor>A\<rfloor>; fv (new x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (new x)) = \<lfloor>last_index Vs ` A\<rfloor>
 2. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (Cast x1 x2) = \<lfloor>A\<rfloor>; fv (Cast x1 x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (Cast x1 x2)) = \<lfloor>last_index Vs ` A\<rfloor>
 3. \<And>x A Vs. \<lbrakk>\ (Val x) = \<lfloor>A\<rfloor>; fv (Val x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (Val x)) = \<lfloor>last_index Vs ` A\<rfloor>
 4. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x3 = \<lfloor>A\<rfloor>; fv x3 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x3) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1 \<guillemotleft>x2\<guillemotright> x3) = \<lfloor>A\<rfloor>; fv (x1 \<guillemotleft>x2\<guillemotright> x3) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1 \<guillemotleft>x2\<guillemotright> x3)) = \<lfloor>last_index Vs ` A\<rfloor>
 5. \<And>x A Vs. \<lbrakk>\ (Var x) = \<lfloor>A\<rfloor>; fv (Var x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (Var x)) = \<lfloor>last_index Vs ` A\<rfloor>
 6. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (x1:=x2) = \<lfloor>A\<rfloor>; fv (x1:=x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (x1:=x2)) = \<lfloor>last_index Vs ` A\<rfloor>
 7. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (x1\<bullet>x2{x3}) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2{x3}) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (x1\<bullet>x2{x3})) = \<lfloor>last_index Vs ` A\<rfloor>
 8. \<And>x1 x2 x3 x4 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x4 = \<lfloor>A\<rfloor>; fv x4 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x4) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1\<bullet>x2{x3} := x4) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2{x3} := x4) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1\<bullet>x2{x3} := x4)) = \<lfloor>last_index Vs ` A\<rfloor>
 9. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A>s x3 = \<lfloor>A\<rfloor>; fvs x3 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A>s (compEs\<^sub>1 Vs x3) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1\<bullet>x2(x3)) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2(x3)) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1\<bullet>x2(x3))) = \<lfloor>last_index Vs ` A\<rfloor>
 10. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x3 = \<lfloor>A\<rfloor>; fv x3 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x3) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> {x1:x2; x3} = \<lfloor>A\<rfloor>; fv {x1:x2; x3} \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs {x1:x2; x3}) = \<lfloor>last_index Vs ` A\<rfloor>
A total of 17 subgoals...
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\ e = \<lfloor>B\<rfloor>

goal (17 subgoals):
 1. \<And>x A Vs. \<lbrakk>\ (new x) = \<lfloor>A\<rfloor>; fv (new x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (new x)) = \<lfloor>last_index Vs ` A\<rfloor>
 2. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (Cast x1 x2) = \<lfloor>A\<rfloor>; fv (Cast x1 x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (Cast x1 x2)) = \<lfloor>last_index Vs ` A\<rfloor>
 3. \<And>x A Vs. \<lbrakk>\ (Val x) = \<lfloor>A\<rfloor>; fv (Val x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (Val x)) = \<lfloor>last_index Vs ` A\<rfloor>
 4. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x3 = \<lfloor>A\<rfloor>; fv x3 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x3) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1 \<guillemotleft>x2\<guillemotright> x3) = \<lfloor>A\<rfloor>; fv (x1 \<guillemotleft>x2\<guillemotright> x3) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1 \<guillemotleft>x2\<guillemotright> x3)) = \<lfloor>last_index Vs ` A\<rfloor>
 5. \<And>x A Vs. \<lbrakk>\ (Var x) = \<lfloor>A\<rfloor>; fv (Var x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (Var x)) = \<lfloor>last_index Vs ` A\<rfloor>
 6. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (x1:=x2) = \<lfloor>A\<rfloor>; fv (x1:=x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (x1:=x2)) = \<lfloor>last_index Vs ` A\<rfloor>
 7. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (x1\<bullet>x2{x3}) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2{x3}) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (x1\<bullet>x2{x3})) = \<lfloor>last_index Vs ` A\<rfloor>
 8. \<And>x1 x2 x3 x4 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x4 = \<lfloor>A\<rfloor>; fv x4 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x4) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1\<bullet>x2{x3} := x4) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2{x3} := x4) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1\<bullet>x2{x3} := x4)) = \<lfloor>last_index Vs ` A\<rfloor>
 9. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A>s x3 = \<lfloor>A\<rfloor>; fvs x3 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A>s (compEs\<^sub>1 Vs x3) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1\<bullet>x2(x3)) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2(x3)) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1\<bullet>x2(x3))) = \<lfloor>last_index Vs ` A\<rfloor>
 10. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x3 = \<lfloor>A\<rfloor>; fv x3 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x3) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> {x1:x2; x3} = \<lfloor>A\<rfloor>; fv {x1:x2; x3} \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs {x1:x2; x3}) = \<lfloor>last_index Vs ` A\<rfloor>
A total of 17 subgoals...
[PROOF STEP]
from calculation
[PROOF STATE]
proof (chain)
picking this:
fv e \<subseteq> set (Vs @ [V'])
\ e = \<lfloor>B\<rfloor>
[PROOF STEP]
have "B \<subseteq> set (Vs@[V'])"
[PROOF STATE]
proof (prove)
using this:
fv e \<subseteq> set (Vs @ [V'])
\ e = \<lfloor>B\<rfloor>

goal (1 subgoal):
 1. B \<subseteq> set (Vs @ [V'])
[PROOF STEP]
by(auto dest!:A_fv)
[PROOF STATE]
proof (state)
this:
B \<subseteq> set (Vs @ [V'])

goal (17 subgoals):
 1. \<And>x A Vs. \<lbrakk>\ (new x) = \<lfloor>A\<rfloor>; fv (new x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (new x)) = \<lfloor>last_index Vs ` A\<rfloor>
 2. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (Cast x1 x2) = \<lfloor>A\<rfloor>; fv (Cast x1 x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (Cast x1 x2)) = \<lfloor>last_index Vs ` A\<rfloor>
 3. \<And>x A Vs. \<lbrakk>\ (Val x) = \<lfloor>A\<rfloor>; fv (Val x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (Val x)) = \<lfloor>last_index Vs ` A\<rfloor>
 4. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x3 = \<lfloor>A\<rfloor>; fv x3 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x3) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1 \<guillemotleft>x2\<guillemotright> x3) = \<lfloor>A\<rfloor>; fv (x1 \<guillemotleft>x2\<guillemotright> x3) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1 \<guillemotleft>x2\<guillemotright> x3)) = \<lfloor>last_index Vs ` A\<rfloor>
 5. \<And>x A Vs. \<lbrakk>\ (Var x) = \<lfloor>A\<rfloor>; fv (Var x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (Var x)) = \<lfloor>last_index Vs ` A\<rfloor>
 6. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (x1:=x2) = \<lfloor>A\<rfloor>; fv (x1:=x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (x1:=x2)) = \<lfloor>last_index Vs ` A\<rfloor>
 7. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (x1\<bullet>x2{x3}) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2{x3}) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (x1\<bullet>x2{x3})) = \<lfloor>last_index Vs ` A\<rfloor>
 8. \<And>x1 x2 x3 x4 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x4 = \<lfloor>A\<rfloor>; fv x4 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x4) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1\<bullet>x2{x3} := x4) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2{x3} := x4) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1\<bullet>x2{x3} := x4)) = \<lfloor>last_index Vs ` A\<rfloor>
 9. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A>s x3 = \<lfloor>A\<rfloor>; fvs x3 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A>s (compEs\<^sub>1 Vs x3) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1\<bullet>x2(x3)) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2(x3)) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1\<bullet>x2(x3))) = \<lfloor>last_index Vs ` A\<rfloor>
 10. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x3 = \<lfloor>A\<rfloor>; fv x3 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x3) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> {x1:x2; x3} = \<lfloor>A\<rfloor>; fv {x1:x2; x3} \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs {x1:x2; x3}) = \<lfloor>last_index Vs ` A\<rfloor>
A total of 17 subgoals...
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
fv e \<subseteq> set (Vs @ [V'])
\ e = \<lfloor>B\<rfloor>
B \<subseteq> set (Vs @ [V'])
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
fv e \<subseteq> set (Vs @ [V'])
\ e = \<lfloor>B\<rfloor>
B \<subseteq> set (Vs @ [V'])

goal (1 subgoal):
 1. \ (compE\<^sub>1 Vs {V':T; e}) = \<lfloor>last_index Vs ` A\<rfloor>
[PROOF STEP]
using Block
[PROOF STATE]
proof (prove)
using this:
fv e \<subseteq> set (Vs @ [V'])
\ e = \<lfloor>B\<rfloor>
B \<subseteq> set (Vs @ [V'])
\<lbrakk>\ e = \<lfloor>?A\<rfloor>; fv e \<subseteq> set ?Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 ?Vs e) = \<lfloor>last_index ?Vs ` ?A\<rfloor>
\ {V':T; e} = \<lfloor>A\<rfloor>
fv {V':T; e} \<subseteq> set Vs

goal (1 subgoal):
 1. \ (compE\<^sub>1 Vs {V':T; e}) = \<lfloor>last_index Vs ` A\<rfloor>
[PROOF STEP]
by(auto simp add: hyperset_defs image_last_index last_index_size_conv)
[PROOF STATE]
proof (state)
this:
\ (compE\<^sub>1 Vs {V':T; e}) = \<lfloor>last_index Vs ` A\<rfloor>

goal (16 subgoals):
 1. \<And>x A Vs. \<lbrakk>\ (new x) = \<lfloor>A\<rfloor>; fv (new x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (new x)) = \<lfloor>last_index Vs ` A\<rfloor>
 2. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (Cast x1 x2) = \<lfloor>A\<rfloor>; fv (Cast x1 x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (Cast x1 x2)) = \<lfloor>last_index Vs ` A\<rfloor>
 3. \<And>x A Vs. \<lbrakk>\ (Val x) = \<lfloor>A\<rfloor>; fv (Val x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (Val x)) = \<lfloor>last_index Vs ` A\<rfloor>
 4. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x3 = \<lfloor>A\<rfloor>; fv x3 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x3) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1 \<guillemotleft>x2\<guillemotright> x3) = \<lfloor>A\<rfloor>; fv (x1 \<guillemotleft>x2\<guillemotright> x3) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1 \<guillemotleft>x2\<guillemotright> x3)) = \<lfloor>last_index Vs ` A\<rfloor>
 5. \<And>x A Vs. \<lbrakk>\ (Var x) = \<lfloor>A\<rfloor>; fv (Var x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (Var x)) = \<lfloor>last_index Vs ` A\<rfloor>
 6. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (x1:=x2) = \<lfloor>A\<rfloor>; fv (x1:=x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (x1:=x2)) = \<lfloor>last_index Vs ` A\<rfloor>
 7. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (x1\<bullet>x2{x3}) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2{x3}) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (x1\<bullet>x2{x3})) = \<lfloor>last_index Vs ` A\<rfloor>
 8. \<And>x1 x2 x3 x4 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x4 = \<lfloor>A\<rfloor>; fv x4 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x4) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1\<bullet>x2{x3} := x4) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2{x3} := x4) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1\<bullet>x2{x3} := x4)) = \<lfloor>last_index Vs ` A\<rfloor>
 9. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A>s x3 = \<lfloor>A\<rfloor>; fvs x3 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A>s (compEs\<^sub>1 Vs x3) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1\<bullet>x2(x3)) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2(x3)) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1\<bullet>x2(x3))) = \<lfloor>last_index Vs ` A\<rfloor>
 10. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1;; x2) = \<lfloor>A\<rfloor>; fv (x1;; x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1;; x2)) = \<lfloor>last_index Vs ` A\<rfloor>
A total of 16 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (16 subgoals):
 1. \<And>x A Vs. \<lbrakk>\ (new x) = \<lfloor>A\<rfloor>; fv (new x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (new x)) = \<lfloor>last_index Vs ` A\<rfloor>
 2. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (Cast x1 x2) = \<lfloor>A\<rfloor>; fv (Cast x1 x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (Cast x1 x2)) = \<lfloor>last_index Vs ` A\<rfloor>
 3. \<And>x A Vs. \<lbrakk>\ (Val x) = \<lfloor>A\<rfloor>; fv (Val x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (Val x)) = \<lfloor>last_index Vs ` A\<rfloor>
 4. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x3 = \<lfloor>A\<rfloor>; fv x3 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x3) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1 \<guillemotleft>x2\<guillemotright> x3) = \<lfloor>A\<rfloor>; fv (x1 \<guillemotleft>x2\<guillemotright> x3) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1 \<guillemotleft>x2\<guillemotright> x3)) = \<lfloor>last_index Vs ` A\<rfloor>
 5. \<And>x A Vs. \<lbrakk>\ (Var x) = \<lfloor>A\<rfloor>; fv (Var x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (Var x)) = \<lfloor>last_index Vs ` A\<rfloor>
 6. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (x1:=x2) = \<lfloor>A\<rfloor>; fv (x1:=x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (x1:=x2)) = \<lfloor>last_index Vs ` A\<rfloor>
 7. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (x1\<bullet>x2{x3}) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2{x3}) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (x1\<bullet>x2{x3})) = \<lfloor>last_index Vs ` A\<rfloor>
 8. \<And>x1 x2 x3 x4 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x4 = \<lfloor>A\<rfloor>; fv x4 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x4) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1\<bullet>x2{x3} := x4) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2{x3} := x4) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1\<bullet>x2{x3} := x4)) = \<lfloor>last_index Vs ` A\<rfloor>
 9. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A>s x3 = \<lfloor>A\<rfloor>; fvs x3 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A>s (compEs\<^sub>1 Vs x3) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1\<bullet>x2(x3)) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2(x3)) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1\<bullet>x2(x3))) = \<lfloor>last_index Vs ` A\<rfloor>
 10. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1;; x2) = \<lfloor>A\<rfloor>; fv (x1;; x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1;; x2)) = \<lfloor>last_index Vs ` A\<rfloor>
A total of 16 subgoals...
[PROOF STEP]
case (TryCatch e\<^sub>1 C V' e\<^sub>2)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\ e\<^sub>1 = \<lfloor>?A\<rfloor>; fv e\<^sub>1 \<subseteq> set ?Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 ?Vs e\<^sub>1) = \<lfloor>last_index ?Vs ` ?A\<rfloor>
\<lbrakk>\ e\<^sub>2 = \<lfloor>?A\<rfloor>; fv e\<^sub>2 \<subseteq> set ?Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 ?Vs e\<^sub>2) = \<lfloor>last_index ?Vs ` ?A\<rfloor>
\ (try e\<^sub>1 catch(C V') e\<^sub>2) = \<lfloor>A\<rfloor>
fv (try e\<^sub>1 catch(C V') e\<^sub>2) \<subseteq> set Vs

goal (16 subgoals):
 1. \<And>x A Vs. \<lbrakk>\ (new x) = \<lfloor>A\<rfloor>; fv (new x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (new x)) = \<lfloor>last_index Vs ` A\<rfloor>
 2. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (Cast x1 x2) = \<lfloor>A\<rfloor>; fv (Cast x1 x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (Cast x1 x2)) = \<lfloor>last_index Vs ` A\<rfloor>
 3. \<And>x A Vs. \<lbrakk>\ (Val x) = \<lfloor>A\<rfloor>; fv (Val x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (Val x)) = \<lfloor>last_index Vs ` A\<rfloor>
 4. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x3 = \<lfloor>A\<rfloor>; fv x3 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x3) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1 \<guillemotleft>x2\<guillemotright> x3) = \<lfloor>A\<rfloor>; fv (x1 \<guillemotleft>x2\<guillemotright> x3) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1 \<guillemotleft>x2\<guillemotright> x3)) = \<lfloor>last_index Vs ` A\<rfloor>
 5. \<And>x A Vs. \<lbrakk>\ (Var x) = \<lfloor>A\<rfloor>; fv (Var x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (Var x)) = \<lfloor>last_index Vs ` A\<rfloor>
 6. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (x1:=x2) = \<lfloor>A\<rfloor>; fv (x1:=x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (x1:=x2)) = \<lfloor>last_index Vs ` A\<rfloor>
 7. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (x1\<bullet>x2{x3}) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2{x3}) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (x1\<bullet>x2{x3})) = \<lfloor>last_index Vs ` A\<rfloor>
 8. \<And>x1 x2 x3 x4 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x4 = \<lfloor>A\<rfloor>; fv x4 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x4) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1\<bullet>x2{x3} := x4) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2{x3} := x4) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1\<bullet>x2{x3} := x4)) = \<lfloor>last_index Vs ` A\<rfloor>
 9. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A>s x3 = \<lfloor>A\<rfloor>; fvs x3 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A>s (compEs\<^sub>1 Vs x3) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1\<bullet>x2(x3)) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2(x3)) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1\<bullet>x2(x3))) = \<lfloor>last_index Vs ` A\<rfloor>
 10. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1;; x2) = \<lfloor>A\<rfloor>; fv (x1;; x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1;; x2)) = \<lfloor>last_index Vs ` A\<rfloor>
A total of 16 subgoals...
[PROOF STEP]
hence fve\<^sub>2: "fv e\<^sub>2 \<subseteq> set (Vs@[V'])"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\ e\<^sub>1 = \<lfloor>?A\<rfloor>; fv e\<^sub>1 \<subseteq> set ?Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 ?Vs e\<^sub>1) = \<lfloor>last_index ?Vs ` ?A\<rfloor>
\<lbrakk>\ e\<^sub>2 = \<lfloor>?A\<rfloor>; fv e\<^sub>2 \<subseteq> set ?Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 ?Vs e\<^sub>2) = \<lfloor>last_index ?Vs ` ?A\<rfloor>
\ (try e\<^sub>1 catch(C V') e\<^sub>2) = \<lfloor>A\<rfloor>
fv (try e\<^sub>1 catch(C V') e\<^sub>2) \<subseteq> set Vs

goal (1 subgoal):
 1. fv e\<^sub>2 \<subseteq> set (Vs @ [V'])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fv e\<^sub>2 \<subseteq> set (Vs @ [V'])

goal (16 subgoals):
 1. \<And>x A Vs. \<lbrakk>\ (new x) = \<lfloor>A\<rfloor>; fv (new x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (new x)) = \<lfloor>last_index Vs ` A\<rfloor>
 2. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (Cast x1 x2) = \<lfloor>A\<rfloor>; fv (Cast x1 x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (Cast x1 x2)) = \<lfloor>last_index Vs ` A\<rfloor>
 3. \<And>x A Vs. \<lbrakk>\ (Val x) = \<lfloor>A\<rfloor>; fv (Val x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (Val x)) = \<lfloor>last_index Vs ` A\<rfloor>
 4. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x3 = \<lfloor>A\<rfloor>; fv x3 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x3) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1 \<guillemotleft>x2\<guillemotright> x3) = \<lfloor>A\<rfloor>; fv (x1 \<guillemotleft>x2\<guillemotright> x3) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1 \<guillemotleft>x2\<guillemotright> x3)) = \<lfloor>last_index Vs ` A\<rfloor>
 5. \<And>x A Vs. \<lbrakk>\ (Var x) = \<lfloor>A\<rfloor>; fv (Var x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (Var x)) = \<lfloor>last_index Vs ` A\<rfloor>
 6. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (x1:=x2) = \<lfloor>A\<rfloor>; fv (x1:=x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (x1:=x2)) = \<lfloor>last_index Vs ` A\<rfloor>
 7. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (x1\<bullet>x2{x3}) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2{x3}) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (x1\<bullet>x2{x3})) = \<lfloor>last_index Vs ` A\<rfloor>
 8. \<And>x1 x2 x3 x4 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x4 = \<lfloor>A\<rfloor>; fv x4 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x4) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1\<bullet>x2{x3} := x4) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2{x3} := x4) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1\<bullet>x2{x3} := x4)) = \<lfloor>last_index Vs ` A\<rfloor>
 9. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A>s x3 = \<lfloor>A\<rfloor>; fvs x3 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A>s (compEs\<^sub>1 Vs x3) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1\<bullet>x2(x3)) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2(x3)) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1\<bullet>x2(x3))) = \<lfloor>last_index Vs ` A\<rfloor>
 10. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1;; x2) = \<lfloor>A\<rfloor>; fv (x1;; x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1;; x2)) = \<lfloor>last_index Vs ` A\<rfloor>
A total of 16 subgoals...
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \ (compE\<^sub>1 Vs (try e\<^sub>1 catch(C V') e\<^sub>2)) = \<lfloor>last_index Vs ` A\<rfloor>
[PROOF STEP]
proof (cases "\ e\<^sub>1")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \ e\<^sub>1 = None \<Longrightarrow> \ (compE\<^sub>1 Vs (try e\<^sub>1 catch(C V') e\<^sub>2)) = \<lfloor>last_index Vs ` A\<rfloor>
 2. \<And>a. \ e\<^sub>1 = \<lfloor>a\<rfloor> \<Longrightarrow> \ (compE\<^sub>1 Vs (try e\<^sub>1 catch(C V') e\<^sub>2)) = \<lfloor>last_index Vs ` A\<rfloor>
[PROOF STEP]
assume A\<^sub>1: "\ e\<^sub>1 = None"
[PROOF STATE]
proof (state)
this:
\ e\<^sub>1 = None

goal (2 subgoals):
 1. \ e\<^sub>1 = None \<Longrightarrow> \ (compE\<^sub>1 Vs (try e\<^sub>1 catch(C V') e\<^sub>2)) = \<lfloor>last_index Vs ` A\<rfloor>
 2. \<And>a. \ e\<^sub>1 = \<lfloor>a\<rfloor> \<Longrightarrow> \ (compE\<^sub>1 Vs (try e\<^sub>1 catch(C V') e\<^sub>2)) = \<lfloor>last_index Vs ` A\<rfloor>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\ e\<^sub>1 = None
[PROOF STEP]
obtain A\<^sub>2 where A\<^sub>2: "\ e\<^sub>2 = \<lfloor>A\<^sub>2\<rfloor>"
[PROOF STATE]
proof (prove)
using this:
\ e\<^sub>1 = None

goal (1 subgoal):
 1. (\<And>A\<^sub>2. \ e\<^sub>2 = \<lfloor>A\<^sub>2\<rfloor> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using TryCatch
[PROOF STATE]
proof (prove)
using this:
\ e\<^sub>1 = None
\<lbrakk>\ e\<^sub>1 = \<lfloor>?A\<rfloor>; fv e\<^sub>1 \<subseteq> set ?Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 ?Vs e\<^sub>1) = \<lfloor>last_index ?Vs ` ?A\<rfloor>
\<lbrakk>\ e\<^sub>2 = \<lfloor>?A\<rfloor>; fv e\<^sub>2 \<subseteq> set ?Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 ?Vs e\<^sub>2) = \<lfloor>last_index ?Vs ` ?A\<rfloor>
\ (try e\<^sub>1 catch(C V') e\<^sub>2) = \<lfloor>A\<rfloor>
fv (try e\<^sub>1 catch(C V') e\<^sub>2) \<subseteq> set Vs

goal (1 subgoal):
 1. (\<And>A\<^sub>2. \ e\<^sub>2 = \<lfloor>A\<^sub>2\<rfloor> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(simp add:hyperset_defs)
[PROOF STATE]
proof (state)
this:
\ e\<^sub>2 = \<lfloor>A\<^sub>2\<rfloor>

goal (2 subgoals):
 1. \ e\<^sub>1 = None \<Longrightarrow> \ (compE\<^sub>1 Vs (try e\<^sub>1 catch(C V') e\<^sub>2)) = \<lfloor>last_index Vs ` A\<rfloor>
 2. \<And>a. \ e\<^sub>1 = \<lfloor>a\<rfloor> \<Longrightarrow> \ (compE\<^sub>1 Vs (try e\<^sub>1 catch(C V') e\<^sub>2)) = \<lfloor>last_index Vs ` A\<rfloor>
[PROOF STEP]
hence "A\<^sub>2 \<subseteq> set (Vs@[V'])"
[PROOF STATE]
proof (prove)
using this:
\ e\<^sub>2 = \<lfloor>A\<^sub>2\<rfloor>

goal (1 subgoal):
 1. A\<^sub>2 \<subseteq> set (Vs @ [V'])
[PROOF STEP]
using TryCatch.prems A_fv[OF A\<^sub>2]
[PROOF STATE]
proof (prove)
using this:
\ e\<^sub>2 = \<lfloor>A\<^sub>2\<rfloor>
\ (try e\<^sub>1 catch(C V') e\<^sub>2) = \<lfloor>A\<rfloor>
fv (try e\<^sub>1 catch(C V') e\<^sub>2) \<subseteq> set Vs
A\<^sub>2 \<subseteq> fv e\<^sub>2

goal (1 subgoal):
 1. A\<^sub>2 \<subseteq> set (Vs @ [V'])
[PROOF STEP]
by simp blast
[PROOF STATE]
proof (state)
this:
A\<^sub>2 \<subseteq> set (Vs @ [V'])

goal (2 subgoals):
 1. \ e\<^sub>1 = None \<Longrightarrow> \ (compE\<^sub>1 Vs (try e\<^sub>1 catch(C V') e\<^sub>2)) = \<lfloor>last_index Vs ` A\<rfloor>
 2. \<And>a. \ e\<^sub>1 = \<lfloor>a\<rfloor> \<Longrightarrow> \ (compE\<^sub>1 Vs (try e\<^sub>1 catch(C V') e\<^sub>2)) = \<lfloor>last_index Vs ` A\<rfloor>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
A\<^sub>2 \<subseteq> set (Vs @ [V'])

goal (1 subgoal):
 1. \ (compE\<^sub>1 Vs (try e\<^sub>1 catch(C V') e\<^sub>2)) = \<lfloor>last_index Vs ` A\<rfloor>
[PROOF STEP]
using TryCatch fve\<^sub>2 A\<^sub>1 A\<^sub>2
[PROOF STATE]
proof (prove)
using this:
A\<^sub>2 \<subseteq> set (Vs @ [V'])
\<lbrakk>\ e\<^sub>1 = \<lfloor>?A\<rfloor>; fv e\<^sub>1 \<subseteq> set ?Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 ?Vs e\<^sub>1) = \<lfloor>last_index ?Vs ` ?A\<rfloor>
\<lbrakk>\ e\<^sub>2 = \<lfloor>?A\<rfloor>; fv e\<^sub>2 \<subseteq> set ?Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 ?Vs e\<^sub>2) = \<lfloor>last_index ?Vs ` ?A\<rfloor>
\ (try e\<^sub>1 catch(C V') e\<^sub>2) = \<lfloor>A\<rfloor>
fv (try e\<^sub>1 catch(C V') e\<^sub>2) \<subseteq> set Vs
fv e\<^sub>2 \<subseteq> set (Vs @ [V'])
\ e\<^sub>1 = None
\ e\<^sub>2 = \<lfloor>A\<^sub>2\<rfloor>

goal (1 subgoal):
 1. \ (compE\<^sub>1 Vs (try e\<^sub>1 catch(C V') e\<^sub>2)) = \<lfloor>last_index Vs ` A\<rfloor>
[PROOF STEP]
by(auto simp add:hyperset_defs image_last_index last_index_size_conv)
[PROOF STATE]
proof (state)
this:
\ (compE\<^sub>1 Vs (try e\<^sub>1 catch(C V') e\<^sub>2)) = \<lfloor>last_index Vs ` A\<rfloor>

goal (1 subgoal):
 1. \<And>a. \ e\<^sub>1 = \<lfloor>a\<rfloor> \<Longrightarrow> \ (compE\<^sub>1 Vs (try e\<^sub>1 catch(C V') e\<^sub>2)) = \<lfloor>last_index Vs ` A\<rfloor>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. \ e\<^sub>1 = \<lfloor>a\<rfloor> \<Longrightarrow> \ (compE\<^sub>1 Vs (try e\<^sub>1 catch(C V') e\<^sub>2)) = \<lfloor>last_index Vs ` A\<rfloor>
[PROOF STEP]
fix A\<^sub>1
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. \ e\<^sub>1 = \<lfloor>a\<rfloor> \<Longrightarrow> \ (compE\<^sub>1 Vs (try e\<^sub>1 catch(C V') e\<^sub>2)) = \<lfloor>last_index Vs ` A\<rfloor>
[PROOF STEP]
assume A\<^sub>1: "\ e\<^sub>1 =  \<lfloor>A\<^sub>1\<rfloor>"
[PROOF STATE]
proof (state)
this:
\ e\<^sub>1 = \<lfloor>A\<^sub>1\<rfloor>

goal (1 subgoal):
 1. \<And>a. \ e\<^sub>1 = \<lfloor>a\<rfloor> \<Longrightarrow> \ (compE\<^sub>1 Vs (try e\<^sub>1 catch(C V') e\<^sub>2)) = \<lfloor>last_index Vs ` A\<rfloor>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \ (compE\<^sub>1 Vs (try e\<^sub>1 catch(C V') e\<^sub>2)) = \<lfloor>last_index Vs ` A\<rfloor>
[PROOF STEP]
proof (cases  "\ e\<^sub>2")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \ e\<^sub>2 = None \<Longrightarrow> \ (compE\<^sub>1 Vs (try e\<^sub>1 catch(C V') e\<^sub>2)) = \<lfloor>last_index Vs ` A\<rfloor>
 2. \<And>a. \ e\<^sub>2 = \<lfloor>a\<rfloor> \<Longrightarrow> \ (compE\<^sub>1 Vs (try e\<^sub>1 catch(C V') e\<^sub>2)) = \<lfloor>last_index Vs ` A\<rfloor>
[PROOF STEP]
assume A\<^sub>2: "\ e\<^sub>2 = None"
[PROOF STATE]
proof (state)
this:
\ e\<^sub>2 = None

goal (2 subgoals):
 1. \ e\<^sub>2 = None \<Longrightarrow> \ (compE\<^sub>1 Vs (try e\<^sub>1 catch(C V') e\<^sub>2)) = \<lfloor>last_index Vs ` A\<rfloor>
 2. \<And>a. \ e\<^sub>2 = \<lfloor>a\<rfloor> \<Longrightarrow> \ (compE\<^sub>1 Vs (try e\<^sub>1 catch(C V') e\<^sub>2)) = \<lfloor>last_index Vs ` A\<rfloor>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\ e\<^sub>2 = None
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\ e\<^sub>2 = None

goal (1 subgoal):
 1. \ (compE\<^sub>1 Vs (try e\<^sub>1 catch(C V') e\<^sub>2)) = \<lfloor>last_index Vs ` A\<rfloor>
[PROOF STEP]
using TryCatch A\<^sub>1
[PROOF STATE]
proof (prove)
using this:
\ e\<^sub>2 = None
\<lbrakk>\ e\<^sub>1 = \<lfloor>?A\<rfloor>; fv e\<^sub>1 \<subseteq> set ?Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 ?Vs e\<^sub>1) = \<lfloor>last_index ?Vs ` ?A\<rfloor>
\<lbrakk>\ e\<^sub>2 = \<lfloor>?A\<rfloor>; fv e\<^sub>2 \<subseteq> set ?Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 ?Vs e\<^sub>2) = \<lfloor>last_index ?Vs ` ?A\<rfloor>
\ (try e\<^sub>1 catch(C V') e\<^sub>2) = \<lfloor>A\<rfloor>
fv (try e\<^sub>1 catch(C V') e\<^sub>2) \<subseteq> set Vs
\ e\<^sub>1 = \<lfloor>A\<^sub>1\<rfloor>

goal (1 subgoal):
 1. \ (compE\<^sub>1 Vs (try e\<^sub>1 catch(C V') e\<^sub>2)) = \<lfloor>last_index Vs ` A\<rfloor>
[PROOF STEP]
by(simp add:hyperset_defs)
[PROOF STATE]
proof (state)
this:
\ (compE\<^sub>1 Vs (try e\<^sub>1 catch(C V') e\<^sub>2)) = \<lfloor>last_index Vs ` A\<rfloor>

goal (1 subgoal):
 1. \<And>a. \ e\<^sub>2 = \<lfloor>a\<rfloor> \<Longrightarrow> \ (compE\<^sub>1 Vs (try e\<^sub>1 catch(C V') e\<^sub>2)) = \<lfloor>last_index Vs ` A\<rfloor>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. \ e\<^sub>2 = \<lfloor>a\<rfloor> \<Longrightarrow> \ (compE\<^sub>1 Vs (try e\<^sub>1 catch(C V') e\<^sub>2)) = \<lfloor>last_index Vs ` A\<rfloor>
[PROOF STEP]
fix A\<^sub>2
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. \ e\<^sub>2 = \<lfloor>a\<rfloor> \<Longrightarrow> \ (compE\<^sub>1 Vs (try e\<^sub>1 catch(C V') e\<^sub>2)) = \<lfloor>last_index Vs ` A\<rfloor>
[PROOF STEP]
assume A\<^sub>2: "\ e\<^sub>2 = \<lfloor>A\<^sub>2\<rfloor>"
[PROOF STATE]
proof (state)
this:
\ e\<^sub>2 = \<lfloor>A\<^sub>2\<rfloor>

goal (1 subgoal):
 1. \<And>a. \ e\<^sub>2 = \<lfloor>a\<rfloor> \<Longrightarrow> \ (compE\<^sub>1 Vs (try e\<^sub>1 catch(C V') e\<^sub>2)) = \<lfloor>last_index Vs ` A\<rfloor>
[PROOF STEP]
have "A\<^sub>1 \<subseteq> set Vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A\<^sub>1 \<subseteq> set Vs
[PROOF STEP]
using TryCatch.prems A_fv[OF A\<^sub>1]
[PROOF STATE]
proof (prove)
using this:
\ (try e\<^sub>1 catch(C V') e\<^sub>2) = \<lfloor>A\<rfloor>
fv (try e\<^sub>1 catch(C V') e\<^sub>2) \<subseteq> set Vs
A\<^sub>1 \<subseteq> fv e\<^sub>1

goal (1 subgoal):
 1. A\<^sub>1 \<subseteq> set Vs
[PROOF STEP]
by simp blast
[PROOF STATE]
proof (state)
this:
A\<^sub>1 \<subseteq> set Vs

goal (1 subgoal):
 1. \<And>a. \ e\<^sub>2 = \<lfloor>a\<rfloor> \<Longrightarrow> \ (compE\<^sub>1 Vs (try e\<^sub>1 catch(C V') e\<^sub>2)) = \<lfloor>last_index Vs ` A\<rfloor>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
A\<^sub>1 \<subseteq> set Vs

goal (1 subgoal):
 1. \<And>a. \ e\<^sub>2 = \<lfloor>a\<rfloor> \<Longrightarrow> \ (compE\<^sub>1 Vs (try e\<^sub>1 catch(C V') e\<^sub>2)) = \<lfloor>last_index Vs ` A\<rfloor>
[PROOF STEP]
have "A\<^sub>2 \<subseteq> set (Vs@[V'])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A\<^sub>2 \<subseteq> set (Vs @ [V'])
[PROOF STEP]
using TryCatch.prems A_fv[OF A\<^sub>2]
[PROOF STATE]
proof (prove)
using this:
\ (try e\<^sub>1 catch(C V') e\<^sub>2) = \<lfloor>A\<rfloor>
fv (try e\<^sub>1 catch(C V') e\<^sub>2) \<subseteq> set Vs
A\<^sub>2 \<subseteq> fv e\<^sub>2

goal (1 subgoal):
 1. A\<^sub>2 \<subseteq> set (Vs @ [V'])
[PROOF STEP]
by simp blast
[PROOF STATE]
proof (state)
this:
A\<^sub>2 \<subseteq> set (Vs @ [V'])

goal (1 subgoal):
 1. \<And>a. \ e\<^sub>2 = \<lfloor>a\<rfloor> \<Longrightarrow> \ (compE\<^sub>1 Vs (try e\<^sub>1 catch(C V') e\<^sub>2)) = \<lfloor>last_index Vs ` A\<rfloor>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
A\<^sub>1 \<subseteq> set Vs
A\<^sub>2 \<subseteq> set (Vs @ [V'])
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
A\<^sub>1 \<subseteq> set Vs
A\<^sub>2 \<subseteq> set (Vs @ [V'])

goal (1 subgoal):
 1. \ (compE\<^sub>1 Vs (try e\<^sub>1 catch(C V') e\<^sub>2)) = \<lfloor>last_index Vs ` A\<rfloor>
[PROOF STEP]
using TryCatch A\<^sub>1 A\<^sub>2
[PROOF STATE]
proof (prove)
using this:
A\<^sub>1 \<subseteq> set Vs
A\<^sub>2 \<subseteq> set (Vs @ [V'])
\<lbrakk>\ e\<^sub>1 = \<lfloor>?A\<rfloor>; fv e\<^sub>1 \<subseteq> set ?Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 ?Vs e\<^sub>1) = \<lfloor>last_index ?Vs ` ?A\<rfloor>
\<lbrakk>\ e\<^sub>2 = \<lfloor>?A\<rfloor>; fv e\<^sub>2 \<subseteq> set ?Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 ?Vs e\<^sub>2) = \<lfloor>last_index ?Vs ` ?A\<rfloor>
\ (try e\<^sub>1 catch(C V') e\<^sub>2) = \<lfloor>A\<rfloor>
fv (try e\<^sub>1 catch(C V') e\<^sub>2) \<subseteq> set Vs
\ e\<^sub>1 = \<lfloor>A\<^sub>1\<rfloor>
\ e\<^sub>2 = \<lfloor>A\<^sub>2\<rfloor>

goal (1 subgoal):
 1. \ (compE\<^sub>1 Vs (try e\<^sub>1 catch(C V') e\<^sub>2)) = \<lfloor>last_index Vs ` A\<rfloor>
[PROOF STEP]
by (auto simp add: Diff_subset_conv last_index_size_conv subsetD hyperset_defs dest!: sym [of _ A])
[PROOF STATE]
proof (state)
this:
\ (compE\<^sub>1 Vs (try e\<^sub>1 catch(C V') e\<^sub>2)) = \<lfloor>last_index Vs ` A\<rfloor>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\ (compE\<^sub>1 Vs (try e\<^sub>1 catch(C V') e\<^sub>2)) = \<lfloor>last_index Vs ` A\<rfloor>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\ (compE\<^sub>1 Vs (try e\<^sub>1 catch(C V') e\<^sub>2)) = \<lfloor>last_index Vs ` A\<rfloor>

goal (15 subgoals):
 1. \<And>x A Vs. \<lbrakk>\ (new x) = \<lfloor>A\<rfloor>; fv (new x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (new x)) = \<lfloor>last_index Vs ` A\<rfloor>
 2. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (Cast x1 x2) = \<lfloor>A\<rfloor>; fv (Cast x1 x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (Cast x1 x2)) = \<lfloor>last_index Vs ` A\<rfloor>
 3. \<And>x A Vs. \<lbrakk>\ (Val x) = \<lfloor>A\<rfloor>; fv (Val x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (Val x)) = \<lfloor>last_index Vs ` A\<rfloor>
 4. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x3 = \<lfloor>A\<rfloor>; fv x3 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x3) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1 \<guillemotleft>x2\<guillemotright> x3) = \<lfloor>A\<rfloor>; fv (x1 \<guillemotleft>x2\<guillemotright> x3) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1 \<guillemotleft>x2\<guillemotright> x3)) = \<lfloor>last_index Vs ` A\<rfloor>
 5. \<And>x A Vs. \<lbrakk>\ (Var x) = \<lfloor>A\<rfloor>; fv (Var x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (Var x)) = \<lfloor>last_index Vs ` A\<rfloor>
 6. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (x1:=x2) = \<lfloor>A\<rfloor>; fv (x1:=x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (x1:=x2)) = \<lfloor>last_index Vs ` A\<rfloor>
 7. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (x1\<bullet>x2{x3}) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2{x3}) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (x1\<bullet>x2{x3})) = \<lfloor>last_index Vs ` A\<rfloor>
 8. \<And>x1 x2 x3 x4 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x4 = \<lfloor>A\<rfloor>; fv x4 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x4) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1\<bullet>x2{x3} := x4) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2{x3} := x4) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1\<bullet>x2{x3} := x4)) = \<lfloor>last_index Vs ` A\<rfloor>
 9. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A>s x3 = \<lfloor>A\<rfloor>; fvs x3 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A>s (compEs\<^sub>1 Vs x3) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1\<bullet>x2(x3)) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2(x3)) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1\<bullet>x2(x3))) = \<lfloor>last_index Vs ` A\<rfloor>
 10. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1;; x2) = \<lfloor>A\<rfloor>; fv (x1;; x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1;; x2)) = \<lfloor>last_index Vs ` A\<rfloor>
A total of 15 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (15 subgoals):
 1. \<And>x A Vs. \<lbrakk>\ (new x) = \<lfloor>A\<rfloor>; fv (new x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (new x)) = \<lfloor>last_index Vs ` A\<rfloor>
 2. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (Cast x1 x2) = \<lfloor>A\<rfloor>; fv (Cast x1 x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (Cast x1 x2)) = \<lfloor>last_index Vs ` A\<rfloor>
 3. \<And>x A Vs. \<lbrakk>\ (Val x) = \<lfloor>A\<rfloor>; fv (Val x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (Val x)) = \<lfloor>last_index Vs ` A\<rfloor>
 4. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x3 = \<lfloor>A\<rfloor>; fv x3 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x3) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1 \<guillemotleft>x2\<guillemotright> x3) = \<lfloor>A\<rfloor>; fv (x1 \<guillemotleft>x2\<guillemotright> x3) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1 \<guillemotleft>x2\<guillemotright> x3)) = \<lfloor>last_index Vs ` A\<rfloor>
 5. \<And>x A Vs. \<lbrakk>\ (Var x) = \<lfloor>A\<rfloor>; fv (Var x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (Var x)) = \<lfloor>last_index Vs ` A\<rfloor>
 6. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (x1:=x2) = \<lfloor>A\<rfloor>; fv (x1:=x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (x1:=x2)) = \<lfloor>last_index Vs ` A\<rfloor>
 7. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (x1\<bullet>x2{x3}) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2{x3}) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (x1\<bullet>x2{x3})) = \<lfloor>last_index Vs ` A\<rfloor>
 8. \<And>x1 x2 x3 x4 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x4 = \<lfloor>A\<rfloor>; fv x4 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x4) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1\<bullet>x2{x3} := x4) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2{x3} := x4) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1\<bullet>x2{x3} := x4)) = \<lfloor>last_index Vs ` A\<rfloor>
 9. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A>s x3 = \<lfloor>A\<rfloor>; fvs x3 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A>s (compEs\<^sub>1 Vs x3) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1\<bullet>x2(x3)) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2(x3)) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1\<bullet>x2(x3))) = \<lfloor>last_index Vs ` A\<rfloor>
 10. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1;; x2) = \<lfloor>A\<rfloor>; fv (x1;; x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1;; x2)) = \<lfloor>last_index Vs ` A\<rfloor>
A total of 15 subgoals...
[PROOF STEP]
case (Cond e e\<^sub>1 e\<^sub>2)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\ e = \<lfloor>?A\<rfloor>; fv e \<subseteq> set ?Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 ?Vs e) = \<lfloor>last_index ?Vs ` ?A\<rfloor>
\<lbrakk>\ e\<^sub>1 = \<lfloor>?A\<rfloor>; fv e\<^sub>1 \<subseteq> set ?Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 ?Vs e\<^sub>1) = \<lfloor>last_index ?Vs ` ?A\<rfloor>
\<lbrakk>\ e\<^sub>2 = \<lfloor>?A\<rfloor>; fv e\<^sub>2 \<subseteq> set ?Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 ?Vs e\<^sub>2) = \<lfloor>last_index ?Vs ` ?A\<rfloor>
\ (if (e) e\<^sub>1 else e\<^sub>2) = \<lfloor>A\<rfloor>
fv (if (e) e\<^sub>1 else e\<^sub>2) \<subseteq> set Vs

goal (15 subgoals):
 1. \<And>x A Vs. \<lbrakk>\ (new x) = \<lfloor>A\<rfloor>; fv (new x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (new x)) = \<lfloor>last_index Vs ` A\<rfloor>
 2. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (Cast x1 x2) = \<lfloor>A\<rfloor>; fv (Cast x1 x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (Cast x1 x2)) = \<lfloor>last_index Vs ` A\<rfloor>
 3. \<And>x A Vs. \<lbrakk>\ (Val x) = \<lfloor>A\<rfloor>; fv (Val x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (Val x)) = \<lfloor>last_index Vs ` A\<rfloor>
 4. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x3 = \<lfloor>A\<rfloor>; fv x3 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x3) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1 \<guillemotleft>x2\<guillemotright> x3) = \<lfloor>A\<rfloor>; fv (x1 \<guillemotleft>x2\<guillemotright> x3) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1 \<guillemotleft>x2\<guillemotright> x3)) = \<lfloor>last_index Vs ` A\<rfloor>
 5. \<And>x A Vs. \<lbrakk>\ (Var x) = \<lfloor>A\<rfloor>; fv (Var x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (Var x)) = \<lfloor>last_index Vs ` A\<rfloor>
 6. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (x1:=x2) = \<lfloor>A\<rfloor>; fv (x1:=x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (x1:=x2)) = \<lfloor>last_index Vs ` A\<rfloor>
 7. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (x1\<bullet>x2{x3}) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2{x3}) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (x1\<bullet>x2{x3})) = \<lfloor>last_index Vs ` A\<rfloor>
 8. \<And>x1 x2 x3 x4 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x4 = \<lfloor>A\<rfloor>; fv x4 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x4) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1\<bullet>x2{x3} := x4) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2{x3} := x4) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1\<bullet>x2{x3} := x4)) = \<lfloor>last_index Vs ` A\<rfloor>
 9. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A>s x3 = \<lfloor>A\<rfloor>; fvs x3 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A>s (compEs\<^sub>1 Vs x3) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1\<bullet>x2(x3)) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2(x3)) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1\<bullet>x2(x3))) = \<lfloor>last_index Vs ` A\<rfloor>
 10. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1;; x2) = \<lfloor>A\<rfloor>; fv (x1;; x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1;; x2)) = \<lfloor>last_index Vs ` A\<rfloor>
A total of 15 subgoals...
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>\ e = \<lfloor>?A\<rfloor>; fv e \<subseteq> set ?Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 ?Vs e) = \<lfloor>last_index ?Vs ` ?A\<rfloor>
\<lbrakk>\ e\<^sub>1 = \<lfloor>?A\<rfloor>; fv e\<^sub>1 \<subseteq> set ?Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 ?Vs e\<^sub>1) = \<lfloor>last_index ?Vs ` ?A\<rfloor>
\<lbrakk>\ e\<^sub>2 = \<lfloor>?A\<rfloor>; fv e\<^sub>2 \<subseteq> set ?Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 ?Vs e\<^sub>2) = \<lfloor>last_index ?Vs ` ?A\<rfloor>
\ (if (e) e\<^sub>1 else e\<^sub>2) = \<lfloor>A\<rfloor>
fv (if (e) e\<^sub>1 else e\<^sub>2) \<subseteq> set Vs

goal (15 subgoals):
 1. \<And>x A Vs. \<lbrakk>\ (new x) = \<lfloor>A\<rfloor>; fv (new x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (new x)) = \<lfloor>last_index Vs ` A\<rfloor>
 2. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (Cast x1 x2) = \<lfloor>A\<rfloor>; fv (Cast x1 x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (Cast x1 x2)) = \<lfloor>last_index Vs ` A\<rfloor>
 3. \<And>x A Vs. \<lbrakk>\ (Val x) = \<lfloor>A\<rfloor>; fv (Val x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (Val x)) = \<lfloor>last_index Vs ` A\<rfloor>
 4. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x3 = \<lfloor>A\<rfloor>; fv x3 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x3) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1 \<guillemotleft>x2\<guillemotright> x3) = \<lfloor>A\<rfloor>; fv (x1 \<guillemotleft>x2\<guillemotright> x3) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1 \<guillemotleft>x2\<guillemotright> x3)) = \<lfloor>last_index Vs ` A\<rfloor>
 5. \<And>x A Vs. \<lbrakk>\ (Var x) = \<lfloor>A\<rfloor>; fv (Var x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (Var x)) = \<lfloor>last_index Vs ` A\<rfloor>
 6. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (x1:=x2) = \<lfloor>A\<rfloor>; fv (x1:=x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (x1:=x2)) = \<lfloor>last_index Vs ` A\<rfloor>
 7. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (x1\<bullet>x2{x3}) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2{x3}) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (x1\<bullet>x2{x3})) = \<lfloor>last_index Vs ` A\<rfloor>
 8. \<And>x1 x2 x3 x4 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x4 = \<lfloor>A\<rfloor>; fv x4 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x4) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1\<bullet>x2{x3} := x4) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2{x3} := x4) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1\<bullet>x2{x3} := x4)) = \<lfloor>last_index Vs ` A\<rfloor>
 9. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A>s x3 = \<lfloor>A\<rfloor>; fvs x3 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A>s (compEs\<^sub>1 Vs x3) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1\<bullet>x2(x3)) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2(x3)) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1\<bullet>x2(x3))) = \<lfloor>last_index Vs ` A\<rfloor>
 10. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1;; x2) = \<lfloor>A\<rfloor>; fv (x1;; x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1;; x2)) = \<lfloor>last_index Vs ` A\<rfloor>
A total of 15 subgoals...
[PROOF STEP]
assume "\ e = None \<or> \ e\<^sub>1 = None \<or> \ e\<^sub>2 = None"
[PROOF STATE]
proof (state)
this:
\ e = None \<or> \ e\<^sub>1 = None \<or> \ e\<^sub>2 = None

goal (15 subgoals):
 1. \<And>x A Vs. \<lbrakk>\ (new x) = \<lfloor>A\<rfloor>; fv (new x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (new x)) = \<lfloor>last_index Vs ` A\<rfloor>
 2. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (Cast x1 x2) = \<lfloor>A\<rfloor>; fv (Cast x1 x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (Cast x1 x2)) = \<lfloor>last_index Vs ` A\<rfloor>
 3. \<And>x A Vs. \<lbrakk>\ (Val x) = \<lfloor>A\<rfloor>; fv (Val x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (Val x)) = \<lfloor>last_index Vs ` A\<rfloor>
 4. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x3 = \<lfloor>A\<rfloor>; fv x3 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x3) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1 \<guillemotleft>x2\<guillemotright> x3) = \<lfloor>A\<rfloor>; fv (x1 \<guillemotleft>x2\<guillemotright> x3) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1 \<guillemotleft>x2\<guillemotright> x3)) = \<lfloor>last_index Vs ` A\<rfloor>
 5. \<And>x A Vs. \<lbrakk>\ (Var x) = \<lfloor>A\<rfloor>; fv (Var x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (Var x)) = \<lfloor>last_index Vs ` A\<rfloor>
 6. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (x1:=x2) = \<lfloor>A\<rfloor>; fv (x1:=x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (x1:=x2)) = \<lfloor>last_index Vs ` A\<rfloor>
 7. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (x1\<bullet>x2{x3}) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2{x3}) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (x1\<bullet>x2{x3})) = \<lfloor>last_index Vs ` A\<rfloor>
 8. \<And>x1 x2 x3 x4 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x4 = \<lfloor>A\<rfloor>; fv x4 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x4) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1\<bullet>x2{x3} := x4) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2{x3} := x4) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1\<bullet>x2{x3} := x4)) = \<lfloor>last_index Vs ` A\<rfloor>
 9. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A>s x3 = \<lfloor>A\<rfloor>; fvs x3 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A>s (compEs\<^sub>1 Vs x3) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1\<bullet>x2(x3)) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2(x3)) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1\<bullet>x2(x3))) = \<lfloor>last_index Vs ` A\<rfloor>
 10. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1;; x2) = \<lfloor>A\<rfloor>; fv (x1;; x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1;; x2)) = \<lfloor>last_index Vs ` A\<rfloor>
A total of 15 subgoals...
[PROOF STEP]
hence ?case
[PROOF STATE]
proof (prove)
using this:
\ e = None \<or> \ e\<^sub>1 = None \<or> \ e\<^sub>2 = None

goal (1 subgoal):
 1. \ (compE\<^sub>1 Vs (if (e) e\<^sub>1 else e\<^sub>2)) = \<lfloor>last_index Vs ` A\<rfloor>
[PROOF STEP]
using Cond
[PROOF STATE]
proof (prove)
using this:
\ e = None \<or> \ e\<^sub>1 = None \<or> \ e\<^sub>2 = None
\<lbrakk>\ e = \<lfloor>?A\<rfloor>; fv e \<subseteq> set ?Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 ?Vs e) = \<lfloor>last_index ?Vs ` ?A\<rfloor>
\<lbrakk>\ e\<^sub>1 = \<lfloor>?A\<rfloor>; fv e\<^sub>1 \<subseteq> set ?Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 ?Vs e\<^sub>1) = \<lfloor>last_index ?Vs ` ?A\<rfloor>
\<lbrakk>\ e\<^sub>2 = \<lfloor>?A\<rfloor>; fv e\<^sub>2 \<subseteq> set ?Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 ?Vs e\<^sub>2) = \<lfloor>last_index ?Vs ` ?A\<rfloor>
\ (if (e) e\<^sub>1 else e\<^sub>2) = \<lfloor>A\<rfloor>
fv (if (e) e\<^sub>1 else e\<^sub>2) \<subseteq> set Vs

goal (1 subgoal):
 1. \ (compE\<^sub>1 Vs (if (e) e\<^sub>1 else e\<^sub>2)) = \<lfloor>last_index Vs ` A\<rfloor>
[PROOF STEP]
by (auto simp add: hyperset_defs)
[PROOF STATE]
proof (state)
this:
\ (compE\<^sub>1 Vs (if (e) e\<^sub>1 else e\<^sub>2)) = \<lfloor>last_index Vs ` A\<rfloor>

goal (15 subgoals):
 1. \<And>x A Vs. \<lbrakk>\ (new x) = \<lfloor>A\<rfloor>; fv (new x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (new x)) = \<lfloor>last_index Vs ` A\<rfloor>
 2. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (Cast x1 x2) = \<lfloor>A\<rfloor>; fv (Cast x1 x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (Cast x1 x2)) = \<lfloor>last_index Vs ` A\<rfloor>
 3. \<And>x A Vs. \<lbrakk>\ (Val x) = \<lfloor>A\<rfloor>; fv (Val x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (Val x)) = \<lfloor>last_index Vs ` A\<rfloor>
 4. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x3 = \<lfloor>A\<rfloor>; fv x3 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x3) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1 \<guillemotleft>x2\<guillemotright> x3) = \<lfloor>A\<rfloor>; fv (x1 \<guillemotleft>x2\<guillemotright> x3) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1 \<guillemotleft>x2\<guillemotright> x3)) = \<lfloor>last_index Vs ` A\<rfloor>
 5. \<And>x A Vs. \<lbrakk>\ (Var x) = \<lfloor>A\<rfloor>; fv (Var x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (Var x)) = \<lfloor>last_index Vs ` A\<rfloor>
 6. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (x1:=x2) = \<lfloor>A\<rfloor>; fv (x1:=x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (x1:=x2)) = \<lfloor>last_index Vs ` A\<rfloor>
 7. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (x1\<bullet>x2{x3}) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2{x3}) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (x1\<bullet>x2{x3})) = \<lfloor>last_index Vs ` A\<rfloor>
 8. \<And>x1 x2 x3 x4 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x4 = \<lfloor>A\<rfloor>; fv x4 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x4) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1\<bullet>x2{x3} := x4) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2{x3} := x4) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1\<bullet>x2{x3} := x4)) = \<lfloor>last_index Vs ` A\<rfloor>
 9. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A>s x3 = \<lfloor>A\<rfloor>; fvs x3 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A>s (compEs\<^sub>1 Vs x3) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1\<bullet>x2(x3)) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2(x3)) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1\<bullet>x2(x3))) = \<lfloor>last_index Vs ` A\<rfloor>
 10. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1;; x2) = \<lfloor>A\<rfloor>; fv (x1;; x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1;; x2)) = \<lfloor>last_index Vs ` A\<rfloor>
A total of 15 subgoals...
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\ e = None \<or> \ e\<^sub>1 = None \<or> \ e\<^sub>2 = None \<Longrightarrow> \ (compE\<^sub>1 Vs (if (e) e\<^sub>1 else e\<^sub>2)) = \<lfloor>last_index Vs ` A\<rfloor>

goal (15 subgoals):
 1. \<And>x A Vs. \<lbrakk>\ (new x) = \<lfloor>A\<rfloor>; fv (new x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (new x)) = \<lfloor>last_index Vs ` A\<rfloor>
 2. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (Cast x1 x2) = \<lfloor>A\<rfloor>; fv (Cast x1 x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (Cast x1 x2)) = \<lfloor>last_index Vs ` A\<rfloor>
 3. \<And>x A Vs. \<lbrakk>\ (Val x) = \<lfloor>A\<rfloor>; fv (Val x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (Val x)) = \<lfloor>last_index Vs ` A\<rfloor>
 4. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x3 = \<lfloor>A\<rfloor>; fv x3 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x3) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1 \<guillemotleft>x2\<guillemotright> x3) = \<lfloor>A\<rfloor>; fv (x1 \<guillemotleft>x2\<guillemotright> x3) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1 \<guillemotleft>x2\<guillemotright> x3)) = \<lfloor>last_index Vs ` A\<rfloor>
 5. \<And>x A Vs. \<lbrakk>\ (Var x) = \<lfloor>A\<rfloor>; fv (Var x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (Var x)) = \<lfloor>last_index Vs ` A\<rfloor>
 6. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (x1:=x2) = \<lfloor>A\<rfloor>; fv (x1:=x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (x1:=x2)) = \<lfloor>last_index Vs ` A\<rfloor>
 7. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (x1\<bullet>x2{x3}) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2{x3}) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (x1\<bullet>x2{x3})) = \<lfloor>last_index Vs ` A\<rfloor>
 8. \<And>x1 x2 x3 x4 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x4 = \<lfloor>A\<rfloor>; fv x4 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x4) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1\<bullet>x2{x3} := x4) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2{x3} := x4) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1\<bullet>x2{x3} := x4)) = \<lfloor>last_index Vs ` A\<rfloor>
 9. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A>s x3 = \<lfloor>A\<rfloor>; fvs x3 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A>s (compEs\<^sub>1 Vs x3) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1\<bullet>x2(x3)) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2(x3)) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1\<bullet>x2(x3))) = \<lfloor>last_index Vs ` A\<rfloor>
 10. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1;; x2) = \<lfloor>A\<rfloor>; fv (x1;; x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1;; x2)) = \<lfloor>last_index Vs ` A\<rfloor>
A total of 15 subgoals...
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\ e = None \<or> \ e\<^sub>1 = None \<or> \ e\<^sub>2 = None \<Longrightarrow> \ (compE\<^sub>1 Vs (if (e) e\<^sub>1 else e\<^sub>2)) = \<lfloor>last_index Vs ` A\<rfloor>

goal (15 subgoals):
 1. \<And>x A Vs. \<lbrakk>\ (new x) = \<lfloor>A\<rfloor>; fv (new x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (new x)) = \<lfloor>last_index Vs ` A\<rfloor>
 2. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (Cast x1 x2) = \<lfloor>A\<rfloor>; fv (Cast x1 x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (Cast x1 x2)) = \<lfloor>last_index Vs ` A\<rfloor>
 3. \<And>x A Vs. \<lbrakk>\ (Val x) = \<lfloor>A\<rfloor>; fv (Val x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (Val x)) = \<lfloor>last_index Vs ` A\<rfloor>
 4. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x3 = \<lfloor>A\<rfloor>; fv x3 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x3) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1 \<guillemotleft>x2\<guillemotright> x3) = \<lfloor>A\<rfloor>; fv (x1 \<guillemotleft>x2\<guillemotright> x3) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1 \<guillemotleft>x2\<guillemotright> x3)) = \<lfloor>last_index Vs ` A\<rfloor>
 5. \<And>x A Vs. \<lbrakk>\ (Var x) = \<lfloor>A\<rfloor>; fv (Var x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (Var x)) = \<lfloor>last_index Vs ` A\<rfloor>
 6. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (x1:=x2) = \<lfloor>A\<rfloor>; fv (x1:=x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (x1:=x2)) = \<lfloor>last_index Vs ` A\<rfloor>
 7. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (x1\<bullet>x2{x3}) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2{x3}) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (x1\<bullet>x2{x3})) = \<lfloor>last_index Vs ` A\<rfloor>
 8. \<And>x1 x2 x3 x4 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x4 = \<lfloor>A\<rfloor>; fv x4 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x4) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1\<bullet>x2{x3} := x4) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2{x3} := x4) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1\<bullet>x2{x3} := x4)) = \<lfloor>last_index Vs ` A\<rfloor>
 9. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A>s x3 = \<lfloor>A\<rfloor>; fvs x3 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A>s (compEs\<^sub>1 Vs x3) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1\<bullet>x2(x3)) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2(x3)) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1\<bullet>x2(x3))) = \<lfloor>last_index Vs ` A\<rfloor>
 10. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1;; x2) = \<lfloor>A\<rfloor>; fv (x1;; x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1;; x2)) = \<lfloor>last_index Vs ` A\<rfloor>
A total of 15 subgoals...
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\ e = None \<or> \ e\<^sub>1 = None \<or> \ e\<^sub>2 = None \<Longrightarrow> \ (compE\<^sub>1 Vs (if (e) e\<^sub>1 else e\<^sub>2)) = \<lfloor>last_index Vs ` A\<rfloor>

goal (15 subgoals):
 1. \<And>x A Vs. \<lbrakk>\ (new x) = \<lfloor>A\<rfloor>; fv (new x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (new x)) = \<lfloor>last_index Vs ` A\<rfloor>
 2. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (Cast x1 x2) = \<lfloor>A\<rfloor>; fv (Cast x1 x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (Cast x1 x2)) = \<lfloor>last_index Vs ` A\<rfloor>
 3. \<And>x A Vs. \<lbrakk>\ (Val x) = \<lfloor>A\<rfloor>; fv (Val x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (Val x)) = \<lfloor>last_index Vs ` A\<rfloor>
 4. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x3 = \<lfloor>A\<rfloor>; fv x3 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x3) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1 \<guillemotleft>x2\<guillemotright> x3) = \<lfloor>A\<rfloor>; fv (x1 \<guillemotleft>x2\<guillemotright> x3) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1 \<guillemotleft>x2\<guillemotright> x3)) = \<lfloor>last_index Vs ` A\<rfloor>
 5. \<And>x A Vs. \<lbrakk>\ (Var x) = \<lfloor>A\<rfloor>; fv (Var x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (Var x)) = \<lfloor>last_index Vs ` A\<rfloor>
 6. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (x1:=x2) = \<lfloor>A\<rfloor>; fv (x1:=x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (x1:=x2)) = \<lfloor>last_index Vs ` A\<rfloor>
 7. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (x1\<bullet>x2{x3}) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2{x3}) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (x1\<bullet>x2{x3})) = \<lfloor>last_index Vs ` A\<rfloor>
 8. \<And>x1 x2 x3 x4 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x4 = \<lfloor>A\<rfloor>; fv x4 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x4) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1\<bullet>x2{x3} := x4) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2{x3} := x4) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1\<bullet>x2{x3} := x4)) = \<lfloor>last_index Vs ` A\<rfloor>
 9. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A>s x3 = \<lfloor>A\<rfloor>; fvs x3 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A>s (compEs\<^sub>1 Vs x3) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1\<bullet>x2(x3)) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2(x3)) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1\<bullet>x2(x3))) = \<lfloor>last_index Vs ` A\<rfloor>
 10. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1;; x2) = \<lfloor>A\<rfloor>; fv (x1;; x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1;; x2)) = \<lfloor>last_index Vs ` A\<rfloor>
A total of 15 subgoals...
[PROOF STEP]
fix A A\<^sub>1 A\<^sub>2
[PROOF STATE]
proof (state)
goal (15 subgoals):
 1. \<And>x A Vs. \<lbrakk>\ (new x) = \<lfloor>A\<rfloor>; fv (new x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (new x)) = \<lfloor>last_index Vs ` A\<rfloor>
 2. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (Cast x1 x2) = \<lfloor>A\<rfloor>; fv (Cast x1 x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (Cast x1 x2)) = \<lfloor>last_index Vs ` A\<rfloor>
 3. \<And>x A Vs. \<lbrakk>\ (Val x) = \<lfloor>A\<rfloor>; fv (Val x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (Val x)) = \<lfloor>last_index Vs ` A\<rfloor>
 4. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x3 = \<lfloor>A\<rfloor>; fv x3 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x3) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1 \<guillemotleft>x2\<guillemotright> x3) = \<lfloor>A\<rfloor>; fv (x1 \<guillemotleft>x2\<guillemotright> x3) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1 \<guillemotleft>x2\<guillemotright> x3)) = \<lfloor>last_index Vs ` A\<rfloor>
 5. \<And>x A Vs. \<lbrakk>\ (Var x) = \<lfloor>A\<rfloor>; fv (Var x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (Var x)) = \<lfloor>last_index Vs ` A\<rfloor>
 6. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (x1:=x2) = \<lfloor>A\<rfloor>; fv (x1:=x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (x1:=x2)) = \<lfloor>last_index Vs ` A\<rfloor>
 7. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (x1\<bullet>x2{x3}) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2{x3}) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (x1\<bullet>x2{x3})) = \<lfloor>last_index Vs ` A\<rfloor>
 8. \<And>x1 x2 x3 x4 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x4 = \<lfloor>A\<rfloor>; fv x4 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x4) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1\<bullet>x2{x3} := x4) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2{x3} := x4) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1\<bullet>x2{x3} := x4)) = \<lfloor>last_index Vs ` A\<rfloor>
 9. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A>s x3 = \<lfloor>A\<rfloor>; fvs x3 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A>s (compEs\<^sub>1 Vs x3) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1\<bullet>x2(x3)) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2(x3)) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1\<bullet>x2(x3))) = \<lfloor>last_index Vs ` A\<rfloor>
 10. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1;; x2) = \<lfloor>A\<rfloor>; fv (x1;; x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1;; x2)) = \<lfloor>last_index Vs ` A\<rfloor>
A total of 15 subgoals...
[PROOF STEP]
assume "\ e = \<lfloor>A\<rfloor>" and A\<^sub>1: "\ e\<^sub>1 = \<lfloor>A\<^sub>1\<rfloor>" and A\<^sub>2: "\ e\<^sub>2 = \<lfloor>A\<^sub>2\<rfloor>"
[PROOF STATE]
proof (state)
this:
\ e = \<lfloor>A\<rfloor>
\ e\<^sub>1 = \<lfloor>A\<^sub>1\<rfloor>
\ e\<^sub>2 = \<lfloor>A\<^sub>2\<rfloor>

goal (15 subgoals):
 1. \<And>x A Vs. \<lbrakk>\ (new x) = \<lfloor>A\<rfloor>; fv (new x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (new x)) = \<lfloor>last_index Vs ` A\<rfloor>
 2. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (Cast x1 x2) = \<lfloor>A\<rfloor>; fv (Cast x1 x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (Cast x1 x2)) = \<lfloor>last_index Vs ` A\<rfloor>
 3. \<And>x A Vs. \<lbrakk>\ (Val x) = \<lfloor>A\<rfloor>; fv (Val x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (Val x)) = \<lfloor>last_index Vs ` A\<rfloor>
 4. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x3 = \<lfloor>A\<rfloor>; fv x3 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x3) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1 \<guillemotleft>x2\<guillemotright> x3) = \<lfloor>A\<rfloor>; fv (x1 \<guillemotleft>x2\<guillemotright> x3) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1 \<guillemotleft>x2\<guillemotright> x3)) = \<lfloor>last_index Vs ` A\<rfloor>
 5. \<And>x A Vs. \<lbrakk>\ (Var x) = \<lfloor>A\<rfloor>; fv (Var x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (Var x)) = \<lfloor>last_index Vs ` A\<rfloor>
 6. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (x1:=x2) = \<lfloor>A\<rfloor>; fv (x1:=x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (x1:=x2)) = \<lfloor>last_index Vs ` A\<rfloor>
 7. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (x1\<bullet>x2{x3}) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2{x3}) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (x1\<bullet>x2{x3})) = \<lfloor>last_index Vs ` A\<rfloor>
 8. \<And>x1 x2 x3 x4 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x4 = \<lfloor>A\<rfloor>; fv x4 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x4) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1\<bullet>x2{x3} := x4) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2{x3} := x4) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1\<bullet>x2{x3} := x4)) = \<lfloor>last_index Vs ` A\<rfloor>
 9. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A>s x3 = \<lfloor>A\<rfloor>; fvs x3 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A>s (compEs\<^sub>1 Vs x3) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1\<bullet>x2(x3)) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2(x3)) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1\<bullet>x2(x3))) = \<lfloor>last_index Vs ` A\<rfloor>
 10. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1;; x2) = \<lfloor>A\<rfloor>; fv (x1;; x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1;; x2)) = \<lfloor>last_index Vs ` A\<rfloor>
A total of 15 subgoals...
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\ e = \<lfloor>A\<rfloor>
\ e\<^sub>1 = \<lfloor>A\<^sub>1\<rfloor>
\ e\<^sub>2 = \<lfloor>A\<^sub>2\<rfloor>

goal (15 subgoals):
 1. \<And>x A Vs. \<lbrakk>\ (new x) = \<lfloor>A\<rfloor>; fv (new x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (new x)) = \<lfloor>last_index Vs ` A\<rfloor>
 2. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (Cast x1 x2) = \<lfloor>A\<rfloor>; fv (Cast x1 x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (Cast x1 x2)) = \<lfloor>last_index Vs ` A\<rfloor>
 3. \<And>x A Vs. \<lbrakk>\ (Val x) = \<lfloor>A\<rfloor>; fv (Val x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (Val x)) = \<lfloor>last_index Vs ` A\<rfloor>
 4. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x3 = \<lfloor>A\<rfloor>; fv x3 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x3) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1 \<guillemotleft>x2\<guillemotright> x3) = \<lfloor>A\<rfloor>; fv (x1 \<guillemotleft>x2\<guillemotright> x3) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1 \<guillemotleft>x2\<guillemotright> x3)) = \<lfloor>last_index Vs ` A\<rfloor>
 5. \<And>x A Vs. \<lbrakk>\ (Var x) = \<lfloor>A\<rfloor>; fv (Var x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (Var x)) = \<lfloor>last_index Vs ` A\<rfloor>
 6. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (x1:=x2) = \<lfloor>A\<rfloor>; fv (x1:=x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (x1:=x2)) = \<lfloor>last_index Vs ` A\<rfloor>
 7. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (x1\<bullet>x2{x3}) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2{x3}) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (x1\<bullet>x2{x3})) = \<lfloor>last_index Vs ` A\<rfloor>
 8. \<And>x1 x2 x3 x4 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x4 = \<lfloor>A\<rfloor>; fv x4 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x4) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1\<bullet>x2{x3} := x4) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2{x3} := x4) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1\<bullet>x2{x3} := x4)) = \<lfloor>last_index Vs ` A\<rfloor>
 9. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A>s x3 = \<lfloor>A\<rfloor>; fvs x3 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A>s (compEs\<^sub>1 Vs x3) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1\<bullet>x2(x3)) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2(x3)) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1\<bullet>x2(x3))) = \<lfloor>last_index Vs ` A\<rfloor>
 10. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1;; x2) = \<lfloor>A\<rfloor>; fv (x1;; x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1;; x2)) = \<lfloor>last_index Vs ` A\<rfloor>
A total of 15 subgoals...
[PROOF STEP]
have "A\<^sub>1 \<subseteq> set Vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A\<^sub>1 \<subseteq> set Vs
[PROOF STEP]
using Cond.prems A_fv[OF A\<^sub>1]
[PROOF STATE]
proof (prove)
using this:
\ (if (e) e\<^sub>1 else e\<^sub>2) = \<lfloor>A__\<rfloor>
fv (if (e) e\<^sub>1 else e\<^sub>2) \<subseteq> set Vs
A\<^sub>1 \<subseteq> fv e\<^sub>1

goal (1 subgoal):
 1. A\<^sub>1 \<subseteq> set Vs
[PROOF STEP]
by simp blast
[PROOF STATE]
proof (state)
this:
A\<^sub>1 \<subseteq> set Vs

goal (15 subgoals):
 1. \<And>x A Vs. \<lbrakk>\ (new x) = \<lfloor>A\<rfloor>; fv (new x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (new x)) = \<lfloor>last_index Vs ` A\<rfloor>
 2. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (Cast x1 x2) = \<lfloor>A\<rfloor>; fv (Cast x1 x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (Cast x1 x2)) = \<lfloor>last_index Vs ` A\<rfloor>
 3. \<And>x A Vs. \<lbrakk>\ (Val x) = \<lfloor>A\<rfloor>; fv (Val x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (Val x)) = \<lfloor>last_index Vs ` A\<rfloor>
 4. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x3 = \<lfloor>A\<rfloor>; fv x3 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x3) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1 \<guillemotleft>x2\<guillemotright> x3) = \<lfloor>A\<rfloor>; fv (x1 \<guillemotleft>x2\<guillemotright> x3) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1 \<guillemotleft>x2\<guillemotright> x3)) = \<lfloor>last_index Vs ` A\<rfloor>
 5. \<And>x A Vs. \<lbrakk>\ (Var x) = \<lfloor>A\<rfloor>; fv (Var x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (Var x)) = \<lfloor>last_index Vs ` A\<rfloor>
 6. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (x1:=x2) = \<lfloor>A\<rfloor>; fv (x1:=x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (x1:=x2)) = \<lfloor>last_index Vs ` A\<rfloor>
 7. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (x1\<bullet>x2{x3}) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2{x3}) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (x1\<bullet>x2{x3})) = \<lfloor>last_index Vs ` A\<rfloor>
 8. \<And>x1 x2 x3 x4 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x4 = \<lfloor>A\<rfloor>; fv x4 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x4) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1\<bullet>x2{x3} := x4) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2{x3} := x4) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1\<bullet>x2{x3} := x4)) = \<lfloor>last_index Vs ` A\<rfloor>
 9. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A>s x3 = \<lfloor>A\<rfloor>; fvs x3 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A>s (compEs\<^sub>1 Vs x3) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1\<bullet>x2(x3)) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2(x3)) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1\<bullet>x2(x3))) = \<lfloor>last_index Vs ` A\<rfloor>
 10. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1;; x2) = \<lfloor>A\<rfloor>; fv (x1;; x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1;; x2)) = \<lfloor>last_index Vs ` A\<rfloor>
A total of 15 subgoals...
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
A\<^sub>1 \<subseteq> set Vs

goal (15 subgoals):
 1. \<And>x A Vs. \<lbrakk>\ (new x) = \<lfloor>A\<rfloor>; fv (new x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (new x)) = \<lfloor>last_index Vs ` A\<rfloor>
 2. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (Cast x1 x2) = \<lfloor>A\<rfloor>; fv (Cast x1 x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (Cast x1 x2)) = \<lfloor>last_index Vs ` A\<rfloor>
 3. \<And>x A Vs. \<lbrakk>\ (Val x) = \<lfloor>A\<rfloor>; fv (Val x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (Val x)) = \<lfloor>last_index Vs ` A\<rfloor>
 4. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x3 = \<lfloor>A\<rfloor>; fv x3 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x3) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1 \<guillemotleft>x2\<guillemotright> x3) = \<lfloor>A\<rfloor>; fv (x1 \<guillemotleft>x2\<guillemotright> x3) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1 \<guillemotleft>x2\<guillemotright> x3)) = \<lfloor>last_index Vs ` A\<rfloor>
 5. \<And>x A Vs. \<lbrakk>\ (Var x) = \<lfloor>A\<rfloor>; fv (Var x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (Var x)) = \<lfloor>last_index Vs ` A\<rfloor>
 6. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (x1:=x2) = \<lfloor>A\<rfloor>; fv (x1:=x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (x1:=x2)) = \<lfloor>last_index Vs ` A\<rfloor>
 7. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (x1\<bullet>x2{x3}) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2{x3}) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (x1\<bullet>x2{x3})) = \<lfloor>last_index Vs ` A\<rfloor>
 8. \<And>x1 x2 x3 x4 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x4 = \<lfloor>A\<rfloor>; fv x4 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x4) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1\<bullet>x2{x3} := x4) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2{x3} := x4) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1\<bullet>x2{x3} := x4)) = \<lfloor>last_index Vs ` A\<rfloor>
 9. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A>s x3 = \<lfloor>A\<rfloor>; fvs x3 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A>s (compEs\<^sub>1 Vs x3) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1\<bullet>x2(x3)) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2(x3)) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1\<bullet>x2(x3))) = \<lfloor>last_index Vs ` A\<rfloor>
 10. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1;; x2) = \<lfloor>A\<rfloor>; fv (x1;; x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1;; x2)) = \<lfloor>last_index Vs ` A\<rfloor>
A total of 15 subgoals...
[PROOF STEP]
have "A\<^sub>2 \<subseteq> set Vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A\<^sub>2 \<subseteq> set Vs
[PROOF STEP]
using Cond.prems A_fv[OF A\<^sub>2]
[PROOF STATE]
proof (prove)
using this:
\ (if (e) e\<^sub>1 else e\<^sub>2) = \<lfloor>A__\<rfloor>
fv (if (e) e\<^sub>1 else e\<^sub>2) \<subseteq> set Vs
A\<^sub>2 \<subseteq> fv e\<^sub>2

goal (1 subgoal):
 1. A\<^sub>2 \<subseteq> set Vs
[PROOF STEP]
by simp blast
[PROOF STATE]
proof (state)
this:
A\<^sub>2 \<subseteq> set Vs

goal (15 subgoals):
 1. \<And>x A Vs. \<lbrakk>\ (new x) = \<lfloor>A\<rfloor>; fv (new x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (new x)) = \<lfloor>last_index Vs ` A\<rfloor>
 2. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (Cast x1 x2) = \<lfloor>A\<rfloor>; fv (Cast x1 x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (Cast x1 x2)) = \<lfloor>last_index Vs ` A\<rfloor>
 3. \<And>x A Vs. \<lbrakk>\ (Val x) = \<lfloor>A\<rfloor>; fv (Val x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (Val x)) = \<lfloor>last_index Vs ` A\<rfloor>
 4. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x3 = \<lfloor>A\<rfloor>; fv x3 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x3) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1 \<guillemotleft>x2\<guillemotright> x3) = \<lfloor>A\<rfloor>; fv (x1 \<guillemotleft>x2\<guillemotright> x3) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1 \<guillemotleft>x2\<guillemotright> x3)) = \<lfloor>last_index Vs ` A\<rfloor>
 5. \<And>x A Vs. \<lbrakk>\ (Var x) = \<lfloor>A\<rfloor>; fv (Var x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (Var x)) = \<lfloor>last_index Vs ` A\<rfloor>
 6. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (x1:=x2) = \<lfloor>A\<rfloor>; fv (x1:=x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (x1:=x2)) = \<lfloor>last_index Vs ` A\<rfloor>
 7. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (x1\<bullet>x2{x3}) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2{x3}) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (x1\<bullet>x2{x3})) = \<lfloor>last_index Vs ` A\<rfloor>
 8. \<And>x1 x2 x3 x4 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x4 = \<lfloor>A\<rfloor>; fv x4 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x4) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1\<bullet>x2{x3} := x4) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2{x3} := x4) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1\<bullet>x2{x3} := x4)) = \<lfloor>last_index Vs ` A\<rfloor>
 9. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A>s x3 = \<lfloor>A\<rfloor>; fvs x3 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A>s (compEs\<^sub>1 Vs x3) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1\<bullet>x2(x3)) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2(x3)) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1\<bullet>x2(x3))) = \<lfloor>last_index Vs ` A\<rfloor>
 10. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1;; x2) = \<lfloor>A\<rfloor>; fv (x1;; x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1;; x2)) = \<lfloor>last_index Vs ` A\<rfloor>
A total of 15 subgoals...
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\ e = \<lfloor>A\<rfloor>
\ e\<^sub>1 = \<lfloor>A\<^sub>1\<rfloor>
\ e\<^sub>2 = \<lfloor>A\<^sub>2\<rfloor>
A\<^sub>1 \<subseteq> set Vs
A\<^sub>2 \<subseteq> set Vs
[PROOF STEP]
have ?case
[PROOF STATE]
proof (prove)
using this:
\ e = \<lfloor>A\<rfloor>
\ e\<^sub>1 = \<lfloor>A\<^sub>1\<rfloor>
\ e\<^sub>2 = \<lfloor>A\<^sub>2\<rfloor>
A\<^sub>1 \<subseteq> set Vs
A\<^sub>2 \<subseteq> set Vs

goal (1 subgoal):
 1. \ (compE\<^sub>1 Vs (if (e) e\<^sub>1 else e\<^sub>2)) = \<lfloor>last_index Vs ` A__\<rfloor>
[PROOF STEP]
using Cond
[PROOF STATE]
proof (prove)
using this:
\ e = \<lfloor>A\<rfloor>
\ e\<^sub>1 = \<lfloor>A\<^sub>1\<rfloor>
\ e\<^sub>2 = \<lfloor>A\<^sub>2\<rfloor>
A\<^sub>1 \<subseteq> set Vs
A\<^sub>2 \<subseteq> set Vs
\<lbrakk>\ e = \<lfloor>?A\<rfloor>; fv e \<subseteq> set ?Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 ?Vs e) = \<lfloor>last_index ?Vs ` ?A\<rfloor>
\<lbrakk>\ e\<^sub>1 = \<lfloor>?A\<rfloor>; fv e\<^sub>1 \<subseteq> set ?Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 ?Vs e\<^sub>1) = \<lfloor>last_index ?Vs ` ?A\<rfloor>
\<lbrakk>\ e\<^sub>2 = \<lfloor>?A\<rfloor>; fv e\<^sub>2 \<subseteq> set ?Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 ?Vs e\<^sub>2) = \<lfloor>last_index ?Vs ` ?A\<rfloor>
\ (if (e) e\<^sub>1 else e\<^sub>2) = \<lfloor>A__\<rfloor>
fv (if (e) e\<^sub>1 else e\<^sub>2) \<subseteq> set Vs

goal (1 subgoal):
 1. \ (compE\<^sub>1 Vs (if (e) e\<^sub>1 else e\<^sub>2)) = \<lfloor>last_index Vs ` A__\<rfloor>
[PROOF STEP]
by(auto simp add:hyperset_defs image_Un
          inj_on_image_Int[OF inj_on_last_index])
[PROOF STATE]
proof (state)
this:
\ (compE\<^sub>1 Vs (if (e) e\<^sub>1 else e\<^sub>2)) = \<lfloor>last_index Vs ` A__\<rfloor>

goal (15 subgoals):
 1. \<And>x A Vs. \<lbrakk>\ (new x) = \<lfloor>A\<rfloor>; fv (new x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (new x)) = \<lfloor>last_index Vs ` A\<rfloor>
 2. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (Cast x1 x2) = \<lfloor>A\<rfloor>; fv (Cast x1 x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (Cast x1 x2)) = \<lfloor>last_index Vs ` A\<rfloor>
 3. \<And>x A Vs. \<lbrakk>\ (Val x) = \<lfloor>A\<rfloor>; fv (Val x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (Val x)) = \<lfloor>last_index Vs ` A\<rfloor>
 4. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x3 = \<lfloor>A\<rfloor>; fv x3 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x3) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1 \<guillemotleft>x2\<guillemotright> x3) = \<lfloor>A\<rfloor>; fv (x1 \<guillemotleft>x2\<guillemotright> x3) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1 \<guillemotleft>x2\<guillemotright> x3)) = \<lfloor>last_index Vs ` A\<rfloor>
 5. \<And>x A Vs. \<lbrakk>\ (Var x) = \<lfloor>A\<rfloor>; fv (Var x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (Var x)) = \<lfloor>last_index Vs ` A\<rfloor>
 6. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (x1:=x2) = \<lfloor>A\<rfloor>; fv (x1:=x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (x1:=x2)) = \<lfloor>last_index Vs ` A\<rfloor>
 7. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (x1\<bullet>x2{x3}) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2{x3}) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (x1\<bullet>x2{x3})) = \<lfloor>last_index Vs ` A\<rfloor>
 8. \<And>x1 x2 x3 x4 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x4 = \<lfloor>A\<rfloor>; fv x4 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x4) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1\<bullet>x2{x3} := x4) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2{x3} := x4) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1\<bullet>x2{x3} := x4)) = \<lfloor>last_index Vs ` A\<rfloor>
 9. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A>s x3 = \<lfloor>A\<rfloor>; fvs x3 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A>s (compEs\<^sub>1 Vs x3) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1\<bullet>x2(x3)) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2(x3)) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1\<bullet>x2(x3))) = \<lfloor>last_index Vs ` A\<rfloor>
 10. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1;; x2) = \<lfloor>A\<rfloor>; fv (x1;; x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1;; x2)) = \<lfloor>last_index Vs ` A\<rfloor>
A total of 15 subgoals...
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>\ e = \<lfloor>?Aa2\<rfloor>; \ e\<^sub>1 = \<lfloor>?A\<^sub>12\<rfloor>; \ e\<^sub>2 = \<lfloor>?A\<^sub>22\<rfloor>\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (if (e) e\<^sub>1 else e\<^sub>2)) = \<lfloor>last_index Vs ` A\<rfloor>

goal (15 subgoals):
 1. \<And>x A Vs. \<lbrakk>\ (new x) = \<lfloor>A\<rfloor>; fv (new x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (new x)) = \<lfloor>last_index Vs ` A\<rfloor>
 2. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (Cast x1 x2) = \<lfloor>A\<rfloor>; fv (Cast x1 x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (Cast x1 x2)) = \<lfloor>last_index Vs ` A\<rfloor>
 3. \<And>x A Vs. \<lbrakk>\ (Val x) = \<lfloor>A\<rfloor>; fv (Val x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (Val x)) = \<lfloor>last_index Vs ` A\<rfloor>
 4. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x3 = \<lfloor>A\<rfloor>; fv x3 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x3) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1 \<guillemotleft>x2\<guillemotright> x3) = \<lfloor>A\<rfloor>; fv (x1 \<guillemotleft>x2\<guillemotright> x3) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1 \<guillemotleft>x2\<guillemotright> x3)) = \<lfloor>last_index Vs ` A\<rfloor>
 5. \<And>x A Vs. \<lbrakk>\ (Var x) = \<lfloor>A\<rfloor>; fv (Var x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (Var x)) = \<lfloor>last_index Vs ` A\<rfloor>
 6. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (x1:=x2) = \<lfloor>A\<rfloor>; fv (x1:=x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (x1:=x2)) = \<lfloor>last_index Vs ` A\<rfloor>
 7. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (x1\<bullet>x2{x3}) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2{x3}) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (x1\<bullet>x2{x3})) = \<lfloor>last_index Vs ` A\<rfloor>
 8. \<And>x1 x2 x3 x4 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x4 = \<lfloor>A\<rfloor>; fv x4 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x4) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1\<bullet>x2{x3} := x4) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2{x3} := x4) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1\<bullet>x2{x3} := x4)) = \<lfloor>last_index Vs ` A\<rfloor>
 9. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A>s x3 = \<lfloor>A\<rfloor>; fvs x3 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A>s (compEs\<^sub>1 Vs x3) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1\<bullet>x2(x3)) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2(x3)) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1\<bullet>x2(x3))) = \<lfloor>last_index Vs ` A\<rfloor>
 10. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1;; x2) = \<lfloor>A\<rfloor>; fv (x1;; x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1;; x2)) = \<lfloor>last_index Vs ` A\<rfloor>
A total of 15 subgoals...
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\ e = None \<or> \ e\<^sub>1 = None \<or> \ e\<^sub>2 = None \<Longrightarrow> \ (compE\<^sub>1 Vs (if (e) e\<^sub>1 else e\<^sub>2)) = \<lfloor>last_index Vs ` A\<rfloor>
\<lbrakk>\ e = \<lfloor>?Aa2\<rfloor>; \ e\<^sub>1 = \<lfloor>?A\<^sub>12\<rfloor>; \ e\<^sub>2 = \<lfloor>?A\<^sub>22\<rfloor>\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (if (e) e\<^sub>1 else e\<^sub>2)) = \<lfloor>last_index Vs ` A\<rfloor>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\ e = None \<or> \ e\<^sub>1 = None \<or> \ e\<^sub>2 = None \<Longrightarrow> \ (compE\<^sub>1 Vs (if (e) e\<^sub>1 else e\<^sub>2)) = \<lfloor>last_index Vs ` A\<rfloor>
\<lbrakk>\ e = \<lfloor>?Aa2\<rfloor>; \ e\<^sub>1 = \<lfloor>?A\<^sub>12\<rfloor>; \ e\<^sub>2 = \<lfloor>?A\<^sub>22\<rfloor>\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (if (e) e\<^sub>1 else e\<^sub>2)) = \<lfloor>last_index Vs ` A\<rfloor>

goal (1 subgoal):
 1. \ (compE\<^sub>1 Vs (if (e) e\<^sub>1 else e\<^sub>2)) = \<lfloor>last_index Vs ` A\<rfloor>
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\ (compE\<^sub>1 Vs (if (e) e\<^sub>1 else e\<^sub>2)) = \<lfloor>last_index Vs ` A\<rfloor>

goal (14 subgoals):
 1. \<And>x A Vs. \<lbrakk>\ (new x) = \<lfloor>A\<rfloor>; fv (new x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (new x)) = \<lfloor>last_index Vs ` A\<rfloor>
 2. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (Cast x1 x2) = \<lfloor>A\<rfloor>; fv (Cast x1 x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (Cast x1 x2)) = \<lfloor>last_index Vs ` A\<rfloor>
 3. \<And>x A Vs. \<lbrakk>\ (Val x) = \<lfloor>A\<rfloor>; fv (Val x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (Val x)) = \<lfloor>last_index Vs ` A\<rfloor>
 4. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x3 = \<lfloor>A\<rfloor>; fv x3 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x3) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1 \<guillemotleft>x2\<guillemotright> x3) = \<lfloor>A\<rfloor>; fv (x1 \<guillemotleft>x2\<guillemotright> x3) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1 \<guillemotleft>x2\<guillemotright> x3)) = \<lfloor>last_index Vs ` A\<rfloor>
 5. \<And>x A Vs. \<lbrakk>\ (Var x) = \<lfloor>A\<rfloor>; fv (Var x) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (Var x)) = \<lfloor>last_index Vs ` A\<rfloor>
 6. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (x1:=x2) = \<lfloor>A\<rfloor>; fv (x1:=x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (x1:=x2)) = \<lfloor>last_index Vs ` A\<rfloor>
 7. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<A> (x1\<bullet>x2{x3}) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2{x3}) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs (x1\<bullet>x2{x3})) = \<lfloor>last_index Vs ` A\<rfloor>
 8. \<And>x1 x2 x3 x4 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x4 = \<lfloor>A\<rfloor>; fv x4 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x4) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1\<bullet>x2{x3} := x4) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2{x3} := x4) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1\<bullet>x2{x3} := x4)) = \<lfloor>last_index Vs ` A\<rfloor>
 9. \<And>x1 x2 x3 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A>s x3 = \<lfloor>A\<rfloor>; fvs x3 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A>s (compEs\<^sub>1 Vs x3) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1\<bullet>x2(x3)) = \<lfloor>A\<rfloor>; fv (x1\<bullet>x2(x3)) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1\<bullet>x2(x3))) = \<lfloor>last_index Vs ` A\<rfloor>
 10. \<And>x1 x2 A Vs. \<lbrakk>\<And>A Vs. \<lbrakk>\ x1 = \<lfloor>A\<rfloor>; fv x1 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs x1) = \<lfloor>last_index Vs ` A\<rfloor>; \<And>A Vs. \<lbrakk>\<A> x2 = \<lfloor>A\<rfloor>; fv x2 \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \<A> (compE\<^sub>1 Vs x2) = \<lfloor>last_index Vs ` A\<rfloor>; \ (x1;; x2) = \<lfloor>A\<rfloor>; fv (x1;; x2) \<subseteq> set Vs\<rbrakk> \<Longrightarrow> \ (compE\<^sub>1 Vs (x1;; x2)) = \<lfloor>last_index Vs ` A\<rfloor>
A total of 14 subgoals...
[PROOF STEP]
qed (auto simp add:hyperset_defs)