[STATEMENT]
lemma path_pd_ipd0: assumes \<open>is_path \<pi>\<close> and \<open>\<pi> 0 \<noteq> return\<close> \<open>\<pi> n \<noteq> \<pi> 0\<close> and \<open>\<pi> n pd\<rightarrow> \<pi> 0\<close>
obtains k where \<open>k \<le> n\<close> and \<open>\<pi> k = ipd(\<pi> 0)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k. \<lbrakk>k \<le> n; \<pi> k = ipd (\<pi> 0)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<And>k. \<lbrakk>k \<le> n; \<pi> k = ipd (\<pi> 0)\<rbrakk> \<Longrightarrow> thesis; ?P3\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>k. \<lbrakk>k \<le> n; \<pi> k = ipd (\<pi> 0)\<rbrakk> \<Longrightarrow> thesis; \<not> ?P3\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
assume *: \<open>\<pi> n = return\<close>
[PROOF STATE]
proof (state)
this:
\<pi> n = local.return

goal (2 subgoals):
 1. \<lbrakk>\<And>k. \<lbrakk>k \<le> n; \<pi> k = ipd (\<pi> 0)\<rbrakk> \<Longrightarrow> thesis; ?P3\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>k. \<lbrakk>k \<le> n; \<pi> k = ipd (\<pi> 0)\<rbrakk> \<Longrightarrow> thesis; \<not> ?P3\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have \<open>ipd (\<pi> 0) pd\<rightarrow> (\<pi> 0)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ipd (\<pi> 0) pd\<rightarrow> \<pi> 0
[PROOF STEP]
by (metis is_ipd_def is_pd_def assms(2,4) ipd_is_ipd)
[PROOF STATE]
proof (state)
this:
ipd (\<pi> 0) pd\<rightarrow> \<pi> 0

goal (2 subgoals):
 1. \<lbrakk>\<And>k. \<lbrakk>k \<le> n; \<pi> k = ipd (\<pi> 0)\<rbrakk> \<Longrightarrow> thesis; ?P3\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>k. \<lbrakk>k \<le> n; \<pi> k = ipd (\<pi> 0)\<rbrakk> \<Longrightarrow> thesis; \<not> ?P3\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
with assms(1,2,3) *
[PROOF STATE]
proof (chain)
picking this:
is_path \<pi>
\<pi> 0 \<noteq> local.return
\<pi> n \<noteq> \<pi> 0
\<pi> n = local.return
ipd (\<pi> 0) pd\<rightarrow> \<pi> 0
[PROOF STEP]
show \<open>thesis\<close>
[PROOF STATE]
proof (prove)
using this:
is_path \<pi>
\<pi> 0 \<noteq> local.return
\<pi> n \<noteq> \<pi> 0
\<pi> n = local.return
ipd (\<pi> 0) pd\<rightarrow> \<pi> 0

goal (1 subgoal):
 1. thesis
[PROOF STEP]
unfolding is_pd_def
[PROOF STATE]
proof (prove)
using this:
is_path \<pi>
\<pi> 0 \<noteq> local.return
\<pi> n \<noteq> \<pi> 0
\<pi> n = local.return
\<pi> 0 \<in> local.nodes \<and> (\<forall>\<pi>' n. is_path \<pi>' \<and> \<pi>' 0 = \<pi> 0 \<and> \<pi>' n = local.return \<longrightarrow> (\<exists>k\<le>n. \<pi>' k = ipd (\<pi> 0)))

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

goal (1 subgoal):
 1. \<lbrakk>\<And>k. \<lbrakk>k \<le> n; \<pi> k = ipd (\<pi> 0)\<rbrakk> \<Longrightarrow> thesis; \<pi> n \<noteq> local.return\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>k. \<lbrakk>k \<le> n; \<pi> k = ipd (\<pi> 0)\<rbrakk> \<Longrightarrow> thesis; \<pi> n \<noteq> local.return\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
assume \<open>\<pi> n \<noteq> return\<close>
[PROOF STATE]
proof (state)
this:
\<pi> n \<noteq> local.return

goal (1 subgoal):
 1. \<lbrakk>\<And>k. \<lbrakk>k \<le> n; \<pi> k = ipd (\<pi> 0)\<rbrakk> \<Longrightarrow> thesis; \<pi> n \<noteq> local.return\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
from path_pd_ipd0' [OF assms(1) this assms(3,4)] that
[PROOF STATE]
proof (chain)
picking this:
(\<And>k. \<lbrakk>k \<le> n; \<pi> k = ipd (\<pi> 0)\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
\<lbrakk>?k1 \<le> n; \<pi> ?k1 = ipd (\<pi> 0)\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
show \<open>thesis\<close>
[PROOF STATE]
proof (prove)
using this:
(\<And>k. \<lbrakk>k \<le> n; \<pi> k = ipd (\<pi> 0)\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
\<lbrakk>?k1 \<le> n; \<pi> ?k1 = ipd (\<pi> 0)\<rbrakk> \<Longrightarrow> thesis

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma path_pd_ipd: assumes \<open>is_path \<pi>\<close> and \<open>\<pi> k \<noteq> return\<close> \<open>\<pi> n \<noteq> \<pi> k\<close> and \<open>\<pi> n pd\<rightarrow> \<pi> k\<close> and kn: \<open>k < n\<close>
obtains l where \<open>k < l\<close> and \<open>l \<le> n\<close> and \<open>\<pi> l = ipd(\<pi> k)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>l. \<lbrakk>k < l; l \<le> n; \<pi> l = ipd (\<pi> k)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>l. \<lbrakk>k < l; l \<le> n; \<pi> l = ipd (\<pi> k)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have \<open>is_path (\<pi> \<guillemotleft> k)\<close> \<open>(\<pi> \<guillemotleft> k) 0 \<noteq> return\<close> \<open>(\<pi> \<guillemotleft> k) (n - k) \<noteq> (\<pi> \<guillemotleft> k) 0\<close> \<open>(\<pi> \<guillemotleft> k) (n - k) pd\<rightarrow> (\<pi> \<guillemotleft> k) 0\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (is_path (\<pi> \<guillemotleft> k) &&& (\<pi> \<guillemotleft> k) 0 \<noteq> local.return) &&& (\<pi> \<guillemotleft> k) (n - k) \<noteq> (\<pi> \<guillemotleft> k) 0 &&& (\<pi> \<guillemotleft> k) (n - k) pd\<rightarrow> (\<pi> \<guillemotleft> k) 0
[PROOF STEP]
using assms path_path_shift
[PROOF STATE]
proof (prove)
using this:
is_path \<pi>
\<pi> k \<noteq> local.return
\<pi> n \<noteq> \<pi> k
\<pi> n pd\<rightarrow> \<pi> k
k < n
is_path ?\<pi> \<Longrightarrow> is_path (?\<pi> \<guillemotleft> ?m)

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

goal (1 subgoal):
 1. (\<And>l. \<lbrakk>k < l; l \<le> n; \<pi> l = ipd (\<pi> k)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with path_pd_ipd0[of \<open>\<pi>\<guillemotleft>k\<close> \<open>n-k\<close>]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>is_path (\<pi> \<guillemotleft> k); (\<pi> \<guillemotleft> k) 0 \<noteq> local.return; (\<pi> \<guillemotleft> k) (n - k) \<noteq> (\<pi> \<guillemotleft> k) 0; (\<pi> \<guillemotleft> k) (n - k) pd\<rightarrow> (\<pi> \<guillemotleft> k) 0; \<And>ka. \<lbrakk>ka \<le> n - k; (\<pi> \<guillemotleft> k) ka = ipd ((\<pi> \<guillemotleft> k) 0)\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
is_path (\<pi> \<guillemotleft> k)
(\<pi> \<guillemotleft> k) 0 \<noteq> local.return
(\<pi> \<guillemotleft> k) (n - k) \<noteq> (\<pi> \<guillemotleft> k) 0
(\<pi> \<guillemotleft> k) (n - k) pd\<rightarrow> (\<pi> \<guillemotleft> k) 0
[PROOF STEP]
obtain ka where \<open>ka \<le> n - k\<close> \<open>(\<pi> \<guillemotleft> k) ka = ipd ((\<pi> \<guillemotleft> k) 0)\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_path (\<pi> \<guillemotleft> k); (\<pi> \<guillemotleft> k) 0 \<noteq> local.return; (\<pi> \<guillemotleft> k) (n - k) \<noteq> (\<pi> \<guillemotleft> k) 0; (\<pi> \<guillemotleft> k) (n - k) pd\<rightarrow> (\<pi> \<guillemotleft> k) 0; \<And>ka. \<lbrakk>ka \<le> n - k; (\<pi> \<guillemotleft> k) ka = ipd ((\<pi> \<guillemotleft> k) 0)\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
is_path (\<pi> \<guillemotleft> k)
(\<pi> \<guillemotleft> k) 0 \<noteq> local.return
(\<pi> \<guillemotleft> k) (n - k) \<noteq> (\<pi> \<guillemotleft> k) 0
(\<pi> \<guillemotleft> k) (n - k) pd\<rightarrow> (\<pi> \<guillemotleft> k) 0

goal (1 subgoal):
 1. (\<And>ka. \<lbrakk>ka \<le> n - k; (\<pi> \<guillemotleft> k) ka = ipd ((\<pi> \<guillemotleft> k) 0)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
ka \<le> n - k
(\<pi> \<guillemotleft> k) ka = ipd ((\<pi> \<guillemotleft> k) 0)

goal (1 subgoal):
 1. (\<And>l. \<lbrakk>k < l; l \<le> n; \<pi> l = ipd (\<pi> k)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
hence \<open>k + ka \<le> n\<close> \<open>\<pi> (k + ka) = ipd (\<pi> k)\<close>
[PROOF STATE]
proof (prove)
using this:
ka \<le> n - k
(\<pi> \<guillemotleft> k) ka = ipd ((\<pi> \<guillemotleft> k) 0)

goal (1 subgoal):
 1. k + ka \<le> n &&& \<pi> (k + ka) = ipd (\<pi> k)
[PROOF STEP]
using kn
[PROOF STATE]
proof (prove)
using this:
ka \<le> n - k
(\<pi> \<guillemotleft> k) ka = ipd ((\<pi> \<guillemotleft> k) 0)
k < n

goal (1 subgoal):
 1. k + ka \<le> n &&& \<pi> (k + ka) = ipd (\<pi> k)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k + ka \<le> n
\<pi> (k + ka) = ipd (\<pi> k)

goal (1 subgoal):
 1. (\<And>l. \<lbrakk>k < l; l \<le> n; \<pi> l = ipd (\<pi> k)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
k + ka \<le> n
\<pi> (k + ka) = ipd (\<pi> k)

goal (1 subgoal):
 1. (\<And>l. \<lbrakk>k < l; l \<le> n; \<pi> l = ipd (\<pi> k)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
hence \<open>\<pi> (k + ka) ipd\<rightarrow> \<pi> k\<close>
[PROOF STATE]
proof (prove)
using this:
k + ka \<le> n
\<pi> (k + ka) = ipd (\<pi> k)

goal (1 subgoal):
 1. \<pi> (k + ka) ipd\<rightarrow> \<pi> k
[PROOF STEP]
by (metis assms(1) assms(2) ipd_is_ipd path_nodes)
[PROOF STATE]
proof (state)
this:
\<pi> (k + ka) ipd\<rightarrow> \<pi> k

goal (1 subgoal):
 1. (\<And>l. \<lbrakk>k < l; l \<le> n; \<pi> l = ipd (\<pi> k)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
hence \<open>k < k + ka\<close>
[PROOF STATE]
proof (prove)
using this:
\<pi> (k + ka) ipd\<rightarrow> \<pi> k

goal (1 subgoal):
 1. k < k + ka
[PROOF STEP]
unfolding is_ipd_def
[PROOF STATE]
proof (prove)
using this:
\<pi> k \<noteq> \<pi> (k + ka) \<and> \<pi> (k + ka) pd\<rightarrow> \<pi> k \<and> (\<forall>z. z \<noteq> \<pi> k \<and> z pd\<rightarrow> \<pi> k \<longrightarrow> z pd\<rightarrow> \<pi> (k + ka))

goal (1 subgoal):
 1. k < k + ka
[PROOF STEP]
by (metis nat_neq_iff not_add_less1)
[PROOF STATE]
proof (state)
this:
k < k + ka

goal (1 subgoal):
 1. (\<And>l. \<lbrakk>k < l; l \<le> n; \<pi> l = ipd (\<pi> k)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
k + ka \<le> n
\<pi> (k + ka) = ipd (\<pi> k)
k < k + ka
[PROOF STEP]
show \<open>thesis\<close>
[PROOF STATE]
proof (prove)
using this:
k + ka \<le> n
\<pi> (k + ka) = ipd (\<pi> k)
k < k + ka

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that[of \<open>k+ka\<close>]
[PROOF STATE]
proof (prove)
using this:
k + ka \<le> n
\<pi> (k + ka) = ipd (\<pi> k)
k < k + ka
\<lbrakk>k < k + ka; k + ka \<le> n; \<pi> (k + ka) = ipd (\<pi> k)\<rbrakk> \<Longrightarrow> thesis

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma path_ret_ipd: assumes \<open>is_path \<pi>\<close> and \<open>\<pi> k \<noteq> return\<close> \<open>\<pi> n = return\<close>
obtains l where \<open>k < l\<close> and \<open>l \<le> n\<close> and \<open>\<pi> l = ipd(\<pi> k)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>l. \<lbrakk>k < l; l \<le> n; \<pi> l = ipd (\<pi> k)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>l. \<lbrakk>k < l; l \<le> n; \<pi> l = ipd (\<pi> k)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have \<open>\<pi> n \<noteq> \<pi> k\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> n \<noteq> \<pi> k
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_path \<pi>
\<pi> k \<noteq> local.return
\<pi> n = local.return

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

goal (1 subgoal):
 1. (\<And>l. \<lbrakk>k < l; l \<le> n; \<pi> l = ipd (\<pi> k)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<pi> n \<noteq> \<pi> k

goal (1 subgoal):
 1. (\<And>l. \<lbrakk>k < l; l \<le> n; \<pi> l = ipd (\<pi> k)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have \<open>k \<le> n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k \<le> n
[PROOF STEP]
apply (rule ccontr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> k \<le> n \<Longrightarrow> False
[PROOF STEP]
using term_path_stable assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_path ?\<pi>; ?\<pi> ?i = local.return; ?i \<le> ?j\<rbrakk> \<Longrightarrow> ?\<pi> ?j = local.return
is_path \<pi>
\<pi> k \<noteq> local.return
\<pi> n = local.return

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

goal (1 subgoal):
 1. (\<And>l. \<lbrakk>k < l; l \<le> n; \<pi> l = ipd (\<pi> k)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
hence \<open>k < n\<close>
[PROOF STATE]
proof (prove)
using this:
k \<le> n

goal (1 subgoal):
 1. k < n
[PROOF STEP]
by (metis assms(2,3) dual_order.order_iff_strict)
[PROOF STATE]
proof (state)
this:
k < n

goal (1 subgoal):
 1. (\<And>l. \<lbrakk>k < l; l \<le> n; \<pi> l = ipd (\<pi> k)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
k < n

goal (1 subgoal):
 1. (\<And>l. \<lbrakk>k < l; l \<le> n; \<pi> l = ipd (\<pi> k)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have \<open>\<pi> n pd\<rightarrow> \<pi> k\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> n pd\<rightarrow> \<pi> k
[PROOF STEP]
by (metis assms(1,3) path_nodes return_pd)
[PROOF STATE]
proof (state)
this:
\<pi> n pd\<rightarrow> \<pi> k

goal (1 subgoal):
 1. (\<And>l. \<lbrakk>k < l; l \<le> n; \<pi> l = ipd (\<pi> k)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<pi> n \<noteq> \<pi> k
k < n
\<pi> n pd\<rightarrow> \<pi> k
[PROOF STEP]
obtain l where \<open>k < l\<close> \<open>l \<le> n\<close> \<open>\<pi> l = ipd (\<pi> k)\<close>
[PROOF STATE]
proof (prove)
using this:
\<pi> n \<noteq> \<pi> k
k < n
\<pi> n pd\<rightarrow> \<pi> k

goal (1 subgoal):
 1. (\<And>l. \<lbrakk>k < l; l \<le> n; \<pi> l = ipd (\<pi> k)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms path_pd_ipd
[PROOF STATE]
proof (prove)
using this:
\<pi> n \<noteq> \<pi> k
k < n
\<pi> n pd\<rightarrow> \<pi> k
is_path \<pi>
\<pi> k \<noteq> local.return
\<pi> n = local.return
\<lbrakk>is_path ?\<pi>; ?\<pi> ?k \<noteq> local.return; ?\<pi> ?n \<noteq> ?\<pi> ?k; ?\<pi> ?n pd\<rightarrow> ?\<pi> ?k; ?k < ?n; \<And>l. \<lbrakk>?k < l; l \<le> ?n; ?\<pi> l = ipd (?\<pi> ?k)\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>l. \<lbrakk>k < l; l \<le> n; \<pi> l = ipd (\<pi> k)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
k < l
l \<le> n
\<pi> l = ipd (\<pi> k)

goal (1 subgoal):
 1. (\<And>l. \<lbrakk>k < l; l \<le> n; \<pi> l = ipd (\<pi> k)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
thus \<open>thesis\<close>
[PROOF STATE]
proof (prove)
using this:
k < l
l \<le> n
\<pi> l = ipd (\<pi> k)

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
k < l
l \<le> n
\<pi> l = ipd (\<pi> k)
\<lbrakk>k < ?l1; ?l1 \<le> n; \<pi> ?l1 = ipd (\<pi> k)\<rbrakk> \<Longrightarrow> thesis

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pd_intro: assumes \<open>l pd\<rightarrow> k\<close> \<open>is_path \<pi>\<close> \<open>\<pi> 0 = k\<close> \<open>\<pi> n = return\<close>
obtains i where \<open>i \<le> n\<close> \<open>\<pi> i = l\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i. \<lbrakk>i \<le> n; \<pi> i = l\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
l pd\<rightarrow> k
is_path \<pi>
\<pi> 0 = k
\<pi> n = local.return

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>i \<le> n; \<pi> i = l\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding is_pd_def
[PROOF STATE]
proof (prove)
using this:
k \<in> local.nodes \<and> (\<forall>\<pi> n. is_path \<pi> \<and> \<pi> 0 = k \<and> \<pi> n = local.return \<longrightarrow> (\<exists>k\<le>n. \<pi> k = l))
is_path \<pi>
\<pi> 0 = k
\<pi> n = local.return

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>i \<le> n; \<pi> i = l\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis


[STATEMENT]
lemma path_pd_pd0: assumes path:  \<open>is_path \<pi>\<close> and lpdn: \<open>\<pi> l pd\<rightarrow> n\<close> and npd0: \<open>n pd\<rightarrow> \<pi> 0\<close>
obtains k where \<open>k \<le> l\<close> \<open>\<pi> k = n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k. \<lbrakk>k \<le> l; \<pi> k = n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>k. \<lbrakk>k \<le> l; \<pi> k = n\<rbrakk> \<Longrightarrow> thesis; \<not> thesis\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume \<open>\<not> thesis\<close>
[PROOF STATE]
proof (state)
this:
\<not> thesis

goal (1 subgoal):
 1. \<lbrakk>\<And>k. \<lbrakk>k \<le> l; \<pi> k = n\<rbrakk> \<Longrightarrow> thesis; \<not> thesis\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence notn: \<open>\<And> k. k \<le> l \<Longrightarrow> \<pi> k \<noteq> n\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> thesis

goal (1 subgoal):
 1. \<And>k. k \<le> l \<Longrightarrow> \<pi> k \<noteq> n
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
\<not> thesis
\<lbrakk>?k1 \<le> l; \<pi> ?k1 = n\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. \<And>k. k \<le> l \<Longrightarrow> \<pi> k \<noteq> n
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
?k1 \<le> l \<Longrightarrow> \<pi> ?k1 \<noteq> n

goal (1 subgoal):
 1. \<lbrakk>\<And>k. \<lbrakk>k \<le> l; \<pi> k = n\<rbrakk> \<Longrightarrow> thesis; \<not> thesis\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have nret: \<open>\<pi> l \<noteq> return\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> l \<noteq> local.return
[PROOF STEP]
by (metis is_pd_def assms(1,3) notn)
[PROOF STATE]
proof (state)
this:
\<pi> l \<noteq> local.return

goal (1 subgoal):
 1. \<lbrakk>\<And>k. \<lbrakk>k \<le> l; \<pi> k = n\<rbrakk> \<Longrightarrow> thesis; \<not> thesis\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
obtain \<pi>' n' where path': \<open>is_path \<pi>'\<close> and \<pi>0': \<open>\<pi>' 0 = \<pi> l\<close> and \<pi>n': \<open>\<pi>' n' = return\<close> and nonepd: \<open>\<forall> i>0. \<not> \<pi> l pd\<rightarrow> \<pi>' i\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<pi>' n'. \<lbrakk>is_path \<pi>'; \<pi>' 0 = \<pi> l; \<pi>' n' = local.return; \<forall>i>0. \<not> \<pi> l pd\<rightarrow> \<pi>' i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using nret path path_nodes ret_path_none_pd
[PROOF STATE]
proof (prove)
using this:
\<pi> l \<noteq> local.return
is_path \<pi>
is_path ?\<pi> \<Longrightarrow> ?\<pi> ?k \<in> local.nodes
\<lbrakk>?x \<in> local.nodes; ?x \<noteq> local.return; \<And>\<pi> n. \<lbrakk>is_path \<pi>; \<pi> 0 = ?x; \<pi> n = local.return; \<forall>i>0. \<not> ?x pd\<rightarrow> \<pi> i\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>\<pi>' n'. \<lbrakk>is_path \<pi>'; \<pi>' 0 = \<pi> l; \<pi>' n' = local.return; \<forall>i>0. \<not> \<pi> l pd\<rightarrow> \<pi>' i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
is_path \<pi>'
\<pi>' 0 = \<pi> l
\<pi>' n' = local.return
\<forall>i>0. \<not> \<pi> l pd\<rightarrow> \<pi>' i

goal (1 subgoal):
 1. \<lbrakk>\<And>k. \<lbrakk>k \<le> l; \<pi> k = n\<rbrakk> \<Longrightarrow> thesis; \<not> thesis\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have \<open>\<pi> l \<noteq> n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> l \<noteq> n
[PROOF STEP]
using notn
[PROOF STATE]
proof (prove)
using this:
?k1 \<le> l \<Longrightarrow> \<pi> ?k1 \<noteq> n

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

goal (1 subgoal):
 1. \<lbrakk>\<And>k. \<lbrakk>k \<le> l; \<pi> k = n\<rbrakk> \<Longrightarrow> thesis; \<not> thesis\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence \<open>\<forall> i. \<pi>' i \<noteq> n\<close>
[PROOF STATE]
proof (prove)
using this:
\<pi> l \<noteq> n

goal (1 subgoal):
 1. \<forall>i. \<pi>' i \<noteq> n
[PROOF STEP]
using nonepd \<pi>0' lpdn
[PROOF STATE]
proof (prove)
using this:
\<pi> l \<noteq> n
\<forall>i>0. \<not> \<pi> l pd\<rightarrow> \<pi>' i
\<pi>' 0 = \<pi> l
\<pi> l pd\<rightarrow> n

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

goal (1 subgoal):
 1. \<lbrakk>\<And>k. \<lbrakk>k \<le> l; \<pi> k = n\<rbrakk> \<Longrightarrow> thesis; \<not> thesis\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence notn': \<open>\<forall> i. (\<pi>@\<^bsup>l\<^esup> \<pi>') i \<noteq> n\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>i. \<pi>' i \<noteq> n

goal (1 subgoal):
 1. \<forall>i. (\<pi> @\<^bsup>l\<^esup> \<pi>') i \<noteq> n
[PROOF STEP]
using notn \<pi>0'
[PROOF STATE]
proof (prove)
using this:
\<forall>i. \<pi>' i \<noteq> n
?k1 \<le> l \<Longrightarrow> \<pi> ?k1 \<noteq> n
\<pi>' 0 = \<pi> l

goal (1 subgoal):
 1. \<forall>i. (\<pi> @\<^bsup>l\<^esup> \<pi>') i \<noteq> n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>i. (\<pi> @\<^bsup>l\<^esup> \<pi>') i \<noteq> n

goal (1 subgoal):
 1. \<lbrakk>\<And>k. \<lbrakk>k \<le> l; \<pi> k = n\<rbrakk> \<Longrightarrow> thesis; \<not> thesis\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have \<open>is_path (\<pi>@\<^bsup>l\<^esup> \<pi>')\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_path (\<pi> @\<^bsup>l\<^esup> \<pi>')
[PROOF STEP]
using path path'
[PROOF STATE]
proof (prove)
using this:
is_path \<pi>
is_path \<pi>'

goal (1 subgoal):
 1. is_path (\<pi> @\<^bsup>l\<^esup> \<pi>')
[PROOF STEP]
by (metis \<pi>0' path_cons)
[PROOF STATE]
proof (state)
this:
is_path (\<pi> @\<^bsup>l\<^esup> \<pi>')

goal (1 subgoal):
 1. \<lbrakk>\<And>k. \<lbrakk>k \<le> l; \<pi> k = n\<rbrakk> \<Longrightarrow> thesis; \<not> thesis\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
is_path (\<pi> @\<^bsup>l\<^esup> \<pi>')

goal (1 subgoal):
 1. \<lbrakk>\<And>k. \<lbrakk>k \<le> l; \<pi> k = n\<rbrakk> \<Longrightarrow> thesis; \<not> thesis\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have \<open>(\<pi>@\<^bsup>l\<^esup> \<pi>') 0 = \<pi> 0\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<pi> @\<^bsup>l\<^esup> \<pi>') 0 = \<pi> 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<pi> @\<^bsup>l\<^esup> \<pi>') 0 = \<pi> 0

goal (1 subgoal):
 1. \<lbrakk>\<And>k. \<lbrakk>k \<le> l; \<pi> k = n\<rbrakk> \<Longrightarrow> thesis; \<not> thesis\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<pi> @\<^bsup>l\<^esup> \<pi>') 0 = \<pi> 0

goal (1 subgoal):
 1. \<lbrakk>\<And>k. \<lbrakk>k \<le> l; \<pi> k = n\<rbrakk> \<Longrightarrow> thesis; \<not> thesis\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have \<open>(\<pi>@\<^bsup>l\<^esup> \<pi>') (n' + l) = return\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<pi> @\<^bsup>l\<^esup> \<pi>') (n' + l) = local.return
[PROOF STEP]
using \<pi>0' \<pi>n'
[PROOF STATE]
proof (prove)
using this:
\<pi>' 0 = \<pi> l
\<pi>' n' = local.return

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

goal (1 subgoal):
 1. \<lbrakk>\<And>k. \<lbrakk>k \<le> l; \<pi> k = n\<rbrakk> \<Longrightarrow> thesis; \<not> thesis\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
is_path (\<pi> @\<^bsup>l\<^esup> \<pi>')
(\<pi> @\<^bsup>l\<^esup> \<pi>') 0 = \<pi> 0
(\<pi> @\<^bsup>l\<^esup> \<pi>') (n' + l) = local.return
[PROOF STEP]
show \<open>False\<close>
[PROOF STATE]
proof (prove)
using this:
is_path (\<pi> @\<^bsup>l\<^esup> \<pi>')
(\<pi> @\<^bsup>l\<^esup> \<pi>') 0 = \<pi> 0
(\<pi> @\<^bsup>l\<^esup> \<pi>') (n' + l) = local.return

goal (1 subgoal):
 1. False
[PROOF STEP]
using notn' npd0
[PROOF STATE]
proof (prove)
using this:
is_path (\<pi> @\<^bsup>l\<^esup> \<pi>')
(\<pi> @\<^bsup>l\<^esup> \<pi>') 0 = \<pi> 0
(\<pi> @\<^bsup>l\<^esup> \<pi>') (n' + l) = local.return
\<forall>i. (\<pi> @\<^bsup>l\<^esup> \<pi>') i \<noteq> n
n pd\<rightarrow> \<pi> 0

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding is_pd_def
[PROOF STATE]
proof (prove)
using this:
is_path (\<pi> @\<^bsup>l\<^esup> \<pi>')
(\<pi> @\<^bsup>l\<^esup> \<pi>') 0 = \<pi> 0
(\<pi> @\<^bsup>l\<^esup> \<pi>') (n' + l) = local.return
\<forall>i. (\<pi> @\<^bsup>l\<^esup> \<pi>') i \<noteq> n
\<pi> 0 \<in> local.nodes \<and> (\<forall>\<pi>' na. is_path \<pi>' \<and> \<pi>' 0 = \<pi> 0 \<and> \<pi>' na = local.return \<longrightarrow> (\<exists>k\<le>na. \<pi>' k = n))

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma icd_imp_cd: \<open>n icd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<Longrightarrow> n cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n icd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<Longrightarrow> n cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
by (metis is_icdi_def)


[STATEMENT]
lemma ipd_impl_not_cd:  assumes \<open>j \<in> {k..i}\<close> and \<open>\<pi> j = ipd (\<pi> k)\<close> shows \<open>\<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
by (metis assms(1) assms(2) is_cdi_def)


[STATEMENT]
lemma cd_not_ret: assumes \<open>i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<close> shows \<open>\<pi> k \<noteq> return\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> k \<noteq> local.return
[PROOF STEP]
by (metis is_cdi_def assms nat_less_le term_path_stable)


[STATEMENT]
lemma cd_path_shift: assumes \<open>j \<le> k\<close> \<open>is_path \<pi> \<close> shows \<open>(i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k) = (i - j cd\<^bsup>\<pi>\<guillemotleft>j\<^esup>\<rightarrow> k-j)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k) = (i - j cd\<^bsup>\<pi> \<guillemotleft> j\<^esup>\<rightarrow> k - j)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<Longrightarrow> i - j cd\<^bsup>\<pi> \<guillemotleft> j\<^esup>\<rightarrow> k - j
 2. i - j cd\<^bsup>\<pi> \<guillemotleft> j\<^esup>\<rightarrow> k - j \<Longrightarrow> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
assume a: \<open>i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close>
[PROOF STATE]
proof (state)
this:
i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k

goal (2 subgoals):
 1. i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<Longrightarrow> i - j cd\<^bsup>\<pi> \<guillemotleft> j\<^esup>\<rightarrow> k - j
 2. i - j cd\<^bsup>\<pi> \<guillemotleft> j\<^esup>\<rightarrow> k - j \<Longrightarrow> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
hence b: \<open>k < i\<close>
[PROOF STATE]
proof (prove)
using this:
i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k

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

goal (2 subgoals):
 1. i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<Longrightarrow> i - j cd\<^bsup>\<pi> \<guillemotleft> j\<^esup>\<rightarrow> k - j
 2. i - j cd\<^bsup>\<pi> \<guillemotleft> j\<^esup>\<rightarrow> k - j \<Longrightarrow> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
hence \<open>is_path (\<pi> \<guillemotleft> j)\<close> \<open>k - j < i - j\<close>
[PROOF STATE]
proof (prove)
using this:
k < i

goal (1 subgoal):
 1. is_path (\<pi> \<guillemotleft> j) &&& k - j < i - j
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
k < i
j \<le> k
is_path \<pi>

goal (1 subgoal):
 1. is_path (\<pi> \<guillemotleft> j) &&& k - j < i - j
[PROOF STEP]
apply (metis path_path_shift)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k - j < i - j
[PROOF STEP]
by (metis assms(1) b diff_less_mono)
[PROOF STATE]
proof (state)
this:
is_path (\<pi> \<guillemotleft> j)
k - j < i - j

goal (2 subgoals):
 1. i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<Longrightarrow> i - j cd\<^bsup>\<pi> \<guillemotleft> j\<^esup>\<rightarrow> k - j
 2. i - j cd\<^bsup>\<pi> \<guillemotleft> j\<^esup>\<rightarrow> k - j \<Longrightarrow> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
is_path (\<pi> \<guillemotleft> j)
k - j < i - j

goal (2 subgoals):
 1. i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<Longrightarrow> i - j cd\<^bsup>\<pi> \<guillemotleft> j\<^esup>\<rightarrow> k - j
 2. i - j cd\<^bsup>\<pi> \<guillemotleft> j\<^esup>\<rightarrow> k - j \<Longrightarrow> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
have c: \<open>\<forall> j \<in> {k..i}. \<pi> j \<noteq> ipd (\<pi> k)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>j\<in>{k..i}. \<pi> j \<noteq> ipd (\<pi> k)
[PROOF STEP]
by (metis a ipd_impl_not_cd)
[PROOF STATE]
proof (state)
this:
\<forall>j\<in>{k..i}. \<pi> j \<noteq> ipd (\<pi> k)

goal (2 subgoals):
 1. i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<Longrightarrow> i - j cd\<^bsup>\<pi> \<guillemotleft> j\<^esup>\<rightarrow> k - j
 2. i - j cd\<^bsup>\<pi> \<guillemotleft> j\<^esup>\<rightarrow> k - j \<Longrightarrow> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
hence \<open>\<forall> ja \<in> {k - j..i - j}. (\<pi> \<guillemotleft> j) ja \<noteq> ipd ((\<pi> \<guillemotleft> j) (k - j))\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>j\<in>{k..i}. \<pi> j \<noteq> ipd (\<pi> k)

goal (1 subgoal):
 1. \<forall>ja\<in>{k - j..i - j}. (\<pi> \<guillemotleft> j) ja \<noteq> ipd ((\<pi> \<guillemotleft> j) (k - j))
[PROOF STEP]
using b assms
[PROOF STATE]
proof (prove)
using this:
\<forall>j\<in>{k..i}. \<pi> j \<noteq> ipd (\<pi> k)
k < i
j \<le> k
is_path \<pi>

goal (1 subgoal):
 1. \<forall>ja\<in>{k - j..i - j}. (\<pi> \<guillemotleft> j) ja \<noteq> ipd ((\<pi> \<guillemotleft> j) (k - j))
[PROOF STEP]
by auto fastforce
[PROOF STATE]
proof (state)
this:
\<forall>ja\<in>{k - j..i - j}. (\<pi> \<guillemotleft> j) ja \<noteq> ipd ((\<pi> \<guillemotleft> j) (k - j))

goal (2 subgoals):
 1. i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<Longrightarrow> i - j cd\<^bsup>\<pi> \<guillemotleft> j\<^esup>\<rightarrow> k - j
 2. i - j cd\<^bsup>\<pi> \<guillemotleft> j\<^esup>\<rightarrow> k - j \<Longrightarrow> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>ja\<in>{k - j..i - j}. (\<pi> \<guillemotleft> j) ja \<noteq> ipd ((\<pi> \<guillemotleft> j) (k - j))

goal (2 subgoals):
 1. i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<Longrightarrow> i - j cd\<^bsup>\<pi> \<guillemotleft> j\<^esup>\<rightarrow> k - j
 2. i - j cd\<^bsup>\<pi> \<guillemotleft> j\<^esup>\<rightarrow> k - j \<Longrightarrow> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
have \<open>j < i\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j < i
[PROOF STEP]
using assms(1) b
[PROOF STATE]
proof (prove)
using this:
j \<le> k
k < i

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

goal (2 subgoals):
 1. i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<Longrightarrow> i - j cd\<^bsup>\<pi> \<guillemotleft> j\<^esup>\<rightarrow> k - j
 2. i - j cd\<^bsup>\<pi> \<guillemotleft> j\<^esup>\<rightarrow> k - j \<Longrightarrow> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
hence \<open>(\<pi>\<guillemotleft>j) (i - j) \<noteq> return\<close>
[PROOF STATE]
proof (prove)
using this:
j < i

goal (1 subgoal):
 1. (\<pi> \<guillemotleft> j) (i - j) \<noteq> local.return
[PROOF STEP]
using a
[PROOF STATE]
proof (prove)
using this:
j < i
i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k

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

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

goal (2 subgoals):
 1. i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<Longrightarrow> i - j cd\<^bsup>\<pi> \<guillemotleft> j\<^esup>\<rightarrow> k - j
 2. i - j cd\<^bsup>\<pi> \<guillemotleft> j\<^esup>\<rightarrow> k - j \<Longrightarrow> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
is_path (\<pi> \<guillemotleft> j)
k - j < i - j
\<forall>ja\<in>{k - j..i - j}. (\<pi> \<guillemotleft> j) ja \<noteq> ipd ((\<pi> \<guillemotleft> j) (k - j))
(\<pi> \<guillemotleft> j) (i - j) \<noteq> local.return
[PROOF STEP]
show \<open>i - j cd\<^bsup>\<pi>\<guillemotleft>j\<^esup>\<rightarrow> k-j\<close>
[PROOF STATE]
proof (prove)
using this:
is_path (\<pi> \<guillemotleft> j)
k - j < i - j
\<forall>ja\<in>{k - j..i - j}. (\<pi> \<guillemotleft> j) ja \<noteq> ipd ((\<pi> \<guillemotleft> j) (k - j))
(\<pi> \<guillemotleft> j) (i - j) \<noteq> local.return

goal (1 subgoal):
 1. i - j cd\<^bsup>\<pi> \<guillemotleft> j\<^esup>\<rightarrow> k - j
[PROOF STEP]
unfolding is_cdi_def
[PROOF STATE]
proof (prove)
using this:
is_path (\<pi> \<guillemotleft> j)
k - j < i - j
\<forall>ja\<in>{k - j..i - j}. (\<pi> \<guillemotleft> j) ja \<noteq> ipd ((\<pi> \<guillemotleft> j) (k - j))
(\<pi> \<guillemotleft> j) (i - j) \<noteq> local.return

goal (1 subgoal):
 1. is_path (\<pi> \<guillemotleft> j) \<and> k - j < i - j \<and> (\<pi> \<guillemotleft> j) (i - j) \<noteq> local.return \<and> (\<forall>ja\<in>{k - j..i - j}. (\<pi> \<guillemotleft> j) ja \<noteq> ipd ((\<pi> \<guillemotleft> j) (k - j)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
i - j cd\<^bsup>\<pi> \<guillemotleft> j\<^esup>\<rightarrow> k - j

goal (1 subgoal):
 1. i - j cd\<^bsup>\<pi> \<guillemotleft> j\<^esup>\<rightarrow> k - j \<Longrightarrow> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i - j cd\<^bsup>\<pi> \<guillemotleft> j\<^esup>\<rightarrow> k - j \<Longrightarrow> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
assume a: \<open>i - j cd\<^bsup>\<pi>\<guillemotleft>j\<^esup>\<rightarrow> k-j\<close>
[PROOF STATE]
proof (state)
this:
i - j cd\<^bsup>\<pi> \<guillemotleft> j\<^esup>\<rightarrow> k - j

goal (1 subgoal):
 1. i - j cd\<^bsup>\<pi> \<guillemotleft> j\<^esup>\<rightarrow> k - j \<Longrightarrow> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
hence b: \<open>k - j < i-j\<close>
[PROOF STATE]
proof (prove)
using this:
i - j cd\<^bsup>\<pi> \<guillemotleft> j\<^esup>\<rightarrow> k - j

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

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

goal (1 subgoal):
 1. i - j cd\<^bsup>\<pi> \<guillemotleft> j\<^esup>\<rightarrow> k - j \<Longrightarrow> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
have c: \<open>\<forall> ja \<in> {k - j..i - j}. (\<pi> \<guillemotleft> j) ja \<noteq> ipd ((\<pi> \<guillemotleft> j) (k - j))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>ja\<in>{k - j..i - j}. (\<pi> \<guillemotleft> j) ja \<noteq> ipd ((\<pi> \<guillemotleft> j) (k - j))
[PROOF STEP]
by (metis a ipd_impl_not_cd)
[PROOF STATE]
proof (state)
this:
\<forall>ja\<in>{k - j..i - j}. (\<pi> \<guillemotleft> j) ja \<noteq> ipd ((\<pi> \<guillemotleft> j) (k - j))

goal (1 subgoal):
 1. i - j cd\<^bsup>\<pi> \<guillemotleft> j\<^esup>\<rightarrow> k - j \<Longrightarrow> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
have \<open>\<forall> j \<in> {k..i}. \<pi> j \<noteq> ipd (\<pi> k)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>j\<in>{k..i}. \<pi> j \<noteq> ipd (\<pi> k)
[PROOF STEP]
proof (rule,goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j. j \<in> {k..i} \<Longrightarrow> \<pi> j \<noteq> ipd (\<pi> k)
[PROOF STEP]
case (1 n)
[PROOF STATE]
proof (state)
this:
n \<in> {k..i}

goal (1 subgoal):
 1. \<And>j. j \<in> {k..i} \<Longrightarrow> \<pi> j \<noteq> ipd (\<pi> k)
[PROOF STEP]
hence \<open>n-j \<in> {k-j..i-j}\<close>
[PROOF STATE]
proof (prove)
using this:
n \<in> {k..i}

goal (1 subgoal):
 1. n - j \<in> {k - j..i - j}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
n \<in> {k..i}
j \<le> k
is_path \<pi>

goal (1 subgoal):
 1. n - j \<in> {k - j..i - j}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n - j \<in> {k - j..i - j}

goal (1 subgoal):
 1. \<And>j. j \<in> {k..i} \<Longrightarrow> \<pi> j \<noteq> ipd (\<pi> k)
[PROOF STEP]
hence \<open>\<pi> (j + (n-j)) \<noteq> ipd(\<pi> (j + (k-j)))\<close>
[PROOF STATE]
proof (prove)
using this:
n - j \<in> {k - j..i - j}

goal (1 subgoal):
 1. \<pi> (j + (n - j)) \<noteq> ipd (\<pi> (j + (k - j)))
[PROOF STEP]
by (metis c path_shift_def)
[PROOF STATE]
proof (state)
this:
\<pi> (j + (n - j)) \<noteq> ipd (\<pi> (j + (k - j)))

goal (1 subgoal):
 1. \<And>j. j \<in> {k..i} \<Longrightarrow> \<pi> j \<noteq> ipd (\<pi> k)
[PROOF STEP]
thus \<open>?case\<close>
[PROOF STATE]
proof (prove)
using this:
\<pi> (j + (n - j)) \<noteq> ipd (\<pi> (j + (k - j)))

goal (1 subgoal):
 1. \<pi> n \<noteq> ipd (\<pi> k)
[PROOF STEP]
using 1 assms(1)
[PROOF STATE]
proof (prove)
using this:
\<pi> (j + (n - j)) \<noteq> ipd (\<pi> (j + (k - j)))
n \<in> {k..i}
j \<le> k

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>j\<in>{k..i}. \<pi> j \<noteq> ipd (\<pi> k)

goal (1 subgoal):
 1. i - j cd\<^bsup>\<pi> \<guillemotleft> j\<^esup>\<rightarrow> k - j \<Longrightarrow> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>j\<in>{k..i}. \<pi> j \<noteq> ipd (\<pi> k)

goal (1 subgoal):
 1. i - j cd\<^bsup>\<pi> \<guillemotleft> j\<^esup>\<rightarrow> k - j \<Longrightarrow> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
have \<open>j < i\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j < i
[PROOF STEP]
using assms(1) b
[PROOF STATE]
proof (prove)
using this:
j \<le> k
k - j < i - j

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

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

goal (1 subgoal):
 1. \<pi> i \<noteq> local.return
[PROOF STEP]
using a
[PROOF STATE]
proof (prove)
using this:
j < i
i - j cd\<^bsup>\<pi> \<guillemotleft> j\<^esup>\<rightarrow> k - j

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

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

goal (1 subgoal):
 1. i - j cd\<^bsup>\<pi> \<guillemotleft> j\<^esup>\<rightarrow> k - j \<Longrightarrow> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
k - j < i - j
\<forall>j\<in>{k..i}. \<pi> j \<noteq> ipd (\<pi> k)
\<pi> i \<noteq> local.return
[PROOF STEP]
show \<open>i cd\<^bsup>\<pi>\<^esup>\<rightarrow>k\<close>
[PROOF STATE]
proof (prove)
using this:
k - j < i - j
\<forall>j\<in>{k..i}. \<pi> j \<noteq> ipd (\<pi> k)
\<pi> i \<noteq> local.return

goal (1 subgoal):
 1. i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
unfolding is_cdi_def
[PROOF STATE]
proof (prove)
using this:
k - j < i - j
\<forall>j\<in>{k..i}. \<pi> j \<noteq> ipd (\<pi> k)
\<pi> i \<noteq> local.return

goal (1 subgoal):
 1. is_path \<pi> \<and> k < i \<and> \<pi> i \<noteq> local.return \<and> (\<forall>j\<in>{k..i}. \<pi> j \<noteq> ipd (\<pi> k))
[PROOF STEP]
by (metis assms(1) assms(2) diff_is_0_eq' le_diff_iff nat_le_linear nat_less_le)
[PROOF STATE]
proof (state)
this:
i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cd_path_shift0: assumes \<open>is_path \<pi>\<close> shows \<open>(i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k) = (i-k cd\<^bsup>\<pi>\<guillemotleft>k\<^esup>\<rightarrow>0)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k) = (i - k cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> 0)
[PROOF STEP]
using cd_path_shift[OF _ assms]
[PROOF STATE]
proof (prove)
using this:
?j \<le> ?k \<Longrightarrow> (?i cd\<^bsup>\<pi>\<^esup>\<rightarrow> ?k) = (?i - ?j cd\<^bsup>\<pi> \<guillemotleft> ?j\<^esup>\<rightarrow> ?k - ?j)

goal (1 subgoal):
 1. (i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k) = (i - k cd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> 0)
[PROOF STEP]
by (metis diff_self_eq_0 le_refl)


[STATEMENT]
lemma icd_path_shift: assumes \<open>l \<le> k\<close> \<open>is_path \<pi>\<close> shows \<open>(i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k) = (i - l icd\<^bsup>\<pi>\<guillemotleft>l\<^esup>\<rightarrow> k - l)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k) = (i - l icd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> k - l)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k) = (i - l icd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> k - l)
[PROOF STEP]
have \<open>is_path (\<pi>\<guillemotleft>l)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_path (\<pi> \<guillemotleft> l)
[PROOF STEP]
using path_path_shift assms(2)
[PROOF STATE]
proof (prove)
using this:
is_path ?\<pi> \<Longrightarrow> is_path (?\<pi> \<guillemotleft> ?m)
is_path \<pi>

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

goal (1 subgoal):
 1. (i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k) = (i - l icd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> k - l)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
is_path (\<pi> \<guillemotleft> l)

goal (1 subgoal):
 1. (i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k) = (i - l icd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> k - l)
[PROOF STEP]
have \<open>(i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k) = (i - l cd\<^bsup>\<pi>\<guillemotleft>l\<^esup>\<rightarrow> k - l)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k) = (i - l cd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> k - l)
[PROOF STEP]
using assms cd_path_shift
[PROOF STATE]
proof (prove)
using this:
l \<le> k
is_path \<pi>
\<lbrakk>?j \<le> ?k; is_path ?\<pi>\<rbrakk> \<Longrightarrow> (?i cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?k) = (?i - ?j cd\<^bsup>?\<pi> \<guillemotleft> ?j\<^esup>\<rightarrow> ?k - ?j)

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

goal (1 subgoal):
 1. (i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k) = (i - l icd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> k - l)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k) = (i - l cd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> k - l)

goal (1 subgoal):
 1. (i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k) = (i - l icd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> k - l)
[PROOF STEP]
have \<open>(\<forall> m \<in> {k<..<i}. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m) = (\<forall> m \<in> {k - l<..<i - l}. \<not> i - l cd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> m)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>m\<in>{k<..<i}. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m) = (\<forall>m\<in>{k - l<..<i - l}. \<not> i - l cd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> m)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<forall>m\<in>{k<..<i}. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m) = (\<forall>m\<in>{k - l<..<i - l}. \<not> i - l cd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> m)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<forall>m\<in>{k<..<i}. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m) = (\<forall>m\<in>{k - l<..<i - l}. \<not> i - l cd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> m)
[PROOF STEP]
fix m
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<forall>m\<in>{k<..<i}. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m) = (\<forall>m\<in>{k - l<..<i - l}. \<not> i - l cd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> m)
[PROOF STEP]
assume *: \<open>\<forall> m \<in> {k - l<..<i - l}. \<not> i - l cd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> m\<close> \<open>m \<in> {k<..<i}\<close>
[PROOF STATE]
proof (state)
this:
\<forall>m\<in>{k - l<..<i - l}. \<not> i - l cd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> m
m \<in> {k<..<i}

goal (1 subgoal):
 1. (\<forall>m\<in>{k<..<i}. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m) = (\<forall>m\<in>{k - l<..<i - l}. \<not> i - l cd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> m)
[PROOF STEP]
hence \<open>m-l \<in> {k-l<..<i-l}\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>m\<in>{k - l<..<i - l}. \<not> i - l cd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> m
m \<in> {k<..<i}

goal (1 subgoal):
 1. m - l \<in> {k - l<..<i - l}
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
\<forall>m\<in>{k - l<..<i - l}. \<not> i - l cd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> m
m \<in> {k<..<i}
l \<le> k

goal (1 subgoal):
 1. m - l \<in> {k - l<..<i - l}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
m - l \<in> {k - l<..<i - l}

goal (1 subgoal):
 1. (\<forall>m\<in>{k<..<i}. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m) = (\<forall>m\<in>{k - l<..<i - l}. \<not> i - l cd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> m)
[PROOF STEP]
hence \<open>\<not> i - l cd\<^bsup>\<pi>\<guillemotleft>l\<^esup>\<rightarrow>(m-l)\<close>
[PROOF STATE]
proof (prove)
using this:
m - l \<in> {k - l<..<i - l}

goal (1 subgoal):
 1. \<not> i - l cd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> m - l
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
m - l \<in> {k - l<..<i - l}
\<forall>m\<in>{k - l<..<i - l}. \<not> i - l cd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> m
m \<in> {k<..<i}

goal (1 subgoal):
 1. \<not> i - l cd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> m - l
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> i - l cd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> m - l

goal (1 subgoal):
 1. (\<forall>m\<in>{k<..<i}. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m) = (\<forall>m\<in>{k - l<..<i - l}. \<not> i - l cd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> m)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<not> i - l cd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> m - l

goal (1 subgoal):
 1. (\<forall>m\<in>{k<..<i}. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m) = (\<forall>m\<in>{k - l<..<i - l}. \<not> i - l cd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> m)
[PROOF STEP]
have \<open>l \<le> m\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l \<le> m
[PROOF STEP]
using * assms
[PROOF STATE]
proof (prove)
using this:
\<forall>m\<in>{k - l<..<i - l}. \<not> i - l cd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> m
m \<in> {k<..<i}
l \<le> k
is_path \<pi>

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

goal (1 subgoal):
 1. (\<forall>m\<in>{k<..<i}. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m) = (\<forall>m\<in>{k - l<..<i - l}. \<not> i - l cd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> m)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<not> i - l cd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> m - l
l \<le> m
[PROOF STEP]
have \<open>\<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow>m\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> i - l cd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> m - l
l \<le> m

goal (1 subgoal):
 1. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
[PROOF STEP]
using assms(2) cd_path_shift
[PROOF STATE]
proof (prove)
using this:
\<not> i - l cd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> m - l
l \<le> m
is_path \<pi>
\<lbrakk>?j \<le> ?k; is_path ?\<pi>\<rbrakk> \<Longrightarrow> (?i cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?k) = (?i - ?j cd\<^bsup>?\<pi> \<guillemotleft> ?j\<^esup>\<rightarrow> ?k - ?j)

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

goal (1 subgoal):
 1. (\<forall>m\<in>{k<..<i}. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m) = (\<forall>m\<in>{k - l<..<i - l}. \<not> i - l cd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> m)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<forall>m\<in>{k - l<..<i - l}. \<not> i - l cd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> m; ?m3 \<in> {k<..<i}\<rbrakk> \<Longrightarrow> \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> ?m3

goal (1 subgoal):
 1. (\<forall>m\<in>{k<..<i}. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m) = (\<forall>m\<in>{k - l<..<i - l}. \<not> i - l cd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> m)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<forall>m\<in>{k - l<..<i - l}. \<not> i - l cd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> m; ?m3 \<in> {k<..<i}\<rbrakk> \<Longrightarrow> \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> ?m3

goal (1 subgoal):
 1. (\<forall>m\<in>{k<..<i}. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m) = (\<forall>m\<in>{k - l<..<i - l}. \<not> i - l cd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> m)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<forall>m\<in>{k - l<..<i - l}. \<not> i - l cd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> m; ?m3 \<in> {k<..<i}\<rbrakk> \<Longrightarrow> \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> ?m3

goal (1 subgoal):
 1. (\<forall>m\<in>{k<..<i}. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m) = (\<forall>m\<in>{k - l<..<i - l}. \<not> i - l cd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> m)
[PROOF STEP]
fix m
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<forall>m\<in>{k<..<i}. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m) = (\<forall>m\<in>{k - l<..<i - l}. \<not> i - l cd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> m)
[PROOF STEP]
assume *: \<open>\<forall> m \<in> {k<..<i}. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m\<close> \<open>m-l \<in> {k-l<..<i-l}\<close>
[PROOF STATE]
proof (state)
this:
\<forall>m\<in>{k<..<i}. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
m - l \<in> {k - l<..<i - l}

goal (1 subgoal):
 1. (\<forall>m\<in>{k<..<i}. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m) = (\<forall>m\<in>{k - l<..<i - l}. \<not> i - l cd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> m)
[PROOF STEP]
hence \<open>m \<in> {k<..<i}\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>m\<in>{k<..<i}. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
m - l \<in> {k - l<..<i - l}

goal (1 subgoal):
 1. m \<in> {k<..<i}
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
\<forall>m\<in>{k<..<i}. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
m - l \<in> {k - l<..<i - l}
l \<le> k

goal (1 subgoal):
 1. m \<in> {k<..<i}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
m \<in> {k<..<i}

goal (1 subgoal):
 1. (\<forall>m\<in>{k<..<i}. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m) = (\<forall>m\<in>{k - l<..<i - l}. \<not> i - l cd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> m)
[PROOF STEP]
hence \<open>\<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow>m\<close>
[PROOF STATE]
proof (prove)
using this:
m \<in> {k<..<i}

goal (1 subgoal):
 1. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
m \<in> {k<..<i}
\<forall>m\<in>{k<..<i}. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
m - l \<in> {k - l<..<i - l}

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

goal (1 subgoal):
 1. (\<forall>m\<in>{k<..<i}. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m) = (\<forall>m\<in>{k - l<..<i - l}. \<not> i - l cd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> m)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m

goal (1 subgoal):
 1. (\<forall>m\<in>{k<..<i}. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m) = (\<forall>m\<in>{k - l<..<i - l}. \<not> i - l cd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> m)
[PROOF STEP]
have \<open>l \<le> m\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l \<le> m
[PROOF STEP]
using * assms
[PROOF STATE]
proof (prove)
using this:
\<forall>m\<in>{k<..<i}. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
m - l \<in> {k - l<..<i - l}
l \<le> k
is_path \<pi>

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

goal (1 subgoal):
 1. (\<forall>m\<in>{k<..<i}. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m) = (\<forall>m\<in>{k - l<..<i - l}. \<not> i - l cd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> m)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
l \<le> m
[PROOF STEP]
have \<open>\<not> i - l cd\<^bsup>\<pi>\<guillemotleft>l\<^esup>\<rightarrow>(m-l)\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
l \<le> m

goal (1 subgoal):
 1. \<not> i - l cd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> m - l
[PROOF STEP]
using assms(2) cd_path_shift
[PROOF STATE]
proof (prove)
using this:
\<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
l \<le> m
is_path \<pi>
\<lbrakk>?j \<le> ?k; is_path ?\<pi>\<rbrakk> \<Longrightarrow> (?i cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?k) = (?i - ?j cd\<^bsup>?\<pi> \<guillemotleft> ?j\<^esup>\<rightarrow> ?k - ?j)

goal (1 subgoal):
 1. \<not> i - l cd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> m - l
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> i - l cd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> m - l

goal (1 subgoal):
 1. (\<forall>m\<in>{k<..<i}. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m) = (\<forall>m\<in>{k - l<..<i - l}. \<not> i - l cd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> m)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<forall>m\<in>{k<..<i}. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m; ?m3 - l \<in> {k - l<..<i - l}\<rbrakk> \<Longrightarrow> \<not> i - l cd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> ?m3 - l

goal (1 subgoal):
 1. (\<forall>m\<in>{k<..<i}. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m) = (\<forall>m\<in>{k - l<..<i - l}. \<not> i - l cd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> m)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<forall>m\<in>{k - l<..<i - l}. \<not> i - l cd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> m; ?m3 \<in> {k<..<i}\<rbrakk> \<Longrightarrow> \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> ?m3
\<lbrakk>\<forall>m\<in>{k<..<i}. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m; ?m3 - l \<in> {k - l<..<i - l}\<rbrakk> \<Longrightarrow> \<not> i - l cd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> ?m3 - l
[PROOF STEP]
show \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<forall>m\<in>{k - l<..<i - l}. \<not> i - l cd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> m; ?m3 \<in> {k<..<i}\<rbrakk> \<Longrightarrow> \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> ?m3
\<lbrakk>\<forall>m\<in>{k<..<i}. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m; ?m3 - l \<in> {k - l<..<i - l}\<rbrakk> \<Longrightarrow> \<not> i - l cd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> ?m3 - l

goal (1 subgoal):
 1. (\<forall>m\<in>{k<..<i}. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m) = (\<forall>m\<in>{k - l<..<i - l}. \<not> i - l cd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> m)
[PROOF STEP]
by auto (metis diff_add_inverse)
[PROOF STATE]
proof (state)
this:
(\<forall>m\<in>{k<..<i}. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m) = (\<forall>m\<in>{k - l<..<i - l}. \<not> i - l cd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> m)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<forall>m\<in>{k<..<i}. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m) = (\<forall>m\<in>{k - l<..<i - l}. \<not> i - l cd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> m)

goal (1 subgoal):
 1. (i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k) = (i - l icd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> k - l)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
is_path (\<pi> \<guillemotleft> l)
(i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k) = (i - l cd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> k - l)
(\<forall>m\<in>{k<..<i}. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m) = (\<forall>m\<in>{k - l<..<i - l}. \<not> i - l cd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> m)
[PROOF STEP]
show \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
is_path (\<pi> \<guillemotleft> l)
(i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k) = (i - l cd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> k - l)
(\<forall>m\<in>{k<..<i}. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m) = (\<forall>m\<in>{k - l<..<i - l}. \<not> i - l cd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> m)

goal (1 subgoal):
 1. (i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k) = (i - l icd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> k - l)
[PROOF STEP]
unfolding is_icdi_def
[PROOF STATE]
proof (prove)
using this:
is_path (\<pi> \<guillemotleft> l)
(i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k) = (i - l cd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> k - l)
(\<forall>m\<in>{k<..<i}. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m) = (\<forall>m\<in>{k - l<..<i - l}. \<not> i - l cd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> m)

goal (1 subgoal):
 1. (is_path \<pi> \<and> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<and> (\<forall>m\<in>{k<..<i}. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m)) = (is_path (\<pi> \<guillemotleft> l) \<and> i - l cd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> k - l \<and> (\<forall>m\<in>{k - l<..<i - l}. \<not> i - l cd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> m))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_path (\<pi> \<guillemotleft> l)
(i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k) = (i - l cd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> k - l)
(\<forall>m\<in>{k<..<i}. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m) = (\<forall>m\<in>{k - l<..<i - l}. \<not> i - l cd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> m)
l \<le> k
is_path \<pi>

goal (1 subgoal):
 1. (is_path \<pi> \<and> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k \<and> (\<forall>m\<in>{k<..<i}. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m)) = (is_path (\<pi> \<guillemotleft> l) \<and> i - l cd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> k - l \<and> (\<forall>m\<in>{k - l<..<i - l}. \<not> i - l cd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> m))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k) = (i - l icd\<^bsup>\<pi> \<guillemotleft> l\<^esup>\<rightarrow> k - l)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma icd_path_shift0: assumes \<open>is_path \<pi>\<close> shows \<open>(i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k) = (i-k icd\<^bsup>\<pi>\<guillemotleft>k\<^esup>\<rightarrow>0)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k) = (i - k icd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> 0)
[PROOF STEP]
using icd_path_shift[OF _ assms]
[PROOF STATE]
proof (prove)
using this:
?l \<le> ?k \<Longrightarrow> (?i icd\<^bsup>\<pi>\<^esup>\<rightarrow> ?k) = (?i - ?l icd\<^bsup>\<pi> \<guillemotleft> ?l\<^esup>\<rightarrow> ?k - ?l)

goal (1 subgoal):
 1. (i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k) = (i - k icd\<^bsup>\<pi> \<guillemotleft> k\<^esup>\<rightarrow> 0)
[PROOF STEP]
by (metis diff_self_eq_0 le_refl)


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

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

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


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


[STATEMENT]
lemma not_cd_impl_ipd:  assumes \<open>is_path \<pi>\<close> and \<open>k < i\<close> and \<open>\<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close> and \<open>\<pi> i \<noteq> return\<close> obtains j where \<open>j \<in> {k..i}\<close> and \<open>\<pi> j = ipd (\<pi> k)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>j. \<lbrakk>j \<in> {k..i}; \<pi> j = ipd (\<pi> k)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis assms(1) assms(2) assms(3) assms(4) is_cdi_def)


[STATEMENT]
lemma icd_is_the_icd: assumes \<open>i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close> shows \<open>k = (THE k. i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k = (THE k. i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k)
[PROOF STEP]
using assms icd_uniq
[PROOF STATE]
proof (prove)
using this:
i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k
\<lbrakk>?m icd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?n; ?m icd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?n'\<rbrakk> \<Longrightarrow> ?n = ?n'

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


[STATEMENT]
lemma all_ipd_imp_ret: assumes \<open>is_path \<pi>\<close> and \<open>\<forall> i. \<pi> i \<noteq> return \<longrightarrow> (\<exists> j>i. \<pi> j = ipd (\<pi> i))\<close> shows \<open>\<exists>j. \<pi> j = return\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>j. \<pi> j = local.return
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>j. \<pi> j = local.return
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>j. \<pi> j = local.return
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>j. \<pi> j = local.return
[PROOF STEP]
assume *: \<open>\<pi> 0 = x\<close>
[PROOF STATE]
proof (state)
this:
\<pi> 0 = x

goal (1 subgoal):
 1. \<exists>j. \<pi> j = local.return
[PROOF STEP]
have \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>j. \<pi> j = local.return
[PROOF STEP]
using wf_pdt_inv * assms
[PROOF STATE]
proof (prove)
using this:
wf pdt_inv
\<pi> 0 = x
is_path \<pi>
\<forall>i. \<pi> i \<noteq> local.return \<longrightarrow> (\<exists>j>i. \<pi> j = ipd (\<pi> i))

goal (1 subgoal):
 1. \<exists>j. \<pi> j = local.return
[PROOF STEP]
proof(induction \<open>x\<close> arbitrary: \<open>\<pi>\<close> rule: wf_induct_rule )
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x \<pi>. \<lbrakk>\<And>y \<pi>. \<lbrakk>(y, x) \<in> pdt_inv; \<pi> 0 = y; is_path \<pi>; \<forall>i. \<pi> i \<noteq> local.return \<longrightarrow> (\<exists>j>i. \<pi> j = ipd (\<pi> i))\<rbrakk> \<Longrightarrow> \<exists>j. \<pi> j = local.return; \<pi> 0 = x; is_path \<pi>; \<forall>i. \<pi> i \<noteq> local.return \<longrightarrow> (\<exists>j>i. \<pi> j = ipd (\<pi> i))\<rbrakk> \<Longrightarrow> \<exists>j. \<pi> j = local.return
[PROOF STEP]
case (less x \<pi>)
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?y1, x) \<in> pdt_inv; ?\<pi>1 0 = ?y1; is_path ?\<pi>1; \<forall>i. ?\<pi>1 i \<noteq> local.return \<longrightarrow> (\<exists>j>i. ?\<pi>1 j = ipd (?\<pi>1 i))\<rbrakk> \<Longrightarrow> \<exists>j. ?\<pi>1 j = local.return
\<pi> 0 = x
is_path \<pi>
\<forall>i. \<pi> i \<noteq> local.return \<longrightarrow> (\<exists>j>i. \<pi> j = ipd (\<pi> i))

goal (1 subgoal):
 1. \<And>x \<pi>. \<lbrakk>\<And>y \<pi>. \<lbrakk>(y, x) \<in> pdt_inv; \<pi> 0 = y; is_path \<pi>; \<forall>i. \<pi> i \<noteq> local.return \<longrightarrow> (\<exists>j>i. \<pi> j = ipd (\<pi> i))\<rbrakk> \<Longrightarrow> \<exists>j. \<pi> j = local.return; \<pi> 0 = x; is_path \<pi>; \<forall>i. \<pi> i \<noteq> local.return \<longrightarrow> (\<exists>j>i. \<pi> j = ipd (\<pi> i))\<rbrakk> \<Longrightarrow> \<exists>j. \<pi> j = local.return
[PROOF STEP]
show \<open>?case\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>j. \<pi> j = local.return
[PROOF STEP]
proof (cases \<open>x = return\<close>)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = local.return \<Longrightarrow> \<exists>j. \<pi> j = local.return
 2. x \<noteq> local.return \<Longrightarrow> \<exists>j. \<pi> j = local.return
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x = local.return

goal (2 subgoals):
 1. x = local.return \<Longrightarrow> \<exists>j. \<pi> j = local.return
 2. x \<noteq> local.return \<Longrightarrow> \<exists>j. \<pi> j = local.return
[PROOF STEP]
thus \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
x = local.return

goal (1 subgoal):
 1. \<exists>j. \<pi> j = local.return
[PROOF STEP]
using less(2)
[PROOF STATE]
proof (prove)
using this:
x = local.return
\<pi> 0 = x

goal (1 subgoal):
 1. \<exists>j. \<pi> j = local.return
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>j. \<pi> j = local.return

goal (1 subgoal):
 1. x \<noteq> local.return \<Longrightarrow> \<exists>j. \<pi> j = local.return
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<noteq> local.return \<Longrightarrow> \<exists>j. \<pi> j = local.return
[PROOF STEP]
assume not_ret: \<open>x \<noteq> return\<close>
[PROOF STATE]
proof (state)
this:
x \<noteq> local.return

goal (1 subgoal):
 1. x \<noteq> local.return \<Longrightarrow> \<exists>j. \<pi> j = local.return
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<noteq> local.return

goal (1 subgoal):
 1. x \<noteq> local.return \<Longrightarrow> \<exists>j. \<pi> j = local.return
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> local.return
[PROOF STEP]
obtain k where k_ipd: \<open>\<pi> k = ipd x\<close>
[PROOF STATE]
proof (prove)
using this:
x \<noteq> local.return

goal (1 subgoal):
 1. (\<And>k. \<pi> k = ipd x \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using less(2,4)
[PROOF STATE]
proof (prove)
using this:
x \<noteq> local.return
\<pi> 0 = x
\<forall>i. \<pi> i \<noteq> local.return \<longrightarrow> (\<exists>j>i. \<pi> j = ipd (\<pi> i))

goal (1 subgoal):
 1. (\<And>k. \<pi> k = ipd x \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<pi> k = ipd x

goal (1 subgoal):
 1. x \<noteq> local.return \<Longrightarrow> \<exists>j. \<pi> j = local.return
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<pi> k = ipd x

goal (1 subgoal):
 1. x \<noteq> local.return \<Longrightarrow> \<exists>j. \<pi> j = local.return
[PROOF STEP]
have \<open>x \<in> nodes\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> local.nodes
[PROOF STEP]
using less(2,3)
[PROOF STATE]
proof (prove)
using this:
\<pi> 0 = x
is_path \<pi>

goal (1 subgoal):
 1. x \<in> local.nodes
[PROOF STEP]
by (metis path_nodes)
[PROOF STATE]
proof (state)
this:
x \<in> local.nodes

goal (1 subgoal):
 1. x \<noteq> local.return \<Longrightarrow> \<exists>j. \<pi> j = local.return
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> local.return
\<pi> k = ipd x
x \<in> local.nodes
[PROOF STEP]
have \<open>(x, \<pi> k) \<in> pdt\<close>
[PROOF STATE]
proof (prove)
using this:
x \<noteq> local.return
\<pi> k = ipd x
x \<in> local.nodes

goal (1 subgoal):
 1. (x, \<pi> k) \<in> pdt
[PROOF STEP]
by (metis ipd_in_pdt)
[PROOF STATE]
proof (state)
this:
(x, \<pi> k) \<in> pdt

goal (1 subgoal):
 1. x \<noteq> local.return \<Longrightarrow> \<exists>j. \<pi> j = local.return
[PROOF STEP]
hence a: \<open>(\<pi> k, x) \<in> pdt_inv\<close>
[PROOF STATE]
proof (prove)
using this:
(x, \<pi> k) \<in> pdt

goal (1 subgoal):
 1. (\<pi> k, x) \<in> pdt_inv
[PROOF STEP]
unfolding pdt_inv_def
[PROOF STATE]
proof (prove)
using this:
(x, \<pi> k) \<in> pdt

goal (1 subgoal):
 1. (\<pi> k, x) \<in> pdt\<inverse>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<pi> k, x) \<in> pdt_inv

goal (1 subgoal):
 1. x \<noteq> local.return \<Longrightarrow> \<exists>j. \<pi> j = local.return
[PROOF STEP]
have b: \<open>is_path (\<pi> \<guillemotleft> k)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_path (\<pi> \<guillemotleft> k)
[PROOF STEP]
by (metis less.prems(2) path_path_shift)
[PROOF STATE]
proof (state)
this:
is_path (\<pi> \<guillemotleft> k)

goal (1 subgoal):
 1. x \<noteq> local.return \<Longrightarrow> \<exists>j. \<pi> j = local.return
[PROOF STEP]
have c: \<open>\<forall> i. (\<pi>\<guillemotleft>k) i \<noteq> return \<longrightarrow> (\<exists>j>i. (\<pi>\<guillemotleft>k) j = ipd ((\<pi>\<guillemotleft>k) i))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. (\<pi> \<guillemotleft> k) i \<noteq> local.return \<longrightarrow> (\<exists>j>i. (\<pi> \<guillemotleft> k) j = ipd ((\<pi> \<guillemotleft> k) i))
[PROOF STEP]
using less(4)
[PROOF STATE]
proof (prove)
using this:
\<forall>i. \<pi> i \<noteq> local.return \<longrightarrow> (\<exists>j>i. \<pi> j = ipd (\<pi> i))

goal (1 subgoal):
 1. \<forall>i. (\<pi> \<guillemotleft> k) i \<noteq> local.return \<longrightarrow> (\<exists>j>i. (\<pi> \<guillemotleft> k) j = ipd ((\<pi> \<guillemotleft> k) i))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>\<forall>i. \<pi> i \<noteq> local.return \<longrightarrow> (\<exists>j>i. \<pi> j = ipd (\<pi> i)); \<pi> (k + i) \<noteq> local.return\<rbrakk> \<Longrightarrow> \<exists>j>i. \<pi> (k + j) = ipd (\<pi> (k + i))
[PROOF STEP]
by (metis (full_types) ab_semigroup_add_class.add_ac(1) less_add_same_cancel1 less_imp_add_positive)
[PROOF STATE]
proof (state)
this:
\<forall>i. (\<pi> \<guillemotleft> k) i \<noteq> local.return \<longrightarrow> (\<exists>j>i. (\<pi> \<guillemotleft> k) j = ipd ((\<pi> \<guillemotleft> k) i))

goal (1 subgoal):
 1. x \<noteq> local.return \<Longrightarrow> \<exists>j. \<pi> j = local.return
[PROOF STEP]
from less(1)[OF a _ b c]
[PROOF STATE]
proof (chain)
picking this:
(\<pi> \<guillemotleft> k) 0 = \<pi> k \<Longrightarrow> \<exists>j. (\<pi> \<guillemotleft> k) j = local.return
[PROOF STEP]
have \<open>\<exists>j. (\<pi>\<guillemotleft>k) j = return\<close>
[PROOF STATE]
proof (prove)
using this:
(\<pi> \<guillemotleft> k) 0 = \<pi> k \<Longrightarrow> \<exists>j. (\<pi> \<guillemotleft> k) j = local.return

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

goal (1 subgoal):
 1. x \<noteq> local.return \<Longrightarrow> \<exists>j. \<pi> j = local.return
[PROOF STEP]
thus \<open>\<exists>j. \<pi> j = return\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>j. (\<pi> \<guillemotleft> k) j = local.return

goal (1 subgoal):
 1. \<exists>j. \<pi> j = local.return
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>j. \<pi> j = local.return

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>j. \<pi> j = local.return

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>j. \<pi> j = local.return

goal (1 subgoal):
 1. \<exists>j. \<pi> j = local.return
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<pi> 0 = ?x3 \<Longrightarrow> \<exists>j. \<pi> j = local.return

goal (1 subgoal):
 1. \<exists>j. \<pi> j = local.return
[PROOF STEP]
thus \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
\<pi> 0 = ?x3 \<Longrightarrow> \<exists>j. \<pi> j = local.return

goal (1 subgoal):
 1. \<exists>j. \<pi> j = local.return
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>j. \<pi> j = local.return

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma loop_has_cd: assumes \<open>is_path \<pi>\<close> \<open>0 < i\<close> \<open>\<pi> i = \<pi> 0\<close> \<open>\<pi> 0 \<noteq> return\<close> shows \<open>\<exists> k < i. i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k<i. i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<exists>k<i. i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k) \<Longrightarrow> False
[PROOF STEP]
let \<open>?\<pi>\<close> = \<open>(\<lambda> n. \<pi> (n mod i))\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<exists>k<i. i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k) \<Longrightarrow> False
[PROOF STEP]
assume \<open>\<not> (\<exists>k<i. i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k)\<close>
[PROOF STATE]
proof (state)
this:
\<not> (\<exists>k<i. i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k)

goal (1 subgoal):
 1. \<not> (\<exists>k<i. i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k) \<Longrightarrow> False
[PROOF STEP]
hence \<open>\<forall> k <i. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>k<i. i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k)

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

goal (1 subgoal):
 1. \<not> (\<exists>k<i. i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k) \<Longrightarrow> False
[PROOF STEP]
hence *: \<open>\<forall> k<i. (\<exists>j \<in> {k..i}. \<pi> j = ipd (\<pi> k))\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>k<i. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k

goal (1 subgoal):
 1. \<forall>k<i. \<exists>j\<in>{k..i}. \<pi> j = ipd (\<pi> k)
[PROOF STEP]
using assms(1,3,4) not_cd_impl_ipd
[PROOF STATE]
proof (prove)
using this:
\<forall>k<i. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
is_path \<pi>
\<pi> i = \<pi> 0
\<pi> 0 \<noteq> local.return
\<lbrakk>is_path ?\<pi>; ?k < ?i; \<not> ?i cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?k; ?\<pi> ?i \<noteq> local.return; \<And>j. \<lbrakk>j \<in> {?k..?i}; ?\<pi> j = ipd (?\<pi> ?k)\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<forall>k<i. \<exists>j\<in>{k..i}. \<pi> j = ipd (\<pi> k)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<forall>k<i. \<exists>j\<in>{k..i}. \<pi> j = ipd (\<pi> k)

goal (1 subgoal):
 1. \<not> (\<exists>k<i. i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k) \<Longrightarrow> False
[PROOF STEP]
have \<open>\<forall> k. (\<exists> j > k. ?\<pi> j = ipd (?\<pi> k))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k. \<exists>j>k. \<pi> (j mod i) = ipd (\<pi> (k mod i))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. \<exists>j>k. \<pi> (j mod i) = ipd (\<pi> (k mod i))
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. \<exists>j>k. \<pi> (j mod i) = ipd (\<pi> (k mod i))
[PROOF STEP]
have \<open>k mod i < i\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k mod i < i
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
0 < i

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

goal (1 subgoal):
 1. \<And>k. \<exists>j>k. \<pi> (j mod i) = ipd (\<pi> (k mod i))
[PROOF STEP]
with *
[PROOF STATE]
proof (chain)
picking this:
\<forall>k<i. \<exists>j\<in>{k..i}. \<pi> j = ipd (\<pi> k)
k mod i < i
[PROOF STEP]
obtain j where \<open>j \<in> {(k mod i)..i}\<close> \<open>\<pi> j = ipd (\<pi> (k mod i))\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>k<i. \<exists>j\<in>{k..i}. \<pi> j = ipd (\<pi> k)
k mod i < i

goal (1 subgoal):
 1. (\<And>j. \<lbrakk>j \<in> {k mod i..i}; \<pi> j = ipd (\<pi> (k mod i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
j \<in> {k mod i..i}
\<pi> j = ipd (\<pi> (k mod i))

goal (1 subgoal):
 1. \<And>k. \<exists>j>k. \<pi> (j mod i) = ipd (\<pi> (k mod i))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
j \<in> {k mod i..i}
\<pi> j = ipd (\<pi> (k mod i))
[PROOF STEP]
obtain j' where 1: \<open>j' < i\<close> \<open>\<pi> j' = ipd (\<pi> (k mod i))\<close>
[PROOF STATE]
proof (prove)
using this:
j \<in> {k mod i..i}
\<pi> j = ipd (\<pi> (k mod i))

goal (1 subgoal):
 1. (\<And>j'. \<lbrakk>j' < i; \<pi> j' = ipd (\<pi> (k mod i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases \<open>j = i\<close>, auto ,metis assms(2) assms(3),metis le_neq_implies_less)
[PROOF STATE]
proof (state)
this:
j' < i
\<pi> j' = ipd (\<pi> (k mod i))

goal (1 subgoal):
 1. \<And>k. \<exists>j>k. \<pi> (j mod i) = ipd (\<pi> (k mod i))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
j' < i
\<pi> j' = ipd (\<pi> (k mod i))
[PROOF STEP]
obtain j'' where 2: \<open>j'' > k\<close> \<open>j'' mod i = j'\<close>
[PROOF STATE]
proof (prove)
using this:
j' < i
\<pi> j' = ipd (\<pi> (k mod i))

goal (1 subgoal):
 1. (\<And>j''. \<lbrakk>k < j''; j'' mod i = j'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis mod_bound_instance)
[PROOF STATE]
proof (state)
this:
k < j''
j'' mod i = j'

goal (1 subgoal):
 1. \<And>k. \<exists>j>k. \<pi> (j mod i) = ipd (\<pi> (k mod i))
[PROOF STEP]
hence \<open>?\<pi> j'' = ipd (?\<pi> k)\<close>
[PROOF STATE]
proof (prove)
using this:
k < j''
j'' mod i = j'

goal (1 subgoal):
 1. \<pi> (j'' mod i) = ipd (\<pi> (k mod i))
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
k < j''
j'' mod i = j'
j' < i
\<pi> j' = ipd (\<pi> (k mod i))

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

goal (1 subgoal):
 1. \<And>k. \<exists>j>k. \<pi> (j mod i) = ipd (\<pi> (k mod i))
[PROOF STEP]
with 2(1)
[PROOF STATE]
proof (chain)
picking this:
k < j''
\<pi> (j'' mod i) = ipd (\<pi> (k mod i))
[PROOF STEP]
show \<open>\<exists> j > k. ?\<pi> j = ipd (?\<pi> k)\<close>
[PROOF STATE]
proof (prove)
using this:
k < j''
\<pi> (j'' mod i) = ipd (\<pi> (k mod i))

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>k. \<exists>j>k. \<pi> (j mod i) = ipd (\<pi> (k mod i))

goal (1 subgoal):
 1. \<not> (\<exists>k<i. i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k) \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>k. \<exists>j>k. \<pi> (j mod i) = ipd (\<pi> (k mod i))

goal (1 subgoal):
 1. \<not> (\<exists>k<i. i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k) \<Longrightarrow> False
[PROOF STEP]
have \<open>is_path ?\<pi>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_path (\<lambda>n. \<pi> (n mod i))
[PROOF STEP]
by (metis assms(1) assms(2) assms(3) is_path_loop)
[PROOF STATE]
proof (state)
this:
is_path (\<lambda>n. \<pi> (n mod i))

goal (1 subgoal):
 1. \<not> (\<exists>k<i. i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k) \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>k. \<exists>j>k. \<pi> (j mod i) = ipd (\<pi> (k mod i))
is_path (\<lambda>n. \<pi> (n mod i))
[PROOF STEP]
obtain k where \<open>?\<pi> k = return\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>k. \<exists>j>k. \<pi> (j mod i) = ipd (\<pi> (k mod i))
is_path (\<lambda>n. \<pi> (n mod i))

goal (1 subgoal):
 1. (\<And>k. \<pi> (k mod i) = local.return \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis (lifting) all_ipd_imp_ret)
[PROOF STATE]
proof (state)
this:
\<pi> (k mod i) = local.return

goal (1 subgoal):
 1. \<not> (\<exists>k<i. i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k) \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<pi> (k mod i) = local.return

goal (1 subgoal):
 1. \<not> (\<exists>k<i. i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k) \<Longrightarrow> False
[PROOF STEP]
have \<open>k mod i < i\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k mod i < i
[PROOF STEP]
by (simp add: assms(2))
[PROOF STATE]
proof (state)
this:
k mod i < i

goal (1 subgoal):
 1. \<not> (\<exists>k<i. i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k) \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<pi> (k mod i) = local.return
k mod i < i
[PROOF STEP]
have \<open>\<pi> i = return\<close>
[PROOF STATE]
proof (prove)
using this:
\<pi> (k mod i) = local.return
k mod i < i

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

goal (1 subgoal):
 1. \<not> (\<exists>k<i. i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k) \<Longrightarrow> False
[PROOF STEP]
thus \<open>False\<close>
[PROOF STATE]
proof (prove)
using this:
\<pi> i = local.return

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma loop_has_cd': assumes \<open>is_path \<pi>\<close> \<open>j < i\<close> \<open>\<pi> i = \<pi> j\<close> \<open>\<pi> j \<noteq> return\<close> shows \<open>\<exists> k \<in> {j..<i}. i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k\<in>{j..<i}. i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>k\<in>{j..<i}. i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
have \<open>\<exists> k'< i-j. i-j cd\<^bsup>\<pi>\<guillemotleft>j\<^esup>\<rightarrow>k'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k'<i - j. i - j cd\<^bsup>\<pi> \<guillemotleft> j\<^esup>\<rightarrow> k'
[PROOF STEP]
apply(rule loop_has_cd)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. is_path (\<pi> \<guillemotleft> j)
 2. 0 < i - j
 3. (\<pi> \<guillemotleft> j) (i - j) = (\<pi> \<guillemotleft> j) 0
 4. (\<pi> \<guillemotleft> j) 0 \<noteq> local.return
[PROOF STEP]
apply (metis assms(1) path_path_shift)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. 0 < i - j
 2. (\<pi> \<guillemotleft> j) (i - j) = (\<pi> \<guillemotleft> j) 0
 3. (\<pi> \<guillemotleft> j) 0 \<noteq> local.return
[PROOF STEP]
apply (auto simp add: assms less_imp_le)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<exists>k'<i - j. i - j cd\<^bsup>\<pi> \<guillemotleft> j\<^esup>\<rightarrow> k'

goal (1 subgoal):
 1. \<exists>k\<in>{j..<i}. i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>k'<i - j. i - j cd\<^bsup>\<pi> \<guillemotleft> j\<^esup>\<rightarrow> k'
[PROOF STEP]
obtain k where k: \<open>k<i-j\<close> \<open>i-j cd\<^bsup>\<pi>\<guillemotleft>j\<^esup>\<rightarrow>k\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>k'<i - j. i - j cd\<^bsup>\<pi> \<guillemotleft> j\<^esup>\<rightarrow> k'

goal (1 subgoal):
 1. (\<And>k. \<lbrakk>k < i - j; i - j cd\<^bsup>\<pi> \<guillemotleft> j\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k < i - j
i - j cd\<^bsup>\<pi> \<guillemotleft> j\<^esup>\<rightarrow> k

goal (1 subgoal):
 1. \<exists>k\<in>{j..<i}. i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
hence k': \<open>(k+j) < i\<close>  \<open>i-j cd\<^bsup>\<pi>\<guillemotleft>j\<^esup>\<rightarrow> (k+j)-j\<close>
[PROOF STATE]
proof (prove)
using this:
k < i - j
i - j cd\<^bsup>\<pi> \<guillemotleft> j\<^esup>\<rightarrow> k

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

goal (1 subgoal):
 1. \<exists>k\<in>{j..<i}. i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
note cd_path_shift[OF _ assms(1)]
[PROOF STATE]
proof (state)
this:
?j \<le> ?k \<Longrightarrow> (?i cd\<^bsup>\<pi>\<^esup>\<rightarrow> ?k) = (?i - ?j cd\<^bsup>\<pi> \<guillemotleft> ?j\<^esup>\<rightarrow> ?k - ?j)

goal (1 subgoal):
 1. \<exists>k\<in>{j..<i}. i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
hence \<open>i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k+j\<close>
[PROOF STATE]
proof (prove)
using this:
?j \<le> ?k \<Longrightarrow> (?i cd\<^bsup>\<pi>\<^esup>\<rightarrow> ?k) = (?i - ?j cd\<^bsup>\<pi> \<guillemotleft> ?j\<^esup>\<rightarrow> ?k - ?j)

goal (1 subgoal):
 1. i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k + j
[PROOF STEP]
using k'(2)
[PROOF STATE]
proof (prove)
using this:
?j \<le> ?k \<Longrightarrow> (?i cd\<^bsup>\<pi>\<^esup>\<rightarrow> ?k) = (?i - ?j cd\<^bsup>\<pi> \<guillemotleft> ?j\<^esup>\<rightarrow> ?k - ?j)
i - j cd\<^bsup>\<pi> \<guillemotleft> j\<^esup>\<rightarrow> k + j - j

goal (1 subgoal):
 1. i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k + j
[PROOF STEP]
by (metis le_add1 add.commute)
[PROOF STATE]
proof (state)
this:
i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k + j

goal (1 subgoal):
 1. \<exists>k\<in>{j..<i}. i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
with k'(1)
[PROOF STATE]
proof (chain)
picking this:
k + j < i
i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k + j
[PROOF STEP]
show \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
k + j < i
i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k + j

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

goal:
No subgoals!
[PROOF STEP]
qed