[STATEMENT]
lemma cs_inj: assumes \<open>is_path \<pi>\<close> \<open>\<pi> n \<noteq> return\<close> \<open>cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>\<^esup> n'\<close> shows \<open>n = n'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n = n'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_path \<pi>
\<pi> n \<noteq> local.return
cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>\<^esup> n'

goal (1 subgoal):
 1. n = n'
[PROOF STEP]
proof (induction \<open>cs\<^bsup>\<pi>\<^esup> n\<close> arbitrary: \<open>\<pi>\<close> \<open>n\<close> \<open>n'\<close> rule:rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<pi> n n'. \<lbrakk>[] = cs\<^bsup>\<pi>\<^esup> n; is_path \<pi>; \<pi> n \<noteq> local.return; cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>\<^esup> n'\<rbrakk> \<Longrightarrow> n = n'
 2. \<And>x xs \<pi> n n'. \<lbrakk>\<And>\<pi> n n'. \<lbrakk>xs = cs\<^bsup>\<pi>\<^esup> n; is_path \<pi>; \<pi> n \<noteq> local.return; cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>\<^esup> n'\<rbrakk> \<Longrightarrow> n = n'; xs @ [x] = cs\<^bsup>\<pi>\<^esup> n; is_path \<pi>; \<pi> n \<noteq> local.return; cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>\<^esup> n'\<rbrakk> \<Longrightarrow> n = n'
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
[] = cs\<^bsup>\<pi>\<^esup> n
is_path \<pi>
\<pi> n \<noteq> local.return
cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>\<^esup> n'

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

goal (1 subgoal):
 1. False
[PROOF STEP]
using cs_not_nil
[PROOF STATE]
proof (prove)
using this:
[] = cs\<^bsup>\<pi>\<^esup> n
is_path \<pi>
\<pi> n \<noteq> local.return
cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>\<^esup> n'
cs\<^bsup>?\<pi>\<^esup> ?n \<noteq> []

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

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

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

goal (1 subgoal):
 1. \<And>x xs \<pi> n n'. \<lbrakk>\<And>\<pi> n n'. \<lbrakk>xs = cs\<^bsup>\<pi>\<^esup> n; is_path \<pi>; \<pi> n \<noteq> local.return; cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>\<^esup> n'\<rbrakk> \<Longrightarrow> n = n'; xs @ [x] = cs\<^bsup>\<pi>\<^esup> n; is_path \<pi>; \<pi> n \<noteq> local.return; cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>\<^esup> n'\<rbrakk> \<Longrightarrow> n = n'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs \<pi> n n'. \<lbrakk>\<And>\<pi> n n'. \<lbrakk>xs = cs\<^bsup>\<pi>\<^esup> n; is_path \<pi>; \<pi> n \<noteq> local.return; cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>\<^esup> n'\<rbrakk> \<Longrightarrow> n = n'; xs @ [x] = cs\<^bsup>\<pi>\<^esup> n; is_path \<pi>; \<pi> n \<noteq> local.return; cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>\<^esup> n'\<rbrakk> \<Longrightarrow> n = n'
[PROOF STEP]
case (snoc x xs \<pi> n n')
[PROOF STATE]
proof (state)
this:
\<lbrakk>xs = cs\<^bsup>?\<pi>1\<^esup> ?n1; is_path ?\<pi>1; ?\<pi>1 ?n1 \<noteq> local.return; cs\<^bsup>?\<pi>1\<^esup> ?n1 = cs\<^bsup>?\<pi>1\<^esup> ?n'1\<rbrakk> \<Longrightarrow> ?n1 = ?n'1
xs @ [x] = cs\<^bsup>\<pi>\<^esup> n
is_path \<pi>
\<pi> n \<noteq> local.return
cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>\<^esup> n'

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

goal (2 subgoals):
 1. xs = [] \<Longrightarrow> n = n'
 2. \<And>a list. xs = a # list \<Longrightarrow> n = n'
[PROOF STEP]
hence *: \<open>\<not> (\<exists> k. n icd\<^bsup>\<pi>\<^esup>\<rightarrow>k)\<close>
[PROOF STATE]
proof (prove)
using this:
xs = []

goal (1 subgoal):
 1. \<nexists>k. n icd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
using snoc(2) cs_not_nil
[PROOF STATE]
proof (prove)
using this:
xs = []
xs @ [x] = cs\<^bsup>\<pi>\<^esup> n
cs\<^bsup>?\<pi>\<^esup> ?n \<noteq> []

goal (1 subgoal):
 1. \<nexists>k. n icd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
by (auto,metis append1_eq_conv append_Nil cs_not_nil)
[PROOF STATE]
proof (state)
this:
\<nexists>k. n icd\<^bsup>\<pi>\<^esup>\<rightarrow> k

goal (2 subgoals):
 1. xs = [] \<Longrightarrow> n = n'
 2. \<And>a list. xs = a # list \<Longrightarrow> n = n'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<nexists>k. n icd\<^bsup>\<pi>\<^esup>\<rightarrow> k

goal (2 subgoals):
 1. xs = [] \<Longrightarrow> n = n'
 2. \<And>a list. xs = a # list \<Longrightarrow> n = n'
[PROOF STEP]
have \<open>[x] = cs\<^bsup>\<pi>\<^esup> n'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [x] = cs\<^bsup>\<pi>\<^esup> n'
[PROOF STEP]
using Nil snoc
[PROOF STATE]
proof (prove)
using this:
xs = []
\<lbrakk>xs = cs\<^bsup>?\<pi>1\<^esup> ?n1; is_path ?\<pi>1; ?\<pi>1 ?n1 \<noteq> local.return; cs\<^bsup>?\<pi>1\<^esup> ?n1 = cs\<^bsup>?\<pi>1\<^esup> ?n'1\<rbrakk> \<Longrightarrow> ?n1 = ?n'1
xs @ [x] = cs\<^bsup>\<pi>\<^esup> n
is_path \<pi>
\<pi> n \<noteq> local.return
cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>\<^esup> n'

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

goal (2 subgoals):
 1. xs = [] \<Longrightarrow> n = n'
 2. \<And>a list. xs = a # list \<Longrightarrow> n = n'
[PROOF STEP]
hence **: \<open>\<not> (\<exists> k. n' icd\<^bsup>\<pi>\<^esup>\<rightarrow>k)\<close>
[PROOF STATE]
proof (prove)
using this:
[x] = cs\<^bsup>\<pi>\<^esup> n'

goal (1 subgoal):
 1. \<nexists>k. n' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
using cs_not_nil
[PROOF STATE]
proof (prove)
using this:
[x] = cs\<^bsup>\<pi>\<^esup> n'
cs\<^bsup>?\<pi>\<^esup> ?n \<noteq> []

goal (1 subgoal):
 1. \<nexists>k. n' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
by (auto,metis append1_eq_conv append_Nil cs_not_nil)
[PROOF STATE]
proof (state)
this:
\<nexists>k. n' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k

goal (2 subgoals):
 1. xs = [] \<Longrightarrow> n = n'
 2. \<And>a list. xs = a # list \<Longrightarrow> n = n'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<nexists>k. n icd\<^bsup>\<pi>\<^esup>\<rightarrow> k
\<nexists>k. n' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
have \<open>\<forall> k. \<not> n cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close> \<open>\<forall> k. \<not> n' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close>
[PROOF STATE]
proof (prove)
using this:
\<nexists>k. n icd\<^bsup>\<pi>\<^esup>\<rightarrow> k
\<nexists>k. n' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k

goal (1 subgoal):
 1. \<forall>k. \<not> n cd\<^bsup>\<pi>\<^esup>\<rightarrow> k &&& \<forall>k. \<not> n' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
using excd_impl_exicd
[PROOF STATE]
proof (prove)
using this:
\<nexists>k. n icd\<^bsup>\<pi>\<^esup>\<rightarrow> k
\<nexists>k. n' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k
\<exists>k. ?i cd\<^bsup>?\<pi>\<^esup>\<rightarrow> k \<Longrightarrow> \<exists>k. ?i icd\<^bsup>?\<pi>\<^esup>\<rightarrow> k

goal (1 subgoal):
 1. \<forall>k. \<not> n cd\<^bsup>\<pi>\<^esup>\<rightarrow> k &&& \<forall>k. \<not> n' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
by auto blast+
[PROOF STATE]
proof (state)
this:
\<forall>k. \<not> n cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
\<forall>k. \<not> n' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k

goal (2 subgoals):
 1. xs = [] \<Longrightarrow> n = n'
 2. \<And>a list. xs = a # list \<Longrightarrow> n = n'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>k. \<not> n cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
\<forall>k. \<not> n' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k

goal (2 subgoals):
 1. xs = [] \<Longrightarrow> n = n'
 2. \<And>a list. xs = a # list \<Longrightarrow> n = n'
[PROOF STEP]
hence  \<open>\<pi> n = \<pi> n'\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>k. \<not> n cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
\<forall>k. \<not> n' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k

goal (1 subgoal):
 1. \<pi> n = \<pi> n'
[PROOF STEP]
using snoc(5,2)
[PROOF STATE]
proof (prove)
using this:
\<forall>k. \<not> n cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
\<forall>k. \<not> n' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>\<^esup> n'
xs @ [x] = cs\<^bsup>\<pi>\<^esup> n

goal (1 subgoal):
 1. \<pi> n = \<pi> n'
[PROOF STEP]
by auto (metis * ** list.inject)
[PROOF STATE]
proof (state)
this:
\<pi> n = \<pi> n'

goal (2 subgoals):
 1. xs = [] \<Longrightarrow> n = n'
 2. \<And>a list. xs = a # list \<Longrightarrow> n = n'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>k. \<not> n cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
\<forall>k. \<not> n' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
\<pi> n = \<pi> n'
[PROOF STEP]
show \<open>n = n'\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>k. \<not> n cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
\<forall>k. \<not> n' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
\<pi> n = \<pi> n'

goal (1 subgoal):
 1. n = n'
[PROOF STEP]
using other_claim' snoc
[PROOF STATE]
proof (prove)
using this:
\<forall>k. \<not> n cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
\<forall>k. \<not> n' cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
\<pi> n = \<pi> n'
\<lbrakk>is_path ?\<pi>; ?\<pi> ?i = ?\<pi> ?j; ?\<pi> ?i \<noteq> local.return; \<forall>k. \<not> ?i cd\<^bsup>?\<pi>\<^esup>\<rightarrow> k; \<forall>k. \<not> ?j cd\<^bsup>?\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> ?i = ?j
\<lbrakk>xs = cs\<^bsup>?\<pi>1\<^esup> ?n1; is_path ?\<pi>1; ?\<pi>1 ?n1 \<noteq> local.return; cs\<^bsup>?\<pi>1\<^esup> ?n1 = cs\<^bsup>?\<pi>1\<^esup> ?n'1\<rbrakk> \<Longrightarrow> ?n1 = ?n'1
xs @ [x] = cs\<^bsup>\<pi>\<^esup> n
is_path \<pi>
\<pi> n \<noteq> local.return
cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>\<^esup> n'

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

goal (1 subgoal):
 1. \<And>a list. xs = a # list \<Longrightarrow> n = n'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. xs = a # list \<Longrightarrow> n = n'
[PROOF STEP]
case (Cons y ys)
[PROOF STATE]
proof (state)
this:
xs = y # ys

goal (1 subgoal):
 1. \<And>a list. xs = a # list \<Longrightarrow> n = n'
[PROOF STEP]
hence *: \<open>\<exists> k. n icd\<^bsup>\<pi>\<^esup>\<rightarrow>k\<close>
[PROOF STATE]
proof (prove)
using this:
xs = y # ys

goal (1 subgoal):
 1. \<exists>k. n icd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
using snoc(2)
[PROOF STATE]
proof (prove)
using this:
xs = y # ys
xs @ [x] = cs\<^bsup>\<pi>\<^esup> n

goal (1 subgoal):
 1. \<exists>k. n icd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
by auto (metis append_is_Nil_conv list.distinct(1) list.inject)
[PROOF STATE]
proof (state)
this:
\<exists>k. n icd\<^bsup>\<pi>\<^esup>\<rightarrow> k

goal (1 subgoal):
 1. \<And>a list. xs = a # list \<Longrightarrow> n = n'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>k. n icd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
obtain k where k: \<open>n icd\<^bsup>\<pi>\<^esup>\<rightarrow>k\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>k. n icd\<^bsup>\<pi>\<^esup>\<rightarrow> k

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

goal (1 subgoal):
 1. \<And>a list. xs = a # list \<Longrightarrow> n = n'
[PROOF STEP]
have \<open>k = (THE k . n icd\<^bsup>\<pi>\<^esup>\<rightarrow> k)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k = (THE k. n icd\<^bsup>\<pi>\<^esup>\<rightarrow> k)
[PROOF STEP]
using k
[PROOF STATE]
proof (prove)
using this:
n icd\<^bsup>\<pi>\<^esup>\<rightarrow> k

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

goal (1 subgoal):
 1. \<And>a list. xs = a # list \<Longrightarrow> n = n'
[PROOF STEP]
hence xsk: \<open>xs = cs\<^bsup>\<pi>\<^esup> k\<close>
[PROOF STATE]
proof (prove)
using this:
k = (THE k. n icd\<^bsup>\<pi>\<^esup>\<rightarrow> k)

goal (1 subgoal):
 1. xs = cs\<^bsup>\<pi>\<^esup> k
[PROOF STEP]
using * k snoc(2)
[PROOF STATE]
proof (prove)
using this:
k = (THE k. n icd\<^bsup>\<pi>\<^esup>\<rightarrow> k)
\<exists>k. n icd\<^bsup>\<pi>\<^esup>\<rightarrow> k
n icd\<^bsup>\<pi>\<^esup>\<rightarrow> k
xs @ [x] = cs\<^bsup>\<pi>\<^esup> n

goal (1 subgoal):
 1. xs = cs\<^bsup>\<pi>\<^esup> k
[PROOF STEP]
unfolding cs.simps[of \<open>\<pi>\<close> \<open>n\<close>]
[PROOF STATE]
proof (prove)
using this:
k = (THE k. n icd\<^bsup>\<pi>\<^esup>\<rightarrow> k)
\<exists>k. n icd\<^bsup>\<pi>\<^esup>\<rightarrow> k
n icd\<^bsup>\<pi>\<^esup>\<rightarrow> k
xs @ [x] = (if Ex (is_icdi n \<pi>) then cs\<^bsup>\<pi>\<^esup> The (is_icdi n \<pi>) @ [\<pi> n] else [\<pi> n])

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

goal (1 subgoal):
 1. \<And>a list. xs = a # list \<Longrightarrow> n = n'
[PROOF STEP]
have **: \<open>\<exists> k. n' icd\<^bsup>\<pi>\<^esup>\<rightarrow>k\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k. n' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
using snoc(2)[unfolded snoc(5)]
[PROOF STATE]
proof (prove)
using this:
xs @ [x] = cs\<^bsup>\<pi>\<^esup> n'

goal (1 subgoal):
 1. \<exists>k. n' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
by auto (metis Cons append1_eq_conv append_Nil list.distinct(1))
[PROOF STATE]
proof (state)
this:
\<exists>k. n' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k

goal (1 subgoal):
 1. \<And>a list. xs = a # list \<Longrightarrow> n = n'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>k. n' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
obtain k' where k': \<open>n' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>k. n' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k

goal (1 subgoal):
 1. (\<And>k'. n' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'

goal (1 subgoal):
 1. \<And>a list. xs = a # list \<Longrightarrow> n = n'
[PROOF STEP]
hence \<open>k' = (THE k . n' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k)\<close>
[PROOF STATE]
proof (prove)
using this:
n' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'

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

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

goal (1 subgoal):
 1. \<And>a list. xs = a # list \<Longrightarrow> n = n'
[PROOF STEP]
hence xsk': \<open>xs = cs\<^bsup>\<pi>\<^esup> k'\<close>
[PROOF STATE]
proof (prove)
using this:
k' = (THE k. n' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k)

goal (1 subgoal):
 1. xs = cs\<^bsup>\<pi>\<^esup> k'
[PROOF STEP]
using ** k' snoc(5,2)
[PROOF STATE]
proof (prove)
using this:
k' = (THE k. n' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k)
\<exists>k. n' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k
n' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'
cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>\<^esup> n'
xs @ [x] = cs\<^bsup>\<pi>\<^esup> n

goal (1 subgoal):
 1. xs = cs\<^bsup>\<pi>\<^esup> k'
[PROOF STEP]
unfolding cs.simps[of \<open>\<pi>\<close> \<open>n'\<close>]
[PROOF STATE]
proof (prove)
using this:
k' = (THE k. n' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k)
\<exists>k. n' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k
n' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'
cs\<^bsup>\<pi>\<^esup> n = (if Ex (is_icdi n' \<pi>) then cs\<^bsup>\<pi>\<^esup> The (is_icdi n' \<pi>) @ [\<pi> n'] else [\<pi> n'])
xs @ [x] = cs\<^bsup>\<pi>\<^esup> n

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

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

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>\<^esup> k'
[PROOF STEP]
using xsk
[PROOF STATE]
proof (prove)
using this:
xs = cs\<^bsup>\<pi>\<^esup> k'
xs = cs\<^bsup>\<pi>\<^esup> k

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

goal (1 subgoal):
 1. \<And>a list. xs = a # list \<Longrightarrow> n = n'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>\<^esup> k'

goal (1 subgoal):
 1. \<And>a list. xs = a # list \<Longrightarrow> n = n'
[PROOF STEP]
have kn: \<open>k < n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k < n
[PROOF STEP]
using k
[PROOF STATE]
proof (prove)
using this:
n icd\<^bsup>\<pi>\<^esup>\<rightarrow> k

goal (1 subgoal):
 1. k < n
[PROOF STEP]
by (metis is_icdi_def is_cdi_def)
[PROOF STATE]
proof (state)
this:
k < n

goal (1 subgoal):
 1. \<And>a list. xs = a # list \<Longrightarrow> n = n'
[PROOF STEP]
hence \<open>\<pi> k \<noteq> return\<close>
[PROOF STATE]
proof (prove)
using this:
k < n

goal (1 subgoal):
 1. \<pi> k \<noteq> local.return
[PROOF STEP]
using snoc
[PROOF STATE]
proof (prove)
using this:
k < n
\<lbrakk>xs = cs\<^bsup>?\<pi>1\<^esup> ?n1; is_path ?\<pi>1; ?\<pi>1 ?n1 \<noteq> local.return; cs\<^bsup>?\<pi>1\<^esup> ?n1 = cs\<^bsup>?\<pi>1\<^esup> ?n'1\<rbrakk> \<Longrightarrow> ?n1 = ?n'1
xs @ [x] = cs\<^bsup>\<pi>\<^esup> n
is_path \<pi>
\<pi> n \<noteq> local.return
cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>\<^esup> n'

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

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

goal (1 subgoal):
 1. k' = k
[PROOF STEP]
using snoc(1) xsk snoc(3)
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>\<^esup> k'
\<pi> k \<noteq> local.return
\<lbrakk>xs = cs\<^bsup>?\<pi>1\<^esup> ?n1; is_path ?\<pi>1; ?\<pi>1 ?n1 \<noteq> local.return; cs\<^bsup>?\<pi>1\<^esup> ?n1 = cs\<^bsup>?\<pi>1\<^esup> ?n'1\<rbrakk> \<Longrightarrow> ?n1 = ?n'1
xs = cs\<^bsup>\<pi>\<^esup> k
is_path \<pi>

goal (1 subgoal):
 1. k' = k
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
k' = k

goal (1 subgoal):
 1. \<And>a list. xs = a # list \<Longrightarrow> n = n'
[PROOF STEP]
have nk0: \<open>n - k icd\<^bsup>\<pi>\<guillemotleft>k\<^esup>\<rightarrow> 0\<close> \<open>n' - k icd\<^bsup>\<pi>\<guillemotleft>k\<^esup>\<rightarrow> 0\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n - k icd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> 0 &&& n' - k icd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> 0
[PROOF STEP]
using k k' icd_path_shift0 snoc(3)
[PROOF STATE]
proof (prove)
using this:
n icd\<^bsup>\<pi>\<^esup>\<rightarrow> k
n' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'
is_path ?\<pi> \<Longrightarrow> (?i icd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?k) = (?i - ?k icd\<^bsup>?\<pi> \<guillemotleft> ?k\<^esup>\<rightarrow> 0)
is_path \<pi>

goal (1 subgoal):
 1. n - k icd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> 0 &&& n' - k icd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n - k icd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> 0
n' - k icd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> 0

goal (1 subgoal):
 1. \<And>a list. xs = a # list \<Longrightarrow> n = n'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
n - k icd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> 0
n' - k icd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> 0

goal (1 subgoal):
 1. \<And>a list. xs = a # list \<Longrightarrow> n = n'
[PROOF STEP]
have nkr: \<open>(\<pi>\<guillemotleft>k)(n-k) \<noteq> return\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<pi> \<guillemotleft> k) (n - k) \<noteq> local.return
[PROOF STEP]
using snoc(4) kn
[PROOF STATE]
proof (prove)
using this:
\<pi> n \<noteq> local.return
k < n

goal (1 subgoal):
 1. (\<pi> \<guillemotleft> k) (n - k) \<noteq> local.return
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<pi> \<guillemotleft> k) (n - k) \<noteq> local.return

goal (1 subgoal):
 1. \<And>a list. xs = a # list \<Longrightarrow> n = n'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<pi> \<guillemotleft> k) (n - k) \<noteq> local.return

goal (1 subgoal):
 1. \<And>a list. xs = a # list \<Longrightarrow> n = n'
[PROOF STEP]
have \<open>is_path (\<pi>\<guillemotleft>k)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_path (\<pi> \<guillemotleft> k)
[PROOF STEP]
by (metis path_path_shift snoc.prems(1))
[PROOF STATE]
proof (state)
this:
is_path (\<pi> \<guillemotleft> k)

goal (1 subgoal):
 1. \<And>a list. xs = a # list \<Longrightarrow> n = n'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
is_path (\<pi> \<guillemotleft> k)

goal (1 subgoal):
 1. \<And>a list. xs = a # list \<Longrightarrow> n = n'
[PROOF STEP]
have kn': \<open>k < n'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k < n'
[PROOF STEP]
using k' kk'
[PROOF STATE]
proof (prove)
using this:
n' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k'
k' = k

goal (1 subgoal):
 1. k < n'
[PROOF STEP]
by (metis is_icdi_def is_cdi_def)
[PROOF STATE]
proof (state)
this:
k < n'

goal (1 subgoal):
 1. \<And>a list. xs = a # list \<Longrightarrow> n = n'
[PROOF STEP]
have \<open>\<pi> n = \<pi> n'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> n = \<pi> n'
[PROOF STEP]
using snoc(5) * **
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>\<^esup> n'
\<exists>k. n icd\<^bsup>\<pi>\<^esup>\<rightarrow> k
\<exists>k. n' icd\<^bsup>\<pi>\<^esup>\<rightarrow> k

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

goal (1 subgoal):
 1. \<And>a list. xs = a # list \<Longrightarrow> n = n'
[PROOF STEP]
hence \<open>(\<pi>\<guillemotleft>k)(n-k) = (\<pi>\<guillemotleft>k)(n'-k)\<close>
[PROOF STATE]
proof (prove)
using this:
\<pi> n = \<pi> n'

goal (1 subgoal):
 1. (\<pi> \<guillemotleft> k) (n - k) = (\<pi> \<guillemotleft> k) (n' - k)
[PROOF STEP]
using kn kn'
[PROOF STATE]
proof (prove)
using this:
\<pi> n = \<pi> n'
k < n
k < n'

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

goal (1 subgoal):
 1. \<And>a list. xs = a # list \<Longrightarrow> n = n'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
n - k icd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> 0
n' - k icd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> 0
(\<pi> \<guillemotleft> k) (n - k) \<noteq> local.return
is_path (\<pi> \<guillemotleft> k)
(\<pi> \<guillemotleft> k) (n - k) = (\<pi> \<guillemotleft> k) (n' - k)
[PROOF STEP]
have \<open>n - k = n' - k\<close>
[PROOF STATE]
proof (prove)
using this:
n - k icd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> 0
n' - k icd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> 0
(\<pi> \<guillemotleft> k) (n - k) \<noteq> local.return
is_path (\<pi> \<guillemotleft> k)
(\<pi> \<guillemotleft> k) (n - k) = (\<pi> \<guillemotleft> k) (n' - k)

goal (1 subgoal):
 1. n - k = n' - k
[PROOF STEP]
using other_claim
[PROOF STATE]
proof (prove)
using this:
n - k icd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> 0
n' - k icd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> 0
(\<pi> \<guillemotleft> k) (n - k) \<noteq> local.return
is_path (\<pi> \<guillemotleft> k)
(\<pi> \<guillemotleft> k) (n - k) = (\<pi> \<guillemotleft> k) (n' - k)
\<lbrakk>is_path ?\<pi>; ?\<pi> ?i = ?\<pi> ?j; ?\<pi> ?i \<noteq> local.return; ?i icd\<^bsup>?\<pi>\<^esup>\<rightarrow> 0; ?j icd\<^bsup>?\<pi>\<^esup>\<rightarrow> 0\<rbrakk> \<Longrightarrow> ?i = ?j

goal (1 subgoal):
 1. n - k = n' - k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n - k = n' - k

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

goal (1 subgoal):
 1. n = n'
[PROOF STEP]
using kn kn'
[PROOF STATE]
proof (prove)
using this:
n - k = n' - k
k < n
k < n'

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
n = n'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cs_cases: fixes \<pi> i
obtains (base) \<open>cs\<^bsup>\<pi>\<^esup> i = [\<pi> i]\<close> and \<open>\<forall> k. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close> |
(depend) k where  \<open>cs\<^bsup>\<pi>\<^esup> i = (cs\<^bsup>\<pi>\<^esup> k)@[\<pi> i]\<close> and \<open>i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>cs\<^bsup>\<pi>\<^esup> i = [\<pi> i]; \<forall>k. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> thesis; \<And>k. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> k @ [\<pi> i]; i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>cs\<^bsup>\<pi>\<^esup> i = [\<pi> i]; \<forall>k. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> thesis; \<And>k. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> k @ [\<pi> i]; i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> thesis; ?P4\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<lbrakk>cs\<^bsup>\<pi>\<^esup> i = [\<pi> i]; \<forall>k. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> thesis; \<And>k. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> k @ [\<pi> i]; i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> thesis; \<not> ?P4\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
assume *: \<open>\<exists> k. i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close>
[PROOF STATE]
proof (state)
this:
\<exists>k. i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k

goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>cs\<^bsup>\<pi>\<^esup> i = [\<pi> i]; \<forall>k. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> thesis; \<And>k. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> k @ [\<pi> i]; i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> thesis; ?P4\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<lbrakk>cs\<^bsup>\<pi>\<^esup> i = [\<pi> i]; \<forall>k. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> thesis; \<And>k. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> k @ [\<pi> i]; i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> thesis; \<not> ?P4\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>k. i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
obtain k where k: \<open>i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>k. i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k

goal (1 subgoal):
 1. (\<And>k. i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k

goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>cs\<^bsup>\<pi>\<^esup> i = [\<pi> i]; \<forall>k. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> thesis; \<And>k. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> k @ [\<pi> i]; i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> thesis; ?P4\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<lbrakk>cs\<^bsup>\<pi>\<^esup> i = [\<pi> i]; \<forall>k. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> thesis; \<And>k. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> k @ [\<pi> i]; i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> thesis; \<not> ?P4\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
hence \<open>k = (THE k. i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k)\<close>
[PROOF STATE]
proof (prove)
using this:
i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k

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

goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>cs\<^bsup>\<pi>\<^esup> i = [\<pi> i]; \<forall>k. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> thesis; \<And>k. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> k @ [\<pi> i]; i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> thesis; ?P4\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<lbrakk>cs\<^bsup>\<pi>\<^esup> i = [\<pi> i]; \<forall>k. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> thesis; \<And>k. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> k @ [\<pi> i]; i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> thesis; \<not> ?P4\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
hence \<open>cs\<^bsup>\<pi>\<^esup> i = (cs\<^bsup>\<pi>\<^esup> k)@[\<pi> i]\<close>
[PROOF STATE]
proof (prove)
using this:
k = (THE k. i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k)

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

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

goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>cs\<^bsup>\<pi>\<^esup> i = [\<pi> i]; \<forall>k. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> thesis; \<And>k. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> k @ [\<pi> i]; i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> thesis; ?P4\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<lbrakk>cs\<^bsup>\<pi>\<^esup> i = [\<pi> i]; \<forall>k. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> thesis; \<And>k. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> k @ [\<pi> i]; i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> thesis; \<not> ?P4\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
with k that
[PROOF STATE]
proof (chain)
picking this:
i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k
\<lbrakk>cs\<^bsup>\<pi>\<^esup> i = [\<pi> i]; \<forall>k. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> thesis
\<lbrakk>cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> ?k1 @ [\<pi> i]; i icd\<^bsup>\<pi>\<^esup>\<rightarrow> ?k1\<rbrakk> \<Longrightarrow> thesis
cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> k @ [\<pi> i]
[PROOF STEP]
show \<open>thesis\<close>
[PROOF STATE]
proof (prove)
using this:
i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k
\<lbrakk>cs\<^bsup>\<pi>\<^esup> i = [\<pi> i]; \<forall>k. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> thesis
\<lbrakk>cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> ?k1 @ [\<pi> i]; i icd\<^bsup>\<pi>\<^esup>\<rightarrow> ?k1\<rbrakk> \<Longrightarrow> thesis
cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> k @ [\<pi> i]

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

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>cs\<^bsup>\<pi>\<^esup> i = [\<pi> i]; \<forall>k. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> thesis; \<And>k. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> k @ [\<pi> i]; i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> thesis; \<nexists>k. i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>cs\<^bsup>\<pi>\<^esup> i = [\<pi> i]; \<forall>k. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> thesis; \<And>k. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> k @ [\<pi> i]; i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> thesis; \<nexists>k. i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
assume *: \<open>\<not> (\<exists> k. i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k)\<close>
[PROOF STATE]
proof (state)
this:
\<nexists>k. i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k

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

goal (1 subgoal):
 1. \<forall>k. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
by (metis excd_impl_exicd)
[PROOF STATE]
proof (state)
this:
\<forall>k. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>cs\<^bsup>\<pi>\<^esup> i = [\<pi> i]; \<forall>k. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> thesis; \<And>k. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> k @ [\<pi> i]; i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> thesis; \<nexists>k. i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>k. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>cs\<^bsup>\<pi>\<^esup> i = [\<pi> i]; \<forall>k. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> thesis; \<And>k. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> k @ [\<pi> i]; i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> thesis; \<nexists>k. i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have \<open>cs\<^bsup>\<pi>\<^esup> i = [\<pi> i]\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> i = [\<pi> i]
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
\<nexists>k. i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k

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

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>cs\<^bsup>\<pi>\<^esup> i = [\<pi> i]; \<forall>k. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> thesis; \<And>k. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> k @ [\<pi> i]; i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> thesis; \<nexists>k. i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>k. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
cs\<^bsup>\<pi>\<^esup> i = [\<pi> i]
[PROOF STEP]
show \<open>thesis\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>k. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
cs\<^bsup>\<pi>\<^esup> i = [\<pi> i]

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
\<forall>k. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
cs\<^bsup>\<pi>\<^esup> i = [\<pi> i]
\<lbrakk>cs\<^bsup>\<pi>\<^esup> i = [\<pi> i]; \<forall>k. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> thesis
\<lbrakk>cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> ?k1 @ [\<pi> i]; i icd\<^bsup>\<pi>\<^esup>\<rightarrow> ?k1\<rbrakk> \<Longrightarrow> thesis

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cs_length_one: assumes \<open>length (cs\<^bsup>\<pi>\<^esup> i) = 1\<close> shows  \<open>cs\<^bsup>\<pi>\<^esup> i = [\<pi> i]\<close> and \<open>\<forall> k. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> i = [\<pi> i] &&& \<forall>k. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
apply (cases \<open>i\<close> \<open>\<pi>\<close> rule: cs_cases)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i = [\<pi> i]; \<forall>k. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> i = [\<pi> i]
 2. \<And>k. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> k @ [\<pi> i]; i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> i = [\<pi> i]
 3. \<forall>k. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
using assms cs_not_nil
[PROOF STATE]
proof (prove)
using this:
length (cs\<^bsup>\<pi>\<^esup> i) = 1
cs\<^bsup>?\<pi>\<^esup> ?n \<noteq> []

goal (3 subgoals):
 1. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i = [\<pi> i]; \<forall>k. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> i = [\<pi> i]
 2. \<And>k. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> k @ [\<pi> i]; i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> i = [\<pi> i]
 3. \<forall>k. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>length (if Ex (is_icdi i \<pi>) then cs\<^bsup>\<pi>\<^esup> The (is_icdi i \<pi>) @ [\<pi> i] else [\<pi> i]) = Suc 0; \<And>\<pi> n. (if Ex (is_icdi n \<pi>) then cs\<^bsup>\<pi>\<^esup> The (is_icdi n \<pi>) @ [\<pi> n] else [\<pi> n]) \<noteq> []; i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (cases \<open>i\<close> \<open>\<pi>\<close> rule: cs_cases)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>k. \<lbrakk>length (if Ex (is_icdi i \<pi>) then cs\<^bsup>\<pi>\<^esup> The (is_icdi i \<pi>) @ [\<pi> i] else [\<pi> i]) = Suc 0; \<And>\<pi> n. (if Ex (is_icdi n \<pi>) then cs\<^bsup>\<pi>\<^esup> The (is_icdi n \<pi>) @ [\<pi> n] else [\<pi> n]) \<noteq> []; i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; cs\<^bsup>\<pi>\<^esup> i = [\<pi> i]; \<forall>k. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> False
 2. \<And>k ka. \<lbrakk>length (if Ex (is_icdi i \<pi>) then cs\<^bsup>\<pi>\<^esup> The (is_icdi i \<pi>) @ [\<pi> i] else [\<pi> i]) = Suc 0; \<And>\<pi> n. (if Ex (is_icdi n \<pi>) then cs\<^bsup>\<pi>\<^esup> The (is_icdi n \<pi>) @ [\<pi> n] else [\<pi> n]) \<noteq> []; i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> ka @ [\<pi> i]; i icd\<^bsup>\<pi>\<^esup>\<rightarrow> ka\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
using assms cs_not_nil
[PROOF STATE]
proof (prove)
using this:
length (cs\<^bsup>\<pi>\<^esup> i) = 1
cs\<^bsup>?\<pi>\<^esup> ?n \<noteq> []

goal (2 subgoals):
 1. \<And>k. \<lbrakk>length (if Ex (is_icdi i \<pi>) then cs\<^bsup>\<pi>\<^esup> The (is_icdi i \<pi>) @ [\<pi> i] else [\<pi> i]) = Suc 0; \<And>\<pi> n. (if Ex (is_icdi n \<pi>) then cs\<^bsup>\<pi>\<^esup> The (is_icdi n \<pi>) @ [\<pi> n] else [\<pi> n]) \<noteq> []; i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; cs\<^bsup>\<pi>\<^esup> i = [\<pi> i]; \<forall>k. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> False
 2. \<And>k ka. \<lbrakk>length (if Ex (is_icdi i \<pi>) then cs\<^bsup>\<pi>\<^esup> The (is_icdi i \<pi>) @ [\<pi> i] else [\<pi> i]) = Suc 0; \<And>\<pi> n. (if Ex (is_icdi n \<pi>) then cs\<^bsup>\<pi>\<^esup> The (is_icdi n \<pi>) @ [\<pi> n] else [\<pi> n]) \<noteq> []; i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> ka @ [\<pi> i]; i icd\<^bsup>\<pi>\<^esup>\<rightarrow> ka\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by auto


[STATEMENT]
lemma cs_length_g_one: assumes \<open>length (cs\<^bsup>\<pi>\<^esup> i) \<noteq> 1\<close> obtains k where  \<open>cs\<^bsup>\<pi>\<^esup> i = (cs\<^bsup>\<pi>\<^esup> k)@[\<pi> i]\<close> and \<open>i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> k @ [\<pi> i]; i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply (cases \<open>i\<close> \<open>\<pi>\<close> rule: cs_cases)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>k. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> k @ [\<pi> i]; i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> thesis; cs\<^bsup>\<pi>\<^esup> i = [\<pi> i]; \<forall>k. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> thesis
 2. \<And>k. \<lbrakk>\<And>k. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> k @ [\<pi> i]; i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> thesis; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> k @ [\<pi> i]; i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using assms cs_not_nil
[PROOF STATE]
proof (prove)
using this:
length (cs\<^bsup>\<pi>\<^esup> i) \<noteq> 1
cs\<^bsup>?\<pi>\<^esup> ?n \<noteq> []

goal (2 subgoals):
 1. \<lbrakk>\<And>k. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> k @ [\<pi> i]; i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> thesis; cs\<^bsup>\<pi>\<^esup> i = [\<pi> i]; \<forall>k. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> thesis
 2. \<And>k. \<lbrakk>\<And>k. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> k @ [\<pi> i]; i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> thesis; cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> k @ [\<pi> i]; i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by auto


[STATEMENT]
lemma claim: assumes  path: \<open>is_path \<pi>\<close> \<open>is_path \<pi>'\<close> and  ii: \<open>cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>'\<^esup> i'\<close> and jj: \<open>cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>'\<^esup> j'\<close>
and bl: \<open>butlast (cs\<^bsup>\<pi>\<^esup> i) = butlast (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 (cases )
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> i' < j'
 2. \<not> ?P \<Longrightarrow> i' < j'
[PROOF STEP]
assume *: \<open>length (cs\<^bsup>\<pi>\<^esup> i) = 1\<close>
[PROOF STATE]
proof (state)
this:
length (cs\<^bsup>\<pi>\<^esup> i) = 1

goal (2 subgoals):
 1. ?P \<Longrightarrow> i' < j'
 2. \<not> ?P \<Longrightarrow> i' < j'
[PROOF STEP]
hence **: \<open>length (cs\<^bsup>\<pi>\<^esup> i) = 1\<close> \<open>length (cs\<^bsup>\<pi>\<^esup> j) = 1\<close> \<open>length (cs\<^bsup>\<pi>'\<^esup> i') = 1\<close> \<open>length (cs\<^bsup>\<pi>'\<^esup> j') = 1\<close>
[PROOF STATE]
proof (prove)
using this:
length (cs\<^bsup>\<pi>\<^esup> i) = 1

goal (1 subgoal):
 1. (length (cs\<^bsup>\<pi>\<^esup> i) = 1 &&& length (cs\<^bsup>\<pi>\<^esup> j) = 1) &&& length (cs\<^bsup>\<pi>'\<^esup> i') = 1 &&& length (cs\<^bsup>\<pi>'\<^esup> j') = 1
[PROOF STEP]
apply metis
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. length (cs\<^bsup>\<pi>\<^esup> j) = 1
 2. length (cs\<^bsup>\<pi>'\<^esup> i') = 1
 3. length (cs\<^bsup>\<pi>'\<^esup> j') = 1
[PROOF STEP]
apply (metis "*" bl butlast.simps(2) butlast_snoc cs_length_g_one cs_length_one(1) cs_not_nil)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. length (cs\<^bsup>\<pi>'\<^esup> i') = 1
 2. length (cs\<^bsup>\<pi>'\<^esup> j') = 1
[PROOF STEP]
apply (metis "*" ii)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (cs\<^bsup>\<pi>'\<^esup> j') = 1
[PROOF STEP]
by (metis "*" bl butlast.simps(2) butlast_snoc cs_length_g_one cs_length_one(1) cs_not_nil jj)
[PROOF STATE]
proof (state)
this:
length (cs\<^bsup>\<pi>\<^esup> i) = 1
length (cs\<^bsup>\<pi>\<^esup> j) = 1
length (cs\<^bsup>\<pi>'\<^esup> i') = 1
length (cs\<^bsup>\<pi>'\<^esup> j') = 1

goal (2 subgoals):
 1. ?P \<Longrightarrow> i' < j'
 2. \<not> ?P \<Longrightarrow> i' < j'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length (cs\<^bsup>\<pi>\<^esup> i) = 1
length (cs\<^bsup>\<pi>\<^esup> j) = 1
length (cs\<^bsup>\<pi>'\<^esup> i') = 1
length (cs\<^bsup>\<pi>'\<^esup> j') = 1
[PROOF STEP]
obtain \<open>cs\<^bsup>\<pi>\<^esup> i = [\<pi> i]\<close> \<open>cs\<^bsup>\<pi>\<^esup> j = [\<pi> j]\<close> \<open>cs\<^bsup>\<pi>'\<^esup> j' = [\<pi>' j']\<close> \<open>cs\<^bsup>\<pi>'\<^esup> i'= [\<pi>' i']\<close>
    \<open>\<forall> k. \<not> j cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close> \<open>\<forall> k. \<not> i' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k\<close> \<open>\<forall> k. \<not> j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k\<close>
[PROOF STATE]
proof (prove)
using this:
length (cs\<^bsup>\<pi>\<^esup> i) = 1
length (cs\<^bsup>\<pi>\<^esup> j) = 1
length (cs\<^bsup>\<pi>'\<^esup> i') = 1
length (cs\<^bsup>\<pi>'\<^esup> j') = 1

goal (1 subgoal):
 1. (\<lbrakk>cs\<^bsup>\<pi>\<^esup> i = [\<pi> i]; cs\<^bsup>\<pi>\<^esup> j = [\<pi> j]; cs\<^bsup>\<pi>'\<^esup> j' = [\<pi>' j']; cs\<^bsup>\<pi>'\<^esup> i' = [\<pi>' i']; \<forall>k. \<not> j cd\<^bsup>\<pi>\<^esup>\<rightarrow> k; \<forall>k. \<not> i' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k; \<forall>k. \<not> j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis cs_length_one ** )
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> i = [\<pi> i]
cs\<^bsup>\<pi>\<^esup> j = [\<pi> j]
cs\<^bsup>\<pi>'\<^esup> j' = [\<pi>' j']
cs\<^bsup>\<pi>'\<^esup> i' = [\<pi>' i']
\<forall>k. \<not> j cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
\<forall>k. \<not> i' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k
\<forall>k. \<not> j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k

goal (2 subgoals):
 1. ?P \<Longrightarrow> i' < j'
 2. \<not> ?P \<Longrightarrow> i' < j'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> i = [\<pi> i]
cs\<^bsup>\<pi>\<^esup> j = [\<pi> j]
cs\<^bsup>\<pi>'\<^esup> j' = [\<pi>' j']
cs\<^bsup>\<pi>'\<^esup> i' = [\<pi>' i']
\<forall>k. \<not> j cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
\<forall>k. \<not> i' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k
\<forall>k. \<not> j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k

goal (2 subgoals):
 1. ?P \<Longrightarrow> i' < j'
 2. \<not> ?P \<Longrightarrow> i' < j'
[PROOF STEP]
hence \<open>\<pi> i = \<pi>' i'\<close> \<open>\<pi> j = \<pi>' j'\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> i = [\<pi> i]
cs\<^bsup>\<pi>\<^esup> j = [\<pi> j]
cs\<^bsup>\<pi>'\<^esup> j' = [\<pi>' j']
cs\<^bsup>\<pi>'\<^esup> i' = [\<pi>' i']
\<forall>k. \<not> j cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
\<forall>k. \<not> i' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k
\<forall>k. \<not> j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k

goal (1 subgoal):
 1. \<pi> i = \<pi>' i' &&& \<pi> j = \<pi>' j'
[PROOF STEP]
using  assms
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> i = [\<pi> i]
cs\<^bsup>\<pi>\<^esup> j = [\<pi> j]
cs\<^bsup>\<pi>'\<^esup> j' = [\<pi>' j']
cs\<^bsup>\<pi>'\<^esup> i' = [\<pi>' i']
\<forall>k. \<not> j cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
\<forall>k. \<not> i' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k
\<forall>k. \<not> j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k
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

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> i' < j'
 2. \<not> ?P \<Longrightarrow> i' < j'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
cs\<^bsup>\<pi>\<^esup> i = [\<pi> i]
cs\<^bsup>\<pi>\<^esup> j = [\<pi> j]
cs\<^bsup>\<pi>'\<^esup> j' = [\<pi>' j']
cs\<^bsup>\<pi>'\<^esup> i' = [\<pi>' i']
\<forall>k. \<not> j cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
\<forall>k. \<not> i' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k
\<forall>k. \<not> j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k
\<pi> i = \<pi>' i'
\<pi> j = \<pi>' j'
[PROOF STEP]
show \<open>i' < j'\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> i = [\<pi> i]
cs\<^bsup>\<pi>\<^esup> j = [\<pi> j]
cs\<^bsup>\<pi>'\<^esup> j' = [\<pi>' j']
cs\<^bsup>\<pi>'\<^esup> i' = [\<pi>' i']
\<forall>k. \<not> j cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
\<forall>k. \<not> i' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k
\<forall>k. \<not> j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k
\<pi> i = \<pi>' i'
\<pi> j = \<pi>' j'

goal (1 subgoal):
 1. i' < j'
[PROOF STEP]
using nret ilj path claim''
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> i = [\<pi> i]
cs\<^bsup>\<pi>\<^esup> j = [\<pi> j]
cs\<^bsup>\<pi>'\<^esup> j' = [\<pi>' j']
cs\<^bsup>\<pi>'\<^esup> i' = [\<pi>' i']
\<forall>k. \<not> j cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
\<forall>k. \<not> i' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k
\<forall>k. \<not> j' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k
\<pi> i = \<pi>' i'
\<pi> j = \<pi>' j'
\<pi> i \<noteq> local.return
i < j
is_path \<pi>
is_path \<pi>'
\<lbrakk>is_path ?\<pi>; is_path ?\<pi>'; ?\<pi> ?i = ?\<pi>' ?i'; ?\<pi> ?j = ?\<pi>' ?j'; \<forall>k. \<not> ?j cd\<^bsup>?\<pi>\<^esup>\<rightarrow> k; \<forall>k. \<not> ?i' cd\<^bsup>?\<pi>'\<^esup>\<rightarrow> k; ?\<pi> ?i \<noteq> local.return; ?i < ?j\<rbrakk> \<Longrightarrow> ?i' < ?j'

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

goal (1 subgoal):
 1. length (cs\<^bsup>\<pi>\<^esup> i) \<noteq> 1 \<Longrightarrow> i' < j'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length (cs\<^bsup>\<pi>\<^esup> i) \<noteq> 1 \<Longrightarrow> i' < j'
[PROOF STEP]
assume *: \<open>length (cs\<^bsup>\<pi>\<^esup> i) \<noteq> 1\<close>
[PROOF STATE]
proof (state)
this:
length (cs\<^bsup>\<pi>\<^esup> i) \<noteq> 1

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

goal (1 subgoal):
 1. (length (cs\<^bsup>\<pi>\<^esup> i) \<noteq> 1 &&& length (cs\<^bsup>\<pi>\<^esup> j) \<noteq> 1) &&& length (cs\<^bsup>\<pi>'\<^esup> i') \<noteq> 1 &&& length (cs\<^bsup>\<pi>'\<^esup> j') \<noteq> 1
[PROOF STEP]
apply metis
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. length (cs\<^bsup>\<pi>\<^esup> j) \<noteq> 1
 2. length (cs\<^bsup>\<pi>'\<^esup> i') \<noteq> 1
 3. length (cs\<^bsup>\<pi>'\<^esup> j') \<noteq> 1
[PROOF STEP]
apply (metis "*" bl butlast.simps(2) butlast_snoc cs_length_g_one cs_length_one(1) cs_not_nil)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. length (cs\<^bsup>\<pi>'\<^esup> i') \<noteq> 1
 2. length (cs\<^bsup>\<pi>'\<^esup> j') \<noteq> 1
[PROOF STEP]
apply (metis "*" ii)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (cs\<^bsup>\<pi>'\<^esup> j') \<noteq> 1
[PROOF STEP]
by (metis "*" bl butlast.simps(2) butlast_snoc cs_length_g_one cs_length_one(1) cs_not_nil jj)
[PROOF STATE]
proof (state)
this:
length (cs\<^bsup>\<pi>\<^esup> i) \<noteq> 1
length (cs\<^bsup>\<pi>\<^esup> j) \<noteq> 1
length (cs\<^bsup>\<pi>'\<^esup> i') \<noteq> 1
length (cs\<^bsup>\<pi>'\<^esup> j') \<noteq> 1

goal (1 subgoal):
 1. length (cs\<^bsup>\<pi>\<^esup> i) \<noteq> 1 \<Longrightarrow> i' < j'
[PROOF STEP]
obtain k l k' l' where ***:
    \<open>cs\<^bsup>\<pi>\<^esup> i = (cs\<^bsup>\<pi>\<^esup> k)@[\<pi> i]\<close> \<open>cs\<^bsup>\<pi>\<^esup> j = (cs\<^bsup>\<pi>\<^esup> l)@[\<pi> j]\<close>  \<open>cs\<^bsup>\<pi>'\<^esup> i' = (cs\<^bsup>\<pi>'\<^esup> k')@[\<pi>' i']\<close> \<open>cs\<^bsup>\<pi>'\<^esup> j' = (cs\<^bsup>\<pi>'\<^esup> l')@[\<pi>' j']\<close> and
    icds: \<open>i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close> \<open>j icd\<^bsup>\<pi>\<^esup>\<rightarrow> l\<close> \<open>i' icd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'\<close> \<open>j' icd\<^bsup>\<pi>'\<^esup>\<rightarrow> l'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k l k' l'. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> k @ [\<pi> i]; cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>\<^esup> l @ [\<pi> j]; cs\<^bsup>\<pi>'\<^esup> i' = cs\<^bsup>\<pi>'\<^esup> k' @ [\<pi>' i']; cs\<^bsup>\<pi>'\<^esup> j' = cs\<^bsup>\<pi>'\<^esup> l' @ [\<pi>' j']; i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k; j icd\<^bsup>\<pi>\<^esup>\<rightarrow> l; i' icd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'; j' icd\<^bsup>\<pi>'\<^esup>\<rightarrow> l'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis ** cs_length_g_one)
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> k @ [\<pi> i]
cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>\<^esup> l @ [\<pi> j]
cs\<^bsup>\<pi>'\<^esup> i' = cs\<^bsup>\<pi>'\<^esup> k' @ [\<pi>' i']
cs\<^bsup>\<pi>'\<^esup> j' = cs\<^bsup>\<pi>'\<^esup> l' @ [\<pi>' j']
i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k
j icd\<^bsup>\<pi>\<^esup>\<rightarrow> l
i' icd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'
j' icd\<^bsup>\<pi>'\<^esup>\<rightarrow> l'

goal (1 subgoal):
 1. length (cs\<^bsup>\<pi>\<^esup> i) \<noteq> 1 \<Longrightarrow> i' < j'
[PROOF STEP]
hence \<open>cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>\<^esup> l\<close> \<open>cs\<^bsup>\<pi>'\<^esup> k' = cs\<^bsup>\<pi>'\<^esup> l'\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> k @ [\<pi> i]
cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>\<^esup> l @ [\<pi> j]
cs\<^bsup>\<pi>'\<^esup> i' = cs\<^bsup>\<pi>'\<^esup> k' @ [\<pi>' i']
cs\<^bsup>\<pi>'\<^esup> j' = cs\<^bsup>\<pi>'\<^esup> l' @ [\<pi>' j']
i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k
j icd\<^bsup>\<pi>\<^esup>\<rightarrow> l
i' icd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'
j' icd\<^bsup>\<pi>'\<^esup>\<rightarrow> l'

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>\<^esup> l &&& cs\<^bsup>\<pi>'\<^esup> k' = cs\<^bsup>\<pi>'\<^esup> l'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> k @ [\<pi> i]
cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>\<^esup> l @ [\<pi> j]
cs\<^bsup>\<pi>'\<^esup> i' = cs\<^bsup>\<pi>'\<^esup> k' @ [\<pi>' i']
cs\<^bsup>\<pi>'\<^esup> j' = cs\<^bsup>\<pi>'\<^esup> l' @ [\<pi>' j']
i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k
j icd\<^bsup>\<pi>\<^esup>\<rightarrow> l
i' icd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'
j' icd\<^bsup>\<pi>'\<^esup>\<rightarrow> l'
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

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

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

goal (1 subgoal):
 1. length (cs\<^bsup>\<pi>\<^esup> i) \<noteq> 1 \<Longrightarrow> i' < j'
[PROOF STEP]
have \<open>\<pi> k \<noteq> return\<close> \<open>\<pi>' k' \<noteq> return\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> k \<noteq> local.return &&& \<pi>' k' \<noteq> local.return
[PROOF STEP]
using nret
[PROOF STATE]
proof (prove)
using this:
\<pi> i \<noteq> local.return

goal (1 subgoal):
 1. \<pi> k \<noteq> local.return &&& \<pi>' k' \<noteq> local.return
[PROOF STEP]
apply (metis is_icdi_def icds(1) is_cdi_def term_path_stable less_imp_le)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi>' k' \<noteq> local.return
[PROOF STEP]
by (metis is_cdi_def is_icdi_def icds(3) term_path_stable less_imp_le)
[PROOF STATE]
proof (state)
this:
\<pi> k \<noteq> local.return
\<pi>' k' \<noteq> local.return

goal (1 subgoal):
 1. length (cs\<^bsup>\<pi>\<^esup> i) \<noteq> 1 \<Longrightarrow> i' < j'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>\<^esup> l
cs\<^bsup>\<pi>'\<^esup> k' = cs\<^bsup>\<pi>'\<^esup> l'
\<pi> k \<noteq> local.return
\<pi>' k' \<noteq> local.return
[PROOF STEP]
have lk[simp]: \<open>l = k\<close> \<open>l' = k'\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>\<^esup> l
cs\<^bsup>\<pi>'\<^esup> k' = cs\<^bsup>\<pi>'\<^esup> l'
\<pi> k \<noteq> local.return
\<pi>' k' \<noteq> local.return

goal (1 subgoal):
 1. l = k &&& l' = k'
[PROOF STEP]
using path cs_inj
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>\<^esup> l
cs\<^bsup>\<pi>'\<^esup> k' = cs\<^bsup>\<pi>'\<^esup> l'
\<pi> k \<noteq> local.return
\<pi>' k' \<noteq> local.return
is_path \<pi>
is_path \<pi>'
\<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. l = k &&& l' = k'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l = k
l' = k'

goal (1 subgoal):
 1. length (cs\<^bsup>\<pi>\<^esup> i) \<noteq> 1 \<Longrightarrow> i' < j'
[PROOF STEP]
let \<open>?\<pi>\<close> = \<open>\<pi> \<guillemotleft> k\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length (cs\<^bsup>\<pi>\<^esup> i) \<noteq> 1 \<Longrightarrow> i' < j'
[PROOF STEP]
let \<open>?\<pi>'\<close> = \<open>\<pi>'\<guillemotleft>k'\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length (cs\<^bsup>\<pi>\<^esup> i) \<noteq> 1 \<Longrightarrow> i' < j'
[PROOF STEP]
have \<open>i-k icd\<^bsup>?\<pi>\<^esup>\<rightarrow> 0\<close> \<open>j-k icd\<^bsup>?\<pi>\<^esup>\<rightarrow> 0\<close> \<open>i'-k' icd\<^bsup>?\<pi>'\<^esup>\<rightarrow> 0\<close> \<open>j'-k' icd\<^bsup>?\<pi>'\<^esup>\<rightarrow> 0\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (i - k icd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> 0 &&& j - k icd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> 0) &&& i' - k' icd\<^bsup>\<pi>' \<guillemotleft> k'\<^esup>\<rightarrow> 0 &&& j' - k' icd\<^bsup>\<pi>' \<guillemotleft> k'\<^esup>\<rightarrow> 0
[PROOF STEP]
using icd_path_shift0 path icds
[PROOF STATE]
proof (prove)
using this:
is_path ?\<pi> \<Longrightarrow> (?i icd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?k) = (?i - ?k icd\<^bsup>?\<pi> \<guillemotleft> ?k\<^esup>\<rightarrow> 0)
is_path \<pi>
is_path \<pi>'
i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k
j icd\<^bsup>\<pi>\<^esup>\<rightarrow> l
i' icd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'
j' icd\<^bsup>\<pi>'\<^esup>\<rightarrow> l'

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

goal (1 subgoal):
 1. length (cs\<^bsup>\<pi>\<^esup> i) \<noteq> 1 \<Longrightarrow> i' < j'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
i - k icd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> 0
j - k icd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> 0
i' - k' icd\<^bsup>\<pi>' \<guillemotleft> k'\<^esup>\<rightarrow> 0
j' - k' icd\<^bsup>\<pi>' \<guillemotleft> k'\<^esup>\<rightarrow> 0

goal (1 subgoal):
 1. length (cs\<^bsup>\<pi>\<^esup> i) \<noteq> 1 \<Longrightarrow> i' < j'
[PROOF STEP]
have ki: \<open>k < i\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k < i
[PROOF STEP]
using icds
[PROOF STATE]
proof (prove)
using this:
i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k
j icd\<^bsup>\<pi>\<^esup>\<rightarrow> l
i' icd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'
j' icd\<^bsup>\<pi>'\<^esup>\<rightarrow> l'

goal (1 subgoal):
 1. k < i
[PROOF STEP]
by (metis is_icdi_def is_cdi_def)
[PROOF STATE]
proof (state)
this:
k < i

goal (1 subgoal):
 1. length (cs\<^bsup>\<pi>\<^esup> i) \<noteq> 1 \<Longrightarrow> i' < j'
[PROOF STEP]
hence \<open>i-k < j-k\<close>
[PROOF STATE]
proof (prove)
using this:
k < i

goal (1 subgoal):
 1. i - k < j - k
[PROOF STEP]
by (metis diff_is_0_eq diff_less_mono ilj nat_le_linear order.strict_trans)
[PROOF STATE]
proof (state)
this:
i - k < j - k

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

goal (1 subgoal):
 1. length (cs\<^bsup>\<pi>\<^esup> i) \<noteq> 1 \<Longrightarrow> i' < j'
[PROOF STEP]
have \<pi>i: \<open>\<pi> i = \<pi>' i'\<close> \<open>\<pi> j = \<pi>' j'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> i = \<pi>' i' &&& \<pi> j = \<pi>' j'
[PROOF STEP]
using assms ***
[PROOF STATE]
proof (prove)
using this:
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
cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> k @ [\<pi> i]
cs\<^bsup>\<pi>\<^esup> j = cs\<^bsup>\<pi>\<^esup> l @ [\<pi> j]
cs\<^bsup>\<pi>'\<^esup> i' = cs\<^bsup>\<pi>'\<^esup> k' @ [\<pi>' i']
cs\<^bsup>\<pi>'\<^esup> j' = cs\<^bsup>\<pi>'\<^esup> l' @ [\<pi>' j']

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

goal (1 subgoal):
 1. length (cs\<^bsup>\<pi>\<^esup> i) \<noteq> 1 \<Longrightarrow> i' < j'
[PROOF STEP]
have \<open>k' < i'\<close> \<open>k' < j'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k' < i' &&& k' < j'
[PROOF STEP]
using icds
[PROOF STATE]
proof (prove)
using this:
i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k
j icd\<^bsup>\<pi>\<^esup>\<rightarrow> l
i' icd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'
j' icd\<^bsup>\<pi>'\<^esup>\<rightarrow> l'

goal (1 subgoal):
 1. k' < i' &&& k' < j'
[PROOF STEP]
unfolding lk
[PROOF STATE]
proof (prove)
using this:
i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k
j icd\<^bsup>\<pi>\<^esup>\<rightarrow> k
i' icd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'
j' icd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'

goal (1 subgoal):
 1. k' < i' &&& k' < j'
[PROOF STEP]
by (metis is_cdi_def is_icdi_def)+
[PROOF STATE]
proof (state)
this:
k' < i'
k' < j'

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

goal (1 subgoal):
 1. (\<pi> \<guillemotleft> k) (i - k) = (\<pi>' \<guillemotleft> k') (i' - k') &&& (\<pi> \<guillemotleft> k) (j - k) = (\<pi>' \<guillemotleft> k') (j' - k')
[PROOF STEP]
using \<pi>i ki ilj
[PROOF STATE]
proof (prove)
using this:
k' < i'
k' < j'
\<pi> i = \<pi>' i'
\<pi> j = \<pi>' j'
k < i
i < j

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

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

goal (1 subgoal):
 1. length (cs\<^bsup>\<pi>\<^esup> i) \<noteq> 1 \<Longrightarrow> i' < j'
[PROOF STEP]
have \<open>?\<pi> (i-k) \<noteq> return\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<pi> \<guillemotleft> k) (i - k) \<noteq> local.return
[PROOF STEP]
using nret ki
[PROOF STATE]
proof (prove)
using this:
\<pi> i \<noteq> local.return
k < i

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

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

goal (1 subgoal):
 1. length (cs\<^bsup>\<pi>\<^esup> i) \<noteq> 1 \<Longrightarrow> i' < j'
[PROOF STEP]
have \<open>is_path ?\<pi>\<close> \<open>is_path ?\<pi>'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_path (\<pi> \<guillemotleft> k) &&& is_path (\<pi>' \<guillemotleft> k')
[PROOF STEP]
using path path_path_shift
[PROOF STATE]
proof (prove)
using this:
is_path \<pi>
is_path \<pi>'
is_path ?\<pi> \<Longrightarrow> is_path (?\<pi> \<guillemotleft> ?m)

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

goal (1 subgoal):
 1. length (cs\<^bsup>\<pi>\<^esup> i) \<noteq> 1 \<Longrightarrow> i' < j'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
i - k icd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> 0
j - k icd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> 0
i' - k' icd\<^bsup>\<pi>' \<guillemotleft> k'\<^esup>\<rightarrow> 0
j' - k' icd\<^bsup>\<pi>' \<guillemotleft> k'\<^esup>\<rightarrow> 0
i - k < j - k
(\<pi> \<guillemotleft> k) (i - k) = (\<pi>' \<guillemotleft> k') (i' - k')
(\<pi> \<guillemotleft> k) (j - k) = (\<pi>' \<guillemotleft> k') (j' - k')
(\<pi> \<guillemotleft> k) (i - k) \<noteq> local.return
is_path (\<pi> \<guillemotleft> k)
is_path (\<pi>' \<guillemotleft> k')
[PROOF STEP]
have \<open>i'-k' < j' - k'\<close>
[PROOF STATE]
proof (prove)
using this:
i - k icd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> 0
j - k icd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> 0
i' - k' icd\<^bsup>\<pi>' \<guillemotleft> k'\<^esup>\<rightarrow> 0
j' - k' icd\<^bsup>\<pi>' \<guillemotleft> k'\<^esup>\<rightarrow> 0
i - k < j - k
(\<pi> \<guillemotleft> k) (i - k) = (\<pi>' \<guillemotleft> k') (i' - k')
(\<pi> \<guillemotleft> k) (j - k) = (\<pi>' \<guillemotleft> k') (j' - k')
(\<pi> \<guillemotleft> k) (i - k) \<noteq> local.return
is_path (\<pi> \<guillemotleft> k)
is_path (\<pi>' \<guillemotleft> k')

goal (1 subgoal):
 1. i' - k' < j' - k'
[PROOF STEP]
using claim'
[PROOF STATE]
proof (prove)
using this:
i - k icd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> 0
j - k icd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> 0
i' - k' icd\<^bsup>\<pi>' \<guillemotleft> k'\<^esup>\<rightarrow> 0
j' - k' icd\<^bsup>\<pi>' \<guillemotleft> k'\<^esup>\<rightarrow> 0
i - k < j - k
(\<pi> \<guillemotleft> k) (i - k) = (\<pi>' \<guillemotleft> k') (i' - k')
(\<pi> \<guillemotleft> k) (j - k) = (\<pi>' \<guillemotleft> k') (j' - k')
(\<pi> \<guillemotleft> k) (i - k) \<noteq> local.return
is_path (\<pi> \<guillemotleft> k)
is_path (\<pi>' \<guillemotleft> k')
\<lbrakk>is_path ?\<pi>; is_path ?\<pi>'; ?\<pi> ?i = ?\<pi>' ?i'; ?\<pi> ?j = ?\<pi>' ?j'; ?i icd\<^bsup>?\<pi>\<^esup>\<rightarrow> 0; ?j icd\<^bsup>?\<pi>\<^esup>\<rightarrow> 0; ?i' icd\<^bsup>?\<pi>'\<^esup>\<rightarrow> 0; ?j' icd\<^bsup>?\<pi>'\<^esup>\<rightarrow> 0; ?i < ?j; ?\<pi> ?i \<noteq> local.return\<rbrakk> \<Longrightarrow> ?i' < ?j'

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

goal (1 subgoal):
 1. length (cs\<^bsup>\<pi>\<^esup> i) \<noteq> 1 \<Longrightarrow> i' < j'
[PROOF STEP]
thus \<open>i' < j'\<close>
[PROOF STATE]
proof (prove)
using this:
i' - k' < j' - k'

goal (1 subgoal):
 1. i' < j'
[PROOF STEP]
by (metis diff_is_0_eq diff_less_mono less_nat_zero_code linorder_neqE_nat nat_le_linear)
[PROOF STATE]
proof (state)
this:
i' < j'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cs_split': assumes \<open>cs\<^bsup>\<pi>\<^esup> i = xs@[x,x']@ys\<close>  shows \<open>\<exists> m. cs\<^bsup>\<pi>\<^esup> m = xs@[x] \<and> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>m. cs\<^bsup>\<pi>\<^esup> m = xs @ [x] \<and> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> i = xs @ [x, x'] @ ys

goal (1 subgoal):
 1. \<exists>m. cs\<^bsup>\<pi>\<^esup> m = xs @ [x] \<and> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
[PROOF STEP]
proof (induction \<open>ys\<close> arbitrary: \<open>i\<close> rule:rev_induct )
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. cs\<^bsup>\<pi>\<^esup> i = xs @ [x, x'] @ [] \<Longrightarrow> \<exists>m. cs\<^bsup>\<pi>\<^esup> m = xs @ [x] \<and> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
 2. \<And>xa xsa i. \<lbrakk>\<And>i. cs\<^bsup>\<pi>\<^esup> i = xs @ [x, x'] @ xsa \<Longrightarrow> \<exists>m. cs\<^bsup>\<pi>\<^esup> m = xs @ [x] \<and> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m; cs\<^bsup>\<pi>\<^esup> i = xs @ [x, x'] @ xsa @ [xa]\<rbrakk> \<Longrightarrow> \<exists>m. cs\<^bsup>\<pi>\<^esup> m = xs @ [x] \<and> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
[PROOF STEP]
case (snoc y ys)
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> ?i1 = xs @ [x, x'] @ ys \<Longrightarrow> \<exists>m. cs\<^bsup>\<pi>\<^esup> m = xs @ [x] \<and> ?i1 cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
cs\<^bsup>\<pi>\<^esup> i = xs @ [x, x'] @ ys @ [y]

goal (2 subgoals):
 1. \<And>i. cs\<^bsup>\<pi>\<^esup> i = xs @ [x, x'] @ [] \<Longrightarrow> \<exists>m. cs\<^bsup>\<pi>\<^esup> m = xs @ [x] \<and> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
 2. \<And>xa xsa i. \<lbrakk>\<And>i. cs\<^bsup>\<pi>\<^esup> i = xs @ [x, x'] @ xsa \<Longrightarrow> \<exists>m. cs\<^bsup>\<pi>\<^esup> m = xs @ [x] \<and> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m; cs\<^bsup>\<pi>\<^esup> i = xs @ [x, x'] @ xsa @ [xa]\<rbrakk> \<Longrightarrow> \<exists>m. cs\<^bsup>\<pi>\<^esup> m = xs @ [x] \<and> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
[PROOF STEP]
hence \<open>length (cs\<^bsup>\<pi>\<^esup> i) \<noteq> 1\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> ?i1 = xs @ [x, x'] @ ys \<Longrightarrow> \<exists>m. cs\<^bsup>\<pi>\<^esup> m = xs @ [x] \<and> ?i1 cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
cs\<^bsup>\<pi>\<^esup> i = xs @ [x, x'] @ ys @ [y]

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

goal (2 subgoals):
 1. \<And>i. cs\<^bsup>\<pi>\<^esup> i = xs @ [x, x'] @ [] \<Longrightarrow> \<exists>m. cs\<^bsup>\<pi>\<^esup> m = xs @ [x] \<and> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
 2. \<And>xa xsa i. \<lbrakk>\<And>i. cs\<^bsup>\<pi>\<^esup> i = xs @ [x, x'] @ xsa \<Longrightarrow> \<exists>m. cs\<^bsup>\<pi>\<^esup> m = xs @ [x] \<and> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m; cs\<^bsup>\<pi>\<^esup> i = xs @ [x, x'] @ xsa @ [xa]\<rbrakk> \<Longrightarrow> \<exists>m. cs\<^bsup>\<pi>\<^esup> m = xs @ [x] \<and> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length (cs\<^bsup>\<pi>\<^esup> i) \<noteq> 1
[PROOF STEP]
obtain i' where \<open>cs\<^bsup>\<pi>\<^esup> i = (cs\<^bsup>\<pi>\<^esup> i') @ [\<pi> i]\<close> and *: \<open>i icd\<^bsup>\<pi>\<^esup>\<rightarrow> i'\<close>
[PROOF STATE]
proof (prove)
using this:
length (cs\<^bsup>\<pi>\<^esup> i) \<noteq> 1

goal (1 subgoal):
 1. (\<And>i'. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> i' @ [\<pi> i]; i icd\<^bsup>\<pi>\<^esup>\<rightarrow> i'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using cs_length_g_one[of \<open>\<pi>\<close> \<open>i\<close>]
[PROOF STATE]
proof (prove)
using this:
length (cs\<^bsup>\<pi>\<^esup> i) \<noteq> 1
\<lbrakk>length (cs\<^bsup>\<pi>\<^esup> i) \<noteq> 1; \<And>k. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> k @ [\<pi> i]; i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

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

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

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> i' = xs @ [x, x'] @ ys
[PROOF STEP]
using snoc(2)
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> i' @ [\<pi> i]
i icd\<^bsup>\<pi>\<^esup>\<rightarrow> i'
cs\<^bsup>\<pi>\<^esup> i = xs @ [x, x'] @ ys @ [y]

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> i' = xs @ [x, x'] @ ys
[PROOF STEP]
by (metis append1_eq_conv append_assoc)
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> i' = xs @ [x, x'] @ ys

goal (2 subgoals):
 1. \<And>i. cs\<^bsup>\<pi>\<^esup> i = xs @ [x, x'] @ [] \<Longrightarrow> \<exists>m. cs\<^bsup>\<pi>\<^esup> m = xs @ [x] \<and> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
 2. \<And>xa xsa i. \<lbrakk>\<And>i. cs\<^bsup>\<pi>\<^esup> i = xs @ [x, x'] @ xsa \<Longrightarrow> \<exists>m. cs\<^bsup>\<pi>\<^esup> m = xs @ [x] \<and> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m; cs\<^bsup>\<pi>\<^esup> i = xs @ [x, x'] @ xsa @ [xa]\<rbrakk> \<Longrightarrow> \<exists>m. cs\<^bsup>\<pi>\<^esup> m = xs @ [x] \<and> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
cs\<^bsup>\<pi>\<^esup> i' = xs @ [x, x'] @ ys
[PROOF STEP]
obtain m where **: \<open>cs\<^bsup>\<pi>\<^esup> m = xs @ [x]\<close> and \<open>i' cd\<^bsup>\<pi>\<^esup>\<rightarrow> m\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> i' = xs @ [x, x'] @ ys

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 snoc(1)
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> i' = xs @ [x, x'] @ ys
cs\<^bsup>\<pi>\<^esup> ?i1 = xs @ [x, x'] @ ys \<Longrightarrow> \<exists>m. cs\<^bsup>\<pi>\<^esup> m = xs @ [x] \<and> ?i1 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 (2 subgoals):
 1. \<And>i. cs\<^bsup>\<pi>\<^esup> i = xs @ [x, x'] @ [] \<Longrightarrow> \<exists>m. cs\<^bsup>\<pi>\<^esup> m = xs @ [x] \<and> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
 2. \<And>xa xsa i. \<lbrakk>\<And>i. cs\<^bsup>\<pi>\<^esup> i = xs @ [x, x'] @ xsa \<Longrightarrow> \<exists>m. cs\<^bsup>\<pi>\<^esup> m = xs @ [x] \<and> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m; cs\<^bsup>\<pi>\<^esup> i = xs @ [x, x'] @ xsa @ [xa]\<rbrakk> \<Longrightarrow> \<exists>m. cs\<^bsup>\<pi>\<^esup> m = xs @ [x] \<and> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
[PROOF STEP]
hence \<open>i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> m = xs @ [x]
i' cd\<^bsup>\<pi>\<^esup>\<rightarrow> m

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

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

goal (2 subgoals):
 1. \<And>i. cs\<^bsup>\<pi>\<^esup> i = xs @ [x, x'] @ [] \<Longrightarrow> \<exists>m. cs\<^bsup>\<pi>\<^esup> m = xs @ [x] \<and> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
 2. \<And>xa xsa i. \<lbrakk>\<And>i. cs\<^bsup>\<pi>\<^esup> i = xs @ [x, x'] @ xsa \<Longrightarrow> \<exists>m. cs\<^bsup>\<pi>\<^esup> m = xs @ [x] \<and> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m; cs\<^bsup>\<pi>\<^esup> i = xs @ [x, x'] @ xsa @ [xa]\<rbrakk> \<Longrightarrow> \<exists>m. cs\<^bsup>\<pi>\<^esup> m = xs @ [x] \<and> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
[PROOF STEP]
with **
[PROOF STATE]
proof (chain)
picking this:
cs\<^bsup>\<pi>\<^esup> m = xs @ [x]
i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
[PROOF STEP]
show \<open>?case\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> m = xs @ [x]
i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m

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

goal (1 subgoal):
 1. \<And>i. cs\<^bsup>\<pi>\<^esup> i = xs @ [x, x'] @ [] \<Longrightarrow> \<exists>m. cs\<^bsup>\<pi>\<^esup> m = xs @ [x] \<and> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. cs\<^bsup>\<pi>\<^esup> i = xs @ [x, x'] @ [] \<Longrightarrow> \<exists>m. cs\<^bsup>\<pi>\<^esup> m = xs @ [x] \<and> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> i = xs @ [x, x'] @ []

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

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

goal (1 subgoal):
 1. \<And>i. cs\<^bsup>\<pi>\<^esup> i = xs @ [x, x'] @ [] \<Longrightarrow> \<exists>m. cs\<^bsup>\<pi>\<^esup> m = xs @ [x] \<and> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length (cs\<^bsup>\<pi>\<^esup> i) \<noteq> 1
[PROOF STEP]
obtain i' where a: \<open>cs\<^bsup>\<pi>\<^esup> i = (cs\<^bsup>\<pi>\<^esup> i') @ [\<pi> i]\<close> and *: \<open>i icd\<^bsup>\<pi>\<^esup>\<rightarrow> i'\<close>
[PROOF STATE]
proof (prove)
using this:
length (cs\<^bsup>\<pi>\<^esup> i) \<noteq> 1

goal (1 subgoal):
 1. (\<And>i'. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> i' @ [\<pi> i]; i icd\<^bsup>\<pi>\<^esup>\<rightarrow> i'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using cs_length_g_one[of \<open>\<pi>\<close> \<open>i\<close>]
[PROOF STATE]
proof (prove)
using this:
length (cs\<^bsup>\<pi>\<^esup> i) \<noteq> 1
\<lbrakk>length (cs\<^bsup>\<pi>\<^esup> i) \<noteq> 1; \<And>k. \<lbrakk>cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> k @ [\<pi> i]; i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

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

goal (1 subgoal):
 1. \<And>i. cs\<^bsup>\<pi>\<^esup> i = xs @ [x, x'] @ [] \<Longrightarrow> \<exists>m. cs\<^bsup>\<pi>\<^esup> m = xs @ [x] \<and> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
[PROOF STEP]
have \<open>cs\<^bsup>\<pi>\<^esup> i = (xs@[x])@[x']\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> i = (xs @ [x]) @ [x']
[PROOF STEP]
using Nil
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> i = xs @ [x, x'] @ []

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

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

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> i' = xs @ [x]
[PROOF STEP]
using append1_eq_conv a
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> i = (xs @ [x]) @ [x']
(?xs @ [?x] = ?ys @ [?y]) = (?xs = ?ys \<and> ?x = ?y)
cs\<^bsup>\<pi>\<^esup> i = cs\<^bsup>\<pi>\<^esup> i' @ [\<pi> i]

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

goal (1 subgoal):
 1. \<And>i. cs\<^bsup>\<pi>\<^esup> i = xs @ [x, x'] @ [] \<Longrightarrow> \<exists>m. cs\<^bsup>\<pi>\<^esup> m = xs @ [x] \<and> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
[PROOF STEP]
thus \<open>?case\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> i' = xs @ [x]

goal (1 subgoal):
 1. \<exists>m. cs\<^bsup>\<pi>\<^esup> m = xs @ [x] \<and> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> i' = xs @ [x]
i icd\<^bsup>\<pi>\<^esup>\<rightarrow> i'

goal (1 subgoal):
 1. \<exists>m. cs\<^bsup>\<pi>\<^esup> m = xs @ [x] \<and> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
[PROOF STEP]
unfolding is_icdi_def
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> i' = xs @ [x]
is_path \<pi> \<and> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> i' \<and> (\<forall>m\<in>{i'<..<i}. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cs_split: assumes \<open>cs\<^bsup>\<pi>\<^esup> i = xs@[x]@ys@[\<pi> i]\<close>  shows \<open>\<exists> m. cs\<^bsup>\<pi>\<^esup> m = xs@[x] \<and> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>m. cs\<^bsup>\<pi>\<^esup> m = xs @ [x] \<and> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>m. cs\<^bsup>\<pi>\<^esup> m = xs @ [x] \<and> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
[PROOF STEP]
obtain x' ys' where \<open>ys@[\<pi> i] = [x']@ys'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x' ys'. ys @ [\<pi> i] = [x'] @ ys' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis append_Cons append_Nil neq_Nil_conv)
[PROOF STATE]
proof (state)
this:
ys @ [\<pi> i] = [x'] @ ys'

goal (1 subgoal):
 1. \<exists>m. cs\<^bsup>\<pi>\<^esup> m = xs @ [x] \<and> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
[PROOF STEP]
thus \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
ys @ [\<pi> i] = [x'] @ ys'

goal (1 subgoal):
 1. \<exists>m. cs\<^bsup>\<pi>\<^esup> m = xs @ [x] \<and> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
[PROOF STEP]
using cs_split'[of \<open>\<pi>\<close> \<open>i\<close> \<open>xs\<close> \<open>x\<close> \<open>x'\<close> \<open>ys'\<close>] assms
[PROOF STATE]
proof (prove)
using this:
ys @ [\<pi> i] = [x'] @ ys'
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
cs\<^bsup>\<pi>\<^esup> i = xs @ [x] @ ys @ [\<pi> i]

goal (1 subgoal):
 1. \<exists>m. cs\<^bsup>\<pi>\<^esup> m = xs @ [x] \<and> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>m. cs\<^bsup>\<pi>\<^esup> m = xs @ [x] \<and> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cs_less_split: assumes \<open>xs \<prec> ys\<close> obtains a as where \<open>ys = xs@a#as\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a as. ys = xs @ a # as \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
xs \<prec> ys

goal (1 subgoal):
 1. (\<And>a as. ys = xs @ a # as \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding cs_less.simps
[PROOF STATE]
proof (prove)
using this:
\<exists>xsa ysa. xs = xsa \<and> ys = ysa \<and> length xsa < length ysa \<and> take (length xsa) ysa = xsa

goal (1 subgoal):
 1. (\<And>a as. ys = xs @ a # as \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>a as. ys = xs @ a # as \<Longrightarrow> thesis; length xs < length ys; take (length xs) ys = xs\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by (metis Cons_nth_drop_Suc append_take_drop_id)


[STATEMENT]
lemma cs_select_is_cs: assumes \<open>is_path \<pi>\<close> \<open>xs \<noteq> Nil\<close> \<open>xs \<prec> cs\<^bsup>\<pi>\<^esup> k\<close> shows \<open>cs\<^bsup>\<pi>\<^esup> (\<pi>\<exclamdown>xs) = xs\<close> \<open>k cd\<^bsup>\<pi>\<^esup>\<rightarrow> (\<pi>\<exclamdown>xs)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> (\<pi> \<exclamdown> xs) = xs &&& k cd\<^bsup>\<pi>\<^esup>\<rightarrow> (\<pi> \<exclamdown> xs)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. cs\<^bsup>\<pi>\<^esup> (\<pi> \<exclamdown> xs) = xs
 2. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> (\<pi> \<exclamdown> xs)
[PROOF STEP]
obtain b bs where b: \<open>cs\<^bsup>\<pi>\<^esup> k = xs@b#bs\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>b bs. cs\<^bsup>\<pi>\<^esup> k = xs @ b # bs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms cs_less_split
[PROOF STATE]
proof (prove)
using this:
is_path \<pi>
xs \<noteq> []
xs \<prec> cs\<^bsup>\<pi>\<^esup> k
\<lbrakk>?xs \<prec> ?ys; \<And>a as. ?ys = ?xs @ a # as \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

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

goal (2 subgoals):
 1. cs\<^bsup>\<pi>\<^esup> (\<pi> \<exclamdown> xs) = xs
 2. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> (\<pi> \<exclamdown> xs)
[PROOF STEP]
obtain a as where a: \<open>xs = as@[a]\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>as a. xs = as @ [a] \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_path \<pi>
xs \<noteq> []
xs \<prec> cs\<^bsup>\<pi>\<^esup> k

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

goal (2 subgoals):
 1. cs\<^bsup>\<pi>\<^esup> (\<pi> \<exclamdown> xs) = xs
 2. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> (\<pi> \<exclamdown> xs)
[PROOF STEP]
have \<open>cs\<^bsup>\<pi>\<^esup> k = as@[a,b]@bs\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> k = as @ [a, b] @ bs
[PROOF STEP]
using a b
[PROOF STATE]
proof (prove)
using this:
xs = as @ [a]
cs\<^bsup>\<pi>\<^esup> k = xs @ b # bs

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

goal (2 subgoals):
 1. cs\<^bsup>\<pi>\<^esup> (\<pi> \<exclamdown> xs) = xs
 2. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> (\<pi> \<exclamdown> xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
cs\<^bsup>\<pi>\<^esup> k = as @ [a, b] @ bs
[PROOF STEP]
obtain k' where csk: \<open>cs\<^bsup>\<pi>\<^esup> k' = xs\<close> and is_cd: \<open>k cd\<^bsup>\<pi>\<^esup>\<rightarrow> k'\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> k = as @ [a, b] @ bs

goal (1 subgoal):
 1. (\<And>k'. \<lbrakk>cs\<^bsup>\<pi>\<^esup> k' = xs; k cd\<^bsup>\<pi>\<^esup>\<rightarrow> k'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using cs_split' a
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> k = as @ [a, b] @ bs
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
xs = as @ [a]

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

goal (2 subgoals):
 1. cs\<^bsup>\<pi>\<^esup> (\<pi> \<exclamdown> xs) = xs
 2. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> (\<pi> \<exclamdown> xs)
[PROOF STEP]
hence nret: \<open>\<pi> k' \<noteq> return\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> k' = xs
k cd\<^bsup>\<pi>\<^esup>\<rightarrow> k'

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

goal (2 subgoals):
 1. cs\<^bsup>\<pi>\<^esup> (\<pi> \<exclamdown> xs) = xs
 2. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> (\<pi> \<exclamdown> xs)
[PROOF STEP]
show a: \<open>cs\<^bsup>\<pi>\<^esup> (\<pi>\<exclamdown>xs) = xs\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> (\<pi> \<exclamdown> xs) = xs
[PROOF STEP]
unfolding cs_select_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> (THE k. cs\<^bsup>\<pi>\<^esup> k = xs) = xs
[PROOF STEP]
using cs_inj[OF assms(1) nret] csk the_equality[of _ \<open>k'\<close>]
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> k' = cs\<^bsup>\<pi>\<^esup> ?n' \<Longrightarrow> k' = ?n'
cs\<^bsup>\<pi>\<^esup> k' = xs
\<lbrakk>?P k'; \<And>x. ?P x \<Longrightarrow> x = k'\<rbrakk> \<Longrightarrow> (THE x. ?P x) = k'

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

goal (1 subgoal):
 1. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> (\<pi> \<exclamdown> xs)
[PROOF STEP]
show \<open>k cd\<^bsup>\<pi>\<^esup>\<rightarrow> (\<pi>\<exclamdown>xs)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> (\<pi> \<exclamdown> xs)
[PROOF STEP]
unfolding cs_select_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> (THE k. cs\<^bsup>\<pi>\<^esup> k = xs)
[PROOF STEP]
by (metis a assms(1) cs_inj cs_select_def csk is_cd nret)
[PROOF STATE]
proof (state)
this:
k cd\<^bsup>\<pi>\<^esup>\<rightarrow> (\<pi> \<exclamdown> xs)

goal:
No subgoals!
[PROOF STEP]
qed