[STATEMENT]
lemma (in TC2) wt_instrs_xapp[trans]:
assumes wtis: "\<turnstile> is\<^sub>1 @ is\<^sub>2, xt [::] \<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2"
  and P_\<tau>s\<^sub>1: "\<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"
  and is_\<tau>s: "size is\<^sub>1 = size \<tau>s\<^sub>1" and PC: "is_class P C" and ST_mxs: "size ST < mxs"
shows "\<turnstile> is\<^sub>1 @ is\<^sub>2, xt @ [(0,size is\<^sub>1 - 1,C,size is\<^sub>1,size ST)] [::] \<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2"
(*<*)(is "\<turnstile> ?is, xt@[?xte] [::] ?\<tau>s" is "\<turnstile> ?is, ?xt' [::] ?\<tau>s")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> is\<^sub>1 @ is\<^sub>2, xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)] [::] \<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<turnstile> is\<^sub>1 @ is\<^sub>2, xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)] [::] \<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2
[PROOF STEP]
have P_\<tau>s\<^sub>1': "\<And>\<tau>. \<tau> \<in> set \<tau>s\<^sub>1 \<Longrightarrow> (\<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)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<tau>. \<tau> \<in> set \<tau>s\<^sub>1 \<Longrightarrow> \<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
[PROOF STEP]
using P_\<tau>s\<^sub>1
[PROOF STATE]
proof (prove)
using this:
\<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

goal (1 subgoal):
 1. \<And>\<tau>. \<tau> \<in> set \<tau>s\<^sub>1 \<Longrightarrow> \<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
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
?\<tau>2 \<in> set \<tau>s\<^sub>1 \<Longrightarrow> \<forall>ST' LT'. ?\<tau>2 = \<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

goal (1 subgoal):
 1. \<turnstile> is\<^sub>1 @ is\<^sub>2, xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)] [::] \<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2
[PROOF STEP]
have "size ?is < size ?\<tau>s" and "pcs ?xt' \<subseteq> {0..<size ?is}"
    and P_pc: "\<And>pc. pc< size ?is \<Longrightarrow> P,T\<^sub>r,mxs,size ?\<tau>s,xt \<turnstile> ?is!pc,pc :: ?\<tau>s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (is\<^sub>1 @ is\<^sub>2) < length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) &&& pcs (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) \<subseteq> {0..<length (is\<^sub>1 @ is\<^sub>2)} &&& (\<And>pc. pc < length (is\<^sub>1 @ is\<^sub>2) \<Longrightarrow> P,T\<^sub>r,mxs,length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2),xt \<turnstile> (is\<^sub>1 @ is\<^sub>2) ! pc,pc :: \<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2)
[PROOF STEP]
using wtis
[PROOF STATE]
proof (prove)
using this:
\<turnstile> is\<^sub>1 @ is\<^sub>2, xt [::] \<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2

goal (1 subgoal):
 1. length (is\<^sub>1 @ is\<^sub>2) < length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) &&& pcs (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) \<subseteq> {0..<length (is\<^sub>1 @ is\<^sub>2)} &&& (\<And>pc. pc < length (is\<^sub>1 @ is\<^sub>2) \<Longrightarrow> P,T\<^sub>r,mxs,length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2),xt \<turnstile> (is\<^sub>1 @ is\<^sub>2) ! pc,pc :: \<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2)
[PROOF STEP]
by(simp_all add:wt_instrs_def)
[PROOF STATE]
proof (state)
this:
length (is\<^sub>1 @ is\<^sub>2) < length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2)
pcs (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) \<subseteq> {0..<length (is\<^sub>1 @ is\<^sub>2)}
?pc2 < length (is\<^sub>1 @ is\<^sub>2) \<Longrightarrow> P,T\<^sub>r,mxs,length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2),xt \<turnstile> (is\<^sub>1 @ is\<^sub>2) ! ?pc2,?pc2 :: \<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2

goal (1 subgoal):
 1. \<turnstile> is\<^sub>1 @ is\<^sub>2, xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)] [::] \<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
length (is\<^sub>1 @ is\<^sub>2) < length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2)
pcs (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) \<subseteq> {0..<length (is\<^sub>1 @ is\<^sub>2)}
?pc2 < length (is\<^sub>1 @ is\<^sub>2) \<Longrightarrow> P,T\<^sub>r,mxs,length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2),xt \<turnstile> (is\<^sub>1 @ is\<^sub>2) ! ?pc2,?pc2 :: \<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2

goal (1 subgoal):
 1. \<turnstile> is\<^sub>1 @ is\<^sub>2, xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)] [::] \<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
length (is\<^sub>1 @ is\<^sub>2) < length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2)
pcs (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) \<subseteq> {0..<length (is\<^sub>1 @ is\<^sub>2)}
?pc2 < length (is\<^sub>1 @ is\<^sub>2) \<Longrightarrow> P,T\<^sub>r,mxs,length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2),xt \<turnstile> (is\<^sub>1 @ is\<^sub>2) ! ?pc2,?pc2 :: \<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2

goal (1 subgoal):
 1. \<turnstile> is\<^sub>1 @ is\<^sub>2, xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)] [::] \<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2
[PROOF STEP]
fix pc
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<turnstile> is\<^sub>1 @ is\<^sub>2, xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)] [::] \<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2
[PROOF STEP]
let ?mpc = "size ?\<tau>s" and ?i = "?is!pc" and ?t = "?\<tau>s!pc"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<turnstile> is\<^sub>1 @ is\<^sub>2, xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)] [::] \<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2
[PROOF STEP]
assume "pc< size ?is"
[PROOF STATE]
proof (state)
this:
pc < length (is\<^sub>1 @ is\<^sub>2)

goal (1 subgoal):
 1. \<turnstile> is\<^sub>1 @ is\<^sub>2, xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)] [::] \<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pc < length (is\<^sub>1 @ is\<^sub>2)
[PROOF STEP]
have wti: "P,T\<^sub>r,mxs,?mpc,xt \<turnstile> ?i,pc :: ?\<tau>s"
[PROOF STATE]
proof (prove)
using this:
pc < length (is\<^sub>1 @ is\<^sub>2)

goal (1 subgoal):
 1. P,T\<^sub>r,mxs,length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2),xt \<turnstile> (is\<^sub>1 @ is\<^sub>2) ! pc,pc :: \<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2
[PROOF STEP]
by(rule P_pc)
[PROOF STATE]
proof (state)
this:
P,T\<^sub>r,mxs,length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2),xt \<turnstile> (is\<^sub>1 @ is\<^sub>2) ! pc,pc :: \<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2

goal (1 subgoal):
 1. \<turnstile> is\<^sub>1 @ is\<^sub>2, xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)] [::] \<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
P,T\<^sub>r,mxs,length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2),xt \<turnstile> (is\<^sub>1 @ is\<^sub>2) ! pc,pc :: \<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2
[PROOF STEP]
have app: "app ?i P mxs T\<^sub>r pc ?mpc xt ?t"
       and eff_ss: "\<And>pc' \<tau>'. (pc',\<tau>') \<in> set (eff ?i P pc xt (?\<tau>s!pc))
                           \<Longrightarrow> P \<turnstile> \<tau>' \<le>' ?\<tau>s!pc'"
[PROOF STATE]
proof (prove)
using this:
P,T\<^sub>r,mxs,length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2),xt \<turnstile> (is\<^sub>1 @ is\<^sub>2) ! pc,pc :: \<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2

goal (1 subgoal):
 1. app ((is\<^sub>1 @ is\<^sub>2) ! pc) P mxs T\<^sub>r pc (length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2)) xt ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc) &&& (\<And>pc' \<tau>'. (pc', \<tau>') \<in> set (eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc xt ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc)) \<Longrightarrow> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc')
[PROOF STEP]
by(fastforce simp add: wt_instr_def)+
[PROOF STATE]
proof (state)
this:
app ((is\<^sub>1 @ is\<^sub>2) ! pc) P mxs T\<^sub>r pc (length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2)) xt ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc)
(?pc'2, ?\<tau>'2) \<in> set (eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc xt ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc)) \<Longrightarrow> P \<turnstile> ?\<tau>'2 \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! ?pc'2

goal (1 subgoal):
 1. \<turnstile> is\<^sub>1 @ is\<^sub>2, xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)] [::] \<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2
[PROOF STEP]
have "app ?i P mxs T\<^sub>r pc ?mpc ?xt' ?t
             \<and> (\<forall>(pc',\<tau>') \<in> set (eff ?i P pc ?xt' ?t). P \<turnstile> \<tau>' \<le>' ?\<tau>s!pc')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. app ((is\<^sub>1 @ is\<^sub>2) ! pc) P mxs T\<^sub>r pc (length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2)) (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc) \<and> (\<forall>(pc', \<tau>')\<in>set (eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc)). P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc')
[PROOF STEP]
proof (cases ?t)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc = None \<Longrightarrow> app ((is\<^sub>1 @ is\<^sub>2) ! pc) P mxs T\<^sub>r pc (length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2)) (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc) \<and> (\<forall>(pc', \<tau>')\<in>set (eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc)). P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc')
 2. \<And>a. (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc = \<lfloor>a\<rfloor> \<Longrightarrow> app ((is\<^sub>1 @ is\<^sub>2) ! pc) P mxs T\<^sub>r pc (length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2)) (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc) \<and> (\<forall>(pc', \<tau>')\<in>set (eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc)). P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc')
[PROOF STEP]
case (Some \<tau>)
[PROOF STATE]
proof (state)
this:
(\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc = \<lfloor>\<tau>\<rfloor>

goal (2 subgoals):
 1. (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc = None \<Longrightarrow> app ((is\<^sub>1 @ is\<^sub>2) ! pc) P mxs T\<^sub>r pc (length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2)) (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc) \<and> (\<forall>(pc', \<tau>')\<in>set (eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc)). P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc')
 2. \<And>a. (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc = \<lfloor>a\<rfloor> \<Longrightarrow> app ((is\<^sub>1 @ is\<^sub>2) ! pc) P mxs T\<^sub>r pc (length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2)) (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc) \<and> (\<forall>(pc', \<tau>')\<in>set (eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc)). P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc')
[PROOF STEP]
obtain ST' LT' where \<tau>: "\<tau> = (ST', LT')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ST' LT'. \<tau> = (ST', LT') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases \<tau>) simp
[PROOF STATE]
proof (state)
this:
\<tau> = (ST', LT')

goal (2 subgoals):
 1. (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc = None \<Longrightarrow> app ((is\<^sub>1 @ is\<^sub>2) ! pc) P mxs T\<^sub>r pc (length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2)) (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc) \<and> (\<forall>(pc', \<tau>')\<in>set (eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc)). P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc')
 2. \<And>a. (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc = \<lfloor>a\<rfloor> \<Longrightarrow> app ((is\<^sub>1 @ is\<^sub>2) ! pc) P mxs T\<^sub>r pc (length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2)) (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc) \<and> (\<forall>(pc', \<tau>')\<in>set (eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc)). P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc')
[PROOF STEP]
have app\<^sub>i: "app\<^sub>i (?i,P,pc,mxs,T\<^sub>r,\<tau>)" and xcpt_app: "xcpt_app ?i P pc mxs xt \<tau>"
         and eff_pc: "\<And>pc' \<tau>'. (pc',\<tau>') \<in> set (eff ?i P pc xt ?t) \<Longrightarrow> pc' < ?mpc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. app\<^sub>i ((is\<^sub>1 @ is\<^sub>2) ! pc, P, pc, mxs, T\<^sub>r, \<tau>) &&& xcpt_app ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc mxs xt \<tau> &&& (\<And>pc' \<tau>'. (pc', \<tau>') \<in> set (eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc xt ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc)) \<Longrightarrow> pc' < length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2))
[PROOF STEP]
using Some app
[PROOF STATE]
proof (prove)
using this:
(\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc = \<lfloor>\<tau>\<rfloor>
app ((is\<^sub>1 @ is\<^sub>2) ! pc) P mxs T\<^sub>r pc (length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2)) xt ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc)

goal (1 subgoal):
 1. app\<^sub>i ((is\<^sub>1 @ is\<^sub>2) ! pc, P, pc, mxs, T\<^sub>r, \<tau>) &&& xcpt_app ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc mxs xt \<tau> &&& (\<And>pc' \<tau>'. (pc', \<tau>') \<in> set (eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc xt ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc)) \<Longrightarrow> pc' < length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2))
[PROOF STEP]
by(fastforce simp add: app_def)+
[PROOF STATE]
proof (state)
this:
app\<^sub>i ((is\<^sub>1 @ is\<^sub>2) ! pc, P, pc, mxs, T\<^sub>r, \<tau>)
xcpt_app ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc mxs xt \<tau>
(?pc'2, ?\<tau>'2) \<in> set (eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc xt ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc)) \<Longrightarrow> ?pc'2 < length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2)

goal (2 subgoals):
 1. (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc = None \<Longrightarrow> app ((is\<^sub>1 @ is\<^sub>2) ! pc) P mxs T\<^sub>r pc (length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2)) (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc) \<and> (\<forall>(pc', \<tau>')\<in>set (eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc)). P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc')
 2. \<And>a. (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc = \<lfloor>a\<rfloor> \<Longrightarrow> app ((is\<^sub>1 @ is\<^sub>2) ! pc) P mxs T\<^sub>r pc (length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2)) (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc) \<and> (\<forall>(pc', \<tau>')\<in>set (eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc)). P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc')
[PROOF STEP]
have "xcpt_app ?i P pc mxs ?xt' \<tau>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xcpt_app ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc mxs (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) \<tau>
[PROOF STEP]
proof(cases "pc < length \<tau>s\<^sub>1 - 1")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. pc < length \<tau>s\<^sub>1 - 1 \<Longrightarrow> xcpt_app ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc mxs (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) \<tau>
 2. \<not> pc < length \<tau>s\<^sub>1 - 1 \<Longrightarrow> xcpt_app ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc mxs (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) \<tau>
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> pc < length \<tau>s\<^sub>1 - 1

goal (2 subgoals):
 1. pc < length \<tau>s\<^sub>1 - 1 \<Longrightarrow> xcpt_app ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc mxs (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) \<tau>
 2. \<not> pc < length \<tau>s\<^sub>1 - 1 \<Longrightarrow> xcpt_app ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc mxs (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) \<tau>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> pc < length \<tau>s\<^sub>1 - 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> pc < length \<tau>s\<^sub>1 - 1

goal (1 subgoal):
 1. xcpt_app ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc mxs (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) \<tau>
[PROOF STEP]
using Some \<tau> is_\<tau>s xcpt_app
[PROOF STATE]
proof (prove)
using this:
\<not> pc < length \<tau>s\<^sub>1 - 1
(\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc = \<lfloor>\<tau>\<rfloor>
\<tau> = (ST', LT')
length is\<^sub>1 = length \<tau>s\<^sub>1
xcpt_app ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc mxs xt \<tau>

goal (1 subgoal):
 1. xcpt_app ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc mxs (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) \<tau>
[PROOF STEP]
by (clarsimp simp: xcpt_app_def relevant_entries_def
                             is_relevant_entry_def)
[PROOF STATE]
proof (state)
this:
xcpt_app ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc mxs (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) \<tau>

goal (1 subgoal):
 1. pc < length \<tau>s\<^sub>1 - 1 \<Longrightarrow> xcpt_app ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc mxs (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) \<tau>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pc < length \<tau>s\<^sub>1 - 1 \<Longrightarrow> xcpt_app ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc mxs (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) \<tau>
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
pc < length \<tau>s\<^sub>1 - 1

goal (1 subgoal):
 1. pc < length \<tau>s\<^sub>1 - 1 \<Longrightarrow> xcpt_app ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc mxs (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) \<tau>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pc < length \<tau>s\<^sub>1 - 1
[PROOF STEP]
have True': "pc < length \<tau>s\<^sub>1"
[PROOF STATE]
proof (prove)
using this:
pc < length \<tau>s\<^sub>1 - 1

goal (1 subgoal):
 1. pc < length \<tau>s\<^sub>1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
pc < length \<tau>s\<^sub>1

goal (1 subgoal):
 1. pc < length \<tau>s\<^sub>1 - 1 \<Longrightarrow> xcpt_app ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc mxs (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) \<tau>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pc < length \<tau>s\<^sub>1
[PROOF STEP]
have "\<tau>s\<^sub>1 ! pc = ?t"
[PROOF STATE]
proof (prove)
using this:
pc < length \<tau>s\<^sub>1

goal (1 subgoal):
 1. \<tau>s\<^sub>1 ! pc = (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc
[PROOF STEP]
by(fastforce simp: nth_append)
[PROOF STATE]
proof (state)
this:
\<tau>s\<^sub>1 ! pc = (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc

goal (1 subgoal):
 1. pc < length \<tau>s\<^sub>1 - 1 \<Longrightarrow> xcpt_app ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc mxs (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) \<tau>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<tau>s\<^sub>1 ! pc = (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc

goal (1 subgoal):
 1. pc < length \<tau>s\<^sub>1 - 1 \<Longrightarrow> xcpt_app ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc mxs (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) \<tau>
[PROOF STEP]
have \<tau>s\<^sub>1_pc: "\<tau>s\<^sub>1 ! pc \<in> set \<tau>s\<^sub>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>s\<^sub>1 ! pc \<in> set \<tau>s\<^sub>1
[PROOF STEP]
by(rule nth_mem[OF True'])
[PROOF STATE]
proof (state)
this:
\<tau>s\<^sub>1 ! pc \<in> set \<tau>s\<^sub>1

goal (1 subgoal):
 1. pc < length \<tau>s\<^sub>1 - 1 \<Longrightarrow> xcpt_app ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc mxs (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) \<tau>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<tau>s\<^sub>1 ! pc = (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc
\<tau>s\<^sub>1 ! pc \<in> set \<tau>s\<^sub>1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<tau>s\<^sub>1 ! pc = (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc
\<tau>s\<^sub>1 ! pc \<in> set \<tau>s\<^sub>1

goal (1 subgoal):
 1. xcpt_app ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc mxs (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) \<tau>
[PROOF STEP]
using Some \<tau> PC ST_mxs xcpt_app P_\<tau>s\<^sub>1'[OF \<tau>s\<^sub>1_pc]
[PROOF STATE]
proof (prove)
using this:
\<tau>s\<^sub>1 ! pc = (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc
\<tau>s\<^sub>1 ! pc \<in> set \<tau>s\<^sub>1
(\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc = \<lfloor>\<tau>\<rfloor>
\<tau> = (ST', LT')
is_class P C
length ST < mxs
xcpt_app ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc mxs xt \<tau>
\<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

goal (1 subgoal):
 1. xcpt_app ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc mxs (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) \<tau>
[PROOF STEP]
by (simp add: xcpt_app_def relevant_entries_def)
[PROOF STATE]
proof (state)
this:
xcpt_app ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc mxs (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) \<tau>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
xcpt_app ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc mxs (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) \<tau>

goal (2 subgoals):
 1. (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc = None \<Longrightarrow> app ((is\<^sub>1 @ is\<^sub>2) ! pc) P mxs T\<^sub>r pc (length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2)) (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc) \<and> (\<forall>(pc', \<tau>')\<in>set (eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc)). P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc')
 2. \<And>a. (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc = \<lfloor>a\<rfloor> \<Longrightarrow> app ((is\<^sub>1 @ is\<^sub>2) ! pc) P mxs T\<^sub>r pc (length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2)) (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc) \<and> (\<forall>(pc', \<tau>')\<in>set (eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc)). P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
xcpt_app ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc mxs (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) \<tau>

goal (2 subgoals):
 1. (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc = None \<Longrightarrow> app ((is\<^sub>1 @ is\<^sub>2) ! pc) P mxs T\<^sub>r pc (length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2)) (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc) \<and> (\<forall>(pc', \<tau>')\<in>set (eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc)). P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc')
 2. \<And>a. (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc = \<lfloor>a\<rfloor> \<Longrightarrow> app ((is\<^sub>1 @ is\<^sub>2) ! pc) P mxs T\<^sub>r pc (length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2)) (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc) \<and> (\<forall>(pc', \<tau>')\<in>set (eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc)). P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc')
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
xcpt_app ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc mxs (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) \<tau>

goal (2 subgoals):
 1. (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc = None \<Longrightarrow> app ((is\<^sub>1 @ is\<^sub>2) ! pc) P mxs T\<^sub>r pc (length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2)) (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc) \<and> (\<forall>(pc', \<tau>')\<in>set (eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc)). P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc')
 2. \<And>a. (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc = \<lfloor>a\<rfloor> \<Longrightarrow> app ((is\<^sub>1 @ is\<^sub>2) ! pc) P mxs T\<^sub>r pc (length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2)) (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc) \<and> (\<forall>(pc', \<tau>')\<in>set (eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc)). P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc')
[PROOF STEP]
fix pc' \<tau>'
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc = None \<Longrightarrow> app ((is\<^sub>1 @ is\<^sub>2) ! pc) P mxs T\<^sub>r pc (length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2)) (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc) \<and> (\<forall>(pc', \<tau>')\<in>set (eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc)). P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc')
 2. \<And>a. (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc = \<lfloor>a\<rfloor> \<Longrightarrow> app ((is\<^sub>1 @ is\<^sub>2) ! pc) P mxs T\<^sub>r pc (length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2)) (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc) \<and> (\<forall>(pc', \<tau>')\<in>set (eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc)). P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc')
[PROOF STEP]
assume efft: "(pc',\<tau>') \<in> set (eff ?i P pc ?xt' ?t)"
[PROOF STATE]
proof (state)
this:
(pc', \<tau>') \<in> set (eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc))

goal (2 subgoals):
 1. (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc = None \<Longrightarrow> app ((is\<^sub>1 @ is\<^sub>2) ! pc) P mxs T\<^sub>r pc (length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2)) (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc) \<and> (\<forall>(pc', \<tau>')\<in>set (eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc)). P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc')
 2. \<And>a. (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc = \<lfloor>a\<rfloor> \<Longrightarrow> app ((is\<^sub>1 @ is\<^sub>2) ! pc) P mxs T\<^sub>r pc (length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2)) (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc) \<and> (\<forall>(pc', \<tau>')\<in>set (eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc)). P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc')
[PROOF STEP]
have "pc' < ?mpc \<and> P \<turnstile> \<tau>' \<le>' ?\<tau>s!pc'" (is "?P1 \<and> ?P2")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pc' < length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) \<and> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc'
[PROOF STEP]
proof(cases "(pc',\<tau>') \<in> set (eff ?i P pc xt ?t)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (pc', \<tau>') \<in> set (eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc xt ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc)) \<Longrightarrow> pc' < length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) \<and> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc'
 2. (pc', \<tau>') \<notin> set (eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc xt ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc)) \<Longrightarrow> pc' < length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) \<and> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc'
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
(pc', \<tau>') \<in> set (eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc xt ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc))

goal (2 subgoals):
 1. (pc', \<tau>') \<in> set (eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc xt ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc)) \<Longrightarrow> pc' < length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) \<and> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc'
 2. (pc', \<tau>') \<notin> set (eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc xt ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc)) \<Longrightarrow> pc' < length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) \<and> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc'
[PROOF STEP]
have ?P1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pc' < length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2)
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
(pc', \<tau>') \<in> set (eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc xt ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc))

goal (1 subgoal):
 1. pc' < length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2)
[PROOF STEP]
by(rule eff_pc)
[PROOF STATE]
proof (state)
this:
pc' < length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2)

goal (2 subgoals):
 1. (pc', \<tau>') \<in> set (eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc xt ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc)) \<Longrightarrow> pc' < length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) \<and> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc'
 2. (pc', \<tau>') \<notin> set (eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc xt ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc)) \<Longrightarrow> pc' < length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) \<and> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
pc' < length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2)

goal (2 subgoals):
 1. (pc', \<tau>') \<in> set (eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc xt ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc)) \<Longrightarrow> pc' < length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) \<and> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc'
 2. (pc', \<tau>') \<notin> set (eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc xt ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc)) \<Longrightarrow> pc' < length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) \<and> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc'
[PROOF STEP]
have ?P2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc'
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
(pc', \<tau>') \<in> set (eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc xt ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc))

goal (1 subgoal):
 1. P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc'
[PROOF STEP]
by(rule eff_ss)
[PROOF STATE]
proof (state)
this:
P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc'

goal (2 subgoals):
 1. (pc', \<tau>') \<in> set (eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc xt ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc)) \<Longrightarrow> pc' < length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) \<and> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc'
 2. (pc', \<tau>') \<notin> set (eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc xt ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc)) \<Longrightarrow> pc' < length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) \<and> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
pc' < length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2)
P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
pc' < length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2)
P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc'

goal (1 subgoal):
 1. pc' < length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) \<and> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
pc' < length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) \<and> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc'

goal (1 subgoal):
 1. (pc', \<tau>') \<notin> set (eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc xt ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc)) \<Longrightarrow> pc' < length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) \<and> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (pc', \<tau>') \<notin> set (eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc xt ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc)) \<Longrightarrow> pc' < length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) \<and> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc'
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
(pc', \<tau>') \<notin> set (eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc xt ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc))

goal (1 subgoal):
 1. (pc', \<tau>') \<notin> set (eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc xt ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc)) \<Longrightarrow> pc' < length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) \<and> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(pc', \<tau>') \<notin> set (eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc xt ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc))
[PROOF STEP]
have xte: "(pc',\<tau>') \<in> set (xcpt_eff ?i P pc \<tau> [?xte])"
[PROOF STATE]
proof (prove)
using this:
(pc', \<tau>') \<notin> set (eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc xt ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc))

goal (1 subgoal):
 1. (pc', \<tau>') \<in> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc \<tau> [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)])
[PROOF STEP]
using efft Some
[PROOF STATE]
proof (prove)
using this:
(pc', \<tau>') \<notin> set (eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc xt ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc))
(pc', \<tau>') \<in> set (eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc))
(\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc = \<lfloor>\<tau>\<rfloor>

goal (1 subgoal):
 1. (pc', \<tau>') \<in> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc \<tau> [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)])
[PROOF STEP]
by(clarsimp simp: eff_def)
[PROOF STATE]
proof (state)
this:
(pc', \<tau>') \<in> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc \<tau> [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)])

goal (1 subgoal):
 1. (pc', \<tau>') \<notin> set (eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc xt ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc)) \<Longrightarrow> pc' < length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) \<and> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(pc', \<tau>') \<in> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc \<tau> [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)])
[PROOF STEP]
have ?P1
[PROOF STATE]
proof (prove)
using this:
(pc', \<tau>') \<in> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc \<tau> [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)])

goal (1 subgoal):
 1. pc' < length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2)
[PROOF STEP]
using Some \<tau> is_\<tau>s
[PROOF STATE]
proof (prove)
using this:
(pc', \<tau>') \<in> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc \<tau> [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)])
(\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc = \<lfloor>\<tau>\<rfloor>
\<tau> = (ST', LT')
length is\<^sub>1 = length \<tau>s\<^sub>1

goal (1 subgoal):
 1. pc' < length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2)
[PROOF STEP]
by(clarsimp simp: xcpt_eff_def relevant_entries_def split: if_split_asm)
[PROOF STATE]
proof (state)
this:
pc' < length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2)

goal (1 subgoal):
 1. (pc', \<tau>') \<notin> set (eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc xt ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc)) \<Longrightarrow> pc' < length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) \<and> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
pc' < length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2)

goal (1 subgoal):
 1. (pc', \<tau>') \<notin> set (eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc xt ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc)) \<Longrightarrow> pc' < length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) \<and> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc'
[PROOF STEP]
have ?P2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc'
[PROOF STEP]
proof(cases "pc < length \<tau>s\<^sub>1 - 1")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. pc < length \<tau>s\<^sub>1 - 1 \<Longrightarrow> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc'
 2. \<not> pc < length \<tau>s\<^sub>1 - 1 \<Longrightarrow> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc'
[PROOF STEP]
case False': False
[PROOF STATE]
proof (state)
this:
\<not> pc < length \<tau>s\<^sub>1 - 1

goal (2 subgoals):
 1. pc < length \<tau>s\<^sub>1 - 1 \<Longrightarrow> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc'
 2. \<not> pc < length \<tau>s\<^sub>1 - 1 \<Longrightarrow> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> pc < length \<tau>s\<^sub>1 - 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> pc < length \<tau>s\<^sub>1 - 1

goal (1 subgoal):
 1. P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc'
[PROOF STEP]
using False Some \<tau> xte is_\<tau>s
[PROOF STATE]
proof (prove)
using this:
\<not> pc < length \<tau>s\<^sub>1 - 1
(pc', \<tau>') \<notin> set (eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc xt ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc))
(\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc = \<lfloor>\<tau>\<rfloor>
\<tau> = (ST', LT')
(pc', \<tau>') \<in> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc \<tau> [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)])
length is\<^sub>1 = length \<tau>s\<^sub>1

goal (1 subgoal):
 1. P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc'
[PROOF STEP]
by(simp add: xcpt_eff_def relevant_entries_def is_relevant_entry_def)
[PROOF STATE]
proof (state)
this:
P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc'

goal (1 subgoal):
 1. pc < length \<tau>s\<^sub>1 - 1 \<Longrightarrow> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pc < length \<tau>s\<^sub>1 - 1 \<Longrightarrow> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc'
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
pc < length \<tau>s\<^sub>1 - 1

goal (1 subgoal):
 1. pc < length \<tau>s\<^sub>1 - 1 \<Longrightarrow> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pc < length \<tau>s\<^sub>1 - 1
[PROOF STEP]
have True': "pc < length \<tau>s\<^sub>1"
[PROOF STATE]
proof (prove)
using this:
pc < length \<tau>s\<^sub>1 - 1

goal (1 subgoal):
 1. pc < length \<tau>s\<^sub>1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
pc < length \<tau>s\<^sub>1

goal (1 subgoal):
 1. pc < length \<tau>s\<^sub>1 - 1 \<Longrightarrow> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc'
[PROOF STEP]
have \<tau>s\<^sub>1_pc: "\<tau>s\<^sub>1 ! pc \<in> set \<tau>s\<^sub>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>s\<^sub>1 ! pc \<in> set \<tau>s\<^sub>1
[PROOF STEP]
by(rule nth_mem[OF True'])
[PROOF STATE]
proof (state)
this:
\<tau>s\<^sub>1 ! pc \<in> set \<tau>s\<^sub>1

goal (1 subgoal):
 1. pc < length \<tau>s\<^sub>1 - 1 \<Longrightarrow> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc'
[PROOF STEP]
have "P \<turnstile> \<lfloor>(Class C # drop (length ST' - length ST) ST', LT')\<rfloor>
                         \<le>' ty\<^sub>i' (Class C # ST) E A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> \<lfloor>(Class C # drop (length ST' - length ST) ST', LT')\<rfloor> \<le>' ty\<^sub>i' (Class C # ST) E A
[PROOF STEP]
using True' Some \<tau> P_\<tau>s\<^sub>1'[OF \<tau>s\<^sub>1_pc]
[PROOF STATE]
proof (prove)
using this:
pc < length \<tau>s\<^sub>1
(\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc = \<lfloor>\<tau>\<rfloor>
\<tau> = (ST', LT')
\<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

goal (1 subgoal):
 1. P \<turnstile> \<lfloor>(Class C # drop (length ST' - length ST) ST', LT')\<rfloor> \<le>' ty\<^sub>i' (Class C # ST) E A
[PROOF STEP]
by (fastforce simp: nth_append ty\<^sub>i'_def)
[PROOF STATE]
proof (state)
this:
P \<turnstile> \<lfloor>(Class C # drop (length ST' - length ST) ST', LT')\<rfloor> \<le>' ty\<^sub>i' (Class C # ST) E A

goal (1 subgoal):
 1. pc < length \<tau>s\<^sub>1 - 1 \<Longrightarrow> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
P \<turnstile> \<lfloor>(Class C # drop (length ST' - length ST) ST', LT')\<rfloor> \<le>' ty\<^sub>i' (Class C # ST) E A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> \<lfloor>(Class C # drop (length ST' - length ST) ST', LT')\<rfloor> \<le>' ty\<^sub>i' (Class C # ST) E A

goal (1 subgoal):
 1. P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc'
[PROOF STEP]
using \<tau> xte is_\<tau>s
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> \<lfloor>(Class C # drop (length ST' - length ST) ST', LT')\<rfloor> \<le>' ty\<^sub>i' (Class C # ST) E A
\<tau> = (ST', LT')
(pc', \<tau>') \<in> set (xcpt_eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc \<tau> [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)])
length is\<^sub>1 = length \<tau>s\<^sub>1

goal (1 subgoal):
 1. P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc'
[PROOF STEP]
by(simp add: xcpt_eff_def relevant_entries_def split: if_split_asm)
[PROOF STATE]
proof (state)
this:
P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc'

goal (1 subgoal):
 1. (pc', \<tau>') \<notin> set (eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc xt ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc)) \<Longrightarrow> pc' < length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) \<and> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
pc' < length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2)
P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
pc' < length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2)
P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc'

goal (1 subgoal):
 1. pc' < length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) \<and> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
pc' < length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) \<and> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
pc' < length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) \<and> P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc'

goal (2 subgoals):
 1. (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc = None \<Longrightarrow> app ((is\<^sub>1 @ is\<^sub>2) ! pc) P mxs T\<^sub>r pc (length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2)) (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc) \<and> (\<forall>(pc', \<tau>')\<in>set (eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc)). P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc')
 2. \<And>a. (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc = \<lfloor>a\<rfloor> \<Longrightarrow> app ((is\<^sub>1 @ is\<^sub>2) ! pc) P mxs T\<^sub>r pc (length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2)) (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc) \<and> (\<forall>(pc', \<tau>')\<in>set (eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc)). P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc')
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(?pc'4, ?\<tau>'4) \<in> set (eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc)) \<Longrightarrow> ?pc'4 < length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) \<and> P \<turnstile> ?\<tau>'4 \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! ?pc'4

goal (2 subgoals):
 1. (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc = None \<Longrightarrow> app ((is\<^sub>1 @ is\<^sub>2) ! pc) P mxs T\<^sub>r pc (length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2)) (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc) \<and> (\<forall>(pc', \<tau>')\<in>set (eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc)). P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc')
 2. \<And>a. (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc = \<lfloor>a\<rfloor> \<Longrightarrow> app ((is\<^sub>1 @ is\<^sub>2) ! pc) P mxs T\<^sub>r pc (length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2)) (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc) \<and> (\<forall>(pc', \<tau>')\<in>set (eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc)). P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
xcpt_app ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc mxs (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) \<tau>
(?pc'4, ?\<tau>'4) \<in> set (eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc)) \<Longrightarrow> ?pc'4 < length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) \<and> P \<turnstile> ?\<tau>'4 \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! ?pc'4
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
xcpt_app ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc mxs (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) \<tau>
(?pc'4, ?\<tau>'4) \<in> set (eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc)) \<Longrightarrow> ?pc'4 < length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) \<and> P \<turnstile> ?\<tau>'4 \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! ?pc'4

goal (1 subgoal):
 1. app ((is\<^sub>1 @ is\<^sub>2) ! pc) P mxs T\<^sub>r pc (length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2)) (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc) \<and> (\<forall>(pc', \<tau>')\<in>set (eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc)). P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc')
[PROOF STEP]
using Some app\<^sub>i
[PROOF STATE]
proof (prove)
using this:
xcpt_app ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc mxs (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) \<tau>
(?pc'4, ?\<tau>'4) \<in> set (eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc)) \<Longrightarrow> ?pc'4 < length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) \<and> P \<turnstile> ?\<tau>'4 \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! ?pc'4
(\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc = \<lfloor>\<tau>\<rfloor>
app\<^sub>i ((is\<^sub>1 @ is\<^sub>2) ! pc, P, pc, mxs, T\<^sub>r, \<tau>)

goal (1 subgoal):
 1. app ((is\<^sub>1 @ is\<^sub>2) ! pc) P mxs T\<^sub>r pc (length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2)) (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc) \<and> (\<forall>(pc', \<tau>')\<in>set (eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc)). P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc')
[PROOF STEP]
by(fastforce simp add: app_def)
[PROOF STATE]
proof (state)
this:
app ((is\<^sub>1 @ is\<^sub>2) ! pc) P mxs T\<^sub>r pc (length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2)) (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc) \<and> (\<forall>(pc', \<tau>')\<in>set (eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc)). P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc')

goal (1 subgoal):
 1. (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc = None \<Longrightarrow> app ((is\<^sub>1 @ is\<^sub>2) ! pc) P mxs T\<^sub>r pc (length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2)) (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc) \<and> (\<forall>(pc', \<tau>')\<in>set (eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc)). P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc')
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
app ((is\<^sub>1 @ is\<^sub>2) ! pc) P mxs T\<^sub>r pc (length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2)) (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc) \<and> (\<forall>(pc', \<tau>')\<in>set (eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc)). P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc')

goal (1 subgoal):
 1. \<turnstile> is\<^sub>1 @ is\<^sub>2, xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)] [::] \<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
app ((is\<^sub>1 @ is\<^sub>2) ! pc) P mxs T\<^sub>r pc (length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2)) (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc) \<and> (\<forall>(pc', \<tau>')\<in>set (eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc)). P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc')
[PROOF STEP]
have "P,T\<^sub>r,mxs,size ?\<tau>s,?xt' \<turnstile> ?is!pc,pc :: ?\<tau>s"
[PROOF STATE]
proof (prove)
using this:
app ((is\<^sub>1 @ is\<^sub>2) ! pc) P mxs T\<^sub>r pc (length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2)) (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc) \<and> (\<forall>(pc', \<tau>')\<in>set (eff ((is\<^sub>1 @ is\<^sub>2) ! pc) P pc (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) ((\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc)). P \<turnstile> \<tau>' \<le>' (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2) ! pc')

goal (1 subgoal):
 1. P,T\<^sub>r,mxs,length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2),xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)] \<turnstile> (is\<^sub>1 @ is\<^sub>2) ! pc,pc :: \<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2
[PROOF STEP]
by(simp add: wt_instr_def)
[PROOF STATE]
proof (state)
this:
P,T\<^sub>r,mxs,length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2),xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)] \<turnstile> (is\<^sub>1 @ is\<^sub>2) ! pc,pc :: \<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2

goal (1 subgoal):
 1. \<turnstile> is\<^sub>1 @ is\<^sub>2, xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)] [::] \<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?pc4 < length (is\<^sub>1 @ is\<^sub>2) \<Longrightarrow> P,T\<^sub>r,mxs,length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2),xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)] \<turnstile> (is\<^sub>1 @ is\<^sub>2) ! ?pc4,?pc4 :: \<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2

goal (1 subgoal):
 1. \<turnstile> is\<^sub>1 @ is\<^sub>2, xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)] [::] \<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
length (is\<^sub>1 @ is\<^sub>2) < length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2)
pcs (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) \<subseteq> {0..<length (is\<^sub>1 @ is\<^sub>2)}
?pc2 < length (is\<^sub>1 @ is\<^sub>2) \<Longrightarrow> P,T\<^sub>r,mxs,length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2),xt \<turnstile> (is\<^sub>1 @ is\<^sub>2) ! ?pc2,?pc2 :: \<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2
?pc4 < length (is\<^sub>1 @ is\<^sub>2) \<Longrightarrow> P,T\<^sub>r,mxs,length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2),xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)] \<turnstile> (is\<^sub>1 @ is\<^sub>2) ! ?pc4,?pc4 :: \<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
length (is\<^sub>1 @ is\<^sub>2) < length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2)
pcs (xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)]) \<subseteq> {0..<length (is\<^sub>1 @ is\<^sub>2)}
?pc2 < length (is\<^sub>1 @ is\<^sub>2) \<Longrightarrow> P,T\<^sub>r,mxs,length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2),xt \<turnstile> (is\<^sub>1 @ is\<^sub>2) ! ?pc2,?pc2 :: \<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2
?pc4 < length (is\<^sub>1 @ is\<^sub>2) \<Longrightarrow> P,T\<^sub>r,mxs,length (\<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2),xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)] \<turnstile> (is\<^sub>1 @ is\<^sub>2) ! ?pc4,?pc4 :: \<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2

goal (1 subgoal):
 1. \<turnstile> is\<^sub>1 @ is\<^sub>2, xt @ [(0, length is\<^sub>1 - 1, C, 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(simp add:wt_instrs_def)
[PROOF STATE]
proof (state)
this:
\<turnstile> is\<^sub>1 @ is\<^sub>2, xt @ [(0, length is\<^sub>1 - 1, C, length is\<^sub>1, length ST)] [::] \<tau>s\<^sub>1 @ ty\<^sub>i' (Class C # ST) E A # \<tau>s\<^sub>2

goal:
No subgoals!
[PROOF STEP]
qed


[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]
proof(induct n)
[PROOF STATE]
proof (state)
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]
case (Suc n)
[PROOF STATE]
proof (state)
this:
drop n ?xs = y # ys \<Longrightarrow> drop (Suc n) ?xs = ys
drop (Suc n) xs = y # ys

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]
then
[PROOF STATE]
proof (chain)
picking this:
drop n ?xs = y # ys \<Longrightarrow> drop (Suc n) ?xs = ys
drop (Suc n) xs = y # ys
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
drop n ?xs = y # ys \<Longrightarrow> drop (Suc n) ?xs = ys
drop (Suc n) xs = y # ys

goal (1 subgoal):
 1. drop (Suc (Suc n)) xs = ys
[PROOF STEP]
by(simp add: drop_Suc)
[PROOF STATE]
proof (state)
this:
drop (Suc (Suc n)) xs = ys

goal (1 subgoal):
 1. \<And>xs. drop 0 xs = y # ys \<Longrightarrow> drop (Suc 0) xs = ys
[PROOF STEP]
qed simp


[STATEMENT]
lemma drop_mess:
assumes "Suc (length xs\<^sub>0) \<le> length xs"
  and "drop (length xs - Suc (length xs\<^sub>0)) xs = x # xs\<^sub>0"
shows "drop (length xs - length xs\<^sub>0) xs = xs\<^sub>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. drop (length xs - length xs\<^sub>0) xs = xs\<^sub>0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Suc (length xs\<^sub>0) \<le> length xs
drop (length xs - Suc (length xs\<^sub>0)) xs = x # xs\<^sub>0

goal (1 subgoal):
 1. drop (length xs - length xs\<^sub>0) xs = xs\<^sub>0
[PROOF STEP]
proof(cases xs)
[PROOF STATE]
proof (state)
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]
case (Cons a list)
[PROOF STATE]
proof (state)
this:
xs = a # list

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]
then
[PROOF STATE]
proof (chain)
picking this:
xs = a # list
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
xs = a # list

goal (1 subgoal):
 1. drop (length xs - length xs\<^sub>0) xs = xs\<^sub>0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
xs = a # list
Suc (length xs\<^sub>0) \<le> length xs
drop (length xs - Suc (length xs\<^sub>0)) xs = x # xs\<^sub>0

goal (1 subgoal):
 1. drop (length xs - length xs\<^sub>0) xs = xs\<^sub>0
[PROOF STEP]
proof(cases "length list - length xs\<^sub>0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>xs = a # list; Suc (length xs\<^sub>0) \<le> length xs; drop (length xs - Suc (length xs\<^sub>0)) xs = x # xs\<^sub>0; length list - length xs\<^sub>0 = 0\<rbrakk> \<Longrightarrow> drop (length xs - length xs\<^sub>0) xs = xs\<^sub>0
 2. \<And>nat. \<lbrakk>xs = a # list; Suc (length xs\<^sub>0) \<le> length xs; drop (length xs - Suc (length xs\<^sub>0)) xs = x # xs\<^sub>0; length list - length xs\<^sub>0 = Suc nat\<rbrakk> \<Longrightarrow> drop (length xs - length xs\<^sub>0) xs = xs\<^sub>0
[PROOF STEP]
case Suc
[PROOF STATE]
proof (state)
this:
length list - length xs\<^sub>0 = Suc nat_

goal (2 subgoals):
 1. \<lbrakk>xs = a # list; Suc (length xs\<^sub>0) \<le> length xs; drop (length xs - Suc (length xs\<^sub>0)) xs = x # xs\<^sub>0; length list - length xs\<^sub>0 = 0\<rbrakk> \<Longrightarrow> drop (length xs - length xs\<^sub>0) xs = xs\<^sub>0
 2. \<And>nat. \<lbrakk>xs = a # list; Suc (length xs\<^sub>0) \<le> length xs; drop (length xs - Suc (length xs\<^sub>0)) xs = x # xs\<^sub>0; length list - length xs\<^sub>0 = Suc nat\<rbrakk> \<Longrightarrow> drop (length xs - length xs\<^sub>0) xs = xs\<^sub>0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length list - length xs\<^sub>0 = Suc nat_
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
length list - length xs\<^sub>0 = Suc nat_

goal (1 subgoal):
 1. drop (length xs - length xs\<^sub>0) xs = xs\<^sub>0
[PROOF STEP]
using Cons assms
[PROOF STATE]
proof (prove)
using this:
length list - length xs\<^sub>0 = Suc nat_
xs = a # list
Suc (length xs\<^sub>0) \<le> length xs
drop (length xs - Suc (length xs\<^sub>0)) xs = x # xs\<^sub>0

goal (1 subgoal):
 1. drop (length xs - length xs\<^sub>0) xs = xs\<^sub>0
[PROOF STEP]
by (simp add: Suc_diff_le drop_Cons_Suc)
[PROOF STATE]
proof (state)
this:
drop (length xs - length xs\<^sub>0) xs = xs\<^sub>0

goal (1 subgoal):
 1. \<lbrakk>xs = a # list; Suc (length xs\<^sub>0) \<le> length xs; drop (length xs - Suc (length xs\<^sub>0)) xs = x # xs\<^sub>0; length list - length xs\<^sub>0 = 0\<rbrakk> \<Longrightarrow> drop (length xs - length xs\<^sub>0) xs = xs\<^sub>0
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
drop (length xs - length xs\<^sub>0) xs = xs\<^sub>0

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; xs = []\<rbrakk> \<Longrightarrow> drop (length xs - length xs\<^sub>0) xs = xs\<^sub>0
[PROOF STEP]
qed simp