[STATEMENT]
lemma claim'': assumes path\<pi>: \<open>is_path \<pi>\<close> and path\<pi>': \<open>is_path \<pi>'\<close>
and \<pi>i: \<open>\<pi> i = \<pi>' i'\<close> and \<pi>j: \<open>\<pi> j = \<pi>' j'\<close>
and not_cd:  \<open>\<forall> k. \<not> j cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close>  \<open>\<forall> k. \<not> i' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> k\<close>
and nret: \<open>\<pi> i \<noteq> return\<close>
and ilj: \<open>i < j\<close>
shows \<open>i' < j'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i' < j'
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> i' < j' \<Longrightarrow> False
[PROOF STEP]
assume \<open>\<not> i' < j'\<close>
[PROOF STATE]
proof (state)
this:
\<not> i' < j'

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

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

goal (1 subgoal):
 1. \<not> i' < j' \<Longrightarrow> False
[PROOF STEP]
show \<open>False\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> False
 2. \<not> ?P \<Longrightarrow> False
[PROOF STEP]
assume j'li': \<open>j' < i'\<close>
[PROOF STATE]
proof (state)
this:
j' < i'

goal (2 subgoals):
 1. ?P \<Longrightarrow> False
 2. \<not> ?P \<Longrightarrow> False
[PROOF STEP]
define \<pi>'' where \<open>\<pi>'' \<equiv> (\<pi>@\<^bsup>j\<^esup>(\<pi>'\<guillemotleft>j'))\<guillemotleft>i\<close>
[PROOF STATE]
proof (state)
this:
\<pi>'' \<equiv> \<pi> @\<^bsup>j\<^esup> (\<pi>' \<guillemotleft> j') \<guillemotleft> i

goal (2 subgoals):
 1. ?P \<Longrightarrow> False
 2. \<not> ?P \<Longrightarrow> False
[PROOF STEP]
note \<pi>''_def[simp]
[PROOF STATE]
proof (state)
this:
\<pi>'' \<equiv> \<pi> @\<^bsup>j\<^esup> (\<pi>' \<guillemotleft> j') \<guillemotleft> i

goal (2 subgoals):
 1. ?P \<Longrightarrow> False
 2. \<not> ?P \<Longrightarrow> False
[PROOF STEP]
have \<open>\<pi> j = (\<pi>' \<guillemotleft> j') 0\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> j = (\<pi>' \<guillemotleft> j') 0
[PROOF STEP]
by (metis path_shift_def Nat.add_0_right \<pi>j)
[PROOF STATE]
proof (state)
this:
\<pi> j = (\<pi>' \<guillemotleft> j') 0

goal (2 subgoals):
 1. ?P \<Longrightarrow> False
 2. \<not> ?P \<Longrightarrow> False
[PROOF STEP]
hence \<open>is_path \<pi>''\<close>
[PROOF STATE]
proof (prove)
using this:
\<pi> j = (\<pi>' \<guillemotleft> j') 0

goal (1 subgoal):
 1. is_path \<pi>''
[PROOF STEP]
using path\<pi> path\<pi>' \<pi>''_def path_path_shift path_cons
[PROOF STATE]
proof (prove)
using this:
\<pi> j = (\<pi>' \<guillemotleft> j') 0
is_path \<pi>
is_path \<pi>'
\<pi>'' \<equiv> \<pi> @\<^bsup>j\<^esup> (\<pi>' \<guillemotleft> j') \<guillemotleft> i
is_path ?\<pi> \<Longrightarrow> is_path (?\<pi> \<guillemotleft> ?m)
\<lbrakk>is_path ?\<pi>; is_path ?\<pi>'; ?\<pi> ?m = ?\<pi>' 0\<rbrakk> \<Longrightarrow> is_path (?\<pi> @\<^bsup>?m\<^esup> ?\<pi>')

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> False
 2. \<not> ?P \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
is_path \<pi>''

goal (2 subgoals):
 1. ?P \<Longrightarrow> False
 2. \<not> ?P \<Longrightarrow> False
[PROOF STEP]
have \<open>\<pi>'' (j-i+(i'-j')) = \<pi>'' 0\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi>'' (j - i + (i' - j')) = \<pi>'' 0
[PROOF STEP]
using ilj jlei \<pi>i \<pi>j
[PROOF STATE]
proof (prove)
using this:
i < j
j' \<le> i'
\<pi> i = \<pi>' i'
\<pi> j = \<pi>' j'

goal (1 subgoal):
 1. \<pi>'' (j - i + (i' - j')) = \<pi>'' 0
[PROOF STEP]
by (auto, metis add_diff_cancel_left' le_antisym le_diff_conv le_eq_less_or_eq)
[PROOF STATE]
proof (state)
this:
\<pi>'' (j - i + (i' - j')) = \<pi>'' 0

goal (2 subgoals):
 1. ?P \<Longrightarrow> False
 2. \<not> ?P \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<pi>'' (j - i + (i' - j')) = \<pi>'' 0

goal (2 subgoals):
 1. ?P \<Longrightarrow> False
 2. \<not> ?P \<Longrightarrow> False
[PROOF STEP]
have \<open>\<pi>'' 0 \<noteq> return\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi>'' 0 \<noteq> local.return
[PROOF STEP]
by (simp add: ilj less_or_eq_imp_le nret)
[PROOF STATE]
proof (state)
this:
\<pi>'' 0 \<noteq> local.return

goal (2 subgoals):
 1. ?P \<Longrightarrow> False
 2. \<not> ?P \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<pi>'' 0 \<noteq> local.return

goal (2 subgoals):
 1. ?P \<Longrightarrow> False
 2. \<not> ?P \<Longrightarrow> False
[PROOF STEP]
have \<open>0 < j-i+(i'-j')\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < j - i + (i' - j')
[PROOF STEP]
by (metis add_is_0 ilj neq0_conv zero_less_diff)
[PROOF STATE]
proof (state)
this:
0 < j - i + (i' - j')

goal (2 subgoals):
 1. ?P \<Longrightarrow> False
 2. \<not> ?P \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
is_path \<pi>''
\<pi>'' (j - i + (i' - j')) = \<pi>'' 0
\<pi>'' 0 \<noteq> local.return
0 < j - i + (i' - j')
[PROOF STEP]
obtain k where k: \<open>k < j-i+(i'-j')\<close> \<open>j-i+(i'-j') cd\<^bsup>\<pi>''\<^esup>\<rightarrow> k\<close>
[PROOF STATE]
proof (prove)
using this:
is_path \<pi>''
\<pi>'' (j - i + (i' - j')) = \<pi>'' 0
\<pi>'' 0 \<noteq> local.return
0 < j - i + (i' - j')

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

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

goal (1 subgoal):
 1. \<forall>l\<in>{k..j - i + (i' - j')}. \<pi>'' l \<noteq> ipd (\<pi>'' k)
[PROOF STEP]
by (metis is_cdi_def)
[PROOF STATE]
proof (state)
this:
\<forall>l\<in>{k..j - i + (i' - j')}. \<pi>'' l \<noteq> ipd (\<pi>'' k)

goal (2 subgoals):
 1. ?P \<Longrightarrow> False
 2. \<not> ?P \<Longrightarrow> False
[PROOF STEP]
show \<open>False\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
proof (cases \<open>k < j-i\<close>)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. k < j - i \<Longrightarrow> False
 2. \<not> k < j - i \<Longrightarrow> False
[PROOF STEP]
assume a: \<open>k < j - i\<close>
[PROOF STATE]
proof (state)
this:
k < j - i

goal (2 subgoals):
 1. k < j - i \<Longrightarrow> False
 2. \<not> k < j - i \<Longrightarrow> False
[PROOF STEP]
hence b: \<open>\<pi>'' k = \<pi> (i + k)\<close>
[PROOF STATE]
proof (prove)
using this:
k < j - i

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

goal (2 subgoals):
 1. k < j - i \<Longrightarrow> False
 2. \<not> k < j - i \<Longrightarrow> False
[PROOF STEP]
have \<open>\<forall> l \<in> {i+k..j}. \<pi> l \<noteq> ipd (\<pi> (i+k))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>l\<in>{i + k..j}. \<pi> l \<noteq> ipd (\<pi> (i + k))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>l. l \<in> {i + k..j} \<Longrightarrow> \<pi> l \<noteq> ipd (\<pi> (i + k))
[PROOF STEP]
fix l
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>l. l \<in> {i + k..j} \<Longrightarrow> \<pi> l \<noteq> ipd (\<pi> (i + k))
[PROOF STEP]
assume l: \<open>l \<in> {i + k..j}\<close>
[PROOF STATE]
proof (state)
this:
l \<in> {i + k..j}

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

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

goal (1 subgoal):
 1. \<And>l. l \<in> {i + k..j} \<Longrightarrow> \<pi> l \<noteq> ipd (\<pi> (i + k))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<pi> l = \<pi>'' (l - i)

goal (1 subgoal):
 1. \<And>l. l \<in> {i + k..j} \<Longrightarrow> \<pi> l \<noteq> ipd (\<pi> (i + k))
[PROOF STEP]
from a l
[PROOF STATE]
proof (chain)
picking this:
k < j - i
l \<in> {i + k..j}
[PROOF STEP]
have \<open>l-i \<in> {k .. j-i + (i'-j')}\<close>
[PROOF STATE]
proof (prove)
using this:
k < j - i
l \<in> {i + k..j}

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

goal (1 subgoal):
 1. \<And>l. l \<in> {i + k..j} \<Longrightarrow> \<pi> l \<noteq> ipd (\<pi> (i + k))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<pi> l = \<pi>'' (l - i)
l - i \<in> {k..j - i + (i' - j')}
[PROOF STEP]
show \<open>\<pi> l \<noteq> ipd (\<pi> (i + k))\<close>
[PROOF STATE]
proof (prove)
using this:
\<pi> l = \<pi>'' (l - i)
l - i \<in> {k..j - i + (i' - j')}

goal (1 subgoal):
 1. \<pi> l \<noteq> ipd (\<pi> (i + k))
[PROOF STEP]
using * b
[PROOF STATE]
proof (prove)
using this:
\<pi> l = \<pi>'' (l - i)
l - i \<in> {k..j - i + (i' - j')}
\<forall>l\<in>{k..j - i + (i' - j')}. \<pi>'' l \<noteq> ipd (\<pi>'' k)
\<pi>'' k = \<pi> (i + k)

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

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

goal (2 subgoals):
 1. k < j - i \<Longrightarrow> False
 2. \<not> k < j - i \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>l\<in>{i + k..j}. \<pi> l \<noteq> ipd (\<pi> (i + k))

goal (2 subgoals):
 1. k < j - i \<Longrightarrow> False
 2. \<not> k < j - i \<Longrightarrow> False
[PROOF STEP]
have \<open>i + k < j\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i + k < j
[PROOF STEP]
using a
[PROOF STATE]
proof (prove)
using this:
k < j - i

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

goal (2 subgoals):
 1. k < j - i \<Longrightarrow> False
 2. \<not> k < j - i \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
i + k < j

goal (2 subgoals):
 1. k < j - i \<Longrightarrow> False
 2. \<not> k < j - i \<Longrightarrow> False
[PROOF STEP]
have \<open>\<pi> j \<noteq> return\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> j \<noteq> local.return
[PROOF STEP]
by (metis \<pi>i \<pi>j j'li' nret path\<pi>' term_path_stable less_imp_le)
[PROOF STATE]
proof (state)
this:
\<pi> j \<noteq> local.return

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<pi>'' k = \<pi>' (j' + (i + k) - j)
[PROOF STEP]
unfolding \<pi>''_def path_shift_def path_append_def
[PROOF STATE]
proof (prove)
using this:
j - i \<le> k

goal (1 subgoal):
 1. (if i + k \<le> j then \<pi> (i + k) else \<pi>' (j' + (i + k - j))) = \<pi>' (j' + (i + k) - j)
[PROOF STEP]
using ilj
[PROOF STATE]
proof (prove)
using this:
j - i \<le> k
i < j

goal (1 subgoal):
 1. (if i + k \<le> j then \<pi> (i + k) else \<pi>' (j' + (i + k - j))) = \<pi>' (j' + (i + k) - j)
[PROOF STEP]
by(auto,metis \<pi>j add_diff_cancel_left' le_antisym le_diff_conv add.commute)
[PROOF STATE]
proof (state)
this:
\<pi>'' k = \<pi>' (j' + (i + k) - j)

goal (1 subgoal):
 1. \<not> k < j - i \<Longrightarrow> False
[PROOF STEP]
have \<open>\<forall> l \<in> {j' + (i+k) - j..i'}. \<pi>' l \<noteq> ipd (\<pi>' (j' + (i+k) - j))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>l\<in>{j' + (i + k) - j..i'}. \<pi>' l \<noteq> ipd (\<pi>' (j' + (i + k) - j))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>l. l \<in> {j' + (i + k) - j..i'} \<Longrightarrow> \<pi>' l \<noteq> ipd (\<pi>' (j' + (i + k) - j))
[PROOF STEP]
fix l
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>l. l \<in> {j' + (i + k) - j..i'} \<Longrightarrow> \<pi>' l \<noteq> ipd (\<pi>' (j' + (i + k) - j))
[PROOF STEP]
assume l: \<open>l \<in> {j' + (i+k) - j..i'}\<close>
[PROOF STATE]
proof (state)
this:
l \<in> {j' + (i + k) - j..i'}

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

goal (1 subgoal):
 1. \<pi>' l = \<pi>'' (j + l - i - j')
[PROOF STEP]
unfolding \<pi>''_def path_shift_def path_append_def
[PROOF STATE]
proof (prove)
using this:
l \<in> {j' + (i + k) - j..i'}

goal (1 subgoal):
 1. \<pi>' l = (if i + (j + l - i - j') \<le> j then \<pi> (i + (j + l - i - j')) else \<pi>' (j' + (i + (j + l - i - j') - j)))
[PROOF STEP]
using ilj
[PROOF STATE]
proof (prove)
using this:
l \<in> {j' + (i + k) - j..i'}
i < j

goal (1 subgoal):
 1. \<pi>' l = (if i + (j + l - i - j') \<le> j then \<pi> (i + (j + l - i - j')) else \<pi>' (j' + (i + (j + l - i - j') - j)))
[PROOF STEP]
by (auto, metis Nat.diff_add_assoc \<pi>j a add.commute add_diff_cancel_left' add_leD1 le_antisym le_diff_conv)
[PROOF STATE]
proof (state)
this:
\<pi>' l = \<pi>'' (j + l - i - j')

goal (1 subgoal):
 1. \<And>l. l \<in> {j' + (i + k) - j..i'} \<Longrightarrow> \<pi>' l \<noteq> ipd (\<pi>' (j' + (i + k) - j))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<pi>' l = \<pi>'' (j + l - i - j')

goal (1 subgoal):
 1. \<And>l. l \<in> {j' + (i + k) - j..i'} \<Longrightarrow> \<pi>' l \<noteq> ipd (\<pi>' (j' + (i + k) - j))
[PROOF STEP]
from a l
[PROOF STATE]
proof (chain)
picking this:
j - i \<le> k
l \<in> {j' + (i + k) - j..i'}
[PROOF STEP]
have \<open>j + l - i - j' \<in> {k .. j-i + (i'-j')}\<close>
[PROOF STATE]
proof (prove)
using this:
j - i \<le> k
l \<in> {j' + (i + k) - j..i'}

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

goal (1 subgoal):
 1. \<And>l. l \<in> {j' + (i + k) - j..i'} \<Longrightarrow> \<pi>' l \<noteq> ipd (\<pi>' (j' + (i + k) - j))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<pi>' l = \<pi>'' (j + l - i - j')
j + l - i - j' \<in> {k..j - i + (i' - j')}
[PROOF STEP]
show \<open>\<pi>' l \<noteq> ipd (\<pi>' (j' + (i + k) - j))\<close>
[PROOF STATE]
proof (prove)
using this:
\<pi>' l = \<pi>'' (j + l - i - j')
j + l - i - j' \<in> {k..j - i + (i' - j')}

goal (1 subgoal):
 1. \<pi>' l \<noteq> ipd (\<pi>' (j' + (i + k) - j))
[PROOF STEP]
using * b
[PROOF STATE]
proof (prove)
using this:
\<pi>' l = \<pi>'' (j + l - i - j')
j + l - i - j' \<in> {k..j - i + (i' - j')}
\<forall>l\<in>{k..j - i + (i' - j')}. \<pi>'' l \<noteq> ipd (\<pi>'' k)
\<pi>'' k = \<pi>' (j' + (i + k) - j)

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

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

goal (1 subgoal):
 1. \<not> k < j - i \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>l\<in>{j' + (i + k) - j..i'}. \<pi>' l \<noteq> ipd (\<pi>' (j' + (i + k) - j))

goal (1 subgoal):
 1. \<not> k < j - i \<Longrightarrow> False
[PROOF STEP]
have \<open>j' + (i+k) - j < i'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j' + (i + k) - j < i'
[PROOF STEP]
using a  j'li' ilj k(1)
[PROOF STATE]
proof (prove)
using this:
j - i \<le> k
j' < i'
i < j
k < j - i + (i' - j')

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

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

goal (1 subgoal):
 1. \<not> k < j - i \<Longrightarrow> False
[PROOF STEP]
have \<open>\<pi>' i' \<noteq> return\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi>' i' \<noteq> local.return
[PROOF STEP]
by (metis \<pi>i nret)
[PROOF STATE]
proof (state)
this:
\<pi>' i' \<noteq> local.return

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

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

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

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

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

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

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

goal (1 subgoal):
 1. j' = i'
[PROOF STEP]
by (metis \<open>\<not> i' < j'\<close> linorder_cases)
[PROOF STATE]
proof (state)
this:
j' = i'

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

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

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

goal (1 subgoal):
 1. False
[PROOF STEP]
by (metis ilj loop_has_cd' not_cd(1) nret path\<pi>)
[PROOF STATE]
proof (state)
this:
False

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma other_claim': assumes path: \<open>is_path \<pi>\<close> and eq: \<open>\<pi> i = \<pi> j\<close> and \<open>\<pi> i \<noteq> return\<close>
and icd: \<open>\<forall> k. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close> and \<open>\<forall> k. \<not> j cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close> shows \<open>i = j\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i = j
[PROOF STEP]
proof (rule ccontr,cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>i \<noteq> j; ?P2\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>i \<noteq> j; \<not> ?P2\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume \<open>i < j\<close>
[PROOF STATE]
proof (state)
this:
i < j

goal (2 subgoals):
 1. \<lbrakk>i \<noteq> j; ?P2\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>i \<noteq> j; \<not> ?P2\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
thus \<open>False\<close>
[PROOF STATE]
proof (prove)
using this:
i < j

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

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

goal (1 subgoal):
 1. \<lbrakk>i \<noteq> j; \<not> i < j\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>i \<noteq> j; \<not> i < j\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume \<open>\<not> i < j\<close> \<open>i \<noteq> j\<close>
[PROOF STATE]
proof (state)
this:
\<not> i < j
i \<noteq> j

goal (1 subgoal):
 1. \<lbrakk>i \<noteq> j; \<not> i < j\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence \<open>j < i\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> i < j
i \<noteq> j

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

goal (1 subgoal):
 1. \<lbrakk>i \<noteq> j; \<not> i < j\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
thus \<open>False\<close>
[PROOF STATE]
proof (prove)
using this:
j < i

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma icd_no_cd_path_shift: assumes \<open>i icd\<^bsup>\<pi>\<^esup>\<rightarrow> 0\<close> shows \<open>(\<forall> k. \<not> i - 1 cd\<^bsup>\<pi>\<guillemotleft>1\<^esup>\<rightarrow> k)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k. \<not> i - 1 cd\<^bsup>\<pi> \<guillemotleft> 1\<^esup>\<rightarrow> k
[PROOF STEP]
proof (rule,rule ccontr,goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. \<not> \<not> i - 1 cd\<^bsup>\<pi> \<guillemotleft> 1\<^esup>\<rightarrow> k \<Longrightarrow> False
[PROOF STEP]
case (1 k)
[PROOF STATE]
proof (state)
this:
\<not> \<not> i - 1 cd\<^bsup>\<pi> \<guillemotleft> 1\<^esup>\<rightarrow> k

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

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

goal (1 subgoal):
 1. \<And>k. \<not> \<not> i - 1 cd\<^bsup>\<pi> \<guillemotleft> 1\<^esup>\<rightarrow> k \<Longrightarrow> False
[PROOF STEP]
have **: \<open>1 \<le> k + 1\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<le> k + 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
1 \<le> k + 1

goal (1 subgoal):
 1. \<And>k. \<not> \<not> i - 1 cd\<^bsup>\<pi> \<guillemotleft> 1\<^esup>\<rightarrow> k \<Longrightarrow> False
[PROOF STEP]
have ***: \<open>is_path \<pi>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_path \<pi>
[PROOF STEP]
by (metis assms is_icdi_def)
[PROOF STATE]
proof (state)
this:
is_path \<pi>

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

goal (1 subgoal):
 1. i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k + 1
[PROOF STEP]
using cd_path_shift[OF ** ***] *
[PROOF STATE]
proof (prove)
using this:
is_path \<pi>
(?i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k + 1) = (?i - 1 cd\<^bsup>\<pi> \<guillemotleft> 1\<^esup>\<rightarrow> k + 1 - 1)
i - 1 cd\<^bsup>\<pi> \<guillemotleft> 1\<^esup>\<rightarrow> k

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

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

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

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

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

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

goal (1 subgoal):
 1. \<And>k. \<not> \<not> i - 1 cd\<^bsup>\<pi> \<guillemotleft> 1\<^esup>\<rightarrow> k \<Longrightarrow> False
[PROOF STEP]
have \<open>0 < k + 1\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < k + 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < k + 1

goal (1 subgoal):
 1. \<And>k. \<not> \<not> i - 1 cd\<^bsup>\<pi> \<guillemotleft> 1\<^esup>\<rightarrow> k \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k + 1
k + 1 < i
0 < k + 1
[PROOF STEP]
show \<open>False\<close>
[PROOF STATE]
proof (prove)
using this:
i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k + 1
k + 1 < i
0 < k + 1

goal (1 subgoal):
 1. False
[PROOF STEP]
using assms[unfolded is_icdi_def]
[PROOF STATE]
proof (prove)
using this:
i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k + 1
k + 1 < i
0 < k + 1
is_path \<pi> \<and> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> 0 \<and> (\<forall>m\<in>{0<..<i}. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma claim': assumes path\<pi>: \<open>is_path \<pi>\<close> and path\<pi>': \<open>is_path \<pi>'\<close> and
  \<pi>i: \<open>\<pi> i = \<pi>' i'\<close> and \<pi>j: \<open>\<pi> j = \<pi>' j'\<close> and not_cd:
  \<open>i icd\<^bsup>\<pi>\<^esup>\<rightarrow> 0\<close> \<open>j icd\<^bsup>\<pi>\<^esup>\<rightarrow> 0\<close>
  \<open>i' icd\<^bsup>\<pi>'\<^esup>\<rightarrow> 0\<close> \<open>j' icd\<^bsup>\<pi>'\<^esup>\<rightarrow> 0\<close>
   and ilj: \<open>i < j\<close>
   and nret: \<open>\<pi> i \<noteq> return\<close>
  shows \<open>i' < j'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i' < j'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i' < j'
[PROOF STEP]
have g0: \<open>0 < i\<close> \<open>0 < j\<close> \<open>0 < i'\<close> \<open>0 < j'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0 < i &&& 0 < j) &&& 0 < i' &&& 0 < j'
[PROOF STEP]
using not_cd[unfolded is_icdi_def is_cdi_def]
[PROOF STATE]
proof (prove)
using this:
is_path \<pi> \<and> (is_path \<pi> \<and> 0 < i \<and> \<pi> i \<noteq> local.return \<and> (\<forall>j\<in>{0..i}. \<pi> j \<noteq> ipd (\<pi> 0))) \<and> (\<forall>m\<in>{0<..<i}. \<not> (is_path \<pi> \<and> m < i \<and> \<pi> i \<noteq> local.return \<and> (\<forall>j\<in>{m..i}. \<pi> j \<noteq> ipd (\<pi> m))))
is_path \<pi> \<and> (is_path \<pi> \<and> 0 < j \<and> \<pi> j \<noteq> local.return \<and> (\<forall>j\<in>{0..j}. \<pi> j \<noteq> ipd (\<pi> 0))) \<and> (\<forall>m\<in>{0<..<j}. \<not> (is_path \<pi> \<and> m < j \<and> \<pi> j \<noteq> local.return \<and> (\<forall>j\<in>{m..j}. \<pi> j \<noteq> ipd (\<pi> m))))
is_path \<pi>' \<and> (is_path \<pi>' \<and> 0 < i' \<and> \<pi>' i' \<noteq> local.return \<and> (\<forall>j\<in>{0..i'}. \<pi>' j \<noteq> ipd (\<pi>' 0))) \<and> (\<forall>m\<in>{0<..<i'}. \<not> (is_path \<pi>' \<and> m < i' \<and> \<pi>' i' \<noteq> local.return \<and> (\<forall>j\<in>{m..i'}. \<pi>' j \<noteq> ipd (\<pi>' m))))
is_path \<pi>' \<and> (is_path \<pi>' \<and> 0 < j' \<and> \<pi>' j' \<noteq> local.return \<and> (\<forall>j\<in>{0..j'}. \<pi>' j \<noteq> ipd (\<pi>' 0))) \<and> (\<forall>m\<in>{0<..<j'}. \<not> (is_path \<pi>' \<and> m < j' \<and> \<pi>' j' \<noteq> local.return \<and> (\<forall>j\<in>{m..j'}. \<pi>' j \<noteq> ipd (\<pi>' m))))

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

goal (1 subgoal):
 1. i' < j'
[PROOF STEP]
have  \<open>(\<pi> \<guillemotleft> 1) (i - 1) = (\<pi>' \<guillemotleft> 1) (i' - 1)\<close> \<open>(\<pi> \<guillemotleft> 1) (j - 1) = (\<pi>' \<guillemotleft> 1) (j' - 1)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<pi> \<guillemotleft> 1) (i - 1) = (\<pi>' \<guillemotleft> 1) (i' - 1) &&& (\<pi> \<guillemotleft> 1) (j - 1) = (\<pi>' \<guillemotleft> 1) (j' - 1)
[PROOF STEP]
using \<pi>i \<pi>j g0
[PROOF STATE]
proof (prove)
using this:
\<pi> i = \<pi>' i'
\<pi> j = \<pi>' j'
0 < i
0 < j
0 < i'
0 < j'

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

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

goal (1 subgoal):
 1. i' < j'
[PROOF STEP]
have \<open>\<forall> k. \<not> (j - 1) cd\<^bsup>\<pi>\<guillemotleft>1\<^esup>\<rightarrow> k\<close> \<open>\<forall> k. \<not> (i' - 1) cd\<^bsup>\<pi>'\<guillemotleft>1\<^esup>\<rightarrow> k\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k. \<not> j - 1 cd\<^bsup>\<pi> \<guillemotleft> 1\<^esup>\<rightarrow> k &&& \<forall>k. \<not> i' - 1 cd\<^bsup>\<pi>' \<guillemotleft> 1\<^esup>\<rightarrow> k
[PROOF STEP]
by (metis icd_no_cd_path_shift not_cd(2)) (metis icd_no_cd_path_shift not_cd(3))
[PROOF STATE]
proof (state)
this:
\<forall>k. \<not> j - 1 cd\<^bsup>\<pi> \<guillemotleft> 1\<^esup>\<rightarrow> k
\<forall>k. \<not> i' - 1 cd\<^bsup>\<pi>' \<guillemotleft> 1\<^esup>\<rightarrow> k

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

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

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

goal (1 subgoal):
 1. i' < j'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
is_path (\<pi> \<guillemotleft> 1)
is_path (\<pi>' \<guillemotleft> 1)

goal (1 subgoal):
 1. i' < j'
[PROOF STEP]
have \<open>(\<pi>\<guillemotleft>1) (i - 1) \<noteq> return\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<pi> \<guillemotleft> 1) (i - 1) \<noteq> local.return
[PROOF STEP]
using g0 nret
[PROOF STATE]
proof (prove)
using this:
0 < i
0 < j
0 < i'
0 < j'
\<pi> i \<noteq> local.return

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

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

goal (1 subgoal):
 1. i' < j'
[PROOF STEP]
have \<open>i - 1 < j - 1\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i - 1 < j - 1
[PROOF STEP]
using g0 ilj
[PROOF STATE]
proof (prove)
using this:
0 < i
0 < j
0 < i'
0 < j'
i < j

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

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

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

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

goal (1 subgoal):
 1. i' < j'
[PROOF STEP]
thus \<open>i'<j'\<close>
[PROOF STATE]
proof (prove)
using this:
i' - 1 < j' - 1

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma other_claim: assumes path: \<open>is_path \<pi>\<close> and eq: \<open>\<pi> i = \<pi> j\<close> and \<open>\<pi> i \<noteq> return\<close>
and icd: \<open>i icd\<^bsup>\<pi>\<^esup>\<rightarrow> 0\<close> and \<open>j icd\<^bsup>\<pi>\<^esup>\<rightarrow> 0\<close> shows \<open>i = j\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i = j
[PROOF STEP]
proof (rule ccontr,cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>i \<noteq> j; ?P2\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>i \<noteq> j; \<not> ?P2\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume \<open>i < j\<close>
[PROOF STATE]
proof (state)
this:
i < j

goal (2 subgoals):
 1. \<lbrakk>i \<noteq> j; ?P2\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>i \<noteq> j; \<not> ?P2\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
thus \<open>False\<close>
[PROOF STATE]
proof (prove)
using this:
i < j

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

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

goal (1 subgoal):
 1. \<lbrakk>i \<noteq> j; \<not> i < j\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>i \<noteq> j; \<not> i < j\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume \<open>\<not> i < j\<close> \<open>i \<noteq> j\<close>
[PROOF STATE]
proof (state)
this:
\<not> i < j
i \<noteq> j

goal (1 subgoal):
 1. \<lbrakk>i \<noteq> j; \<not> i < j\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence \<open>j < i\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> i < j
i \<noteq> j

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

goal (1 subgoal):
 1. \<lbrakk>i \<noteq> j; \<not> i < j\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
thus \<open>False\<close>
[PROOF STATE]
proof (prove)
using this:
j < i

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cd_trans0: assumes \<open>j cd\<^bsup>\<pi>\<^esup>\<rightarrow> 0\<close> and \<open>k cd\<^bsup>\<pi>\<^esup>\<rightarrow>j\<close> shows \<open>k cd\<^bsup>\<pi>\<^esup>\<rightarrow> 0\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> 0
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> k cd\<^bsup>\<pi>\<^esup>\<rightarrow> 0 \<Longrightarrow> False
[PROOF STEP]
have path: \<open>is_path \<pi>\<close> and ij: \<open>0 < j\<close> and jk: \<open>j < k\<close>
  and nret: \<open>\<pi> j \<noteq> return\<close> \<open>\<pi> k \<noteq> return\<close>
  and noipdi: \<open>\<forall> l \<in> {0..j}. \<pi> l \<noteq> ipd (\<pi> 0)\<close>
  and noipdj: \<open>\<forall> l \<in> {j..k}. \<pi> l \<noteq> ipd (\<pi> j)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (is_path \<pi> &&& 0 < j &&& j < k) &&& (\<pi> j \<noteq> local.return &&& \<pi> k \<noteq> local.return) &&& \<forall>l\<in>{0..j}. \<pi> l \<noteq> ipd (\<pi> 0) &&& \<forall>l\<in>{j..k}. \<pi> l \<noteq> ipd (\<pi> j)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
j cd\<^bsup>\<pi>\<^esup>\<rightarrow> 0
k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j

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

goal (1 subgoal):
 1. (is_path \<pi> &&& 0 < j &&& j < k) &&& (\<pi> j \<noteq> local.return &&& \<pi> k \<noteq> local.return) &&& \<forall>l\<in>{0..j}. \<pi> l \<noteq> ipd (\<pi> 0) &&& \<forall>l\<in>{j..k}. \<pi> l \<noteq> ipd (\<pi> j)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_path \<pi>
0 < j
j < k
\<pi> j \<noteq> local.return
\<pi> k \<noteq> local.return
\<forall>l\<in>{0..j}. \<pi> l \<noteq> ipd (\<pi> 0)
\<forall>l\<in>{j..k}. \<pi> l \<noteq> ipd (\<pi> j)

goal (1 subgoal):
 1. \<not> k cd\<^bsup>\<pi>\<^esup>\<rightarrow> 0 \<Longrightarrow> False
[PROOF STEP]
assume \<open>\<not> k cd\<^bsup>\<pi>\<^esup>\<rightarrow> 0\<close>
[PROOF STATE]
proof (state)
this:
\<not> k cd\<^bsup>\<pi>\<^esup>\<rightarrow> 0

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

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

goal (1 subgoal):
 1. \<exists>l\<in>{0..k}. \<pi> l = ipd (\<pi> 0)
[PROOF STEP]
using path ij jk nret
[PROOF STATE]
proof (prove)
using this:
\<not> (is_path \<pi> \<and> 0 < k \<and> \<pi> k \<noteq> local.return \<and> (\<forall>j\<in>{0..k}. \<pi> j \<noteq> ipd (\<pi> 0)))
is_path \<pi>
0 < j
j < k
\<pi> j \<noteq> local.return
\<pi> k \<noteq> local.return

goal (1 subgoal):
 1. \<exists>l\<in>{0..k}. \<pi> l = ipd (\<pi> 0)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<exists>l\<in>{0..k}. \<pi> l = ipd (\<pi> 0)

goal (1 subgoal):
 1. \<not> k cd\<^bsup>\<pi>\<^esup>\<rightarrow> 0 \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>l\<in>{0..k}. \<pi> l = ipd (\<pi> 0)
[PROOF STEP]
obtain l where \<open>l \<in> {0..k}\<close> and l: \<open>\<pi> l = ipd (\<pi> 0)\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>l\<in>{0..k}. \<pi> l = ipd (\<pi> 0)

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

goal (1 subgoal):
 1. \<not> k cd\<^bsup>\<pi>\<^esup>\<rightarrow> 0 \<Longrightarrow> False
[PROOF STEP]
hence jl: \<open>j<l\<close> and lk: \<open>l\<le>k\<close>
[PROOF STATE]
proof (prove)
using this:
l \<in> {0..k}
\<pi> l = ipd (\<pi> 0)

goal (1 subgoal):
 1. j < l &&& l \<le> k
[PROOF STEP]
using noipdi ij
[PROOF STATE]
proof (prove)
using this:
l \<in> {0..k}
\<pi> l = ipd (\<pi> 0)
\<forall>l\<in>{0..j}. \<pi> l \<noteq> ipd (\<pi> 0)
0 < j

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

goal (1 subgoal):
 1. \<not> k cd\<^bsup>\<pi>\<^esup>\<rightarrow> 0 \<Longrightarrow> False
[PROOF STEP]
have pdj: \<open>ipd (\<pi> 0) pd\<rightarrow> \<pi> j\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ipd (\<pi> 0) pd\<rightarrow> \<pi> j
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> ipd (\<pi> 0) pd\<rightarrow> \<pi> j \<Longrightarrow> False
[PROOF STEP]
have \<open>\<pi> j \<in> nodes\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> j \<in> local.nodes
[PROOF STEP]
using path
[PROOF STATE]
proof (prove)
using this:
is_path \<pi>

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

goal (1 subgoal):
 1. \<not> ipd (\<pi> 0) pd\<rightarrow> \<pi> j \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<pi> j \<in> local.nodes

goal (1 subgoal):
 1. \<not> ipd (\<pi> 0) pd\<rightarrow> \<pi> j \<Longrightarrow> False
[PROOF STEP]
assume \<open>\<not> ipd (\<pi> 0) pd\<rightarrow> \<pi> j\<close>
[PROOF STATE]
proof (state)
this:
\<not> ipd (\<pi> 0) pd\<rightarrow> \<pi> j

goal (1 subgoal):
 1. \<not> ipd (\<pi> 0) pd\<rightarrow> \<pi> j \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<pi> j \<in> local.nodes
\<not> ipd (\<pi> 0) pd\<rightarrow> \<pi> j
[PROOF STEP]
obtain \<pi>' n where *: \<open>is_path \<pi>'\<close> \<open>\<pi>' 0 = \<pi> j\<close> \<open>\<pi>' n = return\<close> \<open>\<forall> k\<le>n. \<pi>' k \<noteq> ipd(\<pi> 0)\<close>
[PROOF STATE]
proof (prove)
using this:
\<pi> j \<in> local.nodes
\<not> ipd (\<pi> 0) pd\<rightarrow> \<pi> j

goal (1 subgoal):
 1. (\<And>\<pi>' n. \<lbrakk>is_path \<pi>'; \<pi>' 0 = \<pi> j; \<pi>' n = local.return; \<forall>k\<le>n. \<pi>' k \<noteq> ipd (\<pi> 0)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using no_pd_path
[PROOF STATE]
proof (prove)
using this:
\<pi> j \<in> local.nodes
\<not> ipd (\<pi> 0) pd\<rightarrow> \<pi> j
\<lbrakk>?x \<in> local.nodes; \<not> ?y pd\<rightarrow> ?x; \<And>\<pi> n. \<lbrakk>is_path \<pi>; \<pi> 0 = ?x; \<pi> n = local.return; \<forall>k\<le>n. \<pi> k \<noteq> ?y\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>\<pi>' n. \<lbrakk>is_path \<pi>'; \<pi>' 0 = \<pi> j; \<pi>' n = local.return; \<forall>k\<le>n. \<pi>' k \<noteq> ipd (\<pi> 0)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
is_path \<pi>'
\<pi>' 0 = \<pi> j
\<pi>' n = local.return
\<forall>k\<le>n. \<pi>' k \<noteq> ipd (\<pi> 0)

goal (1 subgoal):
 1. \<not> ipd (\<pi> 0) pd\<rightarrow> \<pi> j \<Longrightarrow> False
[PROOF STEP]
hence path': \<open>is_path (\<pi> @\<^bsup>j\<^esup>  \<pi>')\<close>
[PROOF STATE]
proof (prove)
using this:
is_path \<pi>'
\<pi>' 0 = \<pi> j
\<pi>' n = local.return
\<forall>k\<le>n. \<pi>' k \<noteq> ipd (\<pi> 0)

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

goal (1 subgoal):
 1. \<not> ipd (\<pi> 0) pd\<rightarrow> \<pi> j \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
is_path (\<pi> @\<^bsup>j\<^esup> \<pi>')

goal (1 subgoal):
 1. \<not> ipd (\<pi> 0) pd\<rightarrow> \<pi> j \<Longrightarrow> False
[PROOF STEP]
have \<open>\<forall> k \<le> j + n. (\<pi>@\<^bsup>j\<^esup>  \<pi>') k \<noteq> ipd (\<pi> 0)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k\<le>j + n. (\<pi> @\<^bsup>j\<^esup> \<pi>') k \<noteq> ipd (\<pi> 0)
[PROOF STEP]
using noipdi *(4)
[PROOF STATE]
proof (prove)
using this:
\<forall>l\<in>{0..j}. \<pi> l \<noteq> ipd (\<pi> 0)
\<forall>k\<le>n. \<pi>' k \<noteq> ipd (\<pi> 0)

goal (1 subgoal):
 1. \<forall>k\<le>j + n. (\<pi> @\<^bsup>j\<^esup> \<pi>') k \<noteq> ipd (\<pi> 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>k\<le>j + n. (\<pi> @\<^bsup>j\<^esup> \<pi>') k \<noteq> ipd (\<pi> 0)

goal (1 subgoal):
 1. \<not> ipd (\<pi> 0) pd\<rightarrow> \<pi> j \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>k\<le>j + n. (\<pi> @\<^bsup>j\<^esup> \<pi>') k \<noteq> ipd (\<pi> 0)

goal (1 subgoal):
 1. \<not> ipd (\<pi> 0) pd\<rightarrow> \<pi> j \<Longrightarrow> False
[PROOF STEP]
have \<open>(\<pi>@\<^bsup>j\<^esup>  \<pi>') 0 = \<pi> 0\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<pi> @\<^bsup>j\<^esup> \<pi>') 0 = \<pi> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<pi> @\<^bsup>j\<^esup> \<pi>') 0 = \<pi> 0

goal (1 subgoal):
 1. \<not> ipd (\<pi> 0) pd\<rightarrow> \<pi> j \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<pi> @\<^bsup>j\<^esup> \<pi>') 0 = \<pi> 0

goal (1 subgoal):
 1. \<not> ipd (\<pi> 0) pd\<rightarrow> \<pi> j \<Longrightarrow> False
[PROOF STEP]
have \<open>(\<pi>@\<^bsup>j\<^esup>  \<pi>') (j + n) = return\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<pi> @\<^bsup>j\<^esup> \<pi>') (j + n) = local.return
[PROOF STEP]
using *(2,3)
[PROOF STATE]
proof (prove)
using this:
\<pi>' 0 = \<pi> j
\<pi>' n = local.return

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

goal (1 subgoal):
 1. \<not> ipd (\<pi> 0) pd\<rightarrow> \<pi> j \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
is_path (\<pi> @\<^bsup>j\<^esup> \<pi>')
\<forall>k\<le>j + n. (\<pi> @\<^bsup>j\<^esup> \<pi>') k \<noteq> ipd (\<pi> 0)
(\<pi> @\<^bsup>j\<^esup> \<pi>') 0 = \<pi> 0
(\<pi> @\<^bsup>j\<^esup> \<pi>') (j + n) = local.return
[PROOF STEP]
have \<open>\<not> ipd (\<pi> 0) pd\<rightarrow> \<pi> 0\<close>
[PROOF STATE]
proof (prove)
using this:
is_path (\<pi> @\<^bsup>j\<^esup> \<pi>')
\<forall>k\<le>j + n. (\<pi> @\<^bsup>j\<^esup> \<pi>') k \<noteq> ipd (\<pi> 0)
(\<pi> @\<^bsup>j\<^esup> \<pi>') 0 = \<pi> 0
(\<pi> @\<^bsup>j\<^esup> \<pi>') (j + n) = local.return

goal (1 subgoal):
 1. \<not> ipd (\<pi> 0) pd\<rightarrow> \<pi> 0
[PROOF STEP]
unfolding is_pd_def
[PROOF STATE]
proof (prove)
using this:
is_path (\<pi> @\<^bsup>j\<^esup> \<pi>')
\<forall>k\<le>j + n. (\<pi> @\<^bsup>j\<^esup> \<pi>') k \<noteq> ipd (\<pi> 0)
(\<pi> @\<^bsup>j\<^esup> \<pi>') 0 = \<pi> 0
(\<pi> @\<^bsup>j\<^esup> \<pi>') (j + n) = local.return

goal (1 subgoal):
 1. \<not> (\<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))))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<not> ipd (\<pi> 0) pd\<rightarrow> \<pi> 0

goal (1 subgoal):
 1. \<not> ipd (\<pi> 0) pd\<rightarrow> \<pi> j \<Longrightarrow> False
[PROOF STEP]
thus \<open>False\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> ipd (\<pi> 0) pd\<rightarrow> \<pi> 0

goal (1 subgoal):
 1. False
[PROOF STEP]
by (metis is_ipd_def ij ipd_is_ipd nret(1) path path_nodes term_path_stable less_imp_le)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ipd (\<pi> 0) pd\<rightarrow> \<pi> j

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

goal (1 subgoal):
 1. (\<pi> \<guillemotleft> j) (l - j) pd\<rightarrow> (\<pi> \<guillemotleft> j) 0
[PROOF STEP]
using jl l
[PROOF STATE]
proof (prove)
using this:
ipd (\<pi> 0) pd\<rightarrow> \<pi> j
j < l
\<pi> l = ipd (\<pi> 0)

goal (1 subgoal):
 1. (\<pi> \<guillemotleft> j) (l - j) pd\<rightarrow> (\<pi> \<guillemotleft> j) 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<pi> \<guillemotleft> j) (l - j) pd\<rightarrow> (\<pi> \<guillemotleft> j) 0

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

goal (1 subgoal):
 1. \<not> k cd\<^bsup>\<pi>\<^esup>\<rightarrow> 0 \<Longrightarrow> False
[PROOF STEP]
have \<open>is_path (\<pi>\<guillemotleft>j)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_path (\<pi> \<guillemotleft> j)
[PROOF STEP]
by (metis path path_path_shift)
[PROOF STATE]
proof (state)
this:
is_path (\<pi> \<guillemotleft> j)

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

goal (1 subgoal):
 1. \<not> k cd\<^bsup>\<pi>\<^esup>\<rightarrow> 0 \<Longrightarrow> False
[PROOF STEP]
have \<open>\<pi> l \<noteq> return\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> l \<noteq> local.return
[PROOF STEP]
by (metis lk nret(2) path term_path_stable)
[PROOF STATE]
proof (state)
this:
\<pi> l \<noteq> local.return

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

goal (1 subgoal):
 1. (\<pi> \<guillemotleft> j) (l - j) \<noteq> local.return
[PROOF STEP]
using jl
[PROOF STATE]
proof (prove)
using this:
\<pi> l \<noteq> local.return
j < l

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

goal (1 subgoal):
 1. \<not> k cd\<^bsup>\<pi>\<^esup>\<rightarrow> 0 \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<pi> \<guillemotleft> j) (l - j) \<noteq> local.return

goal (1 subgoal):
 1. \<not> k cd\<^bsup>\<pi>\<^esup>\<rightarrow> 0 \<Longrightarrow> False
[PROOF STEP]
have \<open>\<pi> j \<noteq> ipd (\<pi> 0)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> j \<noteq> ipd (\<pi> 0)
[PROOF STEP]
using noipdi
[PROOF STATE]
proof (prove)
using this:
\<forall>l\<in>{0..j}. \<pi> l \<noteq> ipd (\<pi> 0)

goal (1 subgoal):
 1. \<pi> j \<noteq> ipd (\<pi> 0)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<pi> j \<noteq> ipd (\<pi> 0)

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

goal (1 subgoal):
 1. (\<pi> \<guillemotleft> j) (l - j) \<noteq> (\<pi> \<guillemotleft> j) 0
[PROOF STEP]
using jl l
[PROOF STATE]
proof (prove)
using this:
\<pi> j \<noteq> ipd (\<pi> 0)
j < l
\<pi> l = ipd (\<pi> 0)

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

goal (1 subgoal):
 1. \<not> k cd\<^bsup>\<pi>\<^esup>\<rightarrow> 0 \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<pi> \<guillemotleft> j) (l - j) pd\<rightarrow> (\<pi> \<guillemotleft> j) 0
is_path (\<pi> \<guillemotleft> j)
(\<pi> \<guillemotleft> j) (l - j) \<noteq> local.return
(\<pi> \<guillemotleft> j) (l - j) \<noteq> (\<pi> \<guillemotleft> j) 0
[PROOF STEP]
obtain k' where \<open>k' \<le> l-j\<close> and \<open>(\<pi>\<guillemotleft>j) k' = ipd ((\<pi>\<guillemotleft>j) 0)\<close>
[PROOF STATE]
proof (prove)
using this:
(\<pi> \<guillemotleft> j) (l - j) pd\<rightarrow> (\<pi> \<guillemotleft> j) 0
is_path (\<pi> \<guillemotleft> j)
(\<pi> \<guillemotleft> j) (l - j) \<noteq> local.return
(\<pi> \<guillemotleft> j) (l - j) \<noteq> (\<pi> \<guillemotleft> j) 0

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

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

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

goal (1 subgoal):
 1. j + k' \<in> {j..k} &&& \<pi> (j + k') = ipd (\<pi> j)
[PROOF STEP]
using jl lk
[PROOF STATE]
proof (prove)
using this:
k' \<le> l - j
(\<pi> \<guillemotleft> j) k' = ipd ((\<pi> \<guillemotleft> j) 0)
j < l
l \<le> k

goal (1 subgoal):
 1. j + k' \<in> {j..k} &&& \<pi> (j + k') = ipd (\<pi> j)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
j + k' \<in> {j..k}
\<pi> (j + k') = ipd (\<pi> j)

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

goal (1 subgoal):
 1. False
[PROOF STEP]
using noipdj
[PROOF STATE]
proof (prove)
using this:
j + k' \<in> {j..k}
\<pi> (j + k') = ipd (\<pi> j)
\<forall>l\<in>{j..k}. \<pi> l \<noteq> ipd (\<pi> j)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cd_trans: assumes \<open>j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i\<close> and \<open>k cd\<^bsup>\<pi>\<^esup>\<rightarrow>j\<close> shows \<open>k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i
[PROOF STEP]
have path: \<open>is_path \<pi>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_path \<pi>
[PROOF STEP]
using assms is_cdi_def
[PROOF STATE]
proof (prove)
using this:
j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i
k cd\<^bsup>\<pi>\<^esup>\<rightarrow> j
(?i cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?k) = (is_path ?\<pi> \<and> ?k < ?i \<and> ?\<pi> ?i \<noteq> local.return \<and> (\<forall>j\<in>{?k..?i}. ?\<pi> j \<noteq> ipd (?\<pi> ?k)))

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

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

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

goal (1 subgoal):
 1. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i
[PROOF STEP]
let \<open>?\<pi>\<close> = \<open>\<pi>\<guillemotleft>i\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i
[PROOF STEP]
have \<open>j-i cd\<^bsup>?\<pi>\<^esup>\<rightarrow> 0\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j - i cd\<^bsup>\<pi> \<guillemotleft> i\<^esup>\<rightarrow> 0
[PROOF STEP]
using assms(1) cd_path_shift0 path
[PROOF STATE]
proof (prove)
using this:
j cd\<^bsup>\<pi>\<^esup>\<rightarrow> i
is_path ?\<pi> \<Longrightarrow> (?i cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?k) = (?i - ?k cd\<^bsup>?\<pi> \<guillemotleft> ?k\<^esup>\<rightarrow> 0)
is_path \<pi>

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

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

goal (1 subgoal):
 1. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i
[PROOF STEP]
have \<open>k-i cd\<^bsup>?\<pi>\<^esup>\<rightarrow>j-i\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k - i cd\<^bsup>\<pi> \<guillemotleft> i\<^esup>\<rightarrow> j - i
[PROOF STEP]
by (metis assms(2) cd_path_shift is_cdi_def ij less_imp_le_nat)
[PROOF STATE]
proof (state)
this:
k - i cd\<^bsup>\<pi> \<guillemotleft> i\<^esup>\<rightarrow> j - i

goal (1 subgoal):
 1. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
j - i cd\<^bsup>\<pi> \<guillemotleft> i\<^esup>\<rightarrow> 0
k - i cd\<^bsup>\<pi> \<guillemotleft> i\<^esup>\<rightarrow> j - i
[PROOF STEP]
have \<open>k-i cd\<^bsup>?\<pi>\<^esup>\<rightarrow> 0\<close>
[PROOF STATE]
proof (prove)
using this:
j - i cd\<^bsup>\<pi> \<guillemotleft> i\<^esup>\<rightarrow> 0
k - i cd\<^bsup>\<pi> \<guillemotleft> i\<^esup>\<rightarrow> j - i

goal (1 subgoal):
 1. k - i cd\<^bsup>\<pi> \<guillemotleft> i\<^esup>\<rightarrow> 0
[PROOF STEP]
using cd_trans0
[PROOF STATE]
proof (prove)
using this:
j - i cd\<^bsup>\<pi> \<guillemotleft> i\<^esup>\<rightarrow> 0
k - i cd\<^bsup>\<pi> \<guillemotleft> i\<^esup>\<rightarrow> j - i
\<lbrakk>?j cd\<^bsup>?\<pi>\<^esup>\<rightarrow> 0; ?k cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?j\<rbrakk> \<Longrightarrow> ?k cd\<^bsup>?\<pi>\<^esup>\<rightarrow> 0

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

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

goal (1 subgoal):
 1. k cd\<^bsup>\<pi>\<^esup>\<rightarrow> i
[PROOF STEP]
using path cd_path_shift0
[PROOF STATE]
proof (prove)
using this:
k - i cd\<^bsup>\<pi> \<guillemotleft> i\<^esup>\<rightarrow> 0
is_path \<pi>
is_path ?\<pi> \<Longrightarrow> (?i cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?k) = (?i - ?k cd\<^bsup>?\<pi> \<guillemotleft> ?k\<^esup>\<rightarrow> 0)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma excd_impl_exicd: assumes \<open>\<exists> k. i cd\<^bsup>\<pi>\<^esup>\<rightarrow>k\<close> shows \<open>\<exists> k. i icd\<^bsup>\<pi>\<^esup>\<rightarrow>k\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k. i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<exists>k. i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k

goal (1 subgoal):
 1. \<exists>k. i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
proof(induction \<open>i\<close> arbitrary: \<open>\<pi>\<close> rule: less_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x \<pi>. \<lbrakk>\<And>y \<pi>. \<lbrakk>y < x; Ex (is_cdi y \<pi>)\<rbrakk> \<Longrightarrow> Ex (is_icdi y \<pi>); Ex (is_cdi x \<pi>)\<rbrakk> \<Longrightarrow> Ex (is_icdi x \<pi>)
[PROOF STEP]
case (less i)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?y1 < i; \<exists>a. ?y1 cd\<^bsup>?\<pi>1\<^esup>\<rightarrow> a\<rbrakk> \<Longrightarrow> \<exists>a. ?y1 icd\<^bsup>?\<pi>1\<^esup>\<rightarrow> a
\<exists>a. i cd\<^bsup>\<pi>\<^esup>\<rightarrow> a

goal (1 subgoal):
 1. \<And>x \<pi>. \<lbrakk>\<And>y \<pi>. \<lbrakk>y < x; Ex (is_cdi y \<pi>)\<rbrakk> \<Longrightarrow> Ex (is_icdi y \<pi>); Ex (is_cdi x \<pi>)\<rbrakk> \<Longrightarrow> Ex (is_icdi x \<pi>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?y1 < i; \<exists>a. ?y1 cd\<^bsup>?\<pi>1\<^esup>\<rightarrow> a\<rbrakk> \<Longrightarrow> \<exists>a. ?y1 icd\<^bsup>?\<pi>1\<^esup>\<rightarrow> a
\<exists>a. i cd\<^bsup>\<pi>\<^esup>\<rightarrow> a
[PROOF STEP]
obtain k where k: \<open>i cd\<^bsup>\<pi>\<^esup>\<rightarrow>k\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?y1 < i; \<exists>a. ?y1 cd\<^bsup>?\<pi>1\<^esup>\<rightarrow> a\<rbrakk> \<Longrightarrow> \<exists>a. ?y1 icd\<^bsup>?\<pi>1\<^esup>\<rightarrow> a
\<exists>a. i cd\<^bsup>\<pi>\<^esup>\<rightarrow> a

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

goal (1 subgoal):
 1. \<And>x \<pi>. \<lbrakk>\<And>y \<pi>. \<lbrakk>y < x; Ex (is_cdi y \<pi>)\<rbrakk> \<Longrightarrow> Ex (is_icdi y \<pi>); Ex (is_cdi x \<pi>)\<rbrakk> \<Longrightarrow> Ex (is_icdi x \<pi>)
[PROOF STEP]
hence ip: \<open>is_path \<pi>\<close>
[PROOF STATE]
proof (prove)
using this:
i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k

goal (1 subgoal):
 1. is_path \<pi>
[PROOF STEP]
unfolding is_cdi_def
[PROOF STATE]
proof (prove)
using this:
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. is_path \<pi>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_path \<pi>

goal (1 subgoal):
 1. \<And>x \<pi>. \<lbrakk>\<And>y \<pi>. \<lbrakk>y < x; Ex (is_cdi y \<pi>)\<rbrakk> \<Longrightarrow> Ex (is_icdi y \<pi>); Ex (is_cdi x \<pi>)\<rbrakk> \<Longrightarrow> Ex (is_icdi x \<pi>)
[PROOF STEP]
show \<open>?case\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>a. i icd\<^bsup>\<pi>\<^esup>\<rightarrow> a
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>a. i icd\<^bsup>\<pi>\<^esup>\<rightarrow> a
 2. \<not> ?P \<Longrightarrow> \<exists>a. i icd\<^bsup>\<pi>\<^esup>\<rightarrow> a
[PROOF STEP]
assume *: \<open>\<forall> m \<in> {k<..<i}. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m\<close>
[PROOF STATE]
proof (state)
this:
\<forall>m\<in>{k<..<i}. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m

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

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

goal (1 subgoal):
 1. i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
unfolding is_icdi_def
[PROOF STATE]
proof (prove)
using this:
\<forall>m\<in>{k<..<i}. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m
i cd\<^bsup>\<pi>\<^esup>\<rightarrow> 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)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>a. i icd\<^bsup>\<pi>\<^esup>\<rightarrow> a
 2. \<not> ?P \<Longrightarrow> \<exists>a. i icd\<^bsup>\<pi>\<^esup>\<rightarrow> a
[PROOF STEP]
thus \<open>?case\<close>
[PROOF STATE]
proof (prove)
using this:
i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k

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

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

goal (1 subgoal):
 1. \<not> (\<forall>m\<in>{k<..<i}. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m) \<Longrightarrow> \<exists>a. i icd\<^bsup>\<pi>\<^esup>\<rightarrow> a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<forall>m\<in>{k<..<i}. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m)
[PROOF STEP]
obtain m where m: \<open>m \<in> {k<..<i}\<close> \<open>i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>m\<in>{k<..<i}. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m)

goal (1 subgoal):
 1. (\<And>m. \<lbrakk>m \<in> {k<..<i}; i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
m \<in> {k<..<i}
i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m

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

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

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

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

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

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

goal (1 subgoal):
 1. (\<And>k'. i - m icd\<^bsup>\<pi> \<guillemotleft> m\<^esup>\<rightarrow> k' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using less(1)
[PROOF STATE]
proof (prove)
using this:
i - m cd\<^bsup>\<pi> \<guillemotleft> m\<^esup>\<rightarrow> 0
i - m < i
\<lbrakk>?y1 < i; \<exists>a. ?y1 cd\<^bsup>?\<pi>1\<^esup>\<rightarrow> a\<rbrakk> \<Longrightarrow> \<exists>a. ?y1 icd\<^bsup>?\<pi>1\<^esup>\<rightarrow> a

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

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

goal (1 subgoal):
 1. i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k' + m
[PROOF STEP]
using ip
[PROOF STATE]
proof (prove)
using this:
i - m icd\<^bsup>\<pi> \<guillemotleft> m\<^esup>\<rightarrow> k'
is_path \<pi>

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

goal (1 subgoal):
 1. \<not> (\<forall>m\<in>{k<..<i}. \<not> i cd\<^bsup>\<pi>\<^esup>\<rightarrow> m) \<Longrightarrow> \<exists>a. i icd\<^bsup>\<pi>\<^esup>\<rightarrow> a
[PROOF STEP]
thus \<open>?case\<close>
[PROOF STATE]
proof (prove)
using this:
i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k' + m

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>a. i icd\<^bsup>\<pi>\<^esup>\<rightarrow> a

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cd_split: assumes \<open>i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close> and \<open>\<not> i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close> obtains m where \<open>i icd\<^bsup>\<pi>\<^esup>\<rightarrow> m\<close> and \<open>m cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>m. \<lbrakk>i icd\<^bsup>\<pi>\<^esup>\<rightarrow> m; m cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>m. \<lbrakk>i icd\<^bsup>\<pi>\<^esup>\<rightarrow> m; m cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have ki: \<open>k < i\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k < i
[PROOF STEP]
using assms is_cdi_def
[PROOF STATE]
proof (prove)
using this:
i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
\<not> i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k
(?i cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?k) = (is_path ?\<pi> \<and> ?k < ?i \<and> ?\<pi> ?i \<noteq> local.return \<and> (\<forall>j\<in>{?k..?i}. ?\<pi> j \<noteq> ipd (?\<pi> ?k)))

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

goal (1 subgoal):
 1. (\<And>m. \<lbrakk>i icd\<^bsup>\<pi>\<^esup>\<rightarrow> m; m cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
obtain m where m: \<open>i icd\<^bsup>\<pi>\<^esup>\<rightarrow> m\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>m. i icd\<^bsup>\<pi>\<^esup>\<rightarrow> m \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
i cd\<^bsup>\<pi>\<^esup>\<rightarrow> k

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

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

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

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

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

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

goal (1 subgoal):
 1. k < m
[PROOF STEP]
using m assms(2)
[PROOF STATE]
proof (prove)
using this:
k \<le> m
i icd\<^bsup>\<pi>\<^esup>\<rightarrow> m
\<not> i icd\<^bsup>\<pi>\<^esup>\<rightarrow> k

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

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

goal (1 subgoal):
 1. (\<And>m. \<lbrakk>i icd\<^bsup>\<pi>\<^esup>\<rightarrow> m; m cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have \<open>\<pi> m \<noteq> return\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> m \<noteq> local.return
[PROOF STEP]
using m
[PROOF STATE]
proof (prove)
using this:
i icd\<^bsup>\<pi>\<^esup>\<rightarrow> m

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

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

goal (1 subgoal):
 1. (\<And>m. \<lbrakk>i icd\<^bsup>\<pi>\<^esup>\<rightarrow> m; m cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<pi> m \<noteq> local.return

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

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

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

goal (1 subgoal):
 1. (\<And>m. \<lbrakk>i icd\<^bsup>\<pi>\<^esup>\<rightarrow> m; m cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
k < m
\<pi> m \<noteq> local.return
m < i
[PROOF STEP]
have \<open>m cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<close>
[PROOF STATE]
proof (prove)
using this:
k < m
\<pi> m \<noteq> local.return
m < i

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

goal (1 subgoal):
 1. m cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
unfolding is_cdi_def
[PROOF STATE]
proof (prove)
using this:
k < m
\<pi> m \<noteq> local.return
m < 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. is_path \<pi> \<and> k < m \<and> \<pi> m \<noteq> local.return \<and> (\<forall>j\<in>{k..m}. \<pi> j \<noteq> ipd (\<pi> k))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
m cd\<^bsup>\<pi>\<^esup>\<rightarrow> k

goal (1 subgoal):
 1. (\<And>m. \<lbrakk>i icd\<^bsup>\<pi>\<^esup>\<rightarrow> m; m cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with m that
[PROOF STATE]
proof (chain)
picking this:
i icd\<^bsup>\<pi>\<^esup>\<rightarrow> m
\<lbrakk>i icd\<^bsup>\<pi>\<^esup>\<rightarrow> ?m1; ?m1 cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> thesis
m cd\<^bsup>\<pi>\<^esup>\<rightarrow> k
[PROOF STEP]
show \<open>thesis\<close>
[PROOF STATE]
proof (prove)
using this:
i icd\<^bsup>\<pi>\<^esup>\<rightarrow> m
\<lbrakk>i icd\<^bsup>\<pi>\<^esup>\<rightarrow> ?m1; ?m1 cd\<^bsup>\<pi>\<^esup>\<rightarrow> k\<rbrakk> \<Longrightarrow> thesis
m cd\<^bsup>\<pi>\<^esup>\<rightarrow> k

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

goal:
No subgoals!
[PROOF STEP]
qed