[STATEMENT]
lemma regset_spec:
 "\<And>i j xs. xs \<in> regset d i j k =
        ((\<forall>n\<in>set(butlast(trace d i xs)). n < k) \<and> deltas d xs i = j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i j xs. (xs \<in> regset d i j k) = ((\<forall>n\<in>set (butlast (trace d i xs)). n < k) \<and> deltas d xs i = j)
[PROOF STEP]
apply (induct k)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i j xs. (xs \<in> regset d i j 0) = ((\<forall>n\<in>set (butlast (trace d i xs)). n < 0) \<and> deltas d xs i = j)
 2. \<And>k i j xs. (\<And>i j xs. (xs \<in> regset d i j k) = ((\<forall>n\<in>set (butlast (trace d i xs)). n < k) \<and> deltas d xs i = j)) \<Longrightarrow> (xs \<in> regset d i j (Suc k)) = ((\<forall>n\<in>set (butlast (trace d i xs)). n < Suc k) \<and> deltas d xs i = j)
[PROOF STEP]
apply(simp split: list.split)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i j xs. \<forall>x21 x22. xs = x21 # x22 \<longrightarrow> (i = j \<longrightarrow> (x22 = [] \<and> d x21 j = j) = (x22 = [] \<and> deltas d x22 (d x21 j) = j)) \<and> (i \<noteq> j \<longrightarrow> (x22 = [] \<and> d x21 i = j) = (x22 = [] \<and> deltas d x22 (d x21 i) = j))
 2. \<And>k i j xs. (\<And>i j xs. (xs \<in> regset d i j k) = ((\<forall>n\<in>set (butlast (trace d i xs)). n < k) \<and> deltas d xs i = j)) \<Longrightarrow> (xs \<in> regset d i j (Suc k)) = ((\<forall>n\<in>set (butlast (trace d i xs)). n < Suc k) \<and> deltas d xs i = j)
[PROOF STEP]
apply(fastforce)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k i j xs. (\<And>i j xs. (xs \<in> regset d i j k) = ((\<forall>n\<in>set (butlast (trace d i xs)). n < k) \<and> deltas d xs i = j)) \<Longrightarrow> (xs \<in> regset d i j (Suc k)) = ((\<forall>n\<in>set (butlast (trace d i xs)). n < Suc k) \<and> deltas d xs i = j)
[PROOF STEP]
apply (simp add: conc_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k i j xs. (\<And>i j xs. (xs \<in> regset d i j k) = ((\<forall>n\<in>set (butlast (trace d i xs)). n < k) \<and> deltas d xs i = j)) \<Longrightarrow> ((\<forall>n\<in>set (butlast (trace d i xs)). n < k) \<and> deltas d xs i = j \<or> (\<exists>xsa ys. xs = xsa @ ys \<and> (\<forall>n\<in>set (butlast (trace d i xsa)). n < k) \<and> deltas d xsa i = k \<and> (\<exists>xs ysa. ys = xs @ ysa \<and> xs \<in> star (regset d k k k) \<and> (\<forall>n\<in>set (butlast (trace d k ysa)). n < k) \<and> deltas d ysa k = j))) = ((\<forall>n\<in>set (butlast (trace d i xs)). n < Suc k) \<and> deltas d xs i = j)
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>k i j xs. \<lbrakk>\<And>i j xs. (xs \<in> regset d i j k) = ((\<forall>n\<in>set (butlast (trace d i xs)). n < k) \<and> deltas d xs i = j); (\<forall>n\<in>set (butlast (trace d i xs)). n < k) \<and> deltas d xs i = j \<or> (\<exists>xsa ys. xs = xsa @ ys \<and> (\<forall>n\<in>set (butlast (trace d i xsa)). n < k) \<and> deltas d xsa i = k \<and> (\<exists>xs ysa. ys = xs @ ysa \<and> xs \<in> star (regset d k k k) \<and> (\<forall>n\<in>set (butlast (trace d k ysa)). n < k) \<and> deltas d ysa k = j))\<rbrakk> \<Longrightarrow> (\<forall>n\<in>set (butlast (trace d i xs)). n < Suc k) \<and> deltas d xs i = j
 2. \<And>k i j xs. \<lbrakk>\<And>i j xs. (xs \<in> regset d i j k) = ((\<forall>n\<in>set (butlast (trace d i xs)). n < k) \<and> deltas d xs i = j); (\<forall>n\<in>set (butlast (trace d i xs)). n < Suc k) \<and> deltas d xs i = j\<rbrakk> \<Longrightarrow> (\<forall>n\<in>set (butlast (trace d i xs)). n < k) \<and> deltas d xs i = j \<or> (\<exists>xsa ys. xs = xsa @ ys \<and> (\<forall>n\<in>set (butlast (trace d i xsa)). n < k) \<and> deltas d xsa i = k \<and> (\<exists>xs ysa. ys = xs @ ysa \<and> xs \<in> star (regset d k k k) \<and> (\<forall>n\<in>set (butlast (trace d k ysa)). n < k) \<and> deltas d ysa k = j))
[PROOF STEP]
apply (erule disjE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>k i j xs. \<lbrakk>\<And>i j xs. (xs \<in> regset d i j k) = ((\<forall>n\<in>set (butlast (trace d i xs)). n < k) \<and> deltas d xs i = j); (\<forall>n\<in>set (butlast (trace d i xs)). n < k) \<and> deltas d xs i = j\<rbrakk> \<Longrightarrow> (\<forall>n\<in>set (butlast (trace d i xs)). n < Suc k) \<and> deltas d xs i = j
 2. \<And>k i j xs. \<lbrakk>\<And>i j xs. (xs \<in> regset d i j k) = ((\<forall>n\<in>set (butlast (trace d i xs)). n < k) \<and> deltas d xs i = j); \<exists>xsa ys. xs = xsa @ ys \<and> (\<forall>n\<in>set (butlast (trace d i xsa)). n < k) \<and> deltas d xsa i = k \<and> (\<exists>xs ysa. ys = xs @ ysa \<and> xs \<in> star (regset d k k k) \<and> (\<forall>n\<in>set (butlast (trace d k ysa)). n < k) \<and> deltas d ysa k = j)\<rbrakk> \<Longrightarrow> (\<forall>n\<in>set (butlast (trace d i xs)). n < Suc k) \<and> deltas d xs i = j
 3. \<And>k i j xs. \<lbrakk>\<And>i j xs. (xs \<in> regset d i j k) = ((\<forall>n\<in>set (butlast (trace d i xs)). n < k) \<and> deltas d xs i = j); (\<forall>n\<in>set (butlast (trace d i xs)). n < Suc k) \<and> deltas d xs i = j\<rbrakk> \<Longrightarrow> (\<forall>n\<in>set (butlast (trace d i xs)). n < k) \<and> deltas d xs i = j \<or> (\<exists>xsa ys. xs = xsa @ ys \<and> (\<forall>n\<in>set (butlast (trace d i xsa)). n < k) \<and> deltas d xsa i = k \<and> (\<exists>xs ysa. ys = xs @ ysa \<and> xs \<in> star (regset d k k k) \<and> (\<forall>n\<in>set (butlast (trace d k ysa)). n < k) \<and> deltas d ysa k = j))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>k i j xs. \<lbrakk>\<And>i j xs. (xs \<in> regset d i j k) = ((\<forall>n\<in>set (butlast (trace d i xs)). n < k) \<and> deltas d xs i = j); \<exists>xsa ys. xs = xsa @ ys \<and> (\<forall>n\<in>set (butlast (trace d i xsa)). n < k) \<and> deltas d xsa i = k \<and> (\<exists>xs ysa. ys = xs @ ysa \<and> xs \<in> star (regset d k k k) \<and> (\<forall>n\<in>set (butlast (trace d k ysa)). n < k) \<and> deltas d ysa k = j)\<rbrakk> \<Longrightarrow> (\<forall>n\<in>set (butlast (trace d i xs)). n < Suc k) \<and> deltas d xs i = j
 2. \<And>k i j xs. \<lbrakk>\<And>i j xs. (xs \<in> regset d i j k) = ((\<forall>n\<in>set (butlast (trace d i xs)). n < k) \<and> deltas d xs i = j); (\<forall>n\<in>set (butlast (trace d i xs)). n < Suc k) \<and> deltas d xs i = j\<rbrakk> \<Longrightarrow> (\<forall>n\<in>set (butlast (trace d i xs)). n < k) \<and> deltas d xs i = j \<or> (\<exists>xsa ys. xs = xsa @ ys \<and> (\<forall>n\<in>set (butlast (trace d i xsa)). n < k) \<and> deltas d xsa i = k \<and> (\<exists>xs ysa. ys = xs @ ysa \<and> xs \<in> star (regset d k k k) \<and> (\<forall>n\<in>set (butlast (trace d k ysa)). n < k) \<and> deltas d ysa k = j))
[PROOF STEP]
apply (erule exE conjE)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>k i j xs xsa ys xsb ysa. \<lbrakk>\<And>i j xs. (xs \<in> regset d i j k) = ((\<forall>n\<in>set (butlast (trace d i xs)). n < k) \<and> deltas d xs i = j); xs = xsa @ ys; \<forall>n\<in>set (butlast (trace d i xsa)). n < k; deltas d xsa i = k; ys = xsb @ ysa; xsb \<in> star (regset d k k k); \<forall>n\<in>set (butlast (trace d k ysa)). n < k; deltas d ysa k = j\<rbrakk> \<Longrightarrow> (\<forall>n\<in>set (butlast (trace d i xs)). n < Suc k) \<and> deltas d xs i = j
 2. \<And>k i j xs. \<lbrakk>\<And>i j xs. (xs \<in> regset d i j k) = ((\<forall>n\<in>set (butlast (trace d i xs)). n < k) \<and> deltas d xs i = j); (\<forall>n\<in>set (butlast (trace d i xs)). n < Suc k) \<and> deltas d xs i = j\<rbrakk> \<Longrightarrow> (\<forall>n\<in>set (butlast (trace d i xs)). n < k) \<and> deltas d xs i = j \<or> (\<exists>xsa ys. xs = xsa @ ys \<and> (\<forall>n\<in>set (butlast (trace d i xsa)). n < k) \<and> deltas d xsa i = k \<and> (\<exists>xs ysa. ys = xs @ ysa \<and> xs \<in> star (regset d k k k) \<and> (\<forall>n\<in>set (butlast (trace d k ysa)). n < k) \<and> deltas d ysa k = j))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>k i j xs xsa ys xsb ysa. \<lbrakk>\<And>i j xs. (xs \<in> regset d i j k) = ((\<forall>n\<in>set (butlast (trace d i xs)). n < k) \<and> deltas d xs i = j); xs = xsa @ xsb @ ysa; \<forall>n\<in>set (butlast (trace d i xsa)). n < k; deltas d xsa i = k; ys = xsb @ ysa; xsb \<in> star (regset d k k k); \<forall>n\<in>set (butlast (trace d k ysa)). n < k; deltas d ysa k = j\<rbrakk> \<Longrightarrow> (\<forall>n\<in>set (butlast (trace d i xsa @ trace d k xsb @ trace d (deltas d xsb k) ysa)). n < Suc k) \<and> deltas d ysa (deltas d xsb k) = j
 2. \<And>k i j xs. \<lbrakk>\<And>i j xs. (xs \<in> regset d i j k) = ((\<forall>n\<in>set (butlast (trace d i xs)). n < k) \<and> deltas d xs i = j); (\<forall>n\<in>set (butlast (trace d i xs)). n < Suc k) \<and> deltas d xs i = j\<rbrakk> \<Longrightarrow> (\<forall>n\<in>set (butlast (trace d i xs)). n < k) \<and> deltas d xs i = j \<or> (\<exists>xsa ys. xs = xsa @ ys \<and> (\<forall>n\<in>set (butlast (trace d i xsa)). n < k) \<and> deltas d xsa i = k \<and> (\<exists>xs ysa. ys = xs @ ysa \<and> xs \<in> star (regset d k k k) \<and> (\<forall>n\<in>set (butlast (trace d k ysa)). n < k) \<and> deltas d ysa k = j))
[PROOF STEP]
apply (subgoal_tac
      "(\<forall>m\<in>set(butlast(trace d k xsb)). m < Suc k) \<and> deltas d xsb k = k")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>k i j xs xsa ys xsb ysa. \<lbrakk>\<And>i j xs. (xs \<in> regset d i j k) = ((\<forall>n\<in>set (butlast (trace d i xs)). n < k) \<and> deltas d xs i = j); xs = xsa @ xsb @ ysa; \<forall>n\<in>set (butlast (trace d i xsa)). n < k; deltas d xsa i = k; ys = xsb @ ysa; xsb \<in> star (regset d k k k); \<forall>n\<in>set (butlast (trace d k ysa)). n < k; deltas d ysa k = j; (\<forall>m\<in>set (butlast (trace d k xsb)). m < Suc k) \<and> deltas d xsb k = k\<rbrakk> \<Longrightarrow> (\<forall>n\<in>set (butlast (trace d i xsa @ trace d k xsb @ trace d (deltas d xsb k) ysa)). n < Suc k) \<and> deltas d ysa (deltas d xsb k) = j
 2. \<And>k i j xs xsa ys xsb ysa. \<lbrakk>\<And>i j xs. (xs \<in> regset d i j k) = ((\<forall>n\<in>set (butlast (trace d i xs)). n < k) \<and> deltas d xs i = j); xs = xsa @ xsb @ ysa; \<forall>n\<in>set (butlast (trace d i xsa)). n < k; deltas d xsa i = k; ys = xsb @ ysa; xsb \<in> star (regset d k k k); \<forall>n\<in>set (butlast (trace d k ysa)). n < k; deltas d ysa k = j\<rbrakk> \<Longrightarrow> (\<forall>m\<in>set (butlast (trace d k xsb)). m < Suc k) \<and> deltas d xsb k = k
 3. \<And>k i j xs. \<lbrakk>\<And>i j xs. (xs \<in> regset d i j k) = ((\<forall>n\<in>set (butlast (trace d i xs)). n < k) \<and> deltas d xs i = j); (\<forall>n\<in>set (butlast (trace d i xs)). n < Suc k) \<and> deltas d xs i = j\<rbrakk> \<Longrightarrow> (\<forall>n\<in>set (butlast (trace d i xs)). n < k) \<and> deltas d xs i = j \<or> (\<exists>xsa ys. xs = xsa @ ys \<and> (\<forall>n\<in>set (butlast (trace d i xsa)). n < k) \<and> deltas d xsa i = k \<and> (\<exists>xs ysa. ys = xs @ ysa \<and> xs \<in> star (regset d k k k) \<and> (\<forall>n\<in>set (butlast (trace d k ysa)). n < k) \<and> deltas d ysa k = j))
[PROOF STEP]
apply (simp add: set_trace_conv butlast_append ball_Un)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>k i j xs xsa ys xsb ysa. \<lbrakk>\<And>i j xs. (xs \<in> regset d i j k) = ((\<forall>n\<in>set (butlast (trace d i xs)). n < k) \<and> deltas d xs i = j); xs = xsa @ xsb @ ysa; \<forall>n\<in>set (butlast (trace d i xsa)). n < k; deltas d xsa i = k; ys = xsb @ ysa; xsb \<in> star (regset d k k k); \<forall>n\<in>set (butlast (trace d k ysa)). n < k; deltas d ysa k = j\<rbrakk> \<Longrightarrow> (\<forall>m\<in>set (butlast (trace d k xsb)). m < Suc k) \<and> deltas d xsb k = k
 2. \<And>k i j xs. \<lbrakk>\<And>i j xs. (xs \<in> regset d i j k) = ((\<forall>n\<in>set (butlast (trace d i xs)). n < k) \<and> deltas d xs i = j); (\<forall>n\<in>set (butlast (trace d i xs)). n < Suc k) \<and> deltas d xs i = j\<rbrakk> \<Longrightarrow> (\<forall>n\<in>set (butlast (trace d i xs)). n < k) \<and> deltas d xs i = j \<or> (\<exists>xsa ys. xs = xsa @ ys \<and> (\<forall>n\<in>set (butlast (trace d i xsa)). n < k) \<and> deltas d xsa i = k \<and> (\<exists>xs ysa. ys = xs @ ysa \<and> xs \<in> star (regset d k k k) \<and> (\<forall>n\<in>set (butlast (trace d k ysa)). n < k) \<and> deltas d ysa k = j))
[PROOF STEP]
apply (erule star_induct)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>k i j xs xsa ys xsb ysa. \<lbrakk>\<And>i j xs. (xs \<in> regset d i j k) = ((\<forall>n\<in>set (butlast (trace d i xs)). n < k) \<and> deltas d xs i = j); xs = xsa @ xsb @ ysa; \<forall>n\<in>set (butlast (trace d i xsa)). n < k; deltas d xsa i = k; ys = xsb @ ysa; \<forall>n\<in>set (butlast (trace d k ysa)). n < k; deltas d ysa k = j\<rbrakk> \<Longrightarrow> (\<forall>m\<in>set (butlast (trace d k [])). m < Suc k) \<and> deltas d [] k = k
 2. \<And>k i j xs xsa ys xsb ysa u v. \<lbrakk>\<And>i j xs. (xs \<in> regset d i j k) = ((\<forall>n\<in>set (butlast (trace d i xs)). n < k) \<and> deltas d xs i = j); xs = xsa @ xsb @ ysa; \<forall>n\<in>set (butlast (trace d i xsa)). n < k; deltas d xsa i = k; ys = xsb @ ysa; \<forall>n\<in>set (butlast (trace d k ysa)). n < k; deltas d ysa k = j; u \<in> regset d k k k; v \<in> star (regset d k k k); (\<forall>m\<in>set (butlast (trace d k v)). m < Suc k) \<and> deltas d v k = k\<rbrakk> \<Longrightarrow> (\<forall>m\<in>set (butlast (trace d k (u @ v))). m < Suc k) \<and> deltas d (u @ v) k = k
 3. \<And>k i j xs. \<lbrakk>\<And>i j xs. (xs \<in> regset d i j k) = ((\<forall>n\<in>set (butlast (trace d i xs)). n < k) \<and> deltas d xs i = j); (\<forall>n\<in>set (butlast (trace d i xs)). n < Suc k) \<and> deltas d xs i = j\<rbrakk> \<Longrightarrow> (\<forall>n\<in>set (butlast (trace d i xs)). n < k) \<and> deltas d xs i = j \<or> (\<exists>xsa ys. xs = xsa @ ys \<and> (\<forall>n\<in>set (butlast (trace d i xsa)). n < k) \<and> deltas d xsa i = k \<and> (\<exists>xs ysa. ys = xs @ ysa \<and> xs \<in> star (regset d k k k) \<and> (\<forall>n\<in>set (butlast (trace d k ysa)). n < k) \<and> deltas d ysa k = j))
[PROOF STEP]
apply (simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>k i j xs xsa ys xsb ysa u v. \<lbrakk>\<And>i j xs. (xs \<in> regset d i j k) = ((\<forall>n\<in>set (butlast (trace d i xs)). n < k) \<and> deltas d xs i = j); xs = xsa @ xsb @ ysa; \<forall>n\<in>set (butlast (trace d i xsa)). n < k; deltas d xsa i = k; ys = xsb @ ysa; \<forall>n\<in>set (butlast (trace d k ysa)). n < k; deltas d ysa k = j; u \<in> regset d k k k; v \<in> star (regset d k k k); (\<forall>m\<in>set (butlast (trace d k v)). m < Suc k) \<and> deltas d v k = k\<rbrakk> \<Longrightarrow> (\<forall>m\<in>set (butlast (trace d k (u @ v))). m < Suc k) \<and> deltas d (u @ v) k = k
 2. \<And>k i j xs. \<lbrakk>\<And>i j xs. (xs \<in> regset d i j k) = ((\<forall>n\<in>set (butlast (trace d i xs)). n < k) \<and> deltas d xs i = j); (\<forall>n\<in>set (butlast (trace d i xs)). n < Suc k) \<and> deltas d xs i = j\<rbrakk> \<Longrightarrow> (\<forall>n\<in>set (butlast (trace d i xs)). n < k) \<and> deltas d xs i = j \<or> (\<exists>xsa ys. xs = xsa @ ys \<and> (\<forall>n\<in>set (butlast (trace d i xsa)). n < k) \<and> deltas d xsa i = k \<and> (\<exists>xs ysa. ys = xs @ ysa \<and> xs \<in> star (regset d k k k) \<and> (\<forall>n\<in>set (butlast (trace d k ysa)). n < k) \<and> deltas d ysa k = j))
[PROOF STEP]
apply (simp add: set_trace_conv butlast_append ball_Un)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k i j xs. \<lbrakk>\<And>i j xs. (xs \<in> regset d i j k) = ((\<forall>n\<in>set (butlast (trace d i xs)). n < k) \<and> deltas d xs i = j); (\<forall>n\<in>set (butlast (trace d i xs)). n < Suc k) \<and> deltas d xs i = j\<rbrakk> \<Longrightarrow> (\<forall>n\<in>set (butlast (trace d i xs)). n < k) \<and> deltas d xs i = j \<or> (\<exists>xsa ys. xs = xsa @ ys \<and> (\<forall>n\<in>set (butlast (trace d i xsa)). n < k) \<and> deltas d xsa i = k \<and> (\<exists>xs ysa. ys = xs @ ysa \<and> xs \<in> star (regset d k k k) \<and> (\<forall>n\<in>set (butlast (trace d k ysa)). n < k) \<and> deltas d ysa k = j))
[PROOF STEP]
apply (case_tac "k : set(butlast(trace d i xs))")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>k i j xs. \<lbrakk>\<And>i j xs. (xs \<in> regset d i j k) = ((\<forall>n\<in>set (butlast (trace d i xs)). n < k) \<and> deltas d xs i = j); (\<forall>n\<in>set (butlast (trace d i xs)). n < Suc k) \<and> deltas d xs i = j; k \<in> set (butlast (trace d i xs))\<rbrakk> \<Longrightarrow> (\<forall>n\<in>set (butlast (trace d i xs)). n < k) \<and> deltas d xs i = j \<or> (\<exists>xsa ys. xs = xsa @ ys \<and> (\<forall>n\<in>set (butlast (trace d i xsa)). n < k) \<and> deltas d xsa i = k \<and> (\<exists>xs ysa. ys = xs @ ysa \<and> xs \<in> star (regset d k k k) \<and> (\<forall>n\<in>set (butlast (trace d k ysa)). n < k) \<and> deltas d ysa k = j))
 2. \<And>k i j xs. \<lbrakk>\<And>i j xs. (xs \<in> regset d i j k) = ((\<forall>n\<in>set (butlast (trace d i xs)). n < k) \<and> deltas d xs i = j); (\<forall>n\<in>set (butlast (trace d i xs)). n < Suc k) \<and> deltas d xs i = j; k \<notin> set (butlast (trace d i xs))\<rbrakk> \<Longrightarrow> (\<forall>n\<in>set (butlast (trace d i xs)). n < k) \<and> deltas d xs i = j \<or> (\<exists>xsa ys. xs = xsa @ ys \<and> (\<forall>n\<in>set (butlast (trace d i xsa)). n < k) \<and> deltas d xsa i = k \<and> (\<exists>xs ysa. ys = xs @ ysa \<and> xs \<in> star (regset d k k k) \<and> (\<forall>n\<in>set (butlast (trace d k ysa)). n < k) \<and> deltas d ysa k = j))
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>k i j xs. \<lbrakk>\<And>i j xs. (xs \<in> regset d i j k) = ((\<forall>n\<in>set (butlast (trace d i xs)). n < k) \<and> deltas d xs i = j); (\<forall>n\<in>set (butlast (trace d i xs)). n < Suc k) \<and> deltas d xs i = j; k \<notin> set (butlast (trace d i xs))\<rbrakk> \<Longrightarrow> (\<forall>n\<in>set (butlast (trace d i xs)). n < k) \<and> deltas d xs i = j \<or> (\<exists>xsa ys. xs = xsa @ ys \<and> (\<forall>n\<in>set (butlast (trace d i xsa)). n < k) \<and> deltas d xsa i = k \<and> (\<exists>xs ysa. ys = xs @ ysa \<and> xs \<in> star (regset d k k k) \<and> (\<forall>n\<in>set (butlast (trace d k ysa)). n < k) \<and> deltas d ysa k = j))
 2. \<And>k i j xs. \<lbrakk>\<And>i j xs. (xs \<in> regset d i j k) = ((\<forall>n\<in>set (butlast (trace d i xs)). n < k) \<and> deltas d xs i = j); (\<forall>n\<in>set (butlast (trace d i xs)). n < Suc k) \<and> deltas d xs i = j; k \<in> set (butlast (trace d i xs))\<rbrakk> \<Longrightarrow> (\<forall>n\<in>set (butlast (trace d i xs)). n < k) \<and> deltas d xs i = j \<or> (\<exists>xsa ys. xs = xsa @ ys \<and> (\<forall>n\<in>set (butlast (trace d i xsa)). n < k) \<and> deltas d xsa i = k \<and> (\<exists>xs ysa. ys = xs @ ysa \<and> xs \<in> star (regset d k k k) \<and> (\<forall>n\<in>set (butlast (trace d k ysa)). n < k) \<and> deltas d ysa k = j))
[PROOF STEP]
apply (rule disjI1)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>k i j xs. \<lbrakk>\<And>i j xs. (xs \<in> regset d i j k) = ((\<forall>n\<in>set (butlast (trace d i xs)). n < k) \<and> deltas d xs i = j); (\<forall>n\<in>set (butlast (trace d i xs)). n < Suc k) \<and> deltas d xs i = j; k \<notin> set (butlast (trace d i xs))\<rbrakk> \<Longrightarrow> (\<forall>n\<in>set (butlast (trace d i xs)). n < k) \<and> deltas d xs i = j
 2. \<And>k i j xs. \<lbrakk>\<And>i j xs. (xs \<in> regset d i j k) = ((\<forall>n\<in>set (butlast (trace d i xs)). n < k) \<and> deltas d xs i = j); (\<forall>n\<in>set (butlast (trace d i xs)). n < Suc k) \<and> deltas d xs i = j; k \<in> set (butlast (trace d i xs))\<rbrakk> \<Longrightarrow> (\<forall>n\<in>set (butlast (trace d i xs)). n < k) \<and> deltas d xs i = j \<or> (\<exists>xsa ys. xs = xsa @ ys \<and> (\<forall>n\<in>set (butlast (trace d i xsa)). n < k) \<and> deltas d xsa i = k \<and> (\<exists>xs ysa. ys = xs @ ysa \<and> xs \<in> star (regset d k k k) \<and> (\<forall>n\<in>set (butlast (trace d k ysa)). n < k) \<and> deltas d ysa k = j))
[PROOF STEP]
apply (blast intro:lem)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k i j xs. \<lbrakk>\<And>i j xs. (xs \<in> regset d i j k) = ((\<forall>n\<in>set (butlast (trace d i xs)). n < k) \<and> deltas d xs i = j); (\<forall>n\<in>set (butlast (trace d i xs)). n < Suc k) \<and> deltas d xs i = j; k \<in> set (butlast (trace d i xs))\<rbrakk> \<Longrightarrow> (\<forall>n\<in>set (butlast (trace d i xs)). n < k) \<and> deltas d xs i = j \<or> (\<exists>xsa ys. xs = xsa @ ys \<and> (\<forall>n\<in>set (butlast (trace d i xsa)). n < k) \<and> deltas d xsa i = k \<and> (\<exists>xs ysa. ys = xs @ ysa \<and> xs \<in> star (regset d k k k) \<and> (\<forall>n\<in>set (butlast (trace d k ysa)). n < k) \<and> deltas d ysa k = j))
[PROOF STEP]
apply (rule disjI2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k i j xs. \<lbrakk>\<And>i j xs. (xs \<in> regset d i j k) = ((\<forall>n\<in>set (butlast (trace d i xs)). n < k) \<and> deltas d xs i = j); (\<forall>n\<in>set (butlast (trace d i xs)). n < Suc k) \<and> deltas d xs i = j; k \<in> set (butlast (trace d i xs))\<rbrakk> \<Longrightarrow> \<exists>xsa ys. xs = xsa @ ys \<and> (\<forall>n\<in>set (butlast (trace d i xsa)). n < k) \<and> deltas d xsa i = k \<and> (\<exists>xs ysa. ys = xs @ ysa \<and> xs \<in> star (regset d k k k) \<and> (\<forall>n\<in>set (butlast (trace d k ysa)). n < k) \<and> deltas d ysa k = j)
[PROOF STEP]
apply (drule in_set_butlastD[THEN decompose])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k i j xs. \<lbrakk>\<And>i j xs. (xs \<in> regset d i j k) = ((\<forall>n\<in>set (butlast (trace d i xs)). n < k) \<and> deltas d xs i = j); (\<forall>n\<in>set (butlast (trace d i xs)). n < Suc k) \<and> deltas d xs i = j; \<exists>pref mids suf. xs = pref @ concat mids @ suf \<and> deltas d pref i = k \<and> (\<forall>n\<in>set (butlast (trace d i pref)). n \<noteq> k) \<and> (\<forall>mid\<in>set mids. deltas d mid k = k \<and> (\<forall>n\<in>set (butlast (trace d k mid)). n \<noteq> k)) \<and> (\<forall>n\<in>set (butlast (trace d k suf)). n \<noteq> k)\<rbrakk> \<Longrightarrow> \<exists>xsa ys. xs = xsa @ ys \<and> (\<forall>n\<in>set (butlast (trace d i xsa)). n < k) \<and> deltas d xsa i = k \<and> (\<exists>xs ysa. ys = xs @ ysa \<and> xs \<in> star (regset d k k k) \<and> (\<forall>n\<in>set (butlast (trace d k ysa)). n < k) \<and> deltas d ysa k = j)
[PROOF STEP]
apply (clarify)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k i j xs pref mids suf. \<lbrakk>\<And>ia j xs. (xs \<in> regset d ia j (deltas d pref i)) = ((\<forall>n\<in>set (butlast (trace d ia xs)). n < deltas d pref i) \<and> deltas d xs ia = j); \<forall>n\<in>set (butlast (trace d i (pref @ concat mids @ suf))). n < Suc (deltas d pref i); \<forall>n\<in>set (butlast (trace d i pref)). n \<noteq> deltas d pref i; \<forall>mid\<in>set mids. deltas d mid (deltas d pref i) = deltas d pref i \<and> (\<forall>n\<in>set (butlast (trace d (deltas d pref i) mid)). n \<noteq> deltas d pref i); \<forall>n\<in>set (butlast (trace d (deltas d pref i) suf)). n \<noteq> deltas d pref i\<rbrakk> \<Longrightarrow> \<exists>xs ys. pref @ concat mids @ suf = xs @ ys \<and> (\<forall>n\<in>set (butlast (trace d i xs)). n < deltas d pref i) \<and> deltas d xs i = deltas d pref i \<and> (\<exists>xs ysa. ys = xs @ ysa \<and> xs \<in> star (regset d (deltas d pref i) (deltas d pref i) (deltas d pref i)) \<and> (\<forall>n\<in>set (butlast (trace d (deltas d pref i) ysa)). n < deltas d pref i) \<and> deltas d ysa (deltas d pref i) = deltas d (pref @ concat mids @ suf) i)
[PROOF STEP]
apply (rule_tac x = "pref" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k i j xs pref mids suf. \<lbrakk>\<And>ia j xs. (xs \<in> regset d ia j (deltas d pref i)) = ((\<forall>n\<in>set (butlast (trace d ia xs)). n < deltas d pref i) \<and> deltas d xs ia = j); \<forall>n\<in>set (butlast (trace d i (pref @ concat mids @ suf))). n < Suc (deltas d pref i); \<forall>n\<in>set (butlast (trace d i pref)). n \<noteq> deltas d pref i; \<forall>mid\<in>set mids. deltas d mid (deltas d pref i) = deltas d pref i \<and> (\<forall>n\<in>set (butlast (trace d (deltas d pref i) mid)). n \<noteq> deltas d pref i); \<forall>n\<in>set (butlast (trace d (deltas d pref i) suf)). n \<noteq> deltas d pref i\<rbrakk> \<Longrightarrow> \<exists>ys. pref @ concat mids @ suf = pref @ ys \<and> (\<forall>n\<in>set (butlast (trace d i pref)). n < deltas d pref i) \<and> deltas d pref i = deltas d pref i \<and> (\<exists>xs ysa. ys = xs @ ysa \<and> xs \<in> star (regset d (deltas d pref i) (deltas d pref i) (deltas d pref i)) \<and> (\<forall>n\<in>set (butlast (trace d (deltas d pref i) ysa)). n < deltas d pref i) \<and> deltas d ysa (deltas d pref i) = deltas d (pref @ concat mids @ suf) i)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i pref mids suf. \<lbrakk>\<And>ia j xs. (xs \<in> regset d ia j (deltas d pref i)) = ((\<forall>n\<in>set (butlast (trace d ia xs)). n < deltas d pref i) \<and> deltas d xs ia = j); \<forall>n\<in>set (butlast (trace d i pref @ concat (map (trace d (deltas d pref i)) mids) @ trace d (deltas d pref i) suf)). n < Suc (deltas d pref i); \<forall>n\<in>set (butlast (trace d i pref)). n \<noteq> deltas d pref i; \<forall>mid\<in>set mids. deltas d mid (deltas d pref i) = deltas d pref i \<and> (\<forall>n\<in>set (butlast (trace d (deltas d pref i) mid)). n \<noteq> deltas d pref i); \<forall>n\<in>set (butlast (trace d (deltas d pref i) suf)). n \<noteq> deltas d pref i\<rbrakk> \<Longrightarrow> (\<forall>n\<in>set (butlast (trace d i pref)). n < deltas d pref i) \<and> (\<exists>xs ys. concat mids @ suf = xs @ ys \<and> xs \<in> star (regset d (deltas d pref i) (deltas d pref i) (deltas d pref i)) \<and> (\<forall>n\<in>set (butlast (trace d (deltas d pref i) ys)). n < deltas d pref i) \<and> deltas d ys (deltas d pref i) = deltas d suf (deltas d pref i))
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i pref mids suf. \<lbrakk>\<And>ia j xs. (xs \<in> regset d ia j (deltas d pref i)) = ((\<forall>n\<in>set (butlast (trace d ia xs)). n < deltas d pref i) \<and> deltas d xs ia = j); \<forall>n\<in>set (butlast (trace d i pref @ concat (map (trace d (deltas d pref i)) mids) @ trace d (deltas d pref i) suf)). n < Suc (deltas d pref i); \<forall>n\<in>set (butlast (trace d i pref)). n \<noteq> deltas d pref i; \<forall>mid\<in>set mids. deltas d mid (deltas d pref i) = deltas d pref i \<and> (\<forall>n\<in>set (butlast (trace d (deltas d pref i) mid)). n \<noteq> deltas d pref i); \<forall>n\<in>set (butlast (trace d (deltas d pref i) suf)). n \<noteq> deltas d pref i\<rbrakk> \<Longrightarrow> \<forall>n\<in>set (butlast (trace d i pref)). n < deltas d pref i
 2. \<And>i pref mids suf. \<lbrakk>\<And>ia j xs. (xs \<in> regset d ia j (deltas d pref i)) = ((\<forall>n\<in>set (butlast (trace d ia xs)). n < deltas d pref i) \<and> deltas d xs ia = j); \<forall>n\<in>set (butlast (trace d i pref @ concat (map (trace d (deltas d pref i)) mids) @ trace d (deltas d pref i) suf)). n < Suc (deltas d pref i); \<forall>n\<in>set (butlast (trace d i pref)). n \<noteq> deltas d pref i; \<forall>mid\<in>set mids. deltas d mid (deltas d pref i) = deltas d pref i \<and> (\<forall>n\<in>set (butlast (trace d (deltas d pref i) mid)). n \<noteq> deltas d pref i); \<forall>n\<in>set (butlast (trace d (deltas d pref i) suf)). n \<noteq> deltas d pref i\<rbrakk> \<Longrightarrow> \<exists>xs ys. concat mids @ suf = xs @ ys \<and> xs \<in> star (regset d (deltas d pref i) (deltas d pref i) (deltas d pref i)) \<and> (\<forall>n\<in>set (butlast (trace d (deltas d pref i) ys)). n < deltas d pref i) \<and> deltas d ys (deltas d pref i) = deltas d suf (deltas d pref i)
[PROOF STEP]
apply (rule ballI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i pref mids suf n. \<lbrakk>\<And>ia j xs. (xs \<in> regset d ia j (deltas d pref i)) = ((\<forall>n\<in>set (butlast (trace d ia xs)). n < deltas d pref i) \<and> deltas d xs ia = j); \<forall>n\<in>set (butlast (trace d i pref @ concat (map (trace d (deltas d pref i)) mids) @ trace d (deltas d pref i) suf)). n < Suc (deltas d pref i); \<forall>n\<in>set (butlast (trace d i pref)). n \<noteq> deltas d pref i; \<forall>mid\<in>set mids. deltas d mid (deltas d pref i) = deltas d pref i \<and> (\<forall>n\<in>set (butlast (trace d (deltas d pref i) mid)). n \<noteq> deltas d pref i); \<forall>n\<in>set (butlast (trace d (deltas d pref i) suf)). n \<noteq> deltas d pref i; n \<in> set (butlast (trace d i pref))\<rbrakk> \<Longrightarrow> n < deltas d pref i
 2. \<And>i pref mids suf. \<lbrakk>\<And>ia j xs. (xs \<in> regset d ia j (deltas d pref i)) = ((\<forall>n\<in>set (butlast (trace d ia xs)). n < deltas d pref i) \<and> deltas d xs ia = j); \<forall>n\<in>set (butlast (trace d i pref @ concat (map (trace d (deltas d pref i)) mids) @ trace d (deltas d pref i) suf)). n < Suc (deltas d pref i); \<forall>n\<in>set (butlast (trace d i pref)). n \<noteq> deltas d pref i; \<forall>mid\<in>set mids. deltas d mid (deltas d pref i) = deltas d pref i \<and> (\<forall>n\<in>set (butlast (trace d (deltas d pref i) mid)). n \<noteq> deltas d pref i); \<forall>n\<in>set (butlast (trace d (deltas d pref i) suf)). n \<noteq> deltas d pref i\<rbrakk> \<Longrightarrow> \<exists>xs ys. concat mids @ suf = xs @ ys \<and> xs \<in> star (regset d (deltas d pref i) (deltas d pref i) (deltas d pref i)) \<and> (\<forall>n\<in>set (butlast (trace d (deltas d pref i) ys)). n < deltas d pref i) \<and> deltas d ys (deltas d pref i) = deltas d suf (deltas d pref i)
[PROOF STEP]
apply (rule lem)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>i pref mids suf n. \<lbrakk>\<And>ia j xs. (xs \<in> regset d ia j (deltas d pref i)) = ((\<forall>n\<in>set (butlast (trace d ia xs)). n < deltas d pref i) \<and> deltas d xs ia = j); \<forall>n\<in>set (butlast (trace d i pref @ concat (map (trace d (deltas d pref i)) mids) @ trace d (deltas d pref i) suf)). n < Suc (deltas d pref i); \<forall>n\<in>set (butlast (trace d i pref)). n \<noteq> deltas d pref i; \<forall>mid\<in>set mids. deltas d mid (deltas d pref i) = deltas d pref i \<and> (\<forall>n\<in>set (butlast (trace d (deltas d pref i) mid)). n \<noteq> deltas d pref i); \<forall>n\<in>set (butlast (trace d (deltas d pref i) suf)). n \<noteq> deltas d pref i; n \<in> set (butlast (trace d i pref))\<rbrakk> \<Longrightarrow> n < Suc (deltas d pref i)
 2. \<And>i pref mids suf n. \<lbrakk>\<And>ia j xs. (xs \<in> regset d ia j (deltas d pref i)) = ((\<forall>n\<in>set (butlast (trace d ia xs)). n < deltas d pref i) \<and> deltas d xs ia = j); \<forall>n\<in>set (butlast (trace d i pref @ concat (map (trace d (deltas d pref i)) mids) @ trace d (deltas d pref i) suf)). n < Suc (deltas d pref i); \<forall>n\<in>set (butlast (trace d i pref)). n \<noteq> deltas d pref i; \<forall>mid\<in>set mids. deltas d mid (deltas d pref i) = deltas d pref i \<and> (\<forall>n\<in>set (butlast (trace d (deltas d pref i) mid)). n \<noteq> deltas d pref i); \<forall>n\<in>set (butlast (trace d (deltas d pref i) suf)). n \<noteq> deltas d pref i; n \<in> set (butlast (trace d i pref))\<rbrakk> \<Longrightarrow> n \<noteq> deltas d pref i
 3. \<And>i pref mids suf. \<lbrakk>\<And>ia j xs. (xs \<in> regset d ia j (deltas d pref i)) = ((\<forall>n\<in>set (butlast (trace d ia xs)). n < deltas d pref i) \<and> deltas d xs ia = j); \<forall>n\<in>set (butlast (trace d i pref @ concat (map (trace d (deltas d pref i)) mids) @ trace d (deltas d pref i) suf)). n < Suc (deltas d pref i); \<forall>n\<in>set (butlast (trace d i pref)). n \<noteq> deltas d pref i; \<forall>mid\<in>set mids. deltas d mid (deltas d pref i) = deltas d pref i \<and> (\<forall>n\<in>set (butlast (trace d (deltas d pref i) mid)). n \<noteq> deltas d pref i); \<forall>n\<in>set (butlast (trace d (deltas d pref i) suf)). n \<noteq> deltas d pref i\<rbrakk> \<Longrightarrow> \<exists>xs ys. concat mids @ suf = xs @ ys \<and> xs \<in> star (regset d (deltas d pref i) (deltas d pref i) (deltas d pref i)) \<and> (\<forall>n\<in>set (butlast (trace d (deltas d pref i) ys)). n < deltas d pref i) \<and> deltas d ys (deltas d pref i) = deltas d suf (deltas d pref i)
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>i pref mids suf n. \<lbrakk>\<And>ia j xs. (xs \<in> regset d ia j (deltas d pref i)) = ((\<forall>n\<in>set (butlast (trace d ia xs)). n < deltas d pref i) \<and> deltas d xs ia = j); \<forall>n\<in>set (butlast (trace d i pref @ concat (map (trace d (deltas d pref i)) mids) @ trace d (deltas d pref i) suf)). n < Suc (deltas d pref i); \<forall>n\<in>set (butlast (trace d i pref)). n \<noteq> deltas d pref i; \<forall>mid\<in>set mids. deltas d mid (deltas d pref i) = deltas d pref i \<and> (\<forall>n\<in>set (butlast (trace d (deltas d pref i) mid)). n \<noteq> deltas d pref i); \<forall>n\<in>set (butlast (trace d (deltas d pref i) suf)). n \<noteq> deltas d pref i; n \<in> set (butlast (trace d i pref))\<rbrakk> \<Longrightarrow> n \<noteq> deltas d pref i
 2. \<And>i pref mids suf n. \<lbrakk>\<And>ia j xs. (xs \<in> regset d ia j (deltas d pref i)) = ((\<forall>n\<in>set (butlast (trace d ia xs)). n < deltas d pref i) \<and> deltas d xs ia = j); \<forall>n\<in>set (butlast (trace d i pref @ concat (map (trace d (deltas d pref i)) mids) @ trace d (deltas d pref i) suf)). n < Suc (deltas d pref i); \<forall>n\<in>set (butlast (trace d i pref)). n \<noteq> deltas d pref i; \<forall>mid\<in>set mids. deltas d mid (deltas d pref i) = deltas d pref i \<and> (\<forall>n\<in>set (butlast (trace d (deltas d pref i) mid)). n \<noteq> deltas d pref i); \<forall>n\<in>set (butlast (trace d (deltas d pref i) suf)). n \<noteq> deltas d pref i; n \<in> set (butlast (trace d i pref))\<rbrakk> \<Longrightarrow> n < Suc (deltas d pref i)
 3. \<And>i pref mids suf. \<lbrakk>\<And>ia j xs. (xs \<in> regset d ia j (deltas d pref i)) = ((\<forall>n\<in>set (butlast (trace d ia xs)). n < deltas d pref i) \<and> deltas d xs ia = j); \<forall>n\<in>set (butlast (trace d i pref @ concat (map (trace d (deltas d pref i)) mids) @ trace d (deltas d pref i) suf)). n < Suc (deltas d pref i); \<forall>n\<in>set (butlast (trace d i pref)). n \<noteq> deltas d pref i; \<forall>mid\<in>set mids. deltas d mid (deltas d pref i) = deltas d pref i \<and> (\<forall>n\<in>set (butlast (trace d (deltas d pref i) mid)). n \<noteq> deltas d pref i); \<forall>n\<in>set (butlast (trace d (deltas d pref i) suf)). n \<noteq> deltas d pref i\<rbrakk> \<Longrightarrow> \<exists>xs ys. concat mids @ suf = xs @ ys \<and> xs \<in> star (regset d (deltas d pref i) (deltas d pref i) (deltas d pref i)) \<and> (\<forall>n\<in>set (butlast (trace d (deltas d pref i) ys)). n < deltas d pref i) \<and> deltas d ys (deltas d pref i) = deltas d suf (deltas d pref i)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i pref mids suf n. \<lbrakk>\<And>ia j xs. (xs \<in> regset d ia j (deltas d pref i)) = ((\<forall>n\<in>set (butlast (trace d ia xs)). n < deltas d pref i) \<and> deltas d xs ia = j); \<forall>n\<in>set (butlast (trace d i pref @ concat (map (trace d (deltas d pref i)) mids) @ trace d (deltas d pref i) suf)). n < Suc (deltas d pref i); \<forall>n\<in>set (butlast (trace d i pref)). n \<noteq> deltas d pref i; \<forall>mid\<in>set mids. deltas d mid (deltas d pref i) = deltas d pref i \<and> (\<forall>n\<in>set (butlast (trace d (deltas d pref i) mid)). n \<noteq> deltas d pref i); \<forall>n\<in>set (butlast (trace d (deltas d pref i) suf)). n \<noteq> deltas d pref i; n \<in> set (butlast (trace d i pref))\<rbrakk> \<Longrightarrow> n < Suc (deltas d pref i)
 2. \<And>i pref mids suf. \<lbrakk>\<And>ia j xs. (xs \<in> regset d ia j (deltas d pref i)) = ((\<forall>n\<in>set (butlast (trace d ia xs)). n < deltas d pref i) \<and> deltas d xs ia = j); \<forall>n\<in>set (butlast (trace d i pref @ concat (map (trace d (deltas d pref i)) mids) @ trace d (deltas d pref i) suf)). n < Suc (deltas d pref i); \<forall>n\<in>set (butlast (trace d i pref)). n \<noteq> deltas d pref i; \<forall>mid\<in>set mids. deltas d mid (deltas d pref i) = deltas d pref i \<and> (\<forall>n\<in>set (butlast (trace d (deltas d pref i) mid)). n \<noteq> deltas d pref i); \<forall>n\<in>set (butlast (trace d (deltas d pref i) suf)). n \<noteq> deltas d pref i\<rbrakk> \<Longrightarrow> \<exists>xs ys. concat mids @ suf = xs @ ys \<and> xs \<in> star (regset d (deltas d pref i) (deltas d pref i) (deltas d pref i)) \<and> (\<forall>n\<in>set (butlast (trace d (deltas d pref i) ys)). n < deltas d pref i) \<and> deltas d ys (deltas d pref i) = deltas d suf (deltas d pref i)
[PROOF STEP]
apply (drule bspec)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>i pref mids suf n. \<lbrakk>\<And>ia j xs. (xs \<in> regset d ia j (deltas d pref i)) = ((\<forall>n\<in>set (butlast (trace d ia xs)). n < deltas d pref i) \<and> deltas d xs ia = j); \<forall>n\<in>set (butlast (trace d i pref)). n \<noteq> deltas d pref i; \<forall>mid\<in>set mids. deltas d mid (deltas d pref i) = deltas d pref i \<and> (\<forall>n\<in>set (butlast (trace d (deltas d pref i) mid)). n \<noteq> deltas d pref i); \<forall>n\<in>set (butlast (trace d (deltas d pref i) suf)). n \<noteq> deltas d pref i; n \<in> set (butlast (trace d i pref))\<rbrakk> \<Longrightarrow> ?n195 i pref mids suf n \<in> set (butlast (trace d i pref @ concat (map (trace d (deltas d pref i)) mids) @ trace d (deltas d pref i) suf))
 2. \<And>i pref mids suf n. \<lbrakk>\<And>ia j xs. (xs \<in> regset d ia j (deltas d pref i)) = ((\<forall>n\<in>set (butlast (trace d ia xs)). n < deltas d pref i) \<and> deltas d xs ia = j); \<forall>n\<in>set (butlast (trace d i pref)). n \<noteq> deltas d pref i; \<forall>mid\<in>set mids. deltas d mid (deltas d pref i) = deltas d pref i \<and> (\<forall>n\<in>set (butlast (trace d (deltas d pref i) mid)). n \<noteq> deltas d pref i); \<forall>n\<in>set (butlast (trace d (deltas d pref i) suf)). n \<noteq> deltas d pref i; n \<in> set (butlast (trace d i pref)); ?n195 i pref mids suf n < Suc (deltas d pref i)\<rbrakk> \<Longrightarrow> n < Suc (deltas d pref i)
 3. \<And>i pref mids suf. \<lbrakk>\<And>ia j xs. (xs \<in> regset d ia j (deltas d pref i)) = ((\<forall>n\<in>set (butlast (trace d ia xs)). n < deltas d pref i) \<and> deltas d xs ia = j); \<forall>n\<in>set (butlast (trace d i pref @ concat (map (trace d (deltas d pref i)) mids) @ trace d (deltas d pref i) suf)). n < Suc (deltas d pref i); \<forall>n\<in>set (butlast (trace d i pref)). n \<noteq> deltas d pref i; \<forall>mid\<in>set mids. deltas d mid (deltas d pref i) = deltas d pref i \<and> (\<forall>n\<in>set (butlast (trace d (deltas d pref i) mid)). n \<noteq> deltas d pref i); \<forall>n\<in>set (butlast (trace d (deltas d pref i) suf)). n \<noteq> deltas d pref i\<rbrakk> \<Longrightarrow> \<exists>xs ys. concat mids @ suf = xs @ ys \<and> xs \<in> star (regset d (deltas d pref i) (deltas d pref i) (deltas d pref i)) \<and> (\<forall>n\<in>set (butlast (trace d (deltas d pref i) ys)). n < deltas d pref i) \<and> deltas d ys (deltas d pref i) = deltas d suf (deltas d pref i)
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>i pref mids suf n. \<lbrakk>\<And>ia j xs. (xs \<in> regset d ia j (deltas d pref i)) = ((\<forall>n\<in>set (butlast (trace d ia xs)). n < deltas d pref i) \<and> deltas d xs ia = j); \<forall>n\<in>set (butlast (trace d i pref)). n \<noteq> deltas d pref i; \<forall>mid\<in>set mids. deltas d mid (deltas d pref i) = deltas d pref i \<and> (\<forall>n\<in>set (butlast (trace d (deltas d pref i) mid)). n \<noteq> deltas d pref i); \<forall>n\<in>set (butlast (trace d (deltas d pref i) suf)). n \<noteq> deltas d pref i; n \<in> set (butlast (trace d i pref)); ?n195 i pref mids suf n < Suc (deltas d pref i)\<rbrakk> \<Longrightarrow> n < Suc (deltas d pref i)
 2. \<And>i pref mids suf n. \<lbrakk>\<And>ia j xs. (xs \<in> regset d ia j (deltas d pref i)) = ((\<forall>n\<in>set (butlast (trace d ia xs)). n < deltas d pref i) \<and> deltas d xs ia = j); \<forall>n\<in>set (butlast (trace d i pref)). n \<noteq> deltas d pref i; \<forall>mid\<in>set mids. deltas d mid (deltas d pref i) = deltas d pref i \<and> (\<forall>n\<in>set (butlast (trace d (deltas d pref i) mid)). n \<noteq> deltas d pref i); \<forall>n\<in>set (butlast (trace d (deltas d pref i) suf)). n \<noteq> deltas d pref i; n \<in> set (butlast (trace d i pref))\<rbrakk> \<Longrightarrow> ?n195 i pref mids suf n \<in> set (butlast (trace d i pref @ concat (map (trace d (deltas d pref i)) mids) @ trace d (deltas d pref i) suf))
 3. \<And>i pref mids suf. \<lbrakk>\<And>ia j xs. (xs \<in> regset d ia j (deltas d pref i)) = ((\<forall>n\<in>set (butlast (trace d ia xs)). n < deltas d pref i) \<and> deltas d xs ia = j); \<forall>n\<in>set (butlast (trace d i pref @ concat (map (trace d (deltas d pref i)) mids) @ trace d (deltas d pref i) suf)). n < Suc (deltas d pref i); \<forall>n\<in>set (butlast (trace d i pref)). n \<noteq> deltas d pref i; \<forall>mid\<in>set mids. deltas d mid (deltas d pref i) = deltas d pref i \<and> (\<forall>n\<in>set (butlast (trace d (deltas d pref i) mid)). n \<noteq> deltas d pref i); \<forall>n\<in>set (butlast (trace d (deltas d pref i) suf)). n \<noteq> deltas d pref i\<rbrakk> \<Longrightarrow> \<exists>xs ys. concat mids @ suf = xs @ ys \<and> xs \<in> star (regset d (deltas d pref i) (deltas d pref i) (deltas d pref i)) \<and> (\<forall>n\<in>set (butlast (trace d (deltas d pref i) ys)). n < deltas d pref i) \<and> deltas d ys (deltas d pref i) = deltas d suf (deltas d pref i)
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i pref mids suf n. \<lbrakk>\<And>ia j xs. (xs \<in> regset d ia j (deltas d pref i)) = ((\<forall>n\<in>set (butlast (trace d ia xs)). n < deltas d pref i) \<and> deltas d xs ia = j); \<forall>n\<in>set (butlast (trace d i pref)). n \<noteq> deltas d pref i; \<forall>mid\<in>set mids. deltas d mid (deltas d pref i) = deltas d pref i \<and> (\<forall>n\<in>set (butlast (trace d (deltas d pref i) mid)). n \<noteq> deltas d pref i); \<forall>n\<in>set (butlast (trace d (deltas d pref i) suf)). n \<noteq> deltas d pref i; n \<in> set (butlast (trace d i pref))\<rbrakk> \<Longrightarrow> n \<in> set (butlast (trace d i pref @ concat (map (trace d (deltas d pref i)) mids) @ trace d (deltas d pref i) suf))
 2. \<And>i pref mids suf. \<lbrakk>\<And>ia j xs. (xs \<in> regset d ia j (deltas d pref i)) = ((\<forall>n\<in>set (butlast (trace d ia xs)). n < deltas d pref i) \<and> deltas d xs ia = j); \<forall>n\<in>set (butlast (trace d i pref @ concat (map (trace d (deltas d pref i)) mids) @ trace d (deltas d pref i) suf)). n < Suc (deltas d pref i); \<forall>n\<in>set (butlast (trace d i pref)). n \<noteq> deltas d pref i; \<forall>mid\<in>set mids. deltas d mid (deltas d pref i) = deltas d pref i \<and> (\<forall>n\<in>set (butlast (trace d (deltas d pref i) mid)). n \<noteq> deltas d pref i); \<forall>n\<in>set (butlast (trace d (deltas d pref i) suf)). n \<noteq> deltas d pref i\<rbrakk> \<Longrightarrow> \<exists>xs ys. concat mids @ suf = xs @ ys \<and> xs \<in> star (regset d (deltas d pref i) (deltas d pref i) (deltas d pref i)) \<and> (\<forall>n\<in>set (butlast (trace d (deltas d pref i) ys)). n < deltas d pref i) \<and> deltas d ys (deltas d pref i) = deltas d suf (deltas d pref i)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i pref mids suf. \<lbrakk>\<And>ia j xs. (xs \<in> regset d ia j (deltas d pref i)) = ((\<forall>n\<in>set (butlast (trace d ia xs)). n < deltas d pref i) \<and> deltas d xs ia = j); \<forall>n\<in>set (butlast (trace d i pref @ concat (map (trace d (deltas d pref i)) mids) @ trace d (deltas d pref i) suf)). n < Suc (deltas d pref i); \<forall>n\<in>set (butlast (trace d i pref)). n \<noteq> deltas d pref i; \<forall>mid\<in>set mids. deltas d mid (deltas d pref i) = deltas d pref i \<and> (\<forall>n\<in>set (butlast (trace d (deltas d pref i) mid)). n \<noteq> deltas d pref i); \<forall>n\<in>set (butlast (trace d (deltas d pref i) suf)). n \<noteq> deltas d pref i\<rbrakk> \<Longrightarrow> \<exists>xs ys. concat mids @ suf = xs @ ys \<and> xs \<in> star (regset d (deltas d pref i) (deltas d pref i) (deltas d pref i)) \<and> (\<forall>n\<in>set (butlast (trace d (deltas d pref i) ys)). n < deltas d pref i) \<and> deltas d ys (deltas d pref i) = deltas d suf (deltas d pref i)
[PROOF STEP]
apply (rule_tac x = "concat mids" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i pref mids suf. \<lbrakk>\<And>ia j xs. (xs \<in> regset d ia j (deltas d pref i)) = ((\<forall>n\<in>set (butlast (trace d ia xs)). n < deltas d pref i) \<and> deltas d xs ia = j); \<forall>n\<in>set (butlast (trace d i pref @ concat (map (trace d (deltas d pref i)) mids) @ trace d (deltas d pref i) suf)). n < Suc (deltas d pref i); \<forall>n\<in>set (butlast (trace d i pref)). n \<noteq> deltas d pref i; \<forall>mid\<in>set mids. deltas d mid (deltas d pref i) = deltas d pref i \<and> (\<forall>n\<in>set (butlast (trace d (deltas d pref i) mid)). n \<noteq> deltas d pref i); \<forall>n\<in>set (butlast (trace d (deltas d pref i) suf)). n \<noteq> deltas d pref i\<rbrakk> \<Longrightarrow> \<exists>ys. concat mids @ suf = concat mids @ ys \<and> concat mids \<in> star (regset d (deltas d pref i) (deltas d pref i) (deltas d pref i)) \<and> (\<forall>n\<in>set (butlast (trace d (deltas d pref i) ys)). n < deltas d pref i) \<and> deltas d ys (deltas d pref i) = deltas d suf (deltas d pref i)
[PROOF STEP]
apply (simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i pref mids suf. \<lbrakk>\<And>ia j xs. (xs \<in> regset d ia j (deltas d pref i)) = ((\<forall>n\<in>set (butlast (trace d ia xs)). n < deltas d pref i) \<and> deltas d xs ia = j); \<forall>n\<in>set (butlast (trace d i pref @ concat (map (trace d (deltas d pref i)) mids) @ trace d (deltas d pref i) suf)). n < Suc (deltas d pref i); \<forall>n\<in>set (butlast (trace d i pref)). n \<noteq> deltas d pref i; \<forall>mid\<in>set mids. deltas d mid (deltas d pref i) = deltas d pref i \<and> (\<forall>n\<in>set (butlast (trace d (deltas d pref i) mid)). n \<noteq> deltas d pref i); \<forall>n\<in>set (butlast (trace d (deltas d pref i) suf)). n \<noteq> deltas d pref i\<rbrakk> \<Longrightarrow> concat mids \<in> star (regset d (deltas d pref i) (deltas d pref i) (deltas d pref i)) \<and> (\<forall>n\<in>set (butlast (trace d (deltas d pref i) suf)). n < deltas d pref i)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i pref mids suf. \<lbrakk>\<And>ia j xs. (xs \<in> regset d ia j (deltas d pref i)) = ((\<forall>n\<in>set (butlast (trace d ia xs)). n < deltas d pref i) \<and> deltas d xs ia = j); \<forall>n\<in>set (butlast (trace d i pref @ concat (map (trace d (deltas d pref i)) mids) @ trace d (deltas d pref i) suf)). n < Suc (deltas d pref i); \<forall>n\<in>set (butlast (trace d i pref)). n \<noteq> deltas d pref i; \<forall>mid\<in>set mids. deltas d mid (deltas d pref i) = deltas d pref i \<and> (\<forall>n\<in>set (butlast (trace d (deltas d pref i) mid)). n \<noteq> deltas d pref i); \<forall>n\<in>set (butlast (trace d (deltas d pref i) suf)). n \<noteq> deltas d pref i\<rbrakk> \<Longrightarrow> concat mids \<in> star (regset d (deltas d pref i) (deltas d pref i) (deltas d pref i))
 2. \<And>i pref mids suf. \<lbrakk>\<And>ia j xs. (xs \<in> regset d ia j (deltas d pref i)) = ((\<forall>n\<in>set (butlast (trace d ia xs)). n < deltas d pref i) \<and> deltas d xs ia = j); \<forall>n\<in>set (butlast (trace d i pref @ concat (map (trace d (deltas d pref i)) mids) @ trace d (deltas d pref i) suf)). n < Suc (deltas d pref i); \<forall>n\<in>set (butlast (trace d i pref)). n \<noteq> deltas d pref i; \<forall>mid\<in>set mids. deltas d mid (deltas d pref i) = deltas d pref i \<and> (\<forall>n\<in>set (butlast (trace d (deltas d pref i) mid)). n \<noteq> deltas d pref i); \<forall>n\<in>set (butlast (trace d (deltas d pref i) suf)). n \<noteq> deltas d pref i\<rbrakk> \<Longrightarrow> \<forall>n\<in>set (butlast (trace d (deltas d pref i) suf)). n < deltas d pref i
[PROOF STEP]
apply (rule concat_in_star)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i pref mids suf. \<lbrakk>\<And>ia j xs. (xs \<in> regset d ia j (deltas d pref i)) = ((\<forall>n\<in>set (butlast (trace d ia xs)). n < deltas d pref i) \<and> deltas d xs ia = j); \<forall>n\<in>set (butlast (trace d i pref @ concat (map (trace d (deltas d pref i)) mids) @ trace d (deltas d pref i) suf)). n < Suc (deltas d pref i); \<forall>n\<in>set (butlast (trace d i pref)). n \<noteq> deltas d pref i; \<forall>mid\<in>set mids. deltas d mid (deltas d pref i) = deltas d pref i \<and> (\<forall>n\<in>set (butlast (trace d (deltas d pref i) mid)). n \<noteq> deltas d pref i); \<forall>n\<in>set (butlast (trace d (deltas d pref i) suf)). n \<noteq> deltas d pref i\<rbrakk> \<Longrightarrow> set mids \<subseteq> regset d (deltas d pref i) (deltas d pref i) (deltas d pref i)
 2. \<And>i pref mids suf. \<lbrakk>\<And>ia j xs. (xs \<in> regset d ia j (deltas d pref i)) = ((\<forall>n\<in>set (butlast (trace d ia xs)). n < deltas d pref i) \<and> deltas d xs ia = j); \<forall>n\<in>set (butlast (trace d i pref @ concat (map (trace d (deltas d pref i)) mids) @ trace d (deltas d pref i) suf)). n < Suc (deltas d pref i); \<forall>n\<in>set (butlast (trace d i pref)). n \<noteq> deltas d pref i; \<forall>mid\<in>set mids. deltas d mid (deltas d pref i) = deltas d pref i \<and> (\<forall>n\<in>set (butlast (trace d (deltas d pref i) mid)). n \<noteq> deltas d pref i); \<forall>n\<in>set (butlast (trace d (deltas d pref i) suf)). n \<noteq> deltas d pref i\<rbrakk> \<Longrightarrow> \<forall>n\<in>set (butlast (trace d (deltas d pref i) suf)). n < deltas d pref i
[PROOF STEP]
apply (clarsimp simp: subset_iff)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i pref mids suf t n. \<lbrakk>\<And>ia j xs. (xs \<in> regset d ia j (deltas d pref i)) = ((\<forall>n\<in>set (butlast (trace d ia xs)). n < deltas d pref i) \<and> deltas d xs ia = j); \<forall>n\<in>set (butlast (trace d i pref @ concat (map (trace d (deltas d pref i)) mids) @ trace d (deltas d pref i) suf)). n < Suc (deltas d pref i); \<forall>n\<in>set (butlast (trace d i pref)). n \<noteq> deltas d pref i; \<forall>mid\<in>set mids. deltas d mid (deltas d pref i) = deltas d pref i \<and> (\<forall>n\<in>set (butlast (trace d (deltas d pref i) mid)). n \<noteq> deltas d pref i); \<forall>n\<in>set (butlast (trace d (deltas d pref i) suf)). n \<noteq> deltas d pref i; t \<in> set mids; n \<in> set (butlast (trace d (deltas d pref i) t))\<rbrakk> \<Longrightarrow> n < deltas d pref i
 2. \<And>i pref mids suf. \<lbrakk>\<And>ia j xs. (xs \<in> regset d ia j (deltas d pref i)) = ((\<forall>n\<in>set (butlast (trace d ia xs)). n < deltas d pref i) \<and> deltas d xs ia = j); \<forall>n\<in>set (butlast (trace d i pref @ concat (map (trace d (deltas d pref i)) mids) @ trace d (deltas d pref i) suf)). n < Suc (deltas d pref i); \<forall>n\<in>set (butlast (trace d i pref)). n \<noteq> deltas d pref i; \<forall>mid\<in>set mids. deltas d mid (deltas d pref i) = deltas d pref i \<and> (\<forall>n\<in>set (butlast (trace d (deltas d pref i) mid)). n \<noteq> deltas d pref i); \<forall>n\<in>set (butlast (trace d (deltas d pref i) suf)). n \<noteq> deltas d pref i\<rbrakk> \<Longrightarrow> \<forall>n\<in>set (butlast (trace d (deltas d pref i) suf)). n < deltas d pref i
[PROOF STEP]
apply (rule lem)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>i pref mids suf t n. \<lbrakk>\<And>ia j xs. (xs \<in> regset d ia j (deltas d pref i)) = ((\<forall>n\<in>set (butlast (trace d ia xs)). n < deltas d pref i) \<and> deltas d xs ia = j); \<forall>n\<in>set (butlast (trace d i pref @ concat (map (trace d (deltas d pref i)) mids) @ trace d (deltas d pref i) suf)). n < Suc (deltas d pref i); \<forall>n\<in>set (butlast (trace d i pref)). n \<noteq> deltas d pref i; \<forall>mid\<in>set mids. deltas d mid (deltas d pref i) = deltas d pref i \<and> (\<forall>n\<in>set (butlast (trace d (deltas d pref i) mid)). n \<noteq> deltas d pref i); \<forall>n\<in>set (butlast (trace d (deltas d pref i) suf)). n \<noteq> deltas d pref i; t \<in> set mids; n \<in> set (butlast (trace d (deltas d pref i) t))\<rbrakk> \<Longrightarrow> n < Suc (deltas d pref i)
 2. \<And>i pref mids suf t n. \<lbrakk>\<And>ia j xs. (xs \<in> regset d ia j (deltas d pref i)) = ((\<forall>n\<in>set (butlast (trace d ia xs)). n < deltas d pref i) \<and> deltas d xs ia = j); \<forall>n\<in>set (butlast (trace d i pref @ concat (map (trace d (deltas d pref i)) mids) @ trace d (deltas d pref i) suf)). n < Suc (deltas d pref i); \<forall>n\<in>set (butlast (trace d i pref)). n \<noteq> deltas d pref i; \<forall>mid\<in>set mids. deltas d mid (deltas d pref i) = deltas d pref i \<and> (\<forall>n\<in>set (butlast (trace d (deltas d pref i) mid)). n \<noteq> deltas d pref i); \<forall>n\<in>set (butlast (trace d (deltas d pref i) suf)). n \<noteq> deltas d pref i; t \<in> set mids; n \<in> set (butlast (trace d (deltas d pref i) t))\<rbrakk> \<Longrightarrow> n \<noteq> deltas d pref i
 3. \<And>i pref mids suf. \<lbrakk>\<And>ia j xs. (xs \<in> regset d ia j (deltas d pref i)) = ((\<forall>n\<in>set (butlast (trace d ia xs)). n < deltas d pref i) \<and> deltas d xs ia = j); \<forall>n\<in>set (butlast (trace d i pref @ concat (map (trace d (deltas d pref i)) mids) @ trace d (deltas d pref i) suf)). n < Suc (deltas d pref i); \<forall>n\<in>set (butlast (trace d i pref)). n \<noteq> deltas d pref i; \<forall>mid\<in>set mids. deltas d mid (deltas d pref i) = deltas d pref i \<and> (\<forall>n\<in>set (butlast (trace d (deltas d pref i) mid)). n \<noteq> deltas d pref i); \<forall>n\<in>set (butlast (trace d (deltas d pref i) suf)). n \<noteq> deltas d pref i\<rbrakk> \<Longrightarrow> \<forall>n\<in>set (butlast (trace d (deltas d pref i) suf)). n < deltas d pref i
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>i pref mids suf t n. \<lbrakk>\<And>ia j xs. (xs \<in> regset d ia j (deltas d pref i)) = ((\<forall>n\<in>set (butlast (trace d ia xs)). n < deltas d pref i) \<and> deltas d xs ia = j); \<forall>n\<in>set (butlast (trace d i pref @ concat (map (trace d (deltas d pref i)) mids) @ trace d (deltas d pref i) suf)). n < Suc (deltas d pref i); \<forall>n\<in>set (butlast (trace d i pref)). n \<noteq> deltas d pref i; \<forall>mid\<in>set mids. deltas d mid (deltas d pref i) = deltas d pref i \<and> (\<forall>n\<in>set (butlast (trace d (deltas d pref i) mid)). n \<noteq> deltas d pref i); \<forall>n\<in>set (butlast (trace d (deltas d pref i) suf)). n \<noteq> deltas d pref i; t \<in> set mids; n \<in> set (butlast (trace d (deltas d pref i) t))\<rbrakk> \<Longrightarrow> n \<noteq> deltas d pref i
 2. \<And>i pref mids suf t n. \<lbrakk>\<And>ia j xs. (xs \<in> regset d ia j (deltas d pref i)) = ((\<forall>n\<in>set (butlast (trace d ia xs)). n < deltas d pref i) \<and> deltas d xs ia = j); \<forall>n\<in>set (butlast (trace d i pref @ concat (map (trace d (deltas d pref i)) mids) @ trace d (deltas d pref i) suf)). n < Suc (deltas d pref i); \<forall>n\<in>set (butlast (trace d i pref)). n \<noteq> deltas d pref i; \<forall>mid\<in>set mids. deltas d mid (deltas d pref i) = deltas d pref i \<and> (\<forall>n\<in>set (butlast (trace d (deltas d pref i) mid)). n \<noteq> deltas d pref i); \<forall>n\<in>set (butlast (trace d (deltas d pref i) suf)). n \<noteq> deltas d pref i; t \<in> set mids; n \<in> set (butlast (trace d (deltas d pref i) t))\<rbrakk> \<Longrightarrow> n < Suc (deltas d pref i)
 3. \<And>i pref mids suf. \<lbrakk>\<And>ia j xs. (xs \<in> regset d ia j (deltas d pref i)) = ((\<forall>n\<in>set (butlast (trace d ia xs)). n < deltas d pref i) \<and> deltas d xs ia = j); \<forall>n\<in>set (butlast (trace d i pref @ concat (map (trace d (deltas d pref i)) mids) @ trace d (deltas d pref i) suf)). n < Suc (deltas d pref i); \<forall>n\<in>set (butlast (trace d i pref)). n \<noteq> deltas d pref i; \<forall>mid\<in>set mids. deltas d mid (deltas d pref i) = deltas d pref i \<and> (\<forall>n\<in>set (butlast (trace d (deltas d pref i) mid)). n \<noteq> deltas d pref i); \<forall>n\<in>set (butlast (trace d (deltas d pref i) suf)). n \<noteq> deltas d pref i\<rbrakk> \<Longrightarrow> \<forall>n\<in>set (butlast (trace d (deltas d pref i) suf)). n < deltas d pref i
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i pref mids suf t n. \<lbrakk>\<And>ia j xs. (xs \<in> regset d ia j (deltas d pref i)) = ((\<forall>n\<in>set (butlast (trace d ia xs)). n < deltas d pref i) \<and> deltas d xs ia = j); \<forall>n\<in>set (butlast (trace d i pref @ concat (map (trace d (deltas d pref i)) mids) @ trace d (deltas d pref i) suf)). n < Suc (deltas d pref i); \<forall>n\<in>set (butlast (trace d i pref)). n \<noteq> deltas d pref i; \<forall>mid\<in>set mids. deltas d mid (deltas d pref i) = deltas d pref i \<and> (\<forall>n\<in>set (butlast (trace d (deltas d pref i) mid)). n \<noteq> deltas d pref i); \<forall>n\<in>set (butlast (trace d (deltas d pref i) suf)). n \<noteq> deltas d pref i; t \<in> set mids; n \<in> set (butlast (trace d (deltas d pref i) t))\<rbrakk> \<Longrightarrow> n < Suc (deltas d pref i)
 2. \<And>i pref mids suf. \<lbrakk>\<And>ia j xs. (xs \<in> regset d ia j (deltas d pref i)) = ((\<forall>n\<in>set (butlast (trace d ia xs)). n < deltas d pref i) \<and> deltas d xs ia = j); \<forall>n\<in>set (butlast (trace d i pref @ concat (map (trace d (deltas d pref i)) mids) @ trace d (deltas d pref i) suf)). n < Suc (deltas d pref i); \<forall>n\<in>set (butlast (trace d i pref)). n \<noteq> deltas d pref i; \<forall>mid\<in>set mids. deltas d mid (deltas d pref i) = deltas d pref i \<and> (\<forall>n\<in>set (butlast (trace d (deltas d pref i) mid)). n \<noteq> deltas d pref i); \<forall>n\<in>set (butlast (trace d (deltas d pref i) suf)). n \<noteq> deltas d pref i\<rbrakk> \<Longrightarrow> \<forall>n\<in>set (butlast (trace d (deltas d pref i) suf)). n < deltas d pref i
[PROOF STEP]
apply (drule bspec)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>i pref mids suf t n. \<lbrakk>\<And>ia j xs. (xs \<in> regset d ia j (deltas d pref i)) = ((\<forall>n\<in>set (butlast (trace d ia xs)). n < deltas d pref i) \<and> deltas d xs ia = j); \<forall>n\<in>set (butlast (trace d i pref)). n \<noteq> deltas d pref i; \<forall>mid\<in>set mids. deltas d mid (deltas d pref i) = deltas d pref i \<and> (\<forall>n\<in>set (butlast (trace d (deltas d pref i) mid)). n \<noteq> deltas d pref i); \<forall>n\<in>set (butlast (trace d (deltas d pref i) suf)). n \<noteq> deltas d pref i; t \<in> set mids; n \<in> set (butlast (trace d (deltas d pref i) t))\<rbrakk> \<Longrightarrow> ?n212 i pref mids suf t n \<in> set (butlast (trace d i pref @ concat (map (trace d (deltas d pref i)) mids) @ trace d (deltas d pref i) suf))
 2. \<And>i pref mids suf t n. \<lbrakk>\<And>ia j xs. (xs \<in> regset d ia j (deltas d pref i)) = ((\<forall>n\<in>set (butlast (trace d ia xs)). n < deltas d pref i) \<and> deltas d xs ia = j); \<forall>n\<in>set (butlast (trace d i pref)). n \<noteq> deltas d pref i; \<forall>mid\<in>set mids. deltas d mid (deltas d pref i) = deltas d pref i \<and> (\<forall>n\<in>set (butlast (trace d (deltas d pref i) mid)). n \<noteq> deltas d pref i); \<forall>n\<in>set (butlast (trace d (deltas d pref i) suf)). n \<noteq> deltas d pref i; t \<in> set mids; n \<in> set (butlast (trace d (deltas d pref i) t)); ?n212 i pref mids suf t n < Suc (deltas d pref i)\<rbrakk> \<Longrightarrow> n < Suc (deltas d pref i)
 3. \<And>i pref mids suf. \<lbrakk>\<And>ia j xs. (xs \<in> regset d ia j (deltas d pref i)) = ((\<forall>n\<in>set (butlast (trace d ia xs)). n < deltas d pref i) \<and> deltas d xs ia = j); \<forall>n\<in>set (butlast (trace d i pref @ concat (map (trace d (deltas d pref i)) mids) @ trace d (deltas d pref i) suf)). n < Suc (deltas d pref i); \<forall>n\<in>set (butlast (trace d i pref)). n \<noteq> deltas d pref i; \<forall>mid\<in>set mids. deltas d mid (deltas d pref i) = deltas d pref i \<and> (\<forall>n\<in>set (butlast (trace d (deltas d pref i) mid)). n \<noteq> deltas d pref i); \<forall>n\<in>set (butlast (trace d (deltas d pref i) suf)). n \<noteq> deltas d pref i\<rbrakk> \<Longrightarrow> \<forall>n\<in>set (butlast (trace d (deltas d pref i) suf)). n < deltas d pref i
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>i pref mids suf t n. \<lbrakk>\<And>ia j xs. (xs \<in> regset d ia j (deltas d pref i)) = ((\<forall>n\<in>set (butlast (trace d ia xs)). n < deltas d pref i) \<and> deltas d xs ia = j); \<forall>n\<in>set (butlast (trace d i pref)). n \<noteq> deltas d pref i; \<forall>mid\<in>set mids. deltas d mid (deltas d pref i) = deltas d pref i \<and> (\<forall>n\<in>set (butlast (trace d (deltas d pref i) mid)). n \<noteq> deltas d pref i); \<forall>n\<in>set (butlast (trace d (deltas d pref i) suf)). n \<noteq> deltas d pref i; t \<in> set mids; n \<in> set (butlast (trace d (deltas d pref i) t)); ?n212 i pref mids suf t n < Suc (deltas d pref i)\<rbrakk> \<Longrightarrow> n < Suc (deltas d pref i)
 2. \<And>i pref mids suf t n. \<lbrakk>\<And>ia j xs. (xs \<in> regset d ia j (deltas d pref i)) = ((\<forall>n\<in>set (butlast (trace d ia xs)). n < deltas d pref i) \<and> deltas d xs ia = j); \<forall>n\<in>set (butlast (trace d i pref)). n \<noteq> deltas d pref i; \<forall>mid\<in>set mids. deltas d mid (deltas d pref i) = deltas d pref i \<and> (\<forall>n\<in>set (butlast (trace d (deltas d pref i) mid)). n \<noteq> deltas d pref i); \<forall>n\<in>set (butlast (trace d (deltas d pref i) suf)). n \<noteq> deltas d pref i; t \<in> set mids; n \<in> set (butlast (trace d (deltas d pref i) t))\<rbrakk> \<Longrightarrow> ?n212 i pref mids suf t n \<in> set (butlast (trace d i pref @ concat (map (trace d (deltas d pref i)) mids) @ trace d (deltas d pref i) suf))
 3. \<And>i pref mids suf. \<lbrakk>\<And>ia j xs. (xs \<in> regset d ia j (deltas d pref i)) = ((\<forall>n\<in>set (butlast (trace d ia xs)). n < deltas d pref i) \<and> deltas d xs ia = j); \<forall>n\<in>set (butlast (trace d i pref @ concat (map (trace d (deltas d pref i)) mids) @ trace d (deltas d pref i) suf)). n < Suc (deltas d pref i); \<forall>n\<in>set (butlast (trace d i pref)). n \<noteq> deltas d pref i; \<forall>mid\<in>set mids. deltas d mid (deltas d pref i) = deltas d pref i \<and> (\<forall>n\<in>set (butlast (trace d (deltas d pref i) mid)). n \<noteq> deltas d pref i); \<forall>n\<in>set (butlast (trace d (deltas d pref i) suf)). n \<noteq> deltas d pref i\<rbrakk> \<Longrightarrow> \<forall>n\<in>set (butlast (trace d (deltas d pref i) suf)). n < deltas d pref i
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i pref mids suf t n. \<lbrakk>\<And>ia j xs. (xs \<in> regset d ia j (deltas d pref i)) = ((\<forall>n\<in>set (butlast (trace d ia xs)). n < deltas d pref i) \<and> deltas d xs ia = j); \<forall>n\<in>set (butlast (trace d i pref)). n \<noteq> deltas d pref i; \<forall>mid\<in>set mids. deltas d mid (deltas d pref i) = deltas d pref i \<and> (\<forall>n\<in>set (butlast (trace d (deltas d pref i) mid)). n \<noteq> deltas d pref i); \<forall>n\<in>set (butlast (trace d (deltas d pref i) suf)). n \<noteq> deltas d pref i; t \<in> set mids; n \<in> set (butlast (trace d (deltas d pref i) t))\<rbrakk> \<Longrightarrow> n \<in> set (butlast (trace d i pref @ concat (map (trace d (deltas d pref i)) mids) @ trace d (deltas d pref i) suf))
 2. \<And>i pref mids suf. \<lbrakk>\<And>ia j xs. (xs \<in> regset d ia j (deltas d pref i)) = ((\<forall>n\<in>set (butlast (trace d ia xs)). n < deltas d pref i) \<and> deltas d xs ia = j); \<forall>n\<in>set (butlast (trace d i pref @ concat (map (trace d (deltas d pref i)) mids) @ trace d (deltas d pref i) suf)). n < Suc (deltas d pref i); \<forall>n\<in>set (butlast (trace d i pref)). n \<noteq> deltas d pref i; \<forall>mid\<in>set mids. deltas d mid (deltas d pref i) = deltas d pref i \<and> (\<forall>n\<in>set (butlast (trace d (deltas d pref i) mid)). n \<noteq> deltas d pref i); \<forall>n\<in>set (butlast (trace d (deltas d pref i) suf)). n \<noteq> deltas d pref i\<rbrakk> \<Longrightarrow> \<forall>n\<in>set (butlast (trace d (deltas d pref i) suf)). n < deltas d pref i
[PROOF STEP]
apply (simp add: image_eqI in_set_butlast_concatI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i pref mids suf. \<lbrakk>\<And>ia j xs. (xs \<in> regset d ia j (deltas d pref i)) = ((\<forall>n\<in>set (butlast (trace d ia xs)). n < deltas d pref i) \<and> deltas d xs ia = j); \<forall>n\<in>set (butlast (trace d i pref @ concat (map (trace d (deltas d pref i)) mids) @ trace d (deltas d pref i) suf)). n < Suc (deltas d pref i); \<forall>n\<in>set (butlast (trace d i pref)). n \<noteq> deltas d pref i; \<forall>mid\<in>set mids. deltas d mid (deltas d pref i) = deltas d pref i \<and> (\<forall>n\<in>set (butlast (trace d (deltas d pref i) mid)). n \<noteq> deltas d pref i); \<forall>n\<in>set (butlast (trace d (deltas d pref i) suf)). n \<noteq> deltas d pref i\<rbrakk> \<Longrightarrow> \<forall>n\<in>set (butlast (trace d (deltas d pref i) suf)). n < deltas d pref i
[PROOF STEP]
apply (rule ballI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i pref mids suf n. \<lbrakk>\<And>ia j xs. (xs \<in> regset d ia j (deltas d pref i)) = ((\<forall>n\<in>set (butlast (trace d ia xs)). n < deltas d pref i) \<and> deltas d xs ia = j); \<forall>n\<in>set (butlast (trace d i pref @ concat (map (trace d (deltas d pref i)) mids) @ trace d (deltas d pref i) suf)). n < Suc (deltas d pref i); \<forall>n\<in>set (butlast (trace d i pref)). n \<noteq> deltas d pref i; \<forall>mid\<in>set mids. deltas d mid (deltas d pref i) = deltas d pref i \<and> (\<forall>n\<in>set (butlast (trace d (deltas d pref i) mid)). n \<noteq> deltas d pref i); \<forall>n\<in>set (butlast (trace d (deltas d pref i) suf)). n \<noteq> deltas d pref i; n \<in> set (butlast (trace d (deltas d pref i) suf))\<rbrakk> \<Longrightarrow> n < deltas d pref i
[PROOF STEP]
apply (rule lem)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i pref mids suf n. \<lbrakk>\<And>ia j xs. (xs \<in> regset d ia j (deltas d pref i)) = ((\<forall>n\<in>set (butlast (trace d ia xs)). n < deltas d pref i) \<and> deltas d xs ia = j); \<forall>n\<in>set (butlast (trace d i pref @ concat (map (trace d (deltas d pref i)) mids) @ trace d (deltas d pref i) suf)). n < Suc (deltas d pref i); \<forall>n\<in>set (butlast (trace d i pref)). n \<noteq> deltas d pref i; \<forall>mid\<in>set mids. deltas d mid (deltas d pref i) = deltas d pref i \<and> (\<forall>n\<in>set (butlast (trace d (deltas d pref i) mid)). n \<noteq> deltas d pref i); \<forall>n\<in>set (butlast (trace d (deltas d pref i) suf)). n \<noteq> deltas d pref i; n \<in> set (butlast (trace d (deltas d pref i) suf))\<rbrakk> \<Longrightarrow> n < Suc (deltas d pref i)
 2. \<And>i pref mids suf n. \<lbrakk>\<And>ia j xs. (xs \<in> regset d ia j (deltas d pref i)) = ((\<forall>n\<in>set (butlast (trace d ia xs)). n < deltas d pref i) \<and> deltas d xs ia = j); \<forall>n\<in>set (butlast (trace d i pref @ concat (map (trace d (deltas d pref i)) mids) @ trace d (deltas d pref i) suf)). n < Suc (deltas d pref i); \<forall>n\<in>set (butlast (trace d i pref)). n \<noteq> deltas d pref i; \<forall>mid\<in>set mids. deltas d mid (deltas d pref i) = deltas d pref i \<and> (\<forall>n\<in>set (butlast (trace d (deltas d pref i) mid)). n \<noteq> deltas d pref i); \<forall>n\<in>set (butlast (trace d (deltas d pref i) suf)). n \<noteq> deltas d pref i; n \<in> set (butlast (trace d (deltas d pref i) suf))\<rbrakk> \<Longrightarrow> n \<noteq> deltas d pref i
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma trace_below:
 "bounded d k \<Longrightarrow> \<forall>i. i < k \<longrightarrow> (\<forall>n\<in>set(trace d i xs). n < k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded d k \<Longrightarrow> \<forall>i<k. \<forall>n\<in>set (trace d i xs). n < k
[PROOF STEP]
apply (unfold bounded_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n<k. \<forall>x. d x n < k \<Longrightarrow> \<forall>i<k. \<forall>n\<in>set (trace d i xs). n < k
[PROOF STEP]
apply (induct "xs")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>n<k. \<forall>x. d x n < k \<Longrightarrow> \<forall>i<k. \<forall>n\<in>set (trace d i []). n < k
 2. \<And>a xs. \<lbrakk>\<forall>n<k. \<forall>x. d x n < k \<Longrightarrow> \<forall>i<k. \<forall>n\<in>set (trace d i xs). n < k; \<forall>n<k. \<forall>x. d x n < k\<rbrakk> \<Longrightarrow> \<forall>i<k. \<forall>n\<in>set (trace d i (a # xs)). n < k
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>\<forall>n<k. \<forall>x. d x n < k \<Longrightarrow> \<forall>i<k. \<forall>n\<in>set (trace d i xs). n < k; \<forall>n<k. \<forall>x. d x n < k\<rbrakk> \<Longrightarrow> \<forall>i<k. \<forall>n\<in>set (trace d i (a # xs)). n < k
[PROOF STEP]
apply (simp (no_asm))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>\<forall>n<k. \<forall>x. d x n < k \<Longrightarrow> \<forall>i<k. \<forall>n\<in>set (trace d i xs). n < k; \<forall>n<k. \<forall>x. d x n < k\<rbrakk> \<Longrightarrow> \<forall>i<k. d a i < k \<and> (\<forall>n\<in>set (trace d (d a i) xs). n < k)
[PROOF STEP]
apply (blast)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma regset_below:
 "[| bounded d k; i < k; j < k |] ==>
  regset d i j k = {xs. deltas d xs i = j}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bounded d k; i < k; j < k\<rbrakk> \<Longrightarrow> regset d i j k = {xs. deltas d xs i = j}
[PROOF STEP]
apply (rule set_eqI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>bounded d k; i < k; j < k\<rbrakk> \<Longrightarrow> (x \<in> regset d i j k) = (x \<in> {xs. deltas d xs i = j})
[PROOF STEP]
apply (simp add: regset_spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>bounded d k; i < k; j < k\<rbrakk> \<Longrightarrow> ((\<forall>n\<in>set (butlast (trace d i x)). n < k) \<and> deltas d x i = j) = (deltas d x i = j)
[PROOF STEP]
apply (blast dest: trace_below in_set_butlastD)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma deltas_below:
 "\<And>i. bounded d k \<Longrightarrow> i < k \<Longrightarrow> deltas d w i < k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>bounded d k; i < k\<rbrakk> \<Longrightarrow> deltas d w i < k
[PROOF STEP]
apply (unfold bounded_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>\<forall>n<k. \<forall>x. d x n < k; i < k\<rbrakk> \<Longrightarrow> deltas d w i < k
[PROOF STEP]
apply (induct "w")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i. \<lbrakk>\<forall>n<k. \<forall>x. d x n < k; i < k\<rbrakk> \<Longrightarrow> deltas d [] i < k
 2. \<And>a w i. \<lbrakk>\<And>i. \<lbrakk>\<forall>n<k. \<forall>x. d x n < k; i < k\<rbrakk> \<Longrightarrow> deltas d w i < k; \<forall>n<k. \<forall>x. d x n < k; i < k\<rbrakk> \<Longrightarrow> deltas d (a # w) i < k
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma regset_DA_equiv:
 "[| bounded (next A) k; start A < k; j < k |] ==>
  w : regset_of_DA A k = accepts A w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bounded (next A) k; start A < k; j < k\<rbrakk> \<Longrightarrow> (w \<in> regset_of_DA A k) = accepts A w
[PROOF STEP]
apply(unfold regset_of_DA_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bounded (next A) k; start A < k; j < k\<rbrakk> \<Longrightarrow> (w \<in> (\<Union>j\<in>{j. j < k \<and> fin A j}. regset (next A) (start A) j k)) = accepts A w
[PROOF STEP]
apply (simp cong: conj_cong
            add: regset_below deltas_below accepts_def delta_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma finals_map_Val [simp]: "finals (map Val vs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finals (map Val vs)
[PROOF STEP]
by(simp add: finals_iff)


[STATEMENT]
lemma \<tau>red0r_preserves_defass:
  assumes wf: "wf_J_prog P"
  shows "\<lbrakk> \<tau>red0r extTA P t h (e, xs) (e', xs'); \<D> e \<lfloor>dom xs\<rfloor> \<rbrakk> \<Longrightarrow> \<D> e' \<lfloor>dom xs'\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<tau>red0r extTA P t h (e, xs) (e', xs'); \<D> e \<lfloor>dom xs\<rfloor>\<rbrakk> \<Longrightarrow> \<D> e' \<lfloor>dom xs'\<rfloor>
[PROOF STEP]
by(induct rule: rtranclp_induct2)(auto dest: red_preserves_defass[OF wf])


[STATEMENT]
lemma \<tau>red0t_preserves_defass:
  assumes wf: "wf_J_prog P"
  shows "\<lbrakk> \<tau>red0t extTA P t h (e, xs) (e', xs'); \<D> e \<lfloor>dom xs\<rfloor> \<rbrakk> \<Longrightarrow> \<D> e' \<lfloor>dom xs'\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<tau>red0t extTA P t h (e, xs) (e', xs'); \<D> e \<lfloor>dom xs\<rfloor>\<rbrakk> \<Longrightarrow> \<D> e' \<lfloor>dom xs'\<rfloor>
[PROOF STEP]
by(rule \<tau>red0r_preserves_defass[OF wf])(rule tranclp_into_rtranclp)


[STATEMENT]
lemma LAss_lem:
  "\<lbrakk>x \<in> set xs; size xs \<le> size ys \<rbrakk>
  \<Longrightarrow> m1 \<subseteq>\<^sub>m m2(xs[\<mapsto>]ys) \<Longrightarrow> m1(x\<mapsto>y) \<subseteq>\<^sub>m m2(xs[\<mapsto>]ys[index xs x := y])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> set xs; length xs \<le> length ys; m1 \<subseteq>\<^sub>m m2(xs [\<mapsto>] ys)\<rbrakk> \<Longrightarrow> m1(x \<mapsto> y) \<subseteq>\<^sub>m m2(xs [\<mapsto>] ys[index xs x := y])
[PROOF STEP]
apply(simp add:map_le_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> set xs; length xs \<le> length ys; \<forall>a\<in>dom m1. m1 a = (m2(xs [\<mapsto>] ys)) a\<rbrakk> \<Longrightarrow> \<lfloor>y\<rfloor> = (m2(xs [\<mapsto>] ys[index xs x := y])) x \<and> (\<forall>a\<in>dom m1. (a = x \<longrightarrow> \<lfloor>y\<rfloor> = (m2(xs [\<mapsto>] ys[index xs x := y])) x) \<and> (a \<noteq> x \<longrightarrow> (m2(xs [\<mapsto>] ys)) a = (m2(xs [\<mapsto>] ys[index xs x := y])) a))
[PROOF STEP]
apply(simp add:fun_upds_apply index_less_aux eq_sym_conv)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Block_lem:
fixes l :: "'a \<rightharpoonup> 'b"
assumes 0: "l \<subseteq>\<^sub>m [Vs [\<mapsto>] ls]"
    and 1: "l' \<subseteq>\<^sub>m [Vs [\<mapsto>] ls', V\<mapsto>v]"
    and hidden: "V \<in> set Vs \<Longrightarrow> ls ! index Vs V = ls' ! index Vs V"
    and size: "size ls = size ls'"    "size Vs < size ls'"
shows "l'(V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls']"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l'(V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls']
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. l'(V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls']
[PROOF STEP]
have "l'(V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls', V\<mapsto>v](V := l V)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l'(V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls', V \<mapsto> v](V := l V)
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
l' \<subseteq>\<^sub>m [Vs [\<mapsto>] ls', V \<mapsto> v]

goal (1 subgoal):
 1. l'(V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls', V \<mapsto> v](V := l V)
[PROOF STEP]
by(rule map_le_upd)
[PROOF STATE]
proof (state)
this:
l'(V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls', V \<mapsto> v](V := l V)

goal (1 subgoal):
 1. l'(V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls']
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
l'(V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls', V \<mapsto> v](V := l V)

goal (1 subgoal):
 1. l'(V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls']
[PROOF STEP]
have "\<dots> = [Vs [\<mapsto>] ls'](V := l V)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [Vs [\<mapsto>] ls', V \<mapsto> v](V := l V) = [Vs [\<mapsto>] ls'](V := l V)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[Vs [\<mapsto>] ls', V \<mapsto> v](V := l V) = [Vs [\<mapsto>] ls'](V := l V)

goal (1 subgoal):
 1. l'(V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls']
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
[Vs [\<mapsto>] ls', V \<mapsto> v](V := l V) = [Vs [\<mapsto>] ls'](V := l V)

goal (1 subgoal):
 1. l'(V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls']
[PROOF STEP]
have "\<dots> \<subseteq>\<^sub>m [Vs [\<mapsto>] ls']"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [Vs [\<mapsto>] ls'](V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls']
[PROOF STEP]
proof (cases "l V")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. l V = None \<Longrightarrow> [Vs [\<mapsto>] ls'](V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls']
 2. \<And>a. l V = \<lfloor>a\<rfloor> \<Longrightarrow> [Vs [\<mapsto>] ls'](V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls']
[PROOF STEP]
case None
[PROOF STATE]
proof (state)
this:
l V = None

goal (2 subgoals):
 1. l V = None \<Longrightarrow> [Vs [\<mapsto>] ls'](V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls']
 2. \<And>a. l V = \<lfloor>a\<rfloor> \<Longrightarrow> [Vs [\<mapsto>] ls'](V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls']
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
l V = None

goal (1 subgoal):
 1. [Vs [\<mapsto>] ls'](V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls']
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[Vs [\<mapsto>] ls'](V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls']

goal (1 subgoal):
 1. \<And>a. l V = \<lfloor>a\<rfloor> \<Longrightarrow> [Vs [\<mapsto>] ls'](V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls']
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. l V = \<lfloor>a\<rfloor> \<Longrightarrow> [Vs [\<mapsto>] ls'](V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls']
[PROOF STEP]
case (Some w)
[PROOF STATE]
proof (state)
this:
l V = \<lfloor>w\<rfloor>

goal (1 subgoal):
 1. \<And>a. l V = \<lfloor>a\<rfloor> \<Longrightarrow> [Vs [\<mapsto>] ls'](V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls']
[PROOF STEP]
hence "[Vs [\<mapsto>] ls] V = Some w"
[PROOF STATE]
proof (prove)
using this:
l V = \<lfloor>w\<rfloor>

goal (1 subgoal):
 1. [Vs [\<mapsto>] ls] V = \<lfloor>w\<rfloor>
[PROOF STEP]
using 0
[PROOF STATE]
proof (prove)
using this:
l V = \<lfloor>w\<rfloor>
l \<subseteq>\<^sub>m [Vs [\<mapsto>] ls]

goal (1 subgoal):
 1. [Vs [\<mapsto>] ls] V = \<lfloor>w\<rfloor>
[PROOF STEP]
by(force simp add: map_le_def split:if_splits)
[PROOF STATE]
proof (state)
this:
[Vs [\<mapsto>] ls] V = \<lfloor>w\<rfloor>

goal (1 subgoal):
 1. \<And>a. l V = \<lfloor>a\<rfloor> \<Longrightarrow> [Vs [\<mapsto>] ls'](V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls']
[PROOF STEP]
hence VinVs: "V \<in> set Vs" and w: "w = ls ! index Vs V"
[PROOF STATE]
proof (prove)
using this:
[Vs [\<mapsto>] ls] V = \<lfloor>w\<rfloor>

goal (1 subgoal):
 1. V \<in> set Vs &&& w = ls ! index Vs V
[PROOF STEP]
using size
[PROOF STATE]
proof (prove)
using this:
[Vs [\<mapsto>] ls] V = \<lfloor>w\<rfloor>
length ls = length ls'
length Vs < length ls'

goal (1 subgoal):
 1. V \<in> set Vs &&& w = ls ! index Vs V
[PROOF STEP]
by(auto simp add:fun_upds_apply split:if_splits)
[PROOF STATE]
proof (state)
this:
V \<in> set Vs
w = ls ! index Vs V

goal (1 subgoal):
 1. \<And>a. l V = \<lfloor>a\<rfloor> \<Longrightarrow> [Vs [\<mapsto>] ls'](V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls']
[PROOF STEP]
hence "w = ls' ! index Vs V"
[PROOF STATE]
proof (prove)
using this:
V \<in> set Vs
w = ls ! index Vs V

goal (1 subgoal):
 1. w = ls' ! index Vs V
[PROOF STEP]
using hidden[OF VinVs]
[PROOF STATE]
proof (prove)
using this:
V \<in> set Vs
w = ls ! index Vs V
ls ! index Vs V = ls' ! index Vs V

goal (1 subgoal):
 1. w = ls' ! index Vs V
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
w = ls' ! index Vs V

goal (1 subgoal):
 1. \<And>a. l V = \<lfloor>a\<rfloor> \<Longrightarrow> [Vs [\<mapsto>] ls'](V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls']
[PROOF STEP]
hence "[Vs [\<mapsto>] ls'](V := l V) = [Vs [\<mapsto>] ls']"
[PROOF STATE]
proof (prove)
using this:
w = ls' ! index Vs V

goal (1 subgoal):
 1. [Vs [\<mapsto>] ls'](V := l V) = [Vs [\<mapsto>] ls']
[PROOF STEP]
using Some size VinVs
[PROOF STATE]
proof (prove)
using this:
w = ls' ! index Vs V
l V = \<lfloor>w\<rfloor>
length ls = length ls'
length Vs < length ls'
V \<in> set Vs

goal (1 subgoal):
 1. [Vs [\<mapsto>] ls'](V := l V) = [Vs [\<mapsto>] ls']
[PROOF STEP]
by(simp add:index_less_aux map_upds_upd_conv_index)
[PROOF STATE]
proof (state)
this:
[Vs [\<mapsto>] ls'](V := l V) = [Vs [\<mapsto>] ls']

goal (1 subgoal):
 1. \<And>a. l V = \<lfloor>a\<rfloor> \<Longrightarrow> [Vs [\<mapsto>] ls'](V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls']
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
[Vs [\<mapsto>] ls'](V := l V) = [Vs [\<mapsto>] ls']

goal (1 subgoal):
 1. [Vs [\<mapsto>] ls'](V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls']
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[Vs [\<mapsto>] ls'](V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls']

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
[Vs [\<mapsto>] ls'](V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls']

goal (1 subgoal):
 1. l'(V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls']
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
l'(V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls']
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
l'(V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls']

goal (1 subgoal):
 1. l'(V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls']
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
l'(V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls']

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ta_bisim01_extTA2J0_extTA2J1:
  assumes wf: "wf_J_prog P"
  and nt: "\<And>n T C M a h. \<lbrakk> n < length \<lbrace>ta\<rbrace>\<^bsub>t\<^esub>; \<lbrace>ta\<rbrace>\<^bsub>t\<^esub> ! n = NewThread T (C, M, a) h \<rbrakk>
           \<Longrightarrow> typeof_addr h a = \<lfloor>Class_type C\<rfloor> \<and> (\<exists>T meth D. P \<turnstile> C sees M:[]\<rightarrow>T =\<lfloor>meth\<rfloor> in D)"
  shows "ta_bisim01 (extTA2J0 P ta) (extTA2J1 (compP1 P) ta)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ta_bisim01 (extTA2J0 P ta) (extTA2J1 (compP1 P) ta)
[PROOF STEP]
apply(simp add: ta_bisim_def ta_upd_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_all2 (nta_bisim (\<lambda>t. bisim_red0_Red1)) (map (convert_new_thread_action (extNTA2J0 P)) \<lbrace>ta\<rbrace>\<^bsub>t\<^esub>) (map (convert_new_thread_action (extNTA2J1 (compP (\<lambda>C M Ts T (pns, y). compE1 (this # pns) y) P))) \<lbrace>ta\<rbrace>\<^bsub>t\<^esub>)
[PROOF STEP]
apply(auto intro!: list_all2_all_nthI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. n < length \<lbrace>ta\<rbrace>\<^bsub>t\<^esub> \<Longrightarrow> nta_bisim (\<lambda>t. bisim_red0_Red1) (convert_new_thread_action (extNTA2J0 P) (\<lbrace>ta\<rbrace>\<^bsub>t\<^esub> ! n)) (convert_new_thread_action (extNTA2J1 (compP (\<lambda>C M Ts T (pns, y). compE1 (this # pns) y) P)) (\<lbrace>ta\<rbrace>\<^bsub>t\<^esub> ! n))
[PROOF STEP]
apply(case_tac "\<lbrace>ta\<rbrace>\<^bsub>t\<^esub> ! n")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n x11 x12 x13. \<lbrakk>n < length \<lbrace>ta\<rbrace>\<^bsub>t\<^esub>; \<lbrace>ta\<rbrace>\<^bsub>t\<^esub> ! n = NewThread x11 x12 x13\<rbrakk> \<Longrightarrow> nta_bisim (\<lambda>t. bisim_red0_Red1) (convert_new_thread_action (extNTA2J0 P) (\<lbrace>ta\<rbrace>\<^bsub>t\<^esub> ! n)) (convert_new_thread_action (extNTA2J1 (compP (\<lambda>C M Ts T (pns, y). compE1 (this # pns) y) P)) (\<lbrace>ta\<rbrace>\<^bsub>t\<^esub> ! n))
 2. \<And>n x21 x22. \<lbrakk>n < length \<lbrace>ta\<rbrace>\<^bsub>t\<^esub>; \<lbrace>ta\<rbrace>\<^bsub>t\<^esub> ! n = ThreadExists x21 x22\<rbrakk> \<Longrightarrow> nta_bisim (\<lambda>t. bisim_red0_Red1) (convert_new_thread_action (extNTA2J0 P) (\<lbrace>ta\<rbrace>\<^bsub>t\<^esub> ! n)) (convert_new_thread_action (extNTA2J1 (compP (\<lambda>C M Ts T (pns, y). compE1 (this # pns) y) P)) (\<lbrace>ta\<rbrace>\<^bsub>t\<^esub> ! n))
[PROOF STEP]
apply(auto simp add: bisim_red0_Red1_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n x11 a aa b x13. \<lbrakk>n < length \<lbrace>ta\<rbrace>\<^bsub>t\<^esub>; \<lbrace>ta\<rbrace>\<^bsub>t\<^esub> ! n = NewThread x11 (a, aa, b) x13\<rbrakk> \<Longrightarrow> bisim_list1 ({this:Class (fst (method P a aa))=\<lfloor>Addr b\<rfloor>; snd (the (snd (snd (snd (method P a aa)))))}, []) (({0:Class (fst (method (compP (\<lambda>C M Ts T (pns, y). compE1 (this # pns) y) P) a aa))=None; the (snd (snd (snd (method (compP (\<lambda>C M Ts T (pns, y). compE1 (this # pns) y) P) a aa))))}, Addr b # replicate (max_vars (the (snd (snd (snd (method (compP (\<lambda>C M Ts T (pns, y). compE1 (this # pns) y) P) a aa)))))) undefined_value), [])
[PROOF STEP]
apply(drule (1) nt)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n x11 a aa b x13. \<lbrakk>\<lbrace>ta\<rbrace>\<^bsub>t\<^esub> ! n = NewThread x11 (a, aa, b) x13; typeof_addr x13 b = \<lfloor>Class_type a\<rfloor> \<and> (\<exists>T meth D. P \<turnstile> a sees aa: []\<rightarrow>T = \<lfloor>meth\<rfloor> in D)\<rbrakk> \<Longrightarrow> bisim_list1 ({this:Class (fst (method P a aa))=\<lfloor>Addr b\<rfloor>; snd (the (snd (snd (snd (method P a aa)))))}, []) (({0:Class (fst (method (compP (\<lambda>C M Ts T (pns, y). compE1 (this # pns) y) P) a aa))=None; the (snd (snd (snd (method (compP (\<lambda>C M Ts T (pns, y). compE1 (this # pns) y) P) a aa))))}, Addr b # replicate (max_vars (the (snd (snd (snd (method (compP (\<lambda>C M Ts T (pns, y). compE1 (this # pns) y) P) a aa)))))) undefined_value), [])
[PROOF STEP]
apply(clarify)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n x11 a aa b x13 T ab ba x. \<lbrakk>\<lbrace>ta\<rbrace>\<^bsub>t\<^esub> ! n = NewThread x11 (a, aa, b) x13; typeof_addr x13 b = \<lfloor>Class_type a\<rfloor>; P \<turnstile> a sees aa: []\<rightarrow>T = \<lfloor>(ab, ba)\<rfloor> in x\<rbrakk> \<Longrightarrow> bisim_list1 ({this:Class (fst (method P a aa))=\<lfloor>Addr b\<rfloor>; snd (the (snd (snd (snd (method P a aa)))))}, []) (({0:Class (fst (method (compP (\<lambda>C M Ts T (pns, y). compE1 (this # pns) y) P) a aa))=None; the (snd (snd (snd (method (compP (\<lambda>C M Ts T (pns, y). compE1 (this # pns) y) P) a aa))))}, Addr b # replicate (max_vars (the (snd (snd (snd (method (compP (\<lambda>C M Ts T (pns, y). compE1 (this # pns) y) P) a aa)))))) undefined_value), [])
[PROOF STEP]
apply(erule bisim_list_extTA2J0_extTA2J1[OF wf, simplified])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma red_external_ta_bisim01:
  "\<lbrakk> wf_J_prog P; P,t \<turnstile> \<langle>a\<bullet>M(vs), h\<rangle> -ta\<rightarrow>ext \<langle>va, h'\<rangle> \<rbrakk> \<Longrightarrow> ta_bisim01 (extTA2J0 P ta) (extTA2J1 (compP1 P) ta)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wf_J_prog P; P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>\<rbrakk> \<Longrightarrow> ta_bisim01 (extTA2J0 P ta) (extTA2J1 (compP1 P) ta)
[PROOF STEP]
apply(rule ta_bisim01_extTA2J0_extTA2J1, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n T C Ma aa ha. \<lbrakk>wf_J_prog P; P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>; n < length \<lbrace>ta\<rbrace>\<^bsub>t\<^esub>; \<lbrace>ta\<rbrace>\<^bsub>t\<^esub> ! n = NewThread T (C, Ma, aa) ha\<rbrakk> \<Longrightarrow> typeof_addr ha aa = \<lfloor>Class_type C\<rfloor> \<and> (\<exists>T meth D. P \<turnstile> C sees Ma: []\<rightarrow>T = \<lfloor>meth\<rfloor> in D)
[PROOF STEP]
apply(drule (1) red_external_new_thread_sees, auto simp add: in_set_conv_nth)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n T C Ma aa ha Ta aaa b x. \<lbrakk>P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>; n < length \<lbrace>ta\<rbrace>\<^bsub>t\<^esub>; \<lbrace>ta\<rbrace>\<^bsub>t\<^esub> ! n = NewThread T (C, Ma, aa) ha; typeof_addr h' aa = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C sees Ma: []\<rightarrow>Ta = \<lfloor>(aaa, b)\<rfloor> in x\<rbrakk> \<Longrightarrow> typeof_addr ha aa = \<lfloor>Class_type C\<rfloor>
[PROOF STEP]
apply(drule red_ext_new_thread_heap, auto simp add: in_set_conv_nth)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done