[STATEMENT]
lemma (in TC1) compT_LT_prefix:
 "\<And>E A ST\<^sub>0. \<lbrakk> \<lfloor>(ST,LT)\<rfloor> \<in> set(compT E A ST\<^sub>0 e); \<B> e (size E) \<rbrakk>
               \<Longrightarrow> P \<turnstile> \<lfloor>(ST,LT)\<rfloor> \<le>' ty\<^sub>i' ST E A"
and
 "\<And>E A ST\<^sub>0. \<lbrakk> \<lfloor>(ST,LT)\<rfloor> \<in> set(compTs E A ST\<^sub>0 es); \<B>s es (size E) \<rbrakk>
               \<Longrightarrow> P \<turnstile> \<lfloor>(ST,LT)\<rfloor> \<le>' ty\<^sub>i' ST E A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 e); \<B> e (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A) &&& (\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compTs E A ST\<^sub>0 es); \<B>s es (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 e); \<B> e (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A) &&& (\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compTs E A ST\<^sub>0 es); \<B>s es (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A)
[PROOF STEP]
proof(induct e and es rule: compT.induct compTs.induct)
[PROOF STATE]
proof (state)
goal (22 subgoals):
 1. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (new x)); \<B> (new x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 2. \<And>x1 x2 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x2); \<B> x2 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Cast x1 x2)); \<B> (Cast x1 x2) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 3. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Val x)); \<B> (Val x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 4. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x1); \<B> x1 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x3); \<B> x3 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1 \<guillemotleft>x2\<guillemotright> x3)); \<B> (x1 \<guillemotleft>x2\<guillemotright> x3) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 5. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Var x)); \<B> (Var x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 6. \<And>x1 x2 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x2); \<B> x2 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1:=x2)); \<B> (x1:=x2) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 7. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x1); \<B> x1 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>x2{x3})); \<B> (x1\<bullet>x2{x3}) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 8. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2{x3})); \<B> (x1\<bullet>\<^sub>sx2{x3}) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 9. \<And>x1 x2 x3 x4 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x1); \<B> x1 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x4); \<B> x4 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>x2{x3} := x4)); \<B> (x1\<bullet>x2{x3} := x4) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 10. \<And>x1 x2 x3 x4 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x4); \<B> x4 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2{x3} := x4)); \<B> (x1\<bullet>\<^sub>sx2{x3} := x4) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
A total of 22 subgoals...
[PROOF STEP]
case FAss
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT ?E2 ?A2 ?ST\<^sub>02 x1_); \<B> x1_ (length ?E2)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST ?E2 ?A2
\<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT ?E2 ?A2 ?ST\<^sub>02 x4_); \<B> x4_ (length ?E2)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST ?E2 ?A2
\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1_\<bullet>x2_{x3_} := x4_))
\<B> (x1_\<bullet>x2_{x3_} := x4_) (length E)

goal (22 subgoals):
 1. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (new x)); \<B> (new x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 2. \<And>x1 x2 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x2); \<B> x2 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Cast x1 x2)); \<B> (Cast x1 x2) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 3. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Val x)); \<B> (Val x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 4. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x1); \<B> x1 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x3); \<B> x3 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1 \<guillemotleft>x2\<guillemotright> x3)); \<B> (x1 \<guillemotleft>x2\<guillemotright> x3) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 5. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Var x)); \<B> (Var x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 6. \<And>x1 x2 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x2); \<B> x2 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1:=x2)); \<B> (x1:=x2) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 7. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x1); \<B> x1 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>x2{x3})); \<B> (x1\<bullet>x2{x3}) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 8. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2{x3})); \<B> (x1\<bullet>\<^sub>sx2{x3}) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 9. \<And>x1 x2 x3 x4 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x1); \<B> x1 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x4); \<B> x4 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>x2{x3} := x4)); \<B> (x1\<bullet>x2{x3} := x4) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 10. \<And>x1 x2 x3 x4 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x4); \<B> x4 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2{x3} := x4)); \<B> (x1\<bullet>\<^sub>sx2{x3} := x4) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
A total of 22 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT ?E2 ?A2 ?ST\<^sub>02 x1_); \<B> x1_ (length ?E2)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST ?E2 ?A2
\<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT ?E2 ?A2 ?ST\<^sub>02 x4_); \<B> x4_ (length ?E2)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST ?E2 ?A2
\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1_\<bullet>x2_{x3_} := x4_))
\<B> (x1_\<bullet>x2_{x3_} := x4_) (length E)

goal (1 subgoal):
 1. P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
[PROOF STEP]
by(fastforce simp:hyperset_defs elim!:sup_state_opt_trans)
[PROOF STATE]
proof (state)
this:
P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A

goal (21 subgoals):
 1. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (new x)); \<B> (new x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 2. \<And>x1 x2 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x2); \<B> x2 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Cast x1 x2)); \<B> (Cast x1 x2) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 3. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Val x)); \<B> (Val x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 4. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x1); \<B> x1 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x3); \<B> x3 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1 \<guillemotleft>x2\<guillemotright> x3)); \<B> (x1 \<guillemotleft>x2\<guillemotright> x3) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 5. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Var x)); \<B> (Var x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 6. \<And>x1 x2 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x2); \<B> x2 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1:=x2)); \<B> (x1:=x2) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 7. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x1); \<B> x1 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>x2{x3})); \<B> (x1\<bullet>x2{x3}) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 8. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2{x3})); \<B> (x1\<bullet>\<^sub>sx2{x3}) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 9. \<And>x1 x2 x3 x4 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x4); \<B> x4 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2{x3} := x4)); \<B> (x1\<bullet>\<^sub>sx2{x3} := x4) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 10. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x1); \<B> x1 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compTs E A ST\<^sub>0 x3); \<B>s x3 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>x2(x3))); \<B> (x1\<bullet>x2(x3)) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
A total of 21 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (21 subgoals):
 1. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (new x)); \<B> (new x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 2. \<And>x1 x2 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x2); \<B> x2 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Cast x1 x2)); \<B> (Cast x1 x2) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 3. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Val x)); \<B> (Val x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 4. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x1); \<B> x1 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x3); \<B> x3 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1 \<guillemotleft>x2\<guillemotright> x3)); \<B> (x1 \<guillemotleft>x2\<guillemotright> x3) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 5. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Var x)); \<B> (Var x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 6. \<And>x1 x2 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x2); \<B> x2 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1:=x2)); \<B> (x1:=x2) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 7. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x1); \<B> x1 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>x2{x3})); \<B> (x1\<bullet>x2{x3}) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 8. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2{x3})); \<B> (x1\<bullet>\<^sub>sx2{x3}) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 9. \<And>x1 x2 x3 x4 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x4); \<B> x4 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2{x3} := x4)); \<B> (x1\<bullet>\<^sub>sx2{x3} := x4) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 10. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x1); \<B> x1 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compTs E A ST\<^sub>0 x3); \<B>s x3 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>x2(x3))); \<B> (x1\<bullet>x2(x3)) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
A total of 21 subgoals...
[PROOF STEP]
case BinOp
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT ?E2 ?A2 ?ST\<^sub>02 x1_); \<B> x1_ (length ?E2)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST ?E2 ?A2
\<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT ?E2 ?A2 ?ST\<^sub>02 x3_); \<B> x3_ (length ?E2)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST ?E2 ?A2
\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1_ \<guillemotleft>x2_\<guillemotright> x3_))
\<B> (x1_ \<guillemotleft>x2_\<guillemotright> x3_) (length E)

goal (21 subgoals):
 1. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (new x)); \<B> (new x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 2. \<And>x1 x2 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x2); \<B> x2 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Cast x1 x2)); \<B> (Cast x1 x2) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 3. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Val x)); \<B> (Val x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 4. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x1); \<B> x1 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x3); \<B> x3 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1 \<guillemotleft>x2\<guillemotright> x3)); \<B> (x1 \<guillemotleft>x2\<guillemotright> x3) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 5. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Var x)); \<B> (Var x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 6. \<And>x1 x2 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x2); \<B> x2 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1:=x2)); \<B> (x1:=x2) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 7. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x1); \<B> x1 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>x2{x3})); \<B> (x1\<bullet>x2{x3}) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 8. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2{x3})); \<B> (x1\<bullet>\<^sub>sx2{x3}) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 9. \<And>x1 x2 x3 x4 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x4); \<B> x4 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2{x3} := x4)); \<B> (x1\<bullet>\<^sub>sx2{x3} := x4) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 10. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x1); \<B> x1 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compTs E A ST\<^sub>0 x3); \<B>s x3 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>x2(x3))); \<B> (x1\<bullet>x2(x3)) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
A total of 21 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT ?E2 ?A2 ?ST\<^sub>02 x1_); \<B> x1_ (length ?E2)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST ?E2 ?A2
\<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT ?E2 ?A2 ?ST\<^sub>02 x3_); \<B> x3_ (length ?E2)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST ?E2 ?A2
\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1_ \<guillemotleft>x2_\<guillemotright> x3_))
\<B> (x1_ \<guillemotleft>x2_\<guillemotright> x3_) (length E)

goal (1 subgoal):
 1. P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
[PROOF STEP]
by(fastforce simp:hyperset_defs elim!:sup_state_opt_trans split:bop.splits)
[PROOF STATE]
proof (state)
this:
P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A

goal (20 subgoals):
 1. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (new x)); \<B> (new x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 2. \<And>x1 x2 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x2); \<B> x2 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Cast x1 x2)); \<B> (Cast x1 x2) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 3. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Val x)); \<B> (Val x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 4. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Var x)); \<B> (Var x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 5. \<And>x1 x2 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x2); \<B> x2 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1:=x2)); \<B> (x1:=x2) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 6. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x1); \<B> x1 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>x2{x3})); \<B> (x1\<bullet>x2{x3}) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 7. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2{x3})); \<B> (x1\<bullet>\<^sub>sx2{x3}) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 8. \<And>x1 x2 x3 x4 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x4); \<B> x4 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2{x3} := x4)); \<B> (x1\<bullet>\<^sub>sx2{x3} := x4) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 9. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x1); \<B> x1 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compTs E A ST\<^sub>0 x3); \<B>s x3 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>x2(x3))); \<B> (x1\<bullet>x2(x3)) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 10. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compTs E A ST\<^sub>0 x3); \<B>s x3 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2(x3))); \<B> (x1\<bullet>\<^sub>sx2(x3)) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
A total of 20 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (20 subgoals):
 1. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (new x)); \<B> (new x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 2. \<And>x1 x2 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x2); \<B> x2 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Cast x1 x2)); \<B> (Cast x1 x2) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 3. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Val x)); \<B> (Val x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 4. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Var x)); \<B> (Var x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 5. \<And>x1 x2 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x2); \<B> x2 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1:=x2)); \<B> (x1:=x2) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 6. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x1); \<B> x1 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>x2{x3})); \<B> (x1\<bullet>x2{x3}) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 7. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2{x3})); \<B> (x1\<bullet>\<^sub>sx2{x3}) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 8. \<And>x1 x2 x3 x4 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x4); \<B> x4 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2{x3} := x4)); \<B> (x1\<bullet>\<^sub>sx2{x3} := x4) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 9. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x1); \<B> x1 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compTs E A ST\<^sub>0 x3); \<B>s x3 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>x2(x3))); \<B> (x1\<bullet>x2(x3)) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 10. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compTs E A ST\<^sub>0 x3); \<B>s x3 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2(x3))); \<B> (x1\<bullet>\<^sub>sx2(x3)) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
A total of 20 subgoals...
[PROOF STEP]
case Seq
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT ?E2 ?A2 ?ST\<^sub>02 x1_); \<B> x1_ (length ?E2)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST ?E2 ?A2
\<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT ?E2 ?A2 ?ST\<^sub>02 x2_); \<B> x2_ (length ?E2)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST ?E2 ?A2
\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1_;; x2_))
\<B> (x1_;; x2_) (length E)

goal (20 subgoals):
 1. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (new x)); \<B> (new x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 2. \<And>x1 x2 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x2); \<B> x2 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Cast x1 x2)); \<B> (Cast x1 x2) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 3. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Val x)); \<B> (Val x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 4. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Var x)); \<B> (Var x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 5. \<And>x1 x2 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x2); \<B> x2 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1:=x2)); \<B> (x1:=x2) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 6. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x1); \<B> x1 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>x2{x3})); \<B> (x1\<bullet>x2{x3}) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 7. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2{x3})); \<B> (x1\<bullet>\<^sub>sx2{x3}) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 8. \<And>x1 x2 x3 x4 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x4); \<B> x4 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2{x3} := x4)); \<B> (x1\<bullet>\<^sub>sx2{x3} := x4) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 9. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x1); \<B> x1 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compTs E A ST\<^sub>0 x3); \<B>s x3 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>x2(x3))); \<B> (x1\<bullet>x2(x3)) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 10. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compTs E A ST\<^sub>0 x3); \<B>s x3 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2(x3))); \<B> (x1\<bullet>\<^sub>sx2(x3)) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
A total of 20 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT ?E2 ?A2 ?ST\<^sub>02 x1_); \<B> x1_ (length ?E2)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST ?E2 ?A2
\<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT ?E2 ?A2 ?ST\<^sub>02 x2_); \<B> x2_ (length ?E2)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST ?E2 ?A2
\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1_;; x2_))
\<B> (x1_;; x2_) (length E)

goal (1 subgoal):
 1. P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
[PROOF STEP]
by(fastforce simp:hyperset_defs elim!:sup_state_opt_trans)
[PROOF STATE]
proof (state)
this:
P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A

goal (19 subgoals):
 1. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (new x)); \<B> (new x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 2. \<And>x1 x2 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x2); \<B> x2 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Cast x1 x2)); \<B> (Cast x1 x2) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 3. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Val x)); \<B> (Val x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 4. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Var x)); \<B> (Var x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 5. \<And>x1 x2 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x2); \<B> x2 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1:=x2)); \<B> (x1:=x2) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 6. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x1); \<B> x1 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>x2{x3})); \<B> (x1\<bullet>x2{x3}) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 7. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2{x3})); \<B> (x1\<bullet>\<^sub>sx2{x3}) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 8. \<And>x1 x2 x3 x4 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x4); \<B> x4 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2{x3} := x4)); \<B> (x1\<bullet>\<^sub>sx2{x3} := x4) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 9. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x1); \<B> x1 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compTs E A ST\<^sub>0 x3); \<B>s x3 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>x2(x3))); \<B> (x1\<bullet>x2(x3)) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 10. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compTs E A ST\<^sub>0 x3); \<B>s x3 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2(x3))); \<B> (x1\<bullet>\<^sub>sx2(x3)) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
A total of 19 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (19 subgoals):
 1. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (new x)); \<B> (new x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 2. \<And>x1 x2 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x2); \<B> x2 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Cast x1 x2)); \<B> (Cast x1 x2) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 3. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Val x)); \<B> (Val x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 4. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Var x)); \<B> (Var x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 5. \<And>x1 x2 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x2); \<B> x2 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1:=x2)); \<B> (x1:=x2) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 6. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x1); \<B> x1 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>x2{x3})); \<B> (x1\<bullet>x2{x3}) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 7. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2{x3})); \<B> (x1\<bullet>\<^sub>sx2{x3}) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 8. \<And>x1 x2 x3 x4 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x4); \<B> x4 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2{x3} := x4)); \<B> (x1\<bullet>\<^sub>sx2{x3} := x4) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 9. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x1); \<B> x1 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compTs E A ST\<^sub>0 x3); \<B>s x3 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>x2(x3))); \<B> (x1\<bullet>x2(x3)) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 10. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compTs E A ST\<^sub>0 x3); \<B>s x3 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2(x3))); \<B> (x1\<bullet>\<^sub>sx2(x3)) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
A total of 19 subgoals...
[PROOF STEP]
case While
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT ?E2 ?A2 ?ST\<^sub>02 x1_); \<B> x1_ (length ?E2)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST ?E2 ?A2
\<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT ?E2 ?A2 ?ST\<^sub>02 x2_); \<B> x2_ (length ?E2)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST ?E2 ?A2
\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (while (x1_) x2_))
\<B> (while (x1_) x2_) (length E)

goal (19 subgoals):
 1. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (new x)); \<B> (new x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 2. \<And>x1 x2 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x2); \<B> x2 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Cast x1 x2)); \<B> (Cast x1 x2) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 3. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Val x)); \<B> (Val x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 4. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Var x)); \<B> (Var x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 5. \<And>x1 x2 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x2); \<B> x2 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1:=x2)); \<B> (x1:=x2) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 6. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x1); \<B> x1 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>x2{x3})); \<B> (x1\<bullet>x2{x3}) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 7. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2{x3})); \<B> (x1\<bullet>\<^sub>sx2{x3}) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 8. \<And>x1 x2 x3 x4 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x4); \<B> x4 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2{x3} := x4)); \<B> (x1\<bullet>\<^sub>sx2{x3} := x4) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 9. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x1); \<B> x1 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compTs E A ST\<^sub>0 x3); \<B>s x3 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>x2(x3))); \<B> (x1\<bullet>x2(x3)) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 10. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compTs E A ST\<^sub>0 x3); \<B>s x3 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2(x3))); \<B> (x1\<bullet>\<^sub>sx2(x3)) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
A total of 19 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT ?E2 ?A2 ?ST\<^sub>02 x1_); \<B> x1_ (length ?E2)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST ?E2 ?A2
\<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT ?E2 ?A2 ?ST\<^sub>02 x2_); \<B> x2_ (length ?E2)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST ?E2 ?A2
\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (while (x1_) x2_))
\<B> (while (x1_) x2_) (length E)

goal (1 subgoal):
 1. P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
[PROOF STEP]
by(fastforce simp:hyperset_defs elim!:sup_state_opt_trans)
[PROOF STATE]
proof (state)
this:
P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A

goal (18 subgoals):
 1. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (new x)); \<B> (new x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 2. \<And>x1 x2 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x2); \<B> x2 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Cast x1 x2)); \<B> (Cast x1 x2) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 3. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Val x)); \<B> (Val x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 4. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Var x)); \<B> (Var x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 5. \<And>x1 x2 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x2); \<B> x2 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1:=x2)); \<B> (x1:=x2) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 6. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x1); \<B> x1 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>x2{x3})); \<B> (x1\<bullet>x2{x3}) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 7. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2{x3})); \<B> (x1\<bullet>\<^sub>sx2{x3}) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 8. \<And>x1 x2 x3 x4 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x4); \<B> x4 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2{x3} := x4)); \<B> (x1\<bullet>\<^sub>sx2{x3} := x4) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 9. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x1); \<B> x1 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compTs E A ST\<^sub>0 x3); \<B>s x3 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>x2(x3))); \<B> (x1\<bullet>x2(x3)) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 10. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compTs E A ST\<^sub>0 x3); \<B>s x3 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2(x3))); \<B> (x1\<bullet>\<^sub>sx2(x3)) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
A total of 18 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (18 subgoals):
 1. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (new x)); \<B> (new x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 2. \<And>x1 x2 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x2); \<B> x2 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Cast x1 x2)); \<B> (Cast x1 x2) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 3. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Val x)); \<B> (Val x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 4. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Var x)); \<B> (Var x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 5. \<And>x1 x2 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x2); \<B> x2 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1:=x2)); \<B> (x1:=x2) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 6. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x1); \<B> x1 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>x2{x3})); \<B> (x1\<bullet>x2{x3}) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 7. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2{x3})); \<B> (x1\<bullet>\<^sub>sx2{x3}) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 8. \<And>x1 x2 x3 x4 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x4); \<B> x4 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2{x3} := x4)); \<B> (x1\<bullet>\<^sub>sx2{x3} := x4) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 9. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x1); \<B> x1 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compTs E A ST\<^sub>0 x3); \<B>s x3 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>x2(x3))); \<B> (x1\<bullet>x2(x3)) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 10. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compTs E A ST\<^sub>0 x3); \<B>s x3 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2(x3))); \<B> (x1\<bullet>\<^sub>sx2(x3)) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
A total of 18 subgoals...
[PROOF STEP]
case Cond
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT ?E2 ?A2 ?ST\<^sub>02 x1_); \<B> x1_ (length ?E2)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST ?E2 ?A2
\<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT ?E2 ?A2 ?ST\<^sub>02 x2_); \<B> x2_ (length ?E2)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST ?E2 ?A2
\<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT ?E2 ?A2 ?ST\<^sub>02 x3_); \<B> x3_ (length ?E2)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST ?E2 ?A2
\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (if (x1_) x2_ else x3_))
\<B> (if (x1_) x2_ else x3_) (length E)

goal (18 subgoals):
 1. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (new x)); \<B> (new x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 2. \<And>x1 x2 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x2); \<B> x2 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Cast x1 x2)); \<B> (Cast x1 x2) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 3. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Val x)); \<B> (Val x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 4. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Var x)); \<B> (Var x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 5. \<And>x1 x2 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x2); \<B> x2 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1:=x2)); \<B> (x1:=x2) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 6. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x1); \<B> x1 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>x2{x3})); \<B> (x1\<bullet>x2{x3}) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 7. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2{x3})); \<B> (x1\<bullet>\<^sub>sx2{x3}) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 8. \<And>x1 x2 x3 x4 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x4); \<B> x4 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2{x3} := x4)); \<B> (x1\<bullet>\<^sub>sx2{x3} := x4) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 9. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x1); \<B> x1 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compTs E A ST\<^sub>0 x3); \<B>s x3 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>x2(x3))); \<B> (x1\<bullet>x2(x3)) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 10. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compTs E A ST\<^sub>0 x3); \<B>s x3 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2(x3))); \<B> (x1\<bullet>\<^sub>sx2(x3)) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
A total of 18 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT ?E2 ?A2 ?ST\<^sub>02 x1_); \<B> x1_ (length ?E2)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST ?E2 ?A2
\<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT ?E2 ?A2 ?ST\<^sub>02 x2_); \<B> x2_ (length ?E2)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST ?E2 ?A2
\<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT ?E2 ?A2 ?ST\<^sub>02 x3_); \<B> x3_ (length ?E2)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST ?E2 ?A2
\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (if (x1_) x2_ else x3_))
\<B> (if (x1_) x2_ else x3_) (length E)

goal (1 subgoal):
 1. P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
[PROOF STEP]
by(fastforce simp:hyperset_defs elim!:sup_state_opt_trans)
[PROOF STATE]
proof (state)
this:
P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A

goal (17 subgoals):
 1. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (new x)); \<B> (new x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 2. \<And>x1 x2 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x2); \<B> x2 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Cast x1 x2)); \<B> (Cast x1 x2) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 3. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Val x)); \<B> (Val x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 4. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Var x)); \<B> (Var x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 5. \<And>x1 x2 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x2); \<B> x2 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1:=x2)); \<B> (x1:=x2) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 6. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x1); \<B> x1 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>x2{x3})); \<B> (x1\<bullet>x2{x3}) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 7. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2{x3})); \<B> (x1\<bullet>\<^sub>sx2{x3}) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 8. \<And>x1 x2 x3 x4 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x4); \<B> x4 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2{x3} := x4)); \<B> (x1\<bullet>\<^sub>sx2{x3} := x4) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 9. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x1); \<B> x1 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compTs E A ST\<^sub>0 x3); \<B>s x3 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>x2(x3))); \<B> (x1\<bullet>x2(x3)) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 10. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compTs E A ST\<^sub>0 x3); \<B>s x3 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2(x3))); \<B> (x1\<bullet>\<^sub>sx2(x3)) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
A total of 17 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (17 subgoals):
 1. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (new x)); \<B> (new x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 2. \<And>x1 x2 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x2); \<B> x2 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Cast x1 x2)); \<B> (Cast x1 x2) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 3. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Val x)); \<B> (Val x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 4. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Var x)); \<B> (Var x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 5. \<And>x1 x2 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x2); \<B> x2 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1:=x2)); \<B> (x1:=x2) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 6. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x1); \<B> x1 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>x2{x3})); \<B> (x1\<bullet>x2{x3}) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 7. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2{x3})); \<B> (x1\<bullet>\<^sub>sx2{x3}) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 8. \<And>x1 x2 x3 x4 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x4); \<B> x4 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2{x3} := x4)); \<B> (x1\<bullet>\<^sub>sx2{x3} := x4) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 9. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x1); \<B> x1 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compTs E A ST\<^sub>0 x3); \<B>s x3 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>x2(x3))); \<B> (x1\<bullet>x2(x3)) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 10. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compTs E A ST\<^sub>0 x3); \<B>s x3 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2(x3))); \<B> (x1\<bullet>\<^sub>sx2(x3)) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
A total of 17 subgoals...
[PROOF STEP]
case Block
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT ?E2 ?A2 ?ST\<^sub>02 x3_); \<B> x3_ (length ?E2)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST ?E2 ?A2
\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 {x1_:x2_; x3_})
\<B> {x1_:x2_; x3_} (length E)

goal (17 subgoals):
 1. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (new x)); \<B> (new x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 2. \<And>x1 x2 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x2); \<B> x2 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Cast x1 x2)); \<B> (Cast x1 x2) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 3. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Val x)); \<B> (Val x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 4. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Var x)); \<B> (Var x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 5. \<And>x1 x2 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x2); \<B> x2 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1:=x2)); \<B> (x1:=x2) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 6. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x1); \<B> x1 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>x2{x3})); \<B> (x1\<bullet>x2{x3}) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 7. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2{x3})); \<B> (x1\<bullet>\<^sub>sx2{x3}) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 8. \<And>x1 x2 x3 x4 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x4); \<B> x4 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2{x3} := x4)); \<B> (x1\<bullet>\<^sub>sx2{x3} := x4) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 9. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x1); \<B> x1 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compTs E A ST\<^sub>0 x3); \<B>s x3 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>x2(x3))); \<B> (x1\<bullet>x2(x3)) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 10. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compTs E A ST\<^sub>0 x3); \<B>s x3 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2(x3))); \<B> (x1\<bullet>\<^sub>sx2(x3)) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
A total of 17 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT ?E2 ?A2 ?ST\<^sub>02 x3_); \<B> x3_ (length ?E2)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST ?E2 ?A2
\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 {x1_:x2_; x3_})
\<B> {x1_:x2_; x3_} (length E)

goal (1 subgoal):
 1. P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
[PROOF STEP]
by(force simp add:hyperset_defs ty\<^sub>i'_def simp del:pair_conv_ty\<^sub>i'
             elim!:sup_state_opt_trans)
[PROOF STATE]
proof (state)
this:
P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A

goal (16 subgoals):
 1. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (new x)); \<B> (new x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 2. \<And>x1 x2 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x2); \<B> x2 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Cast x1 x2)); \<B> (Cast x1 x2) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 3. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Val x)); \<B> (Val x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 4. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Var x)); \<B> (Var x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 5. \<And>x1 x2 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x2); \<B> x2 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1:=x2)); \<B> (x1:=x2) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 6. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x1); \<B> x1 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>x2{x3})); \<B> (x1\<bullet>x2{x3}) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 7. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2{x3})); \<B> (x1\<bullet>\<^sub>sx2{x3}) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 8. \<And>x1 x2 x3 x4 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x4); \<B> x4 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2{x3} := x4)); \<B> (x1\<bullet>\<^sub>sx2{x3} := x4) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 9. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x1); \<B> x1 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compTs E A ST\<^sub>0 x3); \<B>s x3 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>x2(x3))); \<B> (x1\<bullet>x2(x3)) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 10. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compTs E A ST\<^sub>0 x3); \<B>s x3 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2(x3))); \<B> (x1\<bullet>\<^sub>sx2(x3)) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
A total of 16 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (16 subgoals):
 1. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (new x)); \<B> (new x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 2. \<And>x1 x2 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x2); \<B> x2 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Cast x1 x2)); \<B> (Cast x1 x2) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 3. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Val x)); \<B> (Val x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 4. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Var x)); \<B> (Var x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 5. \<And>x1 x2 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x2); \<B> x2 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1:=x2)); \<B> (x1:=x2) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 6. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x1); \<B> x1 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>x2{x3})); \<B> (x1\<bullet>x2{x3}) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 7. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2{x3})); \<B> (x1\<bullet>\<^sub>sx2{x3}) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 8. \<And>x1 x2 x3 x4 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x4); \<B> x4 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2{x3} := x4)); \<B> (x1\<bullet>\<^sub>sx2{x3} := x4) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 9. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x1); \<B> x1 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compTs E A ST\<^sub>0 x3); \<B>s x3 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>x2(x3))); \<B> (x1\<bullet>x2(x3)) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 10. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compTs E A ST\<^sub>0 x3); \<B>s x3 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2(x3))); \<B> (x1\<bullet>\<^sub>sx2(x3)) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
A total of 16 subgoals...
[PROOF STEP]
case Call
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT ?E2 ?A2 ?ST\<^sub>02 x1_); \<B> x1_ (length ?E2)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST ?E2 ?A2
\<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compTs ?E2 ?A2 ?ST\<^sub>02 x3_); \<B>s x3_ (length ?E2)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST ?E2 ?A2
\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1_\<bullet>x2_(x3_)))
\<B> (x1_\<bullet>x2_(x3_)) (length E)

goal (16 subgoals):
 1. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (new x)); \<B> (new x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 2. \<And>x1 x2 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x2); \<B> x2 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Cast x1 x2)); \<B> (Cast x1 x2) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 3. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Val x)); \<B> (Val x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 4. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Var x)); \<B> (Var x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 5. \<And>x1 x2 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x2); \<B> x2 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1:=x2)); \<B> (x1:=x2) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 6. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x1); \<B> x1 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>x2{x3})); \<B> (x1\<bullet>x2{x3}) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 7. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2{x3})); \<B> (x1\<bullet>\<^sub>sx2{x3}) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 8. \<And>x1 x2 x3 x4 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x4); \<B> x4 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2{x3} := x4)); \<B> (x1\<bullet>\<^sub>sx2{x3} := x4) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 9. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x1); \<B> x1 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compTs E A ST\<^sub>0 x3); \<B>s x3 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>x2(x3))); \<B> (x1\<bullet>x2(x3)) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 10. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compTs E A ST\<^sub>0 x3); \<B>s x3 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2(x3))); \<B> (x1\<bullet>\<^sub>sx2(x3)) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
A total of 16 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT ?E2 ?A2 ?ST\<^sub>02 x1_); \<B> x1_ (length ?E2)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST ?E2 ?A2
\<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compTs ?E2 ?A2 ?ST\<^sub>02 x3_); \<B>s x3_ (length ?E2)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST ?E2 ?A2
\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1_\<bullet>x2_(x3_)))
\<B> (x1_\<bullet>x2_(x3_)) (length E)

goal (1 subgoal):
 1. P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
[PROOF STEP]
by(fastforce simp:hyperset_defs elim!:sup_state_opt_trans)
[PROOF STATE]
proof (state)
this:
P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A

goal (15 subgoals):
 1. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (new x)); \<B> (new x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 2. \<And>x1 x2 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x2); \<B> x2 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Cast x1 x2)); \<B> (Cast x1 x2) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 3. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Val x)); \<B> (Val x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 4. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Var x)); \<B> (Var x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 5. \<And>x1 x2 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x2); \<B> x2 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1:=x2)); \<B> (x1:=x2) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 6. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x1); \<B> x1 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>x2{x3})); \<B> (x1\<bullet>x2{x3}) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 7. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2{x3})); \<B> (x1\<bullet>\<^sub>sx2{x3}) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 8. \<And>x1 x2 x3 x4 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x4); \<B> x4 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2{x3} := x4)); \<B> (x1\<bullet>\<^sub>sx2{x3} := x4) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 9. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compTs E A ST\<^sub>0 x3); \<B>s x3 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2(x3))); \<B> (x1\<bullet>\<^sub>sx2(x3)) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 10. \<And>x E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x); \<B> x (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (throw x)); \<B> (throw x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
A total of 15 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (15 subgoals):
 1. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (new x)); \<B> (new x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 2. \<And>x1 x2 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x2); \<B> x2 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Cast x1 x2)); \<B> (Cast x1 x2) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 3. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Val x)); \<B> (Val x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 4. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Var x)); \<B> (Var x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 5. \<And>x1 x2 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x2); \<B> x2 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1:=x2)); \<B> (x1:=x2) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 6. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x1); \<B> x1 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>x2{x3})); \<B> (x1\<bullet>x2{x3}) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 7. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2{x3})); \<B> (x1\<bullet>\<^sub>sx2{x3}) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 8. \<And>x1 x2 x3 x4 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x4); \<B> x4 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2{x3} := x4)); \<B> (x1\<bullet>\<^sub>sx2{x3} := x4) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 9. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compTs E A ST\<^sub>0 x3); \<B>s x3 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2(x3))); \<B> (x1\<bullet>\<^sub>sx2(x3)) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 10. \<And>x E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x); \<B> x (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (throw x)); \<B> (throw x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
A total of 15 subgoals...
[PROOF STEP]
case Cons_exp
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT ?E2 ?A2 ?ST\<^sub>02 x1_); \<B> x1_ (length ?E2)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST ?E2 ?A2
\<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compTs ?E2 ?A2 ?ST\<^sub>02 x2_); \<B>s x2_ (length ?E2)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST ?E2 ?A2
\<lfloor>(ST, LT)\<rfloor> \<in> set (compTs E A ST\<^sub>0 (x1_ # x2_))
\<B>s (x1_ # x2_) (length E)

goal (15 subgoals):
 1. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (new x)); \<B> (new x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 2. \<And>x1 x2 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x2); \<B> x2 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Cast x1 x2)); \<B> (Cast x1 x2) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 3. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Val x)); \<B> (Val x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 4. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Var x)); \<B> (Var x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 5. \<And>x1 x2 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x2); \<B> x2 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1:=x2)); \<B> (x1:=x2) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 6. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x1); \<B> x1 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>x2{x3})); \<B> (x1\<bullet>x2{x3}) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 7. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2{x3})); \<B> (x1\<bullet>\<^sub>sx2{x3}) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 8. \<And>x1 x2 x3 x4 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x4); \<B> x4 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2{x3} := x4)); \<B> (x1\<bullet>\<^sub>sx2{x3} := x4) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 9. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compTs E A ST\<^sub>0 x3); \<B>s x3 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2(x3))); \<B> (x1\<bullet>\<^sub>sx2(x3)) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 10. \<And>x E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x); \<B> x (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (throw x)); \<B> (throw x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
A total of 15 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT ?E2 ?A2 ?ST\<^sub>02 x1_); \<B> x1_ (length ?E2)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST ?E2 ?A2
\<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compTs ?E2 ?A2 ?ST\<^sub>02 x2_); \<B>s x2_ (length ?E2)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST ?E2 ?A2
\<lfloor>(ST, LT)\<rfloor> \<in> set (compTs E A ST\<^sub>0 (x1_ # x2_))
\<B>s (x1_ # x2_) (length E)

goal (1 subgoal):
 1. P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
[PROOF STEP]
by(fastforce simp:hyperset_defs elim!:sup_state_opt_trans)
[PROOF STATE]
proof (state)
this:
P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A

goal (14 subgoals):
 1. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (new x)); \<B> (new x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 2. \<And>x1 x2 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x2); \<B> x2 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Cast x1 x2)); \<B> (Cast x1 x2) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 3. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Val x)); \<B> (Val x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 4. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Var x)); \<B> (Var x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 5. \<And>x1 x2 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x2); \<B> x2 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1:=x2)); \<B> (x1:=x2) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 6. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x1); \<B> x1 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>x2{x3})); \<B> (x1\<bullet>x2{x3}) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 7. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2{x3})); \<B> (x1\<bullet>\<^sub>sx2{x3}) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 8. \<And>x1 x2 x3 x4 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x4); \<B> x4 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2{x3} := x4)); \<B> (x1\<bullet>\<^sub>sx2{x3} := x4) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 9. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compTs E A ST\<^sub>0 x3); \<B>s x3 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2(x3))); \<B> (x1\<bullet>\<^sub>sx2(x3)) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 10. \<And>x E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x); \<B> x (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (throw x)); \<B> (throw x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
A total of 14 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (14 subgoals):
 1. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (new x)); \<B> (new x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 2. \<And>x1 x2 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x2); \<B> x2 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Cast x1 x2)); \<B> (Cast x1 x2) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 3. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Val x)); \<B> (Val x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 4. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Var x)); \<B> (Var x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 5. \<And>x1 x2 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x2); \<B> x2 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1:=x2)); \<B> (x1:=x2) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 6. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x1); \<B> x1 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>x2{x3})); \<B> (x1\<bullet>x2{x3}) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 7. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2{x3})); \<B> (x1\<bullet>\<^sub>sx2{x3}) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 8. \<And>x1 x2 x3 x4 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x4); \<B> x4 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2{x3} := x4)); \<B> (x1\<bullet>\<^sub>sx2{x3} := x4) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 9. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compTs E A ST\<^sub>0 x3); \<B>s x3 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2(x3))); \<B> (x1\<bullet>\<^sub>sx2(x3)) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 10. \<And>x E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x); \<B> x (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (throw x)); \<B> (throw x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
A total of 14 subgoals...
[PROOF STEP]
case TryCatch
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT ?E2 ?A2 ?ST\<^sub>02 x1_); \<B> x1_ (length ?E2)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST ?E2 ?A2
\<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT ?E2 ?A2 ?ST\<^sub>02 x4_); \<B> x4_ (length ?E2)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST ?E2 ?A2
\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (try x1_ catch(x2_ x3_) x4_))
\<B> (try x1_ catch(x2_ x3_) x4_) (length E)

goal (14 subgoals):
 1. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (new x)); \<B> (new x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 2. \<And>x1 x2 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x2); \<B> x2 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Cast x1 x2)); \<B> (Cast x1 x2) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 3. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Val x)); \<B> (Val x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 4. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Var x)); \<B> (Var x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 5. \<And>x1 x2 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x2); \<B> x2 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1:=x2)); \<B> (x1:=x2) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 6. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x1); \<B> x1 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>x2{x3})); \<B> (x1\<bullet>x2{x3}) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 7. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2{x3})); \<B> (x1\<bullet>\<^sub>sx2{x3}) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 8. \<And>x1 x2 x3 x4 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x4); \<B> x4 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2{x3} := x4)); \<B> (x1\<bullet>\<^sub>sx2{x3} := x4) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 9. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compTs E A ST\<^sub>0 x3); \<B>s x3 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2(x3))); \<B> (x1\<bullet>\<^sub>sx2(x3)) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 10. \<And>x E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x); \<B> x (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (throw x)); \<B> (throw x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
A total of 14 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT ?E2 ?A2 ?ST\<^sub>02 x1_); \<B> x1_ (length ?E2)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST ?E2 ?A2
\<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT ?E2 ?A2 ?ST\<^sub>02 x4_); \<B> x4_ (length ?E2)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST ?E2 ?A2
\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (try x1_ catch(x2_ x3_) x4_))
\<B> (try x1_ catch(x2_ x3_) x4_) (length E)

goal (1 subgoal):
 1. P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
[PROOF STEP]
by(fastforce simp:hyperset_defs intro!: ty\<^sub>i'_incr
                elim!:sup_state_opt_trans)
[PROOF STATE]
proof (state)
this:
P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A

goal (13 subgoals):
 1. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (new x)); \<B> (new x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 2. \<And>x1 x2 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x2); \<B> x2 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Cast x1 x2)); \<B> (Cast x1 x2) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 3. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Val x)); \<B> (Val x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 4. \<And>x E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (Var x)); \<B> (Var x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 5. \<And>x1 x2 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x2); \<B> x2 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1:=x2)); \<B> (x1:=x2) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 6. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x1); \<B> x1 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>x2{x3})); \<B> (x1\<bullet>x2{x3}) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 7. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2{x3})); \<B> (x1\<bullet>\<^sub>sx2{x3}) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 8. \<And>x1 x2 x3 x4 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x4); \<B> x4 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2{x3} := x4)); \<B> (x1\<bullet>\<^sub>sx2{x3} := x4) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 9. \<And>x1 x2 x3 E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compTs E A ST\<^sub>0 x3); \<B>s x3 (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (x1\<bullet>\<^sub>sx2(x3))); \<B> (x1\<bullet>\<^sub>sx2(x3)) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
 10. \<And>x E A ST\<^sub>0. \<lbrakk>\<And>E A ST\<^sub>0. \<lbrakk>\<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 x); \<B> x (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A; \<lfloor>(ST, LT)\<rfloor> \<in> set (compT E A ST\<^sub>0 (throw x)); \<B> (throw x) (length E)\<rbrakk> \<Longrightarrow> P \<turnstile> \<lfloor>(ST, LT)\<rfloor> \<le>' ty\<^sub>i' ST E A
A total of 13 subgoals...
[PROOF STEP]
qed (auto simp:hyperset_defs)