[STATEMENT]
lemma path_cons: assumes \<open>is_path \<pi>\<close> \<open>is_path \<pi>'\<close> \<open>\<pi> m = \<pi>' 0\<close> shows \<open>is_path (\<pi> @\<^bsup>m\<^esup> \<pi>')\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_path (\<pi> @\<^bsup>m\<^esup> \<pi>')
[PROOF STEP]
unfolding is_path_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. ((\<pi> @\<^bsup>m\<^esup> \<pi>') n, (\<pi> @\<^bsup>m\<^esup> \<pi>') (Suc n)) \<in> local.edges
[PROOF STEP]
proof(rule,cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n. ?P2 n \<Longrightarrow> ((\<pi> @\<^bsup>m\<^esup> \<pi>') n, (\<pi> @\<^bsup>m\<^esup> \<pi>') (Suc n)) \<in> local.edges
 2. \<And>n. \<not> ?P2 n \<Longrightarrow> ((\<pi> @\<^bsup>m\<^esup> \<pi>') n, (\<pi> @\<^bsup>m\<^esup> \<pi>') (Suc n)) \<in> local.edges
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n. ?P2 n \<Longrightarrow> ((\<pi> @\<^bsup>m\<^esup> \<pi>') n, (\<pi> @\<^bsup>m\<^esup> \<pi>') (Suc n)) \<in> local.edges
 2. \<And>n. \<not> ?P2 n \<Longrightarrow> ((\<pi> @\<^bsup>m\<^esup> \<pi>') n, (\<pi> @\<^bsup>m\<^esup> \<pi>') (Suc n)) \<in> local.edges
[PROOF STEP]
assume \<open>m < n\<close>
[PROOF STATE]
proof (state)
this:
m < n

goal (2 subgoals):
 1. \<And>n. ?P2 n \<Longrightarrow> ((\<pi> @\<^bsup>m\<^esup> \<pi>') n, (\<pi> @\<^bsup>m\<^esup> \<pi>') (Suc n)) \<in> local.edges
 2. \<And>n. \<not> ?P2 n \<Longrightarrow> ((\<pi> @\<^bsup>m\<^esup> \<pi>') n, (\<pi> @\<^bsup>m\<^esup> \<pi>') (Suc n)) \<in> local.edges
[PROOF STEP]
thus \<open>((\<pi> @\<^bsup>m\<^esup> \<pi>') n, (\<pi> @\<^bsup>m\<^esup>  \<pi>') (Suc n)) \<in> edges\<close>
[PROOF STATE]
proof (prove)
using this:
m < n

goal (1 subgoal):
 1. ((\<pi> @\<^bsup>m\<^esup> \<pi>') n, (\<pi> @\<^bsup>m\<^esup> \<pi>') (Suc n)) \<in> local.edges
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
m < n
is_path \<pi>'

goal (1 subgoal):
 1. ((\<pi> @\<^bsup>m\<^esup> \<pi>') n, (\<pi> @\<^bsup>m\<^esup> \<pi>') (Suc n)) \<in> local.edges
[PROOF STEP]
unfolding is_path_def path_append_def
[PROOF STATE]
proof (prove)
using this:
m < n
\<forall>n. (\<pi>' n, \<pi>' (Suc n)) \<in> local.edges

goal (1 subgoal):
 1. (if n \<le> m then \<pi> n else \<pi>' (n - m), if Suc n \<le> m then \<pi> (Suc n) else \<pi>' (Suc n - m)) \<in> local.edges
[PROOF STEP]
by (auto,metis Suc_diff_Suc diff_Suc_Suc less_SucI)
[PROOF STATE]
proof (state)
this:
((\<pi> @\<^bsup>m\<^esup> \<pi>') n, (\<pi> @\<^bsup>m\<^esup> \<pi>') (Suc n)) \<in> local.edges

goal (1 subgoal):
 1. \<And>n. \<not> m < n \<Longrightarrow> ((\<pi> @\<^bsup>m\<^esup> \<pi>') n, (\<pi> @\<^bsup>m\<^esup> \<pi>') (Suc n)) \<in> local.edges
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. \<not> m < n \<Longrightarrow> ((\<pi> @\<^bsup>m\<^esup> \<pi>') n, (\<pi> @\<^bsup>m\<^esup> \<pi>') (Suc n)) \<in> local.edges
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. \<not> m < n \<Longrightarrow> ((\<pi> @\<^bsup>m\<^esup> \<pi>') n, (\<pi> @\<^bsup>m\<^esup> \<pi>') (Suc n)) \<in> local.edges
[PROOF STEP]
assume *: \<open>\<not> m < n\<close>
[PROOF STATE]
proof (state)
this:
\<not> m < n

goal (1 subgoal):
 1. \<And>n. \<not> m < n \<Longrightarrow> ((\<pi> @\<^bsup>m\<^esup> \<pi>') n, (\<pi> @\<^bsup>m\<^esup> \<pi>') (Suc n)) \<in> local.edges
[PROOF STEP]
thus \<open>((\<pi> @\<^bsup>m\<^esup>  \<pi>') n, (\<pi> @\<^bsup>m\<^esup>  \<pi>') (Suc n)) \<in> edges\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> m < n

goal (1 subgoal):
 1. ((\<pi> @\<^bsup>m\<^esup> \<pi>') n, (\<pi> @\<^bsup>m\<^esup> \<pi>') (Suc n)) \<in> local.edges
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<not> m < n; ?P1\<rbrakk> \<Longrightarrow> ((\<pi> @\<^bsup>m\<^esup> \<pi>') n, (\<pi> @\<^bsup>m\<^esup> \<pi>') (Suc n)) \<in> local.edges
 2. \<lbrakk>\<not> m < n; \<not> ?P1\<rbrakk> \<Longrightarrow> ((\<pi> @\<^bsup>m\<^esup> \<pi>') n, (\<pi> @\<^bsup>m\<^esup> \<pi>') (Suc n)) \<in> local.edges
[PROOF STEP]
assume [simp]: \<open>n = m\<close>
[PROOF STATE]
proof (state)
this:
n = m

goal (2 subgoals):
 1. \<lbrakk>\<not> m < n; ?P1\<rbrakk> \<Longrightarrow> ((\<pi> @\<^bsup>m\<^esup> \<pi>') n, (\<pi> @\<^bsup>m\<^esup> \<pi>') (Suc n)) \<in> local.edges
 2. \<lbrakk>\<not> m < n; \<not> ?P1\<rbrakk> \<Longrightarrow> ((\<pi> @\<^bsup>m\<^esup> \<pi>') n, (\<pi> @\<^bsup>m\<^esup> \<pi>') (Suc n)) \<in> local.edges
[PROOF STEP]
thus \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
n = m

goal (1 subgoal):
 1. ((\<pi> @\<^bsup>m\<^esup> \<pi>') n, (\<pi> @\<^bsup>m\<^esup> \<pi>') (Suc n)) \<in> local.edges
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
n = m
is_path \<pi>
is_path \<pi>'
\<pi> m = \<pi>' 0

goal (1 subgoal):
 1. ((\<pi> @\<^bsup>m\<^esup> \<pi>') n, (\<pi> @\<^bsup>m\<^esup> \<pi>') (Suc n)) \<in> local.edges
[PROOF STEP]
unfolding is_path_def path_append_def
[PROOF STATE]
proof (prove)
using this:
n = m
\<forall>n. (\<pi> n, \<pi> (Suc n)) \<in> local.edges
\<forall>n. (\<pi>' n, \<pi>' (Suc n)) \<in> local.edges
\<pi> m = \<pi>' 0

goal (1 subgoal):
 1. (if n \<le> m then \<pi> n else \<pi>' (n - m), if Suc n \<le> m then \<pi> (Suc n) else \<pi>' (Suc n - m)) \<in> local.edges
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
((\<pi> @\<^bsup>m\<^esup> \<pi>') n, (\<pi> @\<^bsup>m\<^esup> \<pi>') (Suc n)) \<in> local.edges

goal (1 subgoal):
 1. \<lbrakk>\<not> m < n; n \<noteq> m\<rbrakk> \<Longrightarrow> ((\<pi> @\<^bsup>m\<^esup> \<pi>') n, (\<pi> @\<^bsup>m\<^esup> \<pi>') (Suc n)) \<in> local.edges
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<not> m < n; n \<noteq> m\<rbrakk> \<Longrightarrow> ((\<pi> @\<^bsup>m\<^esup> \<pi>') n, (\<pi> @\<^bsup>m\<^esup> \<pi>') (Suc n)) \<in> local.edges
[PROOF STEP]
assume \<open>n \<noteq> m\<close>
[PROOF STATE]
proof (state)
this:
n \<noteq> m

goal (1 subgoal):
 1. \<lbrakk>\<not> m < n; n \<noteq> m\<rbrakk> \<Longrightarrow> ((\<pi> @\<^bsup>m\<^esup> \<pi>') n, (\<pi> @\<^bsup>m\<^esup> \<pi>') (Suc n)) \<in> local.edges
[PROOF STEP]
hence \<open>Suc n \<le> m\<close> \<open>n\<le> m\<close>
[PROOF STATE]
proof (prove)
using this:
n \<noteq> m

goal (1 subgoal):
 1. Suc n \<le> m &&& n \<le> m
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
n \<noteq> m
\<not> m < n

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

goal (1 subgoal):
 1. \<lbrakk>\<not> m < n; n \<noteq> m\<rbrakk> \<Longrightarrow> ((\<pi> @\<^bsup>m\<^esup> \<pi>') n, (\<pi> @\<^bsup>m\<^esup> \<pi>') (Suc n)) \<in> local.edges
[PROOF STEP]
with assms(1)
[PROOF STATE]
proof (chain)
picking this:
is_path \<pi>
Suc n \<le> m
n \<le> m
[PROOF STEP]
show \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
is_path \<pi>
Suc n \<le> m
n \<le> m

goal (1 subgoal):
 1. ((\<pi> @\<^bsup>m\<^esup> \<pi>') n, (\<pi> @\<^bsup>m\<^esup> \<pi>') (Suc n)) \<in> local.edges
[PROOF STEP]
unfolding is_path_def
[PROOF STATE]
proof (prove)
using this:
\<forall>n. (\<pi> n, \<pi> (Suc n)) \<in> local.edges
Suc n \<le> m
n \<le> m

goal (1 subgoal):
 1. ((\<pi> @\<^bsup>m\<^esup> \<pi>') n, (\<pi> @\<^bsup>m\<^esup> \<pi>') (Suc n)) \<in> local.edges
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
((\<pi> @\<^bsup>m\<^esup> \<pi>') n, (\<pi> @\<^bsup>m\<^esup> \<pi>') (Suc n)) \<in> local.edges

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
((\<pi> @\<^bsup>m\<^esup> \<pi>') n, (\<pi> @\<^bsup>m\<^esup> \<pi>') (Suc n)) \<in> local.edges

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_path_loop: assumes \<open>is_path \<pi>\<close> \<open>0 < i\<close> \<open>\<pi> i = \<pi> 0\<close> shows \<open>is_path (\<lambda> n. \<pi> (n mod i))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_path (\<lambda>n. \<pi> (n mod i))
[PROOF STEP]
unfolding is_path_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. (\<pi> (n mod i), \<pi> (Suc n mod i)) \<in> local.edges
[PROOF STEP]
proof (rule,cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n. ?P2 n \<Longrightarrow> (\<pi> (n mod i), \<pi> (Suc n mod i)) \<in> local.edges
 2. \<And>n. \<not> ?P2 n \<Longrightarrow> (\<pi> (n mod i), \<pi> (Suc n mod i)) \<in> local.edges
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n. ?P2 n \<Longrightarrow> (\<pi> (n mod i), \<pi> (Suc n mod i)) \<in> local.edges
 2. \<And>n. \<not> ?P2 n \<Longrightarrow> (\<pi> (n mod i), \<pi> (Suc n mod i)) \<in> local.edges
[PROOF STEP]
assume \<open>0 < Suc n mod i\<close>
[PROOF STATE]
proof (state)
this:
0 < Suc n mod i

goal (2 subgoals):
 1. \<And>n. ?P2 n \<Longrightarrow> (\<pi> (n mod i), \<pi> (Suc n mod i)) \<in> local.edges
 2. \<And>n. \<not> ?P2 n \<Longrightarrow> (\<pi> (n mod i), \<pi> (Suc n mod i)) \<in> local.edges
[PROOF STEP]
hence \<open>Suc n mod i = Suc (n mod i)\<close>
[PROOF STATE]
proof (prove)
using this:
0 < Suc n mod i

goal (1 subgoal):
 1. Suc n mod i = Suc (n mod i)
[PROOF STEP]
by (metis mod_Suc neq0_conv)
[PROOF STATE]
proof (state)
this:
Suc n mod i = Suc (n mod i)

goal (2 subgoals):
 1. \<And>n. ?P2 n \<Longrightarrow> (\<pi> (n mod i), \<pi> (Suc n mod i)) \<in> local.edges
 2. \<And>n. \<not> ?P2 n \<Longrightarrow> (\<pi> (n mod i), \<pi> (Suc n mod i)) \<in> local.edges
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Suc n mod i = Suc (n mod i)

goal (2 subgoals):
 1. \<And>n. ?P2 n \<Longrightarrow> (\<pi> (n mod i), \<pi> (Suc n mod i)) \<in> local.edges
 2. \<And>n. \<not> ?P2 n \<Longrightarrow> (\<pi> (n mod i), \<pi> (Suc n mod i)) \<in> local.edges
[PROOF STEP]
have \<open>(\<pi> (n mod i), \<pi> (Suc (n mod i))) \<in> edges\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<pi> (n mod i), \<pi> (Suc (n mod i))) \<in> local.edges
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
is_path \<pi>

goal (1 subgoal):
 1. (\<pi> (n mod i), \<pi> (Suc (n mod i))) \<in> local.edges
[PROOF STEP]
unfolding is_path_def
[PROOF STATE]
proof (prove)
using this:
\<forall>n. (\<pi> n, \<pi> (Suc n)) \<in> local.edges

goal (1 subgoal):
 1. (\<pi> (n mod i), \<pi> (Suc (n mod i))) \<in> local.edges
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<pi> (n mod i), \<pi> (Suc (n mod i))) \<in> local.edges

goal (2 subgoals):
 1. \<And>n. ?P2 n \<Longrightarrow> (\<pi> (n mod i), \<pi> (Suc n mod i)) \<in> local.edges
 2. \<And>n. \<not> ?P2 n \<Longrightarrow> (\<pi> (n mod i), \<pi> (Suc n mod i)) \<in> local.edges
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Suc n mod i = Suc (n mod i)
(\<pi> (n mod i), \<pi> (Suc (n mod i))) \<in> local.edges
[PROOF STEP]
show \<open>(\<pi> (n mod i), \<pi> (Suc n mod i)) \<in> edges\<close>
[PROOF STATE]
proof (prove)
using this:
Suc n mod i = Suc (n mod i)
(\<pi> (n mod i), \<pi> (Suc (n mod i))) \<in> local.edges

goal (1 subgoal):
 1. (\<pi> (n mod i), \<pi> (Suc n mod i)) \<in> local.edges
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<pi> (n mod i), \<pi> (Suc n mod i)) \<in> local.edges

goal (1 subgoal):
 1. \<And>n. \<not> 0 < Suc n mod i \<Longrightarrow> (\<pi> (n mod i), \<pi> (Suc n mod i)) \<in> local.edges
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. \<not> 0 < Suc n mod i \<Longrightarrow> (\<pi> (n mod i), \<pi> (Suc n mod i)) \<in> local.edges
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. \<not> 0 < Suc n mod i \<Longrightarrow> (\<pi> (n mod i), \<pi> (Suc n mod i)) \<in> local.edges
[PROOF STEP]
assume \<open>\<not> 0 < Suc n mod i\<close>
[PROOF STATE]
proof (state)
this:
\<not> 0 < Suc n mod i

goal (1 subgoal):
 1. \<And>n. \<not> 0 < Suc n mod i \<Longrightarrow> (\<pi> (n mod i), \<pi> (Suc n mod i)) \<in> local.edges
[PROOF STEP]
hence \<open>Suc n mod i = 0\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> 0 < Suc n mod i

goal (1 subgoal):
 1. Suc n mod i = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Suc n mod i = 0

goal (1 subgoal):
 1. \<And>n. \<not> 0 < Suc n mod i \<Longrightarrow> (\<pi> (n mod i), \<pi> (Suc n mod i)) \<in> local.edges
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Suc n mod i = 0

goal (1 subgoal):
 1. \<And>n. \<not> 0 < Suc n mod i \<Longrightarrow> (\<pi> (n mod i), \<pi> (Suc n mod i)) \<in> local.edges
[PROOF STEP]
hence \<open>n mod i = i - 1\<close>
[PROOF STATE]
proof (prove)
using this:
Suc n mod i = 0

goal (1 subgoal):
 1. n mod i = i - 1
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
Suc n mod i = 0
0 < i

goal (1 subgoal):
 1. n mod i = i - 1
[PROOF STEP]
by (metis Zero_neq_Suc diff_Suc_1 mod_Suc)
[PROOF STATE]
proof (state)
this:
n mod i = i - 1

goal (1 subgoal):
 1. \<And>n. \<not> 0 < Suc n mod i \<Longrightarrow> (\<pi> (n mod i), \<pi> (Suc n mod i)) \<in> local.edges
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Suc n mod i = 0
n mod i = i - 1
[PROOF STEP]
show \<open>(\<pi>(n mod i), \<pi> (Suc n mod i)) \<in> edges\<close>
[PROOF STATE]
proof (prove)
using this:
Suc n mod i = 0
n mod i = i - 1

goal (1 subgoal):
 1. (\<pi> (n mod i), \<pi> (Suc n mod i)) \<in> local.edges
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
Suc n mod i = 0
n mod i = i - 1
is_path \<pi>

goal (1 subgoal):
 1. (\<pi> (n mod i), \<pi> (Suc n mod i)) \<in> local.edges
[PROOF STEP]
unfolding is_path_def
[PROOF STATE]
proof (prove)
using this:
Suc n mod i = 0
n mod i = i - 1
\<forall>n. (\<pi> n, \<pi> (Suc n)) \<in> local.edges

goal (1 subgoal):
 1. (\<pi> (n mod i), \<pi> (Suc n mod i)) \<in> local.edges
[PROOF STEP]
by (metis assms(3) mod_Suc)
[PROOF STATE]
proof (state)
this:
(\<pi> (n mod i), \<pi> (Suc n mod i)) \<in> local.edges

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma path_nodes: \<open>is_path \<pi> \<Longrightarrow> \<pi> k \<in> nodes\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_path \<pi> \<Longrightarrow> \<pi> k \<in> local.nodes
[PROOF STEP]
unfolding is_path_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. (\<pi> n, \<pi> (Suc n)) \<in> local.edges \<Longrightarrow> \<pi> k \<in> local.nodes
[PROOF STEP]
using edges_nodes
[PROOF STATE]
proof (prove)
using this:
local.edges \<subseteq> local.nodes \<times> local.nodes

goal (1 subgoal):
 1. \<forall>n. (\<pi> n, \<pi> (Suc n)) \<in> local.edges \<Longrightarrow> \<pi> k \<in> local.nodes
[PROOF STEP]
by force


[STATEMENT]
lemma direct_path_return': assumes \<open>is_path \<pi> \<close> \<open>\<pi> 0 = x\<close> \<open>x \<noteq> return\<close> \<open>\<pi> n = return\<close>
obtains \<pi>' n' where \<open>is_path \<pi>'\<close> \<open>\<pi>' 0 = x\<close> \<open>\<pi>' n' = return\<close> \<open>\<forall> i> 0. \<pi>' i \<noteq> x\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<pi>' n'. \<lbrakk>is_path \<pi>'; \<pi>' 0 = x; \<pi>' n' = local.return; \<forall>i>0. \<pi>' i \<noteq> x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_path \<pi>
\<pi> 0 = x
x \<noteq> local.return
\<pi> n = local.return

goal (1 subgoal):
 1. (\<And>\<pi>' n'. \<lbrakk>is_path \<pi>'; \<pi>' 0 = x; \<pi>' n' = local.return; \<forall>i>0. \<pi>' i \<noteq> x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof (induction \<open>n\<close> arbitrary: \<open>\<pi>\<close>  rule: less_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa \<pi>. \<lbrakk>\<And>y \<pi>. \<lbrakk>y < xa; \<And>\<pi>' n'. \<lbrakk>is_path \<pi>'; \<pi>' 0 = x; \<pi>' n' = local.return; \<forall>i>0. \<pi>' i \<noteq> x\<rbrakk> \<Longrightarrow> thesis; is_path \<pi>; \<pi> 0 = x; x \<noteq> local.return; \<pi> y = local.return\<rbrakk> \<Longrightarrow> thesis; \<And>\<pi>' n'. \<lbrakk>is_path \<pi>'; \<pi>' 0 = x; \<pi>' n' = local.return; \<forall>i>0. \<pi>' i \<noteq> x\<rbrakk> \<Longrightarrow> thesis; is_path \<pi>; \<pi> 0 = x; x \<noteq> local.return; \<pi> xa = local.return\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
case (less n \<pi>)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?y1 < n; \<And>\<pi>' n'. \<lbrakk>is_path \<pi>'; \<pi>' 0 = x; \<pi>' n' = local.return; \<forall>i>0. \<pi>' i \<noteq> x\<rbrakk> \<Longrightarrow> thesis; is_path ?\<pi>1; ?\<pi>1 0 = x; x \<noteq> local.return; ?\<pi>1 ?y1 = local.return\<rbrakk> \<Longrightarrow> thesis
\<lbrakk>is_path ?\<pi>'1; ?\<pi>'1 0 = x; ?\<pi>'1 ?n'1 = local.return; \<forall>i>0. ?\<pi>'1 i \<noteq> x\<rbrakk> \<Longrightarrow> thesis
is_path \<pi>
\<pi> 0 = x
x \<noteq> local.return
\<pi> n = local.return

goal (1 subgoal):
 1. \<And>xa \<pi>. \<lbrakk>\<And>y \<pi>. \<lbrakk>y < xa; \<And>\<pi>' n'. \<lbrakk>is_path \<pi>'; \<pi>' 0 = x; \<pi>' n' = local.return; \<forall>i>0. \<pi>' i \<noteq> x\<rbrakk> \<Longrightarrow> thesis; is_path \<pi>; \<pi> 0 = x; x \<noteq> local.return; \<pi> y = local.return\<rbrakk> \<Longrightarrow> thesis; \<And>\<pi>' n'. \<lbrakk>is_path \<pi>'; \<pi>' 0 = x; \<pi>' n' = local.return; \<forall>i>0. \<pi>' i \<noteq> x\<rbrakk> \<Longrightarrow> thesis; is_path \<pi>; \<pi> 0 = x; x \<noteq> local.return; \<pi> xa = local.return\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
hence ih: \<open>\<And> n' \<pi>'. n' < n \<Longrightarrow> is_path \<pi>' \<Longrightarrow> \<pi>' 0 = x \<Longrightarrow> \<pi>' n' = return \<Longrightarrow> thesis\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?y1 < n; \<And>\<pi>' n'. \<lbrakk>is_path \<pi>'; \<pi>' 0 = x; \<pi>' n' = local.return; \<forall>i>0. \<pi>' i \<noteq> x\<rbrakk> \<Longrightarrow> thesis; is_path ?\<pi>1; ?\<pi>1 0 = x; x \<noteq> local.return; ?\<pi>1 ?y1 = local.return\<rbrakk> \<Longrightarrow> thesis
\<lbrakk>is_path ?\<pi>'1; ?\<pi>'1 0 = x; ?\<pi>'1 ?n'1 = local.return; \<forall>i>0. ?\<pi>'1 i \<noteq> x\<rbrakk> \<Longrightarrow> thesis
is_path \<pi>
\<pi> 0 = x
x \<noteq> local.return
\<pi> n = local.return

goal (1 subgoal):
 1. \<And>n' \<pi>'. \<lbrakk>n' < n; is_path \<pi>'; \<pi>' 0 = x; \<pi>' n' = local.return\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?y1 < n; \<And>\<pi>' n'. \<lbrakk>is_path \<pi>'; \<pi>' 0 = x; \<pi>' n' = local.return; \<forall>i>0. \<pi>' i \<noteq> x\<rbrakk> \<Longrightarrow> thesis; is_path ?\<pi>1; ?\<pi>1 0 = x; x \<noteq> local.return; ?\<pi>1 ?y1 = local.return\<rbrakk> \<Longrightarrow> thesis
\<lbrakk>is_path ?\<pi>'1; ?\<pi>'1 0 = x; ?\<pi>'1 ?n'1 = local.return; \<forall>i>0. ?\<pi>'1 i \<noteq> x\<rbrakk> \<Longrightarrow> thesis
is_path \<pi>
\<pi> 0 = x
x \<noteq> local.return
\<pi> n = local.return
is_path \<pi>
\<pi> 0 = x
x \<noteq> local.return
\<pi> n = local.return

goal (1 subgoal):
 1. \<And>n' \<pi>'. \<lbrakk>n' < n; is_path \<pi>'; \<pi>' 0 = x; \<pi>' n' = local.return\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>?n'1 < n; is_path ?\<pi>'1; ?\<pi>'1 0 = x; ?\<pi>'1 ?n'1 = local.return\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. \<And>xa \<pi>. \<lbrakk>\<And>y \<pi>. \<lbrakk>y < xa; \<And>\<pi>' n'. \<lbrakk>is_path \<pi>'; \<pi>' 0 = x; \<pi>' n' = local.return; \<forall>i>0. \<pi>' i \<noteq> x\<rbrakk> \<Longrightarrow> thesis; is_path \<pi>; \<pi> 0 = x; x \<noteq> local.return; \<pi> y = local.return\<rbrakk> \<Longrightarrow> thesis; \<And>\<pi>' n'. \<lbrakk>is_path \<pi>'; \<pi>' 0 = x; \<pi>' n' = local.return; \<forall>i>0. \<pi>' i \<noteq> x\<rbrakk> \<Longrightarrow> thesis; is_path \<pi>; \<pi> 0 = x; x \<noteq> local.return; \<pi> xa = local.return\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
show \<open>thesis\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> thesis
 2. \<not> ?P \<Longrightarrow> thesis
[PROOF STEP]
assume \<open>\<forall> i>0. \<pi> i \<noteq> x\<close>
[PROOF STATE]
proof (state)
this:
\<forall>i>0. \<pi> i \<noteq> x

goal (2 subgoals):
 1. ?P \<Longrightarrow> thesis
 2. \<not> ?P \<Longrightarrow> thesis
[PROOF STEP]
thus \<open>thesis\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>i>0. \<pi> i \<noteq> x

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using less
[PROOF STATE]
proof (prove)
using this:
\<forall>i>0. \<pi> i \<noteq> x
\<lbrakk>?y1 < n; \<And>\<pi>' n'. \<lbrakk>is_path \<pi>'; \<pi>' 0 = x; \<pi>' n' = local.return; \<forall>i>0. \<pi>' i \<noteq> x\<rbrakk> \<Longrightarrow> thesis; is_path ?\<pi>1; ?\<pi>1 0 = x; x \<noteq> local.return; ?\<pi>1 ?y1 = local.return\<rbrakk> \<Longrightarrow> thesis
\<lbrakk>is_path ?\<pi>'1; ?\<pi>'1 0 = x; ?\<pi>'1 ?n'1 = local.return; \<forall>i>0. ?\<pi>'1 i \<noteq> x\<rbrakk> \<Longrightarrow> thesis
is_path \<pi>
\<pi> 0 = x
x \<noteq> local.return
\<pi> n = local.return

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

goal (1 subgoal):
 1. \<not> (\<forall>i>0. \<pi> i \<noteq> x) \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<forall>i>0. \<pi> i \<noteq> x) \<Longrightarrow> thesis
[PROOF STEP]
assume \<open>\<not> (\<forall> i>0. \<pi> i \<noteq> x)\<close>
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>i>0. \<pi> i \<noteq> x)

goal (1 subgoal):
 1. \<not> (\<forall>i>0. \<pi> i \<noteq> x) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<forall>i>0. \<pi> i \<noteq> x)
[PROOF STEP]
obtain i where \<open>0<i\<close> \<open>\<pi> i = x\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>i>0. \<pi> i \<noteq> x)

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>0 < i; \<pi> i = x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < i
\<pi> i = x

goal (1 subgoal):
 1. \<not> (\<forall>i>0. \<pi> i \<noteq> x) \<Longrightarrow> thesis
[PROOF STEP]
hence \<open>(\<pi>\<guillemotleft>i) 0 = x\<close>
[PROOF STATE]
proof (prove)
using this:
0 < i
\<pi> i = x

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

goal (1 subgoal):
 1. \<not> (\<forall>i>0. \<pi> i \<noteq> x) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<pi> \<guillemotleft> i) 0 = x

goal (1 subgoal):
 1. \<not> (\<forall>i>0. \<pi> i \<noteq> x) \<Longrightarrow> thesis
[PROOF STEP]
have \<open>i < n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < n
[PROOF STEP]
using less(3,5,6) \<open>\<pi> i = x\<close>
[PROOF STATE]
proof (prove)
using this:
is_path \<pi>
x \<noteq> local.return
\<pi> n = local.return
\<pi> i = x

goal (1 subgoal):
 1. i < n
[PROOF STEP]
by (metis linorder_neqE_nat term_path_stable less_imp_le)
[PROOF STATE]
proof (state)
this:
i < n

goal (1 subgoal):
 1. \<not> (\<forall>i>0. \<pi> i \<noteq> x) \<Longrightarrow> thesis
[PROOF STEP]
hence \<open>(\<pi>\<guillemotleft>i) (n-i) = return\<close>
[PROOF STATE]
proof (prove)
using this:
i < n

goal (1 subgoal):
 1. (\<pi> \<guillemotleft> i) (n - i) = local.return
[PROOF STEP]
using less(6)
[PROOF STATE]
proof (prove)
using this:
i < n
\<pi> n = local.return

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

goal (1 subgoal):
 1. \<not> (\<forall>i>0. \<pi> i \<noteq> x) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<pi> \<guillemotleft> i) (n - i) = local.return

goal (1 subgoal):
 1. \<not> (\<forall>i>0. \<pi> i \<noteq> x) \<Longrightarrow> thesis
[PROOF STEP]
have \<open>is_path (\<pi>\<guillemotleft>i)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_path (\<pi> \<guillemotleft> i)
[PROOF STEP]
using less(3)
[PROOF STATE]
proof (prove)
using this:
is_path \<pi>

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

goal (1 subgoal):
 1. \<not> (\<forall>i>0. \<pi> i \<noteq> x) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
is_path (\<pi> \<guillemotleft> i)

goal (1 subgoal):
 1. \<not> (\<forall>i>0. \<pi> i \<noteq> x) \<Longrightarrow> thesis
[PROOF STEP]
have \<open>n - i < n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n - i < n
[PROOF STEP]
using \<open>0<i\<close> \<open>i < n\<close>
[PROOF STATE]
proof (prove)
using this:
0 < i
i < n

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

goal (1 subgoal):
 1. \<not> (\<forall>i>0. \<pi> i \<noteq> x) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<pi> \<guillemotleft> i) 0 = x
(\<pi> \<guillemotleft> i) (n - i) = local.return
is_path (\<pi> \<guillemotleft> i)
n - i < n
[PROOF STEP]
show \<open>thesis\<close>
[PROOF STATE]
proof (prove)
using this:
(\<pi> \<guillemotleft> i) 0 = x
(\<pi> \<guillemotleft> i) (n - i) = local.return
is_path (\<pi> \<guillemotleft> i)
n - i < n

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using ih
[PROOF STATE]
proof (prove)
using this:
(\<pi> \<guillemotleft> i) 0 = x
(\<pi> \<guillemotleft> i) (n - i) = local.return
is_path (\<pi> \<guillemotleft> i)
n - i < n
\<lbrakk>?n'1 < n; is_path ?\<pi>'1; ?\<pi>'1 0 = x; ?\<pi>'1 ?n'1 = local.return\<rbrakk> \<Longrightarrow> thesis

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma direct_path_return: assumes  \<open>x \<in> nodes\<close> \<open>x \<noteq> return\<close>
obtains \<pi> n where \<open>is_path \<pi>\<close> \<open>\<pi> 0 = x\<close> \<open>\<pi> n = return\<close> \<open>\<forall> i> 0. \<pi> i \<noteq> x\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<pi> n. \<lbrakk>is_path \<pi>; \<pi> 0 = x; \<pi> n = local.return; \<forall>i>0. \<pi> i \<noteq> x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using direct_path_return'[of _ \<open>x\<close>] reaching_ret[OF assms(1)] assms(2)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_path ?\<pi>; ?\<pi> 0 = x; x \<noteq> local.return; ?\<pi> ?n = local.return; \<And>\<pi>' n'. \<lbrakk>is_path \<pi>'; \<pi>' 0 = x; \<pi>' n' = local.return; \<forall>i>0. \<pi>' i \<noteq> x\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
\<exists>\<pi> n. is_path \<pi> \<and> \<pi> 0 = x \<and> \<pi> n = local.return
x \<noteq> local.return

goal (1 subgoal):
 1. (\<And>\<pi> n. \<lbrakk>is_path \<pi>; \<pi> 0 = x; \<pi> n = local.return; \<forall>i>0. \<pi> i \<noteq> x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast


[STATEMENT]
lemma path_append_eq_up_to: \<open>(\<pi> @\<^bsup>k\<^esup> \<pi>') =\<^bsub>k\<^esub> \<pi>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<pi> @\<^bsup>k\<^esup> \<pi>') =\<^bsub>k\<^esub> \<pi>
[PROOF STEP]
unfolding eq_up_to_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i\<le>k. (\<pi> @\<^bsup>k\<^esup> \<pi>') i = \<pi> i
[PROOF STEP]
by auto


[STATEMENT]
lemma eq_up_to_le: assumes \<open>k \<le> n\<close> \<open>\<pi> =\<^bsub>n\<^esub>  \<pi>'\<close> shows \<open>\<pi> =\<^bsub>k\<^esub> \<pi>'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> =\<^bsub>k\<^esub> \<pi>'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
k \<le> n
\<pi> =\<^bsub>n\<^esub> \<pi>'

goal (1 subgoal):
 1. \<pi> =\<^bsub>k\<^esub> \<pi>'
[PROOF STEP]
unfolding eq_up_to_def
[PROOF STATE]
proof (prove)
using this:
k \<le> n
\<forall>i\<le>n. \<pi> i = \<pi>' i

goal (1 subgoal):
 1. \<forall>i\<le>k. \<pi> i = \<pi>' i
[PROOF STEP]
by auto


[STATEMENT]
lemma eq_up_to_refl: shows \<open>\<pi> =\<^bsub>k\<^esub> \<pi>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> =\<^bsub>k\<^esub> \<pi>
[PROOF STEP]
unfolding eq_up_to_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i\<le>k. \<pi> i = \<pi> i
[PROOF STEP]
by auto


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

goal (1 subgoal):
 1. \<pi>' =\<^bsub>k\<^esub> \<pi>
[PROOF STEP]
unfolding eq_up_to_def
[PROOF STATE]
proof (prove)
using this:
\<forall>i\<le>k. \<pi> i = \<pi>' i

goal (1 subgoal):
 1. \<forall>i\<le>k. \<pi>' i = \<pi> i
[PROOF STEP]
by auto


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

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

goal (1 subgoal):
 1. \<pi> j = \<pi>' j
[PROOF STEP]
by auto


[STATEMENT]
lemma path_swap_ret: assumes \<open>is_path \<pi>\<close> obtains \<pi>' n where \<open>is_path \<pi>'\<close> \<open>\<pi> =\<^bsub>k\<^esub> \<pi>'\<close> \<open>\<pi>' n = return\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<pi>' n. \<lbrakk>is_path \<pi>'; \<pi> =\<^bsub>k\<^esub> \<pi>'; \<pi>' n = local.return\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>\<pi>' n. \<lbrakk>is_path \<pi>'; \<pi> =\<^bsub>k\<^esub> \<pi>'; \<pi>' n = local.return\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have nd: \<open>\<pi> k \<in> nodes\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> k \<in> local.nodes
[PROOF STEP]
using assms path_nodes
[PROOF STATE]
proof (prove)
using this:
is_path \<pi>
is_path ?\<pi> \<Longrightarrow> ?\<pi> ?k \<in> local.nodes

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

goal (1 subgoal):
 1. (\<And>\<pi>' n. \<lbrakk>is_path \<pi>'; \<pi> =\<^bsub>k\<^esub> \<pi>'; \<pi>' n = local.return\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
obtain \<pi>' n where *: \<open>is_path \<pi>'\<close> \<open>\<pi>' 0 = \<pi> k\<close> \<open>\<pi>' n = return\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<pi>' n. \<lbrakk>is_path \<pi>'; \<pi>' 0 = \<pi> k; \<pi>' n = local.return\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using reaching_ret[OF nd]
[PROOF STATE]
proof (prove)
using this:
\<exists>\<pi>' n. is_path \<pi>' \<and> \<pi>' 0 = \<pi> k \<and> \<pi>' n = local.return

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

goal (1 subgoal):
 1. (\<And>\<pi>' n. \<lbrakk>is_path \<pi>'; \<pi> =\<^bsub>k\<^esub> \<pi>'; \<pi>' n = local.return\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have \<open>\<pi> =\<^bsub>k\<^esub> (\<pi>@\<^bsup>k\<^esup> \<pi>')\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> =\<^bsub>k\<^esub> (\<pi> @\<^bsup>k\<^esup> \<pi>')
[PROOF STEP]
by (metis eq_up_to_sym path_append_eq_up_to)
[PROOF STATE]
proof (state)
this:
\<pi> =\<^bsub>k\<^esub> (\<pi> @\<^bsup>k\<^esup> \<pi>')

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

goal (1 subgoal):
 1. (\<And>\<pi>' n. \<lbrakk>is_path \<pi>'; \<pi> =\<^bsub>k\<^esub> \<pi>'; \<pi>' n = local.return\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have \<open>is_path (\<pi>@\<^bsup>k\<^esup> \<pi>')\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_path (\<pi> @\<^bsup>k\<^esup> \<pi>')
[PROOF STEP]
using assms * path_cons
[PROOF STATE]
proof (prove)
using this:
is_path \<pi>
is_path \<pi>'
\<pi>' 0 = \<pi> k
\<pi>' n = local.return
\<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> @\<^bsup>k\<^esup> \<pi>')
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
is_path (\<pi> @\<^bsup>k\<^esup> \<pi>')

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

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

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

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

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
\<pi> =\<^bsub>k\<^esub> (\<pi> @\<^bsup>k\<^esup> \<pi>')
is_path (\<pi> @\<^bsup>k\<^esup> \<pi>')
(\<pi> @\<^bsup>k\<^esup> \<pi>') (k + n) = local.return
\<lbrakk>is_path ?\<pi>'1; \<pi> =\<^bsub>k\<^esub> ?\<pi>'1; ?\<pi>'1 ?n1 = local.return\<rbrakk> \<Longrightarrow> thesis

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma path_suc: \<open>path \<sigma> (Suc k) = fst (step (path \<sigma> k, \<sigma>\<^bsup>k\<^esup>))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path \<sigma> (Suc k) = fst (local.step (path \<sigma> k, \<sigma>\<^bsup>k\<^esup>))
[PROOF STEP]
by (induction \<open>k\<close>, auto simp: path_def kth_state_def)


[STATEMENT]
lemma kth_state_suc: \<open>\<sigma>\<^bsup>Suc k\<^esup>  = snd (step (path \<sigma> k, \<sigma>\<^bsup>k\<^esup>))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma>\<^bsup>Suc k\<^esup> = snd (local.step (path \<sigma> k, \<sigma>\<^bsup>k\<^esup>))
[PROOF STEP]
by (induction \<open>k\<close>, auto simp: path_def kth_state_def)


[STATEMENT]
lemma pd_trans: assumes 1: \<open>y pd\<rightarrow> x\<close> and 2: \<open>z pd\<rightarrow>y\<close> shows \<open>z pd\<rightarrow>x\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z pd\<rightarrow> x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. z pd\<rightarrow> x
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. z pd\<rightarrow> x
[PROOF STEP]
fix \<pi> n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. z pd\<rightarrow> x
[PROOF STEP]
assume 3[simp]: \<open>is_path \<pi>\<close> \<open>\<pi> 0 = x\<close> \<open>\<pi> n = return\<close>
[PROOF STATE]
proof (state)
this:
is_path \<pi>
\<pi> 0 = x
\<pi> n = local.return

goal (1 subgoal):
 1. z pd\<rightarrow> x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_path \<pi>
\<pi> 0 = x
\<pi> n = local.return
[PROOF STEP]
obtain k where \<open>\<pi> k = y\<close> and 7: \<open>k \<le> n\<close>
[PROOF STATE]
proof (prove)
using this:
is_path \<pi>
\<pi> 0 = x
\<pi> n = local.return

goal (1 subgoal):
 1. (\<And>k. \<lbrakk>\<pi> k = y; k \<le> n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
is_path \<pi>
\<pi> 0 = x
\<pi> n = local.return
y pd\<rightarrow> x

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

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

goal (1 subgoal):
 1. z pd\<rightarrow> x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<pi> k = y
k \<le> n
[PROOF STEP]
have \<open>(\<pi>\<guillemotleft>k) 0 = y\<close> and \<open>(\<pi>\<guillemotleft>k) (n-k) = return\<close>
[PROOF STATE]
proof (prove)
using this:
\<pi> k = y
k \<le> n

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

goal (1 subgoal):
 1. z pd\<rightarrow> x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<pi> \<guillemotleft> k) 0 = y
(\<pi> \<guillemotleft> k) (n - k) = local.return

goal (1 subgoal):
 1. z pd\<rightarrow> x
[PROOF STEP]
have \<open>is_path (\<pi>\<guillemotleft>k)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_path (\<pi> \<guillemotleft> k)
[PROOF STEP]
by(metis 3(1) path_path_shift)
[PROOF STATE]
proof (state)
this:
is_path (\<pi> \<guillemotleft> k)

goal (1 subgoal):
 1. z pd\<rightarrow> x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<pi> \<guillemotleft> k) 0 = y
(\<pi> \<guillemotleft> k) (n - k) = local.return
is_path (\<pi> \<guillemotleft> k)
[PROOF STEP]
obtain k' where 8: \<open>(\<pi>\<guillemotleft>k) k' = z\<close> and \<open>k' \<le> n-k\<close>
[PROOF STATE]
proof (prove)
using this:
(\<pi> \<guillemotleft> k) 0 = y
(\<pi> \<guillemotleft> k) (n - k) = local.return
is_path (\<pi> \<guillemotleft> k)

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

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

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

goal (1 subgoal):
 1. z pd\<rightarrow> x
[PROOF STEP]
hence \<open>k+k'\<le>n\<close> and \<open>\<pi> (k+ k') = z\<close>
[PROOF STATE]
proof (prove)
using this:
(\<pi> \<guillemotleft> k) k' = z
k' \<le> n - k

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

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

goal (1 subgoal):
 1. z pd\<rightarrow> x
[PROOF STEP]
hence \<open>\<exists>k\<le>n. \<pi> k = z\<close>
[PROOF STATE]
proof (prove)
using this:
k + k' \<le> n
\<pi> (k + k') = z

goal (1 subgoal):
 1. \<exists>k\<le>n. \<pi> k = z
[PROOF STEP]
using path_nodes
[PROOF STATE]
proof (prove)
using this:
k + k' \<le> n
\<pi> (k + k') = z
is_path ?\<pi> \<Longrightarrow> ?\<pi> ?k \<in> local.nodes

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

goal (1 subgoal):
 1. z pd\<rightarrow> x
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>is_path ?\<pi>3; ?\<pi>3 0 = x; ?\<pi>3 ?n3 = local.return\<rbrakk> \<Longrightarrow> \<exists>k\<le>?n3. ?\<pi>3 k = z

goal (1 subgoal):
 1. z pd\<rightarrow> x
[PROOF STEP]
thus \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_path ?\<pi>3; ?\<pi>3 0 = x; ?\<pi>3 ?n3 = local.return\<rbrakk> \<Longrightarrow> \<exists>k\<le>?n3. ?\<pi>3 k = z

goal (1 subgoal):
 1. z pd\<rightarrow> x
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_path ?\<pi>3; ?\<pi>3 0 = x; ?\<pi>3 ?n3 = local.return\<rbrakk> \<Longrightarrow> \<exists>k\<le>?n3. ?\<pi>3 k = z
y pd\<rightarrow> x

goal (1 subgoal):
 1. z pd\<rightarrow> x
[PROOF STEP]
unfolding is_pd_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_path ?\<pi>3; ?\<pi>3 0 = x; ?\<pi>3 ?n3 = local.return\<rbrakk> \<Longrightarrow> \<exists>k\<le>?n3. ?\<pi>3 k = z
x \<in> local.nodes \<and> (\<forall>\<pi> n. is_path \<pi> \<and> \<pi> 0 = x \<and> \<pi> n = local.return \<longrightarrow> (\<exists>k\<le>n. \<pi> k = y))

goal (1 subgoal):
 1. x \<in> local.nodes \<and> (\<forall>\<pi> n. is_path \<pi> \<and> \<pi> 0 = x \<and> \<pi> n = local.return \<longrightarrow> (\<exists>k\<le>n. \<pi> k = z))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
z pd\<rightarrow> x

goal:
No subgoals!
[PROOF STEP]
qed


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

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

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

goal (1 subgoal):
 1. (\<And>\<pi> n k. \<lbrakk>is_path \<pi>; \<pi> 0 = x; \<pi> n = local.return; \<pi> k = y; k \<le> n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast


[STATEMENT]
lemma pd_antisym: assumes xpdy: \<open>x pd\<rightarrow> y\<close> and ypdx: \<open>y pd\<rightarrow> x\<close> shows \<open>x = y\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x = y
[PROOF STEP]
obtain \<pi> n where path: \<open>is_path \<pi>\<close> and \<pi>0: \<open>\<pi> 0 = x\<close> and \<pi>n: \<open>\<pi> n = return\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<pi> n. \<lbrakk>is_path \<pi>; \<pi> 0 = x; \<pi> n = local.return\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using pd_path[OF ypdx]
[PROOF STATE]
proof (prove)
using this:
(\<And>\<pi> n k. \<lbrakk>is_path \<pi>; \<pi> 0 = x; \<pi> n = local.return; \<pi> k = y; k \<le> n\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

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

goal (1 subgoal):
 1. x = y
[PROOF STEP]
hence kex: \<open>\<exists>k\<le>n. \<pi> k = y\<close>
[PROOF STATE]
proof (prove)
using this:
is_path \<pi>
\<pi> 0 = x
\<pi> n = local.return

goal (1 subgoal):
 1. \<exists>k\<le>n. \<pi> k = y
[PROOF STEP]
using ypdx
[PROOF STATE]
proof (prove)
using this:
is_path \<pi>
\<pi> 0 = x
\<pi> n = local.return
y pd\<rightarrow> x

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

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

goal (1 subgoal):
 1. x = y
[PROOF STEP]
obtain k where k: \<open>k = (GREATEST k. k\<le>n \<and> \<pi> k = y)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k. k = (GREATEST k. k \<le> n \<and> \<pi> k = y) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
k = (GREATEST k. k \<le> n \<and> \<pi> k = y)

goal (1 subgoal):
 1. x = y
[PROOF STEP]
have \<pi>k: \<open>\<pi> k = y\<close> and kn: \<open>k \<le> n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> k = y &&& k \<le> n
[PROOF STEP]
using k kex
[PROOF STATE]
proof (prove)
using this:
k = (GREATEST k. k \<le> n \<and> \<pi> k = y)
\<exists>k\<le>n. \<pi> k = y

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

goal (1 subgoal):
 1. x = y
[PROOF STEP]
have kpath: \<open>is_path (\<pi>\<guillemotleft>k)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_path (\<pi> \<guillemotleft> k)
[PROOF STEP]
by (metis path_path_shift path)
[PROOF STATE]
proof (state)
this:
is_path (\<pi> \<guillemotleft> k)

goal (1 subgoal):
 1. x = y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
is_path (\<pi> \<guillemotleft> k)

goal (1 subgoal):
 1. x = y
[PROOF STEP]
have k0: \<open>(\<pi>\<guillemotleft>k) 0 = y\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<pi> \<guillemotleft> k) 0 = y
[PROOF STEP]
using \<pi>k
[PROOF STATE]
proof (prove)
using this:
\<pi> k = y

goal (1 subgoal):
 1. (\<pi> \<guillemotleft> k) 0 = y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<pi> \<guillemotleft> k) 0 = y

goal (1 subgoal):
 1. x = y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<pi> \<guillemotleft> k) 0 = y

goal (1 subgoal):
 1. x = y
[PROOF STEP]
have kreturn: \<open>(\<pi>\<guillemotleft>k) (n-k) = return\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<pi> \<guillemotleft> k) (n - k) = local.return
[PROOF STEP]
using kn \<pi>n
[PROOF STATE]
proof (prove)
using this:
k \<le> n
\<pi> n = local.return

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

goal (1 subgoal):
 1. x = y
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
is_path (\<pi> \<guillemotleft> k)
(\<pi> \<guillemotleft> k) 0 = y
(\<pi> \<guillemotleft> k) (n - k) = local.return
[PROOF STEP]
have ky': \<open>\<exists>k'\<le>(n-k).(\<pi>\<guillemotleft>k) k' = x\<close>
[PROOF STATE]
proof (prove)
using this:
is_path (\<pi> \<guillemotleft> k)
(\<pi> \<guillemotleft> k) 0 = y
(\<pi> \<guillemotleft> k) (n - k) = local.return

goal (1 subgoal):
 1. \<exists>k'\<le>n - k. (\<pi> \<guillemotleft> k) k' = x
[PROOF STEP]
using xpdy
[PROOF STATE]
proof (prove)
using this:
is_path (\<pi> \<guillemotleft> k)
(\<pi> \<guillemotleft> k) 0 = y
(\<pi> \<guillemotleft> k) (n - k) = local.return
x pd\<rightarrow> y

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

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

goal (1 subgoal):
 1. x = y
[PROOF STEP]
obtain k' where k': \<open>k' = (GREATEST k'. k'\<le>(n-k) \<and> (\<pi>\<guillemotleft>k) k' = x)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k'. k' = (GREATEST k'. k' \<le> n - k \<and> (\<pi> \<guillemotleft> k) k' = x) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
k' = (GREATEST k'. k' \<le> n - k \<and> (\<pi> \<guillemotleft> k) k' = x)

goal (1 subgoal):
 1. x = y
[PROOF STEP]
with ky'
[PROOF STATE]
proof (chain)
picking this:
\<exists>k'\<le>n - k. (\<pi> \<guillemotleft> k) k' = x
k' = (GREATEST k'. k' \<le> n - k \<and> (\<pi> \<guillemotleft> k) k' = x)
[PROOF STEP]
have \<pi>k': \<open>(\<pi>\<guillemotleft>k) k' = x\<close> and kn': \<open>k' \<le> (n-k)\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>k'\<le>n - k. (\<pi> \<guillemotleft> k) k' = x
k' = (GREATEST k'. k' \<le> n - k \<and> (\<pi> \<guillemotleft> k) k' = x)

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

goal (1 subgoal):
 1. x = y
[PROOF STEP]
have k'path: \<open>is_path (\<pi>\<guillemotleft>k\<guillemotleft>k')\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_path (\<pi> \<guillemotleft> k \<guillemotleft> k')
[PROOF STEP]
using kpath
[PROOF STATE]
proof (prove)
using this:
is_path (\<pi> \<guillemotleft> k)

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

goal (1 subgoal):
 1. x = y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
is_path (\<pi> \<guillemotleft> k \<guillemotleft> k')

goal (1 subgoal):
 1. x = y
[PROOF STEP]
have k'0: \<open>(\<pi>\<guillemotleft>k\<guillemotleft>k') 0 = x\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<pi> \<guillemotleft> k \<guillemotleft> k') 0 = x
[PROOF STEP]
using \<pi>k'
[PROOF STATE]
proof (prove)
using this:
(\<pi> \<guillemotleft> k) k' = x

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

goal (1 subgoal):
 1. x = y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<pi> \<guillemotleft> k \<guillemotleft> k') 0 = x

goal (1 subgoal):
 1. x = y
[PROOF STEP]
have k'return: \<open>(\<pi>\<guillemotleft>k\<guillemotleft>k') (n-k-k') = return\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<pi> \<guillemotleft> k \<guillemotleft> k') (n - k - k') = local.return
[PROOF STEP]
using kn' kreturn
[PROOF STATE]
proof (prove)
using this:
k' \<le> n - k
(\<pi> \<guillemotleft> k) (n - k) = local.return

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

goal (1 subgoal):
 1. x = y
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
is_path (\<pi> \<guillemotleft> k \<guillemotleft> k')
(\<pi> \<guillemotleft> k \<guillemotleft> k') 0 = x
(\<pi> \<guillemotleft> k \<guillemotleft> k') (n - k - k') = local.return
[PROOF STEP]
have ky'': \<open>\<exists>k''\<le>(n-k-k').(\<pi>\<guillemotleft>k\<guillemotleft>k') k'' = y\<close>
[PROOF STATE]
proof (prove)
using this:
is_path (\<pi> \<guillemotleft> k \<guillemotleft> k')
(\<pi> \<guillemotleft> k \<guillemotleft> k') 0 = x
(\<pi> \<guillemotleft> k \<guillemotleft> k') (n - k - k') = local.return

goal (1 subgoal):
 1. \<exists>k''\<le>n - k - k'. (\<pi> \<guillemotleft> k \<guillemotleft> k') k'' = y
[PROOF STEP]
using ypdx
[PROOF STATE]
proof (prove)
using this:
is_path (\<pi> \<guillemotleft> k \<guillemotleft> k')
(\<pi> \<guillemotleft> k \<guillemotleft> k') 0 = x
(\<pi> \<guillemotleft> k \<guillemotleft> k') (n - k - k') = local.return
y pd\<rightarrow> x

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

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

goal (1 subgoal):
 1. x = y
[PROOF STEP]
obtain k'' where k'': \<open>k''= (GREATEST k''. k''\<le>(n-k-k') \<and> (\<pi>\<guillemotleft>k\<guillemotleft>k') k'' = y)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k''. k'' = (GREATEST k''. k'' \<le> n - k - k' \<and> (\<pi> \<guillemotleft> k \<guillemotleft> k') k'' = y) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
k'' = (GREATEST k''. k'' \<le> n - k - k' \<and> (\<pi> \<guillemotleft> k \<guillemotleft> k') k'' = y)

goal (1 subgoal):
 1. x = y
[PROOF STEP]
with ky''
[PROOF STATE]
proof (chain)
picking this:
\<exists>k''\<le>n - k - k'. (\<pi> \<guillemotleft> k \<guillemotleft> k') k'' = y
k'' = (GREATEST k''. k'' \<le> n - k - k' \<and> (\<pi> \<guillemotleft> k \<guillemotleft> k') k'' = y)
[PROOF STEP]
have \<pi>k'': \<open>(\<pi>\<guillemotleft>k\<guillemotleft>k') k'' = y\<close> and kn'': \<open>k'' \<le> (n-k-k')\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>k''\<le>n - k - k'. (\<pi> \<guillemotleft> k \<guillemotleft> k') k'' = y
k'' = (GREATEST k''. k'' \<le> n - k - k' \<and> (\<pi> \<guillemotleft> k \<guillemotleft> k') k'' = y)

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

goal (1 subgoal):
 1. x = y
[PROOF STEP]
from this(1)
[PROOF STATE]
proof (chain)
picking this:
(\<pi> \<guillemotleft> k \<guillemotleft> k') k'' = y
[PROOF STEP]
have  \<open>\<pi> (k + k' + k'') = y\<close>
[PROOF STATE]
proof (prove)
using this:
(\<pi> \<guillemotleft> k \<guillemotleft> k') k'' = y

goal (1 subgoal):
 1. \<pi> (k + k' + k'') = y
[PROOF STEP]
by (metis path_shift_def add.commute add.left_commute)
[PROOF STATE]
proof (state)
this:
\<pi> (k + k' + k'') = y

goal (1 subgoal):
 1. x = y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<pi> (k + k' + k'') = y

goal (1 subgoal):
 1. x = y
[PROOF STEP]
have \<open>k + k' +k'' \<le> n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k + k' + k'' \<le> n
[PROOF STEP]
using kn'' kn' kn
[PROOF STATE]
proof (prove)
using this:
k'' \<le> n - k - k'
k' \<le> n - k
k \<le> n

goal (1 subgoal):
 1. k + k' + k'' \<le> n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
k + k' + k'' \<le> n

goal (1 subgoal):
 1. x = y
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<pi> (k + k' + k'') = y
k + k' + k'' \<le> n
[PROOF STEP]
have \<open>k + k' + k''\<le> k\<close>
[PROOF STATE]
proof (prove)
using this:
\<pi> (k + k' + k'') = y
k + k' + k'' \<le> n

goal (1 subgoal):
 1. k + k' + k'' \<le> k
[PROOF STEP]
using k
[PROOF STATE]
proof (prove)
using this:
\<pi> (k + k' + k'') = y
k + k' + k'' \<le> n
k = (GREATEST k. k \<le> n \<and> \<pi> k = y)

goal (1 subgoal):
 1. k + k' + k'' \<le> k
[PROOF STEP]
by(auto simp: GreatestB_le)
[PROOF STATE]
proof (state)
this:
k + k' + k'' \<le> k

goal (1 subgoal):
 1. x = y
[PROOF STEP]
hence \<open>k' = 0\<close>
[PROOF STATE]
proof (prove)
using this:
k + k' + k'' \<le> k

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

goal (1 subgoal):
 1. x = y
[PROOF STEP]
with k0 \<pi>k'
[PROOF STATE]
proof (chain)
picking this:
(\<pi> \<guillemotleft> k) 0 = y
(\<pi> \<guillemotleft> k) k' = x
k' = 0
[PROOF STEP]
show \<open>x = y\<close>
[PROOF STATE]
proof (prove)
using this:
(\<pi> \<guillemotleft> k) 0 = y
(\<pi> \<guillemotleft> k) k' = x
k' = 0

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pd_refl[simp]: \<open>x \<in> nodes \<Longrightarrow> x pd\<rightarrow> x\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> local.nodes \<Longrightarrow> x pd\<rightarrow> x
[PROOF STEP]
unfolding is_pd_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> local.nodes \<Longrightarrow> x \<in> local.nodes \<and> (\<forall>\<pi> n. is_path \<pi> \<and> \<pi> 0 = x \<and> \<pi> n = local.return \<longrightarrow> (\<exists>k\<le>n. \<pi> k = x))
[PROOF STEP]
by blast


[STATEMENT]
lemma pdt_trans_in_pdt: \<open>(x,y) \<in> pdt\<^sup>+ \<Longrightarrow> (x,y) \<in> pdt\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x, y) \<in> pdt\<^sup>+ \<Longrightarrow> (x, y) \<in> pdt
[PROOF STEP]
proof (induction rule: trancl_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>y. (x, y) \<in> pdt \<Longrightarrow> (x, y) \<in> pdt
 2. \<And>y z. \<lbrakk>(x, y) \<in> pdt\<^sup>+; (y, z) \<in> pdt; (x, y) \<in> pdt\<rbrakk> \<Longrightarrow> (x, z) \<in> pdt
[PROOF STEP]
case base
[PROOF STATE]
proof (state)
this:
(x, y_) \<in> pdt

goal (2 subgoals):
 1. \<And>y. (x, y) \<in> pdt \<Longrightarrow> (x, y) \<in> pdt
 2. \<And>y z. \<lbrakk>(x, y) \<in> pdt\<^sup>+; (y, z) \<in> pdt; (x, y) \<in> pdt\<rbrakk> \<Longrightarrow> (x, z) \<in> pdt
[PROOF STEP]
thus \<open>?case\<close>
[PROOF STATE]
proof (prove)
using this:
(x, y_) \<in> pdt

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

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(x, y) \<in> pdt\<^sup>+; (y, z) \<in> pdt; (x, y) \<in> pdt\<rbrakk> \<Longrightarrow> (x, z) \<in> pdt
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(x, y) \<in> pdt\<^sup>+; (y, z) \<in> pdt; (x, y) \<in> pdt\<rbrakk> \<Longrightarrow> (x, z) \<in> pdt
[PROOF STEP]
case (step y z)
[PROOF STATE]
proof (state)
this:
(x, y) \<in> pdt\<^sup>+
(y, z) \<in> pdt
(x, y) \<in> pdt

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(x, y) \<in> pdt\<^sup>+; (y, z) \<in> pdt; (x, y) \<in> pdt\<rbrakk> \<Longrightarrow> (x, z) \<in> pdt
[PROOF STEP]
show \<open>?case\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x, z) \<in> pdt
[PROOF STEP]
unfolding pdt_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x, z) \<in> {(x, y). x \<noteq> y \<and> y pd\<rightarrow> x}
[PROOF STEP]
proof (simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<noteq> z \<and> z pd\<rightarrow> x
[PROOF STEP]
have *: \<open>y pd\<rightarrow> x\<close> \<open>z pd\<rightarrow> y\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y pd\<rightarrow> x &&& z pd\<rightarrow> y
[PROOF STEP]
using step
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> pdt\<^sup>+
(y, z) \<in> pdt
(x, y) \<in> pdt

goal (1 subgoal):
 1. y pd\<rightarrow> x &&& z pd\<rightarrow> y
[PROOF STEP]
unfolding pdt_def
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> {(x, y). x \<noteq> y \<and> y pd\<rightarrow> x}\<^sup>+
(y, z) \<in> {(x, y). x \<noteq> y \<and> y pd\<rightarrow> x}
(x, y) \<in> {(x, y). x \<noteq> y \<and> y pd\<rightarrow> x}

goal (1 subgoal):
 1. y pd\<rightarrow> x &&& z pd\<rightarrow> y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y pd\<rightarrow> x
z pd\<rightarrow> y

goal (1 subgoal):
 1. x \<noteq> z \<and> z pd\<rightarrow> x
[PROOF STEP]
hence [simp]: \<open>z pd\<rightarrow> x\<close>
[PROOF STATE]
proof (prove)
using this:
y pd\<rightarrow> x
z pd\<rightarrow> y

goal (1 subgoal):
 1. z pd\<rightarrow> x
[PROOF STEP]
using pd_trans[where x=\<open>x\<close> and y=\<open>y\<close> and z=\<open>z\<close>]
[PROOF STATE]
proof (prove)
using this:
y pd\<rightarrow> x
z pd\<rightarrow> y
\<lbrakk>y pd\<rightarrow> x; z pd\<rightarrow> y\<rbrakk> \<Longrightarrow> z pd\<rightarrow> x

goal (1 subgoal):
 1. z pd\<rightarrow> x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
z pd\<rightarrow> x

goal (1 subgoal):
 1. x \<noteq> z \<and> z pd\<rightarrow> x
[PROOF STEP]
have \<open>x\<noteq>z\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<noteq> z
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x = z \<Longrightarrow> False
[PROOF STEP]
assume \<open>x = z\<close>
[PROOF STATE]
proof (state)
this:
x = z

goal (1 subgoal):
 1. x = z \<Longrightarrow> False
[PROOF STEP]
hence \<open>z pd\<rightarrow> y\<close> \<open>y pd\<rightarrow> z\<close>
[PROOF STATE]
proof (prove)
using this:
x = z

goal (1 subgoal):
 1. z pd\<rightarrow> y &&& y pd\<rightarrow> z
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
x = z
y pd\<rightarrow> x
z pd\<rightarrow> y

goal (1 subgoal):
 1. z pd\<rightarrow> y &&& y pd\<rightarrow> z
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z pd\<rightarrow> y
y pd\<rightarrow> z

goal (1 subgoal):
 1. x = z \<Longrightarrow> False
[PROOF STEP]
hence \<open>z = y\<close>
[PROOF STATE]
proof (prove)
using this:
z pd\<rightarrow> y
y pd\<rightarrow> z

goal (1 subgoal):
 1. z = y
[PROOF STEP]
using pd_antisym
[PROOF STATE]
proof (prove)
using this:
z pd\<rightarrow> y
y pd\<rightarrow> z
\<lbrakk>?x pd\<rightarrow> ?y; ?y pd\<rightarrow> ?x\<rbrakk> \<Longrightarrow> ?x = ?y

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

goal (1 subgoal):
 1. x = z \<Longrightarrow> False
[PROOF STEP]
thus \<open>False\<close>
[PROOF STATE]
proof (prove)
using this:
z = y

goal (1 subgoal):
 1. False
[PROOF STEP]
using step(2)
[PROOF STATE]
proof (prove)
using this:
z = y
(y, z) \<in> pdt

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding pdt_def
[PROOF STATE]
proof (prove)
using this:
z = y
(y, z) \<in> {(x, y). x \<noteq> y \<and> y pd\<rightarrow> x}

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<noteq> z

goal (1 subgoal):
 1. x \<noteq> z \<and> z pd\<rightarrow> x
[PROOF STEP]
thus \<open>x \<noteq> z \<and> z pd\<rightarrow> x\<close>
[PROOF STATE]
proof (prove)
using this:
x \<noteq> z

goal (1 subgoal):
 1. x \<noteq> z \<and> z pd\<rightarrow> x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<noteq> z \<and> z pd\<rightarrow> x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(x, z) \<in> pdt

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pdt_trancl_pdt: \<open>pdt\<^sup>+ = pdt\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pdt\<^sup>+ = pdt
[PROOF STEP]
using pdt_trans_in_pdt
[PROOF STATE]
proof (prove)
using this:
(?x, ?y) \<in> pdt\<^sup>+ \<Longrightarrow> (?x, ?y) \<in> pdt

goal (1 subgoal):
 1. pdt\<^sup>+ = pdt
[PROOF STEP]
by fast


[STATEMENT]
lemma trans_pdt: \<open>trans pdt\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trans pdt
[PROOF STEP]
by (metis pdt_trancl_pdt trans_trancl)


[STATEMENT]
lemma wf_pdt_inv: \<open>wf (pdt_inv)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf pdt_inv
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> wf pdt_inv \<Longrightarrow> False
[PROOF STEP]
assume \<open>\<not> wf (pdt_inv)\<close>
[PROOF STATE]
proof (state)
this:
\<not> wf pdt_inv

goal (1 subgoal):
 1. \<not> wf pdt_inv \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> wf pdt_inv
[PROOF STEP]
obtain f where  \<open>\<forall>i. (f (Suc i), f i) \<in> pdt\<inverse>\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> wf pdt_inv

goal (1 subgoal):
 1. (\<And>f. \<forall>i. (f (Suc i), f i) \<in> pdt\<inverse> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using wf_iff_no_infinite_down_chain
[PROOF STATE]
proof (prove)
using this:
\<not> wf pdt_inv
wf ?r = (\<nexists>f. \<forall>i. (f (Suc i), f i) \<in> ?r)

goal (1 subgoal):
 1. (\<And>f. \<forall>i. (f (Suc i), f i) \<in> pdt\<inverse> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<forall>i. (f (Suc i), f i) \<in> pdt\<inverse>

goal (1 subgoal):
 1. \<not> wf pdt_inv \<Longrightarrow> False
[PROOF STEP]
hence *: \<open>\<forall> i. (f i, f (Suc i)) \<in> pdt\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>i. (f (Suc i), f i) \<in> pdt\<inverse>

goal (1 subgoal):
 1. \<forall>i. (f i, f (Suc i)) \<in> pdt
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>i. (f i, f (Suc i)) \<in> pdt

goal (1 subgoal):
 1. \<not> wf pdt_inv \<Longrightarrow> False
[PROOF STEP]
have **:\<open>\<forall> i. \<forall> j>i. (f i, f j) \<in> pdt\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i j. i < j \<longrightarrow> (f i, f j) \<in> pdt
[PROOF STEP]
proof(rule,rule,rule)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. i < j \<Longrightarrow> (f i, f j) \<in> pdt
[PROOF STEP]
fix i j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. i < j \<Longrightarrow> (f i, f j) \<in> pdt
[PROOF STEP]
assume  \<open>i < (j::nat)\<close>
[PROOF STATE]
proof (state)
this:
i < j

goal (1 subgoal):
 1. \<And>i j. i < j \<Longrightarrow> (f i, f j) \<in> pdt
[PROOF STEP]
thus \<open>(f i, f j) \<in> pdt\<close>
[PROOF STATE]
proof (prove)
using this:
i < j

goal (1 subgoal):
 1. (f i, f j) \<in> pdt
[PROOF STEP]
proof (induction \<open>j\<close> rule: less_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>y < x; i < y\<rbrakk> \<Longrightarrow> (f i, f y) \<in> pdt; i < x\<rbrakk> \<Longrightarrow> (f i, f x) \<in> pdt
[PROOF STEP]
case (less k)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?y1 < k; i < ?y1\<rbrakk> \<Longrightarrow> (f i, f ?y1) \<in> pdt
i < k

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>y < x; i < y\<rbrakk> \<Longrightarrow> (f i, f y) \<in> pdt; i < x\<rbrakk> \<Longrightarrow> (f i, f x) \<in> pdt
[PROOF STEP]
show \<open>?case\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f i, f k) \<in> pdt
[PROOF STEP]
proof (cases \<open>Suc i < k\<close>)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Suc i < k \<Longrightarrow> (f i, f k) \<in> pdt
 2. \<not> Suc i < k \<Longrightarrow> (f i, f k) \<in> pdt
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
Suc i < k

goal (2 subgoals):
 1. Suc i < k \<Longrightarrow> (f i, f k) \<in> pdt
 2. \<not> Suc i < k \<Longrightarrow> (f i, f k) \<in> pdt
[PROOF STEP]
hence k:\<open>k-1 < k\<close> \<open>i < k-1\<close> and sk: \<open>Suc (k-1) = k\<close>
[PROOF STATE]
proof (prove)
using this:
Suc i < k

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

goal (2 subgoals):
 1. Suc i < k \<Longrightarrow> (f i, f k) \<in> pdt
 2. \<not> Suc i < k \<Longrightarrow> (f i, f k) \<in> pdt
[PROOF STEP]
show \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f i, f k) \<in> pdt
[PROOF STEP]
using less(1)[OF k] *[rule_format,of \<open>k-1\<close>,unfolded sk] trans_pdt[unfolded trans_def]
[PROOF STATE]
proof (prove)
using this:
(f i, f (k - 1)) \<in> pdt
(f (k - 1), f k) \<in> pdt
\<forall>x y z. (x, y) \<in> pdt \<longrightarrow> (y, z) \<in> pdt \<longrightarrow> (x, z) \<in> pdt

goal (1 subgoal):
 1. (f i, f k) \<in> pdt
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(f i, f k) \<in> pdt

goal (1 subgoal):
 1. \<not> Suc i < k \<Longrightarrow> (f i, f k) \<in> pdt
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> Suc i < k \<Longrightarrow> (f i, f k) \<in> pdt
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> Suc i < k

goal (1 subgoal):
 1. \<not> Suc i < k \<Longrightarrow> (f i, f k) \<in> pdt
[PROOF STEP]
hence \<open>Suc i = k\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> Suc i < k

goal (1 subgoal):
 1. Suc i = k
[PROOF STEP]
using less(2)
[PROOF STATE]
proof (prove)
using this:
\<not> Suc i < k
i < k

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

goal (1 subgoal):
 1. \<not> Suc i < k \<Longrightarrow> (f i, f k) \<in> pdt
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Suc i = k
[PROOF STEP]
show \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
Suc i = k

goal (1 subgoal):
 1. (f i, f k) \<in> pdt
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
Suc i = k
\<forall>i. (f i, f (Suc i)) \<in> pdt

goal (1 subgoal):
 1. (f i, f k) \<in> pdt
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(f i, f k) \<in> pdt

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(f i, f k) \<in> pdt

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(f i, f j) \<in> pdt

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>i j. i < j \<longrightarrow> (f i, f j) \<in> pdt

goal (1 subgoal):
 1. \<not> wf pdt_inv \<Longrightarrow> False
[PROOF STEP]
hence ***:\<open>\<forall> i. \<forall> j > i. f j pd\<rightarrow> f i\<close> \<open>\<forall> i. \<forall> j > i. f i \<noteq>  f j\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>i j. i < j \<longrightarrow> (f i, f j) \<in> pdt

goal (1 subgoal):
 1. \<forall>i j. i < j \<longrightarrow> f j pd\<rightarrow> f i &&& \<forall>i j. i < j \<longrightarrow> f i \<noteq> f j
[PROOF STEP]
unfolding pdt_def
[PROOF STATE]
proof (prove)
using this:
\<forall>i j. i < j \<longrightarrow> (f i, f j) \<in> {(x, y). x \<noteq> y \<and> y pd\<rightarrow> x}

goal (1 subgoal):
 1. \<forall>i j. i < j \<longrightarrow> f j pd\<rightarrow> f i &&& \<forall>i j. i < j \<longrightarrow> f i \<noteq> f j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>i j. i < j \<longrightarrow> f j pd\<rightarrow> f i
\<forall>i j. i < j \<longrightarrow> f i \<noteq> f j

goal (1 subgoal):
 1. \<not> wf pdt_inv \<Longrightarrow> False
[PROOF STEP]
hence ****:\<open>\<forall> i>0. f i pd\<rightarrow> f 0\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>i j. i < j \<longrightarrow> f j pd\<rightarrow> f i
\<forall>i j. i < j \<longrightarrow> f i \<noteq> f j

goal (1 subgoal):
 1. \<forall>i>0. f i pd\<rightarrow> f 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>i>0. f i pd\<rightarrow> f 0

goal (1 subgoal):
 1. \<not> wf pdt_inv \<Longrightarrow> False
[PROOF STEP]
hence \<open>f 0 \<in> nodes\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>i>0. f i pd\<rightarrow> f 0

goal (1 subgoal):
 1. f 0 \<in> local.nodes
[PROOF STEP]
using * is_pd_def
[PROOF STATE]
proof (prove)
using this:
\<forall>i>0. f i pd\<rightarrow> f 0
\<forall>i. (f i, f (Suc i)) \<in> pdt
(?y pd\<rightarrow> ?x) = (?x \<in> local.nodes \<and> (\<forall>\<pi> n. is_path \<pi> \<and> \<pi> 0 = ?x \<and> \<pi> n = local.return \<longrightarrow> (\<exists>k\<le>n. \<pi> k = ?y)))

goal (1 subgoal):
 1. f 0 \<in> local.nodes
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
f 0 \<in> local.nodes

goal (1 subgoal):
 1. \<not> wf pdt_inv \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f 0 \<in> local.nodes
[PROOF STEP]
obtain \<pi> n where \<pi>:\<open>is_path \<pi>\<close> \<open>\<pi> 0 = f 0\<close> \<open>\<pi> n = return\<close>
[PROOF STATE]
proof (prove)
using this:
f 0 \<in> local.nodes

goal (1 subgoal):
 1. (\<And>\<pi> n. \<lbrakk>is_path \<pi>; \<pi> 0 = f 0; \<pi> n = local.return\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using reaching_ret
[PROOF STATE]
proof (prove)
using this:
f 0 \<in> local.nodes
?x \<in> local.nodes \<Longrightarrow> \<exists>\<pi> n. is_path \<pi> \<and> \<pi> 0 = ?x \<and> \<pi> n = local.return

goal (1 subgoal):
 1. (\<And>\<pi> n. \<lbrakk>is_path \<pi>; \<pi> 0 = f 0; \<pi> n = local.return\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
is_path \<pi>
\<pi> 0 = f 0
\<pi> n = local.return

goal (1 subgoal):
 1. \<not> wf pdt_inv \<Longrightarrow> False
[PROOF STEP]
hence \<open>\<forall> i>0. \<exists> k\<le>n. \<pi> k = f i\<close>
[PROOF STATE]
proof (prove)
using this:
is_path \<pi>
\<pi> 0 = f 0
\<pi> n = local.return

goal (1 subgoal):
 1. \<forall>i>0. \<exists>k\<le>n. \<pi> k = f i
[PROOF STEP]
using ***(1) \<open>f 0 \<in> nodes\<close>
[PROOF STATE]
proof (prove)
using this:
is_path \<pi>
\<pi> 0 = f 0
\<pi> n = local.return
\<forall>i j. i < j \<longrightarrow> f j pd\<rightarrow> f i
f 0 \<in> local.nodes

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

goal (1 subgoal):
 1. \<forall>i>0. \<exists>k\<le>n. \<pi> k = f i
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>i>0. \<exists>k\<le>n. \<pi> k = f i

goal (1 subgoal):
 1. \<not> wf pdt_inv \<Longrightarrow> False
[PROOF STEP]
hence \<pi>f:\<open>\<forall> i. \<exists> k\<le>n. \<pi> k = f i\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>i>0. \<exists>k\<le>n. \<pi> k = f i

goal (1 subgoal):
 1. \<forall>i. \<exists>k\<le>n. \<pi> k = f i
[PROOF STEP]
using \<pi>(2)
[PROOF STATE]
proof (prove)
using this:
\<forall>i>0. \<exists>k\<le>n. \<pi> k = f i
\<pi> 0 = f 0

goal (1 subgoal):
 1. \<forall>i. \<exists>k\<le>n. \<pi> k = f i
[PROOF STEP]
by (metis le0 not_gr_zero)
[PROOF STATE]
proof (state)
this:
\<forall>i. \<exists>k\<le>n. \<pi> k = f i

goal (1 subgoal):
 1. \<not> wf pdt_inv \<Longrightarrow> False
[PROOF STEP]
have \<open>range f \<subseteq> \<pi> ` {..n}\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. range f \<subseteq> \<pi> ` {..n}
[PROOF STEP]
proof(rule subsetI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> range f \<Longrightarrow> x \<in> \<pi> ` {..n}
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> range f \<Longrightarrow> x \<in> \<pi> ` {..n}
[PROOF STEP]
assume \<open>x \<in> range f\<close>
[PROOF STATE]
proof (state)
this:
x \<in> range f

goal (1 subgoal):
 1. \<And>x. x \<in> range f \<Longrightarrow> x \<in> \<pi> ` {..n}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> range f
[PROOF STEP]
obtain i where \<open>x = f i\<close>
[PROOF STATE]
proof (prove)
using this:
x \<in> range f

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

goal (1 subgoal):
 1. \<And>x. x \<in> range f \<Longrightarrow> x \<in> \<pi> ` {..n}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = f i
[PROOF STEP]
obtain k where \<open>x = \<pi> k\<close> \<open>k \<le> n\<close>
[PROOF STATE]
proof (prove)
using this:
x = f i

goal (1 subgoal):
 1. (\<And>k. \<lbrakk>x = \<pi> k; k \<le> n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<pi>f
[PROOF STATE]
proof (prove)
using this:
x = f i
\<forall>i. \<exists>k\<le>n. \<pi> k = f i

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

goal (1 subgoal):
 1. \<And>x. x \<in> range f \<Longrightarrow> x \<in> \<pi> ` {..n}
[PROOF STEP]
thus \<open>x \<in> \<pi> ` {..n}\<close>
[PROOF STATE]
proof (prove)
using this:
x = \<pi> k
k \<le> n

goal (1 subgoal):
 1. x \<in> \<pi> ` {..n}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<in> \<pi> ` {..n}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
range f \<subseteq> \<pi> ` {..n}

goal (1 subgoal):
 1. \<not> wf pdt_inv \<Longrightarrow> False
[PROOF STEP]
hence f:\<open>finite (range f)\<close>
[PROOF STATE]
proof (prove)
using this:
range f \<subseteq> \<pi> ` {..n}

goal (1 subgoal):
 1. finite (range f)
[PROOF STEP]
using finite_surj
[PROOF STATE]
proof (prove)
using this:
range f \<subseteq> \<pi> ` {..n}
\<lbrakk>finite ?A; ?B \<subseteq> ?f ` ?A\<rbrakk> \<Longrightarrow> finite ?B

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

goal (1 subgoal):
 1. \<not> wf pdt_inv \<Longrightarrow> False
[PROOF STEP]
hence fi:\<open>\<exists> i. infinite {j. f j = f i}\<close>
[PROOF STATE]
proof (prove)
using this:
finite (range f)

goal (1 subgoal):
 1. \<exists>i. infinite {j. f j = f i}
[PROOF STEP]
using pigeonhole_infinite[OF _ f]
[PROOF STATE]
proof (prove)
using this:
finite (range f)
infinite UNIV \<Longrightarrow> \<exists>a0\<in>UNIV. infinite {a \<in> UNIV. f a = f a0}

goal (1 subgoal):
 1. \<exists>i. infinite {j. f j = f i}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>i. infinite {j. f j = f i}

goal (1 subgoal):
 1. \<not> wf pdt_inv \<Longrightarrow> False
[PROOF STEP]
obtain i where \<open>infinite {j. f j = f i}\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i. infinite {j. f j = f i} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using fi
[PROOF STATE]
proof (prove)
using this:
\<exists>i. infinite {j. f j = f i}

goal (1 subgoal):
 1. (\<And>i. infinite {j. f j = f i} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
infinite {j. f j = f i}

goal (1 subgoal):
 1. \<not> wf pdt_inv \<Longrightarrow> False
[PROOF STEP]
thus \<open>False\<close>
[PROOF STATE]
proof (prove)
using this:
infinite {j. f j = f i}

goal (1 subgoal):
 1. False
[PROOF STEP]
by (metis (mono_tags, lifting) "***"(2) bounded_nat_set_is_finite gt_ex mem_Collect_eq nat_neq_iff)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma return_pd: assumes \<open>x \<in> nodes\<close> shows \<open>return pd\<rightarrow> x\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.return pd\<rightarrow> x
[PROOF STEP]
unfolding is_pd_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> local.nodes \<and> (\<forall>\<pi> n. is_path \<pi> \<and> \<pi> 0 = x \<and> \<pi> n = local.return \<longrightarrow> (\<exists>k\<le>n. \<pi> k = local.return))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in> local.nodes

goal (1 subgoal):
 1. x \<in> local.nodes \<and> (\<forall>\<pi> n. is_path \<pi> \<and> \<pi> 0 = x \<and> \<pi> n = local.return \<longrightarrow> (\<exists>k\<le>n. \<pi> k = local.return))
[PROOF STEP]
by blast