[STATEMENT]
lemma cs_split_shift_cd: assumes \<open>n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j\<close> and \<open>j < k\<close> and \<open>k < n\<close> and \<open>\<forall>j'<k. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j' \<longrightarrow> j' \<le> j\<close> shows \<open>cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>\<^esup> j @ cs\<^bsup>\<pi>\<guillemotleft>k\<^esup> (n-k)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>\<^esup> j @ cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> (n - k)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>\<^esup> j @ cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> (n - k)
[PROOF STEP]
have path: \<open>is_path \<pi>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_path \<pi>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j
j < k
k < n
\<forall>j'<k. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j' \<longrightarrow> j' \<le> j

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

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

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>\<^esup> j @ cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> (n - k)
[PROOF STEP]
have 1: \<open>{i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} = {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k} \<union> {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} = {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k} \<union> {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} = {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k} \<union> {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>\<^esup> j @ cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> (n - k)
[PROOF STEP]
have le: \<open>\<forall> i\<in> {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k}. \<forall> j\<in> {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}. i < j\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i\<in>{i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k}. \<forall>j\<in>{i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}. i < j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>i\<in>{i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k}. \<forall>j\<in>{i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}. i < j

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>\<^esup> j @ cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> (n - k)
[PROOF STEP]
have 2: \<open>{i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k} = {i . j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {j}\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k} = {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {j}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k} = {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {j}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k} = {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {j}
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k} = {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {j}
[PROOF STEP]
assume \<open>i\<in>{i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k}\<close>
[PROOF STATE]
proof (state)
this:
i \<in> {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k}

goal (1 subgoal):
 1. {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k} = {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {j}
[PROOF STEP]
hence cd: \<open>n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i\<close> and ik:\<open>i < k\<close>
[PROOF STATE]
proof (prove)
using this:
i \<in> {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k}

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

goal (1 subgoal):
 1. {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k} = {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {j}
[PROOF STEP]
have \<open>i\<in>{i . j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {j}\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<in> {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {j}
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> i \<in> {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {j}
 2. \<not> ?P \<Longrightarrow> i \<in> {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {j}
[PROOF STEP]
assume \<open>i < j\<close>
[PROOF STATE]
proof (state)
this:
i < j

goal (2 subgoals):
 1. ?P \<Longrightarrow> i \<in> {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {j}
 2. \<not> ?P \<Longrightarrow> i \<in> {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {j}
[PROOF STEP]
hence \<open>j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i\<close>
[PROOF STATE]
proof (prove)
using this:
i < j

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> i \<in> {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {j}
 2. \<not> ?P \<Longrightarrow> i \<in> {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {j}
[PROOF STEP]
thus \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i

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

goal (1 subgoal):
 1. \<not> i < j \<Longrightarrow> i \<in> {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {j}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> i < j \<Longrightarrow> i \<in> {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {j}
[PROOF STEP]
assume \<open>\<not> i < j\<close>
[PROOF STATE]
proof (state)
this:
\<not> i < j

goal (1 subgoal):
 1. \<not> i < j \<Longrightarrow> i \<in> {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {j}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<not> i < j

goal (1 subgoal):
 1. \<not> i < j \<Longrightarrow> i \<in> {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {j}
[PROOF STEP]
have \<open>i \<le> j\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<le> j
[PROOF STEP]
using assms(4) ik cd
[PROOF STATE]
proof (prove)
using this:
\<forall>j'<k. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j' \<longrightarrow> j' \<le> j
i < k
n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i

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

goal (1 subgoal):
 1. \<not> i < j \<Longrightarrow> i \<in> {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {j}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<not> i < j
i \<le> j
[PROOF STEP]
show \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> i < j
i \<le> j

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
i \<in> {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {j}

goal (1 subgoal):
 1. {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k} = {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {j}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?i3 \<in> {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k} \<Longrightarrow> ?i3 \<in> {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {j}

goal (1 subgoal):
 1. {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k} = {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {j}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?i3 \<in> {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k} \<Longrightarrow> ?i3 \<in> {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {j}

goal (1 subgoal):
 1. {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k} = {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {j}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
?i3 \<in> {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k} \<Longrightarrow> ?i3 \<in> {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {j}

goal (1 subgoal):
 1. {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k} = {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {j}
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k} = {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {j}
[PROOF STEP]
assume \<open>i\<in>{i . j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {j}\<close>
[PROOF STATE]
proof (state)
this:
i \<in> {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {j}

goal (1 subgoal):
 1. {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k} = {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {j}
[PROOF STEP]
hence \<open>j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<or> i = j\<close>
[PROOF STATE]
proof (prove)
using this:
i \<in> {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {j}

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

goal (1 subgoal):
 1. {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k} = {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {j}
[PROOF STEP]
hence \<open>i\<in>{i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k}\<close>
[PROOF STATE]
proof (prove)
using this:
j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<or> i = j

goal (1 subgoal):
 1. i \<in> {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k}
[PROOF STEP]
using assms(1,2) cd_trans[OF _ assms(1)]
[PROOF STATE]
proof (prove)
using this:
j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<or> i = j
n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j
j < k
j cd\<^bsup>\<pi>\<^esup>\<rightarrow> ?i \<Longrightarrow> n cd\<^bsup>\<pi>\<^esup>\<rightarrow> ?i

goal (1 subgoal):
 1. i \<in> {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j; j < k; \<And>i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<Longrightarrow> n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i; j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i\<rbrakk> \<Longrightarrow> i < k
[PROOF STEP]
unfolding is_cdi_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_path \<pi> \<and> j < n \<and> \<pi> n \<noteq> local.return \<and> (\<forall>ja\<in>{j..n}. \<pi> ja \<noteq> ipd (\<pi> j)); j < k; \<And>i. is_path \<pi> \<and> i < j \<and> \<pi> j \<noteq> local.return \<and> (\<forall>j\<in>{i..j}. \<pi> j \<noteq> ipd (\<pi> i)) \<Longrightarrow> is_path \<pi> \<and> i < n \<and> \<pi> n \<noteq> local.return \<and> (\<forall>j\<in>{i..n}. \<pi> j \<noteq> ipd (\<pi> i)); is_path \<pi> \<and> i < j \<and> \<pi> j \<noteq> local.return \<and> (\<forall>j\<in>{i..j}. \<pi> j \<noteq> ipd (\<pi> i))\<rbrakk> \<Longrightarrow> i < k
[PROOF STEP]
by (metis (poly_guards_query) diff_diff_cancel diff_is_0_eq le_refl le_trans nat_less_le)
[PROOF STATE]
proof (state)
this:
i \<in> {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k}

goal (1 subgoal):
 1. {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k} = {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {j}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?i3 \<in> {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {j} \<Longrightarrow> ?i3 \<in> {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k}

goal (1 subgoal):
 1. {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k} = {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {j}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?i3 \<in> {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k} \<Longrightarrow> ?i3 \<in> {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {j}
?i3 \<in> {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {j} \<Longrightarrow> ?i3 \<in> {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k}
[PROOF STEP]
show \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
?i3 \<in> {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k} \<Longrightarrow> ?i3 \<in> {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {j}
?i3 \<in> {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {j} \<Longrightarrow> ?i3 \<in> {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k}

goal (1 subgoal):
 1. {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k} = {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {j}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
{i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k} = {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {j}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k} = {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {j}

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>\<^esup> j @ cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> (n - k)
[PROOF STEP]
have \<open>cs\<^bsup>\<pi>\<^esup> n = map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> n]\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> n = map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> n]
[PROOF STEP]
using cs_sorted_list_of_cd'
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>?\<pi>\<^esup> ?k = map ?\<pi> (sorted_list_of_set {i. ?k cd\<^bsup>?\<pi>\<^esup>\<rightarrow> i}) @ [?\<pi> ?k]

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> n = map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> n]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> n = map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> n]

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>\<^esup> j @ cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> (n - k)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> n = map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> n]

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>\<^esup> j @ cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> (n - k)
[PROOF STEP]
have \<open>\<dots> = map \<pi> (sorted_list_of_set ({i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k} \<union> {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i})) @ [\<pi> n]\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> n] = map \<pi> (sorted_list_of_set ({i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k} \<union> {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i})) @ [\<pi> n]
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
{i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} = {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k} \<union> {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}

goal (1 subgoal):
 1. map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> n] = map \<pi> (sorted_list_of_set ({i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k} \<union> {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i})) @ [\<pi> n]
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> n] = map \<pi> (sorted_list_of_set ({i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k} \<union> {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i})) @ [\<pi> n]

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>\<^esup> j @ cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> (n - k)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> n] = map \<pi> (sorted_list_of_set ({i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k} \<union> {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i})) @ [\<pi> n]

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>\<^esup> j @ cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> (n - k)
[PROOF STEP]
have \<open>\<dots> = map \<pi> ((sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k}) @ (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i})) @ [\<pi> n]\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map \<pi> (sorted_list_of_set ({i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k} \<union> {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i})) @ [\<pi> n] = map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k} @ sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}) @ [\<pi> n]
[PROOF STEP]
using sorted_list_of_set_append[OF _ _ le] is_cdi_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k}; finite {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}\<rbrakk> \<Longrightarrow> sorted_list_of_set ({i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k} \<union> {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}) = sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k} @ sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}
(?i cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?k) = (is_path ?\<pi> \<and> ?k < ?i \<and> ?\<pi> ?i \<noteq> local.return \<and> (\<forall>j\<in>{?k..?i}. ?\<pi> j \<noteq> ipd (?\<pi> ?k)))

goal (1 subgoal):
 1. map \<pi> (sorted_list_of_set ({i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k} \<union> {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i})) @ [\<pi> n] = map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k} @ sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}) @ [\<pi> n]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
map \<pi> (sorted_list_of_set ({i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k} \<union> {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i})) @ [\<pi> n] = map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k} @ sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}) @ [\<pi> n]

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>\<^esup> j @ cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> (n - k)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
map \<pi> (sorted_list_of_set ({i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k} \<union> {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i})) @ [\<pi> n] = map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k} @ sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}) @ [\<pi> n]

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>\<^esup> j @ cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> (n - k)
[PROOF STEP]
have \<open>\<dots> = (map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k})) @ (map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i})) @ [\<pi> n]\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k} @ sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}) @ [\<pi> n] = map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k}) @ map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}) @ [\<pi> n]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k} @ sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}) @ [\<pi> n] = map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k}) @ map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}) @ [\<pi> n]

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>\<^esup> j @ cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> (n - k)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k} @ sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}) @ [\<pi> n] = map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k}) @ map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}) @ [\<pi> n]

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>\<^esup> j @ cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> (n - k)
[PROOF STEP]
have \<open>\<dots> = cs\<^bsup>\<pi>\<^esup> j @ (map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i})) @ [\<pi> n]\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k}) @ map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}) @ [\<pi> n] = cs\<^bsup>\<pi>\<^esup> j @ map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}) @ [\<pi> n]
[PROOF STEP]
unfolding 2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map \<pi> (sorted_list_of_set (Collect (is_cdi j \<pi>) \<union> {j})) @ map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}) @ [\<pi> n] = cs\<^bsup>\<pi>\<^esup> j @ map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}) @ [\<pi> n]
[PROOF STEP]
using cs_sorted_list_of_cd
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>?\<pi>\<^esup> ?k = map ?\<pi> (sorted_list_of_set ({i. ?k cd\<^bsup>?\<pi>\<^esup>\<rightarrow> i} \<union> {?k}))

goal (1 subgoal):
 1. map \<pi> (sorted_list_of_set (Collect (is_cdi j \<pi>) \<union> {j})) @ map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}) @ [\<pi> n] = cs\<^bsup>\<pi>\<^esup> j @ map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}) @ [\<pi> n]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k}) @ map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}) @ [\<pi> n] = cs\<^bsup>\<pi>\<^esup> j @ map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}) @ [\<pi> n]

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>\<^esup> j @ cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> (n - k)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k}) @ map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}) @ [\<pi> n] = cs\<^bsup>\<pi>\<^esup> j @ map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}) @ [\<pi> n]

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>\<^esup> j @ cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> (n - k)
[PROOF STEP]
have \<open>\<dots> = cs\<^bsup>\<pi>\<^esup> j @ cs\<^bsup>\<pi>\<guillemotleft>k\<^esup> (n-k)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> j @ map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}) @ [\<pi> n] = cs\<^bsup>\<pi>\<^esup> j @ cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> (n - k)
[PROOF STEP]
using cs_path_shift_set_cd[OF path, of \<open>k\<close> \<open>n-k\<close>] assms(3)
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> (n - k) = map \<pi> (sorted_list_of_set {i. k + (n - k) cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}) @ [\<pi> (k + (n - k))]
k < n

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> j @ map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}) @ [\<pi> n] = cs\<^bsup>\<pi>\<^esup> j @ cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> (n - k)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> j @ map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}) @ [\<pi> n] = cs\<^bsup>\<pi>\<^esup> j @ cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> (n - k)

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>\<^esup> j @ cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> (n - k)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>\<^esup> j @ cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> (n - k)
[PROOF STEP]
show \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>\<^esup> j @ cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> (n - k)

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>\<^esup> j @ cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> (n - k)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>\<^esup> j @ cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> (n - k)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cs_split_shift_nocd: assumes \<open>is_path \<pi>\<close> and \<open>k < n\<close> and \<open>\<forall>j. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<longrightarrow> k \<le> j\<close> shows \<open>cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>\<guillemotleft>k\<^esup> (n-k)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> (n - k)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> (n - k)
[PROOF STEP]
have path: \<open>is_path \<pi>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_path \<pi>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_path \<pi>
k < n
\<forall>j. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<longrightarrow> k \<le> j

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

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> (n - k)
[PROOF STEP]
have 1: \<open>{i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} = {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k} \<union> {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} = {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k} \<union> {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} = {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k} \<union> {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> (n - k)
[PROOF STEP]
have le: \<open>\<forall> i\<in> {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k}. \<forall> j\<in> {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}. i < j\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i\<in>{i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k}. \<forall>j\<in>{i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}. i < j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>i\<in>{i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k}. \<forall>j\<in>{i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}. i < j

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> (n - k)
[PROOF STEP]
have 2: \<open>{i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k} = {}\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k} = {}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_path \<pi>
k < n
\<forall>j. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<longrightarrow> k \<le> j

goal (1 subgoal):
 1. {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k} = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k} = {}

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> (n - k)
[PROOF STEP]
have \<open>cs\<^bsup>\<pi>\<^esup> n = map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> n]\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> n = map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> n]
[PROOF STEP]
using cs_sorted_list_of_cd'
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>?\<pi>\<^esup> ?k = map ?\<pi> (sorted_list_of_set {i. ?k cd\<^bsup>?\<pi>\<^esup>\<rightarrow> i}) @ [?\<pi> ?k]

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> n = map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> n]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> n = map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> n]

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> (n - k)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> n = map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> n]

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> (n - k)
[PROOF STEP]
have \<open>\<dots> = map \<pi> (sorted_list_of_set ({i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k} \<union> {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i})) @ [\<pi> n]\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> n] = map \<pi> (sorted_list_of_set ({i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k} \<union> {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i})) @ [\<pi> n]
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
{i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} = {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k} \<union> {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}

goal (1 subgoal):
 1. map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> n] = map \<pi> (sorted_list_of_set ({i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k} \<union> {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i})) @ [\<pi> n]
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> n] = map \<pi> (sorted_list_of_set ({i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k} \<union> {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i})) @ [\<pi> n]

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> (n - k)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> n] = map \<pi> (sorted_list_of_set ({i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k} \<union> {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i})) @ [\<pi> n]

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> (n - k)
[PROOF STEP]
have \<open>\<dots> = map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}) @ [\<pi> n]\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map \<pi> (sorted_list_of_set ({i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k} \<union> {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i})) @ [\<pi> n] = map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}) @ [\<pi> n]
[PROOF STEP]
unfolding 2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map \<pi> (sorted_list_of_set ({} \<union> {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i})) @ [\<pi> n] = map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}) @ [\<pi> n]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
map \<pi> (sorted_list_of_set ({i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k} \<union> {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i})) @ [\<pi> n] = map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}) @ [\<pi> n]

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> (n - k)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
map \<pi> (sorted_list_of_set ({i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> i < k} \<union> {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i})) @ [\<pi> n] = map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}) @ [\<pi> n]

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> (n - k)
[PROOF STEP]
have \<open>\<dots> = cs\<^bsup>\<pi>\<guillemotleft>k\<^esup> (n-k)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}) @ [\<pi> n] = cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> (n - k)
[PROOF STEP]
using cs_path_shift_set_cd[OF path, of \<open>k\<close> \<open>n-k\<close>] assms(2)
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> (n - k) = map \<pi> (sorted_list_of_set {i. k + (n - k) cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}) @ [\<pi> (k + (n - k))]
k < n

goal (1 subgoal):
 1. map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}) @ [\<pi> n] = cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> (n - k)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i \<and> k \<le> i}) @ [\<pi> n] = cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> (n - k)

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> (n - k)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> (n - k)
[PROOF STEP]
show \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi> \<guillemotleft> k\<^esup> (n - k)

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

goal:
No subgoals!
[PROOF STEP]
qed