[STATEMENT]
lemma decompose[rule_format]:
 "\<forall>i. k \<in> set(trace d i xs) \<longrightarrow> (\<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))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. k \<in> set (trace d i xs) \<longrightarrow> (\<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))
[PROOF STEP]
apply (induct "xs")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>i. k \<in> set (trace d i []) \<longrightarrow> (\<exists>pref mids suf. [] = 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))
 2. \<And>a xs. \<forall>i. k \<in> set (trace d i xs) \<longrightarrow> (\<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)) \<Longrightarrow> \<forall>i. k \<in> set (trace d i (a # xs)) \<longrightarrow> (\<exists>pref mids suf. a # 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))
[PROOF STEP]
apply (simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<forall>i. k \<in> set (trace d i xs) \<longrightarrow> (\<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)) \<Longrightarrow> \<forall>i. k \<in> set (trace d i (a # xs)) \<longrightarrow> (\<exists>pref mids suf. a # 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))
[PROOF STEP]
apply (rename_tac a as)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a as. \<forall>i. k \<in> set (trace d i as) \<longrightarrow> (\<exists>pref mids suf. as = 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)) \<Longrightarrow> \<forall>i. k \<in> set (trace d i (a # as)) \<longrightarrow> (\<exists>pref mids suf. a # as = 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))
[PROOF STEP]
apply (intro strip)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a as i. \<lbrakk>\<forall>i. k \<in> set (trace d i as) \<longrightarrow> (\<exists>pref mids suf. as = 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)); k \<in> set (trace d i (a # as))\<rbrakk> \<Longrightarrow> \<exists>pref mids suf. a # as = 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)
[PROOF STEP]
apply (case_tac "d a i = k")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a as i. \<lbrakk>\<forall>i. k \<in> set (trace d i as) \<longrightarrow> (\<exists>pref mids suf. as = 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)); k \<in> set (trace d i (a # as)); d a i = k\<rbrakk> \<Longrightarrow> \<exists>pref mids suf. a # as = 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)
 2. \<And>a as i. \<lbrakk>\<forall>i. k \<in> set (trace d i as) \<longrightarrow> (\<exists>pref mids suf. as = 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)); k \<in> set (trace d i (a # as)); d a i \<noteq> k\<rbrakk> \<Longrightarrow> \<exists>pref mids suf. a # as = 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)
[PROOF STEP]
apply (rule_tac x = "[a]" in exI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a as i. \<lbrakk>\<forall>i. k \<in> set (trace d i as) \<longrightarrow> (\<exists>pref mids suf. as = 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)); k \<in> set (trace d i (a # as)); d a i = k\<rbrakk> \<Longrightarrow> \<exists>mids suf. a # as = [a] @ concat mids @ suf \<and> deltas d [a] i = k \<and> (\<forall>n\<in>set (butlast (trace d i [a])). 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)
 2. \<And>a as i. \<lbrakk>\<forall>i. k \<in> set (trace d i as) \<longrightarrow> (\<exists>pref mids suf. as = 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)); k \<in> set (trace d i (a # as)); d a i \<noteq> k\<rbrakk> \<Longrightarrow> \<exists>pref mids suf. a # as = 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)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a as i. \<lbrakk>\<forall>i. k \<in> set (trace d i as) \<longrightarrow> (\<exists>pref mids suf. as = 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)); d a i = k\<rbrakk> \<Longrightarrow> \<exists>mids suf. as = concat mids @ suf \<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)
 2. \<And>a as i. \<lbrakk>\<forall>i. k \<in> set (trace d i as) \<longrightarrow> (\<exists>pref mids suf. as = 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)); k \<in> set (trace d i (a # as)); d a i \<noteq> k\<rbrakk> \<Longrightarrow> \<exists>pref mids suf. a # as = 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)
[PROOF STEP]
apply (case_tac "k : set(trace d (d a i) as)")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a as i. \<lbrakk>\<forall>i. k \<in> set (trace d i as) \<longrightarrow> (\<exists>pref mids suf. as = 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)); d a i = k; k \<in> set (trace d (d a i) as)\<rbrakk> \<Longrightarrow> \<exists>mids suf. as = concat mids @ suf \<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)
 2. \<And>a as i. \<lbrakk>\<forall>i. k \<in> set (trace d i as) \<longrightarrow> (\<exists>pref mids suf. as = 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)); d a i = k; k \<notin> set (trace d (d a i) as)\<rbrakk> \<Longrightarrow> \<exists>mids suf. as = concat mids @ suf \<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)
 3. \<And>a as i. \<lbrakk>\<forall>i. k \<in> set (trace d i as) \<longrightarrow> (\<exists>pref mids suf. as = 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)); k \<in> set (trace d i (a # as)); d a i \<noteq> k\<rbrakk> \<Longrightarrow> \<exists>pref mids suf. a # as = 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)
[PROOF STEP]
apply (erule allE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a as i. \<lbrakk>d a i = k; k \<in> set (trace d (d a i) as); k \<in> set (trace d (?i16 a as i) as) \<longrightarrow> (\<exists>pref mids suf. as = pref @ concat mids @ suf \<and> deltas d pref (?i16 a as i) = k \<and> (\<forall>n\<in>set (butlast (trace d (?i16 a as 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>mids suf. as = concat mids @ suf \<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)
 2. \<And>a as i. \<lbrakk>\<forall>i. k \<in> set (trace d i as) \<longrightarrow> (\<exists>pref mids suf. as = 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)); d a i = k; k \<notin> set (trace d (d a i) as)\<rbrakk> \<Longrightarrow> \<exists>mids suf. as = concat mids @ suf \<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)
 3. \<And>a as i. \<lbrakk>\<forall>i. k \<in> set (trace d i as) \<longrightarrow> (\<exists>pref mids suf. as = 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)); k \<in> set (trace d i (a # as)); d a i \<noteq> k\<rbrakk> \<Longrightarrow> \<exists>pref mids suf. a # as = 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)
[PROOF STEP]
apply (erule impE)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a as i. \<lbrakk>d a i = k; k \<in> set (trace d (d a i) as)\<rbrakk> \<Longrightarrow> k \<in> set (trace d (?i16 a as i) as)
 2. \<And>a as i. \<lbrakk>d a i = k; k \<in> set (trace d (d a i) as); \<exists>pref mids suf. as = pref @ concat mids @ suf \<and> deltas d pref (?i16 a as i) = k \<and> (\<forall>n\<in>set (butlast (trace d (?i16 a as 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>mids suf. as = concat mids @ suf \<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)
 3. \<And>a as i. \<lbrakk>\<forall>i. k \<in> set (trace d i as) \<longrightarrow> (\<exists>pref mids suf. as = 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)); d a i = k; k \<notin> set (trace d (d a i) as)\<rbrakk> \<Longrightarrow> \<exists>mids suf. as = concat mids @ suf \<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)
 4. \<And>a as i. \<lbrakk>\<forall>i. k \<in> set (trace d i as) \<longrightarrow> (\<exists>pref mids suf. as = 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)); k \<in> set (trace d i (a # as)); d a i \<noteq> k\<rbrakk> \<Longrightarrow> \<exists>pref mids suf. a # as = 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)
[PROOF STEP]
apply (assumption)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a as i. \<lbrakk>d a i = k; k \<in> set (trace d (d a i) as); \<exists>pref mids suf. as = pref @ concat mids @ suf \<and> deltas d pref (d a i) = k \<and> (\<forall>n\<in>set (butlast (trace d (d a 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>mids suf. as = concat mids @ suf \<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)
 2. \<And>a as i. \<lbrakk>\<forall>i. k \<in> set (trace d i as) \<longrightarrow> (\<exists>pref mids suf. as = 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)); d a i = k; k \<notin> set (trace d (d a i) as)\<rbrakk> \<Longrightarrow> \<exists>mids suf. as = concat mids @ suf \<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)
 3. \<And>a as i. \<lbrakk>\<forall>i. k \<in> set (trace d i as) \<longrightarrow> (\<exists>pref mids suf. as = 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)); k \<in> set (trace d i (a # as)); d a i \<noteq> k\<rbrakk> \<Longrightarrow> \<exists>pref mids suf. a # as = 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)
[PROOF STEP]
apply (erule exE)+
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a as i pref mids suf. \<lbrakk>d a i = k; k \<in> set (trace d (d a i) as); as = pref @ concat mids @ suf \<and> deltas d pref (d a i) = k \<and> (\<forall>n\<in>set (butlast (trace d (d a 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>mids suf. as = concat mids @ suf \<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)
 2. \<And>a as i. \<lbrakk>\<forall>i. k \<in> set (trace d i as) \<longrightarrow> (\<exists>pref mids suf. as = 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)); d a i = k; k \<notin> set (trace d (d a i) as)\<rbrakk> \<Longrightarrow> \<exists>mids suf. as = concat mids @ suf \<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)
 3. \<And>a as i. \<lbrakk>\<forall>i. k \<in> set (trace d i as) \<longrightarrow> (\<exists>pref mids suf. as = 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)); k \<in> set (trace d i (a # as)); d a i \<noteq> k\<rbrakk> \<Longrightarrow> \<exists>pref mids suf. a # as = 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)
[PROOF STEP]
apply (rule_tac x = "pref#mids" in exI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a as i pref mids suf. \<lbrakk>d a i = k; k \<in> set (trace d (d a i) as); as = pref @ concat mids @ suf \<and> deltas d pref (d a i) = k \<and> (\<forall>n\<in>set (butlast (trace d (d a 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>suf. as = concat (pref # mids) @ suf \<and> (\<forall>mid\<in>set (pref # 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)
 2. \<And>a as i. \<lbrakk>\<forall>i. k \<in> set (trace d i as) \<longrightarrow> (\<exists>pref mids suf. as = 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)); d a i = k; k \<notin> set (trace d (d a i) as)\<rbrakk> \<Longrightarrow> \<exists>mids suf. as = concat mids @ suf \<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)
 3. \<And>a as i. \<lbrakk>\<forall>i. k \<in> set (trace d i as) \<longrightarrow> (\<exists>pref mids suf. as = 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)); k \<in> set (trace d i (a # as)); d a i \<noteq> k\<rbrakk> \<Longrightarrow> \<exists>pref mids suf. a # as = 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)
[PROOF STEP]
apply (rule_tac x = "suf" in exI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a as i pref mids suf. \<lbrakk>d a i = k; k \<in> set (trace d (d a i) as); as = pref @ concat mids @ suf \<and> deltas d pref (d a i) = k \<and> (\<forall>n\<in>set (butlast (trace d (d a 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> as = concat (pref # mids) @ suf \<and> (\<forall>mid\<in>set (pref # 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)
 2. \<And>a as i. \<lbrakk>\<forall>i. k \<in> set (trace d i as) \<longrightarrow> (\<exists>pref mids suf. as = 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)); d a i = k; k \<notin> set (trace d (d a i) as)\<rbrakk> \<Longrightarrow> \<exists>mids suf. as = concat mids @ suf \<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)
 3. \<And>a as i. \<lbrakk>\<forall>i. k \<in> set (trace d i as) \<longrightarrow> (\<exists>pref mids suf. as = 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)); k \<in> set (trace d i (a # as)); d a i \<noteq> k\<rbrakk> \<Longrightarrow> \<exists>pref mids suf. a # as = 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)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a as i. \<lbrakk>\<forall>i. k \<in> set (trace d i as) \<longrightarrow> (\<exists>pref mids suf. as = 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)); d a i = k; k \<notin> set (trace d (d a i) as)\<rbrakk> \<Longrightarrow> \<exists>mids suf. as = concat mids @ suf \<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)
 2. \<And>a as i. \<lbrakk>\<forall>i. k \<in> set (trace d i as) \<longrightarrow> (\<exists>pref mids suf. as = 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)); k \<in> set (trace d i (a # as)); d a i \<noteq> k\<rbrakk> \<Longrightarrow> \<exists>pref mids suf. a # as = 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)
[PROOF STEP]
apply (rule_tac x = "[]" in exI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a as i. \<lbrakk>\<forall>i. k \<in> set (trace d i as) \<longrightarrow> (\<exists>pref mids suf. as = 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)); d a i = k; k \<notin> set (trace d (d a i) as)\<rbrakk> \<Longrightarrow> \<exists>suf. as = concat [] @ suf \<and> (\<forall>mid\<in>set []. 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)
 2. \<And>a as i. \<lbrakk>\<forall>i. k \<in> set (trace d i as) \<longrightarrow> (\<exists>pref mids suf. as = 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)); k \<in> set (trace d i (a # as)); d a i \<noteq> k\<rbrakk> \<Longrightarrow> \<exists>pref mids suf. a # as = 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)
[PROOF STEP]
apply (rule_tac x = "as" in exI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a as i. \<lbrakk>\<forall>i. k \<in> set (trace d i as) \<longrightarrow> (\<exists>pref mids suf. as = 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)); d a i = k; k \<notin> set (trace d (d a i) as)\<rbrakk> \<Longrightarrow> as = concat [] @ as \<and> (\<forall>mid\<in>set []. 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 as)). n \<noteq> k)
 2. \<And>a as i. \<lbrakk>\<forall>i. k \<in> set (trace d i as) \<longrightarrow> (\<exists>pref mids suf. as = 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)); k \<in> set (trace d i (a # as)); d a i \<noteq> k\<rbrakk> \<Longrightarrow> \<exists>pref mids suf. a # as = 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)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a as i. \<lbrakk>\<forall>i. k \<in> set (trace d i as) \<longrightarrow> (\<exists>pref mids suf. as = 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)); d a i = k; k \<notin> set (trace d k as)\<rbrakk> \<Longrightarrow> \<forall>n\<in>set (butlast (trace d k as)). n \<noteq> k
 2. \<And>a as i. \<lbrakk>\<forall>i. k \<in> set (trace d i as) \<longrightarrow> (\<exists>pref mids suf. as = 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)); k \<in> set (trace d i (a # as)); d a i \<noteq> k\<rbrakk> \<Longrightarrow> \<exists>pref mids suf. a # as = 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)
[PROOF STEP]
apply (blast dest: in_set_butlastD)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a as i. \<lbrakk>\<forall>i. k \<in> set (trace d i as) \<longrightarrow> (\<exists>pref mids suf. as = 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)); k \<in> set (trace d i (a # as)); d a i \<noteq> k\<rbrakk> \<Longrightarrow> \<exists>pref mids suf. a # as = 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)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a as i. \<lbrakk>\<forall>i. k \<in> set (trace d i as) \<longrightarrow> (\<exists>pref mids suf. as = 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)); k \<in> set (trace d (d a i) as); d a i \<noteq> k\<rbrakk> \<Longrightarrow> \<exists>pref mids suf. a # as = 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)
[PROOF STEP]
apply (erule allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a as i. \<lbrakk>k \<in> set (trace d (d a i) as); d a i \<noteq> k; k \<in> set (trace d (?i59 a as i) as) \<longrightarrow> (\<exists>pref mids suf. as = pref @ concat mids @ suf \<and> deltas d pref (?i59 a as i) = k \<and> (\<forall>n\<in>set (butlast (trace d (?i59 a as 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>pref mids suf. a # as = 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)
[PROOF STEP]
apply (erule impE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a as i. \<lbrakk>k \<in> set (trace d (d a i) as); d a i \<noteq> k\<rbrakk> \<Longrightarrow> k \<in> set (trace d (?i59 a as i) as)
 2. \<And>a as i. \<lbrakk>k \<in> set (trace d (d a i) as); d a i \<noteq> k; \<exists>pref mids suf. as = pref @ concat mids @ suf \<and> deltas d pref (?i59 a as i) = k \<and> (\<forall>n\<in>set (butlast (trace d (?i59 a as 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>pref mids suf. a # as = 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)
[PROOF STEP]
apply (assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a as i. \<lbrakk>k \<in> set (trace d (d a i) as); d a i \<noteq> k; \<exists>pref mids suf. as = pref @ concat mids @ suf \<and> deltas d pref (d a i) = k \<and> (\<forall>n\<in>set (butlast (trace d (d a 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>pref mids suf. a # as = 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)
[PROOF STEP]
apply (erule exE)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a as i pref mids suf. \<lbrakk>k \<in> set (trace d (d a i) as); d a i \<noteq> k; as = pref @ concat mids @ suf \<and> deltas d pref (d a i) = k \<and> (\<forall>n\<in>set (butlast (trace d (d a 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>pref mids suf. a # as = 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)
[PROOF STEP]
apply (rule_tac x = "a#pref" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a as i pref mids suf. \<lbrakk>k \<in> set (trace d (d a i) as); d a i \<noteq> k; as = pref @ concat mids @ suf \<and> deltas d pref (d a i) = k \<and> (\<forall>n\<in>set (butlast (trace d (d a 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>mids suf. a # as = (a # pref) @ concat mids @ suf \<and> deltas d (a # pref) i = k \<and> (\<forall>n\<in>set (butlast (trace d i (a # 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)
[PROOF STEP]
apply (rule_tac x = "mids" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a as i pref mids suf. \<lbrakk>k \<in> set (trace d (d a i) as); d a i \<noteq> k; as = pref @ concat mids @ suf \<and> deltas d pref (d a i) = k \<and> (\<forall>n\<in>set (butlast (trace d (d a 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>suf. a # as = (a # pref) @ concat mids @ suf \<and> deltas d (a # pref) i = k \<and> (\<forall>n\<in>set (butlast (trace d i (a # 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)
[PROOF STEP]
apply (rule_tac x = "suf" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a as i pref mids suf. \<lbrakk>k \<in> set (trace d (d a i) as); d a i \<noteq> k; as = pref @ concat mids @ suf \<and> deltas d pref (d a i) = k \<and> (\<forall>n\<in>set (butlast (trace d (d a 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> a # as = (a # pref) @ concat mids @ suf \<and> deltas d (a # pref) i = k \<and> (\<forall>n\<in>set (butlast (trace d i (a # 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)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma length_trace[simp]: "\<And>i. length(trace d i xs) = length xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. length (trace d i xs) = length xs
[PROOF STEP]
by (induct "xs") simp_all


[STATEMENT]
lemma deltas_append[simp]:
  "\<And>i. deltas d (xs@ys) i = deltas d ys (deltas d xs i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. deltas d (xs @ ys) i = deltas d ys (deltas d xs i)
[PROOF STEP]
by (induct "xs") simp_all


[STATEMENT]
lemma trace_append[simp]:
  "\<And>i. trace d i (xs@ys) = trace d i xs @ trace d (deltas d xs i) ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. trace d i (xs @ ys) = trace d i xs @ trace d (deltas d xs i) ys
[PROOF STEP]
by (induct "xs") simp_all


[STATEMENT]
lemma trace_concat[simp]:
 "(\<forall>xs \<in> set xss. deltas d xs i = i) \<Longrightarrow>
  trace d i (concat xss) = concat (map (trace d i) xss)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>xs\<in>set xss. deltas d xs i = i \<Longrightarrow> trace d i (concat xss) = concat (map (trace d i) xss)
[PROOF STEP]
by (induct "xss") simp_all


[STATEMENT]
lemma trace_is_Nil[simp]: "\<And>i. (trace d i xs = []) = (xs = [])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. (trace d i xs = []) = (xs = [])
[PROOF STEP]
by (case_tac "xs") simp_all


[STATEMENT]
lemma trace_is_Cons_conv[simp]:
 "(trace d i xs = n#ns) =
  (case xs of [] \<Rightarrow> False | y#ys \<Rightarrow> n = d y i \<and> ns = trace d n ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (trace d i xs = n # ns) = (case xs of [] \<Rightarrow> False | y # ys \<Rightarrow> n = d y i \<and> ns = trace d n ys)
[PROOF STEP]
apply (case_tac "xs")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. xs = [] \<Longrightarrow> (trace d i xs = n # ns) = (case xs of [] \<Rightarrow> False | y # ys \<Rightarrow> n = d y i \<and> ns = trace d n ys)
 2. \<And>a list. xs = a # list \<Longrightarrow> (trace d i xs = n # ns) = (case xs of [] \<Rightarrow> False | y # ys \<Rightarrow> n = d y i \<and> ns = trace d n ys)
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a list. xs = a # list \<Longrightarrow> (d a i = n \<and> trace d (d a i) list = ns) = (n = d a i \<and> ns = trace d n list)
[PROOF STEP]
apply (blast)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma set_trace_conv:
 "\<And>i. set(trace d i xs) =
  (if xs=[] then {} else insert(deltas d xs i)(set(butlast(trace d i xs))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. set (trace d i xs) = (if xs = [] then {} else insert (deltas d xs i) (set (butlast (trace d i xs))))
[PROOF STEP]
apply (induct "xs")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i. set (trace d i []) = (if [] = [] then {} else insert (deltas d [] i) (set (butlast (trace d i []))))
 2. \<And>a xs i. (\<And>i. set (trace d i xs) = (if xs = [] then {} else insert (deltas d xs i) (set (butlast (trace d i xs))))) \<Longrightarrow> set (trace d i (a # xs)) = (if a # xs = [] then {} else insert (deltas d (a # xs) i) (set (butlast (trace d i (a # xs)))))
[PROOF STEP]
apply (simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a xs i. (\<And>i. set (trace d i xs) = (if xs = [] then {} else insert (deltas d xs i) (set (butlast (trace d i xs))))) \<Longrightarrow> set (trace d i (a # xs)) = (if a # xs = [] then {} else insert (deltas d (a # xs) i) (set (butlast (trace d i (a # xs)))))
[PROOF STEP]
apply (simp add: insert_commute)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma deltas_concat[simp]:
 "(\<forall>mid\<in>set mids. deltas d mid k = k) \<Longrightarrow> deltas d (concat mids) k = k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>mid\<in>set mids. deltas d mid k = k \<Longrightarrow> deltas d (concat mids) k = k
[PROOF STEP]
by (induct mids) simp_all


[STATEMENT]
lemma lem: "[| n < Suc k; n \<noteq> k |] ==> n < k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < Suc k; n \<noteq> k\<rbrakk> \<Longrightarrow> n < k
[PROOF STEP]
by arith