[STATEMENT]
lemma [simp]: "shift 0 xt = xt"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. shift 0 xt = xt
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. shift 0 xt = xt
[PROOF STEP]
by(induct xt)(auto simp:shift_def)


[STATEMENT]
lemma [simp]: "shift n [] = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. shift n [] = []
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. shift n [] = []
[PROOF STEP]
by(simp add:shift_def)


[STATEMENT]
lemma [simp]: "shift n (xt\<^sub>1 @ xt\<^sub>2) = shift n xt\<^sub>1 @ shift n xt\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. shift n (xt\<^sub>1 @ xt\<^sub>2) = shift n xt\<^sub>1 @ shift n xt\<^sub>2
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. shift n (xt\<^sub>1 @ xt\<^sub>2) = shift n xt\<^sub>1 @ shift n xt\<^sub>2
[PROOF STEP]
by(simp add:shift_def)


[STATEMENT]
lemma [simp]: "shift m (shift n xt) = shift (m+n) xt"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. shift m (shift n xt) = shift (m + n) xt
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. shift m (shift n xt) = shift (m + n) xt
[PROOF STEP]
by(induct xt)(auto simp:shift_def)


[STATEMENT]
lemma [simp]: "pcs (shift n xt) = {pc+n|pc. pc \<in> pcs xt}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pcs (shift n xt) = {pc + n |pc. pc \<in> pcs xt}
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pcs (shift n xt) = {pc + n |pc. pc \<in> pcs xt}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pcs (shift n xt) = {pc + n |pc. pc \<in> pcs xt}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pcs (shift n xt) = {pc + n |pc. pc \<in> pcs xt}
[PROOF STEP]
fix x f t C h d
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pcs (shift n xt) = {pc + n |pc. pc \<in> pcs xt}
[PROOF STEP]
assume "(f,t,C,h,d) \<in> set xt" and "f + n \<le> x"
      and "x < t + n"
[PROOF STATE]
proof (state)
this:
(f, t, C, h, d) \<in> set xt
f + n \<le> x
x < t + n

goal (1 subgoal):
 1. pcs (shift n xt) = {pc + n |pc. pc \<in> pcs xt}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(f, t, C, h, d) \<in> set xt
f + n \<le> x
x < t + n
[PROOF STEP]
have "\<exists>pc. x = pc + n \<and> (\<exists>x\<in>set xt. pc \<in> (case x of (f, t, C, h, d) \<Rightarrow> {f..<t}))"
[PROOF STATE]
proof (prove)
using this:
(f, t, C, h, d) \<in> set xt
f + n \<le> x
x < t + n

goal (1 subgoal):
 1. \<exists>pc. x = pc + n \<and> (\<exists>x\<in>set xt. pc \<in> (case x of (f, t, C, h, d) \<Rightarrow> {f..<t}))
[PROOF STEP]
by(rule_tac x = "x-n" in exI) (force split:nat_diff_split)
[PROOF STATE]
proof (state)
this:
\<exists>pc. x = pc + n \<and> (\<exists>x\<in>set xt. pc \<in> (case x of (f, t, C, h, d) \<Rightarrow> {f..<t}))

goal (1 subgoal):
 1. pcs (shift n xt) = {pc + n |pc. pc \<in> pcs xt}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?f2, ?t2, ?C2, ?h2, ?d2) \<in> set xt; ?f2 + n \<le> ?x2; ?x2 < ?t2 + n\<rbrakk> \<Longrightarrow> \<exists>pc. ?x2 = pc + n \<and> (\<exists>x\<in>set xt. pc \<in> (case x of (f, t, C, h, d) \<Rightarrow> {f..<t}))

goal (1 subgoal):
 1. pcs (shift n xt) = {pc + n |pc. pc \<in> pcs xt}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>(?f2, ?t2, ?C2, ?h2, ?d2) \<in> set xt; ?f2 + n \<le> ?x2; ?x2 < ?t2 + n\<rbrakk> \<Longrightarrow> \<exists>pc. ?x2 = pc + n \<and> (\<exists>x\<in>set xt. pc \<in> (case x of (f, t, C, h, d) \<Rightarrow> {f..<t}))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?f2, ?t2, ?C2, ?h2, ?d2) \<in> set xt; ?f2 + n \<le> ?x2; ?x2 < ?t2 + n\<rbrakk> \<Longrightarrow> \<exists>pc. ?x2 = pc + n \<and> (\<exists>x\<in>set xt. pc \<in> (case x of (f, t, C, h, d) \<Rightarrow> {f..<t}))

goal (1 subgoal):
 1. pcs (shift n xt) = {pc + n |pc. pc \<in> pcs xt}
[PROOF STEP]
by(auto simp:shift_def pcs_def) fast
[PROOF STATE]
proof (state)
this:
pcs (shift n xt) = {pc + n |pc. pc \<in> pcs xt}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma shift_compxE\<^sub>2:
shows "\<And>pc pc' d. shift pc (compxE\<^sub>2 e pc' d) = compxE\<^sub>2 e (pc' + pc) d"
and  "\<And>pc pc' d. shift pc (compxEs\<^sub>2 es pc' d) = compxEs\<^sub>2 es (pc' + pc) d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>pc pc' d. shift pc (compxE\<^sub>2 e pc' d) = compxE\<^sub>2 e (pc' + pc) d) &&& (\<And>pc pc' d. shift pc (compxEs\<^sub>2 es pc' d) = compxEs\<^sub>2 es (pc' + pc) d)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>pc pc' d. shift pc (compxE\<^sub>2 e pc' d) = compxE\<^sub>2 e (pc' + pc) d) &&& (\<And>pc pc' d. shift pc (compxEs\<^sub>2 es pc' d) = compxEs\<^sub>2 es (pc' + pc) d)
[PROOF STEP]
by(induct e and es rule: compxE\<^sub>2.induct compxEs\<^sub>2.induct)
  (auto simp:shift_def ac_simps)


[STATEMENT]
lemma compxE\<^sub>2_size_convs[simp]:
shows "n \<noteq> 0 \<Longrightarrow> compxE\<^sub>2 e n d = shift n (compxE\<^sub>2 e 0 d)"
and "n \<noteq> 0 \<Longrightarrow> compxEs\<^sub>2 es n d = shift n (compxEs\<^sub>2 es 0 d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (n \<noteq> 0 \<Longrightarrow> compxE\<^sub>2 e n d = shift n (compxE\<^sub>2 e 0 d)) &&& (n \<noteq> 0 \<Longrightarrow> compxEs\<^sub>2 es n d = shift n (compxEs\<^sub>2 es 0 d))
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (n \<noteq> 0 \<Longrightarrow> compxE\<^sub>2 e n d = shift n (compxE\<^sub>2 e 0 d)) &&& (n \<noteq> 0 \<Longrightarrow> compxEs\<^sub>2 es n d = shift n (compxEs\<^sub>2 es 0 d))
[PROOF STEP]
by(simp_all add:shift_compxE\<^sub>2)


[STATEMENT]
lemma (in TC2) [simp]: "\<tau>s \<noteq> [] \<Longrightarrow> \<turnstile> [],[] [::] \<tau>s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>s \<noteq> [] \<Longrightarrow> \<turnstile> [], [] [::] \<tau>s
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>s \<noteq> [] \<Longrightarrow> \<turnstile> [], [] [::] \<tau>s
[PROOF STEP]
by (simp add: wt_defs)


[STATEMENT]
lemma [simp]: "eff i P pc et None = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eff i P pc et None = []
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eff i P pc et None = []
[PROOF STEP]
by (simp add: Effect.eff_def)


[STATEMENT]
lemma wt_instr_appR:
 "\<lbrakk> P,T,m,mpc,xt \<turnstile> is!pc,pc :: \<tau>s;
    pc < size is; size is < size \<tau>s; mpc \<le> size \<tau>s; mpc \<le> mpc' \<rbrakk>
  \<Longrightarrow> P,T,m,mpc',xt \<turnstile> is!pc,pc :: \<tau>s@\<tau>s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P,T,m,mpc,xt \<turnstile> is ! pc,pc :: \<tau>s; pc < length is; length is < length \<tau>s; mpc \<le> length \<tau>s; mpc \<le> mpc'\<rbrakk> \<Longrightarrow> P,T,m,mpc',xt \<turnstile> is ! pc,pc :: \<tau>s @ \<tau>s'
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P,T,m,mpc,xt \<turnstile> is ! pc,pc :: \<tau>s; pc < length is; length is < length \<tau>s; mpc \<le> length \<tau>s; mpc \<le> mpc'\<rbrakk> \<Longrightarrow> P,T,m,mpc',xt \<turnstile> is ! pc,pc :: \<tau>s @ \<tau>s'
[PROOF STEP]
by (fastforce simp:wt_instr_def app_def)


[STATEMENT]
lemma relevant_entries_shift [simp]:
  "relevant_entries P i (pc+n) (shift n xt) = shift n (relevant_entries P i pc xt)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. relevant_entries P i (pc + n) (shift n xt) = shift n (relevant_entries P i pc xt)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. relevant_entries P i (pc + n) (shift n xt) = shift n (relevant_entries P i pc xt)
[PROOF STEP]
proof(induct xt)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. relevant_entries P i (pc + n) (shift n []) = shift n (relevant_entries P i pc [])
 2. \<And>a xt. relevant_entries P i (pc + n) (shift n xt) = shift n (relevant_entries P i pc xt) \<Longrightarrow> relevant_entries P i (pc + n) (shift n (a # xt)) = shift n (relevant_entries P i pc (a # xt))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. relevant_entries P i (pc + n) (shift n []) = shift n (relevant_entries P i pc [])
 2. \<And>a xt. relevant_entries P i (pc + n) (shift n xt) = shift n (relevant_entries P i pc xt) \<Longrightarrow> relevant_entries P i (pc + n) (shift n (a # xt)) = shift n (relevant_entries P i pc (a # xt))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. relevant_entries P i (pc + n) (shift n []) = shift n (relevant_entries P i pc [])
[PROOF STEP]
by (simp add: relevant_entries_def shift_def)
[PROOF STATE]
proof (state)
this:
relevant_entries P i (pc + n) (shift n []) = shift n (relevant_entries P i pc [])

goal (1 subgoal):
 1. \<And>a xt. relevant_entries P i (pc + n) (shift n xt) = shift n (relevant_entries P i pc xt) \<Longrightarrow> relevant_entries P i (pc + n) (shift n (a # xt)) = shift n (relevant_entries P i pc (a # xt))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xt. relevant_entries P i (pc + n) (shift n xt) = shift n (relevant_entries P i pc xt) \<Longrightarrow> relevant_entries P i (pc + n) (shift n (a # xt)) = shift n (relevant_entries P i pc (a # xt))
[PROOF STEP]
case (Cons a xt)
[PROOF STATE]
proof (state)
this:
relevant_entries P i (pc + n) (shift n xt) = shift n (relevant_entries P i pc xt)

goal (1 subgoal):
 1. \<And>a xt. relevant_entries P i (pc + n) (shift n xt) = shift n (relevant_entries P i pc xt) \<Longrightarrow> relevant_entries P i (pc + n) (shift n (a # xt)) = shift n (relevant_entries P i pc (a # xt))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
relevant_entries P i (pc + n) (shift n xt) = shift n (relevant_entries P i pc xt)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
relevant_entries P i (pc + n) (shift n xt) = shift n (relevant_entries P i pc xt)

goal (1 subgoal):
 1. relevant_entries P i (pc + n) (shift n (a # xt)) = shift n (relevant_entries P i pc (a # xt))
[PROOF STEP]
by (auto simp add: relevant_entries_def shift_def is_relevant_entry_def)
[PROOF STATE]
proof (state)
this:
relevant_entries P i (pc + n) (shift n (a # xt)) = shift n (relevant_entries P i pc (a # xt))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma [simp]:
  "xcpt_eff i P (pc+n) \<tau> (shift n xt) =
   map (\<lambda>(pc,\<tau>). (pc + n, \<tau>)) (xcpt_eff i P pc \<tau> xt)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xcpt_eff i P (pc + n) \<tau> (shift n xt) = map (\<lambda>(pc, \<tau>). (pc + n, \<tau>)) (xcpt_eff i P pc \<tau> xt)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xcpt_eff i P (pc + n) \<tau> (shift n xt) = map (\<lambda>(pc, \<tau>). (pc + n, \<tau>)) (xcpt_eff i P pc \<tau> xt)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. xcpt_eff i P (pc + n) \<tau> (shift n xt) = map (\<lambda>(pc, \<tau>). (pc + n, \<tau>)) (xcpt_eff i P pc \<tau> xt)
[PROOF STEP]
obtain ST LT where "\<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 (1 subgoal):
 1. xcpt_eff i P (pc + n) \<tau> (shift n xt) = map (\<lambda>(pc, \<tau>). (pc + n, \<tau>)) (xcpt_eff i P pc \<tau> xt)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<tau> = (ST, LT)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<tau> = (ST, LT)

goal (1 subgoal):
 1. xcpt_eff i P (pc + n) \<tau> (shift n xt) = map (\<lambda>(pc, \<tau>). (pc + n, \<tau>)) (xcpt_eff i P pc \<tau> xt)
[PROOF STEP]
by(simp add: xcpt_eff_def) (auto simp add: shift_def)
[PROOF STATE]
proof (state)
this:
xcpt_eff i P (pc + n) \<tau> (shift n xt) = map (\<lambda>(pc, \<tau>). (pc + n, \<tau>)) (xcpt_eff i P pc \<tau> xt)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma  [simp]:
  "app\<^sub>i (i, P, pc, m, T, \<tau>) \<Longrightarrow>
   eff i P (pc+n) (shift n xt) (Some \<tau>) =
   map (\<lambda>(pc,\<tau>). (pc+n,\<tau>)) (eff i P pc xt (Some \<tau>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. app\<^sub>i (i, P, pc, m, T, \<tau>) \<Longrightarrow> eff i P (pc + n) (shift n xt) \<lfloor>\<tau>\<rfloor> = map (\<lambda>(pc, \<tau>). (pc + n, \<tau>)) (eff i P pc xt \<lfloor>\<tau>\<rfloor>)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. app\<^sub>i (i, P, pc, m, T, \<tau>) \<Longrightarrow> eff i P (pc + n) (shift n xt) \<lfloor>\<tau>\<rfloor> = map (\<lambda>(pc, \<tau>). (pc + n, \<tau>)) (eff i P pc xt \<lfloor>\<tau>\<rfloor>)
[PROOF STEP]
by(cases "i") (auto simp add:eff_def norm_eff_def)


[STATEMENT]
lemma [simp]:
  "xcpt_app i P (pc+n) mxs (shift n xt) \<tau> = xcpt_app i P pc mxs xt \<tau>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xcpt_app i P (pc + n) mxs (shift n xt) \<tau> = xcpt_app i P pc mxs xt \<tau>
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xcpt_app i P (pc + n) mxs (shift n xt) \<tau> = xcpt_app i P pc mxs xt \<tau>
[PROOF STEP]
by (simp add: xcpt_app_def) (auto simp add: shift_def)


[STATEMENT]
lemma wt_instr_appL:
assumes "P,T,m,mpc,xt \<turnstile> i,pc :: \<tau>s" and "pc < size \<tau>s" and "mpc \<le> size \<tau>s"
shows "P,T,m,mpc + size \<tau>s',shift (size \<tau>s') xt \<turnstile> i,pc+size \<tau>s' :: \<tau>s'@\<tau>s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P,T,m,mpc + length \<tau>s',shift (length \<tau>s') xt \<turnstile> i,pc + length \<tau>s' :: \<tau>s' @ \<tau>s
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P,T,m,mpc + length \<tau>s',shift (length \<tau>s') xt \<turnstile> i,pc + length \<tau>s' :: \<tau>s' @ \<tau>s
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P,T,m,mpc + length \<tau>s',shift (length \<tau>s') xt \<turnstile> i,pc + length \<tau>s' :: \<tau>s' @ \<tau>s
[PROOF STEP]
let ?t = "(\<tau>s'@\<tau>s)!(pc+size \<tau>s')"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P,T,m,mpc + length \<tau>s',shift (length \<tau>s') xt \<turnstile> i,pc + length \<tau>s' :: \<tau>s' @ \<tau>s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P,T,m,mpc + length \<tau>s',shift (length \<tau>s') xt \<turnstile> i,pc + length \<tau>s' :: \<tau>s' @ \<tau>s
[PROOF STEP]
proof(cases ?t)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<tau>s' @ \<tau>s) ! (pc + length \<tau>s') = None \<Longrightarrow> P,T,m,mpc + length \<tau>s',shift (length \<tau>s') xt \<turnstile> i,pc + length \<tau>s' :: \<tau>s' @ \<tau>s
 2. \<And>a. (\<tau>s' @ \<tau>s) ! (pc + length \<tau>s') = \<lfloor>a\<rfloor> \<Longrightarrow> P,T,m,mpc + length \<tau>s',shift (length \<tau>s') xt \<turnstile> i,pc + length \<tau>s' :: \<tau>s' @ \<tau>s
[PROOF STEP]
case (Some \<tau>)
[PROOF STATE]
proof (state)
this:
(\<tau>s' @ \<tau>s) ! (pc + length \<tau>s') = \<lfloor>\<tau>\<rfloor>

goal (2 subgoals):
 1. (\<tau>s' @ \<tau>s) ! (pc + length \<tau>s') = None \<Longrightarrow> P,T,m,mpc + length \<tau>s',shift (length \<tau>s') xt \<turnstile> i,pc + length \<tau>s' :: \<tau>s' @ \<tau>s
 2. \<And>a. (\<tau>s' @ \<tau>s) ! (pc + length \<tau>s') = \<lfloor>a\<rfloor> \<Longrightarrow> P,T,m,mpc + length \<tau>s',shift (length \<tau>s') xt \<turnstile> i,pc + length \<tau>s' :: \<tau>s' @ \<tau>s
[PROOF STEP]
obtain ST LT where [simp]: "\<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' @ \<tau>s) ! (pc + length \<tau>s') = None \<Longrightarrow> P,T,m,mpc + length \<tau>s',shift (length \<tau>s') xt \<turnstile> i,pc + length \<tau>s' :: \<tau>s' @ \<tau>s
 2. \<And>a. (\<tau>s' @ \<tau>s) ! (pc + length \<tau>s') = \<lfloor>a\<rfloor> \<Longrightarrow> P,T,m,mpc + length \<tau>s',shift (length \<tau>s') xt \<turnstile> i,pc + length \<tau>s' :: \<tau>s' @ \<tau>s
[PROOF STEP]
have "app\<^sub>i (i, P, pc + length \<tau>s', m, T, \<tau>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. app\<^sub>i (i, P, pc + length \<tau>s', m, T, \<tau>)
[PROOF STEP]
using Some assms
[PROOF STATE]
proof (prove)
using this:
(\<tau>s' @ \<tau>s) ! (pc + length \<tau>s') = \<lfloor>\<tau>\<rfloor>
P,T,m,mpc,xt \<turnstile> i,pc :: \<tau>s
pc < length \<tau>s
mpc \<le> length \<tau>s

goal (1 subgoal):
 1. app\<^sub>i (i, P, pc + length \<tau>s', m, T, \<tau>)
[PROOF STEP]
by(cases "i") (auto simp:wt_instr_def app_def)
[PROOF STATE]
proof (state)
this:
app\<^sub>i (i, P, pc + length \<tau>s', m, T, \<tau>)

goal (2 subgoals):
 1. (\<tau>s' @ \<tau>s) ! (pc + length \<tau>s') = None \<Longrightarrow> P,T,m,mpc + length \<tau>s',shift (length \<tau>s') xt \<turnstile> i,pc + length \<tau>s' :: \<tau>s' @ \<tau>s
 2. \<And>a. (\<tau>s' @ \<tau>s) ! (pc + length \<tau>s') = \<lfloor>a\<rfloor> \<Longrightarrow> P,T,m,mpc + length \<tau>s',shift (length \<tau>s') xt \<turnstile> i,pc + length \<tau>s' :: \<tau>s' @ \<tau>s
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
app\<^sub>i (i, P, pc + length \<tau>s', m, T, \<tau>)

goal (2 subgoals):
 1. (\<tau>s' @ \<tau>s) ! (pc + length \<tau>s') = None \<Longrightarrow> P,T,m,mpc + length \<tau>s',shift (length \<tau>s') xt \<turnstile> i,pc + length \<tau>s' :: \<tau>s' @ \<tau>s
 2. \<And>a. (\<tau>s' @ \<tau>s) ! (pc + length \<tau>s') = \<lfloor>a\<rfloor> \<Longrightarrow> P,T,m,mpc + length \<tau>s',shift (length \<tau>s') xt \<turnstile> i,pc + length \<tau>s' :: \<tau>s' @ \<tau>s
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
app\<^sub>i (i, P, pc + length \<tau>s', m, T, \<tau>)

goal (2 subgoals):
 1. (\<tau>s' @ \<tau>s) ! (pc + length \<tau>s') = None \<Longrightarrow> P,T,m,mpc + length \<tau>s',shift (length \<tau>s') xt \<turnstile> i,pc + length \<tau>s' :: \<tau>s' @ \<tau>s
 2. \<And>a. (\<tau>s' @ \<tau>s) ! (pc + length \<tau>s') = \<lfloor>a\<rfloor> \<Longrightarrow> P,T,m,mpc + length \<tau>s',shift (length \<tau>s') xt \<turnstile> i,pc + length \<tau>s' :: \<tau>s' @ \<tau>s
[PROOF STEP]
fix pc' \<tau>'
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<tau>s' @ \<tau>s) ! (pc + length \<tau>s') = None \<Longrightarrow> P,T,m,mpc + length \<tau>s',shift (length \<tau>s') xt \<turnstile> i,pc + length \<tau>s' :: \<tau>s' @ \<tau>s
 2. \<And>a. (\<tau>s' @ \<tau>s) ! (pc + length \<tau>s') = \<lfloor>a\<rfloor> \<Longrightarrow> P,T,m,mpc + length \<tau>s',shift (length \<tau>s') xt \<turnstile> i,pc + length \<tau>s' :: \<tau>s' @ \<tau>s
[PROOF STEP]
assume "(pc',\<tau>') \<in> set (eff i P pc xt ?t)"
[PROOF STATE]
proof (state)
this:
(pc', \<tau>') \<in> set (eff i P pc xt ((\<tau>s' @ \<tau>s) ! (pc + length \<tau>s')))

goal (2 subgoals):
 1. (\<tau>s' @ \<tau>s) ! (pc + length \<tau>s') = None \<Longrightarrow> P,T,m,mpc + length \<tau>s',shift (length \<tau>s') xt \<turnstile> i,pc + length \<tau>s' :: \<tau>s' @ \<tau>s
 2. \<And>a. (\<tau>s' @ \<tau>s) ! (pc + length \<tau>s') = \<lfloor>a\<rfloor> \<Longrightarrow> P,T,m,mpc + length \<tau>s',shift (length \<tau>s') xt \<turnstile> i,pc + length \<tau>s' :: \<tau>s' @ \<tau>s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(pc', \<tau>') \<in> set (eff i P pc xt ((\<tau>s' @ \<tau>s) ! (pc + length \<tau>s')))
[PROOF STEP]
have "P \<turnstile> \<tau>' \<le>' \<tau>s!pc'" and "pc' < mpc"
[PROOF STATE]
proof (prove)
using this:
(pc', \<tau>') \<in> set (eff i P pc xt ((\<tau>s' @ \<tau>s) ! (pc + length \<tau>s')))

goal (1 subgoal):
 1. P \<turnstile> \<tau>' \<le>' \<tau>s ! pc' &&& pc' < mpc
[PROOF STEP]
using Some assms
[PROOF STATE]
proof (prove)
using this:
(pc', \<tau>') \<in> set (eff i P pc xt ((\<tau>s' @ \<tau>s) ! (pc + length \<tau>s')))
(\<tau>s' @ \<tau>s) ! (pc + length \<tau>s') = \<lfloor>\<tau>\<rfloor>
P,T,m,mpc,xt \<turnstile> i,pc :: \<tau>s
pc < length \<tau>s
mpc \<le> length \<tau>s

goal (1 subgoal):
 1. P \<turnstile> \<tau>' \<le>' \<tau>s ! pc' &&& pc' < mpc
[PROOF STEP]
by(auto simp:wt_instr_def app_def)
[PROOF STATE]
proof (state)
this:
P \<turnstile> \<tau>' \<le>' \<tau>s ! pc'
pc' < mpc

goal (2 subgoals):
 1. (\<tau>s' @ \<tau>s) ! (pc + length \<tau>s') = None \<Longrightarrow> P,T,m,mpc + length \<tau>s',shift (length \<tau>s') xt \<turnstile> i,pc + length \<tau>s' :: \<tau>s' @ \<tau>s
 2. \<And>a. (\<tau>s' @ \<tau>s) ! (pc + length \<tau>s') = \<lfloor>a\<rfloor> \<Longrightarrow> P,T,m,mpc + length \<tau>s',shift (length \<tau>s') xt \<turnstile> i,pc + length \<tau>s' :: \<tau>s' @ \<tau>s
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(?pc'2, ?\<tau>'2) \<in> set (eff i P pc xt ((\<tau>s' @ \<tau>s) ! (pc + length \<tau>s'))) \<Longrightarrow> P \<turnstile> ?\<tau>'2 \<le>' \<tau>s ! ?pc'2
(?pc'2, ?\<tau>'2) \<in> set (eff i P pc xt ((\<tau>s' @ \<tau>s) ! (pc + length \<tau>s'))) \<Longrightarrow> ?pc'2 < mpc

goal (2 subgoals):
 1. (\<tau>s' @ \<tau>s) ! (pc + length \<tau>s') = None \<Longrightarrow> P,T,m,mpc + length \<tau>s',shift (length \<tau>s') xt \<turnstile> i,pc + length \<tau>s' :: \<tau>s' @ \<tau>s
 2. \<And>a. (\<tau>s' @ \<tau>s) ! (pc + length \<tau>s') = \<lfloor>a\<rfloor> \<Longrightarrow> P,T,m,mpc + length \<tau>s',shift (length \<tau>s') xt \<turnstile> i,pc + length \<tau>s' :: \<tau>s' @ \<tau>s
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
app\<^sub>i (i, P, pc + length \<tau>s', m, T, \<tau>)
(?pc'2, ?\<tau>'2) \<in> set (eff i P pc xt ((\<tau>s' @ \<tau>s) ! (pc + length \<tau>s'))) \<Longrightarrow> P \<turnstile> ?\<tau>'2 \<le>' \<tau>s ! ?pc'2
(?pc'2, ?\<tau>'2) \<in> set (eff i P pc xt ((\<tau>s' @ \<tau>s) ! (pc + length \<tau>s'))) \<Longrightarrow> ?pc'2 < mpc
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
app\<^sub>i (i, P, pc + length \<tau>s', m, T, \<tau>)
(?pc'2, ?\<tau>'2) \<in> set (eff i P pc xt ((\<tau>s' @ \<tau>s) ! (pc + length \<tau>s'))) \<Longrightarrow> P \<turnstile> ?\<tau>'2 \<le>' \<tau>s ! ?pc'2
(?pc'2, ?\<tau>'2) \<in> set (eff i P pc xt ((\<tau>s' @ \<tau>s) ! (pc + length \<tau>s'))) \<Longrightarrow> ?pc'2 < mpc

goal (1 subgoal):
 1. P,T,m,mpc + length \<tau>s',shift (length \<tau>s') xt \<turnstile> i,pc + length \<tau>s' :: \<tau>s' @ \<tau>s
[PROOF STEP]
using Some assms
[PROOF STATE]
proof (prove)
using this:
app\<^sub>i (i, P, pc + length \<tau>s', m, T, \<tau>)
(?pc'2, ?\<tau>'2) \<in> set (eff i P pc xt ((\<tau>s' @ \<tau>s) ! (pc + length \<tau>s'))) \<Longrightarrow> P \<turnstile> ?\<tau>'2 \<le>' \<tau>s ! ?pc'2
(?pc'2, ?\<tau>'2) \<in> set (eff i P pc xt ((\<tau>s' @ \<tau>s) ! (pc + length \<tau>s'))) \<Longrightarrow> ?pc'2 < mpc
(\<tau>s' @ \<tau>s) ! (pc + length \<tau>s') = \<lfloor>\<tau>\<rfloor>
P,T,m,mpc,xt \<turnstile> i,pc :: \<tau>s
pc < length \<tau>s
mpc \<le> length \<tau>s

goal (1 subgoal):
 1. P,T,m,mpc + length \<tau>s',shift (length \<tau>s') xt \<turnstile> i,pc + length \<tau>s' :: \<tau>s' @ \<tau>s
[PROOF STEP]
by(fastforce simp:wt_instr_def app_def)
[PROOF STATE]
proof (state)
this:
P,T,m,mpc + length \<tau>s',shift (length \<tau>s') xt \<turnstile> i,pc + length \<tau>s' :: \<tau>s' @ \<tau>s

goal (1 subgoal):
 1. (\<tau>s' @ \<tau>s) ! (pc + length \<tau>s') = None \<Longrightarrow> P,T,m,mpc + length \<tau>s',shift (length \<tau>s') xt \<turnstile> i,pc + length \<tau>s' :: \<tau>s' @ \<tau>s
[PROOF STEP]
qed (auto simp:wt_instr_def app_def)
[PROOF STATE]
proof (state)
this:
P,T,m,mpc + length \<tau>s',shift (length \<tau>s') xt \<turnstile> i,pc + length \<tau>s' :: \<tau>s' @ \<tau>s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wt_instr_Cons:
assumes wti: "P,T,m,mpc - 1,[] \<turnstile> i,pc - 1 :: \<tau>s"
  and pcl: "0 < pc" and mpcl: "0 < mpc"
  and pcu: "pc < size \<tau>s + 1" and mpcu: "mpc \<le> size \<tau>s + 1"
shows "P,T,m,mpc,[] \<turnstile> i,pc :: \<tau>#\<tau>s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P,T,m,mpc,[] \<turnstile> i,pc :: \<tau> # \<tau>s
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P,T,m,mpc,[] \<turnstile> i,pc :: \<tau> # \<tau>s
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P,T,m,mpc,[] \<turnstile> i,pc :: \<tau> # \<tau>s
[PROOF STEP]
have "pc - 1 < length \<tau>s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pc - 1 < length \<tau>s
[PROOF STEP]
using pcl pcu
[PROOF STATE]
proof (prove)
using this:
0 < pc
pc < length \<tau>s + 1

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

goal (1 subgoal):
 1. P,T,m,mpc,[] \<turnstile> i,pc :: \<tau> # \<tau>s
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
pc - 1 < length \<tau>s

goal (1 subgoal):
 1. P,T,m,mpc,[] \<turnstile> i,pc :: \<tau> # \<tau>s
[PROOF STEP]
have "mpc - 1 \<le> length \<tau>s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mpc - 1 \<le> length \<tau>s
[PROOF STEP]
using mpcl mpcu
[PROOF STATE]
proof (prove)
using this:
0 < mpc
mpc \<le> length \<tau>s + 1

goal (1 subgoal):
 1. mpc - 1 \<le> length \<tau>s
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
mpc - 1 \<le> length \<tau>s

goal (1 subgoal):
 1. P,T,m,mpc,[] \<turnstile> i,pc :: \<tau> # \<tau>s
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
pc - 1 < length \<tau>s
mpc - 1 \<le> length \<tau>s
[PROOF STEP]
have
    "P,T,m,mpc - 1 + length [\<tau>],shift (length [\<tau>]) [] \<turnstile> i,pc - 1 + length [\<tau>] :: [\<tau>] @ \<tau>s"
[PROOF STATE]
proof (prove)
using this:
pc - 1 < length \<tau>s
mpc - 1 \<le> length \<tau>s

goal (1 subgoal):
 1. P,T,m,mpc - 1 + length [\<tau>],shift (length [\<tau>]) [] \<turnstile> i,pc - 1 + length [\<tau>] :: [\<tau>] @ \<tau>s
[PROOF STEP]
by(rule wt_instr_appL[where \<tau>s' = "[\<tau>]", OF wti])
[PROOF STATE]
proof (state)
this:
P,T,m,mpc - 1 + length [\<tau>],shift (length [\<tau>]) [] \<turnstile> i,pc - 1 + length [\<tau>] :: [\<tau>] @ \<tau>s

goal (1 subgoal):
 1. P,T,m,mpc,[] \<turnstile> i,pc :: \<tau> # \<tau>s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
P,T,m,mpc - 1 + length [\<tau>],shift (length [\<tau>]) [] \<turnstile> i,pc - 1 + length [\<tau>] :: [\<tau>] @ \<tau>s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
P,T,m,mpc - 1 + length [\<tau>],shift (length [\<tau>]) [] \<turnstile> i,pc - 1 + length [\<tau>] :: [\<tau>] @ \<tau>s

goal (1 subgoal):
 1. P,T,m,mpc,[] \<turnstile> i,pc :: \<tau> # \<tau>s
[PROOF STEP]
using pcl mpcl
[PROOF STATE]
proof (prove)
using this:
P,T,m,mpc - 1 + length [\<tau>],shift (length [\<tau>]) [] \<turnstile> i,pc - 1 + length [\<tau>] :: [\<tau>] @ \<tau>s
0 < pc
0 < mpc

goal (1 subgoal):
 1. P,T,m,mpc,[] \<turnstile> i,pc :: \<tau> # \<tau>s
[PROOF STEP]
by (simp split:nat_diff_split_asm)
[PROOF STATE]
proof (state)
this:
P,T,m,mpc,[] \<turnstile> i,pc :: \<tau> # \<tau>s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wt_instr_append:
assumes wti: "P,T,m,mpc - size \<tau>s',[] \<turnstile> i,pc - size \<tau>s' :: \<tau>s"
  and pcl: "size \<tau>s' \<le> pc" and mpcl: "size \<tau>s' \<le> mpc"
  and pcu: "pc < size \<tau>s + size \<tau>s'" and mpcu: "mpc \<le> size \<tau>s + size \<tau>s'"
shows "P,T,m,mpc,[] \<turnstile> i,pc :: \<tau>s'@\<tau>s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P,T,m,mpc,[] \<turnstile> i,pc :: \<tau>s' @ \<tau>s
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P,T,m,mpc,[] \<turnstile> i,pc :: \<tau>s' @ \<tau>s
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P,T,m,mpc,[] \<turnstile> i,pc :: \<tau>s' @ \<tau>s
[PROOF STEP]
have "pc - length \<tau>s' < length \<tau>s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pc - length \<tau>s' < length \<tau>s
[PROOF STEP]
using pcl pcu
[PROOF STATE]
proof (prove)
using this:
length \<tau>s' \<le> pc
pc < length \<tau>s + length \<tau>s'

goal (1 subgoal):
 1. pc - length \<tau>s' < length \<tau>s
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
pc - length \<tau>s' < length \<tau>s

goal (1 subgoal):
 1. P,T,m,mpc,[] \<turnstile> i,pc :: \<tau>s' @ \<tau>s
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
pc - length \<tau>s' < length \<tau>s

goal (1 subgoal):
 1. P,T,m,mpc,[] \<turnstile> i,pc :: \<tau>s' @ \<tau>s
[PROOF STEP]
have "mpc - length \<tau>s' \<le> length \<tau>s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mpc - length \<tau>s' \<le> length \<tau>s
[PROOF STEP]
using mpcl mpcu
[PROOF STATE]
proof (prove)
using this:
length \<tau>s' \<le> mpc
mpc \<le> length \<tau>s + length \<tau>s'

goal (1 subgoal):
 1. mpc - length \<tau>s' \<le> length \<tau>s
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
mpc - length \<tau>s' \<le> length \<tau>s

goal (1 subgoal):
 1. P,T,m,mpc,[] \<turnstile> i,pc :: \<tau>s' @ \<tau>s
[PROOF STEP]
thm wt_instr_appL[where \<tau>s' = "\<tau>s'", OF wti]
[PROOF STATE]
proof (state)
this:
mpc - length \<tau>s' \<le> length \<tau>s

goal (1 subgoal):
 1. P,T,m,mpc,[] \<turnstile> i,pc :: \<tau>s' @ \<tau>s
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
pc - length \<tau>s' < length \<tau>s
mpc - length \<tau>s' \<le> length \<tau>s
[PROOF STEP]
have "P,T,m,mpc - length \<tau>s' + length \<tau>s',shift (length \<tau>s') []
                     \<turnstile> i,pc - length \<tau>s' + length \<tau>s' :: \<tau>s' @ \<tau>s"
[PROOF STATE]
proof (prove)
using this:
pc - length \<tau>s' < length \<tau>s
mpc - length \<tau>s' \<le> length \<tau>s

goal (1 subgoal):
 1. P,T,m,mpc - length \<tau>s' + length \<tau>s',shift (length \<tau>s') [] \<turnstile> i,pc - length \<tau>s' + length \<tau>s' :: \<tau>s' @ \<tau>s
[PROOF STEP]
by(rule wt_instr_appL[where \<tau>s' = "\<tau>s'", OF wti])
[PROOF STATE]
proof (state)
this:
P,T,m,mpc - length \<tau>s' + length \<tau>s',shift (length \<tau>s') [] \<turnstile> i,pc - length \<tau>s' + length \<tau>s' :: \<tau>s' @ \<tau>s

goal (1 subgoal):
 1. P,T,m,mpc,[] \<turnstile> i,pc :: \<tau>s' @ \<tau>s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
P,T,m,mpc - length \<tau>s' + length \<tau>s',shift (length \<tau>s') [] \<turnstile> i,pc - length \<tau>s' + length \<tau>s' :: \<tau>s' @ \<tau>s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
P,T,m,mpc - length \<tau>s' + length \<tau>s',shift (length \<tau>s') [] \<turnstile> i,pc - length \<tau>s' + length \<tau>s' :: \<tau>s' @ \<tau>s

goal (1 subgoal):
 1. P,T,m,mpc,[] \<turnstile> i,pc :: \<tau>s' @ \<tau>s
[PROOF STEP]
using pcl mpcl
[PROOF STATE]
proof (prove)
using this:
P,T,m,mpc - length \<tau>s' + length \<tau>s',shift (length \<tau>s') [] \<turnstile> i,pc - length \<tau>s' + length \<tau>s' :: \<tau>s' @ \<tau>s
length \<tau>s' \<le> pc
length \<tau>s' \<le> mpc

goal (1 subgoal):
 1. P,T,m,mpc,[] \<turnstile> i,pc :: \<tau>s' @ \<tau>s
[PROOF STEP]
by (simp split:nat_diff_split_asm)
[PROOF STATE]
proof (state)
this:
P,T,m,mpc,[] \<turnstile> i,pc :: \<tau>s' @ \<tau>s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma xcpt_app_pcs:
  "pc \<notin> pcs xt \<Longrightarrow> xcpt_app i P pc mxs xt \<tau>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pc \<notin> pcs xt \<Longrightarrow> xcpt_app i P pc mxs xt \<tau>
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pc \<notin> pcs xt \<Longrightarrow> xcpt_app i P pc mxs xt \<tau>
[PROOF STEP]
by (auto simp add: xcpt_app_def relevant_entries_def is_relevant_entry_def pcs_def)


[STATEMENT]
lemma xcpt_eff_pcs:
  "pc \<notin> pcs xt \<Longrightarrow> xcpt_eff i P pc \<tau> xt = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pc \<notin> pcs xt \<Longrightarrow> xcpt_eff i P pc \<tau> xt = []
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pc \<notin> pcs xt \<Longrightarrow> xcpt_eff i P pc \<tau> xt = []
[PROOF STEP]
by (cases \<tau>)
   (auto simp add: is_relevant_entry_def xcpt_eff_def relevant_entries_def pcs_def
           intro!: filter_False)


[STATEMENT]
lemma pcs_shift:
  "pc < n \<Longrightarrow> pc \<notin> pcs (shift n xt)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pc < n \<Longrightarrow> pc \<notin> pcs (shift n xt)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pc < n \<Longrightarrow> pc \<notin> pcs (shift n xt)
[PROOF STEP]
by (auto simp add: shift_def pcs_def)


[STATEMENT]
lemma wt_instr_appRx:
  "\<lbrakk> P,T,m,mpc,xt \<turnstile> is!pc,pc :: \<tau>s; pc < size is; size is < size \<tau>s; mpc \<le> size \<tau>s \<rbrakk>
  \<Longrightarrow> P,T,m,mpc,xt @ shift (size is) xt' \<turnstile> is!pc,pc :: \<tau>s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P,T,m,mpc,xt \<turnstile> is ! pc,pc :: \<tau>s; pc < length is; length is < length \<tau>s; mpc \<le> length \<tau>s\<rbrakk> \<Longrightarrow> P,T,m,mpc,xt @ shift (length is) xt' \<turnstile> is ! pc,pc :: \<tau>s
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P,T,m,mpc,xt \<turnstile> is ! pc,pc :: \<tau>s; pc < length is; length is < length \<tau>s; mpc \<le> length \<tau>s\<rbrakk> \<Longrightarrow> P,T,m,mpc,xt @ shift (length is) xt' \<turnstile> is ! pc,pc :: \<tau>s
[PROOF STEP]
by (auto simp:wt_instr_def eff_def app_def xcpt_app_pcs xcpt_eff_pcs)


[STATEMENT]
lemma wt_instr_appLx:
  "\<lbrakk> P,T,m,mpc,xt \<turnstile> i,pc :: \<tau>s; pc \<notin> pcs xt' \<rbrakk>
  \<Longrightarrow> P,T,m,mpc,xt'@xt \<turnstile> i,pc :: \<tau>s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P,T,m,mpc,xt \<turnstile> i,pc :: \<tau>s; pc \<notin> pcs xt'\<rbrakk> \<Longrightarrow> P,T,m,mpc,xt' @ xt \<turnstile> i,pc :: \<tau>s
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P,T,m,mpc,xt \<turnstile> i,pc :: \<tau>s; pc \<notin> pcs xt'\<rbrakk> \<Longrightarrow> P,T,m,mpc,xt' @ xt \<turnstile> i,pc :: \<tau>s
[PROOF STEP]
by (auto simp:wt_instr_def app_def eff_def xcpt_app_pcs xcpt_eff_pcs)


[STATEMENT]
lemma (in TC2) wt_instrs_extR:
  "\<turnstile> is,xt [::] \<tau>s \<Longrightarrow> \<turnstile> is,xt [::] \<tau>s @ \<tau>s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> is, xt [::] \<tau>s \<Longrightarrow> \<turnstile> is, xt [::] \<tau>s @ \<tau>s'
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> is, xt [::] \<tau>s \<Longrightarrow> \<turnstile> is, xt [::] \<tau>s @ \<tau>s'
[PROOF STEP]
by(auto simp add:wt_instrs_def wt_instr_appR)


[STATEMENT]
lemma (in TC2) wt_instrs_ext:
assumes wt\<^sub>1: "\<turnstile> is\<^sub>1,xt\<^sub>1 [::] \<tau>s\<^sub>1@\<tau>s\<^sub>2" and wt\<^sub>2: "\<turnstile> is\<^sub>2,xt\<^sub>2 [::] \<tau>s\<^sub>2"
  and \<tau>s_size: "size \<tau>s\<^sub>1 = size is\<^sub>1"
 shows "\<turnstile> is\<^sub>1@is\<^sub>2, xt\<^sub>1 @ shift (size is\<^sub>1) xt\<^sub>2 [::] \<tau>s\<^sub>1@\<tau>s\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> is\<^sub>1 @ is\<^sub>2, xt\<^sub>1 @ shift (length is\<^sub>1) xt\<^sub>2 [::] \<tau>s\<^sub>1 @ \<tau>s\<^sub>2
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> is\<^sub>1 @ is\<^sub>2, xt\<^sub>1 @ shift (length is\<^sub>1) xt\<^sub>2 [::] \<tau>s\<^sub>1 @ \<tau>s\<^sub>2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<turnstile> is\<^sub>1 @ is\<^sub>2, xt\<^sub>1 @ shift (length is\<^sub>1) xt\<^sub>2 [::] \<tau>s\<^sub>1 @ \<tau>s\<^sub>2
[PROOF STEP]
let ?is = "is\<^sub>1@is\<^sub>2" and ?xt = "xt\<^sub>1 @ shift (size is\<^sub>1) xt\<^sub>2"
    and ?\<tau>s = "\<tau>s\<^sub>1@\<tau>s\<^sub>2"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<turnstile> is\<^sub>1 @ is\<^sub>2, xt\<^sub>1 @ shift (length is\<^sub>1) xt\<^sub>2 [::] \<tau>s\<^sub>1 @ \<tau>s\<^sub>2
[PROOF STEP]
have "size ?is < size ?\<tau>s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (is\<^sub>1 @ is\<^sub>2) < length (\<tau>s\<^sub>1 @ \<tau>s\<^sub>2)
[PROOF STEP]
using wt\<^sub>2 \<tau>s_size
[PROOF STATE]
proof (prove)
using this:
\<turnstile> is\<^sub>2, xt\<^sub>2 [::] \<tau>s\<^sub>2
length \<tau>s\<^sub>1 = length is\<^sub>1

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

goal (1 subgoal):
 1. \<turnstile> is\<^sub>1 @ is\<^sub>2, xt\<^sub>1 @ shift (length is\<^sub>1) xt\<^sub>2 [::] \<tau>s\<^sub>1 @ \<tau>s\<^sub>2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
length (is\<^sub>1 @ is\<^sub>2) < length (\<tau>s\<^sub>1 @ \<tau>s\<^sub>2)

goal (1 subgoal):
 1. \<turnstile> is\<^sub>1 @ is\<^sub>2, xt\<^sub>1 @ shift (length is\<^sub>1) xt\<^sub>2 [::] \<tau>s\<^sub>1 @ \<tau>s\<^sub>2
[PROOF STEP]
have "pcs ?xt \<subseteq> {0..<size ?is}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pcs (xt\<^sub>1 @ shift (length is\<^sub>1) xt\<^sub>2) \<subseteq> {0..<length (is\<^sub>1 @ is\<^sub>2)}
[PROOF STEP]
using wt\<^sub>1 wt\<^sub>2
[PROOF STATE]
proof (prove)
using this:
\<turnstile> is\<^sub>1, xt\<^sub>1 [::] \<tau>s\<^sub>1 @ \<tau>s\<^sub>2
\<turnstile> is\<^sub>2, xt\<^sub>2 [::] \<tau>s\<^sub>2

goal (1 subgoal):
 1. pcs (xt\<^sub>1 @ shift (length is\<^sub>1) xt\<^sub>2) \<subseteq> {0..<length (is\<^sub>1 @ is\<^sub>2)}
[PROOF STEP]
by(fastforce simp:wt_instrs_def)
[PROOF STATE]
proof (state)
this:
pcs (xt\<^sub>1 @ shift (length is\<^sub>1) xt\<^sub>2) \<subseteq> {0..<length (is\<^sub>1 @ is\<^sub>2)}

goal (1 subgoal):
 1. \<turnstile> is\<^sub>1 @ is\<^sub>2, xt\<^sub>1 @ shift (length is\<^sub>1) xt\<^sub>2 [::] \<tau>s\<^sub>1 @ \<tau>s\<^sub>2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
pcs (xt\<^sub>1 @ shift (length is\<^sub>1) xt\<^sub>2) \<subseteq> {0..<length (is\<^sub>1 @ is\<^sub>2)}

goal (1 subgoal):
 1. \<turnstile> is\<^sub>1 @ is\<^sub>2, xt\<^sub>1 @ shift (length is\<^sub>1) xt\<^sub>2 [::] \<tau>s\<^sub>1 @ \<tau>s\<^sub>2
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
pcs (xt\<^sub>1 @ shift (length is\<^sub>1) xt\<^sub>2) \<subseteq> {0..<length (is\<^sub>1 @ is\<^sub>2)}

goal (1 subgoal):
 1. \<turnstile> is\<^sub>1 @ is\<^sub>2, xt\<^sub>1 @ shift (length is\<^sub>1) xt\<^sub>2 [::] \<tau>s\<^sub>1 @ \<tau>s\<^sub>2
[PROOF STEP]
fix pc
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<turnstile> is\<^sub>1 @ is\<^sub>2, xt\<^sub>1 @ shift (length is\<^sub>1) xt\<^sub>2 [::] \<tau>s\<^sub>1 @ \<tau>s\<^sub>2
[PROOF STEP]
assume pc: "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\<^sub>1 @ shift (length is\<^sub>1) xt\<^sub>2 [::] \<tau>s\<^sub>1 @ \<tau>s\<^sub>2
[PROOF STEP]
have "P,T\<^sub>r,mxs,size ?\<tau>s,?xt \<turnstile> ?is!pc,pc :: ?\<tau>s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P,T\<^sub>r,mxs,length (\<tau>s\<^sub>1 @ \<tau>s\<^sub>2),xt\<^sub>1 @ shift (length is\<^sub>1) xt\<^sub>2 \<turnstile> (is\<^sub>1 @ is\<^sub>2) ! pc,pc :: \<tau>s\<^sub>1 @ \<tau>s\<^sub>2
[PROOF STEP]
proof(cases "pc < length is\<^sub>1")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. pc < length is\<^sub>1 \<Longrightarrow> P,T\<^sub>r,mxs,length (\<tau>s\<^sub>1 @ \<tau>s\<^sub>2),xt\<^sub>1 @ shift (length is\<^sub>1) xt\<^sub>2 \<turnstile> (is\<^sub>1 @ is\<^sub>2) ! pc,pc :: \<tau>s\<^sub>1 @ \<tau>s\<^sub>2
 2. \<not> pc < length is\<^sub>1 \<Longrightarrow> P,T\<^sub>r,mxs,length (\<tau>s\<^sub>1 @ \<tau>s\<^sub>2),xt\<^sub>1 @ shift (length is\<^sub>1) xt\<^sub>2 \<turnstile> (is\<^sub>1 @ is\<^sub>2) ! pc,pc :: \<tau>s\<^sub>1 @ \<tau>s\<^sub>2
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
pc < length is\<^sub>1

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

goal (1 subgoal):
 1. P,T\<^sub>r,mxs,length (\<tau>s\<^sub>1 @ \<tau>s\<^sub>2),xt\<^sub>1 @ shift (length is\<^sub>1) xt\<^sub>2 \<turnstile> (is\<^sub>1 @ is\<^sub>2) ! pc,pc :: \<tau>s\<^sub>1 @ \<tau>s\<^sub>2
[PROOF STEP]
using wt\<^sub>1 pc
[PROOF STATE]
proof (prove)
using this:
pc < length is\<^sub>1
\<turnstile> is\<^sub>1, xt\<^sub>1 [::] \<tau>s\<^sub>1 @ \<tau>s\<^sub>2
pc < length (is\<^sub>1 @ is\<^sub>2)

goal (1 subgoal):
 1. P,T\<^sub>r,mxs,length (\<tau>s\<^sub>1 @ \<tau>s\<^sub>2),xt\<^sub>1 @ shift (length is\<^sub>1) xt\<^sub>2 \<turnstile> (is\<^sub>1 @ is\<^sub>2) ! pc,pc :: \<tau>s\<^sub>1 @ \<tau>s\<^sub>2
[PROOF STEP]
by(fastforce simp: wt_instrs_def wt_instr_appRx)
[PROOF STATE]
proof (state)
this:
P,T\<^sub>r,mxs,length (\<tau>s\<^sub>1 @ \<tau>s\<^sub>2),xt\<^sub>1 @ shift (length is\<^sub>1) xt\<^sub>2 \<turnstile> (is\<^sub>1 @ is\<^sub>2) ! pc,pc :: \<tau>s\<^sub>1 @ \<tau>s\<^sub>2

goal (1 subgoal):
 1. \<not> pc < length is\<^sub>1 \<Longrightarrow> P,T\<^sub>r,mxs,length (\<tau>s\<^sub>1 @ \<tau>s\<^sub>2),xt\<^sub>1 @ shift (length is\<^sub>1) xt\<^sub>2 \<turnstile> (is\<^sub>1 @ is\<^sub>2) ! pc,pc :: \<tau>s\<^sub>1 @ \<tau>s\<^sub>2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> pc < length is\<^sub>1 \<Longrightarrow> P,T\<^sub>r,mxs,length (\<tau>s\<^sub>1 @ \<tau>s\<^sub>2),xt\<^sub>1 @ shift (length is\<^sub>1) xt\<^sub>2 \<turnstile> (is\<^sub>1 @ is\<^sub>2) ! pc,pc :: \<tau>s\<^sub>1 @ \<tau>s\<^sub>2
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> pc < length is\<^sub>1

goal (1 subgoal):
 1. \<not> pc < length is\<^sub>1 \<Longrightarrow> P,T\<^sub>r,mxs,length (\<tau>s\<^sub>1 @ \<tau>s\<^sub>2),xt\<^sub>1 @ shift (length is\<^sub>1) xt\<^sub>2 \<turnstile> (is\<^sub>1 @ is\<^sub>2) ! pc,pc :: \<tau>s\<^sub>1 @ \<tau>s\<^sub>2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> pc < length is\<^sub>1
[PROOF STEP]
have "pc - length is\<^sub>1 < length is\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
\<not> pc < length is\<^sub>1

goal (1 subgoal):
 1. pc - length is\<^sub>1 < length is\<^sub>2
[PROOF STEP]
using pc
[PROOF STATE]
proof (prove)
using this:
\<not> pc < length is\<^sub>1
pc < length (is\<^sub>1 @ is\<^sub>2)

goal (1 subgoal):
 1. pc - length is\<^sub>1 < length is\<^sub>2
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
pc - length is\<^sub>1 < length is\<^sub>2

goal (1 subgoal):
 1. \<not> pc < length is\<^sub>1 \<Longrightarrow> P,T\<^sub>r,mxs,length (\<tau>s\<^sub>1 @ \<tau>s\<^sub>2),xt\<^sub>1 @ shift (length is\<^sub>1) xt\<^sub>2 \<turnstile> (is\<^sub>1 @ is\<^sub>2) ! pc,pc :: \<tau>s\<^sub>1 @ \<tau>s\<^sub>2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pc - length is\<^sub>1 < length is\<^sub>2
[PROOF STEP]
have "P,T\<^sub>r,mxs,length \<tau>s\<^sub>2,xt\<^sub>2 \<turnstile> is\<^sub>2 ! (pc - length is\<^sub>1),pc - length is\<^sub>1 :: \<tau>s\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
pc - length is\<^sub>1 < length is\<^sub>2

goal (1 subgoal):
 1. P,T\<^sub>r,mxs,length \<tau>s\<^sub>2,xt\<^sub>2 \<turnstile> is\<^sub>2 ! (pc - length is\<^sub>1),pc - length is\<^sub>1 :: \<tau>s\<^sub>2
[PROOF STEP]
using wt\<^sub>2
[PROOF STATE]
proof (prove)
using this:
pc - length is\<^sub>1 < length is\<^sub>2
\<turnstile> is\<^sub>2, xt\<^sub>2 [::] \<tau>s\<^sub>2

goal (1 subgoal):
 1. P,T\<^sub>r,mxs,length \<tau>s\<^sub>2,xt\<^sub>2 \<turnstile> is\<^sub>2 ! (pc - length is\<^sub>1),pc - length is\<^sub>1 :: \<tau>s\<^sub>2
[PROOF STEP]
by(clarsimp simp: wt_instrs_def)
[PROOF STATE]
proof (state)
this:
P,T\<^sub>r,mxs,length \<tau>s\<^sub>2,xt\<^sub>2 \<turnstile> is\<^sub>2 ! (pc - length is\<^sub>1),pc - length is\<^sub>1 :: \<tau>s\<^sub>2

goal (1 subgoal):
 1. \<not> pc < length is\<^sub>1 \<Longrightarrow> P,T\<^sub>r,mxs,length (\<tau>s\<^sub>1 @ \<tau>s\<^sub>2),xt\<^sub>1 @ shift (length is\<^sub>1) xt\<^sub>2 \<turnstile> (is\<^sub>1 @ is\<^sub>2) ! pc,pc :: \<tau>s\<^sub>1 @ \<tau>s\<^sub>2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P,T\<^sub>r,mxs,length \<tau>s\<^sub>2,xt\<^sub>2 \<turnstile> is\<^sub>2 ! (pc - length is\<^sub>1),pc - length is\<^sub>1 :: \<tau>s\<^sub>2

goal (1 subgoal):
 1. \<not> pc < length is\<^sub>1 \<Longrightarrow> P,T\<^sub>r,mxs,length (\<tau>s\<^sub>1 @ \<tau>s\<^sub>2),xt\<^sub>1 @ shift (length is\<^sub>1) xt\<^sub>2 \<turnstile> (is\<^sub>1 @ is\<^sub>2) ! pc,pc :: \<tau>s\<^sub>1 @ \<tau>s\<^sub>2
[PROOF STEP]
have "pc - length is\<^sub>1 < length \<tau>s\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pc - length is\<^sub>1 < length \<tau>s\<^sub>2
[PROOF STEP]
using pc wt\<^sub>2
[PROOF STATE]
proof (prove)
using this:
pc < length (is\<^sub>1 @ is\<^sub>2)
\<turnstile> is\<^sub>2, xt\<^sub>2 [::] \<tau>s\<^sub>2

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

goal (1 subgoal):
 1. \<not> pc < length is\<^sub>1 \<Longrightarrow> P,T\<^sub>r,mxs,length (\<tau>s\<^sub>1 @ \<tau>s\<^sub>2),xt\<^sub>1 @ shift (length is\<^sub>1) xt\<^sub>2 \<turnstile> (is\<^sub>1 @ is\<^sub>2) ! pc,pc :: \<tau>s\<^sub>1 @ \<tau>s\<^sub>2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
pc - length is\<^sub>1 < length \<tau>s\<^sub>2

goal (1 subgoal):
 1. \<not> pc < length is\<^sub>1 \<Longrightarrow> P,T\<^sub>r,mxs,length (\<tau>s\<^sub>1 @ \<tau>s\<^sub>2),xt\<^sub>1 @ shift (length is\<^sub>1) xt\<^sub>2 \<turnstile> (is\<^sub>1 @ is\<^sub>2) ! pc,pc :: \<tau>s\<^sub>1 @ \<tau>s\<^sub>2
[PROOF STEP]
have "length \<tau>s\<^sub>2 \<le> length \<tau>s\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length \<tau>s\<^sub>2 \<le> length \<tau>s\<^sub>2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length \<tau>s\<^sub>2 \<le> length \<tau>s\<^sub>2

goal (1 subgoal):
 1. \<not> pc < length is\<^sub>1 \<Longrightarrow> P,T\<^sub>r,mxs,length (\<tau>s\<^sub>1 @ \<tau>s\<^sub>2),xt\<^sub>1 @ shift (length is\<^sub>1) xt\<^sub>2 \<turnstile> (is\<^sub>1 @ is\<^sub>2) ! pc,pc :: \<tau>s\<^sub>1 @ \<tau>s\<^sub>2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
length \<tau>s\<^sub>2 \<le> length \<tau>s\<^sub>2

goal (1 subgoal):
 1. \<not> pc < length is\<^sub>1 \<Longrightarrow> P,T\<^sub>r,mxs,length (\<tau>s\<^sub>1 @ \<tau>s\<^sub>2),xt\<^sub>1 @ shift (length is\<^sub>1) xt\<^sub>2 \<turnstile> (is\<^sub>1 @ is\<^sub>2) ! pc,pc :: \<tau>s\<^sub>1 @ \<tau>s\<^sub>2
[PROOF STEP]
have "pc - length is\<^sub>1 + length \<tau>s\<^sub>1 \<notin> pcs xt\<^sub>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pc - length is\<^sub>1 + length \<tau>s\<^sub>1 \<notin> pcs xt\<^sub>1
[PROOF STEP]
using wt\<^sub>1 \<tau>s_size
[PROOF STATE]
proof (prove)
using this:
\<turnstile> is\<^sub>1, xt\<^sub>1 [::] \<tau>s\<^sub>1 @ \<tau>s\<^sub>2
length \<tau>s\<^sub>1 = length is\<^sub>1

goal (1 subgoal):
 1. pc - length is\<^sub>1 + length \<tau>s\<^sub>1 \<notin> pcs xt\<^sub>1
[PROOF STEP]
by(fastforce simp: wt_instrs_def)
[PROOF STATE]
proof (state)
this:
pc - length is\<^sub>1 + length \<tau>s\<^sub>1 \<notin> pcs xt\<^sub>1

goal (1 subgoal):
 1. \<not> pc < length is\<^sub>1 \<Longrightarrow> P,T\<^sub>r,mxs,length (\<tau>s\<^sub>1 @ \<tau>s\<^sub>2),xt\<^sub>1 @ shift (length is\<^sub>1) xt\<^sub>2 \<turnstile> (is\<^sub>1 @ is\<^sub>2) ! pc,pc :: \<tau>s\<^sub>1 @ \<tau>s\<^sub>2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
P,T\<^sub>r,mxs,length \<tau>s\<^sub>2,xt\<^sub>2 \<turnstile> is\<^sub>2 ! (pc - length is\<^sub>1),pc - length is\<^sub>1 :: \<tau>s\<^sub>2
pc - length is\<^sub>1 < length \<tau>s\<^sub>2
length \<tau>s\<^sub>2 \<le> length \<tau>s\<^sub>2
pc - length is\<^sub>1 + length \<tau>s\<^sub>1 \<notin> pcs xt\<^sub>1
[PROOF STEP]
have "P,T\<^sub>r,mxs,length \<tau>s\<^sub>2 + length \<tau>s\<^sub>1,xt\<^sub>1 @ shift (length \<tau>s\<^sub>1) xt\<^sub>2
                         \<turnstile> is\<^sub>2 ! (pc - length is\<^sub>1),pc - length is\<^sub>1 + length \<tau>s\<^sub>1 :: \<tau>s\<^sub>1 @ \<tau>s\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
P,T\<^sub>r,mxs,length \<tau>s\<^sub>2,xt\<^sub>2 \<turnstile> is\<^sub>2 ! (pc - length is\<^sub>1),pc - length is\<^sub>1 :: \<tau>s\<^sub>2
pc - length is\<^sub>1 < length \<tau>s\<^sub>2
length \<tau>s\<^sub>2 \<le> length \<tau>s\<^sub>2
pc - length is\<^sub>1 + length \<tau>s\<^sub>1 \<notin> pcs xt\<^sub>1

goal (1 subgoal):
 1. P,T\<^sub>r,mxs,length \<tau>s\<^sub>2 + length \<tau>s\<^sub>1,xt\<^sub>1 @ shift (length \<tau>s\<^sub>1) xt\<^sub>2 \<turnstile> is\<^sub>2 ! (pc - length is\<^sub>1),pc - length is\<^sub>1 + length \<tau>s\<^sub>1 :: \<tau>s\<^sub>1 @ \<tau>s\<^sub>2
[PROOF STEP]
by(rule wt_instr_appLx[OF wt_instr_appL[where \<tau>s' = "\<tau>s\<^sub>1"]])
[PROOF STATE]
proof (state)
this:
P,T\<^sub>r,mxs,length \<tau>s\<^sub>2 + length \<tau>s\<^sub>1,xt\<^sub>1 @ shift (length \<tau>s\<^sub>1) xt\<^sub>2 \<turnstile> is\<^sub>2 ! (pc - length is\<^sub>1),pc - length is\<^sub>1 + length \<tau>s\<^sub>1 :: \<tau>s\<^sub>1 @ \<tau>s\<^sub>2

goal (1 subgoal):
 1. \<not> pc < length is\<^sub>1 \<Longrightarrow> P,T\<^sub>r,mxs,length (\<tau>s\<^sub>1 @ \<tau>s\<^sub>2),xt\<^sub>1 @ shift (length is\<^sub>1) xt\<^sub>2 \<turnstile> (is\<^sub>1 @ is\<^sub>2) ! pc,pc :: \<tau>s\<^sub>1 @ \<tau>s\<^sub>2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
P,T\<^sub>r,mxs,length \<tau>s\<^sub>2 + length \<tau>s\<^sub>1,xt\<^sub>1 @ shift (length \<tau>s\<^sub>1) xt\<^sub>2 \<turnstile> is\<^sub>2 ! (pc - length is\<^sub>1),pc - length is\<^sub>1 + length \<tau>s\<^sub>1 :: \<tau>s\<^sub>1 @ \<tau>s\<^sub>2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
P,T\<^sub>r,mxs,length \<tau>s\<^sub>2 + length \<tau>s\<^sub>1,xt\<^sub>1 @ shift (length \<tau>s\<^sub>1) xt\<^sub>2 \<turnstile> is\<^sub>2 ! (pc - length is\<^sub>1),pc - length is\<^sub>1 + length \<tau>s\<^sub>1 :: \<tau>s\<^sub>1 @ \<tau>s\<^sub>2

goal (1 subgoal):
 1. P,T\<^sub>r,mxs,length (\<tau>s\<^sub>1 @ \<tau>s\<^sub>2),xt\<^sub>1 @ shift (length is\<^sub>1) xt\<^sub>2 \<turnstile> (is\<^sub>1 @ is\<^sub>2) ! pc,pc :: \<tau>s\<^sub>1 @ \<tau>s\<^sub>2
[PROOF STEP]
using False \<tau>s_size
[PROOF STATE]
proof (prove)
using this:
P,T\<^sub>r,mxs,length \<tau>s\<^sub>2 + length \<tau>s\<^sub>1,xt\<^sub>1 @ shift (length \<tau>s\<^sub>1) xt\<^sub>2 \<turnstile> is\<^sub>2 ! (pc - length is\<^sub>1),pc - length is\<^sub>1 + length \<tau>s\<^sub>1 :: \<tau>s\<^sub>1 @ \<tau>s\<^sub>2
\<not> pc < length is\<^sub>1
length \<tau>s\<^sub>1 = length is\<^sub>1

goal (1 subgoal):
 1. P,T\<^sub>r,mxs,length (\<tau>s\<^sub>1 @ \<tau>s\<^sub>2),xt\<^sub>1 @ shift (length is\<^sub>1) xt\<^sub>2 \<turnstile> (is\<^sub>1 @ is\<^sub>2) ! pc,pc :: \<tau>s\<^sub>1 @ \<tau>s\<^sub>2
[PROOF STEP]
by(simp add:add.commute)
[PROOF STATE]
proof (state)
this:
P,T\<^sub>r,mxs,length (\<tau>s\<^sub>1 @ \<tau>s\<^sub>2),xt\<^sub>1 @ shift (length is\<^sub>1) xt\<^sub>2 \<turnstile> (is\<^sub>1 @ is\<^sub>2) ! pc,pc :: \<tau>s\<^sub>1 @ \<tau>s\<^sub>2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P,T\<^sub>r,mxs,length (\<tau>s\<^sub>1 @ \<tau>s\<^sub>2),xt\<^sub>1 @ shift (length is\<^sub>1) xt\<^sub>2 \<turnstile> (is\<^sub>1 @ is\<^sub>2) ! pc,pc :: \<tau>s\<^sub>1 @ \<tau>s\<^sub>2

goal (1 subgoal):
 1. \<turnstile> is\<^sub>1 @ is\<^sub>2, xt\<^sub>1 @ shift (length is\<^sub>1) xt\<^sub>2 [::] \<tau>s\<^sub>1 @ \<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 @ \<tau>s\<^sub>2),xt\<^sub>1 @ shift (length is\<^sub>1) xt\<^sub>2 \<turnstile> (is\<^sub>1 @ is\<^sub>2) ! ?pc4,?pc4 :: \<tau>s\<^sub>1 @ \<tau>s\<^sub>2

goal (1 subgoal):
 1. \<turnstile> is\<^sub>1 @ is\<^sub>2, xt\<^sub>1 @ shift (length is\<^sub>1) xt\<^sub>2 [::] \<tau>s\<^sub>1 @ \<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 @ \<tau>s\<^sub>2)
pcs (xt\<^sub>1 @ shift (length is\<^sub>1) xt\<^sub>2) \<subseteq> {0..<length (is\<^sub>1 @ is\<^sub>2)}
?pc4 < length (is\<^sub>1 @ is\<^sub>2) \<Longrightarrow> P,T\<^sub>r,mxs,length (\<tau>s\<^sub>1 @ \<tau>s\<^sub>2),xt\<^sub>1 @ shift (length is\<^sub>1) xt\<^sub>2 \<turnstile> (is\<^sub>1 @ is\<^sub>2) ! ?pc4,?pc4 :: \<tau>s\<^sub>1 @ \<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 @ \<tau>s\<^sub>2)
pcs (xt\<^sub>1 @ shift (length is\<^sub>1) xt\<^sub>2) \<subseteq> {0..<length (is\<^sub>1 @ is\<^sub>2)}
?pc4 < length (is\<^sub>1 @ is\<^sub>2) \<Longrightarrow> P,T\<^sub>r,mxs,length (\<tau>s\<^sub>1 @ \<tau>s\<^sub>2),xt\<^sub>1 @ shift (length is\<^sub>1) xt\<^sub>2 \<turnstile> (is\<^sub>1 @ is\<^sub>2) ! ?pc4,?pc4 :: \<tau>s\<^sub>1 @ \<tau>s\<^sub>2

goal (1 subgoal):
 1. \<turnstile> is\<^sub>1 @ is\<^sub>2, xt\<^sub>1 @ shift (length is\<^sub>1) xt\<^sub>2 [::] \<tau>s\<^sub>1 @ \<tau>s\<^sub>2
[PROOF STEP]
by(clarsimp simp:wt_instrs_def)
[PROOF STATE]
proof (state)
this:
\<turnstile> is\<^sub>1 @ is\<^sub>2, xt\<^sub>1 @ shift (length is\<^sub>1) xt\<^sub>2 [::] \<tau>s\<^sub>1 @ \<tau>s\<^sub>2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in TC2) wt_instrs_last_incr[trans]:
assumes wtis: "\<turnstile> is,xt [::] \<tau>s@[\<tau>]" and ss: "P \<turnstile> \<tau> \<le>' \<tau>'"
shows "\<turnstile> is,xt [::] \<tau>s@[\<tau>']"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> is, xt [::] \<tau>s @ [\<tau>']
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> is, xt [::] \<tau>s @ [\<tau>']
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<turnstile> is, xt [::] \<tau>s @ [\<tau>']
[PROOF STEP]
let ?\<tau>s = "\<tau>s@[\<tau>]" and ?\<tau>s' = "\<tau>s@[\<tau>']"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<turnstile> is, xt [::] \<tau>s @ [\<tau>']
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<turnstile> is, xt [::] \<tau>s @ [\<tau>']
[PROOF STEP]
fix pc
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<turnstile> is, xt [::] \<tau>s @ [\<tau>']
[PROOF STEP]
assume pc: "pc< size is"
[PROOF STATE]
proof (state)
this:
pc < length is

goal (1 subgoal):
 1. \<turnstile> is, xt [::] \<tau>s @ [\<tau>']
[PROOF STEP]
let ?i = "is!pc"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<turnstile> is, xt [::] \<tau>s @ [\<tau>']
[PROOF STEP]
have app_pc: "app (is ! pc) P mxs T\<^sub>r pc (length ?\<tau>s) xt (\<tau>s ! pc)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. app (is ! pc) P mxs T\<^sub>r pc (length (\<tau>s @ [\<tau>])) xt (\<tau>s ! pc)
[PROOF STEP]
using wtis pc
[PROOF STATE]
proof (prove)
using this:
\<turnstile> is, xt [::] \<tau>s @ [\<tau>]
pc < length is

goal (1 subgoal):
 1. app (is ! pc) P mxs T\<^sub>r pc (length (\<tau>s @ [\<tau>])) xt (\<tau>s ! pc)
[PROOF STEP]
by(clarsimp simp add:wt_instrs_def wt_instr_def)
[PROOF STATE]
proof (state)
this:
app (is ! pc) P mxs T\<^sub>r pc (length (\<tau>s @ [\<tau>])) xt (\<tau>s ! pc)

goal (1 subgoal):
 1. \<turnstile> is, xt [::] \<tau>s @ [\<tau>']
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
app (is ! pc) P mxs T\<^sub>r pc (length (\<tau>s @ [\<tau>])) xt (\<tau>s ! pc)
[PROOF STEP]
have Apc\<tau>': "\<And>pc' \<tau>'. (pc',\<tau>') \<in> set (eff ?i P pc xt (?\<tau>s!pc))
     \<Longrightarrow> pc' < length ?\<tau>s"
[PROOF STATE]
proof (prove)
using this:
app (is ! pc) P mxs T\<^sub>r pc (length (\<tau>s @ [\<tau>])) xt (\<tau>s ! pc)

goal (1 subgoal):
 1. \<And>pc' \<tau>'. (pc', \<tau>') \<in> set (eff (is ! pc) P pc xt ((\<tau>s @ [\<tau>]) ! pc)) \<Longrightarrow> pc' < length (\<tau>s @ [\<tau>])
[PROOF STEP]
using wtis pc
[PROOF STATE]
proof (prove)
using this:
app (is ! pc) P mxs T\<^sub>r pc (length (\<tau>s @ [\<tau>])) xt (\<tau>s ! pc)
\<turnstile> is, xt [::] \<tau>s @ [\<tau>]
pc < length is

goal (1 subgoal):
 1. \<And>pc' \<tau>'. (pc', \<tau>') \<in> set (eff (is ! pc) P pc xt ((\<tau>s @ [\<tau>]) ! pc)) \<Longrightarrow> pc' < length (\<tau>s @ [\<tau>])
[PROOF STEP]
by(fastforce simp add:wt_instrs_def app_def)
[PROOF STATE]
proof (state)
this:
(?pc'2, ?\<tau>'2) \<in> set (eff (is ! pc) P pc xt ((\<tau>s @ [\<tau>]) ! pc)) \<Longrightarrow> ?pc'2 < length (\<tau>s @ [\<tau>])

goal (1 subgoal):
 1. \<turnstile> is, xt [::] \<tau>s @ [\<tau>']
[PROOF STEP]
have Aepc\<tau>': "\<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)
goal (1 subgoal):
 1. \<And>pc' \<tau>'. (pc', \<tau>') \<in> set (eff (is ! pc) P pc xt ((\<tau>s @ [\<tau>]) ! pc)) \<Longrightarrow> P \<turnstile> \<tau>' \<le>' (\<tau>s @ [\<tau>]) ! pc'
[PROOF STEP]
using wtis pc
[PROOF STATE]
proof (prove)
using this:
\<turnstile> is, xt [::] \<tau>s @ [\<tau>]
pc < length is

goal (1 subgoal):
 1. \<And>pc' \<tau>'. (pc', \<tau>') \<in> set (eff (is ! pc) P pc xt ((\<tau>s @ [\<tau>]) ! pc)) \<Longrightarrow> P \<turnstile> \<tau>' \<le>' (\<tau>s @ [\<tau>]) ! pc'
[PROOF STEP]
by(fastforce simp add:wt_instrs_def wt_instr_def)
[PROOF STATE]
proof (state)
this:
(?pc'2, ?\<tau>'2) \<in> set (eff (is ! pc) P pc xt ((\<tau>s @ [\<tau>]) ! pc)) \<Longrightarrow> P \<turnstile> ?\<tau>'2 \<le>' (\<tau>s @ [\<tau>]) ! ?pc'2

goal (1 subgoal):
 1. \<turnstile> is, xt [::] \<tau>s @ [\<tau>']
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
(?pc'2, ?\<tau>'2) \<in> set (eff (is ! pc) P pc xt ((\<tau>s @ [\<tau>]) ! pc)) \<Longrightarrow> P \<turnstile> ?\<tau>'2 \<le>' (\<tau>s @ [\<tau>]) ! ?pc'2

goal (1 subgoal):
 1. \<turnstile> is, xt [::] \<tau>s @ [\<tau>']
[PROOF STEP]
fix pc1 \<tau>1
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<turnstile> is, xt [::] \<tau>s @ [\<tau>']
[PROOF STEP]
assume pc\<tau>1: "(pc1,\<tau>1) \<in> set (eff ?i P pc xt (?\<tau>s'!pc))"
[PROOF STATE]
proof (state)
this:
(pc1, \<tau>1) \<in> set (eff (is ! pc) P pc xt ((\<tau>s @ [\<tau>']) ! pc))

goal (1 subgoal):
 1. \<turnstile> is, xt [::] \<tau>s @ [\<tau>']
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(pc1, \<tau>1) \<in> set (eff (is ! pc) P pc xt ((\<tau>s @ [\<tau>']) ! pc))
[PROOF STEP]
have epc\<tau>': "(pc1,\<tau>1) \<in> set (eff ?i P pc xt (?\<tau>s!pc))"
[PROOF STATE]
proof (prove)
using this:
(pc1, \<tau>1) \<in> set (eff (is ! pc) P pc xt ((\<tau>s @ [\<tau>']) ! pc))

goal (1 subgoal):
 1. (pc1, \<tau>1) \<in> set (eff (is ! pc) P pc xt ((\<tau>s @ [\<tau>]) ! pc))
[PROOF STEP]
using wtis pc
[PROOF STATE]
proof (prove)
using this:
(pc1, \<tau>1) \<in> set (eff (is ! pc) P pc xt ((\<tau>s @ [\<tau>']) ! pc))
\<turnstile> is, xt [::] \<tau>s @ [\<tau>]
pc < length is

goal (1 subgoal):
 1. (pc1, \<tau>1) \<in> set (eff (is ! pc) P pc xt ((\<tau>s @ [\<tau>]) ! pc))
[PROOF STEP]
by(simp add:wt_instrs_def)
[PROOF STATE]
proof (state)
this:
(pc1, \<tau>1) \<in> set (eff (is ! pc) P pc xt ((\<tau>s @ [\<tau>]) ! pc))

goal (1 subgoal):
 1. \<turnstile> is, xt [::] \<tau>s @ [\<tau>']
[PROOF STEP]
have "P \<turnstile> \<tau>1 \<le>' ?\<tau>s'!pc1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> \<tau>1 \<le>' (\<tau>s @ [\<tau>']) ! pc1
[PROOF STEP]
proof(cases "pc1 < length \<tau>s")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. pc1 < length \<tau>s \<Longrightarrow> P \<turnstile> \<tau>1 \<le>' (\<tau>s @ [\<tau>']) ! pc1
 2. \<not> pc1 < length \<tau>s \<Longrightarrow> P \<turnstile> \<tau>1 \<le>' (\<tau>s @ [\<tau>']) ! pc1
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
pc1 < length \<tau>s

goal (2 subgoals):
 1. pc1 < length \<tau>s \<Longrightarrow> P \<turnstile> \<tau>1 \<le>' (\<tau>s @ [\<tau>']) ! pc1
 2. \<not> pc1 < length \<tau>s \<Longrightarrow> P \<turnstile> \<tau>1 \<le>' (\<tau>s @ [\<tau>']) ! pc1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pc1 < length \<tau>s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
pc1 < length \<tau>s

goal (1 subgoal):
 1. P \<turnstile> \<tau>1 \<le>' (\<tau>s @ [\<tau>']) ! pc1
[PROOF STEP]
using wtis pc pc\<tau>1
[PROOF STATE]
proof (prove)
using this:
pc1 < length \<tau>s
\<turnstile> is, xt [::] \<tau>s @ [\<tau>]
pc < length is
(pc1, \<tau>1) \<in> set (eff (is ! pc) P pc xt ((\<tau>s @ [\<tau>']) ! pc))

goal (1 subgoal):
 1. P \<turnstile> \<tau>1 \<le>' (\<tau>s @ [\<tau>']) ! pc1
[PROOF STEP]
by(fastforce simp add:wt_instrs_def wt_instr_def)
[PROOF STATE]
proof (state)
this:
P \<turnstile> \<tau>1 \<le>' (\<tau>s @ [\<tau>']) ! pc1

goal (1 subgoal):
 1. \<not> pc1 < length \<tau>s \<Longrightarrow> P \<turnstile> \<tau>1 \<le>' (\<tau>s @ [\<tau>']) ! pc1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> pc1 < length \<tau>s \<Longrightarrow> P \<turnstile> \<tau>1 \<le>' (\<tau>s @ [\<tau>']) ! pc1
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> pc1 < length \<tau>s

goal (1 subgoal):
 1. \<not> pc1 < length \<tau>s \<Longrightarrow> P \<turnstile> \<tau>1 \<le>' (\<tau>s @ [\<tau>']) ! pc1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> pc1 < length \<tau>s
[PROOF STEP]
have "pc1 < length ?\<tau>s"
[PROOF STATE]
proof (prove)
using this:
\<not> pc1 < length \<tau>s

goal (1 subgoal):
 1. pc1 < length (\<tau>s @ [\<tau>])
[PROOF STEP]
using Apc\<tau>'[OF epc\<tau>']
[PROOF STATE]
proof (prove)
using this:
\<not> pc1 < length \<tau>s
pc1 < length (\<tau>s @ [\<tau>])

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

goal (1 subgoal):
 1. \<not> pc1 < length \<tau>s \<Longrightarrow> P \<turnstile> \<tau>1 \<le>' (\<tau>s @ [\<tau>']) ! pc1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pc1 < length (\<tau>s @ [\<tau>])
[PROOF STEP]
have [simp]: "pc1 = size \<tau>s"
[PROOF STATE]
proof (prove)
using this:
pc1 < length (\<tau>s @ [\<tau>])

goal (1 subgoal):
 1. pc1 = length \<tau>s
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
pc1 < length (\<tau>s @ [\<tau>])
\<not> pc1 < length \<tau>s

goal (1 subgoal):
 1. pc1 = length \<tau>s
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
pc1 = length \<tau>s

goal (1 subgoal):
 1. \<not> pc1 < length \<tau>s \<Longrightarrow> P \<turnstile> \<tau>1 \<le>' (\<tau>s @ [\<tau>']) ! pc1
[PROOF STEP]
have "P \<turnstile> \<tau>1 \<le>' \<tau>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> \<tau>1 \<le>' \<tau>
[PROOF STEP]
using Aepc\<tau>'[OF epc\<tau>']
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> \<tau>1 \<le>' (\<tau>s @ [\<tau>]) ! pc1

goal (1 subgoal):
 1. P \<turnstile> \<tau>1 \<le>' \<tau>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P \<turnstile> \<tau>1 \<le>' \<tau>

goal (1 subgoal):
 1. \<not> pc1 < length \<tau>s \<Longrightarrow> P \<turnstile> \<tau>1 \<le>' (\<tau>s @ [\<tau>']) ! pc1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
P \<turnstile> \<tau>1 \<le>' \<tau>
[PROOF STEP]
have "P \<turnstile> \<tau>1 \<le>' \<tau>'"
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> \<tau>1 \<le>' \<tau>

goal (1 subgoal):
 1. P \<turnstile> \<tau>1 \<le>' \<tau>'
[PROOF STEP]
by(rule sup_state_opt_trans[OF _ ss])
[PROOF STATE]
proof (state)
this:
P \<turnstile> \<tau>1 \<le>' \<tau>'

goal (1 subgoal):
 1. \<not> pc1 < length \<tau>s \<Longrightarrow> P \<turnstile> \<tau>1 \<le>' (\<tau>s @ [\<tau>']) ! pc1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
P \<turnstile> \<tau>1 \<le>' \<tau>'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> \<tau>1 \<le>' \<tau>'

goal (1 subgoal):
 1. P \<turnstile> \<tau>1 \<le>' (\<tau>s @ [\<tau>']) ! pc1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P \<turnstile> \<tau>1 \<le>' (\<tau>s @ [\<tau>']) ! pc1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P \<turnstile> \<tau>1 \<le>' (\<tau>s @ [\<tau>']) ! pc1

goal (1 subgoal):
 1. \<turnstile> is, xt [::] \<tau>s @ [\<tau>']
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(?pc1.4, ?\<tau>1.4) \<in> set (eff (is ! pc) P pc xt ((\<tau>s @ [\<tau>']) ! pc)) \<Longrightarrow> P \<turnstile> ?\<tau>1.4 \<le>' (\<tau>s @ [\<tau>']) ! ?pc1.4

goal (1 subgoal):
 1. \<turnstile> is, xt [::] \<tau>s @ [\<tau>']
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(?pc1.4, ?\<tau>1.4) \<in> set (eff (is ! pc) P pc xt ((\<tau>s @ [\<tau>']) ! pc)) \<Longrightarrow> P \<turnstile> ?\<tau>1.4 \<le>' (\<tau>s @ [\<tau>']) ! ?pc1.4
[PROOF STEP]
have "P,T\<^sub>r,mxs,size ?\<tau>s',xt \<turnstile> is!pc,pc :: ?\<tau>s'"
[PROOF STATE]
proof (prove)
using this:
(?pc1.4, ?\<tau>1.4) \<in> set (eff (is ! pc) P pc xt ((\<tau>s @ [\<tau>']) ! pc)) \<Longrightarrow> P \<turnstile> ?\<tau>1.4 \<le>' (\<tau>s @ [\<tau>']) ! ?pc1.4

goal (1 subgoal):
 1. P,T\<^sub>r,mxs,length (\<tau>s @ [\<tau>']),xt \<turnstile> is ! pc,pc :: \<tau>s @ [\<tau>']
[PROOF STEP]
using wtis pc
[PROOF STATE]
proof (prove)
using this:
(?pc1.4, ?\<tau>1.4) \<in> set (eff (is ! pc) P pc xt ((\<tau>s @ [\<tau>']) ! pc)) \<Longrightarrow> P \<turnstile> ?\<tau>1.4 \<le>' (\<tau>s @ [\<tau>']) ! ?pc1.4
\<turnstile> is, xt [::] \<tau>s @ [\<tau>]
pc < length is

goal (1 subgoal):
 1. P,T\<^sub>r,mxs,length (\<tau>s @ [\<tau>']),xt \<turnstile> is ! pc,pc :: \<tau>s @ [\<tau>']
[PROOF STEP]
by(clarsimp simp add:wt_instrs_def wt_instr_def)
[PROOF STATE]
proof (state)
this:
P,T\<^sub>r,mxs,length (\<tau>s @ [\<tau>']),xt \<turnstile> is ! pc,pc :: \<tau>s @ [\<tau>']

goal (1 subgoal):
 1. \<turnstile> is, xt [::] \<tau>s @ [\<tau>']
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?pc4 < length is \<Longrightarrow> P,T\<^sub>r,mxs,length (\<tau>s @ [\<tau>']),xt \<turnstile> is ! ?pc4,?pc4 :: \<tau>s @ [\<tau>']

goal (1 subgoal):
 1. \<turnstile> is, xt [::] \<tau>s @ [\<tau>']
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?pc4 < length is \<Longrightarrow> P,T\<^sub>r,mxs,length (\<tau>s @ [\<tau>']),xt \<turnstile> is ! ?pc4,?pc4 :: \<tau>s @ [\<tau>']
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?pc4 < length is \<Longrightarrow> P,T\<^sub>r,mxs,length (\<tau>s @ [\<tau>']),xt \<turnstile> is ! ?pc4,?pc4 :: \<tau>s @ [\<tau>']

goal (1 subgoal):
 1. \<turnstile> is, xt [::] \<tau>s @ [\<tau>']
[PROOF STEP]
using wtis
[PROOF STATE]
proof (prove)
using this:
?pc4 < length is \<Longrightarrow> P,T\<^sub>r,mxs,length (\<tau>s @ [\<tau>']),xt \<turnstile> is ! ?pc4,?pc4 :: \<tau>s @ [\<tau>']
\<turnstile> is, xt [::] \<tau>s @ [\<tau>]

goal (1 subgoal):
 1. \<turnstile> is, xt [::] \<tau>s @ [\<tau>']
[PROOF STEP]
by(simp add:wt_instrs_def)
[PROOF STATE]
proof (state)
this:
\<turnstile> is, xt [::] \<tau>s @ [\<tau>']

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma [iff]: "xcpt_app i P pc mxs [] \<tau>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xcpt_app i P pc mxs [] \<tau>
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xcpt_app i P pc mxs [] \<tau>
[PROOF STEP]
by (simp add: xcpt_app_def relevant_entries_def)


[STATEMENT]
lemma [simp]: "xcpt_eff i P pc \<tau> [] = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xcpt_eff i P pc \<tau> [] = []
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xcpt_eff i P pc \<tau> [] = []
[PROOF STEP]
by (simp add: xcpt_eff_def relevant_entries_def)


[STATEMENT]
lemma (in TC2) wt_New:
  "\<lbrakk> is_class P C; size ST < mxs \<rbrakk> \<Longrightarrow>
   \<turnstile> [New C],[] [::] [ty\<^sub>i' ST E A, ty\<^sub>i' (Class C#ST) E A]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_class P C; length ST < mxs\<rbrakk> \<Longrightarrow> \<turnstile> [New C], [] [::] [ty\<^sub>i' ST E A, ty\<^sub>i' (Class C # ST) E A]
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_class P C; length ST < mxs\<rbrakk> \<Longrightarrow> \<turnstile> [New C], [] [::] [ty\<^sub>i' ST E A, ty\<^sub>i' (Class C # ST) E A]
[PROOF STEP]
by(simp add:wt_defs ty\<^sub>i'_def)


[STATEMENT]
lemma (in TC2) wt_Cast:
  "is_class P C \<Longrightarrow>
   \<turnstile> [Checkcast C],[] [::] [ty\<^sub>i' (Class D # ST) E A, ty\<^sub>i' (Class C # ST) E A]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_class P C \<Longrightarrow> \<turnstile> [Checkcast C], [] [::] [ty\<^sub>i' (Class D # ST) E A, ty\<^sub>i' (Class C # ST) E A]
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_class P C \<Longrightarrow> \<turnstile> [Checkcast C], [] [::] [ty\<^sub>i' (Class D # ST) E A, ty\<^sub>i' (Class C # ST) E A]
[PROOF STEP]
by(simp add: ty\<^sub>i'_def wt_defs)


[STATEMENT]
lemma (in TC2) wt_Push:
  "\<lbrakk> size ST < mxs; typeof v = Some T \<rbrakk>
  \<Longrightarrow> \<turnstile> [Push v],[] [::] [ty\<^sub>i' ST E A, ty\<^sub>i' (T#ST) E A]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length ST < mxs; typeof v = \<lfloor>T\<rfloor>\<rbrakk> \<Longrightarrow> \<turnstile> [Push v], [] [::] [ty\<^sub>i' ST E A, ty\<^sub>i' (T # ST) E A]
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length ST < mxs; typeof v = \<lfloor>T\<rfloor>\<rbrakk> \<Longrightarrow> \<turnstile> [Push v], [] [::] [ty\<^sub>i' ST E A, ty\<^sub>i' (T # ST) E A]
[PROOF STEP]
by(simp add: ty\<^sub>i'_def wt_defs)


[STATEMENT]
lemma (in TC2) wt_Pop:
 "\<turnstile> [Pop],[] [::] (ty\<^sub>i' (T#ST) E A # ty\<^sub>i' ST E A # \<tau>s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> [Pop], [] [::] ty\<^sub>i' (T # ST) E A # ty\<^sub>i' ST E A # \<tau>s
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> [Pop], [] [::] ty\<^sub>i' (T # ST) E A # ty\<^sub>i' ST E A # \<tau>s
[PROOF STEP]
by(simp add: ty\<^sub>i'_def wt_defs)


[STATEMENT]
lemma (in TC2) wt_CmpEq:
  "\<lbrakk> P \<turnstile> T\<^sub>1 \<le> T\<^sub>2 \<or> P \<turnstile> T\<^sub>2 \<le> T\<^sub>1\<rbrakk>
  \<Longrightarrow> \<turnstile> [CmpEq],[] [::] [ty\<^sub>i' (T\<^sub>2 # T\<^sub>1 # ST) E A, ty\<^sub>i' (Boolean # ST) E A]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subtype P T\<^sub>1 T\<^sub>2 \<or> subtype P T\<^sub>2 T\<^sub>1 \<Longrightarrow> \<turnstile> [CmpEq], [] [::] [ty\<^sub>i' (T\<^sub>2 # T\<^sub>1 # ST) E A, ty\<^sub>i' (Boolean # ST) E A]
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subtype P T\<^sub>1 T\<^sub>2 \<or> subtype P T\<^sub>2 T\<^sub>1 \<Longrightarrow> \<turnstile> [CmpEq], [] [::] [ty\<^sub>i' (T\<^sub>2 # T\<^sub>1 # ST) E A, ty\<^sub>i' (Boolean # ST) E A]
[PROOF STEP]
by(auto simp:ty\<^sub>i'_def wt_defs elim!: refTE not_refTE)


[STATEMENT]
lemma (in TC2) wt_IAdd:
  "\<turnstile> [IAdd],[] [::] [ty\<^sub>i' (Integer#Integer#ST) E A, ty\<^sub>i' (Integer#ST) E A]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> [IAdd], [] [::] [ty\<^sub>i' (Integer # Integer # ST) E A, ty\<^sub>i' (Integer # ST) E A]
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> [IAdd], [] [::] [ty\<^sub>i' (Integer # Integer # ST) E A, ty\<^sub>i' (Integer # ST) E A]
[PROOF STEP]
by(simp add:ty\<^sub>i'_def wt_defs)


[STATEMENT]
lemma (in TC2) wt_Load:
  "\<lbrakk> size ST < mxs; size E \<le> mxl; i \<in>\<in> A; i < size E \<rbrakk>
  \<Longrightarrow> \<turnstile> [Load i],[] [::] [ty\<^sub>i' ST E A, ty\<^sub>i' (E!i # ST) E A]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length ST < mxs; length E \<le> mxl; i \<in>\<in> A; i < length E\<rbrakk> \<Longrightarrow> \<turnstile> [Load i], [] [::] [ty\<^sub>i' ST E A, ty\<^sub>i' (E ! i # ST) E A]
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length ST < mxs; length E \<le> mxl; i \<in>\<in> A; i < length E\<rbrakk> \<Longrightarrow> \<turnstile> [Load i], [] [::] [ty\<^sub>i' ST E A, ty\<^sub>i' (E ! i # ST) E A]
[PROOF STEP]
by(auto simp add:ty\<^sub>i'_def wt_defs ty\<^sub>l_def hyperset_defs)


[STATEMENT]
lemma (in TC2) wt_Store:
 "\<lbrakk> P \<turnstile> T \<le> E!i; i < size E; size E \<le> mxl \<rbrakk> \<Longrightarrow>
  \<turnstile> [Store i],[] [::] [ty\<^sub>i' (T#ST) E A, ty\<^sub>i' ST E (\<lfloor>{i}\<rfloor> \<squnion> A)]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>subtype P T (E ! i); i < length E; length E \<le> mxl\<rbrakk> \<Longrightarrow> \<turnstile> [Store i], [] [::] [ty\<^sub>i' (T # ST) E A, ty\<^sub>i' ST E (\<lfloor>{i}\<rfloor> \<squnion> A)]
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>subtype P T (E ! i); i < length E; length E \<le> mxl\<rbrakk> \<Longrightarrow> \<turnstile> [Store i], [] [::] [ty\<^sub>i' (T # ST) E A, ty\<^sub>i' ST E (\<lfloor>{i}\<rfloor> \<squnion> A)]
[PROOF STEP]
by(auto simp:hyperset_defs nth_list_update ty\<^sub>i'_def wt_defs ty\<^sub>l_def
        intro:list_all2_all_nthI)


[STATEMENT]
lemma (in TC2) wt_Get:
 "\<lbrakk> P \<turnstile> C sees F,NonStatic:T in D \<rbrakk> \<Longrightarrow>
  \<turnstile> [Getfield F D],[] [::] [ty\<^sub>i' (Class C # ST) E A, ty\<^sub>i' (T # ST) E A]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> C sees F,NonStatic:T in D \<Longrightarrow> \<turnstile> [Getfield F D], [] [::] [ty\<^sub>i' (Class C # ST) E A, ty\<^sub>i' (T # ST) E A]
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> C sees F,NonStatic:T in D \<Longrightarrow> \<turnstile> [Getfield F D], [] [::] [ty\<^sub>i' (Class C # ST) E A, ty\<^sub>i' (T # ST) E A]
[PROOF STEP]
by(auto simp: ty\<^sub>i'_def wt_defs dest: sees_field_idemp sees_field_decl_above)


[STATEMENT]
lemma (in TC2) wt_GetS:
 "\<lbrakk> size ST < mxs; P \<turnstile> C sees F,Static:T in D \<rbrakk> \<Longrightarrow>
  \<turnstile> [Getstatic C F D],[] [::] [ty\<^sub>i' ST E A, ty\<^sub>i' (T # ST) E A]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length ST < mxs; P \<turnstile> C sees F,Static:T in D\<rbrakk> \<Longrightarrow> \<turnstile> [Getstatic C F D], [] [::] [ty\<^sub>i' ST E A, ty\<^sub>i' (T # ST) E A]
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length ST < mxs; P \<turnstile> C sees F,Static:T in D\<rbrakk> \<Longrightarrow> \<turnstile> [Getstatic C F D], [] [::] [ty\<^sub>i' ST E A, ty\<^sub>i' (T # ST) E A]
[PROOF STEP]
by(auto simp: ty\<^sub>i'_def wt_defs dest: sees_field_idemp sees_field_decl_above)


[STATEMENT]
lemma (in TC2) wt_Put:
  "\<lbrakk> P \<turnstile> C sees F,NonStatic:T in D; P \<turnstile> T' \<le> T \<rbrakk> \<Longrightarrow>
  \<turnstile> [Putfield F D],[] [::] [ty\<^sub>i' (T' # Class C # ST) E A, ty\<^sub>i' ST E A]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<turnstile> C sees F,NonStatic:T in D; subtype P T' T\<rbrakk> \<Longrightarrow> \<turnstile> [Putfield F D], [] [::] [ty\<^sub>i' (T' # Class C # ST) E A, ty\<^sub>i' ST E A]
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<turnstile> C sees F,NonStatic:T in D; subtype P T' T\<rbrakk> \<Longrightarrow> \<turnstile> [Putfield F D], [] [::] [ty\<^sub>i' (T' # Class C # ST) E A, ty\<^sub>i' ST E A]
[PROOF STEP]
by(auto intro: sees_field_idemp sees_field_decl_above simp: ty\<^sub>i'_def wt_defs)


[STATEMENT]
lemma (in TC2) wt_PutS:
  "\<lbrakk> P \<turnstile> C sees F,Static:T in D; P \<turnstile> T' \<le> T \<rbrakk> \<Longrightarrow>
  \<turnstile> [Putstatic C F D],[] [::] [ty\<^sub>i' (T' # ST) E A, ty\<^sub>i' ST E A]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<turnstile> C sees F,Static:T in D; subtype P T' T\<rbrakk> \<Longrightarrow> \<turnstile> [Putstatic C F D], [] [::] [ty\<^sub>i' (T' # ST) E A, ty\<^sub>i' ST E A]
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<turnstile> C sees F,Static:T in D; subtype P T' T\<rbrakk> \<Longrightarrow> \<turnstile> [Putstatic C F D], [] [::] [ty\<^sub>i' (T' # ST) E A, ty\<^sub>i' ST E A]
[PROOF STEP]
by(auto intro: sees_field_idemp sees_field_decl_above simp: ty\<^sub>i'_def wt_defs)


[STATEMENT]
lemma (in TC2) wt_Throw:
  "\<turnstile> [Throw],[] [::] [ty\<^sub>i' (Class C # ST) E A, \<tau>']"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> [instr.Throw], [] [::] [ty\<^sub>i' (Class C # ST) E A, \<tau>']
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> [instr.Throw], [] [::] [ty\<^sub>i' (Class C # ST) E A, \<tau>']
[PROOF STEP]
by(auto simp: ty\<^sub>i'_def wt_defs)


[STATEMENT]
lemma (in TC2) wt_IfFalse:
  "\<lbrakk> 2 \<le> i; nat i < size \<tau>s + 2; P \<turnstile> ty\<^sub>i' ST E A \<le>' \<tau>s ! nat(i - 2) \<rbrakk>
  \<Longrightarrow> \<turnstile> [IfFalse i],[] [::] ty\<^sub>i' (Boolean # ST) E A # ty\<^sub>i' ST E A # \<tau>s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>2 \<le> i; nat i < length \<tau>s + 2; P \<turnstile> ty\<^sub>i' ST E A \<le>' \<tau>s ! nat (i - 2)\<rbrakk> \<Longrightarrow> \<turnstile> [IfFalse i], [] [::] ty\<^sub>i' (Boolean # ST) E A # ty\<^sub>i' ST E A # \<tau>s
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>2 \<le> i; nat i < length \<tau>s + 2; P \<turnstile> ty\<^sub>i' ST E A \<le>' \<tau>s ! nat (i - 2)\<rbrakk> \<Longrightarrow> \<turnstile> [IfFalse i], [] [::] ty\<^sub>i' (Boolean # ST) E A # ty\<^sub>i' ST E A # \<tau>s
[PROOF STEP]
by(simp add: ty\<^sub>i'_def wt_defs eval_nat_numeral nat_diff_distrib)


[STATEMENT]
lemma wt_Goto:
 "\<lbrakk> 0 \<le> int pc + i; nat (int pc + i) < size \<tau>s; size \<tau>s \<le> mpc;
    P \<turnstile> \<tau>s!pc \<le>' \<tau>s ! nat (int pc + i) \<rbrakk>
 \<Longrightarrow> P,T,mxs,mpc,[] \<turnstile> Goto i,pc :: \<tau>s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 \<le> int pc + i; nat (int pc + i) < length \<tau>s; length \<tau>s \<le> mpc; P \<turnstile> \<tau>s ! pc \<le>' \<tau>s ! nat (int pc + i)\<rbrakk> \<Longrightarrow> P,T,mxs,mpc,[] \<turnstile> Goto i,pc :: \<tau>s
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 \<le> int pc + i; nat (int pc + i) < length \<tau>s; length \<tau>s \<le> mpc; P \<turnstile> \<tau>s ! pc \<le>' \<tau>s ! nat (int pc + i)\<rbrakk> \<Longrightarrow> P,T,mxs,mpc,[] \<turnstile> Goto i,pc :: \<tau>s
[PROOF STEP]
by(clarsimp simp add: TC2.wt_defs)


[STATEMENT]
lemma (in TC2) wt_Invoke:
  "\<lbrakk> size es = size Ts'; P \<turnstile> C sees M,NonStatic: Ts\<rightarrow>T = m in D; P \<turnstile> Ts' [\<le>] Ts \<rbrakk>
  \<Longrightarrow> \<turnstile> [Invoke M (size es)],[] [::] [ty\<^sub>i' (rev Ts' @ Class C # ST) E A, ty\<^sub>i' (T#ST) E A]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>size es = length Ts'; P \<turnstile> C sees M, NonStatic :  Ts\<rightarrow>T = m in D; P \<turnstile> Ts' [\<le>] Ts\<rbrakk> \<Longrightarrow> \<turnstile> [Invoke M (size es)], [] [::] [ty\<^sub>i' (rev Ts' @ Class C # ST) E A, ty\<^sub>i' (T # ST) E A]
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>size es = length Ts'; P \<turnstile> C sees M, NonStatic :  Ts\<rightarrow>T = m in D; P \<turnstile> Ts' [\<le>] Ts\<rbrakk> \<Longrightarrow> \<turnstile> [Invoke M (size es)], [] [::] [ty\<^sub>i' (rev Ts' @ Class C # ST) E A, ty\<^sub>i' (T # ST) E A]
[PROOF STEP]
by(fastforce simp add: ty\<^sub>i'_def wt_defs)


[STATEMENT]
lemma (in TC2) wt_Invokestatic:
  "\<lbrakk> size ST < mxs; size es = size Ts'; M \<noteq> clinit;
     P \<turnstile> C sees M,Static: Ts\<rightarrow>T = m in D; P \<turnstile> Ts' [\<le>] Ts \<rbrakk>
  \<Longrightarrow> \<turnstile> [Invokestatic C M (size es)],[] [::] [ty\<^sub>i' (rev Ts' @ ST) E A, ty\<^sub>i' (T#ST) E A]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length ST < mxs; size es = length Ts'; M \<noteq> clinit; P \<turnstile> C sees M, Static :  Ts\<rightarrow>T = m in D; P \<turnstile> Ts' [\<le>] Ts\<rbrakk> \<Longrightarrow> \<turnstile> [Invokestatic C M (size es)], [] [::] [ty\<^sub>i' (rev Ts' @ ST) E A, ty\<^sub>i' (T # ST) E A]
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length ST < mxs; size es = length Ts'; M \<noteq> clinit; P \<turnstile> C sees M, Static :  Ts\<rightarrow>T = m in D; P \<turnstile> Ts' [\<le>] Ts\<rbrakk> \<Longrightarrow> \<turnstile> [Invokestatic C M (size es)], [] [::] [ty\<^sub>i' (rev Ts' @ ST) E A, ty\<^sub>i' (T # ST) E A]
[PROOF STEP]
by(fastforce simp add: ty\<^sub>i'_def wt_defs)