[STATEMENT]
lemma cd_in_cs: assumes \<open>n cd\<^bsup>\<pi>\<^esup>\<rightarrow> m\<close> shows \<open>\<exists> ns. cs\<^bsup>\<pi>\<^esup> n = (cs\<^bsup>\<pi>\<^esup> m) @ ns @[\<pi> n]\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>ns. cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>\<^esup> m @ ns @ [\<pi> n]
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
n cd\<^bsup>\<pi>\<^esup>\<rightarrow> m

goal (1 subgoal):
 1. \<exists>ns. cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>\<^esup> m @ ns @ [\<pi> n]
[PROOF STEP]
proof (induction rule: cd_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. i icd\<^bsup>\<pi>\<^esup>\<rightarrow> m \<Longrightarrow> \<exists>ns. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> m @ ns @ [\<pi> i]
 2. \<And>k' i'. \<lbrakk>k' cd\<^bsup>\<pi>\<^esup>\<rightarrow> m; \<exists>ns. cs\<^bsup>\<pi>\<^esup> k' = cs\<^bsup>\<pi>\<^esup> m @ ns @ [\<pi> k']; i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'\<rbrakk> \<Longrightarrow> \<exists>ns. cs\<^bsup>\<pi>\<^esup> i' = cs\<^bsup>\<pi>\<^esup> m @ ns @ [\<pi> i']
[PROOF STEP]
case (base  n)
[PROOF STATE]
proof (state)
this:
n icd\<^bsup>\<pi>\<^esup>\<rightarrow> m

goal (2 subgoals):
 1. \<And>i. i icd\<^bsup>\<pi>\<^esup>\<rightarrow> m \<Longrightarrow> \<exists>ns. cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> m @ ns @ [\<pi> i]
 2. \<And>k' i'. \<lbrakk>k' cd\<^bsup>\<pi>\<^esup>\<rightarrow> m; \<exists>ns. cs\<^bsup>\<pi>\<^esup> k' = cs\<^bsup>\<pi>\<^esup> m @ ns @ [\<pi> k']; i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'\<rbrakk> \<Longrightarrow> \<exists>ns. cs\<^bsup>\<pi>\<^esup> i' = cs\<^bsup>\<pi>\<^esup> m @ ns @ [\<pi> i']
[PROOF STEP]
thus \<open>?case\<close>
[PROOF STATE]
proof (prove)
using this:
n icd\<^bsup>\<pi>\<^esup>\<rightarrow> m

goal (1 subgoal):
 1. \<exists>ns. cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>\<^esup> m @ ns @ [\<pi> n]
[PROOF STEP]
by (metis append_Nil cs.simps icd_is_the_icd)
[PROOF STATE]
proof (state)
this:
\<exists>ns. cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>\<^esup> m @ ns @ [\<pi> n]

goal (1 subgoal):
 1. \<And>k' i'. \<lbrakk>k' cd\<^bsup>\<pi>\<^esup>\<rightarrow> m; \<exists>ns. cs\<^bsup>\<pi>\<^esup> k' = cs\<^bsup>\<pi>\<^esup> m @ ns @ [\<pi> k']; i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'\<rbrakk> \<Longrightarrow> \<exists>ns. cs\<^bsup>\<pi>\<^esup> i' = cs\<^bsup>\<pi>\<^esup> m @ ns @ [\<pi> i']
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k' i'. \<lbrakk>k' cd\<^bsup>\<pi>\<^esup>\<rightarrow> m; \<exists>ns. cs\<^bsup>\<pi>\<^esup> k' = cs\<^bsup>\<pi>\<^esup> m @ ns @ [\<pi> k']; i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'\<rbrakk> \<Longrightarrow> \<exists>ns. cs\<^bsup>\<pi>\<^esup> i' = cs\<^bsup>\<pi>\<^esup> m @ ns @ [\<pi> i']
[PROOF STEP]
case (IS k n)
[PROOF STATE]
proof (state)
this:
k cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
n icd\<^bsup>\<pi>\<^esup>\<rightarrow> k
\<exists>ns. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>\<^esup> m @ ns @ [\<pi> k]

goal (1 subgoal):
 1. \<And>k' i'. \<lbrakk>k' cd\<^bsup>\<pi>\<^esup>\<rightarrow> m; \<exists>ns. cs\<^bsup>\<pi>\<^esup> k' = cs\<^bsup>\<pi>\<^esup> m @ ns @ [\<pi> k']; i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'\<rbrakk> \<Longrightarrow> \<exists>ns. cs\<^bsup>\<pi>\<^esup> i' = cs\<^bsup>\<pi>\<^esup> m @ ns @ [\<pi> i']
[PROOF STEP]
hence \<open>cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>\<^esup> k @ [\<pi> n]\<close>
[PROOF STATE]
proof (prove)
using this:
k cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
n icd\<^bsup>\<pi>\<^esup>\<rightarrow> k
\<exists>ns. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>\<^esup> m @ ns @ [\<pi> k]

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>\<^esup> k @ [\<pi> n]
[PROOF STEP]
by (metis cs.simps icd_is_the_icd)
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>\<^esup> k @ [\<pi> n]

goal (1 subgoal):
 1. \<And>k' i'. \<lbrakk>k' cd\<^bsup>\<pi>\<^esup>\<rightarrow> m; \<exists>ns. cs\<^bsup>\<pi>\<^esup> k' = cs\<^bsup>\<pi>\<^esup> m @ ns @ [\<pi> k']; i' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'\<rbrakk> \<Longrightarrow> \<exists>ns. cs\<^bsup>\<pi>\<^esup> i' = cs\<^bsup>\<pi>\<^esup> m @ ns @ [\<pi> i']
[PROOF STEP]
thus \<open>?case\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>\<^esup> k @ [\<pi> n]

goal (1 subgoal):
 1. \<exists>ns. cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>\<^esup> m @ ns @ [\<pi> n]
[PROOF STEP]
using IS
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>\<^esup> k @ [\<pi> n]
k cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
n icd\<^bsup>\<pi>\<^esup>\<rightarrow> k
\<exists>ns. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>\<^esup> m @ ns @ [\<pi> k]

goal (1 subgoal):
 1. \<exists>ns. cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>\<^esup> m @ ns @ [\<pi> n]
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<exists>ns. cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>\<^esup> m @ ns @ [\<pi> n]

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma butlast_cs_not_cd: assumes \<open>butlast (cs\<^bsup>\<pi>\<^esup> m) = butlast (cs\<^bsup>\<pi>\<^esup> n)\<close> shows \<open>\<not> m cd\<^bsup>\<pi>\<^esup>\<rightarrow>n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> m cd\<^bsup>\<pi>\<^esup>\<rightarrow> n
[PROOF STEP]
by (metis append_Cons append_Nil append_assoc assms cd_in_cs cs_not_nil list.distinct(1) self_append_conv snoc_eq_iff_butlast)


[STATEMENT]
lemma wn_cs_butlast: assumes \<open>butlast (cs\<^bsup>\<pi>\<^esup> m) = butlast (cs\<^bsup>\<pi>\<^esup> n)\<close> \<open>i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m\<close> \<open>j cd\<^bsup>\<pi>\<^esup>\<rightarrow> n\<close> \<open>m<n\<close> shows \<open>i<j\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < j
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> i < j \<Longrightarrow> False
[PROOF STEP]
assume \<open>\<not> i < j\<close>
[PROOF STATE]
proof (state)
this:
\<not> i < j

goal (1 subgoal):
 1. \<not> i < j \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<not> i < j

goal (1 subgoal):
 1. \<not> i < j \<Longrightarrow> False
[PROOF STEP]
have \<open>\<not> n cd\<^bsup>\<pi>\<^esup>\<rightarrow> m\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> n cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
[PROOF STEP]
by (metis assms(1) butlast_cs_not_cd)
[PROOF STATE]
proof (state)
this:
\<not> n cd\<^bsup>\<pi>\<^esup>\<rightarrow> m

goal (1 subgoal):
 1. \<not> i < j \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<not> i < j
\<not> n cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
[PROOF STEP]
have \<open>n \<le> m\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> i < j
\<not> n cd\<^bsup>\<pi>\<^esup>\<rightarrow> m

goal (1 subgoal):
 1. n \<le> m
[PROOF STEP]
using assms(2,3) cr_wn''
[PROOF STATE]
proof (prove)
using this:
\<not> i < j
\<not> n cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
j cd\<^bsup>\<pi>\<^esup>\<rightarrow> n
\<lbrakk>?i cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?m; ?j cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?n; \<not> ?m cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?n; ?i \<le> ?j\<rbrakk> \<Longrightarrow> ?m \<le> ?n

goal (1 subgoal):
 1. n \<le> m
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n \<le> m

goal (1 subgoal):
 1. \<not> i < j \<Longrightarrow> False
[PROOF STEP]
thus \<open>False\<close>
[PROOF STATE]
proof (prove)
using this:
n \<le> m

goal (1 subgoal):
 1. False
[PROOF STEP]
using assms(4)
[PROOF STATE]
proof (prove)
using this:
n \<le> m
m < n

goal (1 subgoal):
 1. False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem cs_order: assumes path: \<open>is_path \<pi>\<close> \<open>is_path \<pi>'\<close> and csi: \<open>cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'\<close>
and csj: \<open>cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<close> and nret: \<open>\<pi> i \<noteq> return\<close> and ilj: \<open>i < j\<close>
shows \<open>i'<j'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i' < j'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i' < j'
[PROOF STEP]
have \<open>cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>\<^esup> j\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>\<^esup> j
[PROOF STEP]
using cs_inj[OF path(1) nret] ilj
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> ?n' \<Longrightarrow> i = ?n'
i < j

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>\<^esup> j
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>\<^esup> j

goal (1 subgoal):
 1. i' < j'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>\<^esup> j

goal (1 subgoal):
 1. i' < j'
[PROOF STEP]
have \<open>cs\<^bsup>\<pi>\<^esup> i \<noteq> Nil\<close> \<open>cs\<^bsup>\<pi>\<^esup> j \<noteq> Nil\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> i \<noteq> [] &&& cs\<^bsup>\<pi>\<^esup> j \<noteq> []
[PROOF STEP]
by (metis cs_not_nil)+
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> i \<noteq> []
cs\<^bsup>\<pi>\<^esup> j \<noteq> []

goal (1 subgoal):
 1. i' < j'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>\<^esup> j
cs\<^bsup>\<pi>\<^esup> i \<noteq> []
cs\<^bsup>\<pi>\<^esup> j \<noteq> []
[PROOF STEP]
show \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>\<^esup> j
cs\<^bsup>\<pi>\<^esup> i \<noteq> []
cs\<^bsup>\<pi>\<^esup> j \<noteq> []

goal (1 subgoal):
 1. i' < j'
[PROOF STEP]
proof (cases rule: list_neq_prefix_cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>xs x x' ys ys'. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i = xs @ [x] @ ys; cs\<^bsup>\<pi>\<^esup> j = xs @ [x'] @ ys'; x \<noteq> x'\<rbrakk> \<Longrightarrow> i' < j'
 2. \<And>xs. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> j @ xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> i' < j'
 3. \<And>xs. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i @ xs = cs\<^bsup>\<pi>\<^esup> j; xs \<noteq> []\<rbrakk> \<Longrightarrow> i' < j'
[PROOF STEP]
case (diverge xs x x' ys ys')
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> i = xs @ [x] @ ys
cs\<^bsup>\<pi>\<^esup> j = xs @ [x'] @ ys'
x \<noteq> x'

goal (3 subgoals):
 1. \<And>xs x x' ys ys'. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i = xs @ [x] @ ys; cs\<^bsup>\<pi>\<^esup> j = xs @ [x'] @ ys'; x \<noteq> x'\<rbrakk> \<Longrightarrow> i' < j'
 2. \<And>xs. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> j @ xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> i' < j'
 3. \<And>xs. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i @ xs = cs\<^bsup>\<pi>\<^esup> j; xs \<noteq> []\<rbrakk> \<Longrightarrow> i' < j'
[PROOF STEP]
note csx = \<open>cs\<^bsup>\<pi>\<^esup> i = xs @ [x] @ ys\<close>
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> i = xs @ [x] @ ys

goal (3 subgoals):
 1. \<And>xs x x' ys ys'. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i = xs @ [x] @ ys; cs\<^bsup>\<pi>\<^esup> j = xs @ [x'] @ ys'; x \<noteq> x'\<rbrakk> \<Longrightarrow> i' < j'
 2. \<And>xs. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> j @ xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> i' < j'
 3. \<And>xs. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i @ xs = cs\<^bsup>\<pi>\<^esup> j; xs \<noteq> []\<rbrakk> \<Longrightarrow> i' < j'
[PROOF STEP]
note csx' = \<open>cs\<^bsup>\<pi>\<^esup> j = xs @ [x'] @ ys'\<close>
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> j = xs @ [x'] @ ys'

goal (3 subgoals):
 1. \<And>xs x x' ys ys'. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i = xs @ [x] @ ys; cs\<^bsup>\<pi>\<^esup> j = xs @ [x'] @ ys'; x \<noteq> x'\<rbrakk> \<Longrightarrow> i' < j'
 2. \<And>xs. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> j @ xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> i' < j'
 3. \<And>xs. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i @ xs = cs\<^bsup>\<pi>\<^esup> j; xs \<noteq> []\<rbrakk> \<Longrightarrow> i' < j'
[PROOF STEP]
note xx = \<open>x \<noteq> x'\<close>
[PROOF STATE]
proof (state)
this:
x \<noteq> x'

goal (3 subgoals):
 1. \<And>xs x x' ys ys'. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i = xs @ [x] @ ys; cs\<^bsup>\<pi>\<^esup> j = xs @ [x'] @ ys'; x \<noteq> x'\<rbrakk> \<Longrightarrow> i' < j'
 2. \<And>xs. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> j @ xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> i' < j'
 3. \<And>xs. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i @ xs = cs\<^bsup>\<pi>\<^esup> j; xs \<noteq> []\<rbrakk> \<Longrightarrow> i' < j'
[PROOF STEP]
show \<open>i' < j'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i' < j'
[PROOF STEP]
proof (cases \<open>ys\<close>)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ys = [] \<Longrightarrow> i' < j'
 2. \<And>a list. ys = a # list \<Longrightarrow> i' < j'
[PROOF STEP]
assume ys: \<open>ys = Nil\<close>
[PROOF STATE]
proof (state)
this:
ys = []

goal (2 subgoals):
 1. ys = [] \<Longrightarrow> i' < j'
 2. \<And>a list. ys = a # list \<Longrightarrow> i' < j'
[PROOF STEP]
show \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i' < j'
[PROOF STEP]
proof (cases \<open>ys'\<close>)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ys' = [] \<Longrightarrow> i' < j'
 2. \<And>a list. ys' = a # list \<Longrightarrow> i' < j'
[PROOF STEP]
assume ys': \<open>ys' = Nil\<close>
[PROOF STATE]
proof (state)
this:
ys' = []

goal (2 subgoals):
 1. ys' = [] \<Longrightarrow> i' < j'
 2. \<And>a list. ys' = a # list \<Longrightarrow> i' < j'
[PROOF STEP]
have cs: \<open>cs\<^bsup>\<pi>\<^esup> i = xs @ [x]\<close> \<open>cs\<^bsup>\<pi>\<^esup> j = xs @ [x']\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> i = xs @ [x] &&& cs\<^bsup>\<pi>\<^esup> j = xs @ [x']
[PROOF STEP]
by (metis append_Nil2 csx ys, metis append_Nil2 csx' ys')
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> i = xs @ [x]
cs\<^bsup>\<pi>\<^esup> j = xs @ [x']

goal (2 subgoals):
 1. ys' = [] \<Longrightarrow> i' < j'
 2. \<And>a list. ys' = a # list \<Longrightarrow> i' < j'
[PROOF STEP]
hence bl: \<open>butlast (cs\<^bsup>\<pi>\<^esup> i) = butlast (cs\<^bsup>\<pi>\<^esup> j)\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> i = xs @ [x]
cs\<^bsup>\<pi>\<^esup> j = xs @ [x']

goal (1 subgoal):
 1. butlast (cs\<^bsup>\<pi>\<^esup> i) = butlast (cs\<^bsup>\<pi>\<^esup> j)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
butlast (cs\<^bsup>\<pi>\<^esup> i) = butlast (cs\<^bsup>\<pi>\<^esup> j)

goal (2 subgoals):
 1. ys' = [] \<Longrightarrow> i' < j'
 2. \<And>a list. ys' = a # list \<Longrightarrow> i' < j'
[PROOF STEP]
show \<open>i' < j'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i' < j'
[PROOF STEP]
using claim[OF path csi csj bl nret ilj]
[PROOF STATE]
proof (prove)
using this:
i' < j'

goal (1 subgoal):
 1. i' < j'
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
i' < j'

goal (1 subgoal):
 1. \<And>a list. ys' = a # list \<Longrightarrow> i' < j'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. ys' = a # list \<Longrightarrow> i' < j'
[PROOF STEP]
fix y' zs'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. ys' = a # list \<Longrightarrow> i' < j'
[PROOF STEP]
assume ys': \<open>ys' = y'#zs'\<close>
[PROOF STATE]
proof (state)
this:
ys' = y' # zs'

goal (1 subgoal):
 1. \<And>a list. ys' = a # list \<Longrightarrow> i' < j'
[PROOF STEP]
have cs: \<open>cs\<^bsup>\<pi>\<^esup> i = xs @ [x]\<close> \<open>cs\<^bsup>\<pi>\<^esup> j = xs @ [x',y']@ zs'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> i = xs @ [x] &&& cs\<^bsup>\<pi>\<^esup> j = xs @ [x', y'] @ zs'
[PROOF STEP]
by (metis append_Nil2 csx ys, metis append_Cons append_Nil csx' ys')
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> i = xs @ [x]
cs\<^bsup>\<pi>\<^esup> j = xs @ [x', y'] @ zs'

goal (1 subgoal):
 1. \<And>a list. ys' = a # list \<Longrightarrow> i' < j'
[PROOF STEP]
obtain n where n: \<open>cs\<^bsup>\<pi>\<^esup> n = xs@[x']\<close> and jn: \<open>j cd\<^bsup>\<pi>\<^esup>\<rightarrow> n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>n. \<lbrakk>cs\<^bsup>\<pi>\<^esup> n = xs @ [x']; j cd\<^bsup>\<pi>\<^esup>\<rightarrow> n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using cs cs_split'
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> i = xs @ [x]
cs\<^bsup>\<pi>\<^esup> j = xs @ [x', y'] @ zs'
cs\<^bsup>?\<pi>\<^esup> ?i = ?xs @ [?x, ?x'] @ ?ys \<Longrightarrow> \<exists>m. cs\<^bsup>?\<pi>\<^esup> m = ?xs @ [?x] \<and> ?i cd\<^bsup>?\<pi>\<^esup>\<rightarrow> m

goal (1 subgoal):
 1. (\<And>n. \<lbrakk>cs\<^bsup>\<pi>\<^esup> n = xs @ [x']; j cd\<^bsup>\<pi>\<^esup>\<rightarrow> n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> n = xs @ [x']
j cd\<^bsup>\<pi>\<^esup>\<rightarrow> n

goal (1 subgoal):
 1. \<And>a list. ys' = a # list \<Longrightarrow> i' < j'
[PROOF STEP]
obtain n' where n': \<open>cs\<^bsup>\<pi>'\<^esup> n' = xs@[x']\<close> and jn': \<open>j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> n'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>n'. \<lbrakk>cs\<^bsup>\<pi>'\<^esup> n' = xs @ [x']; j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> n'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using cs cs_split'
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> i = xs @ [x]
cs\<^bsup>\<pi>\<^esup> j = xs @ [x', y'] @ zs'
cs\<^bsup>?\<pi>\<^esup> ?i = ?xs @ [?x, ?x'] @ ?ys \<Longrightarrow> \<exists>m. cs\<^bsup>?\<pi>\<^esup> m = ?xs @ [?x] \<and> ?i cd\<^bsup>?\<pi>\<^esup>\<rightarrow> m

goal (1 subgoal):
 1. (\<And>n'. \<lbrakk>cs\<^bsup>\<pi>'\<^esup> n' = xs @ [x']; j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> n'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding csj
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> i = xs @ [x]
cs\<^bsup>\<pi>'\<^esup> j' = xs @ [x', y'] @ zs'
cs\<^bsup>?\<pi>\<^esup> ?i = ?xs @ [?x, ?x'] @ ?ys \<Longrightarrow> \<exists>m. cs\<^bsup>?\<pi>\<^esup> m = ?xs @ [?x] \<and> ?i cd\<^bsup>?\<pi>\<^esup>\<rightarrow> m

goal (1 subgoal):
 1. (\<And>n'. \<lbrakk>cs\<^bsup>\<pi>'\<^esup> n' = xs @ [x']; j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> n'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>'\<^esup> n' = xs @ [x']
j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> n'

goal (1 subgoal):
 1. \<And>a list. ys' = a # list \<Longrightarrow> i' < j'
[PROOF STEP]
have csn : \<open>cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n'\<close> and bl: \<open>butlast (cs\<^bsup>\<pi>\<^esup> i) = butlast (cs\<^bsup>\<pi>\<^esup> n)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n' &&& butlast (cs\<^bsup>\<pi>\<^esup> i) = butlast (cs\<^bsup>\<pi>\<^esup> n)
[PROOF STEP]
using n n' cs
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> n = xs @ [x']
cs\<^bsup>\<pi>'\<^esup> n' = xs @ [x']
cs\<^bsup>\<pi>\<^esup> i = xs @ [x]
cs\<^bsup>\<pi>\<^esup> j = xs @ [x', y'] @ zs'

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n' &&& butlast (cs\<^bsup>\<pi>\<^esup> i) = butlast (cs\<^bsup>\<pi>\<^esup> n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n'
butlast (cs\<^bsup>\<pi>\<^esup> i) = butlast (cs\<^bsup>\<pi>\<^esup> n)

goal (1 subgoal):
 1. \<And>a list. ys' = a # list \<Longrightarrow> i' < j'
[PROOF STEP]
hence bl': \<open>butlast (cs\<^bsup>\<pi>'\<^esup> i') = butlast (cs\<^bsup>\<pi>'\<^esup> n')\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n'
butlast (cs\<^bsup>\<pi>\<^esup> i) = butlast (cs\<^bsup>\<pi>\<^esup> n)

goal (1 subgoal):
 1. butlast (cs\<^bsup>\<pi>'\<^esup> i') = butlast (cs\<^bsup>\<pi>'\<^esup> n')
[PROOF STEP]
using csi
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n'
butlast (cs\<^bsup>\<pi>\<^esup> i) = butlast (cs\<^bsup>\<pi>\<^esup> n)
cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'

goal (1 subgoal):
 1. butlast (cs\<^bsup>\<pi>'\<^esup> i') = butlast (cs\<^bsup>\<pi>'\<^esup> n')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
butlast (cs\<^bsup>\<pi>'\<^esup> i') = butlast (cs\<^bsup>\<pi>'\<^esup> n')

goal (1 subgoal):
 1. \<And>a list. ys' = a # list \<Longrightarrow> i' < j'
[PROOF STEP]
have notcd: \<open>\<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> n
[PROOF STEP]
by (metis butlast_cs_not_cd bl)
[PROOF STATE]
proof (state)
this:
\<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> n

goal (1 subgoal):
 1. \<And>a list. ys' = a # list \<Longrightarrow> i' < j'
[PROOF STEP]
have nin: \<open>i \<noteq> n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<noteq> n
[PROOF STEP]
using cs n xx
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> i = xs @ [x]
cs\<^bsup>\<pi>\<^esup> j = xs @ [x', y'] @ zs'
cs\<^bsup>\<pi>\<^esup> n = xs @ [x']
x \<noteq> x'

goal (1 subgoal):
 1. i \<noteq> n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i \<noteq> n

goal (1 subgoal):
 1. \<And>a list. ys' = a # list \<Longrightarrow> i' < j'
[PROOF STEP]
have iln: \<open>i < n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < n
[PROOF STEP]
apply (rule ccontr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> i < n \<Longrightarrow> False
[PROOF STEP]
using cr_wn'[OF jn notcd] nin ilj
[PROOF STATE]
proof (prove)
using this:
n < i \<Longrightarrow> j < i
i \<noteq> n
i < j

goal (1 subgoal):
 1. \<not> i < n \<Longrightarrow> False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < n

goal (1 subgoal):
 1. \<And>a list. ys' = a # list \<Longrightarrow> i' < j'
[PROOF STEP]
note claim[OF path csi csn bl nret iln]
[PROOF STATE]
proof (state)
this:
i' < n'

goal (1 subgoal):
 1. \<And>a list. ys' = a # list \<Longrightarrow> i' < j'
[PROOF STEP]
hence \<open>i' < n'\<close>
[PROOF STATE]
proof (prove)
using this:
i' < n'

goal (1 subgoal):
 1. i' < n'
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
i' < n'

goal (1 subgoal):
 1. \<And>a list. ys' = a # list \<Longrightarrow> i' < j'
[PROOF STEP]
thus \<open>i' < j'\<close>
[PROOF STATE]
proof (prove)
using this:
i' < n'

goal (1 subgoal):
 1. i' < j'
[PROOF STEP]
using jn'
[PROOF STATE]
proof (prove)
using this:
i' < n'
j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> n'

goal (1 subgoal):
 1. i' < j'
[PROOF STEP]
unfolding is_cdi_def
[PROOF STATE]
proof (prove)
using this:
i' < n'
is_path \<pi>' \<and> n' < j' \<and> \<pi>' j' \<noteq> local.return \<and> (\<forall>j\<in>{n'..j'}. \<pi>' j \<noteq> ipd (\<pi>' n'))

goal (1 subgoal):
 1. i' < j'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i' < j'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
i' < j'

goal (1 subgoal):
 1. \<And>a list. ys = a # list \<Longrightarrow> i' < j'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. ys = a # list \<Longrightarrow> i' < j'
[PROOF STEP]
fix y zs
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. ys = a # list \<Longrightarrow> i' < j'
[PROOF STEP]
assume ys: \<open>ys = y#zs\<close>
[PROOF STATE]
proof (state)
this:
ys = y # zs

goal (1 subgoal):
 1. \<And>a list. ys = a # list \<Longrightarrow> i' < j'
[PROOF STEP]
show \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i' < j'
[PROOF STEP]
proof (cases \<open>ys'\<close>)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ys' = [] \<Longrightarrow> i' < j'
 2. \<And>a list. ys' = a # list \<Longrightarrow> i' < j'
[PROOF STEP]
assume ys' : \<open>ys' = Nil\<close>
[PROOF STATE]
proof (state)
this:
ys' = []

goal (2 subgoals):
 1. ys' = [] \<Longrightarrow> i' < j'
 2. \<And>a list. ys' = a # list \<Longrightarrow> i' < j'
[PROOF STEP]
have cs: \<open>cs\<^bsup>\<pi>\<^esup> i = xs @ [x,y]@zs\<close> \<open>cs\<^bsup>\<pi>\<^esup> j = xs @ [x']\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> i = xs @ [x, y] @ zs &&& cs\<^bsup>\<pi>\<^esup> j = xs @ [x']
[PROOF STEP]
by (metis append_Cons append_Nil csx ys, metis append_Nil2 csx' ys')
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> i = xs @ [x, y] @ zs
cs\<^bsup>\<pi>\<^esup> j = xs @ [x']

goal (2 subgoals):
 1. ys' = [] \<Longrightarrow> i' < j'
 2. \<And>a list. ys' = a # list \<Longrightarrow> i' < j'
[PROOF STEP]
obtain n where n: \<open>cs\<^bsup>\<pi>\<^esup> n = xs@[x]\<close> and jn: \<open>i cd\<^bsup>\<pi>\<^esup>\<rightarrow> n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>n. \<lbrakk>cs\<^bsup>\<pi>\<^esup> n = xs @ [x]; i cd\<^bsup>\<pi>\<^esup>\<rightarrow> n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using cs cs_split'
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> i = xs @ [x, y] @ zs
cs\<^bsup>\<pi>\<^esup> j = xs @ [x']
cs\<^bsup>?\<pi>\<^esup> ?i = ?xs @ [?x, ?x'] @ ?ys \<Longrightarrow> \<exists>m. cs\<^bsup>?\<pi>\<^esup> m = ?xs @ [?x] \<and> ?i cd\<^bsup>?\<pi>\<^esup>\<rightarrow> m

goal (1 subgoal):
 1. (\<And>n. \<lbrakk>cs\<^bsup>\<pi>\<^esup> n = xs @ [x]; i cd\<^bsup>\<pi>\<^esup>\<rightarrow> n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> n = xs @ [x]
i cd\<^bsup>\<pi>\<^esup>\<rightarrow> n

goal (2 subgoals):
 1. ys' = [] \<Longrightarrow> i' < j'
 2. \<And>a list. ys' = a # list \<Longrightarrow> i' < j'
[PROOF STEP]
obtain n' where n': \<open>cs\<^bsup>\<pi>'\<^esup> n' = xs@[x]\<close> and jn': \<open>i' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> n'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>n'. \<lbrakk>cs\<^bsup>\<pi>'\<^esup> n' = xs @ [x]; i' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> n'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using cs cs_split'
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> i = xs @ [x, y] @ zs
cs\<^bsup>\<pi>\<^esup> j = xs @ [x']
cs\<^bsup>?\<pi>\<^esup> ?i = ?xs @ [?x, ?x'] @ ?ys \<Longrightarrow> \<exists>m. cs\<^bsup>?\<pi>\<^esup> m = ?xs @ [?x] \<and> ?i cd\<^bsup>?\<pi>\<^esup>\<rightarrow> m

goal (1 subgoal):
 1. (\<And>n'. \<lbrakk>cs\<^bsup>\<pi>'\<^esup> n' = xs @ [x]; i' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> n'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding csi
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>'\<^esup> i' = xs @ [x, y] @ zs
cs\<^bsup>\<pi>\<^esup> j = xs @ [x']
cs\<^bsup>?\<pi>\<^esup> ?i = ?xs @ [?x, ?x'] @ ?ys \<Longrightarrow> \<exists>m. cs\<^bsup>?\<pi>\<^esup> m = ?xs @ [?x] \<and> ?i cd\<^bsup>?\<pi>\<^esup>\<rightarrow> m

goal (1 subgoal):
 1. (\<And>n'. \<lbrakk>cs\<^bsup>\<pi>'\<^esup> n' = xs @ [x]; i' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> n'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>'\<^esup> n' = xs @ [x]
i' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> n'

goal (2 subgoals):
 1. ys' = [] \<Longrightarrow> i' < j'
 2. \<And>a list. ys' = a # list \<Longrightarrow> i' < j'
[PROOF STEP]
have csn : \<open>cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n'\<close> and bl: \<open>butlast (cs\<^bsup>\<pi>\<^esup> n) = butlast (cs\<^bsup>\<pi>\<^esup> j)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n' &&& butlast (cs\<^bsup>\<pi>\<^esup> n) = butlast (cs\<^bsup>\<pi>\<^esup> j)
[PROOF STEP]
using n n' cs
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> n = xs @ [x]
cs\<^bsup>\<pi>'\<^esup> n' = xs @ [x]
cs\<^bsup>\<pi>\<^esup> i = xs @ [x, y] @ zs
cs\<^bsup>\<pi>\<^esup> j = xs @ [x']

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n' &&& butlast (cs\<^bsup>\<pi>\<^esup> n) = butlast (cs\<^bsup>\<pi>\<^esup> j)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n'
butlast (cs\<^bsup>\<pi>\<^esup> n) = butlast (cs\<^bsup>\<pi>\<^esup> j)

goal (2 subgoals):
 1. ys' = [] \<Longrightarrow> i' < j'
 2. \<And>a list. ys' = a # list \<Longrightarrow> i' < j'
[PROOF STEP]
hence bl': \<open>butlast (cs\<^bsup>\<pi>'\<^esup> j') = butlast (cs\<^bsup>\<pi>'\<^esup> n')\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n'
butlast (cs\<^bsup>\<pi>\<^esup> n) = butlast (cs\<^bsup>\<pi>\<^esup> j)

goal (1 subgoal):
 1. butlast (cs\<^bsup>\<pi>'\<^esup> j') = butlast (cs\<^bsup>\<pi>'\<^esup> n')
[PROOF STEP]
using csj
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n'
butlast (cs\<^bsup>\<pi>\<^esup> n) = butlast (cs\<^bsup>\<pi>\<^esup> j)
cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'

goal (1 subgoal):
 1. butlast (cs\<^bsup>\<pi>'\<^esup> j') = butlast (cs\<^bsup>\<pi>'\<^esup> n')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
butlast (cs\<^bsup>\<pi>'\<^esup> j') = butlast (cs\<^bsup>\<pi>'\<^esup> n')

goal (2 subgoals):
 1. ys' = [] \<Longrightarrow> i' < j'
 2. \<And>a list. ys' = a # list \<Longrightarrow> i' < j'
[PROOF STEP]
have notcd: \<open>\<not> j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> n'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> n'
[PROOF STEP]
by (metis butlast_cs_not_cd bl')
[PROOF STATE]
proof (state)
this:
\<not> j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> n'

goal (2 subgoals):
 1. ys' = [] \<Longrightarrow> i' < j'
 2. \<And>a list. ys' = a # list \<Longrightarrow> i' < j'
[PROOF STEP]
have nin: \<open>n < i\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < i
[PROOF STEP]
using jn
[PROOF STATE]
proof (prove)
using this:
i cd\<^bsup>\<pi>\<^esup>\<rightarrow> n

goal (1 subgoal):
 1. n < i
[PROOF STEP]
unfolding is_cdi_def
[PROOF STATE]
proof (prove)
using this:
is_path \<pi> \<and> n < i \<and> \<pi> i \<noteq> local.return \<and> (\<forall>j\<in>{n..i}. \<pi> j \<noteq> ipd (\<pi> n))

goal (1 subgoal):
 1. n < i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n < i

goal (2 subgoals):
 1. ys' = [] \<Longrightarrow> i' < j'
 2. \<And>a list. ys' = a # list \<Longrightarrow> i' < j'
[PROOF STEP]
have nlj: \<open>n < j\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < j
[PROOF STEP]
using nin ilj
[PROOF STATE]
proof (prove)
using this:
n < i
i < j

goal (1 subgoal):
 1. n < j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n < j

goal (2 subgoals):
 1. ys' = [] \<Longrightarrow> i' < j'
 2. \<And>a list. ys' = a # list \<Longrightarrow> i' < j'
[PROOF STEP]
note claim[OF path csn csj bl _ nlj]
[PROOF STATE]
proof (state)
this:
\<pi> n \<noteq> local.return \<Longrightarrow> n' < j'

goal (2 subgoals):
 1. ys' = [] \<Longrightarrow> i' < j'
 2. \<And>a list. ys' = a # list \<Longrightarrow> i' < j'
[PROOF STEP]
hence nj': \<open>n' < j'\<close>
[PROOF STATE]
proof (prove)
using this:
\<pi> n \<noteq> local.return \<Longrightarrow> n' < j'

goal (1 subgoal):
 1. n' < j'
[PROOF STEP]
using term_path_stable[OF path(1) _] less_imp_le nin nret
[PROOF STATE]
proof (prove)
using this:
\<pi> n \<noteq> local.return \<Longrightarrow> n' < j'
\<lbrakk>\<pi> ?i = local.return; ?i \<le> ?j\<rbrakk> \<Longrightarrow> \<pi> ?j = local.return
?x < ?y \<Longrightarrow> ?x \<le> ?y
n < i
\<pi> i \<noteq> local.return

goal (1 subgoal):
 1. n' < j'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n' < j'

goal (2 subgoals):
 1. ys' = [] \<Longrightarrow> i' < j'
 2. \<And>a list. ys' = a # list \<Longrightarrow> i' < j'
[PROOF STEP]
show \<open>i' < j'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i' < j'
[PROOF STEP]
apply(rule ccontr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> i' < j' \<Longrightarrow> False
[PROOF STEP]
using cdi_prefix[OF jn' nj'] notcd
[PROOF STATE]
proof (prove)
using this:
j' \<le> i' \<Longrightarrow> j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> n'
\<not> j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> n'

goal (1 subgoal):
 1. \<not> i' < j' \<Longrightarrow> False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i' < j'

goal (1 subgoal):
 1. \<And>a list. ys' = a # list \<Longrightarrow> i' < j'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. ys' = a # list \<Longrightarrow> i' < j'
[PROOF STEP]
fix y' zs'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. ys' = a # list \<Longrightarrow> i' < j'
[PROOF STEP]
assume ys' : \<open>ys' = y'#zs'\<close>
[PROOF STATE]
proof (state)
this:
ys' = y' # zs'

goal (1 subgoal):
 1. \<And>a list. ys' = a # list \<Longrightarrow> i' < j'
[PROOF STEP]
have cs: \<open>cs\<^bsup>\<pi>\<^esup> i = xs@[x,y]@zs\<close> \<open>cs\<^bsup>\<pi>\<^esup> j = xs@[x',y']@zs'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> i = xs @ [x, y] @ zs &&& cs\<^bsup>\<pi>\<^esup> j = xs @ [x', y'] @ zs'
[PROOF STEP]
by (metis append_Cons append_Nil csx ys,metis append_Cons append_Nil csx' ys')
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> i = xs @ [x, y] @ zs
cs\<^bsup>\<pi>\<^esup> j = xs @ [x', y'] @ zs'

goal (1 subgoal):
 1. \<And>a list. ys' = a # list \<Longrightarrow> i' < j'
[PROOF STEP]
have neq: \<open>cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>\<^esup> j\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>\<^esup> j
[PROOF STEP]
using cs_inj path nret ilj
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_path ?\<pi>; ?\<pi> ?n \<noteq> local.return; cs\<^bsup>?\<pi>\<^esup> ?n = cs\<^bsup>?\<pi>\<^esup> ?n'\<rbrakk> \<Longrightarrow> ?n = ?n'
is_path \<pi>
is_path \<pi>'
\<pi> i \<noteq> local.return
i < j

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>\<^esup> j
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> i \<noteq> cs\<^bsup>\<pi>\<^esup> j

goal (1 subgoal):
 1. \<And>a list. ys' = a # list \<Longrightarrow> i' < j'
[PROOF STEP]
obtain m where m: \<open>cs\<^bsup>\<pi>\<^esup> m = xs@[x]\<close> and im: \<open>i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>m. \<lbrakk>cs\<^bsup>\<pi>\<^esup> m = xs @ [x]; i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using cs cs_split'
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> i = xs @ [x, y] @ zs
cs\<^bsup>\<pi>\<^esup> j = xs @ [x', y'] @ zs'
cs\<^bsup>?\<pi>\<^esup> ?i = ?xs @ [?x, ?x'] @ ?ys \<Longrightarrow> \<exists>m. cs\<^bsup>?\<pi>\<^esup> m = ?xs @ [?x] \<and> ?i cd\<^bsup>?\<pi>\<^esup>\<rightarrow> m

goal (1 subgoal):
 1. (\<And>m. \<lbrakk>cs\<^bsup>\<pi>\<^esup> m = xs @ [x]; i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> m = xs @ [x]
i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m

goal (1 subgoal):
 1. \<And>a list. ys' = a # list \<Longrightarrow> i' < j'
[PROOF STEP]
obtain n where n: \<open>cs\<^bsup>\<pi>\<^esup> n = xs@[x']\<close> and jn: \<open>j cd\<^bsup>\<pi>\<^esup>\<rightarrow> n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>n. \<lbrakk>cs\<^bsup>\<pi>\<^esup> n = xs @ [x']; j cd\<^bsup>\<pi>\<^esup>\<rightarrow> n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using cs cs_split'
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> i = xs @ [x, y] @ zs
cs\<^bsup>\<pi>\<^esup> j = xs @ [x', y'] @ zs'
cs\<^bsup>?\<pi>\<^esup> ?i = ?xs @ [?x, ?x'] @ ?ys \<Longrightarrow> \<exists>m. cs\<^bsup>?\<pi>\<^esup> m = ?xs @ [?x] \<and> ?i cd\<^bsup>?\<pi>\<^esup>\<rightarrow> m

goal (1 subgoal):
 1. (\<And>n. \<lbrakk>cs\<^bsup>\<pi>\<^esup> n = xs @ [x']; j cd\<^bsup>\<pi>\<^esup>\<rightarrow> n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> n = xs @ [x']
j cd\<^bsup>\<pi>\<^esup>\<rightarrow> n

goal (1 subgoal):
 1. \<And>a list. ys' = a # list \<Longrightarrow> i' < j'
[PROOF STEP]
obtain m' where m': \<open>cs\<^bsup>\<pi>'\<^esup> m' = xs@[x]\<close> and im': \<open>i' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> m'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>m'. \<lbrakk>cs\<^bsup>\<pi>'\<^esup> m' = xs @ [x]; i' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> m'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using cs cs_split'
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> i = xs @ [x, y] @ zs
cs\<^bsup>\<pi>\<^esup> j = xs @ [x', y'] @ zs'
cs\<^bsup>?\<pi>\<^esup> ?i = ?xs @ [?x, ?x'] @ ?ys \<Longrightarrow> \<exists>m. cs\<^bsup>?\<pi>\<^esup> m = ?xs @ [?x] \<and> ?i cd\<^bsup>?\<pi>\<^esup>\<rightarrow> m

goal (1 subgoal):
 1. (\<And>m'. \<lbrakk>cs\<^bsup>\<pi>'\<^esup> m' = xs @ [x]; i' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> m'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding csi
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>'\<^esup> i' = xs @ [x, y] @ zs
cs\<^bsup>\<pi>\<^esup> j = xs @ [x', y'] @ zs'
cs\<^bsup>?\<pi>\<^esup> ?i = ?xs @ [?x, ?x'] @ ?ys \<Longrightarrow> \<exists>m. cs\<^bsup>?\<pi>\<^esup> m = ?xs @ [?x] \<and> ?i cd\<^bsup>?\<pi>\<^esup>\<rightarrow> m

goal (1 subgoal):
 1. (\<And>m'. \<lbrakk>cs\<^bsup>\<pi>'\<^esup> m' = xs @ [x]; i' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> m'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>'\<^esup> m' = xs @ [x]
i' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> m'

goal (1 subgoal):
 1. \<And>a list. ys' = a # list \<Longrightarrow> i' < j'
[PROOF STEP]
obtain n' where n': \<open>cs\<^bsup>\<pi>'\<^esup> n' = xs@[x']\<close> and jn': \<open>j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> n'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>n'. \<lbrakk>cs\<^bsup>\<pi>'\<^esup> n' = xs @ [x']; j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> n'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using cs cs_split'
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> i = xs @ [x, y] @ zs
cs\<^bsup>\<pi>\<^esup> j = xs @ [x', y'] @ zs'
cs\<^bsup>?\<pi>\<^esup> ?i = ?xs @ [?x, ?x'] @ ?ys \<Longrightarrow> \<exists>m. cs\<^bsup>?\<pi>\<^esup> m = ?xs @ [?x] \<and> ?i cd\<^bsup>?\<pi>\<^esup>\<rightarrow> m

goal (1 subgoal):
 1. (\<And>n'. \<lbrakk>cs\<^bsup>\<pi>'\<^esup> n' = xs @ [x']; j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> n'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding csj
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> i = xs @ [x, y] @ zs
cs\<^bsup>\<pi>'\<^esup> j' = xs @ [x', y'] @ zs'
cs\<^bsup>?\<pi>\<^esup> ?i = ?xs @ [?x, ?x'] @ ?ys \<Longrightarrow> \<exists>m. cs\<^bsup>?\<pi>\<^esup> m = ?xs @ [?x] \<and> ?i cd\<^bsup>?\<pi>\<^esup>\<rightarrow> m

goal (1 subgoal):
 1. (\<And>n'. \<lbrakk>cs\<^bsup>\<pi>'\<^esup> n' = xs @ [x']; j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> n'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>'\<^esup> n' = xs @ [x']
j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> n'

goal (1 subgoal):
 1. \<And>a list. ys' = a # list \<Longrightarrow> i' < j'
[PROOF STEP]
have \<open>m \<le> n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m \<le> n
[PROOF STEP]
using ilj m n wn_cs_butlast[OF _ jn im]
[PROOF STATE]
proof (prove)
using this:
i < j
cs\<^bsup>\<pi>\<^esup> m = xs @ [x]
cs\<^bsup>\<pi>\<^esup> n = xs @ [x']
\<lbrakk>butlast (cs\<^bsup>\<pi>\<^esup> n) = butlast (cs\<^bsup>\<pi>\<^esup> m); n < m\<rbrakk> \<Longrightarrow> j < i

goal (1 subgoal):
 1. m \<le> n
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
m \<le> n

goal (1 subgoal):
 1. \<And>a list. ys' = a # list \<Longrightarrow> i' < j'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
m \<le> n

goal (1 subgoal):
 1. \<And>a list. ys' = a # list \<Longrightarrow> i' < j'
[PROOF STEP]
have \<open>m \<noteq> n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m \<noteq> n
[PROOF STEP]
using m n xx
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> m = xs @ [x]
cs\<^bsup>\<pi>\<^esup> n = xs @ [x']
x \<noteq> x'

goal (1 subgoal):
 1. m \<noteq> n
[PROOF STEP]
by (metis last_snoc)
[PROOF STATE]
proof (state)
this:
m \<noteq> n

goal (1 subgoal):
 1. \<And>a list. ys' = a # list \<Longrightarrow> i' < j'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
m \<le> n
m \<noteq> n
[PROOF STEP]
have mn: \<open>m < n\<close>
[PROOF STATE]
proof (prove)
using this:
m \<le> n
m \<noteq> n

goal (1 subgoal):
 1. m < n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
m < n

goal (1 subgoal):
 1. \<And>a list. ys' = a # list \<Longrightarrow> i' < j'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
m < n

goal (1 subgoal):
 1. \<And>a list. ys' = a # list \<Longrightarrow> i' < j'
[PROOF STEP]
have \<open>\<pi> m \<noteq> return\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> m \<noteq> local.return
[PROOF STEP]
by (metis last_cs last_snoc m mn n path(1) term_path_stable xx less_imp_le)
[PROOF STATE]
proof (state)
this:
\<pi> m \<noteq> local.return

goal (1 subgoal):
 1. \<And>a list. ys' = a # list \<Longrightarrow> i' < j'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<pi> m \<noteq> local.return

goal (1 subgoal):
 1. \<And>a list. ys' = a # list \<Longrightarrow> i' < j'
[PROOF STEP]
have \<open>butlast (cs\<^bsup>\<pi>\<^esup> m) = butlast (cs\<^bsup>\<pi>\<^esup> n)\<close> \<open>cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'\<close> \<open>cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. butlast (cs\<^bsup>\<pi>\<^esup> m) = butlast (cs\<^bsup>\<pi>\<^esup> n) &&& cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m' &&& cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n'
[PROOF STEP]
using m n n' m'
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> m = xs @ [x]
cs\<^bsup>\<pi>\<^esup> n = xs @ [x']
cs\<^bsup>\<pi>'\<^esup> n' = xs @ [x']
cs\<^bsup>\<pi>'\<^esup> m' = xs @ [x]

goal (1 subgoal):
 1. butlast (cs\<^bsup>\<pi>\<^esup> m) = butlast (cs\<^bsup>\<pi>\<^esup> n) &&& cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m' &&& cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
butlast (cs\<^bsup>\<pi>\<^esup> m) = butlast (cs\<^bsup>\<pi>\<^esup> n)
cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'
cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n'

goal (1 subgoal):
 1. \<And>a list. ys' = a # list \<Longrightarrow> i' < j'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
m < n
\<pi> m \<noteq> local.return
butlast (cs\<^bsup>\<pi>\<^esup> m) = butlast (cs\<^bsup>\<pi>\<^esup> n)
cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'
cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n'
[PROOF STEP]
have \<open>m' < n'\<close>
[PROOF STATE]
proof (prove)
using this:
m < n
\<pi> m \<noteq> local.return
butlast (cs\<^bsup>\<pi>\<^esup> m) = butlast (cs\<^bsup>\<pi>\<^esup> n)
cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'
cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n'

goal (1 subgoal):
 1. m' < n'
[PROOF STEP]
using claim path
[PROOF STATE]
proof (prove)
using this:
m < n
\<pi> m \<noteq> local.return
butlast (cs\<^bsup>\<pi>\<^esup> m) = butlast (cs\<^bsup>\<pi>\<^esup> n)
cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m'
cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n'
\<lbrakk>is_path ?\<pi>; is_path ?\<pi>'; cs\<^bsup>?\<pi>\<^esup> ?i = cs\<^bsup>?\<pi>'\<^esup> ?i'; cs\<^bsup>?\<pi>\<^esup> ?j = cs\<^bsup>?\<pi>'\<^esup> ?j'; butlast (cs\<^bsup>?\<pi>\<^esup> ?i) = butlast (cs\<^bsup>?\<pi>\<^esup> ?j); ?\<pi> ?i \<noteq> local.return; ?i < ?j\<rbrakk> \<Longrightarrow> ?i' < ?j'
is_path \<pi>
is_path \<pi>'

goal (1 subgoal):
 1. m' < n'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
m' < n'

goal (1 subgoal):
 1. \<And>a list. ys' = a # list \<Longrightarrow> i' < j'
[PROOF STEP]
thus \<open>i' < j'\<close>
[PROOF STATE]
proof (prove)
using this:
m' < n'

goal (1 subgoal):
 1. i' < j'
[PROOF STEP]
using m' n' im' jn' wn_cs_butlast
[PROOF STATE]
proof (prove)
using this:
m' < n'
cs\<^bsup>\<pi>'\<^esup> m' = xs @ [x]
cs\<^bsup>\<pi>'\<^esup> n' = xs @ [x']
i' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> m'
j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> n'
\<lbrakk>butlast (cs\<^bsup>?\<pi>\<^esup> ?m) = butlast (cs\<^bsup>?\<pi>\<^esup> ?n); ?i cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?m; ?j cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?n; ?m < ?n\<rbrakk> \<Longrightarrow> ?i < ?j

goal (1 subgoal):
 1. i' < j'
[PROOF STEP]
by (metis butlast_snoc)
[PROOF STATE]
proof (state)
this:
i' < j'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
i' < j'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
i' < j'

goal (2 subgoals):
 1. \<And>xs. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> j @ xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> i' < j'
 2. \<And>xs. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i @ xs = cs\<^bsup>\<pi>\<^esup> j; xs \<noteq> []\<rbrakk> \<Longrightarrow> i' < j'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xs. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> j @ xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> i' < j'
 2. \<And>xs. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i @ xs = cs\<^bsup>\<pi>\<^esup> j; xs \<noteq> []\<rbrakk> \<Longrightarrow> i' < j'
[PROOF STEP]
case (prefix1 xs)
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> j @ xs
xs \<noteq> []

goal (2 subgoals):
 1. \<And>xs. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> j @ xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> i' < j'
 2. \<And>xs. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i @ xs = cs\<^bsup>\<pi>\<^esup> j; xs \<noteq> []\<rbrakk> \<Longrightarrow> i' < j'
[PROOF STEP]
note pfx = \<open>cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> j @ xs\<close>
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> j @ xs

goal (2 subgoals):
 1. \<And>xs. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> j @ xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> i' < j'
 2. \<And>xs. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i @ xs = cs\<^bsup>\<pi>\<^esup> j; xs \<noteq> []\<rbrakk> \<Longrightarrow> i' < j'
[PROOF STEP]
note xs = \<open>xs \<noteq> []\<close>
[PROOF STATE]
proof (state)
this:
xs \<noteq> []

goal (2 subgoals):
 1. \<And>xs. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> j @ xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> i' < j'
 2. \<And>xs. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i @ xs = cs\<^bsup>\<pi>\<^esup> j; xs \<noteq> []\<rbrakk> \<Longrightarrow> i' < j'
[PROOF STEP]
obtain a as where \<open>xs = a#as\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a as. xs = a # as \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using xs
[PROOF STATE]
proof (prove)
using this:
xs \<noteq> []

goal (1 subgoal):
 1. (\<And>a as. xs = a # as \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis list.exhaust)
[PROOF STATE]
proof (state)
this:
xs = a # as

goal (2 subgoals):
 1. \<And>xs. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> j @ xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> i' < j'
 2. \<And>xs. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i @ xs = cs\<^bsup>\<pi>\<^esup> j; xs \<noteq> []\<rbrakk> \<Longrightarrow> i' < j'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
xs = a # as

goal (2 subgoals):
 1. \<And>xs. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> j @ xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> i' < j'
 2. \<And>xs. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i @ xs = cs\<^bsup>\<pi>\<^esup> j; xs \<noteq> []\<rbrakk> \<Longrightarrow> i' < j'
[PROOF STEP]
obtain bs b where bj: \<open>cs\<^bsup>\<pi>\<^esup> j = bs@[b]\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>bs b. cs\<^bsup>\<pi>\<^esup> j = bs @ [b] \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using cs_not_nil
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>?\<pi>\<^esup> ?n \<noteq> []

goal (1 subgoal):
 1. (\<And>bs b. cs\<^bsup>\<pi>\<^esup> j = bs @ [b] \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis rev_exhaust)
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> j = bs @ [b]

goal (2 subgoals):
 1. \<And>xs. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> j @ xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> i' < j'
 2. \<And>xs. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i @ xs = cs\<^bsup>\<pi>\<^esup> j; xs \<noteq> []\<rbrakk> \<Longrightarrow> i' < j'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
xs = a # as
cs\<^bsup>\<pi>\<^esup> j = bs @ [b]
[PROOF STEP]
have \<open>cs\<^bsup>\<pi>\<^esup> i = bs@[b,a]@as\<close>
[PROOF STATE]
proof (prove)
using this:
xs = a # as
cs\<^bsup>\<pi>\<^esup> j = bs @ [b]

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> i = bs @ [b, a] @ as
[PROOF STEP]
using pfx
[PROOF STATE]
proof (prove)
using this:
xs = a # as
cs\<^bsup>\<pi>\<^esup> j = bs @ [b]
cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> j @ xs

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> i = bs @ [b, a] @ as
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> i = bs @ [b, a] @ as

goal (2 subgoals):
 1. \<And>xs. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> j @ xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> i' < j'
 2. \<And>xs. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i @ xs = cs\<^bsup>\<pi>\<^esup> j; xs \<noteq> []\<rbrakk> \<Longrightarrow> i' < j'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
cs\<^bsup>\<pi>\<^esup> i = bs @ [b, a] @ as
[PROOF STEP]
obtain m where \<open>cs\<^bsup>\<pi>\<^esup> m = bs@[b]\<close> and cdep:  \<open>i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> i = bs @ [b, a] @ as

goal (1 subgoal):
 1. (\<And>m. \<lbrakk>cs\<^bsup>\<pi>\<^esup> m = bs @ [b]; i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using cs_split'
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> i = bs @ [b, a] @ as
cs\<^bsup>?\<pi>\<^esup> ?i = ?xs @ [?x, ?x'] @ ?ys \<Longrightarrow> \<exists>m. cs\<^bsup>?\<pi>\<^esup> m = ?xs @ [?x] \<and> ?i cd\<^bsup>?\<pi>\<^esup>\<rightarrow> m

goal (1 subgoal):
 1. (\<And>m. \<lbrakk>cs\<^bsup>\<pi>\<^esup> m = bs @ [b]; i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> m = bs @ [b]
i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m

goal (2 subgoals):
 1. \<And>xs. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> j @ xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> i' < j'
 2. \<And>xs. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i @ xs = cs\<^bsup>\<pi>\<^esup> j; xs \<noteq> []\<rbrakk> \<Longrightarrow> i' < j'
[PROOF STEP]
hence mi: \<open>m = j\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> m = bs @ [b]
i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m

goal (1 subgoal):
 1. m = j
[PROOF STEP]
using bj cs_inj
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> m = bs @ [b]
i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
cs\<^bsup>\<pi>\<^esup> j = bs @ [b]
\<lbrakk>is_path ?\<pi>; ?\<pi> ?n \<noteq> local.return; cs\<^bsup>?\<pi>\<^esup> ?n = cs\<^bsup>?\<pi>\<^esup> ?n'\<rbrakk> \<Longrightarrow> ?n = ?n'

goal (1 subgoal):
 1. m = j
[PROOF STEP]
by (metis is_cdi_def term_path_stable less_imp_le)
[PROOF STATE]
proof (state)
this:
m = j

goal (2 subgoals):
 1. \<And>xs. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> j @ xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> i' < j'
 2. \<And>xs. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i @ xs = cs\<^bsup>\<pi>\<^esup> j; xs \<noteq> []\<rbrakk> \<Longrightarrow> i' < j'
[PROOF STEP]
hence \<open>i cd\<^bsup>\<pi>\<^esup>\<rightarrow> j\<close>
[PROOF STATE]
proof (prove)
using this:
m = j

goal (1 subgoal):
 1. i cd\<^bsup>\<pi>\<^esup>\<rightarrow> j
[PROOF STEP]
using cdep
[PROOF STATE]
proof (prove)
using this:
m = j
i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m

goal (1 subgoal):
 1. i cd\<^bsup>\<pi>\<^esup>\<rightarrow> j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i cd\<^bsup>\<pi>\<^esup>\<rightarrow> j

goal (2 subgoals):
 1. \<And>xs. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> j @ xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> i' < j'
 2. \<And>xs. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i @ xs = cs\<^bsup>\<pi>\<^esup> j; xs \<noteq> []\<rbrakk> \<Longrightarrow> i' < j'
[PROOF STEP]
hence \<open>False\<close>
[PROOF STATE]
proof (prove)
using this:
i cd\<^bsup>\<pi>\<^esup>\<rightarrow> j

goal (1 subgoal):
 1. False
[PROOF STEP]
using ilj
[PROOF STATE]
proof (prove)
using this:
i cd\<^bsup>\<pi>\<^esup>\<rightarrow> j
i < j

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding is_cdi_def
[PROOF STATE]
proof (prove)
using this:
is_path \<pi> \<and> j < i \<and> \<pi> i \<noteq> local.return \<and> (\<forall>ja\<in>{j..i}. \<pi> ja \<noteq> ipd (\<pi> j))
i < j

goal (1 subgoal):
 1. False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
False

goal (2 subgoals):
 1. \<And>xs. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> j @ xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> i' < j'
 2. \<And>xs. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i @ xs = cs\<^bsup>\<pi>\<^esup> j; xs \<noteq> []\<rbrakk> \<Longrightarrow> i' < j'
[PROOF STEP]
thus \<open>i' < j'\<close>
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. i' < j'
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
i' < j'

goal (1 subgoal):
 1. \<And>xs. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i @ xs = cs\<^bsup>\<pi>\<^esup> j; xs \<noteq> []\<rbrakk> \<Longrightarrow> i' < j'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i @ xs = cs\<^bsup>\<pi>\<^esup> j; xs \<noteq> []\<rbrakk> \<Longrightarrow> i' < j'
[PROOF STEP]
case (prefix2 xs)
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> i @ xs = cs\<^bsup>\<pi>\<^esup> j
xs \<noteq> []

goal (1 subgoal):
 1. \<And>xs. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i @ xs = cs\<^bsup>\<pi>\<^esup> j; xs \<noteq> []\<rbrakk> \<Longrightarrow> i' < j'
[PROOF STEP]
have pfx : \<open>cs\<^bsup>\<pi>'\<^esup> i' @ xs = cs\<^bsup>\<pi>'\<^esup> j'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>'\<^esup> i' @ xs = cs\<^bsup>\<pi>'\<^esup> j'
[PROOF STEP]
using prefix2 csi csj
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> i @ xs = cs\<^bsup>\<pi>\<^esup> j
xs \<noteq> []
cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'
cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'

goal (1 subgoal):
 1. cs\<^bsup>\<pi>'\<^esup> i' @ xs = cs\<^bsup>\<pi>'\<^esup> j'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>'\<^esup> i' @ xs = cs\<^bsup>\<pi>'\<^esup> j'

goal (1 subgoal):
 1. \<And>xs. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i @ xs = cs\<^bsup>\<pi>\<^esup> j; xs \<noteq> []\<rbrakk> \<Longrightarrow> i' < j'
[PROOF STEP]
note xs = \<open>xs \<noteq> []\<close>
[PROOF STATE]
proof (state)
this:
xs \<noteq> []

goal (1 subgoal):
 1. \<And>xs. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i @ xs = cs\<^bsup>\<pi>\<^esup> j; xs \<noteq> []\<rbrakk> \<Longrightarrow> i' < j'
[PROOF STEP]
obtain a as where \<open>xs = a#as\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a as. xs = a # as \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using xs
[PROOF STATE]
proof (prove)
using this:
xs \<noteq> []

goal (1 subgoal):
 1. (\<And>a as. xs = a # as \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis list.exhaust)
[PROOF STATE]
proof (state)
this:
xs = a # as

goal (1 subgoal):
 1. \<And>xs. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i @ xs = cs\<^bsup>\<pi>\<^esup> j; xs \<noteq> []\<rbrakk> \<Longrightarrow> i' < j'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
xs = a # as

goal (1 subgoal):
 1. \<And>xs. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i @ xs = cs\<^bsup>\<pi>\<^esup> j; xs \<noteq> []\<rbrakk> \<Longrightarrow> i' < j'
[PROOF STEP]
obtain bs b where bj: \<open>cs\<^bsup>\<pi>'\<^esup> i'  = bs@[b]\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>bs b. cs\<^bsup>\<pi>'\<^esup> i' = bs @ [b] \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using cs_not_nil
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>?\<pi>\<^esup> ?n \<noteq> []

goal (1 subgoal):
 1. (\<And>bs b. cs\<^bsup>\<pi>'\<^esup> i' = bs @ [b] \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis rev_exhaust)
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>'\<^esup> i' = bs @ [b]

goal (1 subgoal):
 1. \<And>xs. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i @ xs = cs\<^bsup>\<pi>\<^esup> j; xs \<noteq> []\<rbrakk> \<Longrightarrow> i' < j'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
xs = a # as
cs\<^bsup>\<pi>'\<^esup> i' = bs @ [b]
[PROOF STEP]
have \<open>cs\<^bsup>\<pi>'\<^esup> j' = bs@[b,a]@as\<close>
[PROOF STATE]
proof (prove)
using this:
xs = a # as
cs\<^bsup>\<pi>'\<^esup> i' = bs @ [b]

goal (1 subgoal):
 1. cs\<^bsup>\<pi>'\<^esup> j' = bs @ [b, a] @ as
[PROOF STEP]
using pfx
[PROOF STATE]
proof (prove)
using this:
xs = a # as
cs\<^bsup>\<pi>'\<^esup> i' = bs @ [b]
cs\<^bsup>\<pi>'\<^esup> i' @ xs = cs\<^bsup>\<pi>'\<^esup> j'

goal (1 subgoal):
 1. cs\<^bsup>\<pi>'\<^esup> j' = bs @ [b, a] @ as
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>'\<^esup> j' = bs @ [b, a] @ as

goal (1 subgoal):
 1. \<And>xs. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i @ xs = cs\<^bsup>\<pi>\<^esup> j; xs \<noteq> []\<rbrakk> \<Longrightarrow> i' < j'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
cs\<^bsup>\<pi>'\<^esup> j' = bs @ [b, a] @ as
[PROOF STEP]
obtain m where \<open>cs\<^bsup>\<pi>'\<^esup> m = bs@[b]\<close> and cdep:  \<open>j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> m\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>'\<^esup> j' = bs @ [b, a] @ as

goal (1 subgoal):
 1. (\<And>m. \<lbrakk>cs\<^bsup>\<pi>'\<^esup> m = bs @ [b]; j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> m\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using cs_split'
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>'\<^esup> j' = bs @ [b, a] @ as
cs\<^bsup>?\<pi>\<^esup> ?i = ?xs @ [?x, ?x'] @ ?ys \<Longrightarrow> \<exists>m. cs\<^bsup>?\<pi>\<^esup> m = ?xs @ [?x] \<and> ?i cd\<^bsup>?\<pi>\<^esup>\<rightarrow> m

goal (1 subgoal):
 1. (\<And>m. \<lbrakk>cs\<^bsup>\<pi>'\<^esup> m = bs @ [b]; j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> m\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>'\<^esup> m = bs @ [b]
j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> m

goal (1 subgoal):
 1. \<And>xs. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i @ xs = cs\<^bsup>\<pi>\<^esup> j; xs \<noteq> []\<rbrakk> \<Longrightarrow> i' < j'
[PROOF STEP]
hence mi: \<open>m = i'\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>'\<^esup> m = bs @ [b]
j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> m

goal (1 subgoal):
 1. m = i'
[PROOF STEP]
using bj cs_inj
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>'\<^esup> m = bs @ [b]
j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> m
cs\<^bsup>\<pi>'\<^esup> i' = bs @ [b]
\<lbrakk>is_path ?\<pi>; ?\<pi> ?n \<noteq> local.return; cs\<^bsup>?\<pi>\<^esup> ?n = cs\<^bsup>?\<pi>\<^esup> ?n'\<rbrakk> \<Longrightarrow> ?n = ?n'

goal (1 subgoal):
 1. m = i'
[PROOF STEP]
by (metis is_cdi_def term_path_stable less_imp_le)
[PROOF STATE]
proof (state)
this:
m = i'

goal (1 subgoal):
 1. \<And>xs. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i @ xs = cs\<^bsup>\<pi>\<^esup> j; xs \<noteq> []\<rbrakk> \<Longrightarrow> i' < j'
[PROOF STEP]
hence \<open>j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i'\<close>
[PROOF STATE]
proof (prove)
using this:
m = i'

goal (1 subgoal):
 1. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i'
[PROOF STEP]
using cdep
[PROOF STATE]
proof (prove)
using this:
m = i'
j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> m

goal (1 subgoal):
 1. j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i'

goal (1 subgoal):
 1. \<And>xs. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i @ xs = cs\<^bsup>\<pi>\<^esup> j; xs \<noteq> []\<rbrakk> \<Longrightarrow> i' < j'
[PROOF STEP]
thus \<open>i' < j'\<close>
[PROOF STATE]
proof (prove)
using this:
j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> i'

goal (1 subgoal):
 1. i' < j'
[PROOF STEP]
unfolding is_cdi_def
[PROOF STATE]
proof (prove)
using this:
is_path \<pi>' \<and> i' < j' \<and> \<pi>' j' \<noteq> local.return \<and> (\<forall>j\<in>{i'..j'}. \<pi>' j \<noteq> ipd (\<pi>' i'))

goal (1 subgoal):
 1. i' < j'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i' < j'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
i' < j'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cs_order_le: assumes path: \<open>is_path \<pi>\<close> \<open>is_path \<pi>'\<close> and csi: \<open>cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'\<close>
and csj: \<open>cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<close> and nret: \<open>\<pi> i \<noteq> return\<close> and ilj: \<open>i \<le> j\<close>
shows \<open>i'\<le>j'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i' \<le> j'
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> i' \<le> j'
 2. \<not> ?P \<Longrightarrow> i' \<le> j'
[PROOF STEP]
assume \<open>i < j\<close>
[PROOF STATE]
proof (state)
this:
i < j

goal (2 subgoals):
 1. ?P \<Longrightarrow> i' \<le> j'
 2. \<not> ?P \<Longrightarrow> i' \<le> j'
[PROOF STEP]
with cs_order[OF assms(1,2,3,4,5)]
[PROOF STATE]
proof (chain)
picking this:
i < j \<Longrightarrow> i' < j'
i < j
[PROOF STEP]
show \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
i < j \<Longrightarrow> i' < j'
i < j

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

goal (1 subgoal):
 1. \<not> i < j \<Longrightarrow> i' \<le> j'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> i < j \<Longrightarrow> i' \<le> j'
[PROOF STEP]
assume \<open>\<not> i < j\<close>
[PROOF STATE]
proof (state)
this:
\<not> i < j

goal (1 subgoal):
 1. \<not> i < j \<Longrightarrow> i' \<le> j'
[PROOF STEP]
hence \<open>i = j\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> i < j

goal (1 subgoal):
 1. i = j
[PROOF STEP]
using ilj
[PROOF STATE]
proof (prove)
using this:
\<not> i < j
i \<le> j

goal (1 subgoal):
 1. i = j
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
i = j

goal (1 subgoal):
 1. \<not> i < j \<Longrightarrow> i' \<le> j'
[PROOF STEP]
hence csij: \<open>cs\<^bsup>\<pi>'\<^esup> i' = cs\<^bsup>\<pi>'\<^esup> j'\<close>
[PROOF STATE]
proof (prove)
using this:
i = j

goal (1 subgoal):
 1. cs\<^bsup>\<pi>'\<^esup> i' = cs\<^bsup>\<pi>'\<^esup> j'
[PROOF STEP]
using csi csj
[PROOF STATE]
proof (prove)
using this:
i = j
cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'
cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'

goal (1 subgoal):
 1. cs\<^bsup>\<pi>'\<^esup> i' = cs\<^bsup>\<pi>'\<^esup> j'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>'\<^esup> i' = cs\<^bsup>\<pi>'\<^esup> j'

goal (1 subgoal):
 1. \<not> i < j \<Longrightarrow> i' \<le> j'
[PROOF STEP]
have nret': \<open>\<pi>' i' \<noteq> return\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi>' i' \<noteq> local.return
[PROOF STEP]
using nret last_cs csi
[PROOF STATE]
proof (prove)
using this:
\<pi> i \<noteq> local.return
last (cs\<^bsup>?\<pi>\<^esup> ?i) = ?\<pi> ?i
cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'

goal (1 subgoal):
 1. \<pi>' i' \<noteq> local.return
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<pi>' i' \<noteq> local.return

goal (1 subgoal):
 1. \<not> i < j \<Longrightarrow> i' \<le> j'
[PROOF STEP]
show \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i' \<le> j'
[PROOF STEP]
using cs_inj[OF path(2) nret' csij]
[PROOF STATE]
proof (prove)
using this:
i' = j'

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma icdi_path_swap: assumes \<open>is_path \<pi>'\<close> \<open>j icd\<^bsup>\<pi>\<^esup>\<rightarrow>k\<close> \<open>\<pi> =\<^bsub>j\<^esub>  \<pi>'\<close> shows \<open>j icd\<^bsup>\<pi>'\<^esup>\<rightarrow>k\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j icd\<^bsup>\<pi>'\<^esup>\<rightarrow> k
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_path \<pi>'
j icd\<^bsup>\<pi>\<^esup>\<rightarrow> k
\<pi> =\<^bsub>j\<^esub> \<pi>'

goal (1 subgoal):
 1. j icd\<^bsup>\<pi>'\<^esup>\<rightarrow> k
[PROOF STEP]
unfolding eq_up_to_def is_icdi_def is_cdi_def
[PROOF STATE]
proof (prove)
using this:
is_path \<pi>'
is_path \<pi> \<and> (is_path \<pi> \<and> k < j \<and> \<pi> j \<noteq> local.return \<and> (\<forall>j\<in>{k..j}. \<pi> j \<noteq> ipd (\<pi> k))) \<and> (\<forall>m\<in>{k<..<j}. \<not> (is_path \<pi> \<and> m < j \<and> \<pi> j \<noteq> local.return \<and> (\<forall>j\<in>{m..j}. \<pi> j \<noteq> ipd (\<pi> m))))
\<forall>i\<le>j. \<pi> i = \<pi>' i

goal (1 subgoal):
 1. is_path \<pi>' \<and> (is_path \<pi>' \<and> k < j \<and> \<pi>' j \<noteq> local.return \<and> (\<forall>j\<in>{k..j}. \<pi>' j \<noteq> ipd (\<pi>' k))) \<and> (\<forall>m\<in>{k<..<j}. \<not> (is_path \<pi>' \<and> m < j \<and> \<pi>' j \<noteq> local.return \<and> (\<forall>j\<in>{m..j}. \<pi>' j \<noteq> ipd (\<pi>' m))))
[PROOF STEP]
by auto


[STATEMENT]
lemma icdi_path_swap_le: assumes \<open>is_path \<pi>'\<close> \<open>j icd\<^bsup>\<pi>\<^esup>\<rightarrow>k\<close> \<open>\<pi> =\<^bsub>n\<^esub>  \<pi>'\<close> \<open>j \<le> n\<close> shows \<open>j icd\<^bsup>\<pi>'\<^esup>\<rightarrow>k\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j icd\<^bsup>\<pi>'\<^esup>\<rightarrow> k
[PROOF STEP]
by (metis assms icdi_path_swap eq_up_to_le)


[STATEMENT]
lemma cs_path_swap: assumes \<open>is_path \<pi>\<close> \<open>is_path \<pi>'\<close> \<open>\<pi> =\<^bsub>k\<^esub> \<pi>'\<close> shows \<open>cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k
[PROOF STEP]
using assms(1,3)
[PROOF STATE]
proof (prove)
using this:
is_path \<pi>
\<pi> =\<^bsub>k\<^esub> \<pi>'

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k
[PROOF STEP]
proof (induction \<open>\<pi>\<close> \<open>k\<close> rule:cs_induct,cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<pi>'' n. \<lbrakk>\<lbrakk>Ex (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>The (is_icdi n \<pi>'')\<^esub> \<pi>'\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> The (is_icdi n \<pi>'') = cs\<^bsup>\<pi>'\<^esup> The (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>n\<^esub> \<pi>'; is_path \<pi>; \<pi> =\<^bsub>k\<^esub> \<pi>'; ?P3 \<pi>'' n\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n
 2. \<And>\<pi>'' n. \<lbrakk>\<lbrakk>Ex (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>The (is_icdi n \<pi>'')\<^esub> \<pi>'\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> The (is_icdi n \<pi>'') = cs\<^bsup>\<pi>'\<^esup> The (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>n\<^esub> \<pi>'; is_path \<pi>; \<pi> =\<^bsub>k\<^esub> \<pi>'; \<not> ?P3 \<pi>'' n\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n
[PROOF STEP]
case (cs \<pi> k)
[PROOF STATE]
proof (state)
this:
\<lbrakk>Ex (is_icdi k \<pi>); is_path \<pi>; \<pi> =\<^bsub>The (is_icdi k \<pi>)\<^esub> \<pi>'\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> The (is_icdi k \<pi>) = cs\<^bsup>\<pi>'\<^esup> The (is_icdi k \<pi>)
is_path \<pi>
\<pi> =\<^bsub>k\<^esub> \<pi>'

goal (2 subgoals):
 1. \<And>\<pi>'' n. \<lbrakk>\<lbrakk>Ex (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>The (is_icdi n \<pi>'')\<^esub> \<pi>'\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> The (is_icdi n \<pi>'') = cs\<^bsup>\<pi>'\<^esup> The (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>n\<^esub> \<pi>'; is_path \<pi>; \<pi> =\<^bsub>k\<^esub> \<pi>'; ?P3 \<pi>'' n\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n
 2. \<And>\<pi>'' n. \<lbrakk>\<lbrakk>Ex (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>The (is_icdi n \<pi>'')\<^esub> \<pi>'\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> The (is_icdi n \<pi>'') = cs\<^bsup>\<pi>'\<^esup> The (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>n\<^esub> \<pi>'; is_path \<pi>; \<pi> =\<^bsub>k\<^esub> \<pi>'; \<not> ?P3 \<pi>'' n\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n
[PROOF STEP]
let \<open>?l\<close> = \<open>(THE l. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l)\<close>
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<pi>'' n. \<lbrakk>\<lbrakk>Ex (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>The (is_icdi n \<pi>'')\<^esub> \<pi>'\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> The (is_icdi n \<pi>'') = cs\<^bsup>\<pi>'\<^esup> The (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>n\<^esub> \<pi>'; is_path \<pi>; \<pi> =\<^bsub>k\<^esub> \<pi>'; ?P3 \<pi>'' n\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n
 2. \<And>\<pi>'' n. \<lbrakk>\<lbrakk>Ex (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>The (is_icdi n \<pi>'')\<^esub> \<pi>'\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> The (is_icdi n \<pi>'') = cs\<^bsup>\<pi>'\<^esup> The (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>n\<^esub> \<pi>'; is_path \<pi>; \<pi> =\<^bsub>k\<^esub> \<pi>'; \<not> ?P3 \<pi>'' n\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n
[PROOF STEP]
assume *: \<open>\<exists>l. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l\<close>
[PROOF STATE]
proof (state)
this:
\<exists>l. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l

goal (2 subgoals):
 1. \<And>\<pi>'' n. \<lbrakk>\<lbrakk>Ex (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>The (is_icdi n \<pi>'')\<^esub> \<pi>'\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> The (is_icdi n \<pi>'') = cs\<^bsup>\<pi>'\<^esup> The (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>n\<^esub> \<pi>'; is_path \<pi>; \<pi> =\<^bsub>k\<^esub> \<pi>'; ?P3 \<pi>'' n\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n
 2. \<And>\<pi>'' n. \<lbrakk>\<lbrakk>Ex (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>The (is_icdi n \<pi>'')\<^esub> \<pi>'\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> The (is_icdi n \<pi>'') = cs\<^bsup>\<pi>'\<^esup> The (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>n\<^esub> \<pi>'; is_path \<pi>; \<pi> =\<^bsub>k\<^esub> \<pi>'; \<not> ?P3 \<pi>'' n\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n
[PROOF STEP]
have kicd: \<open>k icd\<^bsup>\<pi>\<^esup>\<rightarrow> ?l\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> (THE l. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l)
[PROOF STEP]
by (metis "*" icd_is_the_icd)
[PROOF STATE]
proof (state)
this:
k icd\<^bsup>\<pi>\<^esup>\<rightarrow> (THE l. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l)

goal (2 subgoals):
 1. \<And>\<pi>'' n. \<lbrakk>\<lbrakk>Ex (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>The (is_icdi n \<pi>'')\<^esub> \<pi>'\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> The (is_icdi n \<pi>'') = cs\<^bsup>\<pi>'\<^esup> The (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>n\<^esub> \<pi>'; is_path \<pi>; \<pi> =\<^bsub>k\<^esub> \<pi>'; ?P3 \<pi>'' n\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n
 2. \<And>\<pi>'' n. \<lbrakk>\<lbrakk>Ex (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>The (is_icdi n \<pi>'')\<^esub> \<pi>'\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> The (is_icdi n \<pi>'') = cs\<^bsup>\<pi>'\<^esup> The (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>n\<^esub> \<pi>'; is_path \<pi>; \<pi> =\<^bsub>k\<^esub> \<pi>'; \<not> ?P3 \<pi>'' n\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n
[PROOF STEP]
hence \<open>?l < k\<close>
[PROOF STATE]
proof (prove)
using this:
k icd\<^bsup>\<pi>\<^esup>\<rightarrow> (THE l. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l)

goal (1 subgoal):
 1. (THE l. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l) < k
[PROOF STEP]
unfolding is_cdi_def[of \<open>k\<close> \<open>\<pi>\<close> \<open>?l\<close>] is_icdi_def[of \<open>k\<close> \<open>\<pi>\<close> \<open>?l\<close>]
[PROOF STATE]
proof (prove)
using this:
is_path \<pi> \<and> (is_path \<pi> \<and> The (is_icdi k \<pi>) < k \<and> \<pi> k \<noteq> local.return \<and> (\<forall>j\<in>{The (is_icdi k \<pi>)..k}. \<pi> j \<noteq> ipd (\<pi> (The (is_icdi k \<pi>))))) \<and> (\<forall>m\<in>{The (is_icdi k \<pi>)<..<k}. \<not> k cd\<^bsup>\<pi>\<^esup>\<rightarrow> m)

goal (1 subgoal):
 1. (THE l. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l) < k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(THE l. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l) < k

goal (2 subgoals):
 1. \<And>\<pi>'' n. \<lbrakk>\<lbrakk>Ex (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>The (is_icdi n \<pi>'')\<^esub> \<pi>'\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> The (is_icdi n \<pi>'') = cs\<^bsup>\<pi>'\<^esup> The (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>n\<^esub> \<pi>'; is_path \<pi>; \<pi> =\<^bsub>k\<^esub> \<pi>'; ?P3 \<pi>'' n\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n
 2. \<And>\<pi>'' n. \<lbrakk>\<lbrakk>Ex (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>The (is_icdi n \<pi>'')\<^esub> \<pi>'\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> The (is_icdi n \<pi>'') = cs\<^bsup>\<pi>'\<^esup> The (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>n\<^esub> \<pi>'; is_path \<pi>; \<pi> =\<^bsub>k\<^esub> \<pi>'; \<not> ?P3 \<pi>'' n\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n
[PROOF STEP]
hence \<open>\<forall> i\<le>?l. \<pi> i = \<pi>' i\<close>
[PROOF STATE]
proof (prove)
using this:
(THE l. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l) < k

goal (1 subgoal):
 1. \<forall>i\<le>THE l. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l. \<pi> i = \<pi>' i
[PROOF STEP]
using cs(2,3)
[PROOF STATE]
proof (prove)
using this:
(THE l. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l) < k
is_path \<pi>
\<pi> =\<^bsub>k\<^esub> \<pi>'

goal (1 subgoal):
 1. \<forall>i\<le>THE l. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l. \<pi> i = \<pi>' i
[PROOF STEP]
unfolding eq_up_to_def
[PROOF STATE]
proof (prove)
using this:
(THE l. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l) < k
is_path \<pi>
\<forall>i\<le>k. \<pi> i = \<pi>' i

goal (1 subgoal):
 1. \<forall>i\<le>THE l. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l. \<pi> i = \<pi>' i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>i\<le>THE l. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l. \<pi> i = \<pi>' i

goal (2 subgoals):
 1. \<And>\<pi>'' n. \<lbrakk>\<lbrakk>Ex (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>The (is_icdi n \<pi>'')\<^esub> \<pi>'\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> The (is_icdi n \<pi>'') = cs\<^bsup>\<pi>'\<^esup> The (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>n\<^esub> \<pi>'; is_path \<pi>; \<pi> =\<^bsub>k\<^esub> \<pi>'; ?P3 \<pi>'' n\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n
 2. \<And>\<pi>'' n. \<lbrakk>\<lbrakk>Ex (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>The (is_icdi n \<pi>'')\<^esub> \<pi>'\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> The (is_icdi n \<pi>'') = cs\<^bsup>\<pi>'\<^esup> The (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>n\<^esub> \<pi>'; is_path \<pi>; \<pi> =\<^bsub>k\<^esub> \<pi>'; \<not> ?P3 \<pi>'' n\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n
[PROOF STEP]
hence csl: \<open>cs\<^bsup>\<pi>\<^esup> ?l = cs\<^bsup>\<pi>'\<^esup> ?l\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>i\<le>THE l. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l. \<pi> i = \<pi>' i

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> (THE l. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l) = cs\<^bsup>\<pi>'\<^esup> (THE l. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l)
[PROOF STEP]
using cs(1,2) *
[PROOF STATE]
proof (prove)
using this:
\<forall>i\<le>THE l. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l. \<pi> i = \<pi>' i
\<lbrakk>Ex (is_icdi k \<pi>); is_path \<pi>; \<pi> =\<^bsub>The (is_icdi k \<pi>)\<^esub> \<pi>'\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> The (is_icdi k \<pi>) = cs\<^bsup>\<pi>'\<^esup> The (is_icdi k \<pi>)
is_path \<pi>
\<exists>l. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> (THE l. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l) = cs\<^bsup>\<pi>'\<^esup> (THE l. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l)
[PROOF STEP]
unfolding eq_up_to_def
[PROOF STATE]
proof (prove)
using this:
\<forall>i\<le>THE l. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l. \<pi> i = \<pi>' i
\<lbrakk>Ex (is_icdi k \<pi>); is_path \<pi>; \<forall>i\<le>The (is_icdi k \<pi>). \<pi> i = \<pi>' i\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> The (is_icdi k \<pi>) = cs\<^bsup>\<pi>'\<^esup> The (is_icdi k \<pi>)
is_path \<pi>
\<exists>l. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> (THE l. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l) = cs\<^bsup>\<pi>'\<^esup> (THE l. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> (THE l. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l) = cs\<^bsup>\<pi>'\<^esup> (THE l. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l)

goal (2 subgoals):
 1. \<And>\<pi>'' n. \<lbrakk>\<lbrakk>Ex (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>The (is_icdi n \<pi>'')\<^esub> \<pi>'\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> The (is_icdi n \<pi>'') = cs\<^bsup>\<pi>'\<^esup> The (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>n\<^esub> \<pi>'; is_path \<pi>; \<pi> =\<^bsub>k\<^esub> \<pi>'; ?P3 \<pi>'' n\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n
 2. \<And>\<pi>'' n. \<lbrakk>\<lbrakk>Ex (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>The (is_icdi n \<pi>'')\<^esub> \<pi>'\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> The (is_icdi n \<pi>'') = cs\<^bsup>\<pi>'\<^esup> The (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>n\<^esub> \<pi>'; is_path \<pi>; \<pi> =\<^bsub>k\<^esub> \<pi>'; \<not> ?P3 \<pi>'' n\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n
[PROOF STEP]
have kicd: \<open>k icd\<^bsup>\<pi>\<^esup>\<rightarrow> ?l\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> (THE l. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l)
[PROOF STEP]
by (metis "*" icd_is_the_icd)
[PROOF STATE]
proof (state)
this:
k icd\<^bsup>\<pi>\<^esup>\<rightarrow> (THE l. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l)

goal (2 subgoals):
 1. \<And>\<pi>'' n. \<lbrakk>\<lbrakk>Ex (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>The (is_icdi n \<pi>'')\<^esub> \<pi>'\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> The (is_icdi n \<pi>'') = cs\<^bsup>\<pi>'\<^esup> The (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>n\<^esub> \<pi>'; is_path \<pi>; \<pi> =\<^bsub>k\<^esub> \<pi>'; ?P3 \<pi>'' n\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n
 2. \<And>\<pi>'' n. \<lbrakk>\<lbrakk>Ex (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>The (is_icdi n \<pi>'')\<^esub> \<pi>'\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> The (is_icdi n \<pi>'') = cs\<^bsup>\<pi>'\<^esup> The (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>n\<^esub> \<pi>'; is_path \<pi>; \<pi> =\<^bsub>k\<^esub> \<pi>'; \<not> ?P3 \<pi>'' n\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n
[PROOF STEP]
hence csk: \<open>cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>\<^esup> ?l @ [\<pi> k]\<close>
[PROOF STATE]
proof (prove)
using this:
k icd\<^bsup>\<pi>\<^esup>\<rightarrow> (THE l. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l)

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>\<^esup> (THE l. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l) @ [\<pi> k]
[PROOF STEP]
using kicd
[PROOF STATE]
proof (prove)
using this:
k icd\<^bsup>\<pi>\<^esup>\<rightarrow> (THE l. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l)
k icd\<^bsup>\<pi>\<^esup>\<rightarrow> (THE l. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l)

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>\<^esup> (THE l. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l) @ [\<pi> k]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>\<^esup> (THE l. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l) @ [\<pi> k]

goal (2 subgoals):
 1. \<And>\<pi>'' n. \<lbrakk>\<lbrakk>Ex (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>The (is_icdi n \<pi>'')\<^esub> \<pi>'\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> The (is_icdi n \<pi>'') = cs\<^bsup>\<pi>'\<^esup> The (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>n\<^esub> \<pi>'; is_path \<pi>; \<pi> =\<^bsub>k\<^esub> \<pi>'; ?P3 \<pi>'' n\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n
 2. \<And>\<pi>'' n. \<lbrakk>\<lbrakk>Ex (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>The (is_icdi n \<pi>'')\<^esub> \<pi>'\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> The (is_icdi n \<pi>'') = cs\<^bsup>\<pi>'\<^esup> The (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>n\<^esub> \<pi>'; is_path \<pi>; \<pi> =\<^bsub>k\<^esub> \<pi>'; \<not> ?P3 \<pi>'' n\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n
[PROOF STEP]
have kicd': \<open>k icd\<^bsup>\<pi>'\<^esup>\<rightarrow> ?l\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k icd\<^bsup>\<pi>'\<^esup>\<rightarrow> (THE l. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l)
[PROOF STEP]
using kicd icdi_path_swap[OF assms(2) _ cs(3)]
[PROOF STATE]
proof (prove)
using this:
k icd\<^bsup>\<pi>\<^esup>\<rightarrow> (THE l. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l)
k icd\<^bsup>\<pi>\<^esup>\<rightarrow> ?k \<Longrightarrow> k icd\<^bsup>\<pi>'\<^esup>\<rightarrow> ?k

goal (1 subgoal):
 1. k icd\<^bsup>\<pi>'\<^esup>\<rightarrow> (THE l. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
k icd\<^bsup>\<pi>'\<^esup>\<rightarrow> (THE l. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l)

goal (2 subgoals):
 1. \<And>\<pi>'' n. \<lbrakk>\<lbrakk>Ex (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>The (is_icdi n \<pi>'')\<^esub> \<pi>'\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> The (is_icdi n \<pi>'') = cs\<^bsup>\<pi>'\<^esup> The (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>n\<^esub> \<pi>'; is_path \<pi>; \<pi> =\<^bsub>k\<^esub> \<pi>'; ?P3 \<pi>'' n\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n
 2. \<And>\<pi>'' n. \<lbrakk>\<lbrakk>Ex (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>The (is_icdi n \<pi>'')\<^esub> \<pi>'\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> The (is_icdi n \<pi>'') = cs\<^bsup>\<pi>'\<^esup> The (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>n\<^esub> \<pi>'; is_path \<pi>; \<pi> =\<^bsub>k\<^esub> \<pi>'; \<not> ?P3 \<pi>'' n\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n
[PROOF STEP]
hence \<open>?l = (THE l. k icd\<^bsup>\<pi>'\<^esup>\<rightarrow> l)\<close>
[PROOF STATE]
proof (prove)
using this:
k icd\<^bsup>\<pi>'\<^esup>\<rightarrow> (THE l. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l)

goal (1 subgoal):
 1. (THE l. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l) = (THE l. k icd\<^bsup>\<pi>'\<^esup>\<rightarrow> l)
[PROOF STEP]
by (metis icd_is_the_icd)
[PROOF STATE]
proof (state)
this:
(THE l. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l) = (THE l. k icd\<^bsup>\<pi>'\<^esup>\<rightarrow> l)

goal (2 subgoals):
 1. \<And>\<pi>'' n. \<lbrakk>\<lbrakk>Ex (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>The (is_icdi n \<pi>'')\<^esub> \<pi>'\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> The (is_icdi n \<pi>'') = cs\<^bsup>\<pi>'\<^esup> The (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>n\<^esub> \<pi>'; is_path \<pi>; \<pi> =\<^bsub>k\<^esub> \<pi>'; ?P3 \<pi>'' n\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n
 2. \<And>\<pi>'' n. \<lbrakk>\<lbrakk>Ex (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>The (is_icdi n \<pi>'')\<^esub> \<pi>'\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> The (is_icdi n \<pi>'') = cs\<^bsup>\<pi>'\<^esup> The (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>n\<^esub> \<pi>'; is_path \<pi>; \<pi> =\<^bsub>k\<^esub> \<pi>'; \<not> ?P3 \<pi>'' n\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n
[PROOF STEP]
hence csk': \<open>cs\<^bsup>\<pi>'\<^esup> k = cs\<^bsup>\<pi>'\<^esup> ?l @ [\<pi>' k]\<close>
[PROOF STATE]
proof (prove)
using this:
(THE l. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l) = (THE l. k icd\<^bsup>\<pi>'\<^esup>\<rightarrow> l)

goal (1 subgoal):
 1. cs\<^bsup>\<pi>'\<^esup> k = cs\<^bsup>\<pi>'\<^esup> (THE l. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l) @ [\<pi>' k]
[PROOF STEP]
using kicd'
[PROOF STATE]
proof (prove)
using this:
(THE l. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l) = (THE l. k icd\<^bsup>\<pi>'\<^esup>\<rightarrow> l)
k icd\<^bsup>\<pi>'\<^esup>\<rightarrow> (THE l. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l)

goal (1 subgoal):
 1. cs\<^bsup>\<pi>'\<^esup> k = cs\<^bsup>\<pi>'\<^esup> (THE l. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l) @ [\<pi>' k]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>'\<^esup> k = cs\<^bsup>\<pi>'\<^esup> (THE l. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l) @ [\<pi>' k]

goal (2 subgoals):
 1. \<And>\<pi>'' n. \<lbrakk>\<lbrakk>Ex (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>The (is_icdi n \<pi>'')\<^esub> \<pi>'\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> The (is_icdi n \<pi>'') = cs\<^bsup>\<pi>'\<^esup> The (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>n\<^esub> \<pi>'; is_path \<pi>; \<pi> =\<^bsub>k\<^esub> \<pi>'; ?P3 \<pi>'' n\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n
 2. \<And>\<pi>'' n. \<lbrakk>\<lbrakk>Ex (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>The (is_icdi n \<pi>'')\<^esub> \<pi>'\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> The (is_icdi n \<pi>'') = cs\<^bsup>\<pi>'\<^esup> The (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>n\<^esub> \<pi>'; is_path \<pi>; \<pi> =\<^bsub>k\<^esub> \<pi>'; \<not> ?P3 \<pi>'' n\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n
[PROOF STEP]
have \<open>\<pi>' k = \<pi> k\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi>' k = \<pi> k
[PROOF STEP]
using cs(3)
[PROOF STATE]
proof (prove)
using this:
\<pi> =\<^bsub>k\<^esub> \<pi>'

goal (1 subgoal):
 1. \<pi>' k = \<pi> k
[PROOF STEP]
unfolding eq_up_to_def
[PROOF STATE]
proof (prove)
using this:
\<forall>i\<le>k. \<pi> i = \<pi>' i

goal (1 subgoal):
 1. \<pi>' k = \<pi> k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<pi>' k = \<pi> k

goal (2 subgoals):
 1. \<And>\<pi>'' n. \<lbrakk>\<lbrakk>Ex (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>The (is_icdi n \<pi>'')\<^esub> \<pi>'\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> The (is_icdi n \<pi>'') = cs\<^bsup>\<pi>'\<^esup> The (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>n\<^esub> \<pi>'; is_path \<pi>; \<pi> =\<^bsub>k\<^esub> \<pi>'; ?P3 \<pi>'' n\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n
 2. \<And>\<pi>'' n. \<lbrakk>\<lbrakk>Ex (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>The (is_icdi n \<pi>'')\<^esub> \<pi>'\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> The (is_icdi n \<pi>'') = cs\<^bsup>\<pi>'\<^esup> The (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>n\<^esub> \<pi>'; is_path \<pi>; \<pi> =\<^bsub>k\<^esub> \<pi>'; \<not> ?P3 \<pi>'' n\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n
[PROOF STEP]
with csl csk csk'
[PROOF STATE]
proof (chain)
picking this:
cs\<^bsup>\<pi>\<^esup> (THE l. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l) = cs\<^bsup>\<pi>'\<^esup> (THE l. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l)
cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>\<^esup> (THE l. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l) @ [\<pi> k]
cs\<^bsup>\<pi>'\<^esup> k = cs\<^bsup>\<pi>'\<^esup> (THE l. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l) @ [\<pi>' k]
\<pi>' k = \<pi> k
[PROOF STEP]
show \<open>?case\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> (THE l. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l) = cs\<^bsup>\<pi>'\<^esup> (THE l. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l)
cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>\<^esup> (THE l. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l) @ [\<pi> k]
cs\<^bsup>\<pi>'\<^esup> k = cs\<^bsup>\<pi>'\<^esup> (THE l. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l) @ [\<pi>' k]
\<pi>' k = \<pi> k

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k

goal (1 subgoal):
 1. \<And>\<pi>'' n. \<lbrakk>\<lbrakk>Ex (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>The (is_icdi n \<pi>'')\<^esub> \<pi>'\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> The (is_icdi n \<pi>'') = cs\<^bsup>\<pi>'\<^esup> The (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>n\<^esub> \<pi>'; is_path \<pi>; \<pi> =\<^bsub>k\<^esub> \<pi>'; \<nexists>l. n icd\<^bsup>\<pi>''\<^esup>\<rightarrow> l\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<pi>'' n. \<lbrakk>\<lbrakk>Ex (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>The (is_icdi n \<pi>'')\<^esub> \<pi>'\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> The (is_icdi n \<pi>'') = cs\<^bsup>\<pi>'\<^esup> The (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>n\<^esub> \<pi>'; is_path \<pi>; \<pi> =\<^bsub>k\<^esub> \<pi>'; \<nexists>l. n icd\<^bsup>\<pi>''\<^esup>\<rightarrow> l\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n
[PROOF STEP]
case (cs \<pi> k)
[PROOF STATE]
proof (state)
this:
\<lbrakk>Ex (is_icdi k \<pi>); is_path \<pi>; \<pi> =\<^bsub>The (is_icdi k \<pi>)\<^esub> \<pi>'\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> The (is_icdi k \<pi>) = cs\<^bsup>\<pi>'\<^esup> The (is_icdi k \<pi>)
is_path \<pi>
\<pi> =\<^bsub>k\<^esub> \<pi>'

goal (1 subgoal):
 1. \<And>\<pi>'' n. \<lbrakk>\<lbrakk>Ex (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>The (is_icdi n \<pi>'')\<^esub> \<pi>'\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> The (is_icdi n \<pi>'') = cs\<^bsup>\<pi>'\<^esup> The (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>n\<^esub> \<pi>'; is_path \<pi>; \<pi> =\<^bsub>k\<^esub> \<pi>'; \<nexists>l. n icd\<^bsup>\<pi>''\<^esup>\<rightarrow> l\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n
[PROOF STEP]
assume *: \<open>\<not> (\<exists>l. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l)\<close>
[PROOF STATE]
proof (state)
this:
\<nexists>l. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l

goal (1 subgoal):
 1. \<And>\<pi>'' n. \<lbrakk>\<lbrakk>Ex (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>The (is_icdi n \<pi>'')\<^esub> \<pi>'\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> The (is_icdi n \<pi>'') = cs\<^bsup>\<pi>'\<^esup> The (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>n\<^esub> \<pi>'; is_path \<pi>; \<pi> =\<^bsub>k\<^esub> \<pi>'; \<nexists>l. n icd\<^bsup>\<pi>''\<^esup>\<rightarrow> l\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n
[PROOF STEP]
hence csk: \<open>cs\<^bsup>\<pi>\<^esup> k = [\<pi> k]\<close>
[PROOF STATE]
proof (prove)
using this:
\<nexists>l. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> k = [\<pi> k]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> k = [\<pi> k]

goal (1 subgoal):
 1. \<And>\<pi>'' n. \<lbrakk>\<lbrakk>Ex (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>The (is_icdi n \<pi>'')\<^esub> \<pi>'\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> The (is_icdi n \<pi>'') = cs\<^bsup>\<pi>'\<^esup> The (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>n\<^esub> \<pi>'; is_path \<pi>; \<pi> =\<^bsub>k\<^esub> \<pi>'; \<nexists>l. n icd\<^bsup>\<pi>''\<^esup>\<rightarrow> l\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n
[PROOF STEP]
have \<open>\<not> (\<exists>l. k icd\<^bsup>\<pi>'\<^esup>\<rightarrow> l)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nexists>l. k icd\<^bsup>\<pi>'\<^esup>\<rightarrow> l
[PROOF STEP]
apply (rule ccontr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> (\<nexists>l. k icd\<^bsup>\<pi>'\<^esup>\<rightarrow> l) \<Longrightarrow> False
[PROOF STEP]
using * icdi_path_swap_le[OF cs(2) _, of \<open>k\<close> \<open>\<pi>'\<close>] cs(3)
[PROOF STATE]
proof (prove)
using this:
\<nexists>l. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> l
\<lbrakk>k icd\<^bsup>\<pi>'\<^esup>\<rightarrow> ?k; \<pi>' =\<^bsub>?n\<^esub> \<pi>; k \<le> ?n\<rbrakk> \<Longrightarrow> k icd\<^bsup>\<pi>\<^esup>\<rightarrow> ?k
\<pi> =\<^bsub>k\<^esub> \<pi>'

goal (1 subgoal):
 1. \<not> (\<nexists>l. k icd\<^bsup>\<pi>'\<^esup>\<rightarrow> l) \<Longrightarrow> False
[PROOF STEP]
by (metis eq_up_to_sym le_refl)
[PROOF STATE]
proof (state)
this:
\<nexists>l. k icd\<^bsup>\<pi>'\<^esup>\<rightarrow> l

goal (1 subgoal):
 1. \<And>\<pi>'' n. \<lbrakk>\<lbrakk>Ex (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>The (is_icdi n \<pi>'')\<^esub> \<pi>'\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> The (is_icdi n \<pi>'') = cs\<^bsup>\<pi>'\<^esup> The (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>n\<^esub> \<pi>'; is_path \<pi>; \<pi> =\<^bsub>k\<^esub> \<pi>'; \<nexists>l. n icd\<^bsup>\<pi>''\<^esup>\<rightarrow> l\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n
[PROOF STEP]
hence csk': \<open>cs\<^bsup>\<pi>'\<^esup> k = [\<pi>' k]\<close>
[PROOF STATE]
proof (prove)
using this:
\<nexists>l. k icd\<^bsup>\<pi>'\<^esup>\<rightarrow> l

goal (1 subgoal):
 1. cs\<^bsup>\<pi>'\<^esup> k = [\<pi>' k]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>'\<^esup> k = [\<pi>' k]

goal (1 subgoal):
 1. \<And>\<pi>'' n. \<lbrakk>\<lbrakk>Ex (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>The (is_icdi n \<pi>'')\<^esub> \<pi>'\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> The (is_icdi n \<pi>'') = cs\<^bsup>\<pi>'\<^esup> The (is_icdi n \<pi>''); is_path \<pi>''; \<pi>'' =\<^bsub>n\<^esub> \<pi>'; is_path \<pi>; \<pi> =\<^bsub>k\<^esub> \<pi>'; \<nexists>l. n icd\<^bsup>\<pi>''\<^esup>\<rightarrow> l\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>''\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n
[PROOF STEP]
with csk
[PROOF STATE]
proof (chain)
picking this:
cs\<^bsup>\<pi>\<^esup> k = [\<pi> k]
cs\<^bsup>\<pi>'\<^esup> k = [\<pi>' k]
[PROOF STEP]
show \<open>?case\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> k = [\<pi> k]
cs\<^bsup>\<pi>'\<^esup> k = [\<pi>' k]

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k
[PROOF STEP]
using cs(3) eq_up_to_apply
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> k = [\<pi> k]
cs\<^bsup>\<pi>'\<^esup> k = [\<pi>' k]
\<pi> =\<^bsub>k\<^esub> \<pi>'
\<lbrakk>?\<pi> =\<^bsub>?k\<^esub> ?\<pi>'; ?j \<le> ?k\<rbrakk> \<Longrightarrow> ?\<pi> ?j = ?\<pi>' ?j

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cs_path_swap_le: assumes \<open>is_path \<pi>\<close> \<open>is_path \<pi>'\<close> \<open>\<pi> =\<^bsub>n\<^esub>  \<pi>'\<close> \<open>k \<le> n\<close> shows \<open>cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k
[PROOF STEP]
by (metis assms cs_path_swap eq_up_to_le)