[STATEMENT]
lemma wt_instrs_xapp:
  "\<lbrakk> \<turnstile> is\<^sub>1 @ is\<^sub>2, xt [::] \<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2;
     \<forall>\<tau> \<in> set \<tau>s\<^sub>1. \<forall>ST' LT'. \<tau> = Some(ST',LT') \<longrightarrow>
      size ST \<le> size ST' \<and> P \<turnstile> Some (drop (size ST' - size ST) ST',LT') \<le>' ty\<^sub>i' ST E A;
     size is\<^sub>1 = size \<tau>s\<^sub>1; size ST < mxs; case Co of None \<Rightarrow> D = Throwable | Some C \<Rightarrow> D = C \<and> is_class P C  \<rbrakk> \<Longrightarrow>
  \<turnstile> is\<^sub>1 @ is\<^sub>2, xt @ [(0,size is\<^sub>1 - Suc n,Co,size is\<^sub>1,size ST)] [::] \<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<turnstile> is\<^sub>1 @ is\<^sub>2, xt [::] \<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2; \<forall>\<tau>\<in>set \<tau>s\<^sub>1. \<forall>ST' LT'. \<tau> = \<lfloor>(ST', LT')\<rfloor> \<longrightarrow> length ST \<le> length ST' \<and> P \<turnstile> \<lfloor>(drop (length ST' - length ST) ST', LT')\<rfloor> \<le>' ty\<^sub>i' ST E A; length is\<^sub>1 = length \<tau>s\<^sub>1; length ST < mxs; case Co of None \<Rightarrow> D = Throwable | \<lfloor>C\<rfloor> \<Rightarrow> D = C \<and> is_class P C\<rbrakk> \<Longrightarrow> \<turnstile> is\<^sub>1 @ is\<^sub>2, xt @ [(0, length is\<^sub>1 - Suc n, Co, length is\<^sub>1, length ST)] [::] \<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2
[PROOF STEP]
apply(simp add:wt_instrs_def split del: option.split_asm)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length is\<^sub>2 < Suc (length \<tau>s\<^sub>2) \<and> pcs xt \<subseteq> {0..<length \<tau>s\<^sub>1 + length is\<^sub>2} \<and> (\<forall>pc<length \<tau>s\<^sub>1 + length is\<^sub>2. P,T\<^sub>r,mxs,Suc (length \<tau>s\<^sub>1 + length \<tau>s\<^sub>2),xt \<turnstile> (is\<^sub>1 @ is\<^sub>2) ! pc,pc :: \<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2); \<forall>\<tau>\<in>set \<tau>s\<^sub>1. \<forall>ST' LT'. \<tau> = \<lfloor>(ST', LT')\<rfloor> \<longrightarrow> length ST \<le> length ST' \<and> P \<turnstile> \<lfloor>(drop (length ST' - length ST) ST', LT')\<rfloor> \<le>' ty\<^sub>i' ST E A; length is\<^sub>1 = length \<tau>s\<^sub>1; length ST < mxs; case Co of None \<Rightarrow> D = Throwable | \<lfloor>C\<rfloor> \<Rightarrow> D = C \<and> is_class P C\<rbrakk> \<Longrightarrow> (length \<tau>s\<^sub>1 \<le> Suc n \<or> length \<tau>s\<^sub>1 - Suc n \<le> length \<tau>s\<^sub>1 + length is\<^sub>2) \<and> (\<forall>pc<length \<tau>s\<^sub>1 + length is\<^sub>2. P,T\<^sub>r,mxs,Suc (length \<tau>s\<^sub>1 + length \<tau>s\<^sub>2),xt @ [(0, length \<tau>s\<^sub>1 - Suc n, Co, length \<tau>s\<^sub>1, length ST)] \<turnstile> (is\<^sub>1 @ is\<^sub>2) ! pc,pc :: \<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2)
[PROOF STEP]
apply(rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>length is\<^sub>2 < Suc (length \<tau>s\<^sub>2) \<and> pcs xt \<subseteq> {0..<length \<tau>s\<^sub>1 + length is\<^sub>2} \<and> (\<forall>pc<length \<tau>s\<^sub>1 + length is\<^sub>2. P,T\<^sub>r,mxs,Suc (length \<tau>s\<^sub>1 + length \<tau>s\<^sub>2),xt \<turnstile> (is\<^sub>1 @ is\<^sub>2) ! pc,pc :: \<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2); \<forall>\<tau>\<in>set \<tau>s\<^sub>1. \<forall>ST' LT'. \<tau> = \<lfloor>(ST', LT')\<rfloor> \<longrightarrow> length ST \<le> length ST' \<and> P \<turnstile> \<lfloor>(drop (length ST' - length ST) ST', LT')\<rfloor> \<le>' ty\<^sub>i' ST E A; length is\<^sub>1 = length \<tau>s\<^sub>1; length ST < mxs; case Co of None \<Rightarrow> D = Throwable | \<lfloor>C\<rfloor> \<Rightarrow> D = C \<and> is_class P C\<rbrakk> \<Longrightarrow> length \<tau>s\<^sub>1 \<le> Suc n \<or> length \<tau>s\<^sub>1 - Suc n \<le> length \<tau>s\<^sub>1 + length is\<^sub>2
 2. \<lbrakk>length is\<^sub>2 < Suc (length \<tau>s\<^sub>2) \<and> pcs xt \<subseteq> {0..<length \<tau>s\<^sub>1 + length is\<^sub>2} \<and> (\<forall>pc<length \<tau>s\<^sub>1 + length is\<^sub>2. P,T\<^sub>r,mxs,Suc (length \<tau>s\<^sub>1 + length \<tau>s\<^sub>2),xt \<turnstile> (is\<^sub>1 @ is\<^sub>2) ! pc,pc :: \<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2); \<forall>\<tau>\<in>set \<tau>s\<^sub>1. \<forall>ST' LT'. \<tau> = \<lfloor>(ST', LT')\<rfloor> \<longrightarrow> length ST \<le> length ST' \<and> P \<turnstile> \<lfloor>(drop (length ST' - length ST) ST', LT')\<rfloor> \<le>' ty\<^sub>i' ST E A; length is\<^sub>1 = length \<tau>s\<^sub>1; length ST < mxs; case Co of None \<Rightarrow> D = Throwable | \<lfloor>C\<rfloor> \<Rightarrow> D = C \<and> is_class P C\<rbrakk> \<Longrightarrow> \<forall>pc<length \<tau>s\<^sub>1 + length is\<^sub>2. P,T\<^sub>r,mxs,Suc (length \<tau>s\<^sub>1 + length \<tau>s\<^sub>2),xt @ [(0, length \<tau>s\<^sub>1 - Suc n, Co, length \<tau>s\<^sub>1, length ST)] \<turnstile> (is\<^sub>1 @ is\<^sub>2) ! pc,pc :: \<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2
[PROOF STEP]
apply(clarsimp split del: option.split_asm)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>\<tau>\<in>set \<tau>s\<^sub>1. \<forall>ST' LT'. \<tau> = \<lfloor>(ST', LT')\<rfloor> \<longrightarrow> P \<turnstile> \<lfloor>(ST', LT')\<rfloor> \<le>' ty\<^sub>i' ST E A; ?y < mxs; case Co of None \<Rightarrow> D = Throwable | \<lfloor>C\<rfloor> \<Rightarrow> D = C \<and> is_class P C; pcs xt \<subseteq> {0..<?y + ?y}; \<forall>pc<?y1 + ?y1. P,T\<^sub>r,mxs,Suc (?y2 + ?y2),xt \<turnstile> (is\<^sub>1 @ is\<^sub>2) ! pc,pc :: \<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2; \<not> length \<tau>s\<^sub>1 - Suc n \<le> length \<tau>s\<^sub>1 + length is\<^sub>2\<rbrakk> \<Longrightarrow> ?y \<le> Suc n
 2. \<lbrakk>length is\<^sub>2 < Suc (length \<tau>s\<^sub>2) \<and> pcs xt \<subseteq> {0..<length \<tau>s\<^sub>1 + length is\<^sub>2} \<and> (\<forall>pc<length \<tau>s\<^sub>1 + length is\<^sub>2. P,T\<^sub>r,mxs,Suc (length \<tau>s\<^sub>1 + length \<tau>s\<^sub>2),xt \<turnstile> (is\<^sub>1 @ is\<^sub>2) ! pc,pc :: \<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2); \<forall>\<tau>\<in>set \<tau>s\<^sub>1. \<forall>ST' LT'. \<tau> = \<lfloor>(ST', LT')\<rfloor> \<longrightarrow> length ST \<le> length ST' \<and> P \<turnstile> \<lfloor>(drop (length ST' - length ST) ST', LT')\<rfloor> \<le>' ty\<^sub>i' ST E A; length is\<^sub>1 = length \<tau>s\<^sub>1; length ST < mxs; case Co of None \<Rightarrow> D = Throwable | \<lfloor>C\<rfloor> \<Rightarrow> D = C \<and> is_class P C\<rbrakk> \<Longrightarrow> \<forall>pc<length \<tau>s\<^sub>1 + length is\<^sub>2. P,T\<^sub>r,mxs,Suc (length \<tau>s\<^sub>1 + length \<tau>s\<^sub>2),xt @ [(0, length \<tau>s\<^sub>1 - Suc n, Co, length \<tau>s\<^sub>1, length ST)] \<turnstile> (is\<^sub>1 @ is\<^sub>2) ! pc,pc :: \<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2
[PROOF STEP]
apply arith
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length is\<^sub>2 < Suc (length \<tau>s\<^sub>2) \<and> pcs xt \<subseteq> {0..<length \<tau>s\<^sub>1 + length is\<^sub>2} \<and> (\<forall>pc<length \<tau>s\<^sub>1 + length is\<^sub>2. P,T\<^sub>r,mxs,Suc (length \<tau>s\<^sub>1 + length \<tau>s\<^sub>2),xt \<turnstile> (is\<^sub>1 @ is\<^sub>2) ! pc,pc :: \<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2); \<forall>\<tau>\<in>set \<tau>s\<^sub>1. \<forall>ST' LT'. \<tau> = \<lfloor>(ST', LT')\<rfloor> \<longrightarrow> length ST \<le> length ST' \<and> P \<turnstile> \<lfloor>(drop (length ST' - length ST) ST', LT')\<rfloor> \<le>' ty\<^sub>i' ST E A; length is\<^sub>1 = length \<tau>s\<^sub>1; length ST < mxs; case Co of None \<Rightarrow> D = Throwable | \<lfloor>C\<rfloor> \<Rightarrow> D = C \<and> is_class P C\<rbrakk> \<Longrightarrow> \<forall>pc<length \<tau>s\<^sub>1 + length is\<^sub>2. P,T\<^sub>r,mxs,Suc (length \<tau>s\<^sub>1 + length \<tau>s\<^sub>2),xt @ [(0, length \<tau>s\<^sub>1 - Suc n, Co, length \<tau>s\<^sub>1, length ST)] \<turnstile> (is\<^sub>1 @ is\<^sub>2) ! pc,pc :: \<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2
[PROOF STEP]
apply(clarsimp split del: option.split_asm)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>pc. \<lbrakk>\<forall>\<tau>\<in>set \<tau>s\<^sub>1. \<forall>ST' LT'. \<tau> = \<lfloor>(ST', LT')\<rfloor> \<longrightarrow> length ST \<le> length ST' \<and> P \<turnstile> \<lfloor>(drop (length ST' - length ST) ST', LT')\<rfloor> \<le>' ty\<^sub>i' ST E A; length is\<^sub>1 = length \<tau>s\<^sub>1; length ST < mxs; case Co of None \<Rightarrow> D = Throwable | \<lfloor>C\<rfloor> \<Rightarrow> D = C \<and> is_class P C; length is\<^sub>2 < Suc (length \<tau>s\<^sub>2); pcs xt \<subseteq> {0..<length \<tau>s\<^sub>1 + length is\<^sub>2}; \<forall>pc<length \<tau>s\<^sub>1 + length is\<^sub>2. P,T\<^sub>r,mxs,Suc (length \<tau>s\<^sub>1 + length \<tau>s\<^sub>2),xt \<turnstile> (is\<^sub>1 @ is\<^sub>2) ! pc,pc :: \<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2; pc < length \<tau>s\<^sub>1 + length is\<^sub>2\<rbrakk> \<Longrightarrow> P,T\<^sub>r,mxs,Suc (length \<tau>s\<^sub>1 + length \<tau>s\<^sub>2),xt @ [(0, length \<tau>s\<^sub>1 - Suc n, Co, length \<tau>s\<^sub>1, length ST)] \<turnstile> (is\<^sub>1 @ is\<^sub>2) ! pc,pc :: \<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2
[PROOF STEP]
apply(erule allE, erule (1) impE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>pc. \<lbrakk>\<forall>\<tau>\<in>set \<tau>s\<^sub>1. \<forall>ST' LT'. \<tau> = \<lfloor>(ST', LT')\<rfloor> \<longrightarrow> length ST \<le> length ST' \<and> P \<turnstile> \<lfloor>(drop (length ST' - length ST) ST', LT')\<rfloor> \<le>' ty\<^sub>i' ST E A; length is\<^sub>1 = length \<tau>s\<^sub>1; length ST < mxs; case Co of None \<Rightarrow> D = Throwable | \<lfloor>C\<rfloor> \<Rightarrow> D = C \<and> is_class P C; length is\<^sub>2 < Suc (length \<tau>s\<^sub>2); pcs xt \<subseteq> {0..<length \<tau>s\<^sub>1 + length is\<^sub>2}; pc < length \<tau>s\<^sub>1 + length is\<^sub>2; P,T\<^sub>r,mxs,Suc (length \<tau>s\<^sub>1 + length \<tau>s\<^sub>2),xt \<turnstile> (is\<^sub>1 @ is\<^sub>2) ! pc,pc :: \<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2\<rbrakk> \<Longrightarrow> P,T\<^sub>r,mxs,Suc (length \<tau>s\<^sub>1 + length \<tau>s\<^sub>2),xt @ [(0, length \<tau>s\<^sub>1 - Suc n, Co, length \<tau>s\<^sub>1, length ST)] \<turnstile> (is\<^sub>1 @ is\<^sub>2) ! pc,pc :: \<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2
[PROOF STEP]
apply(clarsimp simp add: wt_instr_def app_def eff_def split del: option.split_asm)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>pc a b. \<lbrakk>\<forall>\<tau>\<in>set \<tau>s\<^sub>1. \<forall>ST' LT'. \<tau> = \<lfloor>(ST', LT')\<rfloor> \<longrightarrow> length ST \<le> length ST' \<and> P \<turnstile> \<lfloor>(drop (length ST' - length ST) ST', LT')\<rfloor> \<le>' ty\<^sub>i' ST E A; length is\<^sub>1 = length \<tau>s\<^sub>1; length ST < mxs; case Co of None \<Rightarrow> D = Throwable | \<lfloor>C\<rfloor> \<Rightarrow> D = C \<and> is_class P C; length is\<^sub>2 < Suc (length \<tau>s\<^sub>2); pcs xt \<subseteq> {0..<length \<tau>s\<^sub>1 + length is\<^sub>2}; pc < length \<tau>s\<^sub>1 + length is\<^sub>2; \<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt). case x of (pc', \<tau>') \<Rightarrow> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! pc'; (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! pc = \<lfloor>(a, b)\<rfloor>; app\<^sub>i ((is\<^sub>1 @ is\<^sub>2) ! pc, P, pc, mxs, T\<^sub>r, a, b); xcpt_app ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc mxs xt (a, b); \<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt). case x of (pc', \<tau>') \<Rightarrow> pc' < Suc (length \<tau>s\<^sub>1 + length \<tau>s\<^sub>2)\<rbrakk> \<Longrightarrow> xcpt_app ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc mxs [(0, length \<tau>s\<^sub>1 - Suc n, Co, length \<tau>s\<^sub>1, length ST)] (a, b) \<and> (\<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> (set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) [(0, length \<tau>s\<^sub>1 - Suc n, Co, length \<tau>s\<^sub>1, length ST)])). case x of (pc', \<tau>') \<Rightarrow> pc' < Suc (length \<tau>s\<^sub>1 + length \<tau>s\<^sub>2)) \<and> (\<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> (set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) [(0, length \<tau>s\<^sub>1 - Suc n, Co, length \<tau>s\<^sub>1, length ST)])). case x of (pc', \<tau>') \<Rightarrow> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! pc')
[PROOF STEP]
apply(rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>pc a b. \<lbrakk>\<forall>\<tau>\<in>set \<tau>s\<^sub>1. \<forall>ST' LT'. \<tau> = \<lfloor>(ST', LT')\<rfloor> \<longrightarrow> length ST \<le> length ST' \<and> P \<turnstile> \<lfloor>(drop (length ST' - length ST) ST', LT')\<rfloor> \<le>' ty\<^sub>i' ST E A; length is\<^sub>1 = length \<tau>s\<^sub>1; length ST < mxs; case Co of None \<Rightarrow> D = Throwable | \<lfloor>C\<rfloor> \<Rightarrow> D = C \<and> is_class P C; length is\<^sub>2 < Suc (length \<tau>s\<^sub>2); pcs xt \<subseteq> {0..<length \<tau>s\<^sub>1 + length is\<^sub>2}; pc < length \<tau>s\<^sub>1 + length is\<^sub>2; \<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt). case x of (pc', \<tau>') \<Rightarrow> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! pc'; (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! pc = \<lfloor>(a, b)\<rfloor>; app\<^sub>i ((is\<^sub>1 @ is\<^sub>2) ! pc, P, pc, mxs, T\<^sub>r, a, b); xcpt_app ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc mxs xt (a, b); \<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt). case x of (pc', \<tau>') \<Rightarrow> pc' < Suc (length \<tau>s\<^sub>1 + length \<tau>s\<^sub>2)\<rbrakk> \<Longrightarrow> xcpt_app ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc mxs [(0, length \<tau>s\<^sub>1 - Suc n, Co, length \<tau>s\<^sub>1, length ST)] (a, b)
 2. \<And>pc a b. \<lbrakk>\<forall>\<tau>\<in>set \<tau>s\<^sub>1. \<forall>ST' LT'. \<tau> = \<lfloor>(ST', LT')\<rfloor> \<longrightarrow> length ST \<le> length ST' \<and> P \<turnstile> \<lfloor>(drop (length ST' - length ST) ST', LT')\<rfloor> \<le>' ty\<^sub>i' ST E A; length is\<^sub>1 = length \<tau>s\<^sub>1; length ST < mxs; case Co of None \<Rightarrow> D = Throwable | \<lfloor>C\<rfloor> \<Rightarrow> D = C \<and> is_class P C; length is\<^sub>2 < Suc (length \<tau>s\<^sub>2); pcs xt \<subseteq> {0..<length \<tau>s\<^sub>1 + length is\<^sub>2}; pc < length \<tau>s\<^sub>1 + length is\<^sub>2; \<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt). case x of (pc', \<tau>') \<Rightarrow> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! pc'; (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! pc = \<lfloor>(a, b)\<rfloor>; app\<^sub>i ((is\<^sub>1 @ is\<^sub>2) ! pc, P, pc, mxs, T\<^sub>r, a, b); xcpt_app ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc mxs xt (a, b); \<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt). case x of (pc', \<tau>') \<Rightarrow> pc' < Suc (length \<tau>s\<^sub>1 + length \<tau>s\<^sub>2)\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> (set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) [(0, length \<tau>s\<^sub>1 - Suc n, Co, length \<tau>s\<^sub>1, length ST)])). case x of (pc', \<tau>') \<Rightarrow> pc' < Suc (length \<tau>s\<^sub>1 + length \<tau>s\<^sub>2)) \<and> (\<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> (set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) [(0, length \<tau>s\<^sub>1 - Suc n, Co, length \<tau>s\<^sub>1, length ST)])). case x of (pc', \<tau>') \<Rightarrow> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! pc')
[PROOF STEP]
apply (thin_tac "\<forall>x\<in> A \<union> B. P x" for A B P)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>pc a b. \<lbrakk>\<forall>\<tau>\<in>set \<tau>s\<^sub>1. \<forall>ST' LT'. \<tau> = \<lfloor>(ST', LT')\<rfloor> \<longrightarrow> length ST \<le> length ST' \<and> P \<turnstile> \<lfloor>(drop (length ST' - length ST) ST', LT')\<rfloor> \<le>' ty\<^sub>i' ST E A; length is\<^sub>1 = length \<tau>s\<^sub>1; length ST < mxs; case Co of None \<Rightarrow> D = Throwable | \<lfloor>C\<rfloor> \<Rightarrow> D = C \<and> is_class P C; length is\<^sub>2 < Suc (length \<tau>s\<^sub>2); pcs xt \<subseteq> {0..<length \<tau>s\<^sub>1 + length is\<^sub>2}; pc < length \<tau>s\<^sub>1 + length is\<^sub>2; (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! pc = \<lfloor>(a, b)\<rfloor>; app\<^sub>i ((is\<^sub>1 @ is\<^sub>2) ! pc, P, pc, mxs, T\<^sub>r, a, b); xcpt_app ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc mxs xt (a, b); \<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt). case x of (pc', \<tau>') \<Rightarrow> pc' < Suc (length \<tau>s\<^sub>1 + length \<tau>s\<^sub>2)\<rbrakk> \<Longrightarrow> xcpt_app ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc mxs [(0, length \<tau>s\<^sub>1 - Suc n, Co, length \<tau>s\<^sub>1, length ST)] (a, b)
 2. \<And>pc a b. \<lbrakk>\<forall>\<tau>\<in>set \<tau>s\<^sub>1. \<forall>ST' LT'. \<tau> = \<lfloor>(ST', LT')\<rfloor> \<longrightarrow> length ST \<le> length ST' \<and> P \<turnstile> \<lfloor>(drop (length ST' - length ST) ST', LT')\<rfloor> \<le>' ty\<^sub>i' ST E A; length is\<^sub>1 = length \<tau>s\<^sub>1; length ST < mxs; case Co of None \<Rightarrow> D = Throwable | \<lfloor>C\<rfloor> \<Rightarrow> D = C \<and> is_class P C; length is\<^sub>2 < Suc (length \<tau>s\<^sub>2); pcs xt \<subseteq> {0..<length \<tau>s\<^sub>1 + length is\<^sub>2}; pc < length \<tau>s\<^sub>1 + length is\<^sub>2; \<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt). case x of (pc', \<tau>') \<Rightarrow> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! pc'; (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! pc = \<lfloor>(a, b)\<rfloor>; app\<^sub>i ((is\<^sub>1 @ is\<^sub>2) ! pc, P, pc, mxs, T\<^sub>r, a, b); xcpt_app ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc mxs xt (a, b); \<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt). case x of (pc', \<tau>') \<Rightarrow> pc' < Suc (length \<tau>s\<^sub>1 + length \<tau>s\<^sub>2)\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> (set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) [(0, length \<tau>s\<^sub>1 - Suc n, Co, length \<tau>s\<^sub>1, length ST)])). case x of (pc', \<tau>') \<Rightarrow> pc' < Suc (length \<tau>s\<^sub>1 + length \<tau>s\<^sub>2)) \<and> (\<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> (set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) [(0, length \<tau>s\<^sub>1 - Suc n, Co, length \<tau>s\<^sub>1, length ST)])). case x of (pc', \<tau>') \<Rightarrow> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! pc')
[PROOF STEP]
apply (thin_tac "\<forall>x\<in> A \<union> B. P x" for A B P)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>pc a b. \<lbrakk>\<forall>\<tau>\<in>set \<tau>s\<^sub>1. \<forall>ST' LT'. \<tau> = \<lfloor>(ST', LT')\<rfloor> \<longrightarrow> length ST \<le> length ST' \<and> P \<turnstile> \<lfloor>(drop (length ST' - length ST) ST', LT')\<rfloor> \<le>' ty\<^sub>i' ST E A; length is\<^sub>1 = length \<tau>s\<^sub>1; length ST < mxs; case Co of None \<Rightarrow> D = Throwable | \<lfloor>C\<rfloor> \<Rightarrow> D = C \<and> is_class P C; length is\<^sub>2 < Suc (length \<tau>s\<^sub>2); pcs xt \<subseteq> {0..<length \<tau>s\<^sub>1 + length is\<^sub>2}; pc < length \<tau>s\<^sub>1 + length is\<^sub>2; (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! pc = \<lfloor>(a, b)\<rfloor>; app\<^sub>i ((is\<^sub>1 @ is\<^sub>2) ! pc, P, pc, mxs, T\<^sub>r, a, b); xcpt_app ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc mxs xt (a, b)\<rbrakk> \<Longrightarrow> xcpt_app ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc mxs [(0, length \<tau>s\<^sub>1 - Suc n, Co, length \<tau>s\<^sub>1, length ST)] (a, b)
 2. \<And>pc a b. \<lbrakk>\<forall>\<tau>\<in>set \<tau>s\<^sub>1. \<forall>ST' LT'. \<tau> = \<lfloor>(ST', LT')\<rfloor> \<longrightarrow> length ST \<le> length ST' \<and> P \<turnstile> \<lfloor>(drop (length ST' - length ST) ST', LT')\<rfloor> \<le>' ty\<^sub>i' ST E A; length is\<^sub>1 = length \<tau>s\<^sub>1; length ST < mxs; case Co of None \<Rightarrow> D = Throwable | \<lfloor>C\<rfloor> \<Rightarrow> D = C \<and> is_class P C; length is\<^sub>2 < Suc (length \<tau>s\<^sub>2); pcs xt \<subseteq> {0..<length \<tau>s\<^sub>1 + length is\<^sub>2}; pc < length \<tau>s\<^sub>1 + length is\<^sub>2; \<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt). case x of (pc', \<tau>') \<Rightarrow> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! pc'; (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! pc = \<lfloor>(a, b)\<rfloor>; app\<^sub>i ((is\<^sub>1 @ is\<^sub>2) ! pc, P, pc, mxs, T\<^sub>r, a, b); xcpt_app ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc mxs xt (a, b); \<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt). case x of (pc', \<tau>') \<Rightarrow> pc' < Suc (length \<tau>s\<^sub>1 + length \<tau>s\<^sub>2)\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> (set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) [(0, length \<tau>s\<^sub>1 - Suc n, Co, length \<tau>s\<^sub>1, length ST)])). case x of (pc', \<tau>') \<Rightarrow> pc' < Suc (length \<tau>s\<^sub>1 + length \<tau>s\<^sub>2)) \<and> (\<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> (set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) [(0, length \<tau>s\<^sub>1 - Suc n, Co, length \<tau>s\<^sub>1, length ST)])). case x of (pc', \<tau>') \<Rightarrow> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! pc')
[PROOF STEP]
apply (clarsimp simp add: xcpt_app_def relevant_entries_def split del: option.split_asm)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>pc a b. \<lbrakk>\<forall>\<tau>\<in>set \<tau>s\<^sub>1. \<forall>ST' LT'. \<tau> = \<lfloor>(ST', LT')\<rfloor> \<longrightarrow> length ST \<le> length ST' \<and> P \<turnstile> \<lfloor>(drop (length ST' - length ST) ST', LT')\<rfloor> \<le>' ty\<^sub>i' ST E A; length is\<^sub>1 = length \<tau>s\<^sub>1; length ST < mxs; case Co of None \<Rightarrow> D = Throwable | \<lfloor>C\<rfloor> \<Rightarrow> D = C \<and> is_class P C; length is\<^sub>2 < Suc (length \<tau>s\<^sub>2); pcs xt \<subseteq> {0..<length \<tau>s\<^sub>1 + length is\<^sub>2}; pc < length \<tau>s\<^sub>1 + length is\<^sub>2; (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! pc = \<lfloor>(a, b)\<rfloor>; app\<^sub>i ((is\<^sub>1 @ is\<^sub>2) ! pc, P, pc, mxs, T\<^sub>r, a, b); \<forall>aa ab ac ad b. (aa, ab, ac, ad, b) \<in> set xt \<and> is_relevant_entry P ((is\<^sub>1 @ is\<^sub>2) ! pc) pc (aa, ab, ac, ad, b) \<longrightarrow> (case ac of None \<Rightarrow> True | \<lfloor>x\<rfloor> \<Rightarrow> is_class P x) \<and> b \<le> length a \<and> b < mxs\<rbrakk> \<Longrightarrow> (Co = Any \<longrightarrow> is_relevant_entry P ((is\<^sub>1 @ is\<^sub>2) ! pc) pc (0, length \<tau>s\<^sub>1 - Suc n, Any, length \<tau>s\<^sub>1, length ST) \<longrightarrow> length ST \<le> length a) \<and> (\<forall>x2. Co = \<lfloor>x2\<rfloor> \<longrightarrow> is_relevant_entry P ((is\<^sub>1 @ is\<^sub>2) ! pc) pc (0, length \<tau>s\<^sub>1 - Suc n, \<lfloor>x2\<rfloor>, length \<tau>s\<^sub>1, length ST) \<longrightarrow> is_class P x2 \<and> length ST \<le> length a)
 2. \<And>pc a b. \<lbrakk>\<forall>\<tau>\<in>set \<tau>s\<^sub>1. \<forall>ST' LT'. \<tau> = \<lfloor>(ST', LT')\<rfloor> \<longrightarrow> length ST \<le> length ST' \<and> P \<turnstile> \<lfloor>(drop (length ST' - length ST) ST', LT')\<rfloor> \<le>' ty\<^sub>i' ST E A; length is\<^sub>1 = length \<tau>s\<^sub>1; length ST < mxs; case Co of None \<Rightarrow> D = Throwable | \<lfloor>C\<rfloor> \<Rightarrow> D = C \<and> is_class P C; length is\<^sub>2 < Suc (length \<tau>s\<^sub>2); pcs xt \<subseteq> {0..<length \<tau>s\<^sub>1 + length is\<^sub>2}; pc < length \<tau>s\<^sub>1 + length is\<^sub>2; \<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt). case x of (pc', \<tau>') \<Rightarrow> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! pc'; (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! pc = \<lfloor>(a, b)\<rfloor>; app\<^sub>i ((is\<^sub>1 @ is\<^sub>2) ! pc, P, pc, mxs, T\<^sub>r, a, b); xcpt_app ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc mxs xt (a, b); \<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt). case x of (pc', \<tau>') \<Rightarrow> pc' < Suc (length \<tau>s\<^sub>1 + length \<tau>s\<^sub>2)\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> (set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) [(0, length \<tau>s\<^sub>1 - Suc n, Co, length \<tau>s\<^sub>1, length ST)])). case x of (pc', \<tau>') \<Rightarrow> pc' < Suc (length \<tau>s\<^sub>1 + length \<tau>s\<^sub>2)) \<and> (\<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> (set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) [(0, length \<tau>s\<^sub>1 - Suc n, Co, length \<tau>s\<^sub>1, length ST)])). case x of (pc', \<tau>') \<Rightarrow> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! pc')
[PROOF STEP]
apply (simp add: nth_append is_relevant_entry_def split: if_split_asm split del: option.split_asm)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>pc a b. \<lbrakk>\<forall>\<tau>\<in>set \<tau>s\<^sub>1. \<forall>ST' LT'. \<tau> = \<lfloor>(ST', LT')\<rfloor> \<longrightarrow> length ST \<le> length ST' \<and> P \<turnstile> \<lfloor>(drop (length ST' - length ST) ST', LT')\<rfloor> \<le>' ty\<^sub>i' ST E A; length is\<^sub>1 = length \<tau>s\<^sub>1; length ST < mxs; case Co of None \<Rightarrow> D = Throwable | \<lfloor>C\<rfloor> \<Rightarrow> D = C \<and> is_class P C; length is\<^sub>2 < Suc (length \<tau>s\<^sub>2); pcs xt \<subseteq> {0..<length \<tau>s\<^sub>1 + length is\<^sub>2}; \<tau>s\<^sub>1 ! pc = \<lfloor>(a, b)\<rfloor>; app\<^sub>i (is\<^sub>1 ! pc, P, pc, mxs, T\<^sub>r, a, b); pc < length \<tau>s\<^sub>1; \<forall>aa ab ac ad b. (aa, ab, ac, ad, b) \<in> set xt \<and> (case ac of None \<Rightarrow> True | \<lfloor>x\<rfloor> \<Rightarrow> is_relevant_class (is\<^sub>1 ! pc) P x) \<and> aa \<le> pc \<and> pc < ab \<longrightarrow> (case ac of None \<Rightarrow> True | \<lfloor>x\<rfloor> \<Rightarrow> is_class P x) \<and> b \<le> length a \<and> b < mxs\<rbrakk> \<Longrightarrow> (Co = Any \<longrightarrow> pc < length \<tau>s\<^sub>1 - Suc n \<longrightarrow> length ST \<le> length a) \<and> (\<forall>x2. Co = \<lfloor>x2\<rfloor> \<longrightarrow> is_relevant_class (is\<^sub>1 ! pc) P x2 \<and> pc < length \<tau>s\<^sub>1 - Suc n \<longrightarrow> is_class P x2 \<and> length ST \<le> length a)
 2. \<And>pc a b. \<lbrakk>\<forall>\<tau>\<in>set \<tau>s\<^sub>1. \<forall>ST' LT'. \<tau> = \<lfloor>(ST', LT')\<rfloor> \<longrightarrow> length ST \<le> length ST' \<and> P \<turnstile> \<lfloor>(drop (length ST' - length ST) ST', LT')\<rfloor> \<le>' ty\<^sub>i' ST E A; length is\<^sub>1 = length \<tau>s\<^sub>1; length ST < mxs; case Co of None \<Rightarrow> D = Throwable | \<lfloor>C\<rfloor> \<Rightarrow> D = C \<and> is_class P C; length is\<^sub>2 < Suc (length \<tau>s\<^sub>2); pcs xt \<subseteq> {0..<length \<tau>s\<^sub>1 + length is\<^sub>2}; pc < length \<tau>s\<^sub>1 + length is\<^sub>2; (ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! (pc - length \<tau>s\<^sub>1) = \<lfloor>(a, b)\<rfloor>; app\<^sub>i (is\<^sub>2 ! (pc - length \<tau>s\<^sub>1), P, pc, mxs, T\<^sub>r, a, b); \<not> pc < length \<tau>s\<^sub>1; \<forall>aa ab ac ad b. (aa, ab, ac, ad, b) \<in> set xt \<and> (case ac of None \<Rightarrow> True | \<lfloor>x\<rfloor> \<Rightarrow> is_relevant_class (is\<^sub>2 ! (pc - length is\<^sub>1)) P x) \<and> aa \<le> pc \<and> pc < ab \<longrightarrow> (case ac of None \<Rightarrow> True | \<lfloor>x\<rfloor> \<Rightarrow> is_class P x) \<and> b \<le> length a \<and> b < mxs\<rbrakk> \<Longrightarrow> \<forall>x2. Co = \<lfloor>x2\<rfloor> \<longrightarrow> is_relevant_class (is\<^sub>2 ! (pc - length \<tau>s\<^sub>1)) P x2 \<and> pc < length \<tau>s\<^sub>1 - Suc n \<longrightarrow> is_class P x2 \<and> length ST \<le> length a
 3. \<And>pc a b. \<lbrakk>\<forall>\<tau>\<in>set \<tau>s\<^sub>1. \<forall>ST' LT'. \<tau> = \<lfloor>(ST', LT')\<rfloor> \<longrightarrow> length ST \<le> length ST' \<and> P \<turnstile> \<lfloor>(drop (length ST' - length ST) ST', LT')\<rfloor> \<le>' ty\<^sub>i' ST E A; length is\<^sub>1 = length \<tau>s\<^sub>1; length ST < mxs; case Co of None \<Rightarrow> D = Throwable | \<lfloor>C\<rfloor> \<Rightarrow> D = C \<and> is_class P C; length is\<^sub>2 < Suc (length \<tau>s\<^sub>2); pcs xt \<subseteq> {0..<length \<tau>s\<^sub>1 + length is\<^sub>2}; pc < length \<tau>s\<^sub>1 + length is\<^sub>2; \<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt). case x of (pc', \<tau>') \<Rightarrow> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! pc'; (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! pc = \<lfloor>(a, b)\<rfloor>; app\<^sub>i ((is\<^sub>1 @ is\<^sub>2) ! pc, P, pc, mxs, T\<^sub>r, a, b); xcpt_app ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc mxs xt (a, b); \<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt). case x of (pc', \<tau>') \<Rightarrow> pc' < Suc (length \<tau>s\<^sub>1 + length \<tau>s\<^sub>2)\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> (set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) [(0, length \<tau>s\<^sub>1 - Suc n, Co, length \<tau>s\<^sub>1, length ST)])). case x of (pc', \<tau>') \<Rightarrow> pc' < Suc (length \<tau>s\<^sub>1 + length \<tau>s\<^sub>2)) \<and> (\<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> (set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) [(0, length \<tau>s\<^sub>1 - Suc n, Co, length \<tau>s\<^sub>1, length ST)])). case x of (pc', \<tau>') \<Rightarrow> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! pc')
[PROOF STEP]
apply (drule_tac x="\<tau>s\<^sub>1!pc" in bspec)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>pc a b. \<lbrakk>length is\<^sub>1 = length \<tau>s\<^sub>1; length ST < mxs; case Co of None \<Rightarrow> D = Throwable | \<lfloor>C\<rfloor> \<Rightarrow> D = C \<and> is_class P C; length is\<^sub>2 < Suc (length \<tau>s\<^sub>2); pcs xt \<subseteq> {0..<length \<tau>s\<^sub>1 + length is\<^sub>2}; \<tau>s\<^sub>1 ! pc = \<lfloor>(a, b)\<rfloor>; app\<^sub>i (is\<^sub>1 ! pc, P, pc, mxs, T\<^sub>r, a, b); pc < length \<tau>s\<^sub>1; \<forall>aa ab ac ad b. (aa, ab, ac, ad, b) \<in> set xt \<and> (case ac of None \<Rightarrow> True | \<lfloor>x\<rfloor> \<Rightarrow> is_relevant_class (is\<^sub>1 ! pc) P x) \<and> aa \<le> pc \<and> pc < ab \<longrightarrow> (case ac of None \<Rightarrow> True | \<lfloor>x\<rfloor> \<Rightarrow> is_class P x) \<and> b \<le> length a \<and> b < mxs\<rbrakk> \<Longrightarrow> \<tau>s\<^sub>1 ! pc \<in> set \<tau>s\<^sub>1
 2. \<And>pc a b. \<lbrakk>length is\<^sub>1 = length \<tau>s\<^sub>1; length ST < mxs; case Co of None \<Rightarrow> D = Throwable | \<lfloor>C\<rfloor> \<Rightarrow> D = C \<and> is_class P C; length is\<^sub>2 < Suc (length \<tau>s\<^sub>2); pcs xt \<subseteq> {0..<length \<tau>s\<^sub>1 + length is\<^sub>2}; \<tau>s\<^sub>1 ! pc = \<lfloor>(a, b)\<rfloor>; app\<^sub>i (is\<^sub>1 ! pc, P, pc, mxs, T\<^sub>r, a, b); pc < length \<tau>s\<^sub>1; \<forall>aa ab ac ad b. (aa, ab, ac, ad, b) \<in> set xt \<and> (case ac of None \<Rightarrow> True | \<lfloor>x\<rfloor> \<Rightarrow> is_relevant_class (is\<^sub>1 ! pc) P x) \<and> aa \<le> pc \<and> pc < ab \<longrightarrow> (case ac of None \<Rightarrow> True | \<lfloor>x\<rfloor> \<Rightarrow> is_class P x) \<and> b \<le> length a \<and> b < mxs; \<forall>ST' LT'. \<tau>s\<^sub>1 ! pc = \<lfloor>(ST', LT')\<rfloor> \<longrightarrow> length ST \<le> length ST' \<and> P \<turnstile> \<lfloor>(drop (length ST' - length ST) ST', LT')\<rfloor> \<le>' ty\<^sub>i' ST E A\<rbrakk> \<Longrightarrow> (Co = Any \<longrightarrow> pc < length \<tau>s\<^sub>1 - Suc n \<longrightarrow> length ST \<le> length a) \<and> (\<forall>x2. Co = \<lfloor>x2\<rfloor> \<longrightarrow> is_relevant_class (is\<^sub>1 ! pc) P x2 \<and> pc < length \<tau>s\<^sub>1 - Suc n \<longrightarrow> is_class P x2 \<and> length ST \<le> length a)
 3. \<And>pc a b. \<lbrakk>\<forall>\<tau>\<in>set \<tau>s\<^sub>1. \<forall>ST' LT'. \<tau> = \<lfloor>(ST', LT')\<rfloor> \<longrightarrow> length ST \<le> length ST' \<and> P \<turnstile> \<lfloor>(drop (length ST' - length ST) ST', LT')\<rfloor> \<le>' ty\<^sub>i' ST E A; length is\<^sub>1 = length \<tau>s\<^sub>1; length ST < mxs; case Co of None \<Rightarrow> D = Throwable | \<lfloor>C\<rfloor> \<Rightarrow> D = C \<and> is_class P C; length is\<^sub>2 < Suc (length \<tau>s\<^sub>2); pcs xt \<subseteq> {0..<length \<tau>s\<^sub>1 + length is\<^sub>2}; pc < length \<tau>s\<^sub>1 + length is\<^sub>2; (ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! (pc - length \<tau>s\<^sub>1) = \<lfloor>(a, b)\<rfloor>; app\<^sub>i (is\<^sub>2 ! (pc - length \<tau>s\<^sub>1), P, pc, mxs, T\<^sub>r, a, b); \<not> pc < length \<tau>s\<^sub>1; \<forall>aa ab ac ad b. (aa, ab, ac, ad, b) \<in> set xt \<and> (case ac of None \<Rightarrow> True | \<lfloor>x\<rfloor> \<Rightarrow> is_relevant_class (is\<^sub>2 ! (pc - length is\<^sub>1)) P x) \<and> aa \<le> pc \<and> pc < ab \<longrightarrow> (case ac of None \<Rightarrow> True | \<lfloor>x\<rfloor> \<Rightarrow> is_class P x) \<and> b \<le> length a \<and> b < mxs\<rbrakk> \<Longrightarrow> \<forall>x2. Co = \<lfloor>x2\<rfloor> \<longrightarrow> is_relevant_class (is\<^sub>2 ! (pc - length \<tau>s\<^sub>1)) P x2 \<and> pc < length \<tau>s\<^sub>1 - Suc n \<longrightarrow> is_class P x2 \<and> length ST \<le> length a
 4. \<And>pc a b. \<lbrakk>\<forall>\<tau>\<in>set \<tau>s\<^sub>1. \<forall>ST' LT'. \<tau> = \<lfloor>(ST', LT')\<rfloor> \<longrightarrow> length ST \<le> length ST' \<and> P \<turnstile> \<lfloor>(drop (length ST' - length ST) ST', LT')\<rfloor> \<le>' ty\<^sub>i' ST E A; length is\<^sub>1 = length \<tau>s\<^sub>1; length ST < mxs; case Co of None \<Rightarrow> D = Throwable | \<lfloor>C\<rfloor> \<Rightarrow> D = C \<and> is_class P C; length is\<^sub>2 < Suc (length \<tau>s\<^sub>2); pcs xt \<subseteq> {0..<length \<tau>s\<^sub>1 + length is\<^sub>2}; pc < length \<tau>s\<^sub>1 + length is\<^sub>2; \<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt). case x of (pc', \<tau>') \<Rightarrow> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! pc'; (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! pc = \<lfloor>(a, b)\<rfloor>; app\<^sub>i ((is\<^sub>1 @ is\<^sub>2) ! pc, P, pc, mxs, T\<^sub>r, a, b); xcpt_app ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc mxs xt (a, b); \<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt). case x of (pc', \<tau>') \<Rightarrow> pc' < Suc (length \<tau>s\<^sub>1 + length \<tau>s\<^sub>2)\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> (set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) [(0, length \<tau>s\<^sub>1 - Suc n, Co, length \<tau>s\<^sub>1, length ST)])). case x of (pc', \<tau>') \<Rightarrow> pc' < Suc (length \<tau>s\<^sub>1 + length \<tau>s\<^sub>2)) \<and> (\<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> (set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) [(0, length \<tau>s\<^sub>1 - Suc n, Co, length \<tau>s\<^sub>1, length ST)])). case x of (pc', \<tau>') \<Rightarrow> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! pc')
[PROOF STEP]
apply (blast intro: nth_mem)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>pc a b. \<lbrakk>length is\<^sub>1 = length \<tau>s\<^sub>1; length ST < mxs; case Co of None \<Rightarrow> D = Throwable | \<lfloor>C\<rfloor> \<Rightarrow> D = C \<and> is_class P C; length is\<^sub>2 < Suc (length \<tau>s\<^sub>2); pcs xt \<subseteq> {0..<length \<tau>s\<^sub>1 + length is\<^sub>2}; \<tau>s\<^sub>1 ! pc = \<lfloor>(a, b)\<rfloor>; app\<^sub>i (is\<^sub>1 ! pc, P, pc, mxs, T\<^sub>r, a, b); pc < length \<tau>s\<^sub>1; \<forall>aa ab ac ad b. (aa, ab, ac, ad, b) \<in> set xt \<and> (case ac of None \<Rightarrow> True | \<lfloor>x\<rfloor> \<Rightarrow> is_relevant_class (is\<^sub>1 ! pc) P x) \<and> aa \<le> pc \<and> pc < ab \<longrightarrow> (case ac of None \<Rightarrow> True | \<lfloor>x\<rfloor> \<Rightarrow> is_class P x) \<and> b \<le> length a \<and> b < mxs; \<forall>ST' LT'. \<tau>s\<^sub>1 ! pc = \<lfloor>(ST', LT')\<rfloor> \<longrightarrow> length ST \<le> length ST' \<and> P \<turnstile> \<lfloor>(drop (length ST' - length ST) ST', LT')\<rfloor> \<le>' ty\<^sub>i' ST E A\<rbrakk> \<Longrightarrow> (Co = Any \<longrightarrow> pc < length \<tau>s\<^sub>1 - Suc n \<longrightarrow> length ST \<le> length a) \<and> (\<forall>x2. Co = \<lfloor>x2\<rfloor> \<longrightarrow> is_relevant_class (is\<^sub>1 ! pc) P x2 \<and> pc < length \<tau>s\<^sub>1 - Suc n \<longrightarrow> is_class P x2 \<and> length ST \<le> length a)
 2. \<And>pc a b. \<lbrakk>\<forall>\<tau>\<in>set \<tau>s\<^sub>1. \<forall>ST' LT'. \<tau> = \<lfloor>(ST', LT')\<rfloor> \<longrightarrow> length ST \<le> length ST' \<and> P \<turnstile> \<lfloor>(drop (length ST' - length ST) ST', LT')\<rfloor> \<le>' ty\<^sub>i' ST E A; length is\<^sub>1 = length \<tau>s\<^sub>1; length ST < mxs; case Co of None \<Rightarrow> D = Throwable | \<lfloor>C\<rfloor> \<Rightarrow> D = C \<and> is_class P C; length is\<^sub>2 < Suc (length \<tau>s\<^sub>2); pcs xt \<subseteq> {0..<length \<tau>s\<^sub>1 + length is\<^sub>2}; pc < length \<tau>s\<^sub>1 + length is\<^sub>2; (ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! (pc - length \<tau>s\<^sub>1) = \<lfloor>(a, b)\<rfloor>; app\<^sub>i (is\<^sub>2 ! (pc - length \<tau>s\<^sub>1), P, pc, mxs, T\<^sub>r, a, b); \<not> pc < length \<tau>s\<^sub>1; \<forall>aa ab ac ad b. (aa, ab, ac, ad, b) \<in> set xt \<and> (case ac of None \<Rightarrow> True | \<lfloor>x\<rfloor> \<Rightarrow> is_relevant_class (is\<^sub>2 ! (pc - length is\<^sub>1)) P x) \<and> aa \<le> pc \<and> pc < ab \<longrightarrow> (case ac of None \<Rightarrow> True | \<lfloor>x\<rfloor> \<Rightarrow> is_class P x) \<and> b \<le> length a \<and> b < mxs\<rbrakk> \<Longrightarrow> \<forall>x2. Co = \<lfloor>x2\<rfloor> \<longrightarrow> is_relevant_class (is\<^sub>2 ! (pc - length \<tau>s\<^sub>1)) P x2 \<and> pc < length \<tau>s\<^sub>1 - Suc n \<longrightarrow> is_class P x2 \<and> length ST \<le> length a
 3. \<And>pc a b. \<lbrakk>\<forall>\<tau>\<in>set \<tau>s\<^sub>1. \<forall>ST' LT'. \<tau> = \<lfloor>(ST', LT')\<rfloor> \<longrightarrow> length ST \<le> length ST' \<and> P \<turnstile> \<lfloor>(drop (length ST' - length ST) ST', LT')\<rfloor> \<le>' ty\<^sub>i' ST E A; length is\<^sub>1 = length \<tau>s\<^sub>1; length ST < mxs; case Co of None \<Rightarrow> D = Throwable | \<lfloor>C\<rfloor> \<Rightarrow> D = C \<and> is_class P C; length is\<^sub>2 < Suc (length \<tau>s\<^sub>2); pcs xt \<subseteq> {0..<length \<tau>s\<^sub>1 + length is\<^sub>2}; pc < length \<tau>s\<^sub>1 + length is\<^sub>2; \<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt). case x of (pc', \<tau>') \<Rightarrow> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! pc'; (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! pc = \<lfloor>(a, b)\<rfloor>; app\<^sub>i ((is\<^sub>1 @ is\<^sub>2) ! pc, P, pc, mxs, T\<^sub>r, a, b); xcpt_app ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc mxs xt (a, b); \<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt). case x of (pc', \<tau>') \<Rightarrow> pc' < Suc (length \<tau>s\<^sub>1 + length \<tau>s\<^sub>2)\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> (set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) [(0, length \<tau>s\<^sub>1 - Suc n, Co, length \<tau>s\<^sub>1, length ST)])). case x of (pc', \<tau>') \<Rightarrow> pc' < Suc (length \<tau>s\<^sub>1 + length \<tau>s\<^sub>2)) \<and> (\<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> (set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) [(0, length \<tau>s\<^sub>1 - Suc n, Co, length \<tau>s\<^sub>1, length ST)])). case x of (pc', \<tau>') \<Rightarrow> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! pc')
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>pc a b. \<lbrakk>\<forall>\<tau>\<in>set \<tau>s\<^sub>1. \<forall>ST' LT'. \<tau> = \<lfloor>(ST', LT')\<rfloor> \<longrightarrow> length ST \<le> length ST' \<and> P \<turnstile> \<lfloor>(drop (length ST' - length ST) ST', LT')\<rfloor> \<le>' ty\<^sub>i' ST E A; length is\<^sub>1 = length \<tau>s\<^sub>1; length ST < mxs; case Co of None \<Rightarrow> D = Throwable | \<lfloor>C\<rfloor> \<Rightarrow> D = C \<and> is_class P C; length is\<^sub>2 < Suc (length \<tau>s\<^sub>2); pcs xt \<subseteq> {0..<length \<tau>s\<^sub>1 + length is\<^sub>2}; pc < length \<tau>s\<^sub>1 + length is\<^sub>2; (ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! (pc - length \<tau>s\<^sub>1) = \<lfloor>(a, b)\<rfloor>; app\<^sub>i (is\<^sub>2 ! (pc - length \<tau>s\<^sub>1), P, pc, mxs, T\<^sub>r, a, b); \<not> pc < length \<tau>s\<^sub>1; \<forall>aa ab ac ad b. (aa, ab, ac, ad, b) \<in> set xt \<and> (case ac of None \<Rightarrow> True | \<lfloor>x\<rfloor> \<Rightarrow> is_relevant_class (is\<^sub>2 ! (pc - length is\<^sub>1)) P x) \<and> aa \<le> pc \<and> pc < ab \<longrightarrow> (case ac of None \<Rightarrow> True | \<lfloor>x\<rfloor> \<Rightarrow> is_class P x) \<and> b \<le> length a \<and> b < mxs\<rbrakk> \<Longrightarrow> \<forall>x2. Co = \<lfloor>x2\<rfloor> \<longrightarrow> is_relevant_class (is\<^sub>2 ! (pc - length \<tau>s\<^sub>1)) P x2 \<and> pc < length \<tau>s\<^sub>1 - Suc n \<longrightarrow> is_class P x2 \<and> length ST \<le> length a
 2. \<And>pc a b. \<lbrakk>\<forall>\<tau>\<in>set \<tau>s\<^sub>1. \<forall>ST' LT'. \<tau> = \<lfloor>(ST', LT')\<rfloor> \<longrightarrow> length ST \<le> length ST' \<and> P \<turnstile> \<lfloor>(drop (length ST' - length ST) ST', LT')\<rfloor> \<le>' ty\<^sub>i' ST E A; length is\<^sub>1 = length \<tau>s\<^sub>1; length ST < mxs; case Co of None \<Rightarrow> D = Throwable | \<lfloor>C\<rfloor> \<Rightarrow> D = C \<and> is_class P C; length is\<^sub>2 < Suc (length \<tau>s\<^sub>2); pcs xt \<subseteq> {0..<length \<tau>s\<^sub>1 + length is\<^sub>2}; pc < length \<tau>s\<^sub>1 + length is\<^sub>2; \<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt). case x of (pc', \<tau>') \<Rightarrow> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! pc'; (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! pc = \<lfloor>(a, b)\<rfloor>; app\<^sub>i ((is\<^sub>1 @ is\<^sub>2) ! pc, P, pc, mxs, T\<^sub>r, a, b); xcpt_app ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc mxs xt (a, b); \<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt). case x of (pc', \<tau>') \<Rightarrow> pc' < Suc (length \<tau>s\<^sub>1 + length \<tau>s\<^sub>2)\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> (set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) [(0, length \<tau>s\<^sub>1 - Suc n, Co, length \<tau>s\<^sub>1, length ST)])). case x of (pc', \<tau>') \<Rightarrow> pc' < Suc (length \<tau>s\<^sub>1 + length \<tau>s\<^sub>2)) \<and> (\<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> (set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) [(0, length \<tau>s\<^sub>1 - Suc n, Co, length \<tau>s\<^sub>1, length ST)])). case x of (pc', \<tau>') \<Rightarrow> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! pc')
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>pc a b. \<lbrakk>\<forall>\<tau>\<in>set \<tau>s\<^sub>1. \<forall>ST' LT'. \<tau> = \<lfloor>(ST', LT')\<rfloor> \<longrightarrow> length ST \<le> length ST' \<and> P \<turnstile> \<lfloor>(drop (length ST' - length ST) ST', LT')\<rfloor> \<le>' ty\<^sub>i' ST E A; length is\<^sub>1 = length \<tau>s\<^sub>1; length ST < mxs; case Co of None \<Rightarrow> D = Throwable | \<lfloor>C\<rfloor> \<Rightarrow> D = C \<and> is_class P C; length is\<^sub>2 < Suc (length \<tau>s\<^sub>2); pcs xt \<subseteq> {0..<length \<tau>s\<^sub>1 + length is\<^sub>2}; pc < length \<tau>s\<^sub>1 + length is\<^sub>2; \<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt). case x of (pc', \<tau>') \<Rightarrow> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! pc'; (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! pc = \<lfloor>(a, b)\<rfloor>; app\<^sub>i ((is\<^sub>1 @ is\<^sub>2) ! pc, P, pc, mxs, T\<^sub>r, a, b); xcpt_app ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc mxs xt (a, b); \<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt). case x of (pc', \<tau>') \<Rightarrow> pc' < Suc (length \<tau>s\<^sub>1 + length \<tau>s\<^sub>2)\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> (set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) [(0, length \<tau>s\<^sub>1 - Suc n, Co, length \<tau>s\<^sub>1, length ST)])). case x of (pc', \<tau>') \<Rightarrow> pc' < Suc (length \<tau>s\<^sub>1 + length \<tau>s\<^sub>2)) \<and> (\<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> (set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) [(0, length \<tau>s\<^sub>1 - Suc n, Co, length \<tau>s\<^sub>1, length ST)])). case x of (pc', \<tau>') \<Rightarrow> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! pc')
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>pc a b. \<lbrakk>\<forall>\<tau>\<in>set \<tau>s\<^sub>1. \<forall>ST' LT'. \<tau> = \<lfloor>(ST', LT')\<rfloor> \<longrightarrow> length ST \<le> length ST' \<and> P \<turnstile> \<lfloor>(drop (length ST' - length ST) ST', LT')\<rfloor> \<le>' ty\<^sub>i' ST E A; length is\<^sub>1 = length \<tau>s\<^sub>1; length ST < mxs; case Co of None \<Rightarrow> D = Throwable | \<lfloor>C\<rfloor> \<Rightarrow> D = C \<and> is_class P C; length is\<^sub>2 < Suc (length \<tau>s\<^sub>2); pcs xt \<subseteq> {0..<length \<tau>s\<^sub>1 + length is\<^sub>2}; pc < length \<tau>s\<^sub>1 + length is\<^sub>2; \<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt). case x of (pc', \<tau>') \<Rightarrow> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! pc'; (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! pc = \<lfloor>(a, b)\<rfloor>; app\<^sub>i ((is\<^sub>1 @ is\<^sub>2) ! pc, P, pc, mxs, T\<^sub>r, a, b); xcpt_app ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc mxs xt (a, b); \<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt). case x of (pc', \<tau>') \<Rightarrow> pc' < Suc (length \<tau>s\<^sub>1 + length \<tau>s\<^sub>2)\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> (set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) [(0, length \<tau>s\<^sub>1 - Suc n, Co, length \<tau>s\<^sub>1, length ST)])). case x of (pc', \<tau>') \<Rightarrow> pc' < Suc (length \<tau>s\<^sub>1 + length \<tau>s\<^sub>2)
 2. \<And>pc a b. \<lbrakk>\<forall>\<tau>\<in>set \<tau>s\<^sub>1. \<forall>ST' LT'. \<tau> = \<lfloor>(ST', LT')\<rfloor> \<longrightarrow> length ST \<le> length ST' \<and> P \<turnstile> \<lfloor>(drop (length ST' - length ST) ST', LT')\<rfloor> \<le>' ty\<^sub>i' ST E A; length is\<^sub>1 = length \<tau>s\<^sub>1; length ST < mxs; case Co of None \<Rightarrow> D = Throwable | \<lfloor>C\<rfloor> \<Rightarrow> D = C \<and> is_class P C; length is\<^sub>2 < Suc (length \<tau>s\<^sub>2); pcs xt \<subseteq> {0..<length \<tau>s\<^sub>1 + length is\<^sub>2}; pc < length \<tau>s\<^sub>1 + length is\<^sub>2; \<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt). case x of (pc', \<tau>') \<Rightarrow> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! pc'; (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! pc = \<lfloor>(a, b)\<rfloor>; app\<^sub>i ((is\<^sub>1 @ is\<^sub>2) ! pc, P, pc, mxs, T\<^sub>r, a, b); xcpt_app ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc mxs xt (a, b); \<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt). case x of (pc', \<tau>') \<Rightarrow> pc' < Suc (length \<tau>s\<^sub>1 + length \<tau>s\<^sub>2)\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> (set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) [(0, length \<tau>s\<^sub>1 - Suc n, Co, length \<tau>s\<^sub>1, length ST)])). case x of (pc', \<tau>') \<Rightarrow> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! pc'
[PROOF STEP]
apply(clarsimp split del: option.split_asm)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>pc a b aa ba. \<lbrakk>\<forall>\<tau>\<in>set \<tau>s\<^sub>1. \<forall>ST' LT'. \<tau> = \<lfloor>(ST', LT')\<rfloor> \<longrightarrow> length ST \<le> length ST' \<and> P \<turnstile> \<lfloor>(drop (length ST' - length ST) ST', LT')\<rfloor> \<le>' ty\<^sub>i' ST E A; length is\<^sub>1 = length \<tau>s\<^sub>1; length ST < mxs; case Co of None \<Rightarrow> D = Throwable | \<lfloor>C\<rfloor> \<Rightarrow> D = C \<and> is_class P C; length is\<^sub>2 < Suc (length \<tau>s\<^sub>2); pcs xt \<subseteq> {0..<length \<tau>s\<^sub>1 + length is\<^sub>2}; pc < length \<tau>s\<^sub>1 + length is\<^sub>2; \<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt). case x of (pc', \<tau>') \<Rightarrow> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! pc'; (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! pc = \<lfloor>(a, b)\<rfloor>; app\<^sub>i ((is\<^sub>1 @ is\<^sub>2) ! pc, P, pc, mxs, T\<^sub>r, a, b); xcpt_app ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc mxs xt (a, b); \<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt). case x of (pc', \<tau>') \<Rightarrow> pc' < Suc (length \<tau>s\<^sub>1 + length \<tau>s\<^sub>2); (aa, ba) \<in> set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<or> (aa, ba) \<in> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt) \<or> (aa, ba) \<in> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) [(0, length \<tau>s\<^sub>1 - Suc n, Co, length \<tau>s\<^sub>1, length ST)])\<rbrakk> \<Longrightarrow> aa < Suc (length \<tau>s\<^sub>1 + length \<tau>s\<^sub>2)
 2. \<And>pc a b. \<lbrakk>\<forall>\<tau>\<in>set \<tau>s\<^sub>1. \<forall>ST' LT'. \<tau> = \<lfloor>(ST', LT')\<rfloor> \<longrightarrow> length ST \<le> length ST' \<and> P \<turnstile> \<lfloor>(drop (length ST' - length ST) ST', LT')\<rfloor> \<le>' ty\<^sub>i' ST E A; length is\<^sub>1 = length \<tau>s\<^sub>1; length ST < mxs; case Co of None \<Rightarrow> D = Throwable | \<lfloor>C\<rfloor> \<Rightarrow> D = C \<and> is_class P C; length is\<^sub>2 < Suc (length \<tau>s\<^sub>2); pcs xt \<subseteq> {0..<length \<tau>s\<^sub>1 + length is\<^sub>2}; pc < length \<tau>s\<^sub>1 + length is\<^sub>2; \<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt). case x of (pc', \<tau>') \<Rightarrow> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! pc'; (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! pc = \<lfloor>(a, b)\<rfloor>; app\<^sub>i ((is\<^sub>1 @ is\<^sub>2) ! pc, P, pc, mxs, T\<^sub>r, a, b); xcpt_app ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc mxs xt (a, b); \<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt). case x of (pc', \<tau>') \<Rightarrow> pc' < Suc (length \<tau>s\<^sub>1 + length \<tau>s\<^sub>2)\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> (set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) [(0, length \<tau>s\<^sub>1 - Suc n, Co, length \<tau>s\<^sub>1, length ST)])). case x of (pc', \<tau>') \<Rightarrow> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! pc'
[PROOF STEP]
apply (erule disjE, blast)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>pc a b aa ba. \<lbrakk>\<forall>\<tau>\<in>set \<tau>s\<^sub>1. \<forall>ST' LT'. \<tau> = \<lfloor>(ST', LT')\<rfloor> \<longrightarrow> length ST \<le> length ST' \<and> P \<turnstile> \<lfloor>(drop (length ST' - length ST) ST', LT')\<rfloor> \<le>' ty\<^sub>i' ST E A; length is\<^sub>1 = length \<tau>s\<^sub>1; length ST < mxs; case Co of None \<Rightarrow> D = Throwable | \<lfloor>C\<rfloor> \<Rightarrow> D = C \<and> is_class P C; length is\<^sub>2 < Suc (length \<tau>s\<^sub>2); pcs xt \<subseteq> {0..<length \<tau>s\<^sub>1 + length is\<^sub>2}; pc < length \<tau>s\<^sub>1 + length is\<^sub>2; \<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt). case x of (pc', \<tau>') \<Rightarrow> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! pc'; (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! pc = \<lfloor>(a, b)\<rfloor>; app\<^sub>i ((is\<^sub>1 @ is\<^sub>2) ! pc, P, pc, mxs, T\<^sub>r, a, b); xcpt_app ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc mxs xt (a, b); \<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt). case x of (pc', \<tau>') \<Rightarrow> pc' < Suc (length \<tau>s\<^sub>1 + length \<tau>s\<^sub>2); (aa, ba) \<in> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt) \<or> (aa, ba) \<in> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) [(0, length \<tau>s\<^sub>1 - Suc n, Co, length \<tau>s\<^sub>1, length ST)])\<rbrakk> \<Longrightarrow> aa < Suc (length \<tau>s\<^sub>1 + length \<tau>s\<^sub>2)
 2. \<And>pc a b. \<lbrakk>\<forall>\<tau>\<in>set \<tau>s\<^sub>1. \<forall>ST' LT'. \<tau> = \<lfloor>(ST', LT')\<rfloor> \<longrightarrow> length ST \<le> length ST' \<and> P \<turnstile> \<lfloor>(drop (length ST' - length ST) ST', LT')\<rfloor> \<le>' ty\<^sub>i' ST E A; length is\<^sub>1 = length \<tau>s\<^sub>1; length ST < mxs; case Co of None \<Rightarrow> D = Throwable | \<lfloor>C\<rfloor> \<Rightarrow> D = C \<and> is_class P C; length is\<^sub>2 < Suc (length \<tau>s\<^sub>2); pcs xt \<subseteq> {0..<length \<tau>s\<^sub>1 + length is\<^sub>2}; pc < length \<tau>s\<^sub>1 + length is\<^sub>2; \<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt). case x of (pc', \<tau>') \<Rightarrow> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! pc'; (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! pc = \<lfloor>(a, b)\<rfloor>; app\<^sub>i ((is\<^sub>1 @ is\<^sub>2) ! pc, P, pc, mxs, T\<^sub>r, a, b); xcpt_app ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc mxs xt (a, b); \<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt). case x of (pc', \<tau>') \<Rightarrow> pc' < Suc (length \<tau>s\<^sub>1 + length \<tau>s\<^sub>2)\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> (set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) [(0, length \<tau>s\<^sub>1 - Suc n, Co, length \<tau>s\<^sub>1, length ST)])). case x of (pc', \<tau>') \<Rightarrow> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! pc'
[PROOF STEP]
apply (erule disjE, blast)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>pc a b aa ba. \<lbrakk>\<forall>\<tau>\<in>set \<tau>s\<^sub>1. \<forall>ST' LT'. \<tau> = \<lfloor>(ST', LT')\<rfloor> \<longrightarrow> length ST \<le> length ST' \<and> P \<turnstile> \<lfloor>(drop (length ST' - length ST) ST', LT')\<rfloor> \<le>' ty\<^sub>i' ST E A; length is\<^sub>1 = length \<tau>s\<^sub>1; length ST < mxs; case Co of None \<Rightarrow> D = Throwable | \<lfloor>C\<rfloor> \<Rightarrow> D = C \<and> is_class P C; length is\<^sub>2 < Suc (length \<tau>s\<^sub>2); pcs xt \<subseteq> {0..<length \<tau>s\<^sub>1 + length is\<^sub>2}; pc < length \<tau>s\<^sub>1 + length is\<^sub>2; \<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt). case x of (pc', \<tau>') \<Rightarrow> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! pc'; (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! pc = \<lfloor>(a, b)\<rfloor>; app\<^sub>i ((is\<^sub>1 @ is\<^sub>2) ! pc, P, pc, mxs, T\<^sub>r, a, b); xcpt_app ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc mxs xt (a, b); \<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt). case x of (pc', \<tau>') \<Rightarrow> pc' < Suc (length \<tau>s\<^sub>1 + length \<tau>s\<^sub>2); (aa, ba) \<in> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) [(0, length \<tau>s\<^sub>1 - Suc n, Co, length \<tau>s\<^sub>1, length ST)])\<rbrakk> \<Longrightarrow> aa < Suc (length \<tau>s\<^sub>1 + length \<tau>s\<^sub>2)
 2. \<And>pc a b. \<lbrakk>\<forall>\<tau>\<in>set \<tau>s\<^sub>1. \<forall>ST' LT'. \<tau> = \<lfloor>(ST', LT')\<rfloor> \<longrightarrow> length ST \<le> length ST' \<and> P \<turnstile> \<lfloor>(drop (length ST' - length ST) ST', LT')\<rfloor> \<le>' ty\<^sub>i' ST E A; length is\<^sub>1 = length \<tau>s\<^sub>1; length ST < mxs; case Co of None \<Rightarrow> D = Throwable | \<lfloor>C\<rfloor> \<Rightarrow> D = C \<and> is_class P C; length is\<^sub>2 < Suc (length \<tau>s\<^sub>2); pcs xt \<subseteq> {0..<length \<tau>s\<^sub>1 + length is\<^sub>2}; pc < length \<tau>s\<^sub>1 + length is\<^sub>2; \<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt). case x of (pc', \<tau>') \<Rightarrow> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! pc'; (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! pc = \<lfloor>(a, b)\<rfloor>; app\<^sub>i ((is\<^sub>1 @ is\<^sub>2) ! pc, P, pc, mxs, T\<^sub>r, a, b); xcpt_app ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc mxs xt (a, b); \<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt). case x of (pc', \<tau>') \<Rightarrow> pc' < Suc (length \<tau>s\<^sub>1 + length \<tau>s\<^sub>2)\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> (set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) [(0, length \<tau>s\<^sub>1 - Suc n, Co, length \<tau>s\<^sub>1, length ST)])). case x of (pc', \<tau>') \<Rightarrow> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! pc'
[PROOF STEP]
apply (clarsimp simp add: xcpt_eff_def relevant_entries_def split: if_split_asm)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>pc a b. \<lbrakk>\<forall>\<tau>\<in>set \<tau>s\<^sub>1. \<forall>ST' LT'. \<tau> = \<lfloor>(ST', LT')\<rfloor> \<longrightarrow> length ST \<le> length ST' \<and> P \<turnstile> \<lfloor>(drop (length ST' - length ST) ST', LT')\<rfloor> \<le>' ty\<^sub>i' ST E A; length is\<^sub>1 = length \<tau>s\<^sub>1; length ST < mxs; case Co of None \<Rightarrow> D = Throwable | \<lfloor>C\<rfloor> \<Rightarrow> D = C \<and> is_class P C; length is\<^sub>2 < Suc (length \<tau>s\<^sub>2); pcs xt \<subseteq> {0..<length \<tau>s\<^sub>1 + length is\<^sub>2}; pc < length \<tau>s\<^sub>1 + length is\<^sub>2; \<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt). case x of (pc', \<tau>') \<Rightarrow> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! pc'; (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! pc = \<lfloor>(a, b)\<rfloor>; app\<^sub>i ((is\<^sub>1 @ is\<^sub>2) ! pc, P, pc, mxs, T\<^sub>r, a, b); xcpt_app ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc mxs xt (a, b); \<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt). case x of (pc', \<tau>') \<Rightarrow> pc' < Suc (length \<tau>s\<^sub>1 + length \<tau>s\<^sub>2)\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> (set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) [(0, length \<tau>s\<^sub>1 - Suc n, Co, length \<tau>s\<^sub>1, length ST)])). case x of (pc', \<tau>') \<Rightarrow> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! pc'
[PROOF STEP]
apply(clarsimp split del: option.split_asm)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>pc a b aa ba. \<lbrakk>\<forall>\<tau>\<in>set \<tau>s\<^sub>1. \<forall>ST' LT'. \<tau> = \<lfloor>(ST', LT')\<rfloor> \<longrightarrow> length ST \<le> length ST' \<and> P \<turnstile> \<lfloor>(drop (length ST' - length ST) ST', LT')\<rfloor> \<le>' ty\<^sub>i' ST E A; length is\<^sub>1 = length \<tau>s\<^sub>1; length ST < mxs; case Co of None \<Rightarrow> D = Throwable | \<lfloor>C\<rfloor> \<Rightarrow> D = C \<and> is_class P C; length is\<^sub>2 < Suc (length \<tau>s\<^sub>2); pcs xt \<subseteq> {0..<length \<tau>s\<^sub>1 + length is\<^sub>2}; pc < length \<tau>s\<^sub>1 + length is\<^sub>2; \<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt). case x of (pc', \<tau>') \<Rightarrow> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! pc'; (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! pc = \<lfloor>(a, b)\<rfloor>; app\<^sub>i ((is\<^sub>1 @ is\<^sub>2) ! pc, P, pc, mxs, T\<^sub>r, a, b); xcpt_app ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc mxs xt (a, b); \<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt). case x of (pc', \<tau>') \<Rightarrow> pc' < Suc (length \<tau>s\<^sub>1 + length \<tau>s\<^sub>2); (aa, ba) \<in> set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<or> (aa, ba) \<in> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt) \<or> (aa, ba) \<in> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) [(0, length \<tau>s\<^sub>1 - Suc n, Co, length \<tau>s\<^sub>1, length ST)])\<rbrakk> \<Longrightarrow> P \<turnstile> ba \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! aa
[PROOF STEP]
apply (erule disjE, blast)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>pc a b aa ba. \<lbrakk>\<forall>\<tau>\<in>set \<tau>s\<^sub>1. \<forall>ST' LT'. \<tau> = \<lfloor>(ST', LT')\<rfloor> \<longrightarrow> length ST \<le> length ST' \<and> P \<turnstile> \<lfloor>(drop (length ST' - length ST) ST', LT')\<rfloor> \<le>' ty\<^sub>i' ST E A; length is\<^sub>1 = length \<tau>s\<^sub>1; length ST < mxs; case Co of None \<Rightarrow> D = Throwable | \<lfloor>C\<rfloor> \<Rightarrow> D = C \<and> is_class P C; length is\<^sub>2 < Suc (length \<tau>s\<^sub>2); pcs xt \<subseteq> {0..<length \<tau>s\<^sub>1 + length is\<^sub>2}; pc < length \<tau>s\<^sub>1 + length is\<^sub>2; \<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt). case x of (pc', \<tau>') \<Rightarrow> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! pc'; (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! pc = \<lfloor>(a, b)\<rfloor>; app\<^sub>i ((is\<^sub>1 @ is\<^sub>2) ! pc, P, pc, mxs, T\<^sub>r, a, b); xcpt_app ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc mxs xt (a, b); \<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt). case x of (pc', \<tau>') \<Rightarrow> pc' < Suc (length \<tau>s\<^sub>1 + length \<tau>s\<^sub>2); (aa, ba) \<in> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt) \<or> (aa, ba) \<in> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) [(0, length \<tau>s\<^sub>1 - Suc n, Co, length \<tau>s\<^sub>1, length ST)])\<rbrakk> \<Longrightarrow> P \<turnstile> ba \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! aa
[PROOF STEP]
apply (erule disjE, blast)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>pc a b aa ba. \<lbrakk>\<forall>\<tau>\<in>set \<tau>s\<^sub>1. \<forall>ST' LT'. \<tau> = \<lfloor>(ST', LT')\<rfloor> \<longrightarrow> length ST \<le> length ST' \<and> P \<turnstile> \<lfloor>(drop (length ST' - length ST) ST', LT')\<rfloor> \<le>' ty\<^sub>i' ST E A; length is\<^sub>1 = length \<tau>s\<^sub>1; length ST < mxs; case Co of None \<Rightarrow> D = Throwable | \<lfloor>C\<rfloor> \<Rightarrow> D = C \<and> is_class P C; length is\<^sub>2 < Suc (length \<tau>s\<^sub>2); pcs xt \<subseteq> {0..<length \<tau>s\<^sub>1 + length is\<^sub>2}; pc < length \<tau>s\<^sub>1 + length is\<^sub>2; \<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt). case x of (pc', \<tau>') \<Rightarrow> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! pc'; (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! pc = \<lfloor>(a, b)\<rfloor>; app\<^sub>i ((is\<^sub>1 @ is\<^sub>2) ! pc, P, pc, mxs, T\<^sub>r, a, b); xcpt_app ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc mxs xt (a, b); \<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) xt). case x of (pc', \<tau>') \<Rightarrow> pc' < Suc (length \<tau>s\<^sub>1 + length \<tau>s\<^sub>2); (aa, ba) \<in> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b) [(0, length \<tau>s\<^sub>1 - Suc n, Co, length \<tau>s\<^sub>1, length ST)])\<rbrakk> \<Longrightarrow> P \<turnstile> ba \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! aa
[PROOF STEP]
apply (clarsimp simp add: xcpt_eff_def relevant_entries_def split: if_split_asm split del: option.split_asm)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>pc a b. \<lbrakk>\<forall>\<tau>\<in>set \<tau>s\<^sub>1. \<forall>ST' LT'. \<tau> = \<lfloor>(ST', LT')\<rfloor> \<longrightarrow> length ST \<le> length ST' \<and> P \<turnstile> \<lfloor>(drop (length ST' - length ST) ST', LT')\<rfloor> \<le>' ty\<^sub>i' ST E A; length is\<^sub>1 = length \<tau>s\<^sub>1; length ST < mxs; case Co of None \<Rightarrow> D = Throwable | \<lfloor>C\<rfloor> \<Rightarrow> D = C \<and> is_class P C; length is\<^sub>2 < Suc (length \<tau>s\<^sub>2); pcs xt \<subseteq> {0..<length \<tau>s\<^sub>1 + length is\<^sub>2}; pc < length \<tau>s\<^sub>1 + length is\<^sub>2; \<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> (\<lambda>x. case x of (f, t, C, h, d) \<Rightarrow> (h, \<lfloor>((case C of None \<Rightarrow> Class Throwable | \<lfloor>x\<rfloor> \<Rightarrow> Class x) # drop (length a - d) a, b)\<rfloor>)) ` {x \<in> set xt. is_relevant_entry P ((is\<^sub>1 @ is\<^sub>2) ! pc) pc x}. case x of (pc', \<tau>') \<Rightarrow> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! pc'; (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! pc = \<lfloor>(a, b)\<rfloor>; app\<^sub>i ((is\<^sub>1 @ is\<^sub>2) ! pc, P, pc, mxs, T\<^sub>r, a, b); xcpt_app ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc mxs xt (a, b); \<forall>x\<in>set (norm_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (a, b)) \<union> (\<lambda>x. case x of (f, t, C, h, d) \<Rightarrow> (h, \<lfloor>((case C of None \<Rightarrow> Class Throwable | \<lfloor>x\<rfloor> \<Rightarrow> Class x) # drop (length a - d) a, b)\<rfloor>)) ` {x \<in> set xt. is_relevant_entry P ((is\<^sub>1 @ is\<^sub>2) ! pc) pc x}. case x of (pc', \<tau>') \<Rightarrow> pc' < Suc (length \<tau>s\<^sub>1 + length \<tau>s\<^sub>2); is_relevant_entry P ((is\<^sub>1 @ is\<^sub>2) ! pc) pc (0, length \<tau>s\<^sub>1 - Suc n, Co, length \<tau>s\<^sub>1, length ST)\<rbrakk> \<Longrightarrow> (Co = Any \<longrightarrow> P \<turnstile> \<lfloor>(Class Throwable # drop (length a - length ST) a, b)\<rfloor> \<le>' ty\<^sub>i' (Class D # ST) E A) \<and> (\<forall>x2. Co = \<lfloor>x2\<rfloor> \<longrightarrow> P \<turnstile> \<lfloor>(Class x2 # drop (length a - length ST) a, b)\<rfloor> \<le>' ty\<^sub>i' (Class D # ST) E A)
[PROOF STEP]
apply (simp add: nth_append is_relevant_entry_def split: if_split_asm split del: option.split_asm)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>pc a b. \<lbrakk>pc < length \<tau>s\<^sub>1 - Suc n; \<forall>x\<in>set (norm_eff (is\<^sub>1 ! pc) P pc (a, b)) \<union> (\<lambda>x. case x of (f, t, C, h, d) \<Rightarrow> (h, \<lfloor>((case C of None \<Rightarrow> Class Throwable | \<lfloor>x\<rfloor> \<Rightarrow> Class x) # drop (length a - d) a, b)\<rfloor>)) ` {x \<in> set xt. case x of (f, t, C, ab) \<Rightarrow> (case C of None \<Rightarrow> True | \<lfloor>x\<rfloor> \<Rightarrow> is_relevant_class (is\<^sub>1 ! pc) P x) \<and> f \<le> pc \<and> pc < t}. case x of (pc', \<tau>') \<Rightarrow> P \<turnstile> \<tau>' \<le>' (if pc' < length \<tau>s\<^sub>1 then \<tau>s\<^sub>1 ! pc' else (ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! (pc' - length \<tau>s\<^sub>1)); \<tau>s\<^sub>1 ! pc = \<lfloor>(a, b)\<rfloor>; app\<^sub>i (is\<^sub>1 ! pc, P, pc, mxs, T\<^sub>r, a, b); xcpt_app (is\<^sub>1 ! pc) P pc mxs xt (a, b); \<forall>x\<in>set (norm_eff (is\<^sub>1 ! pc) P pc (a, b)) \<union> (\<lambda>x. case x of (f, t, C, h, d) \<Rightarrow> (h, \<lfloor>((case C of None \<Rightarrow> Class Throwable | \<lfloor>x\<rfloor> \<Rightarrow> Class x) # drop (length a - d) a, b)\<rfloor>)) ` {x \<in> set xt. case x of (f, t, C, ab) \<Rightarrow> (case C of None \<Rightarrow> True | \<lfloor>x\<rfloor> \<Rightarrow> is_relevant_class (is\<^sub>1 ! pc) P x) \<and> f \<le> pc \<and> pc < t}. case x of (pc', \<tau>') \<Rightarrow> pc' < Suc (length \<tau>s\<^sub>1 + length \<tau>s\<^sub>2); \<forall>\<tau>\<in>set \<tau>s\<^sub>1. \<forall>ST' LT'. \<tau> = \<lfloor>(ST', LT')\<rfloor> \<longrightarrow> length ST \<le> length ST' \<and> P \<turnstile> \<lfloor>(drop (length ST' - length ST) ST', LT')\<rfloor> \<le>' ty\<^sub>i' ST E A; length is\<^sub>1 = length \<tau>s\<^sub>1; length ST < mxs; case Co of None \<Rightarrow> D = Throwable | \<lfloor>C\<rfloor> \<Rightarrow> D = C \<and> is_class P C; length is\<^sub>2 < Suc (length \<tau>s\<^sub>2); pcs xt \<subseteq> {0..<length \<tau>s\<^sub>1 + length is\<^sub>2}; pc < length \<tau>s\<^sub>1; case Co of None \<Rightarrow> True | \<lfloor>x\<rfloor> \<Rightarrow> is_relevant_class (is\<^sub>1 ! pc) P x\<rbrakk> \<Longrightarrow> (Co = Any \<longrightarrow> P \<turnstile> \<lfloor>(Class Throwable # drop (length a - length ST) a, b)\<rfloor> \<le>' ty\<^sub>i' (Class D # ST) E A) \<and> (\<forall>x2. Co = \<lfloor>x2\<rfloor> \<longrightarrow> P \<turnstile> \<lfloor>(Class x2 # drop (length a - length ST) a, b)\<rfloor> \<le>' ty\<^sub>i' (Class D # ST) E A)
[PROOF STEP]
apply (drule_tac x = "\<tau>s\<^sub>1!pc" in bspec)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>pc a b. \<lbrakk>pc < length \<tau>s\<^sub>1 - Suc n; \<forall>x\<in>set (norm_eff (is\<^sub>1 ! pc) P pc (a, b)) \<union> (\<lambda>x. case x of (f, t, C, h, d) \<Rightarrow> (h, \<lfloor>((case C of None \<Rightarrow> Class Throwable | \<lfloor>x\<rfloor> \<Rightarrow> Class x) # drop (length a - d) a, b)\<rfloor>)) ` {x \<in> set xt. case x of (f, t, C, ab) \<Rightarrow> (case C of None \<Rightarrow> True | \<lfloor>x\<rfloor> \<Rightarrow> is_relevant_class (is\<^sub>1 ! pc) P x) \<and> f \<le> pc \<and> pc < t}. case x of (pc', \<tau>') \<Rightarrow> P \<turnstile> \<tau>' \<le>' (if pc' < length \<tau>s\<^sub>1 then \<tau>s\<^sub>1 ! pc' else (ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! (pc' - length \<tau>s\<^sub>1)); \<tau>s\<^sub>1 ! pc = \<lfloor>(a, b)\<rfloor>; app\<^sub>i (is\<^sub>1 ! pc, P, pc, mxs, T\<^sub>r, a, b); xcpt_app (is\<^sub>1 ! pc) P pc mxs xt (a, b); \<forall>x\<in>set (norm_eff (is\<^sub>1 ! pc) P pc (a, b)) \<union> (\<lambda>x. case x of (f, t, C, h, d) \<Rightarrow> (h, \<lfloor>((case C of None \<Rightarrow> Class Throwable | \<lfloor>x\<rfloor> \<Rightarrow> Class x) # drop (length a - d) a, b)\<rfloor>)) ` {x \<in> set xt. case x of (f, t, C, ab) \<Rightarrow> (case C of None \<Rightarrow> True | \<lfloor>x\<rfloor> \<Rightarrow> is_relevant_class (is\<^sub>1 ! pc) P x) \<and> f \<le> pc \<and> pc < t}. case x of (pc', \<tau>') \<Rightarrow> pc' < Suc (length \<tau>s\<^sub>1 + length \<tau>s\<^sub>2); length is\<^sub>1 = length \<tau>s\<^sub>1; length ST < mxs; case Co of None \<Rightarrow> D = Throwable | \<lfloor>C\<rfloor> \<Rightarrow> D = C \<and> is_class P C; length is\<^sub>2 < Suc (length \<tau>s\<^sub>2); pcs xt \<subseteq> {0..<length \<tau>s\<^sub>1 + length is\<^sub>2}; pc < length \<tau>s\<^sub>1; case Co of None \<Rightarrow> True | \<lfloor>x\<rfloor> \<Rightarrow> is_relevant_class (is\<^sub>1 ! pc) P x\<rbrakk> \<Longrightarrow> \<tau>s\<^sub>1 ! pc \<in> set \<tau>s\<^sub>1
 2. \<And>pc a b. \<lbrakk>pc < length \<tau>s\<^sub>1 - Suc n; \<forall>x\<in>set (norm_eff (is\<^sub>1 ! pc) P pc (a, b)) \<union> (\<lambda>x. case x of (f, t, C, h, d) \<Rightarrow> (h, \<lfloor>((case C of None \<Rightarrow> Class Throwable | \<lfloor>x\<rfloor> \<Rightarrow> Class x) # drop (length a - d) a, b)\<rfloor>)) ` {x \<in> set xt. case x of (f, t, C, ab) \<Rightarrow> (case C of None \<Rightarrow> True | \<lfloor>x\<rfloor> \<Rightarrow> is_relevant_class (is\<^sub>1 ! pc) P x) \<and> f \<le> pc \<and> pc < t}. case x of (pc', \<tau>') \<Rightarrow> P \<turnstile> \<tau>' \<le>' (if pc' < length \<tau>s\<^sub>1 then \<tau>s\<^sub>1 ! pc' else (ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! (pc' - length \<tau>s\<^sub>1)); \<tau>s\<^sub>1 ! pc = \<lfloor>(a, b)\<rfloor>; app\<^sub>i (is\<^sub>1 ! pc, P, pc, mxs, T\<^sub>r, a, b); xcpt_app (is\<^sub>1 ! pc) P pc mxs xt (a, b); \<forall>x\<in>set (norm_eff (is\<^sub>1 ! pc) P pc (a, b)) \<union> (\<lambda>x. case x of (f, t, C, h, d) \<Rightarrow> (h, \<lfloor>((case C of None \<Rightarrow> Class Throwable | \<lfloor>x\<rfloor> \<Rightarrow> Class x) # drop (length a - d) a, b)\<rfloor>)) ` {x \<in> set xt. case x of (f, t, C, ab) \<Rightarrow> (case C of None \<Rightarrow> True | \<lfloor>x\<rfloor> \<Rightarrow> is_relevant_class (is\<^sub>1 ! pc) P x) \<and> f \<le> pc \<and> pc < t}. case x of (pc', \<tau>') \<Rightarrow> pc' < Suc (length \<tau>s\<^sub>1 + length \<tau>s\<^sub>2); length is\<^sub>1 = length \<tau>s\<^sub>1; length ST < mxs; case Co of None \<Rightarrow> D = Throwable | \<lfloor>C\<rfloor> \<Rightarrow> D = C \<and> is_class P C; length is\<^sub>2 < Suc (length \<tau>s\<^sub>2); pcs xt \<subseteq> {0..<length \<tau>s\<^sub>1 + length is\<^sub>2}; pc < length \<tau>s\<^sub>1; case Co of None \<Rightarrow> True | \<lfloor>x\<rfloor> \<Rightarrow> is_relevant_class (is\<^sub>1 ! pc) P x; \<forall>ST' LT'. \<tau>s\<^sub>1 ! pc = \<lfloor>(ST', LT')\<rfloor> \<longrightarrow> length ST \<le> length ST' \<and> P \<turnstile> \<lfloor>(drop (length ST' - length ST) ST', LT')\<rfloor> \<le>' ty\<^sub>i' ST E A\<rbrakk> \<Longrightarrow> (Co = Any \<longrightarrow> P \<turnstile> \<lfloor>(Class Throwable # drop (length a - length ST) a, b)\<rfloor> \<le>' ty\<^sub>i' (Class D # ST) E A) \<and> (\<forall>x2. Co = \<lfloor>x2\<rfloor> \<longrightarrow> P \<turnstile> \<lfloor>(Class x2 # drop (length a - length ST) a, b)\<rfloor> \<le>' ty\<^sub>i' (Class D # ST) E A)
[PROOF STEP]
apply (blast intro: nth_mem)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>pc a b. \<lbrakk>pc < length \<tau>s\<^sub>1 - Suc n; \<forall>x\<in>set (norm_eff (is\<^sub>1 ! pc) P pc (a, b)) \<union> (\<lambda>x. case x of (f, t, C, h, d) \<Rightarrow> (h, \<lfloor>((case C of None \<Rightarrow> Class Throwable | \<lfloor>x\<rfloor> \<Rightarrow> Class x) # drop (length a - d) a, b)\<rfloor>)) ` {x \<in> set xt. case x of (f, t, C, ab) \<Rightarrow> (case C of None \<Rightarrow> True | \<lfloor>x\<rfloor> \<Rightarrow> is_relevant_class (is\<^sub>1 ! pc) P x) \<and> f \<le> pc \<and> pc < t}. case x of (pc', \<tau>') \<Rightarrow> P \<turnstile> \<tau>' \<le>' (if pc' < length \<tau>s\<^sub>1 then \<tau>s\<^sub>1 ! pc' else (ty\<^sub>i' (Class D # ST) E A # \<tau>s\<^sub>2) ! (pc' - length \<tau>s\<^sub>1)); \<tau>s\<^sub>1 ! pc = \<lfloor>(a, b)\<rfloor>; app\<^sub>i (is\<^sub>1 ! pc, P, pc, mxs, T\<^sub>r, a, b); xcpt_app (is\<^sub>1 ! pc) P pc mxs xt (a, b); \<forall>x\<in>set (norm_eff (is\<^sub>1 ! pc) P pc (a, b)) \<union> (\<lambda>x. case x of (f, t, C, h, d) \<Rightarrow> (h, \<lfloor>((case C of None \<Rightarrow> Class Throwable | \<lfloor>x\<rfloor> \<Rightarrow> Class x) # drop (length a - d) a, b)\<rfloor>)) ` {x \<in> set xt. case x of (f, t, C, ab) \<Rightarrow> (case C of None \<Rightarrow> True | \<lfloor>x\<rfloor> \<Rightarrow> is_relevant_class (is\<^sub>1 ! pc) P x) \<and> f \<le> pc \<and> pc < t}. case x of (pc', \<tau>') \<Rightarrow> pc' < Suc (length \<tau>s\<^sub>1 + length \<tau>s\<^sub>2); length is\<^sub>1 = length \<tau>s\<^sub>1; length ST < mxs; case Co of None \<Rightarrow> D = Throwable | \<lfloor>C\<rfloor> \<Rightarrow> D = C \<and> is_class P C; length is\<^sub>2 < Suc (length \<tau>s\<^sub>2); pcs xt \<subseteq> {0..<length \<tau>s\<^sub>1 + length is\<^sub>2}; pc < length \<tau>s\<^sub>1; case Co of None \<Rightarrow> True | \<lfloor>x\<rfloor> \<Rightarrow> is_relevant_class (is\<^sub>1 ! pc) P x; \<forall>ST' LT'. \<tau>s\<^sub>1 ! pc = \<lfloor>(ST', LT')\<rfloor> \<longrightarrow> length ST \<le> length ST' \<and> P \<turnstile> \<lfloor>(drop (length ST' - length ST) ST', LT')\<rfloor> \<le>' ty\<^sub>i' ST E A\<rbrakk> \<Longrightarrow> (Co = Any \<longrightarrow> P \<turnstile> \<lfloor>(Class Throwable # drop (length a - length ST) a, b)\<rfloor> \<le>' ty\<^sub>i' (Class D # ST) E A) \<and> (\<forall>x2. Co = \<lfloor>x2\<rfloor> \<longrightarrow> P \<turnstile> \<lfloor>(Class x2 # drop (length a - length ST) a, b)\<rfloor> \<le>' ty\<^sub>i' (Class D # ST) E A)
[PROOF STEP]
apply (fastforce simp add: ty\<^sub>i'_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma wt_instrs_xapp_Some[trans]:
  "\<lbrakk> \<turnstile> is\<^sub>1 @ is\<^sub>2, xt [::] \<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2;
     \<forall>\<tau> \<in> set \<tau>s\<^sub>1. \<forall>ST' LT'. \<tau> = Some(ST',LT') \<longrightarrow>
      size ST \<le> size ST' \<and> P \<turnstile> Some (drop (size ST' - size ST) ST',LT') \<le>' ty\<^sub>i' ST E A;
     size is\<^sub>1 = size \<tau>s\<^sub>1; is_class P C; size ST < mxs  \<rbrakk> \<Longrightarrow>
  \<turnstile> is\<^sub>1 @ is\<^sub>2, xt @ [(0,size is\<^sub>1 - Suc n,Some C,size is\<^sub>1,size ST)] [::] \<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<turnstile> is\<^sub>1 @ is\<^sub>2, xt [::] \<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2; \<forall>\<tau>\<in>set \<tau>s\<^sub>1. \<forall>ST' LT'. \<tau> = \<lfloor>(ST', LT')\<rfloor> \<longrightarrow> length ST \<le> length ST' \<and> P \<turnstile> \<lfloor>(drop (length ST' - length ST) ST', LT')\<rfloor> \<le>' ty\<^sub>i' ST E A; length is\<^sub>1 = length \<tau>s\<^sub>1; is_class P C; length ST < mxs\<rbrakk> \<Longrightarrow> \<turnstile> is\<^sub>1 @ is\<^sub>2, xt @ [(0, length is\<^sub>1 - Suc n, \<lfloor>C\<rfloor>, length is\<^sub>1, length ST)] [::] \<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2
[PROOF STEP]
by(erule (3) wt_instrs_xapp) simp


[STATEMENT]
lemma wt_instrs_xapp_Any:
  "\<lbrakk> \<turnstile> is\<^sub>1 @ is\<^sub>2, xt [::] \<tau>s\<^sub>1 @ ty\<^sub>i' (Class Throwable # ST) E A # \<tau>s\<^sub>2;
     \<forall>\<tau> \<in> set \<tau>s\<^sub>1. \<forall>ST' LT'. \<tau> = Some(ST',LT') \<longrightarrow>
      size ST \<le> size ST' \<and> P \<turnstile> Some (drop (size ST' - size ST) ST',LT') \<le>' ty\<^sub>i' ST E A;
     size is\<^sub>1 = size \<tau>s\<^sub>1; size ST < mxs \<rbrakk> \<Longrightarrow>
  \<turnstile> is\<^sub>1 @ is\<^sub>2, xt @ [(0,size is\<^sub>1 - Suc n,None,size is\<^sub>1,size ST)] [::] \<tau>s\<^sub>1 @ ty\<^sub>i' (Class Throwable # ST) E A # \<tau>s\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<turnstile> is\<^sub>1 @ is\<^sub>2, xt [::] \<tau>s\<^sub>1 @ ty\<^sub>i' (Class Throwable # ST) E A # \<tau>s\<^sub>2; \<forall>\<tau>\<in>set \<tau>s\<^sub>1. \<forall>ST' LT'. \<tau> = \<lfloor>(ST', LT')\<rfloor> \<longrightarrow> length ST \<le> length ST' \<and> P \<turnstile> \<lfloor>(drop (length ST' - length ST) ST', LT')\<rfloor> \<le>' ty\<^sub>i' ST E A; length is\<^sub>1 = length \<tau>s\<^sub>1; length ST < mxs\<rbrakk> \<Longrightarrow> \<turnstile> is\<^sub>1 @ is\<^sub>2, xt @ [(0, length is\<^sub>1 - Suc n, Any, length is\<^sub>1, length ST)] [::] \<tau>s\<^sub>1 @ ty\<^sub>i' (Class Throwable # ST) E A # \<tau>s\<^sub>2
[PROOF STEP]
by(erule (3) wt_instrs_xapp) simp


[STATEMENT]
lemma drop_Cons_Suc:
  "\<And>xs. drop n xs = y#ys \<Longrightarrow> drop (Suc n) xs = ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs. drop n xs = y # ys \<Longrightarrow> drop (Suc n) xs = ys
[PROOF STEP]
apply (induct n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xs. drop 0 xs = y # ys \<Longrightarrow> drop (Suc 0) xs = ys
 2. \<And>n xs. \<lbrakk>\<And>xs. drop n xs = y # ys \<Longrightarrow> drop (Suc n) xs = ys; drop (Suc n) xs = y # ys\<rbrakk> \<Longrightarrow> drop (Suc (Suc n)) xs = ys
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n xs. \<lbrakk>\<And>xs. drop n xs = y # ys \<Longrightarrow> drop (Suc n) xs = ys; drop (Suc n) xs = y # ys\<rbrakk> \<Longrightarrow> drop (Suc (Suc n)) xs = ys
[PROOF STEP]
apply (simp add: drop_Suc)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma drop_mess:
  "\<lbrakk>Suc (length xs\<^sub>0) \<le> length xs; drop (length xs - Suc (length xs\<^sub>0)) xs = x # xs\<^sub>0\<rbrakk>
  \<Longrightarrow> drop (length xs - length xs\<^sub>0) xs = xs\<^sub>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Suc (length xs\<^sub>0) \<le> length xs; drop (length xs - Suc (length xs\<^sub>0)) xs = x # xs\<^sub>0\<rbrakk> \<Longrightarrow> drop (length xs - length xs\<^sub>0) xs = xs\<^sub>0
[PROOF STEP]
apply (cases xs)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Suc (length xs\<^sub>0) \<le> length xs; drop (length xs - Suc (length xs\<^sub>0)) xs = x # xs\<^sub>0; xs = []\<rbrakk> \<Longrightarrow> drop (length xs - length xs\<^sub>0) xs = xs\<^sub>0
 2. \<And>a list. \<lbrakk>Suc (length xs\<^sub>0) \<le> length xs; drop (length xs - Suc (length xs\<^sub>0)) xs = x # xs\<^sub>0; xs = a # list\<rbrakk> \<Longrightarrow> drop (length xs - length xs\<^sub>0) xs = xs\<^sub>0
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>Suc (length xs\<^sub>0) \<le> length xs; drop (length xs - Suc (length xs\<^sub>0)) xs = x # xs\<^sub>0; xs = a # list\<rbrakk> \<Longrightarrow> drop (length xs - length xs\<^sub>0) xs = xs\<^sub>0
[PROOF STEP]
apply (simp add: Suc_diff_le)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>length xs\<^sub>0 \<le> length list; drop (length list - length xs\<^sub>0) (a # list) = x # xs\<^sub>0; xs = a # list\<rbrakk> \<Longrightarrow> drop (length list - length xs\<^sub>0) list = xs\<^sub>0
[PROOF STEP]
apply (case_tac "length list - length xs\<^sub>0")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a list. \<lbrakk>length xs\<^sub>0 \<le> length list; drop (length list - length xs\<^sub>0) (a # list) = x # xs\<^sub>0; xs = a # list; length list - length xs\<^sub>0 = 0\<rbrakk> \<Longrightarrow> drop (length list - length xs\<^sub>0) list = xs\<^sub>0
 2. \<And>a list nat. \<lbrakk>length xs\<^sub>0 \<le> length list; drop (length list - length xs\<^sub>0) (a # list) = x # xs\<^sub>0; xs = a # list; length list - length xs\<^sub>0 = Suc nat\<rbrakk> \<Longrightarrow> drop (length list - length xs\<^sub>0) list = xs\<^sub>0
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a list nat. \<lbrakk>length xs\<^sub>0 \<le> length list; drop (length list - length xs\<^sub>0) (a # list) = x # xs\<^sub>0; xs = a # list; length list - length xs\<^sub>0 = Suc nat\<rbrakk> \<Longrightarrow> drop (length list - length xs\<^sub>0) list = xs\<^sub>0
[PROOF STEP]
apply (simp add: drop_Cons_Suc)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma drop_mess2:
  assumes len: "Suc (Suc (length xs0)) \<le> length xs"
  and drop: "drop (length xs - Suc (Suc (length xs0))) xs = x1 # x2 # xs0"
  shows "drop (length xs - length xs0) xs = xs0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. drop (length xs - length xs0) xs = xs0
[PROOF STEP]
proof(cases xs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. xs = [] \<Longrightarrow> drop (length xs - length xs0) xs = xs0
 2. \<And>a list. xs = a # list \<Longrightarrow> drop (length xs - length xs0) xs = xs0
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
xs = []

goal (2 subgoals):
 1. xs = [] \<Longrightarrow> drop (length xs - length xs0) xs = xs0
 2. \<And>a list. xs = a # list \<Longrightarrow> drop (length xs - length xs0) xs = xs0
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
Suc (Suc (length xs0)) \<le> length xs
drop (length xs - Suc (Suc (length xs0))) xs = x1 # x2 # xs0
xs = []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Suc (Suc (length xs0)) \<le> length xs
drop (length xs - Suc (Suc (length xs0))) xs = x1 # x2 # xs0
xs = []

goal (1 subgoal):
 1. drop (length xs - length xs0) xs = xs0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
drop (length xs - length xs0) xs = xs0

goal (1 subgoal):
 1. \<And>a list. xs = a # list \<Longrightarrow> drop (length xs - length xs0) xs = xs0
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. xs = a # list \<Longrightarrow> drop (length xs - length xs0) xs = xs0
[PROOF STEP]
case (Cons x xs')
[PROOF STATE]
proof (state)
this:
xs = x # xs'

goal (1 subgoal):
 1. \<And>a list. xs = a # list \<Longrightarrow> drop (length xs - length xs0) xs = xs0
[PROOF STEP]
note Cons[simp]
[PROOF STATE]
proof (state)
this:
xs = x # xs'

goal (1 subgoal):
 1. \<And>a list. xs = a # list \<Longrightarrow> drop (length xs - length xs0) xs = xs0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. drop (length xs - length xs0) xs = xs0
[PROOF STEP]
proof(cases xs')
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. xs' = [] \<Longrightarrow> drop (length xs - length xs0) xs = xs0
 2. \<And>a list. xs' = a # list \<Longrightarrow> drop (length xs - length xs0) xs = xs0
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
xs' = []

goal (2 subgoals):
 1. xs' = [] \<Longrightarrow> drop (length xs - length xs0) xs = xs0
 2. \<And>a list. xs' = a # list \<Longrightarrow> drop (length xs - length xs0) xs = xs0
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
Suc (Suc (length xs0)) \<le> length xs
drop (length xs - Suc (Suc (length xs0))) xs = x1 # x2 # xs0
xs' = []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Suc (Suc (length xs0)) \<le> length xs
drop (length xs - Suc (Suc (length xs0))) xs = x1 # x2 # xs0
xs' = []

goal (1 subgoal):
 1. drop (length xs - length xs0) xs = xs0
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
drop (length xs - length xs0) xs = xs0

goal (1 subgoal):
 1. \<And>a list. xs' = a # list \<Longrightarrow> drop (length xs - length xs0) xs = xs0
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. xs' = a # list \<Longrightarrow> drop (length xs - length xs0) xs = xs0
[PROOF STEP]
case (Cons x' xs'')
[PROOF STATE]
proof (state)
this:
xs' = x' # xs''

goal (1 subgoal):
 1. \<And>a list. xs' = a # list \<Longrightarrow> drop (length xs - length xs0) xs = xs0
[PROOF STEP]
note Cons[simp]
[PROOF STATE]
proof (state)
this:
xs' = x' # xs''

goal (1 subgoal):
 1. \<And>a list. xs' = a # list \<Longrightarrow> drop (length xs - length xs0) xs = xs0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. drop (length xs - length xs0) xs = xs0
[PROOF STEP]
proof(rule drop_mess)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Suc (length xs0) \<le> length xs
 2. drop (length xs - Suc (length xs0)) xs = ?x # xs0
[PROOF STEP]
from len
[PROOF STATE]
proof (chain)
picking this:
Suc (Suc (length xs0)) \<le> length xs
[PROOF STEP]
show "Suc (length xs0) \<le> length xs"
[PROOF STATE]
proof (prove)
using this:
Suc (Suc (length xs0)) \<le> length xs

goal (1 subgoal):
 1. Suc (length xs0) \<le> length xs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Suc (length xs0) \<le> length xs

goal (1 subgoal):
 1. drop (length xs - Suc (length xs0)) xs = ?x # xs0
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. drop (length xs - Suc (length xs0)) xs = ?x # xs0
[PROOF STEP]
have "drop (length xs - length (x2 # xs0)) xs = x2 # xs0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. drop (length xs - length (x2 # xs0)) xs = x2 # xs0
[PROOF STEP]
proof(rule drop_mess)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Suc (length (x2 # xs0)) \<le> length xs
 2. drop (length xs - Suc (length (x2 # xs0))) xs = ?x # x2 # xs0
[PROOF STEP]
from len
[PROOF STATE]
proof (chain)
picking this:
Suc (Suc (length xs0)) \<le> length xs
[PROOF STEP]
show "Suc (length (x2 # xs0)) \<le> length xs"
[PROOF STATE]
proof (prove)
using this:
Suc (Suc (length xs0)) \<le> length xs

goal (1 subgoal):
 1. Suc (length (x2 # xs0)) \<le> length xs
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
Suc (length (x2 # xs0)) \<le> length xs

goal (1 subgoal):
 1. drop (length xs - Suc (length (x2 # xs0))) xs = ?x # x2 # xs0
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. drop (length xs - Suc (length (x2 # xs0))) xs = ?x # x2 # xs0
[PROOF STEP]
from drop
[PROOF STATE]
proof (chain)
picking this:
drop (length xs - Suc (Suc (length xs0))) xs = x1 # x2 # xs0
[PROOF STEP]
show "drop (length xs - Suc (length (x2 # xs0))) xs = x1 # x2 # xs0"
[PROOF STATE]
proof (prove)
using this:
drop (length xs - Suc (Suc (length xs0))) xs = x1 # x2 # xs0

goal (1 subgoal):
 1. drop (length xs - Suc (length (x2 # xs0))) xs = x1 # x2 # xs0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
drop (length xs - Suc (length (x2 # xs0))) xs = x1 # x2 # xs0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
drop (length xs - length (x2 # xs0)) xs = x2 # xs0

goal (1 subgoal):
 1. drop (length xs - Suc (length xs0)) xs = ?x # xs0
[PROOF STEP]
thus "drop (length xs - Suc (length xs0)) xs = x2 # xs0"
[PROOF STATE]
proof (prove)
using this:
drop (length xs - length (x2 # xs0)) xs = x2 # xs0

goal (1 subgoal):
 1. drop (length xs - Suc (length xs0)) xs = x2 # xs0
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
drop (length xs - Suc (length xs0)) xs = x2 # xs0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
drop (length xs - length xs0) xs = xs0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
drop (length xs - length xs0) xs = xs0

goal:
No subgoals!
[PROOF STEP]
qed