[STATEMENT]
lemma cs_path_swap_cd: assumes \<open>is_path \<pi>\<close> and \<open>is_path \<pi>'\<close> and \<open>cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n'\<close> and \<open>n cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close>
obtains k' where \<open>n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'\<close> and \<open>cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k'. \<lbrakk>n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'; cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>k'. \<lbrakk>n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'; cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from cd_in_cs[OF assms(4)]
[PROOF STATE]
proof (chain)
picking this:
\<exists>ns. cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>\<^esup> k @ ns @ [\<pi> n]
[PROOF STEP]
obtain ns where *: \<open>cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>\<^esup> k @ ns @ [\<pi> n]\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>ns. cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>\<^esup> k @ ns @ [\<pi> n]

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

goal (1 subgoal):
 1. (\<And>k'. \<lbrakk>n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'; cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
obtain xs x where csk: \<open>cs\<^bsup>\<pi>\<^esup> k = xs @ [x]\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>xs x. cs\<^bsup>\<pi>\<^esup> k = xs @ [x] \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis cs_not_nil rev_exhaust)
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> k = xs @ [x]

goal (1 subgoal):
 1. (\<And>k'. \<lbrakk>n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'; cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have \<open>\<pi> n = \<pi>' n'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> n = \<pi>' n'
[PROOF STEP]
using assms(3) last_cs
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n'
last (cs\<^bsup>?\<pi>\<^esup> ?i) = ?\<pi> ?i

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

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

goal (1 subgoal):
 1. cs\<^bsup>\<pi>'\<^esup> n' = xs @ [x] @ ns @ [\<pi>' n']
[PROOF STEP]
using * assms(3) csk
[PROOF STATE]
proof (prove)
using this:
\<pi> n = \<pi>' n'
cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>\<^esup> k @ ns @ [\<pi> n]
cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n'
cs\<^bsup>\<pi>\<^esup> k = xs @ [x]

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

goal (1 subgoal):
 1. (\<And>k'. \<lbrakk>n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'; cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> k'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from cs_split[OF **]
[PROOF STATE]
proof (chain)
picking this:
\<exists>m. cs\<^bsup>\<pi>'\<^esup> m = xs @ [x] \<and> n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> m
[PROOF STEP]
obtain k' where \<open>cs\<^bsup>\<pi>'\<^esup> k' = xs @ [x]\<close> \<open>n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>m. cs\<^bsup>\<pi>'\<^esup> m = xs @ [x] \<and> n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> m

goal (1 subgoal):
 1. (\<And>k'. \<lbrakk>cs\<^bsup>\<pi>'\<^esup> k' = xs @ [x]; n' 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 @ [x]
n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'

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

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that csk
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>'\<^esup> k' = xs @ [x]
n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k'
\<lbrakk>n' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> ?k'1; cs\<^bsup>\<pi>\<^esup> k = cs\<^bsup>\<pi>'\<^esup> ?k'1\<rbrakk> \<Longrightarrow> thesis
cs\<^bsup>\<pi>\<^esup> k = xs @ [x]

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma path_ipd_swap: assumes \<open>is_path \<pi>\<close> \<open>\<pi> k \<noteq> return\<close> \<open>k < n\<close>
obtains \<pi>' m where \<open>is_path \<pi>'\<close> \<open>\<pi> =\<^bsub>n\<^esub>  \<pi>'\<close> \<open>k < m\<close> \<open>\<pi>' m = ipd (\<pi>' k)\<close> \<open>\<forall> l \<in> {k..<m}. \<pi>' l \<noteq> ipd (\<pi>' k)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<pi>' m. \<lbrakk>is_path \<pi>'; \<pi> =\<^bsub>n\<^esub> \<pi>'; k < m; \<pi>' m = ipd (\<pi>' k); \<forall>l\<in>{k..<m}. \<pi>' l \<noteq> ipd (\<pi>' k)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>\<pi>' m. \<lbrakk>is_path \<pi>'; \<pi> =\<^bsub>n\<^esub> \<pi>'; k < m; \<pi>' m = ipd (\<pi>' k); \<forall>l\<in>{k..<m}. \<pi>' l \<noteq> ipd (\<pi>' k)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
obtain \<pi>' r where *: \<open>\<pi>' 0 = \<pi> n\<close> \<open>is_path \<pi>'\<close> \<open>\<pi>' r = return\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<pi>' r. \<lbrakk>\<pi>' 0 = \<pi> n; is_path \<pi>'; \<pi>' r = local.return\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis assms(1) path_nodes reaching_ret)
[PROOF STATE]
proof (state)
this:
\<pi>' 0 = \<pi> n
is_path \<pi>'
\<pi>' r = local.return

goal (1 subgoal):
 1. (\<And>\<pi>' m. \<lbrakk>is_path \<pi>'; \<pi> =\<^bsub>n\<^esub> \<pi>'; k < m; \<pi>' m = ipd (\<pi>' k); \<forall>l\<in>{k..<m}. \<pi>' l \<noteq> ipd (\<pi>' k)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
let \<open>?\<pi>\<close> = \<open>\<pi>@\<^bsup>n\<^esup>  \<pi>'\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>\<pi>' m. \<lbrakk>is_path \<pi>'; \<pi> =\<^bsub>n\<^esub> \<pi>'; k < m; \<pi>' m = ipd (\<pi>' k); \<forall>l\<in>{k..<m}. \<pi>' l \<noteq> ipd (\<pi>' k)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have path: \<open>is_path ?\<pi>\<close> and ret: \<open>?\<pi> (n + r) = return\<close> and equpto:  \<open>?\<pi> =\<^bsub>n\<^esub>  \<pi>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_path (\<pi> @\<^bsup>n\<^esup> \<pi>') &&& (\<pi> @\<^bsup>n\<^esup> \<pi>') (n + r) = local.return &&& (\<pi> @\<^bsup>n\<^esup> \<pi>') =\<^bsub>n\<^esub> \<pi>
[PROOF STEP]
using assms path_cons * path_append_eq_up_to
[PROOF STATE]
proof (prove)
using this:
is_path \<pi>
\<pi> k \<noteq> local.return
k < n
\<lbrakk>is_path ?\<pi>; is_path ?\<pi>'; ?\<pi> ?m = ?\<pi>' 0\<rbrakk> \<Longrightarrow> is_path (?\<pi> @\<^bsup>?m\<^esup> ?\<pi>')
\<pi>' 0 = \<pi> n
is_path \<pi>'
\<pi>' r = local.return
(?\<pi> @\<^bsup>?k\<^esup> ?\<pi>') =\<^bsub>?k\<^esub> ?\<pi>

goal (1 subgoal):
 1. is_path (\<pi> @\<^bsup>n\<^esup> \<pi>') &&& (\<pi> @\<^bsup>n\<^esup> \<pi>') (n + r) = local.return &&& (\<pi> @\<^bsup>n\<^esup> \<pi>') =\<^bsub>n\<^esub> \<pi>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_path (\<pi> @\<^bsup>n\<^esup> \<pi>')
(\<pi> @\<^bsup>n\<^esup> \<pi>') (n + r) = local.return
(\<pi> @\<^bsup>n\<^esup> \<pi>') =\<^bsub>n\<^esub> \<pi>

goal (1 subgoal):
 1. (\<And>\<pi>' m. \<lbrakk>is_path \<pi>'; \<pi> =\<^bsub>n\<^esub> \<pi>'; k < m; \<pi>' m = ipd (\<pi>' k); \<forall>l\<in>{k..<m}. \<pi>' l \<noteq> ipd (\<pi>' k)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have \<pi>k: \<open>?\<pi> k = \<pi> k\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<pi> @\<^bsup>n\<^esup> \<pi>') k = \<pi> k
[PROOF STEP]
by (metis assms(3) less_imp_le_nat path_append_def)
[PROOF STATE]
proof (state)
this:
(\<pi> @\<^bsup>n\<^esup> \<pi>') k = \<pi> k

goal (1 subgoal):
 1. (\<And>\<pi>' m. \<lbrakk>is_path \<pi>'; \<pi> =\<^bsub>n\<^esub> \<pi>'; k < m; \<pi>' m = ipd (\<pi>' k); \<forall>l\<in>{k..<m}. \<pi>' l \<noteq> ipd (\<pi>' k)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
obtain j where j: \<open>k < j \<and> j \<le> (n + r) \<and> ?\<pi> j = ipd (\<pi> k)\<close> (is \<open>?P j\<close> )
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>j. k < j \<and> j \<le> n + r \<and> (\<pi> @\<^bsup>n\<^esup> \<pi>') j = ipd (\<pi> k) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis \<pi>k assms(2) path path_ret_ipd ret)
[PROOF STATE]
proof (state)
this:
k < j \<and> j \<le> n + r \<and> (\<pi> @\<^bsup>n\<^esup> \<pi>') j = ipd (\<pi> k)

goal (1 subgoal):
 1. (\<And>\<pi>' m. \<lbrakk>is_path \<pi>'; \<pi> =\<^bsub>n\<^esub> \<pi>'; k < m; \<pi>' m = ipd (\<pi>' k); \<forall>l\<in>{k..<m}. \<pi>' l \<noteq> ipd (\<pi>' k)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
define m where m: \<open>m \<equiv> LEAST m . ?P m\<close>
[PROOF STATE]
proof (state)
this:
m \<equiv> LEAST m. k < m \<and> m \<le> n + r \<and> (\<pi> @\<^bsup>n\<^esup> \<pi>') m = ipd (\<pi> k)

goal (1 subgoal):
 1. (\<And>\<pi>' m. \<lbrakk>is_path \<pi>'; \<pi> =\<^bsub>n\<^esub> \<pi>'; k < m; \<pi>' m = ipd (\<pi>' k); \<forall>l\<in>{k..<m}. \<pi>' l \<noteq> ipd (\<pi>' k)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have Pm: \<open>?P m\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k < m \<and> m \<le> n + r \<and> (\<pi> @\<^bsup>n\<^esup> \<pi>') m = ipd (\<pi> k)
[PROOF STEP]
using LeastI[of \<open>?P\<close> \<open>j\<close>] j m
[PROOF STATE]
proof (prove)
using this:
k < j \<and> j \<le> n + r \<and> (\<pi> @\<^bsup>n\<^esup> \<pi>') j = ipd (\<pi> k) \<Longrightarrow> k < (LEAST x. k < x \<and> x \<le> n + r \<and> (\<pi> @\<^bsup>n\<^esup> \<pi>') x = ipd (\<pi> k)) \<and> (LEAST x. k < x \<and> x \<le> n + r \<and> (\<pi> @\<^bsup>n\<^esup> \<pi>') x = ipd (\<pi> k)) \<le> n + r \<and> (\<pi> @\<^bsup>n\<^esup> \<pi>') (LEAST x. k < x \<and> x \<le> n + r \<and> (\<pi> @\<^bsup>n\<^esup> \<pi>') x = ipd (\<pi> k)) = ipd (\<pi> k)
k < j \<and> j \<le> n + r \<and> (\<pi> @\<^bsup>n\<^esup> \<pi>') j = ipd (\<pi> k)
m \<equiv> LEAST m. k < m \<and> m \<le> n + r \<and> (\<pi> @\<^bsup>n\<^esup> \<pi>') m = ipd (\<pi> k)

goal (1 subgoal):
 1. k < m \<and> m \<le> n + r \<and> (\<pi> @\<^bsup>n\<^esup> \<pi>') m = ipd (\<pi> k)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k < m \<and> m \<le> n + r \<and> (\<pi> @\<^bsup>n\<^esup> \<pi>') m = ipd (\<pi> k)

goal (1 subgoal):
 1. (\<And>\<pi>' m. \<lbrakk>is_path \<pi>'; \<pi> =\<^bsub>n\<^esub> \<pi>'; k < m; \<pi>' m = ipd (\<pi>' k); \<forall>l\<in>{k..<m}. \<pi>' l \<noteq> ipd (\<pi>' k)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
hence km: \<open>k < m\<close> \<open>m \<le> (n + r)\<close> \<open>?\<pi> m = ipd (\<pi> k)\<close>
[PROOF STATE]
proof (prove)
using this:
k < m \<and> m \<le> n + r \<and> (\<pi> @\<^bsup>n\<^esup> \<pi>') m = ipd (\<pi> k)

goal (1 subgoal):
 1. k < m &&& m \<le> n + r &&& (\<pi> @\<^bsup>n\<^esup> \<pi>') m = ipd (\<pi> k)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k < m
m \<le> n + r
(\<pi> @\<^bsup>n\<^esup> \<pi>') m = ipd (\<pi> k)

goal (1 subgoal):
 1. (\<And>\<pi>' m. \<lbrakk>is_path \<pi>'; \<pi> =\<^bsub>n\<^esub> \<pi>'; k < m; \<pi>' m = ipd (\<pi>' k); \<forall>l\<in>{k..<m}. \<pi>' l \<noteq> ipd (\<pi>' k)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have le: \<open>\<And>l. ?P l \<Longrightarrow> m \<le> l\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. k < l \<and> l \<le> n + r \<and> (\<pi> @\<^bsup>n\<^esup> \<pi>') l = ipd (\<pi> k) \<Longrightarrow> m \<le> l
[PROOF STEP]
using Least_le[of \<open>?P\<close>] m
[PROOF STATE]
proof (prove)
using this:
k < ?k \<and> ?k \<le> n + r \<and> (\<pi> @\<^bsup>n\<^esup> \<pi>') ?k = ipd (\<pi> k) \<Longrightarrow> (LEAST x. k < x \<and> x \<le> n + r \<and> (\<pi> @\<^bsup>n\<^esup> \<pi>') x = ipd (\<pi> k)) \<le> ?k
m \<equiv> LEAST m. k < m \<and> m \<le> n + r \<and> (\<pi> @\<^bsup>n\<^esup> \<pi>') m = ipd (\<pi> k)

goal (1 subgoal):
 1. \<And>l. k < l \<and> l \<le> n + r \<and> (\<pi> @\<^bsup>n\<^esup> \<pi>') l = ipd (\<pi> k) \<Longrightarrow> m \<le> l
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
k < ?l1 \<and> ?l1 \<le> n + r \<and> (\<pi> @\<^bsup>n\<^esup> \<pi>') ?l1 = ipd (\<pi> k) \<Longrightarrow> m \<le> ?l1

goal (1 subgoal):
 1. (\<And>\<pi>' m. \<lbrakk>is_path \<pi>'; \<pi> =\<^bsub>n\<^esub> \<pi>'; k < m; \<pi>' m = ipd (\<pi>' k); \<forall>l\<in>{k..<m}. \<pi>' l \<noteq> ipd (\<pi>' k)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have \<pi>knipd: \<open>?\<pi> k \<noteq> ipd (\<pi> k)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<pi> @\<^bsup>n\<^esup> \<pi>') k \<noteq> ipd (\<pi> k)
[PROOF STEP]
by (metis \<pi>k assms(1) assms(2) ipd_not_self path_nodes)
[PROOF STATE]
proof (state)
this:
(\<pi> @\<^bsup>n\<^esup> \<pi>') k \<noteq> ipd (\<pi> k)

goal (1 subgoal):
 1. (\<And>\<pi>' m. \<lbrakk>is_path \<pi>'; \<pi> =\<^bsub>n\<^esub> \<pi>'; k < m; \<pi>' m = ipd (\<pi>' k); \<forall>l\<in>{k..<m}. \<pi>' l \<noteq> ipd (\<pi>' k)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have nipd': \<open>\<And>l. k < l \<Longrightarrow> l < m \<Longrightarrow> ?\<pi> l \<noteq> ipd (\<pi> k)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>k < l; l < m\<rbrakk> \<Longrightarrow> (\<pi> @\<^bsup>n\<^esup> \<pi>') l \<noteq> ipd (\<pi> k)
[PROOF STEP]
apply (rule ccontr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>k < l; l < m; \<not> (\<pi> @\<^bsup>n\<^esup> \<pi>') l \<noteq> ipd (\<pi> k)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
using le km(2)
[PROOF STATE]
proof (prove)
using this:
k < ?l1 \<and> ?l1 \<le> n + r \<and> (\<pi> @\<^bsup>n\<^esup> \<pi>') ?l1 = ipd (\<pi> k) \<Longrightarrow> m \<le> ?l1
m \<le> n + r

goal (1 subgoal):
 1. \<And>l. \<lbrakk>k < l; l < m; \<not> (\<pi> @\<^bsup>n\<^esup> \<pi>') l \<noteq> ipd (\<pi> k)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<lbrakk>k < ?l1; ?l1 < m\<rbrakk> \<Longrightarrow> (\<pi> @\<^bsup>n\<^esup> \<pi>') ?l1 \<noteq> ipd (\<pi> k)

goal (1 subgoal):
 1. (\<And>\<pi>' m. \<lbrakk>is_path \<pi>'; \<pi> =\<^bsub>n\<^esub> \<pi>'; k < m; \<pi>' m = ipd (\<pi>' k); \<forall>l\<in>{k..<m}. \<pi>' l \<noteq> ipd (\<pi>' k)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have \<open>\<forall> l \<in> {k..<m}. ?\<pi> l \<noteq> ipd(\<pi> k)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>l\<in>{k..<m}. (\<pi> @\<^bsup>n\<^esup> \<pi>') l \<noteq> ipd (\<pi> k)
[PROOF STEP]
using \<pi>knipd nipd'
[PROOF STATE]
proof (prove)
using this:
(\<pi> @\<^bsup>n\<^esup> \<pi>') k \<noteq> ipd (\<pi> k)
\<lbrakk>k < ?l1; ?l1 < m\<rbrakk> \<Longrightarrow> (\<pi> @\<^bsup>n\<^esup> \<pi>') ?l1 \<noteq> ipd (\<pi> k)

goal (1 subgoal):
 1. \<forall>l\<in>{k..<m}. (\<pi> @\<^bsup>n\<^esup> \<pi>') l \<noteq> ipd (\<pi> k)
[PROOF STEP]
by(auto, metis le_eq_less_or_eq,metis le_eq_less_or_eq)
[PROOF STATE]
proof (state)
this:
\<forall>l\<in>{k..<m}. (\<pi> @\<^bsup>n\<^esup> \<pi>') l \<noteq> ipd (\<pi> k)

goal (1 subgoal):
 1. (\<And>\<pi>' m. \<lbrakk>is_path \<pi>'; \<pi> =\<^bsub>n\<^esub> \<pi>'; k < m; \<pi>' m = ipd (\<pi>' k); \<forall>l\<in>{k..<m}. \<pi>' l \<noteq> ipd (\<pi>' k)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
thus \<open>thesis\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>l\<in>{k..<m}. (\<pi> @\<^bsup>n\<^esup> \<pi>') l \<noteq> ipd (\<pi> k)

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
\<forall>l\<in>{k..<m}. (\<pi> @\<^bsup>n\<^esup> \<pi>') l \<noteq> ipd (\<pi> k)
\<lbrakk>is_path ?\<pi>'1; \<pi> =\<^bsub>n\<^esub> ?\<pi>'1; k < ?m1; ?\<pi>'1 ?m1 = ipd (?\<pi>'1 k); \<forall>l\<in>{k..<?m1}. ?\<pi>'1 l \<noteq> ipd (?\<pi>'1 k)\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (metis \<pi>k eq_up_to_sym km(1) km(3) path path_append_eq_up_to)
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cs_sorted_list_of_cd': \<open>cs\<^bsup>\<pi>\<^esup> k = map \<pi> (sorted_list_of_set { i . k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> k]\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> k = map \<pi> (sorted_list_of_set {i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> k]
[PROOF STEP]
proof (induction \<open>\<pi>\<close> \<open>k\<close> rule: cs.induct, cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<pi> n. \<lbrakk>Ex (is_icdi n \<pi>) \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> The (is_icdi n \<pi>) = map \<pi> (sorted_list_of_set {i. The (is_icdi n \<pi>) cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> (The (is_icdi n \<pi>))]; ?P1 \<pi> n\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> n = map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> n]
 2. \<And>\<pi> n. \<lbrakk>Ex (is_icdi n \<pi>) \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> The (is_icdi n \<pi>) = map \<pi> (sorted_list_of_set {i. The (is_icdi n \<pi>) cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> (The (is_icdi n \<pi>))]; \<not> ?P1 \<pi> n\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> n = map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> n]
[PROOF STEP]
case (1 \<pi> k)
[PROOF STATE]
proof (state)
this:
Ex (is_icdi k \<pi>) \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> The (is_icdi k \<pi>) = map \<pi> (sorted_list_of_set {i. The (is_icdi k \<pi>) cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> (The (is_icdi k \<pi>))]

goal (2 subgoals):
 1. \<And>\<pi> n. \<lbrakk>Ex (is_icdi n \<pi>) \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> The (is_icdi n \<pi>) = map \<pi> (sorted_list_of_set {i. The (is_icdi n \<pi>) cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> (The (is_icdi n \<pi>))]; ?P1 \<pi> n\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> n = map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> n]
 2. \<And>\<pi> n. \<lbrakk>Ex (is_icdi n \<pi>) \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> The (is_icdi n \<pi>) = map \<pi> (sorted_list_of_set {i. The (is_icdi n \<pi>) cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> (The (is_icdi n \<pi>))]; \<not> ?P1 \<pi> n\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> n = map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> n]
[PROOF STEP]
assume \<open>\<exists> j. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> j\<close>
[PROOF STATE]
proof (state)
this:
\<exists>j. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> j

goal (2 subgoals):
 1. \<And>\<pi> n. \<lbrakk>Ex (is_icdi n \<pi>) \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> The (is_icdi n \<pi>) = map \<pi> (sorted_list_of_set {i. The (is_icdi n \<pi>) cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> (The (is_icdi n \<pi>))]; ?P1 \<pi> n\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> n = map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> n]
 2. \<And>\<pi> n. \<lbrakk>Ex (is_icdi n \<pi>) \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> The (is_icdi n \<pi>) = map \<pi> (sorted_list_of_set {i. The (is_icdi n \<pi>) cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> (The (is_icdi n \<pi>))]; \<not> ?P1 \<pi> n\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> n = map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> n]
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>j. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> j
[PROOF STEP]
obtain j where j: "k icd\<^bsup>\<pi>\<^esup>\<rightarrow> j"
[PROOF STATE]
proof (prove)
using this:
\<exists>j. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> j

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

goal (2 subgoals):
 1. \<And>\<pi> n. \<lbrakk>Ex (is_icdi n \<pi>) \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> The (is_icdi n \<pi>) = map \<pi> (sorted_list_of_set {i. The (is_icdi n \<pi>) cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> (The (is_icdi n \<pi>))]; ?P1 \<pi> n\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> n = map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> n]
 2. \<And>\<pi> n. \<lbrakk>Ex (is_icdi n \<pi>) \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> The (is_icdi n \<pi>) = map \<pi> (sorted_list_of_set {i. The (is_icdi n \<pi>) cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> (The (is_icdi n \<pi>))]; \<not> ?P1 \<pi> n\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> n = map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> n]
[PROOF STEP]
hence csj: \<open>cs\<^bsup>\<pi>\<^esup> j = map \<pi> (sorted_list_of_set {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> j]\<close>
[PROOF STATE]
proof (prove)
using this:
k icd\<^bsup>\<pi>\<^esup>\<rightarrow> j

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

goal (2 subgoals):
 1. \<And>\<pi> n. \<lbrakk>Ex (is_icdi n \<pi>) \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> The (is_icdi n \<pi>) = map \<pi> (sorted_list_of_set {i. The (is_icdi n \<pi>) cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> (The (is_icdi n \<pi>))]; ?P1 \<pi> n\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> n = map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> n]
 2. \<And>\<pi> n. \<lbrakk>Ex (is_icdi n \<pi>) \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> The (is_icdi n \<pi>) = map \<pi> (sorted_list_of_set {i. The (is_icdi n \<pi>) cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> (The (is_icdi n \<pi>))]; \<not> ?P1 \<pi> n\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> n = map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> n]
[PROOF STEP]
have \<open>{i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} = insert j {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} = insert j {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}
[PROOF STEP]
using cdi_is_cd_icdi[OF j]
[PROOF STATE]
proof (prove)
using this:
(k cd\<^bsup>\<pi>\<^esup>\<rightarrow> ?i) = (j cd\<^bsup>\<pi>\<^esup>\<rightarrow> ?i \<or> ?i = j)

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

goal (2 subgoals):
 1. \<And>\<pi> n. \<lbrakk>Ex (is_icdi n \<pi>) \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> The (is_icdi n \<pi>) = map \<pi> (sorted_list_of_set {i. The (is_icdi n \<pi>) cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> (The (is_icdi n \<pi>))]; ?P1 \<pi> n\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> n = map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> n]
 2. \<And>\<pi> n. \<lbrakk>Ex (is_icdi n \<pi>) \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> The (is_icdi n \<pi>) = map \<pi> (sorted_list_of_set {i. The (is_icdi n \<pi>) cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> (The (is_icdi n \<pi>))]; \<not> ?P1 \<pi> n\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> n = map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> n]
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
{i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} = insert j {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}

goal (2 subgoals):
 1. \<And>\<pi> n. \<lbrakk>Ex (is_icdi n \<pi>) \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> The (is_icdi n \<pi>) = map \<pi> (sorted_list_of_set {i. The (is_icdi n \<pi>) cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> (The (is_icdi n \<pi>))]; ?P1 \<pi> n\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> n = map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> n]
 2. \<And>\<pi> n. \<lbrakk>Ex (is_icdi n \<pi>) \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> The (is_icdi n \<pi>) = map \<pi> (sorted_list_of_set {i. The (is_icdi n \<pi>) cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> (The (is_icdi n \<pi>))]; \<not> ?P1 \<pi> n\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> n = map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> n]
[PROOF STEP]
have f: \<open>finite {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}
[PROOF STEP]
unfolding is_cdi_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {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))}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}

goal (2 subgoals):
 1. \<And>\<pi> n. \<lbrakk>Ex (is_icdi n \<pi>) \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> The (is_icdi n \<pi>) = map \<pi> (sorted_list_of_set {i. The (is_icdi n \<pi>) cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> (The (is_icdi n \<pi>))]; ?P1 \<pi> n\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> n = map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> n]
 2. \<And>\<pi> n. \<lbrakk>Ex (is_icdi n \<pi>) \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> The (is_icdi n \<pi>) = map \<pi> (sorted_list_of_set {i. The (is_icdi n \<pi>) cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> (The (is_icdi n \<pi>))]; \<not> ?P1 \<pi> n\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> n = map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> n]
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}

goal (2 subgoals):
 1. \<And>\<pi> n. \<lbrakk>Ex (is_icdi n \<pi>) \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> The (is_icdi n \<pi>) = map \<pi> (sorted_list_of_set {i. The (is_icdi n \<pi>) cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> (The (is_icdi n \<pi>))]; ?P1 \<pi> n\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> n = map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> n]
 2. \<And>\<pi> n. \<lbrakk>Ex (is_icdi n \<pi>) \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> The (is_icdi n \<pi>) = map \<pi> (sorted_list_of_set {i. The (is_icdi n \<pi>) cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> (The (is_icdi n \<pi>))]; \<not> ?P1 \<pi> n\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> n = map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> n]
[PROOF STEP]
have \<open>j \<notin> {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j \<notin> {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}
[PROOF STEP]
unfolding is_cdi_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j \<notin> {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))}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
j \<notin> {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}

goal (2 subgoals):
 1. \<And>\<pi> n. \<lbrakk>Ex (is_icdi n \<pi>) \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> The (is_icdi n \<pi>) = map \<pi> (sorted_list_of_set {i. The (is_icdi n \<pi>) cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> (The (is_icdi n \<pi>))]; ?P1 \<pi> n\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> n = map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> n]
 2. \<And>\<pi> n. \<lbrakk>Ex (is_icdi n \<pi>) \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> The (is_icdi n \<pi>) = map \<pi> (sorted_list_of_set {i. The (is_icdi n \<pi>) cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> (The (is_icdi n \<pi>))]; \<not> ?P1 \<pi> n\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> n = map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> n]
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
{i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} = insert j {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}
finite {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}
j \<notin> {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}
[PROOF STEP]
have \<open>sorted_list_of_set { i . k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} = insort j (sorted_list_of_set { i . j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i})\<close>
[PROOF STATE]
proof (prove)
using this:
{i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} = insert j {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}
finite {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}
j \<notin> {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}

goal (1 subgoal):
 1. sorted_list_of_set {i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} = insort j (sorted_list_of_set {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i})
[PROOF STEP]
using sorted_list_of_set_insert
[PROOF STATE]
proof (prove)
using this:
{i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} = insert j {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}
finite {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}
j \<notin> {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}
\<lbrakk>finite ?A; ?x \<notin> ?A\<rbrakk> \<Longrightarrow> sorted_list_of_set (insert ?x ?A) = insort ?x (sorted_list_of_set ?A)

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

goal (2 subgoals):
 1. \<And>\<pi> n. \<lbrakk>Ex (is_icdi n \<pi>) \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> The (is_icdi n \<pi>) = map \<pi> (sorted_list_of_set {i. The (is_icdi n \<pi>) cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> (The (is_icdi n \<pi>))]; ?P1 \<pi> n\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> n = map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> n]
 2. \<And>\<pi> n. \<lbrakk>Ex (is_icdi n \<pi>) \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> The (is_icdi n \<pi>) = map \<pi> (sorted_list_of_set {i. The (is_icdi n \<pi>) cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> (The (is_icdi n \<pi>))]; \<not> ?P1 \<pi> n\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> n = map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> n]
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sorted_list_of_set {i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} = insort j (sorted_list_of_set {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i})

goal (2 subgoals):
 1. \<And>\<pi> n. \<lbrakk>Ex (is_icdi n \<pi>) \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> The (is_icdi n \<pi>) = map \<pi> (sorted_list_of_set {i. The (is_icdi n \<pi>) cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> (The (is_icdi n \<pi>))]; ?P1 \<pi> n\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> n = map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> n]
 2. \<And>\<pi> n. \<lbrakk>Ex (is_icdi n \<pi>) \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> The (is_icdi n \<pi>) = map \<pi> (sorted_list_of_set {i. The (is_icdi n \<pi>) cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> (The (is_icdi n \<pi>))]; \<not> ?P1 \<pi> n\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> n = map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> n]
[PROOF STEP]
have \<open>\<forall> x \<in>  {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}. x < j\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>{i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}. x < j
[PROOF STEP]
unfolding is_cdi_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>{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))}. x < j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>{i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}. x < j

goal (2 subgoals):
 1. \<And>\<pi> n. \<lbrakk>Ex (is_icdi n \<pi>) \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> The (is_icdi n \<pi>) = map \<pi> (sorted_list_of_set {i. The (is_icdi n \<pi>) cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> (The (is_icdi n \<pi>))]; ?P1 \<pi> n\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> n = map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> n]
 2. \<And>\<pi> n. \<lbrakk>Ex (is_icdi n \<pi>) \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> The (is_icdi n \<pi>) = map \<pi> (sorted_list_of_set {i. The (is_icdi n \<pi>) cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> (The (is_icdi n \<pi>))]; \<not> ?P1 \<pi> n\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> n = map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> n]
[PROOF STEP]
hence \<open>\<forall> x \<in> set (sorted_list_of_set {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}). x < j\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>{i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}. x < j

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

goal (2 subgoals):
 1. \<And>\<pi> n. \<lbrakk>Ex (is_icdi n \<pi>) \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> The (is_icdi n \<pi>) = map \<pi> (sorted_list_of_set {i. The (is_icdi n \<pi>) cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> (The (is_icdi n \<pi>))]; ?P1 \<pi> n\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> n = map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> n]
 2. \<And>\<pi> n. \<lbrakk>Ex (is_icdi n \<pi>) \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> The (is_icdi n \<pi>) = map \<pi> (sorted_list_of_set {i. The (is_icdi n \<pi>) cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> (The (is_icdi n \<pi>))]; \<not> ?P1 \<pi> n\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> n = map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> n]
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
sorted_list_of_set {i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} = insort j (sorted_list_of_set {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i})
\<forall>x\<in>set (sorted_list_of_set {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}). x < j
[PROOF STEP]
have \<open>sorted_list_of_set { i . k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} = (sorted_list_of_set { i . j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i})@[j]\<close>
[PROOF STATE]
proof (prove)
using this:
sorted_list_of_set {i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} = insort j (sorted_list_of_set {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i})
\<forall>x\<in>set (sorted_list_of_set {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}). x < j

goal (1 subgoal):
 1. sorted_list_of_set {i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} = sorted_list_of_set {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} @ [j]
[PROOF STEP]
using insort_greater
[PROOF STATE]
proof (prove)
using this:
sorted_list_of_set {i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} = insort j (sorted_list_of_set {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i})
\<forall>x\<in>set (sorted_list_of_set {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}). x < j
\<forall>x\<in>set ?ls. x < ?y \<Longrightarrow> insort ?y ?ls = ?ls @ [?y]

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

goal (2 subgoals):
 1. \<And>\<pi> n. \<lbrakk>Ex (is_icdi n \<pi>) \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> The (is_icdi n \<pi>) = map \<pi> (sorted_list_of_set {i. The (is_icdi n \<pi>) cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> (The (is_icdi n \<pi>))]; ?P1 \<pi> n\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> n = map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> n]
 2. \<And>\<pi> n. \<lbrakk>Ex (is_icdi n \<pi>) \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> The (is_icdi n \<pi>) = map \<pi> (sorted_list_of_set {i. The (is_icdi n \<pi>) cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> (The (is_icdi n \<pi>))]; \<not> ?P1 \<pi> n\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> n = map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> n]
[PROOF STEP]
hence \<open>cs\<^bsup>\<pi>\<^esup> j = map \<pi> (sorted_list_of_set { i . k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i})\<close>
[PROOF STATE]
proof (prove)
using this:
sorted_list_of_set {i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} = sorted_list_of_set {i. j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} @ [j]

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

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

goal (2 subgoals):
 1. \<And>\<pi> n. \<lbrakk>Ex (is_icdi n \<pi>) \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> The (is_icdi n \<pi>) = map \<pi> (sorted_list_of_set {i. The (is_icdi n \<pi>) cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> (The (is_icdi n \<pi>))]; ?P1 \<pi> n\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> n = map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> n]
 2. \<And>\<pi> n. \<lbrakk>Ex (is_icdi n \<pi>) \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> The (is_icdi n \<pi>) = map \<pi> (sorted_list_of_set {i. The (is_icdi n \<pi>) cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> (The (is_icdi n \<pi>))]; \<not> ?P1 \<pi> n\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> n = map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> n]
[PROOF STEP]
thus \<open>?case\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> j = map \<pi> (sorted_list_of_set {i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i})

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> k = map \<pi> (sorted_list_of_set {i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> k]
[PROOF STEP]
by (metis icd_cs j)
[PROOF STATE]
proof (state)
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. \<And>\<pi> n. \<lbrakk>Ex (is_icdi n \<pi>) \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> The (is_icdi n \<pi>) = map \<pi> (sorted_list_of_set {i. The (is_icdi n \<pi>) cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> (The (is_icdi n \<pi>))]; \<nexists>j. n icd\<^bsup>\<pi>\<^esup>\<rightarrow> j\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> n = map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> n]
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<pi> n. \<lbrakk>Ex (is_icdi n \<pi>) \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> The (is_icdi n \<pi>) = map \<pi> (sorted_list_of_set {i. The (is_icdi n \<pi>) cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> (The (is_icdi n \<pi>))]; \<nexists>j. n icd\<^bsup>\<pi>\<^esup>\<rightarrow> j\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> n = map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> n]
[PROOF STEP]
case (1 \<pi> k)
[PROOF STATE]
proof (state)
this:
Ex (is_icdi k \<pi>) \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> The (is_icdi k \<pi>) = map \<pi> (sorted_list_of_set {i. The (is_icdi k \<pi>) cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> (The (is_icdi k \<pi>))]

goal (1 subgoal):
 1. \<And>\<pi> n. \<lbrakk>Ex (is_icdi n \<pi>) \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> The (is_icdi n \<pi>) = map \<pi> (sorted_list_of_set {i. The (is_icdi n \<pi>) cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> (The (is_icdi n \<pi>))]; \<nexists>j. n icd\<^bsup>\<pi>\<^esup>\<rightarrow> j\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> n = map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> n]
[PROOF STEP]
assume *: \<open>\<not> (\<exists> j. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> j)\<close>
[PROOF STATE]
proof (state)
this:
\<nexists>j. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> j

goal (1 subgoal):
 1. \<And>\<pi> n. \<lbrakk>Ex (is_icdi n \<pi>) \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> The (is_icdi n \<pi>) = map \<pi> (sorted_list_of_set {i. The (is_icdi n \<pi>) cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> (The (is_icdi n \<pi>))]; \<nexists>j. n icd\<^bsup>\<pi>\<^esup>\<rightarrow> j\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> n = map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> n]
[PROOF STEP]
hence \<open>cs\<^bsup>\<pi>\<^esup> k = [\<pi> k]\<close>
[PROOF STATE]
proof (prove)
using this:
\<nexists>j. k icd\<^bsup>\<pi>\<^esup>\<rightarrow> j

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

goal (1 subgoal):
 1. \<And>\<pi> n. \<lbrakk>Ex (is_icdi n \<pi>) \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> The (is_icdi n \<pi>) = map \<pi> (sorted_list_of_set {i. The (is_icdi n \<pi>) cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> (The (is_icdi n \<pi>))]; \<nexists>j. n icd\<^bsup>\<pi>\<^esup>\<rightarrow> j\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> n = map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> n]
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> k = [\<pi> k]

goal (1 subgoal):
 1. \<And>\<pi> n. \<lbrakk>Ex (is_icdi n \<pi>) \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> The (is_icdi n \<pi>) = map \<pi> (sorted_list_of_set {i. The (is_icdi n \<pi>) cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> (The (is_icdi n \<pi>))]; \<nexists>j. n icd\<^bsup>\<pi>\<^esup>\<rightarrow> j\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> n = map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> n]
[PROOF STEP]
have \<open>{ i . k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} = {}\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} = {}
[PROOF STEP]
by (auto, metis * excd_impl_exicd)
[PROOF STATE]
proof (state)
this:
{i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} = {}

goal (1 subgoal):
 1. \<And>\<pi> n. \<lbrakk>Ex (is_icdi n \<pi>) \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> The (is_icdi n \<pi>) = map \<pi> (sorted_list_of_set {i. The (is_icdi n \<pi>) cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> (The (is_icdi n \<pi>))]; \<nexists>j. n icd\<^bsup>\<pi>\<^esup>\<rightarrow> j\<rbrakk> \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> n = map \<pi> (sorted_list_of_set {i. n cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> n]
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
cs\<^bsup>\<pi>\<^esup> k = [\<pi> k]
{i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} = {}
[PROOF STEP]
show \<open>?case\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> k = [\<pi> k]
{i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} = {}

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> k = map \<pi> (sorted_list_of_set {i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> k]
[PROOF STEP]
by (metis append_Nil list.simps(8) sorted_list_of_set_empty)
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> k = map \<pi> (sorted_list_of_set {i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}) @ [\<pi> k]

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cs_sorted_list_of_cd: \<open>cs\<^bsup>\<pi>\<^esup> k = map \<pi> (sorted_list_of_set ({ i . k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {k}))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> k = map \<pi> (sorted_list_of_set ({i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {k}))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> k = map \<pi> (sorted_list_of_set ({i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {k}))
[PROOF STEP]
have le: \<open>\<forall> x \<in> {i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow>i}.\<forall> y \<in> {k}. x < y\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>{i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}. \<forall>y\<in>{k}. x < y
[PROOF STEP]
unfolding is_cdi_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>{i. is_path \<pi> \<and> i < k \<and> \<pi> k \<noteq> local.return \<and> (\<forall>j\<in>{i..k}. \<pi> j \<noteq> ipd (\<pi> i))}. \<forall>y\<in>{k}. x < y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>{i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}. \<forall>y\<in>{k}. x < y

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> k = map \<pi> (sorted_list_of_set ({i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {k}))
[PROOF STEP]
have fin: \<open>finite {i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow>i}\<close> \<open>finite {k}\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} &&& finite {k}
[PROOF STEP]
unfolding is_cdi_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {i. is_path \<pi> \<and> i < k \<and> \<pi> k \<noteq> local.return \<and> (\<forall>j\<in>{i..k}. \<pi> j \<noteq> ipd (\<pi> i))} &&& finite {k}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite {i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}
finite {k}

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> k = map \<pi> (sorted_list_of_set ({i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {k}))
[PROOF STEP]
show \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> k = map \<pi> (sorted_list_of_set ({i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {k}))
[PROOF STEP]
unfolding cs_sorted_list_of_cd'[of \<open>\<pi>\<close> \<open>k\<close>] sorted_list_of_set_append[OF fin le]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map \<pi> (sorted_list_of_set (Collect (is_cdi k \<pi>))) @ [\<pi> k] = map \<pi> (sorted_list_of_set (Collect (is_cdi k \<pi>)) @ sorted_list_of_set {k})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> k = map \<pi> (sorted_list_of_set ({i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {k}))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cs_not_ipd: assumes \<open>k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k)\<close> (is \<open>?Q j\<close>)
shows \<open>cs\<^bsup>\<pi>\<^esup> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k)) = [n\<leftarrow>cs\<^bsup>\<pi>\<^esup> k . ipd n \<noteq> ipd (\<pi> k)]\<close>
(is \<open>cs\<^bsup>\<pi>\<^esup> ?j = filter ?P _\<close>)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k)) = filter (\<lambda>n. ipd n \<noteq> ipd (\<pi> k)) (cs\<^bsup>\<pi>\<^esup> k)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k)) = filter (\<lambda>n. ipd n \<noteq> ipd (\<pi> k)) (cs\<^bsup>\<pi>\<^esup> k)
[PROOF STEP]
have csk: \<open>cs\<^bsup>\<pi>\<^esup> k = map \<pi> (sorted_list_of_set ({ i . k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i } \<union> {k}))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> k = map \<pi> (sorted_list_of_set ({i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {k}))
[PROOF STEP]
by (metis cs_sorted_list_of_cd)
[PROOF STATE]
proof (state)
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. cs\<^bsup>\<pi>\<^esup> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k)) = filter (\<lambda>n. ipd n \<noteq> ipd (\<pi> k)) (cs\<^bsup>\<pi>\<^esup> k)
[PROOF STEP]
have csj: \<open>cs\<^bsup>\<pi>\<^esup> ?j = map \<pi> (sorted_list_of_set ({i. ?j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i } \<union> {?j}))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k)) = map \<pi> (sorted_list_of_set ({i. (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k)) cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k)}))
[PROOF STEP]
by (metis cs_sorted_list_of_cd)
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k)) = map \<pi> (sorted_list_of_set ({i. (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k)) cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k)}))

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k)) = filter (\<lambda>n. ipd n \<noteq> ipd (\<pi> k)) (cs\<^bsup>\<pi>\<^esup> k)
[PROOF STEP]
have bound: \<open>\<forall> j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd(\<pi> k) \<longrightarrow> j \<le> k\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k) \<longrightarrow> j \<le> k
[PROOF STEP]
unfolding is_cdi_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>j. (is_path \<pi> \<and> j < k \<and> \<pi> k \<noteq> local.return \<and> (\<forall>ja\<in>{j..k}. \<pi> ja \<noteq> ipd (\<pi> j))) \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k) \<longrightarrow> j \<le> k
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k) \<longrightarrow> j \<le> k

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k)) = filter (\<lambda>n. ipd n \<noteq> ipd (\<pi> k)) (cs\<^bsup>\<pi>\<^esup> k)
[PROOF STEP]
have kcdj: \<open>k cd\<^bsup>\<pi>\<^esup>\<rightarrow> ?j\<close> and ipd': \<open>ipd (\<pi> ?j) \<noteq> ipd(\<pi> k)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k)) &&& ipd (\<pi> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k))) \<noteq> ipd (\<pi> k)
[PROOF STEP]
using GreatestI_nat[of \<open>?Q\<close> \<open>j\<close> \<open>k\<close>, OF assms] bound
[PROOF STATE]
proof (prove)
using this:
(\<And>y. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> y \<and> ipd (\<pi> y) \<noteq> ipd (\<pi> k) \<Longrightarrow> y \<le> k) \<Longrightarrow> k cd\<^bsup>\<pi>\<^esup>\<rightarrow> (GREATEST a. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> a \<and> ipd (\<pi> a) \<noteq> ipd (\<pi> k)) \<and> ipd (\<pi> (GREATEST a. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> a \<and> ipd (\<pi> a) \<noteq> ipd (\<pi> k))) \<noteq> ipd (\<pi> k)
\<forall>j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k) \<longrightarrow> j \<le> k

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

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k)) = filter (\<lambda>n. ipd n \<noteq> ipd (\<pi> k)) (cs\<^bsup>\<pi>\<^esup> k)
[PROOF STEP]
have greatest: \<open>\<And> j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<Longrightarrow> ipd (\<pi> j) \<noteq> ipd (\<pi> k) \<Longrightarrow> j \<le> ?j\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j; ipd (\<pi> j) \<noteq> ipd (\<pi> k)\<rbrakk> \<Longrightarrow> j \<le> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k))
[PROOF STEP]
using Greatest_le_nat[of \<open>?Q\<close>  _ \<open>k\<close>] bound
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>k cd\<^bsup>\<pi>\<^esup>\<rightarrow> ?k \<and> ipd (\<pi> ?k) \<noteq> ipd (\<pi> k); \<And>y. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> y \<and> ipd (\<pi> y) \<noteq> ipd (\<pi> k) \<Longrightarrow> y \<le> k\<rbrakk> \<Longrightarrow> ?k \<le> (GREATEST a. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> a \<and> ipd (\<pi> a) \<noteq> ipd (\<pi> k))
\<forall>j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k) \<longrightarrow> j \<le> k

goal (1 subgoal):
 1. \<And>j. \<lbrakk>k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j; ipd (\<pi> j) \<noteq> ipd (\<pi> k)\<rbrakk> \<Longrightarrow> j \<le> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>k cd\<^bsup>\<pi>\<^esup>\<rightarrow> ?j1; ipd (\<pi> ?j1) \<noteq> ipd (\<pi> k)\<rbrakk> \<Longrightarrow> ?j1 \<le> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k))

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k)) = filter (\<lambda>n. ipd n \<noteq> ipd (\<pi> k)) (cs\<^bsup>\<pi>\<^esup> k)
[PROOF STEP]
have less_not_ipdk: \<open>\<And> j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<Longrightarrow> j < ?j \<Longrightarrow> ipd (\<pi> j) \<noteq> ipd (\<pi> k)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j; j < (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k))\<rbrakk> \<Longrightarrow> ipd (\<pi> j) \<noteq> ipd (\<pi> k)
[PROOF STEP]
by (metis (lifting) ipd' kcdj same_ipd_stable)
[PROOF STATE]
proof (state)
this:
\<lbrakk>k cd\<^bsup>\<pi>\<^esup>\<rightarrow> ?j1; ?j1 < (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k))\<rbrakk> \<Longrightarrow> ipd (\<pi> ?j1) \<noteq> ipd (\<pi> k)

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k)) = filter (\<lambda>n. ipd n \<noteq> ipd (\<pi> k)) (cs\<^bsup>\<pi>\<^esup> k)
[PROOF STEP]
hence le_not_ipdk: \<open>\<And> j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<Longrightarrow> j \<le> ?j \<Longrightarrow> ipd (\<pi> j) \<noteq> ipd (\<pi> k)\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>k cd\<^bsup>\<pi>\<^esup>\<rightarrow> ?j1; ?j1 < (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k))\<rbrakk> \<Longrightarrow> ipd (\<pi> ?j1) \<noteq> ipd (\<pi> k)

goal (1 subgoal):
 1. \<And>j. \<lbrakk>k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j; j \<le> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k))\<rbrakk> \<Longrightarrow> ipd (\<pi> j) \<noteq> ipd (\<pi> k)
[PROOF STEP]
using kcdj ipd'
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>k cd\<^bsup>\<pi>\<^esup>\<rightarrow> ?j1; ?j1 < (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k))\<rbrakk> \<Longrightarrow> ipd (\<pi> ?j1) \<noteq> ipd (\<pi> k)
k cd\<^bsup>\<pi>\<^esup>\<rightarrow> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k))
ipd (\<pi> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k))) \<noteq> ipd (\<pi> k)

goal (1 subgoal):
 1. \<And>j. \<lbrakk>k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j; j \<le> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k))\<rbrakk> \<Longrightarrow> ipd (\<pi> j) \<noteq> ipd (\<pi> k)
[PROOF STEP]
by (case_tac \<open>j = ?j\<close>,auto)
[PROOF STATE]
proof (state)
this:
\<lbrakk>k cd\<^bsup>\<pi>\<^esup>\<rightarrow> ?j1; ?j1 \<le> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k))\<rbrakk> \<Longrightarrow> ipd (\<pi> ?j1) \<noteq> ipd (\<pi> k)

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k)) = filter (\<lambda>n. ipd n \<noteq> ipd (\<pi> k)) (cs\<^bsup>\<pi>\<^esup> k)
[PROOF STEP]
have *: \<open>{j \<in> {i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow>i} \<union> {k}. ?P (\<pi> j)} = insert ?j { i . ?j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {j \<in> {i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {k}. ipd (\<pi> j) \<noteq> ipd (\<pi> k)} = insert (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k)) {i. (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k)) cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x. \<lbrakk>x \<noteq> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k)); ipd (\<pi> x) \<noteq> ipd (\<pi> k); k cd\<^bsup>\<pi>\<^esup>\<rightarrow> x\<rbrakk> \<Longrightarrow> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k)) cd\<^bsup>\<pi>\<^esup>\<rightarrow> x
 2. \<not> k cd\<^bsup>\<pi>\<^esup>\<rightarrow> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k)) \<Longrightarrow> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k)) = k
 3. ipd (\<pi> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k))) = ipd (\<pi> k) \<Longrightarrow> False
 4. \<And>x. \<lbrakk>(GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k)) cd\<^bsup>\<pi>\<^esup>\<rightarrow> x; \<not> k cd\<^bsup>\<pi>\<^esup>\<rightarrow> x\<rbrakk> \<Longrightarrow> x = k
 5. \<And>x. \<lbrakk>(GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k)) cd\<^bsup>\<pi>\<^esup>\<rightarrow> x; ipd (\<pi> x) = ipd (\<pi> k)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (metis (lifting, no_types) greatest cr_wn'' kcdj le_antisym le_refl)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<not> k cd\<^bsup>\<pi>\<^esup>\<rightarrow> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k)) \<Longrightarrow> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k)) = k
 2. ipd (\<pi> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k))) = ipd (\<pi> k) \<Longrightarrow> False
 3. \<And>x. \<lbrakk>(GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k)) cd\<^bsup>\<pi>\<^esup>\<rightarrow> x; \<not> k cd\<^bsup>\<pi>\<^esup>\<rightarrow> x\<rbrakk> \<Longrightarrow> x = k
 4. \<And>x. \<lbrakk>(GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k)) cd\<^bsup>\<pi>\<^esup>\<rightarrow> x; ipd (\<pi> x) = ipd (\<pi> k)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (metis kcdj)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. ipd (\<pi> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k))) = ipd (\<pi> k) \<Longrightarrow> False
 2. \<And>x. \<lbrakk>(GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k)) cd\<^bsup>\<pi>\<^esup>\<rightarrow> x; \<not> k cd\<^bsup>\<pi>\<^esup>\<rightarrow> x\<rbrakk> \<Longrightarrow> x = k
 3. \<And>x. \<lbrakk>(GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k)) cd\<^bsup>\<pi>\<^esup>\<rightarrow> x; ipd (\<pi> x) = ipd (\<pi> k)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (metis ipd')
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>(GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k)) cd\<^bsup>\<pi>\<^esup>\<rightarrow> x; \<not> k cd\<^bsup>\<pi>\<^esup>\<rightarrow> x\<rbrakk> \<Longrightarrow> x = k
 2. \<And>x. \<lbrakk>(GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k)) cd\<^bsup>\<pi>\<^esup>\<rightarrow> x; ipd (\<pi> x) = ipd (\<pi> k)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (metis (full_types) cd_trans kcdj)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>(GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k)) cd\<^bsup>\<pi>\<^esup>\<rightarrow> x; ipd (\<pi> x) = ipd (\<pi> k)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (subgoal_tac \<open>k cd\<^bsup>\<pi>\<^esup>\<rightarrow> x\<close>)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>(GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k)) cd\<^bsup>\<pi>\<^esup>\<rightarrow> x; ipd (\<pi> x) = ipd (\<pi> k); k cd\<^bsup>\<pi>\<^esup>\<rightarrow> x\<rbrakk> \<Longrightarrow> False
 2. \<And>x. \<lbrakk>(GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k)) cd\<^bsup>\<pi>\<^esup>\<rightarrow> x; ipd (\<pi> x) = ipd (\<pi> k)\<rbrakk> \<Longrightarrow> k cd\<^bsup>\<pi>\<^esup>\<rightarrow> x
[PROOF STEP]
apply (metis (lifting, no_types) is_cdi_def less_not_ipdk)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>(GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k)) cd\<^bsup>\<pi>\<^esup>\<rightarrow> x; ipd (\<pi> x) = ipd (\<pi> k)\<rbrakk> \<Longrightarrow> k cd\<^bsup>\<pi>\<^esup>\<rightarrow> x
[PROOF STEP]
by (metis (full_types) cd_trans kcdj)
[PROOF STATE]
proof (state)
this:
{j \<in> {i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {k}. ipd (\<pi> j) \<noteq> ipd (\<pi> k)} = insert (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k)) {i. (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k)) cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k)) = filter (\<lambda>n. ipd n \<noteq> ipd (\<pi> k)) (cs\<^bsup>\<pi>\<^esup> k)
[PROOF STEP]
have \<open>finite ({i . k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {k})\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite ({i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {k})
[PROOF STEP]
unfolding is_cdi_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite ({i. is_path \<pi> \<and> i < k \<and> \<pi> k \<noteq> local.return \<and> (\<forall>j\<in>{i..k}. \<pi> j \<noteq> ipd (\<pi> i))} \<union> {k})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite ({i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {k})

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k)) = filter (\<lambda>n. ipd n \<noteq> ipd (\<pi> k)) (cs\<^bsup>\<pi>\<^esup> k)
[PROOF STEP]
note filter_sorted_list_of_set[OF this, of \<open>?P o \<pi>\<close>]
[PROOF STATE]
proof (state)
this:
filter ((\<lambda>n. ipd n \<noteq> ipd (\<pi> k)) \<circ> \<pi>) (sorted_list_of_set ({i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {k})) = sorted_list_of_set {x \<in> {i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {k}. ((\<lambda>n. ipd n \<noteq> ipd (\<pi> k)) \<circ> \<pi>) x}

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k)) = filter (\<lambda>n. ipd n \<noteq> ipd (\<pi> k)) (cs\<^bsup>\<pi>\<^esup> k)
[PROOF STEP]
hence \<open>[n\<leftarrow>cs\<^bsup>\<pi>\<^esup> k . ipd n \<noteq> ipd(\<pi> k)] = map \<pi> (sorted_list_of_set {j \<in> {i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow>i} \<union> {k}. ?P (\<pi> j)})\<close>
[PROOF STATE]
proof (prove)
using this:
filter ((\<lambda>n. ipd n \<noteq> ipd (\<pi> k)) \<circ> \<pi>) (sorted_list_of_set ({i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {k})) = sorted_list_of_set {x \<in> {i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {k}. ((\<lambda>n. ipd n \<noteq> ipd (\<pi> k)) \<circ> \<pi>) x}

goal (1 subgoal):
 1. filter (\<lambda>n. ipd n \<noteq> ipd (\<pi> k)) (cs\<^bsup>\<pi>\<^esup> k) = map \<pi> (sorted_list_of_set {j \<in> {i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {k}. ipd (\<pi> j) \<noteq> ipd (\<pi> k)})
[PROOF STEP]
unfolding csk filter_map
[PROOF STATE]
proof (prove)
using this:
filter ((\<lambda>n. ipd n \<noteq> ipd (\<pi> k)) \<circ> \<pi>) (sorted_list_of_set ({i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {k})) = sorted_list_of_set {x \<in> {i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {k}. ((\<lambda>n. ipd n \<noteq> ipd (\<pi> k)) \<circ> \<pi>) x}

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

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k)) = filter (\<lambda>n. ipd n \<noteq> ipd (\<pi> k)) (cs\<^bsup>\<pi>\<^esup> k)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
filter (\<lambda>n. ipd n \<noteq> ipd (\<pi> k)) (cs\<^bsup>\<pi>\<^esup> k) = map \<pi> (sorted_list_of_set {j \<in> {i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {k}. ipd (\<pi> j) \<noteq> ipd (\<pi> k)})

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k)) = filter (\<lambda>n. ipd n \<noteq> ipd (\<pi> k)) (cs\<^bsup>\<pi>\<^esup> k)
[PROOF STEP]
have \<open>\<dots> =  map \<pi> (sorted_list_of_set (insert ?j { i . ?j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map \<pi> (sorted_list_of_set {j \<in> {i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {k}. ipd (\<pi> j) \<noteq> ipd (\<pi> k)}) = map \<pi> (sorted_list_of_set (insert (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k)) {i. (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k)) cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}))
[PROOF STEP]
unfolding *
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map \<pi> (sorted_list_of_set (insert (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k)) (Collect (is_cdi (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k)) \<pi>)))) = map \<pi> (sorted_list_of_set (insert (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k)) {i. (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k)) cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
map \<pi> (sorted_list_of_set {j \<in> {i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {k}. ipd (\<pi> j) \<noteq> ipd (\<pi> k)}) = map \<pi> (sorted_list_of_set (insert (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k)) {i. (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k)) cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}))

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k)) = filter (\<lambda>n. ipd n \<noteq> ipd (\<pi> k)) (cs\<^bsup>\<pi>\<^esup> k)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
map \<pi> (sorted_list_of_set {j \<in> {i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {k}. ipd (\<pi> j) \<noteq> ipd (\<pi> k)}) = map \<pi> (sorted_list_of_set (insert (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k)) {i. (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k)) cd\<^bsup>\<pi>\<^esup>\<rightarrow> i}))

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k)) = filter (\<lambda>n. ipd n \<noteq> ipd (\<pi> k)) (cs\<^bsup>\<pi>\<^esup> k)
[PROOF STEP]
have \<open>\<dots> = cs\<^bsup>\<pi>\<^esup> ?j\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map \<pi> (sorted_list_of_set (insert (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k)) {i. (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k)) cd\<^bsup>\<pi>\<^esup>\<rightarrow> i})) = cs\<^bsup>\<pi>\<^esup> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k))
[PROOF STEP]
using csj
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k)) = map \<pi> (sorted_list_of_set ({i. (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k)) cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k)}))

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

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k)) = filter (\<lambda>n. ipd n \<noteq> ipd (\<pi> k)) (cs\<^bsup>\<pi>\<^esup> k)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
filter (\<lambda>n. ipd n \<noteq> ipd (\<pi> k)) (cs\<^bsup>\<pi>\<^esup> k) = cs\<^bsup>\<pi>\<^esup> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k))
[PROOF STEP]
show \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
filter (\<lambda>n. ipd n \<noteq> ipd (\<pi> k)) (cs\<^bsup>\<pi>\<^esup> k) = cs\<^bsup>\<pi>\<^esup> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k))

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k)) = filter (\<lambda>n. ipd n \<noteq> ipd (\<pi> k)) (cs\<^bsup>\<pi>\<^esup> k)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k)) = filter (\<lambda>n. ipd n \<noteq> ipd (\<pi> k)) (cs\<^bsup>\<pi>\<^esup> k)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cs_ipd: assumes ipd: \<open>\<pi> m = ipd (\<pi> k)\<close> \<open>\<forall> n \<in> {k..<m}. \<pi> n \<noteq> ipd (\<pi> k)\<close>
and km: \<open>k < m\<close> shows \<open>cs\<^bsup>\<pi>\<^esup> m = [n\<leftarrow>cs\<^bsup>\<pi>\<^esup> k . ipd n \<noteq> \<pi> m] @ [\<pi> m]\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> m = filter (\<lambda>n. ipd n \<noteq> \<pi> m) (cs\<^bsup>\<pi>\<^esup> k) @ [\<pi> m]
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> m = filter (\<lambda>n. ipd n \<noteq> \<pi> m) (cs\<^bsup>\<pi>\<^esup> k) @ [\<pi> m]
 2. \<not> ?P \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> m = filter (\<lambda>n. ipd n \<noteq> \<pi> m) (cs\<^bsup>\<pi>\<^esup> k) @ [\<pi> m]
[PROOF STEP]
assume \<open>\<exists> j. m icd\<^bsup>\<pi>\<^esup>\<rightarrow> j\<close>
[PROOF STATE]
proof (state)
this:
\<exists>j. m icd\<^bsup>\<pi>\<^esup>\<rightarrow> j

goal (2 subgoals):
 1. ?P \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> m = filter (\<lambda>n. ipd n \<noteq> \<pi> m) (cs\<^bsup>\<pi>\<^esup> k) @ [\<pi> m]
 2. \<not> ?P \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> m = filter (\<lambda>n. ipd n \<noteq> \<pi> m) (cs\<^bsup>\<pi>\<^esup> k) @ [\<pi> m]
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>j. m icd\<^bsup>\<pi>\<^esup>\<rightarrow> j
[PROOF STEP]
obtain j where jicd: \<open>m icd\<^bsup>\<pi>\<^esup>\<rightarrow> j\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>j. m icd\<^bsup>\<pi>\<^esup>\<rightarrow> j

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> m = filter (\<lambda>n. ipd n \<noteq> \<pi> m) (cs\<^bsup>\<pi>\<^esup> k) @ [\<pi> m]
 2. \<not> ?P \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> m = filter (\<lambda>n. ipd n \<noteq> \<pi> m) (cs\<^bsup>\<pi>\<^esup> k) @ [\<pi> m]
[PROOF STEP]
hence *: \<open>cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>\<^esup> j @ [\<pi> m]\<close>
[PROOF STATE]
proof (prove)
using this:
m icd\<^bsup>\<pi>\<^esup>\<rightarrow> j

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>\<^esup> j @ [\<pi> m]
[PROOF STEP]
by (metis icd_cs)
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>\<^esup> j @ [\<pi> m]

goal (2 subgoals):
 1. ?P \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> m = filter (\<lambda>n. ipd n \<noteq> \<pi> m) (cs\<^bsup>\<pi>\<^esup> k) @ [\<pi> m]
 2. \<not> ?P \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> m = filter (\<lambda>n. ipd n \<noteq> \<pi> m) (cs\<^bsup>\<pi>\<^esup> k) @ [\<pi> m]
[PROOF STEP]
have j: \<open>j = (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j = (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m)
[PROOF STEP]
using jicd assms ipd_icd_greatest_cd_not_ipd
[PROOF STATE]
proof (prove)
using this:
m icd\<^bsup>\<pi>\<^esup>\<rightarrow> j
\<pi> m = ipd (\<pi> k)
\<forall>n\<in>{k..<m}. \<pi> n \<noteq> ipd (\<pi> k)
k < m
\<lbrakk>?\<pi> ?m = ipd (?\<pi> ?k); \<forall>n\<in>{?k..<?m}. ?\<pi> n \<noteq> ipd (?\<pi> ?k); ?k < ?m; ?m icd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?j\<rbrakk> \<Longrightarrow> ?j = (GREATEST j. ?k cd\<^bsup>?\<pi>\<^esup>\<rightarrow> j \<and> ipd (?\<pi> j) \<noteq> ?\<pi> ?m)

goal (1 subgoal):
 1. j = (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
j = (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m)

goal (2 subgoals):
 1. ?P \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> m = filter (\<lambda>n. ipd n \<noteq> \<pi> m) (cs\<^bsup>\<pi>\<^esup> k) @ [\<pi> m]
 2. \<not> ?P \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> m = filter (\<lambda>n. ipd n \<noteq> \<pi> m) (cs\<^bsup>\<pi>\<^esup> k) @ [\<pi> m]
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
j = (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m)

goal (2 subgoals):
 1. ?P \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> m = filter (\<lambda>n. ipd n \<noteq> \<pi> m) (cs\<^bsup>\<pi>\<^esup> k) @ [\<pi> m]
 2. \<not> ?P \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> m = filter (\<lambda>n. ipd n \<noteq> \<pi> m) (cs\<^bsup>\<pi>\<^esup> k) @ [\<pi> m]
[PROOF STEP]
have \<open>ipd (\<pi> j) \<noteq> ipd (\<pi> k)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ipd (\<pi> j) \<noteq> ipd (\<pi> k)
[PROOF STEP]
by (metis is_cdi_def is_icdi_def is_ipd_def cd_not_pd ipd(1) ipd_is_ipd jicd path_nodes less_imp_le term_path_stable)
[PROOF STATE]
proof (state)
this:
ipd (\<pi> j) \<noteq> ipd (\<pi> k)

goal (2 subgoals):
 1. ?P \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> m = filter (\<lambda>n. ipd n \<noteq> \<pi> m) (cs\<^bsup>\<pi>\<^esup> k) @ [\<pi> m]
 2. \<not> ?P \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> m = filter (\<lambda>n. ipd n \<noteq> \<pi> m) (cs\<^bsup>\<pi>\<^esup> k) @ [\<pi> m]
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ipd (\<pi> j) \<noteq> ipd (\<pi> k)

goal (2 subgoals):
 1. ?P \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> m = filter (\<lambda>n. ipd n \<noteq> \<pi> m) (cs\<^bsup>\<pi>\<^esup> k) @ [\<pi> m]
 2. \<not> ?P \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> m = filter (\<lambda>n. ipd n \<noteq> \<pi> m) (cs\<^bsup>\<pi>\<^esup> k) @ [\<pi> m]
[PROOF STEP]
have \<open>k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j
[PROOF STEP]
unfolding j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m)
[PROOF STEP]
by (metis (lifting, no_types) assms(3) cd_ipd_is_cd icd_imp_cd ipd(1) ipd(2) j jicd)
[PROOF STATE]
proof (state)
this:
k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j

goal (2 subgoals):
 1. ?P \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> m = filter (\<lambda>n. ipd n \<noteq> \<pi> m) (cs\<^bsup>\<pi>\<^esup> k) @ [\<pi> m]
 2. \<not> ?P \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> m = filter (\<lambda>n. ipd n \<noteq> \<pi> m) (cs\<^bsup>\<pi>\<^esup> k) @ [\<pi> m]
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
j = (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m)
ipd (\<pi> j) \<noteq> ipd (\<pi> k)
k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j
[PROOF STEP]
have \<open>cs\<^bsup>\<pi>\<^esup> j = [n\<leftarrow>cs\<^bsup>\<pi>\<^esup> k . ipd n \<noteq> \<pi> m]\<close>
[PROOF STATE]
proof (prove)
using this:
j = (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m)
ipd (\<pi> j) \<noteq> ipd (\<pi> k)
k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> j = filter (\<lambda>n. ipd n \<noteq> \<pi> m) (cs\<^bsup>\<pi>\<^esup> k)
[PROOF STEP]
using cs_not_ipd[of \<open>k\<close> \<open>\<pi>\<close> \<open>j\<close>] ipd(1)
[PROOF STATE]
proof (prove)
using this:
j = (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> \<pi> m)
ipd (\<pi> j) \<noteq> ipd (\<pi> k)
k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j
k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k) \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> (GREATEST j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<and> ipd (\<pi> j) \<noteq> ipd (\<pi> k)) = filter (\<lambda>n. ipd n \<noteq> ipd (\<pi> k)) (cs\<^bsup>\<pi>\<^esup> k)
\<pi> m = ipd (\<pi> k)

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> j = filter (\<lambda>n. ipd n \<noteq> \<pi> m) (cs\<^bsup>\<pi>\<^esup> k)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> j = filter (\<lambda>n. ipd n \<noteq> \<pi> m) (cs\<^bsup>\<pi>\<^esup> k)

goal (2 subgoals):
 1. ?P \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> m = filter (\<lambda>n. ipd n \<noteq> \<pi> m) (cs\<^bsup>\<pi>\<^esup> k) @ [\<pi> m]
 2. \<not> ?P \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> m = filter (\<lambda>n. ipd n \<noteq> \<pi> m) (cs\<^bsup>\<pi>\<^esup> k) @ [\<pi> m]
[PROOF STEP]
thus \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> j = filter (\<lambda>n. ipd n \<noteq> \<pi> m) (cs\<^bsup>\<pi>\<^esup> k)

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> m = filter (\<lambda>n. ipd n \<noteq> \<pi> m) (cs\<^bsup>\<pi>\<^esup> k) @ [\<pi> m]
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> j = filter (\<lambda>n. ipd n \<noteq> \<pi> m) (cs\<^bsup>\<pi>\<^esup> k)
cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>\<^esup> j @ [\<pi> m]

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

goal (1 subgoal):
 1. \<nexists>j. m icd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> m = filter (\<lambda>n. ipd n \<noteq> \<pi> m) (cs\<^bsup>\<pi>\<^esup> k) @ [\<pi> m]
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nexists>j. m icd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> m = filter (\<lambda>n. ipd n \<noteq> \<pi> m) (cs\<^bsup>\<pi>\<^esup> k) @ [\<pi> m]
[PROOF STEP]
assume noicd: \<open>\<not> (\<exists> j. m icd\<^bsup>\<pi>\<^esup>\<rightarrow> j)\<close>
[PROOF STATE]
proof (state)
this:
\<nexists>j. m icd\<^bsup>\<pi>\<^esup>\<rightarrow> j

goal (1 subgoal):
 1. \<nexists>j. m icd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> m = filter (\<lambda>n. ipd n \<noteq> \<pi> m) (cs\<^bsup>\<pi>\<^esup> k) @ [\<pi> m]
[PROOF STEP]
hence csm: \<open>cs\<^bsup>\<pi>\<^esup> m = [\<pi> m]\<close>
[PROOF STATE]
proof (prove)
using this:
\<nexists>j. m icd\<^bsup>\<pi>\<^esup>\<rightarrow> j

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

goal (1 subgoal):
 1. \<nexists>j. m icd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> m = filter (\<lambda>n. ipd n \<noteq> \<pi> m) (cs\<^bsup>\<pi>\<^esup> k) @ [\<pi> m]
[PROOF STEP]
have \<open>\<And>j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow>j \<Longrightarrow> ipd(\<pi> j) = \<pi> m\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<Longrightarrow> ipd (\<pi> j) = \<pi> m
[PROOF STEP]
using cd_is_cd_ipd[OF km ipd]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>k cd\<^bsup>\<pi>\<^esup>\<rightarrow> ?j; ipd (\<pi> ?j) \<noteq> \<pi> m\<rbrakk> \<Longrightarrow> m cd\<^bsup>\<pi>\<^esup>\<rightarrow> ?j

goal (1 subgoal):
 1. \<And>j. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<Longrightarrow> ipd (\<pi> j) = \<pi> m
[PROOF STEP]
by (metis excd_impl_exicd noicd)
[PROOF STATE]
proof (state)
this:
k cd\<^bsup>\<pi>\<^esup>\<rightarrow> ?j1 \<Longrightarrow> ipd (\<pi> ?j1) = \<pi> m

goal (1 subgoal):
 1. \<nexists>j. m icd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> m = filter (\<lambda>n. ipd n \<noteq> \<pi> m) (cs\<^bsup>\<pi>\<^esup> k) @ [\<pi> m]
[PROOF STEP]
hence *: \<open>{j \<in> {i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {k}. ipd (\<pi> j) \<noteq> \<pi> m} = {}\<close>
[PROOF STATE]
proof (prove)
using this:
k cd\<^bsup>\<pi>\<^esup>\<rightarrow> ?j1 \<Longrightarrow> ipd (\<pi> ?j1) = \<pi> m

goal (1 subgoal):
 1. {j \<in> {i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {k}. ipd (\<pi> j) \<noteq> \<pi> m} = {}
[PROOF STEP]
using ipd(1)
[PROOF STATE]
proof (prove)
using this:
k cd\<^bsup>\<pi>\<^esup>\<rightarrow> ?j1 \<Longrightarrow> ipd (\<pi> ?j1) = \<pi> m
\<pi> m = ipd (\<pi> k)

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

goal (1 subgoal):
 1. \<nexists>j. m icd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> m = filter (\<lambda>n. ipd n \<noteq> \<pi> m) (cs\<^bsup>\<pi>\<^esup> k) @ [\<pi> m]
[PROOF STEP]
have **: \<open>((\<lambda>n. ipd n \<noteq> \<pi> m) o \<pi>) = (\<lambda>n. ipd (\<pi> n) \<noteq> \<pi> m)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. ipd n \<noteq> \<pi> m) \<circ> \<pi> = (\<lambda>n. ipd (\<pi> n) \<noteq> \<pi> m)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>n. ipd n \<noteq> \<pi> m) \<circ> \<pi> = (\<lambda>n. ipd (\<pi> n) \<noteq> \<pi> m)

goal (1 subgoal):
 1. \<nexists>j. m icd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> m = filter (\<lambda>n. ipd n \<noteq> \<pi> m) (cs\<^bsup>\<pi>\<^esup> k) @ [\<pi> m]
[PROOF STEP]
have fin: \<open>finite ({i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {k})\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite ({i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {k})
[PROOF STEP]
unfolding is_cdi_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite ({i. is_path \<pi> \<and> i < k \<and> \<pi> k \<noteq> local.return \<and> (\<forall>j\<in>{i..k}. \<pi> j \<noteq> ipd (\<pi> i))} \<union> {k})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite ({i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {k})

goal (1 subgoal):
 1. \<nexists>j. m icd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> m = filter (\<lambda>n. ipd n \<noteq> \<pi> m) (cs\<^bsup>\<pi>\<^esup> k) @ [\<pi> m]
[PROOF STEP]
note csk = cs_sorted_list_of_cd[of \<open>\<pi>\<close> \<open>k\<close>]
[PROOF STATE]
proof (state)
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. \<nexists>j. m icd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> m = filter (\<lambda>n. ipd n \<noteq> \<pi> m) (cs\<^bsup>\<pi>\<^esup> k) @ [\<pi> m]
[PROOF STEP]
hence \<open>[n\<leftarrow>cs\<^bsup>\<pi>\<^esup> k . ipd n \<noteq> \<pi> m] = [n\<leftarrow> (map \<pi> (sorted_list_of_set ({i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {k}))) . ipd n \<noteq> \<pi> m]\<close>
[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. filter (\<lambda>n. ipd n \<noteq> \<pi> m) (cs\<^bsup>\<pi>\<^esup> k) = filter (\<lambda>n. ipd n \<noteq> \<pi> m) (map \<pi> (sorted_list_of_set ({i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {k})))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
filter (\<lambda>n. ipd n \<noteq> \<pi> m) (cs\<^bsup>\<pi>\<^esup> k) = filter (\<lambda>n. ipd n \<noteq> \<pi> m) (map \<pi> (sorted_list_of_set ({i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {k})))

goal (1 subgoal):
 1. \<nexists>j. m icd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> m = filter (\<lambda>n. ipd n \<noteq> \<pi> m) (cs\<^bsup>\<pi>\<^esup> k) @ [\<pi> m]
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
filter (\<lambda>n. ipd n \<noteq> \<pi> m) (cs\<^bsup>\<pi>\<^esup> k) = filter (\<lambda>n. ipd n \<noteq> \<pi> m) (map \<pi> (sorted_list_of_set ({i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {k})))

goal (1 subgoal):
 1. \<nexists>j. m icd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> m = filter (\<lambda>n. ipd n \<noteq> \<pi> m) (cs\<^bsup>\<pi>\<^esup> k) @ [\<pi> m]
[PROOF STEP]
have \<open>\<dots> = map \<pi> [n <- sorted_list_of_set ({i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {k}). ipd (\<pi> n) \<noteq> \<pi> m]\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filter (\<lambda>n. ipd n \<noteq> \<pi> m) (map \<pi> (sorted_list_of_set ({i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {k}))) = map \<pi> (filter (\<lambda>n. ipd (\<pi> n) \<noteq> \<pi> m) (sorted_list_of_set ({i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {k})))
[PROOF STEP]
by (auto simp add: filter_map **)
[PROOF STATE]
proof (state)
this:
filter (\<lambda>n. ipd n \<noteq> \<pi> m) (map \<pi> (sorted_list_of_set ({i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {k}))) = map \<pi> (filter (\<lambda>n. ipd (\<pi> n) \<noteq> \<pi> m) (sorted_list_of_set ({i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {k})))

goal (1 subgoal):
 1. \<nexists>j. m icd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> m = filter (\<lambda>n. ipd n \<noteq> \<pi> m) (cs\<^bsup>\<pi>\<^esup> k) @ [\<pi> m]
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
filter (\<lambda>n. ipd n \<noteq> \<pi> m) (map \<pi> (sorted_list_of_set ({i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {k}))) = map \<pi> (filter (\<lambda>n. ipd (\<pi> n) \<noteq> \<pi> m) (sorted_list_of_set ({i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {k})))

goal (1 subgoal):
 1. \<nexists>j. m icd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> m = filter (\<lambda>n. ipd n \<noteq> \<pi> m) (cs\<^bsup>\<pi>\<^esup> k) @ [\<pi> m]
[PROOF STEP]
have \<open>\<dots> = []\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map \<pi> (filter (\<lambda>n. ipd (\<pi> n) \<noteq> \<pi> m) (sorted_list_of_set ({i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {k}))) = []
[PROOF STEP]
unfolding * filter_sorted_list_of_set[OF fin, of \<open>\<lambda>n. ipd (\<pi> n) \<noteq> \<pi> m\<close>]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map \<pi> (sorted_list_of_set {}) = []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
map \<pi> (filter (\<lambda>n. ipd (\<pi> n) \<noteq> \<pi> m) (sorted_list_of_set ({i. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i} \<union> {k}))) = []

goal (1 subgoal):
 1. \<nexists>j. m icd\<^bsup>\<pi>\<^esup>\<rightarrow> j \<Longrightarrow> cs\<^bsup>\<pi>\<^esup> m = filter (\<lambda>n. ipd n \<noteq> \<pi> m) (cs\<^bsup>\<pi>\<^esup> k) @ [\<pi> m]
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
filter (\<lambda>n. ipd n \<noteq> \<pi> m) (cs\<^bsup>\<pi>\<^esup> k) = []
[PROOF STEP]
show \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
filter (\<lambda>n. ipd n \<noteq> \<pi> m) (cs\<^bsup>\<pi>\<^esup> k) = []

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> m = filter (\<lambda>n. ipd n \<noteq> \<pi> m) (cs\<^bsup>\<pi>\<^esup> k) @ [\<pi> m]
[PROOF STEP]
using csm
[PROOF STATE]
proof (prove)
using this:
filter (\<lambda>n. ipd n \<noteq> \<pi> m) (cs\<^bsup>\<pi>\<^esup> k) = []
cs\<^bsup>\<pi>\<^esup> m = [\<pi> m]

goal (1 subgoal):
 1. cs\<^bsup>\<pi>\<^esup> m = filter (\<lambda>n. ipd n \<noteq> \<pi> m) (cs\<^bsup>\<pi>\<^esup> k) @ [\<pi> m]
[PROOF STEP]
by (metis append_Nil)
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> m = filter (\<lambda>n. ipd n \<noteq> \<pi> m) (cs\<^bsup>\<pi>\<^esup> k) @ [\<pi> m]

goal:
No subgoals!
[PROOF STEP]
qed