[STATEMENT]
lemma pd_total: assumes xz: \<open>x pd\<rightarrow> z\<close> and yz: \<open>y pd\<rightarrow> z\<close> shows \<open>x pd\<rightarrow> y \<or> y pd\<rightarrow>x\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x pd\<rightarrow> y \<or> y pd\<rightarrow> x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x pd\<rightarrow> y \<or> y pd\<rightarrow> x
[PROOF STEP]
obtain \<pi> n where path: \<open>is_path \<pi>\<close> and \<pi>0: \<open>\<pi> 0 = z\<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 = z; \<pi> n = local.return\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using xz reaching_ret
[PROOF STATE]
proof (prove)
using this:
x pd\<rightarrow> z
?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 = z; \<pi> n = local.return\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding is_pd_def
[PROOF STATE]
proof (prove)
using this:
z \<in> local.nodes \<and> (\<forall>\<pi> n. is_path \<pi> \<and> \<pi> 0 = z \<and> \<pi> n = local.return \<longrightarrow> (\<exists>k\<le>n. \<pi> k = x))
?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 = z; \<pi> n = local.return\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
is_path \<pi>
\<pi> 0 = z
\<pi> n = local.return

goal (1 subgoal):
 1. x pd\<rightarrow> y \<or> y pd\<rightarrow> x
[PROOF STEP]
have *: \<open>\<exists> k\<le>n. (\<pi> k = x \<or> \<pi> k = y)\<close> (is \<open>\<exists> k\<le>n. ?P k\<close>)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k\<le>n. \<pi> k = x \<or> \<pi> k = y
[PROOF STEP]
using path \<pi>0 \<pi>n xz yz
[PROOF STATE]
proof (prove)
using this:
is_path \<pi>
\<pi> 0 = z
\<pi> n = local.return
x pd\<rightarrow> z
y pd\<rightarrow> z

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

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

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

goal (1 subgoal):
 1. x pd\<rightarrow> y \<or> y pd\<rightarrow> x
[PROOF STEP]
hence kn: \<open>k\<le>n\<close> and \<pi>k: \<open>\<pi> k = x \<or> \<pi> k = y\<close>
[PROOF STATE]
proof (prove)
using this:
k = (LEAST k. \<pi> k = x \<or> \<pi> k = y)

goal (1 subgoal):
 1. k \<le> n &&& \<pi> k = x \<or> \<pi> k = y
[PROOF STEP]
using LeastBI_ex[OF *]
[PROOF STATE]
proof (prove)
using this:
k = (LEAST k. \<pi> k = x \<or> \<pi> k = y)
\<pi> (LEAST k. \<pi> k = x \<or> \<pi> k = y) = x \<or> \<pi> (LEAST k. \<pi> k = x \<or> \<pi> k = y) = y
(LEAST k. \<pi> k = x \<or> \<pi> k = y) \<le> n

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

goal (1 subgoal):
 1. x pd\<rightarrow> y \<or> y pd\<rightarrow> x
[PROOF STEP]
note k_le = Least_le[where P = \<open>?P\<close>]
[PROOF STATE]
proof (state)
this:
\<pi> ?k = x \<or> \<pi> ?k = y \<Longrightarrow> (LEAST xa. \<pi> xa = x \<or> \<pi> xa = y) \<le> ?k

goal (1 subgoal):
 1. x pd\<rightarrow> y \<or> y pd\<rightarrow> x
[PROOF STEP]
show \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x pd\<rightarrow> y \<or> y pd\<rightarrow> x
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> x pd\<rightarrow> y \<or> y pd\<rightarrow> x
 2. \<not> ?P \<Longrightarrow> x pd\<rightarrow> y \<or> y pd\<rightarrow> x
[PROOF STEP]
assume kx: \<open>\<pi> k = x\<close>
[PROOF STATE]
proof (state)
this:
\<pi> k = x

goal (2 subgoals):
 1. ?P \<Longrightarrow> x pd\<rightarrow> y \<or> y pd\<rightarrow> x
 2. \<not> ?P \<Longrightarrow> x pd\<rightarrow> y \<or> y pd\<rightarrow> x
[PROOF STEP]
have k_min: \<open>\<And> k'. \<pi> k' = y \<Longrightarrow> k \<le> k'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k'. \<pi> k' = y \<Longrightarrow> k \<le> k'
[PROOF STEP]
using k_le
[PROOF STATE]
proof (prove)
using this:
\<pi> ?k = x \<or> \<pi> ?k = y \<Longrightarrow> (LEAST xa. \<pi> xa = x \<or> \<pi> xa = y) \<le> ?k

goal (1 subgoal):
 1. \<And>k'. \<pi> k' = y \<Longrightarrow> k \<le> k'
[PROOF STEP]
unfolding k
[PROOF STATE]
proof (prove)
using this:
\<pi> ?k = x \<or> \<pi> ?k = y \<Longrightarrow> (LEAST xa. \<pi> xa = x \<or> \<pi> xa = y) \<le> ?k

goal (1 subgoal):
 1. \<And>k'. \<pi> k' = y \<Longrightarrow> (LEAST k. \<pi> k = x \<or> \<pi> k = y) \<le> k'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<pi> ?k'1 = y \<Longrightarrow> k \<le> ?k'1

goal (2 subgoals):
 1. ?P \<Longrightarrow> x pd\<rightarrow> y \<or> y pd\<rightarrow> x
 2. \<not> ?P \<Longrightarrow> x pd\<rightarrow> y \<or> y pd\<rightarrow> x
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<pi> ?k'1 = y \<Longrightarrow> k \<le> ?k'1

goal (2 subgoals):
 1. ?P \<Longrightarrow> x pd\<rightarrow> y \<or> y pd\<rightarrow> x
 2. \<not> ?P \<Longrightarrow> x pd\<rightarrow> y \<or> y pd\<rightarrow> x
[PROOF STEP]
fix \<pi>'
      and n' :: \<open>nat\<close>
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> x pd\<rightarrow> y \<or> y pd\<rightarrow> x
 2. \<not> ?P \<Longrightarrow> x pd\<rightarrow> y \<or> y pd\<rightarrow> x
[PROOF STEP]
assume 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 (state)
this:
is_path \<pi>'
\<pi>' 0 = x
\<pi>' n' = local.return

goal (2 subgoals):
 1. ?P \<Longrightarrow> x pd\<rightarrow> y \<or> y pd\<rightarrow> x
 2. \<not> ?P \<Longrightarrow> x pd\<rightarrow> y \<or> y pd\<rightarrow> x
[PROOF STEP]
have path'': \<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 path_cons[OF path path'] kx \<pi>'0
[PROOF STATE]
proof (prove)
using this:
\<pi> ?m = \<pi>' 0 \<Longrightarrow> is_path (\<pi> @\<^bsup>?m\<^esup> \<pi>')
\<pi> k = x
\<pi>' 0 = x

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> x pd\<rightarrow> y \<or> y pd\<rightarrow> x
 2. \<not> ?P \<Longrightarrow> x pd\<rightarrow> y \<or> y pd\<rightarrow> x
[PROOF STEP]
have \<pi>''0: \<open>(\<pi> @\<^bsup>k\<^esup> \<pi>') 0 = z\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<pi> @\<^bsup>k\<^esup> \<pi>') 0 = z
[PROOF STEP]
using \<pi>0
[PROOF STATE]
proof (prove)
using this:
\<pi> 0 = z

goal (1 subgoal):
 1. (\<pi> @\<^bsup>k\<^esup> \<pi>') 0 = z
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<pi> @\<^bsup>k\<^esup> \<pi>') 0 = z

goal (2 subgoals):
 1. ?P \<Longrightarrow> x pd\<rightarrow> y \<or> y pd\<rightarrow> x
 2. \<not> ?P \<Longrightarrow> x pd\<rightarrow> y \<or> y pd\<rightarrow> x
[PROOF STEP]
have \<pi>''n: \<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 \<pi>'n' kx \<pi>'0
[PROOF STATE]
proof (prove)
using this:
\<pi>' n' = local.return
\<pi> k = x
\<pi>' 0 = x

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 (2 subgoals):
 1. ?P \<Longrightarrow> x pd\<rightarrow> y \<or> y pd\<rightarrow> x
 2. \<not> ?P \<Longrightarrow> x pd\<rightarrow> y \<or> y pd\<rightarrow> x
[PROOF STEP]
obtain k' where k': \<open>k' \<le> k + n'\<close> \<open>(\<pi> @\<^bsup>k\<^esup> \<pi>') k' = y\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k'. \<lbrakk>k' \<le> k + n'; (\<pi> @\<^bsup>k\<^esup> \<pi>') k' = y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using yz path'' \<pi>''0 \<pi>''n
[PROOF STATE]
proof (prove)
using this:
y pd\<rightarrow> z
is_path (\<pi> @\<^bsup>k\<^esup> \<pi>')
(\<pi> @\<^bsup>k\<^esup> \<pi>') 0 = z
(\<pi> @\<^bsup>k\<^esup> \<pi>') (k + n') = local.return

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

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> x pd\<rightarrow> y \<or> y pd\<rightarrow> x
 2. \<not> ?P \<Longrightarrow> x pd\<rightarrow> y \<or> y pd\<rightarrow> x
[PROOF STEP]
have **: \<open>k \<le> k'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k \<le> k'
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> k \<le> k' \<Longrightarrow> False
[PROOF STEP]
assume \<open>\<not> k \<le> k'\<close>
[PROOF STATE]
proof (state)
this:
\<not> k \<le> k'

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

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

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

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

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

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

goal (1 subgoal):
 1. \<not> k \<le> k' \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
k' < k
\<pi> k' = y
[PROOF STEP]
show \<open>False\<close>
[PROOF STATE]
proof (prove)
using this:
k' < k
\<pi> k' = y

goal (1 subgoal):
 1. False
[PROOF STEP]
using k_min
[PROOF STATE]
proof (prove)
using this:
k' < k
\<pi> k' = y
\<pi> ?k'1 = y \<Longrightarrow> k \<le> ?k'1

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
k \<le> k'

goal (2 subgoals):
 1. ?P \<Longrightarrow> x pd\<rightarrow> y \<or> y pd\<rightarrow> x
 2. \<not> ?P \<Longrightarrow> x pd\<rightarrow> y \<or> y pd\<rightarrow> x
[PROOF STEP]
hence \<open>\<pi>' (k' - k) = y\<close>
[PROOF STATE]
proof (prove)
using this:
k \<le> k'

goal (1 subgoal):
 1. \<pi>' (k' - k) = y
[PROOF STEP]
using k' \<pi>'0 kx
[PROOF STATE]
proof (prove)
using this:
k \<le> k'
k' \<le> k + n'
(\<pi> @\<^bsup>k\<^esup> \<pi>') k' = y
\<pi>' 0 = x
\<pi> k = x

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> x pd\<rightarrow> y \<or> y pd\<rightarrow> x
 2. \<not> ?P \<Longrightarrow> x pd\<rightarrow> y \<or> y pd\<rightarrow> x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<pi>' (k' - k) = y

goal (2 subgoals):
 1. ?P \<Longrightarrow> x pd\<rightarrow> y \<or> y pd\<rightarrow> x
 2. \<not> ?P \<Longrightarrow> x pd\<rightarrow> y \<or> y pd\<rightarrow> x
[PROOF STEP]
have \<open>(k' - k) \<le> n'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k' - k \<le> n'
[PROOF STEP]
using k'
[PROOF STATE]
proof (prove)
using this:
k' \<le> k + n'
(\<pi> @\<^bsup>k\<^esup> \<pi>') k' = y

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> x pd\<rightarrow> y \<or> y pd\<rightarrow> x
 2. \<not> ?P \<Longrightarrow> x pd\<rightarrow> y \<or> y pd\<rightarrow> x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<pi>' (k' - k) = y
k' - k \<le> n'
[PROOF STEP]
have \<open>\<exists> k\<le> n'. \<pi>' k = y\<close>
[PROOF STATE]
proof (prove)
using this:
\<pi>' (k' - k) = y
k' - k \<le> n'

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 (2 subgoals):
 1. ?P \<Longrightarrow> x pd\<rightarrow> y \<or> y pd\<rightarrow> x
 2. \<not> ?P \<Longrightarrow> x pd\<rightarrow> y \<or> y pd\<rightarrow> x
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>is_path ?\<pi>'3; ?\<pi>'3 0 = x; ?\<pi>'3 ?n'3 = local.return\<rbrakk> \<Longrightarrow> \<exists>k\<le>?n'3. ?\<pi>'3 k = y

goal (2 subgoals):
 1. ?P \<Longrightarrow> x pd\<rightarrow> y \<or> y pd\<rightarrow> x
 2. \<not> ?P \<Longrightarrow> x pd\<rightarrow> y \<or> y pd\<rightarrow> x
[PROOF STEP]
hence \<open>y pd\<rightarrow> x\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_path ?\<pi>'3; ?\<pi>'3 0 = x; ?\<pi>'3 ?n'3 = local.return\<rbrakk> \<Longrightarrow> \<exists>k\<le>?n'3. ?\<pi>'3 k = y

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

goal (1 subgoal):
 1. y 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 ?n'3 = local.return\<rbrakk> \<Longrightarrow> \<exists>k\<le>?n'3. ?\<pi>'3 k = y
\<pi> k = x
is_path ?\<pi> \<Longrightarrow> ?\<pi> ?k \<in> local.nodes
is_path \<pi>

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 = y))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y pd\<rightarrow> x

goal (2 subgoals):
 1. ?P \<Longrightarrow> x pd\<rightarrow> y \<or> y pd\<rightarrow> x
 2. \<not> ?P \<Longrightarrow> x pd\<rightarrow> y \<or> y pd\<rightarrow> x
[PROOF STEP]
thus \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
y pd\<rightarrow> x

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

goal (1 subgoal):
 1. \<pi> k \<noteq> x \<Longrightarrow> x pd\<rightarrow> y \<or> y pd\<rightarrow> x
[PROOF STEP]
next \<comment> \<open>This is analogous argument\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<pi> k \<noteq> x \<Longrightarrow> x pd\<rightarrow> y \<or> y pd\<rightarrow> x
[PROOF STEP]
assume kx: \<open>\<pi> k \<noteq> x\<close>
[PROOF STATE]
proof (state)
this:
\<pi> k \<noteq> x

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

goal (1 subgoal):
 1. \<pi> k = y
[PROOF STEP]
using \<pi>k
[PROOF STATE]
proof (prove)
using this:
\<pi> k \<noteq> x
\<pi> k = x \<or> \<pi> k = y

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

goal (1 subgoal):
 1. \<pi> k \<noteq> x \<Longrightarrow> x pd\<rightarrow> y \<or> y pd\<rightarrow> x
[PROOF STEP]
have k_min: \<open>\<And> k'. \<pi> k' = x \<Longrightarrow> k \<le> k'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k'. \<pi> k' = x \<Longrightarrow> k \<le> k'
[PROOF STEP]
using k_le
[PROOF STATE]
proof (prove)
using this:
\<pi> ?k = x \<or> \<pi> ?k = y \<Longrightarrow> (LEAST xa. \<pi> xa = x \<or> \<pi> xa = y) \<le> ?k

goal (1 subgoal):
 1. \<And>k'. \<pi> k' = x \<Longrightarrow> k \<le> k'
[PROOF STEP]
unfolding k
[PROOF STATE]
proof (prove)
using this:
\<pi> ?k = x \<or> \<pi> ?k = y \<Longrightarrow> (LEAST xa. \<pi> xa = x \<or> \<pi> xa = y) \<le> ?k

goal (1 subgoal):
 1. \<And>k'. \<pi> k' = x \<Longrightarrow> (LEAST k. \<pi> k = x \<or> \<pi> k = y) \<le> k'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<pi> ?k'1 = x \<Longrightarrow> k \<le> ?k'1

goal (1 subgoal):
 1. \<pi> k \<noteq> x \<Longrightarrow> x pd\<rightarrow> y \<or> y pd\<rightarrow> x
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<pi> ?k'1 = x \<Longrightarrow> k \<le> ?k'1

goal (1 subgoal):
 1. \<pi> k \<noteq> x \<Longrightarrow> x pd\<rightarrow> y \<or> y pd\<rightarrow> x
[PROOF STEP]
fix \<pi>'
      and n' :: \<open>nat\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<pi> k \<noteq> x \<Longrightarrow> x pd\<rightarrow> y \<or> y pd\<rightarrow> x
[PROOF STEP]
assume path': \<open>is_path \<pi>'\<close> and \<pi>'0: \<open>\<pi>' 0 = y\<close> and \<pi>'n': \<open>\<pi>' n' = return\<close>
[PROOF STATE]
proof (state)
this:
is_path \<pi>'
\<pi>' 0 = y
\<pi>' n' = local.return

goal (1 subgoal):
 1. \<pi> k \<noteq> x \<Longrightarrow> x pd\<rightarrow> y \<or> y pd\<rightarrow> x
[PROOF STEP]
have path'': \<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 path_cons[OF path path'] ky \<pi>'0
[PROOF STATE]
proof (prove)
using this:
\<pi> ?m = \<pi>' 0 \<Longrightarrow> is_path (\<pi> @\<^bsup>?m\<^esup> \<pi>')
\<pi> k = y
\<pi>' 0 = y

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

goal (1 subgoal):
 1. \<pi> k \<noteq> x \<Longrightarrow> x pd\<rightarrow> y \<or> y pd\<rightarrow> x
[PROOF STEP]
have \<pi>''0: \<open>(\<pi> @\<^bsup>k\<^esup> \<pi>') 0 = z\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<pi> @\<^bsup>k\<^esup> \<pi>') 0 = z
[PROOF STEP]
using \<pi>0
[PROOF STATE]
proof (prove)
using this:
\<pi> 0 = z

goal (1 subgoal):
 1. (\<pi> @\<^bsup>k\<^esup> \<pi>') 0 = z
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<pi> @\<^bsup>k\<^esup> \<pi>') 0 = z

goal (1 subgoal):
 1. \<pi> k \<noteq> x \<Longrightarrow> x pd\<rightarrow> y \<or> y pd\<rightarrow> x
[PROOF STEP]
have \<pi>''n: \<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 \<pi>'n' ky \<pi>'0
[PROOF STATE]
proof (prove)
using this:
\<pi>' n' = local.return
\<pi> k = y
\<pi>' 0 = y

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. \<pi> k \<noteq> x \<Longrightarrow> x pd\<rightarrow> y \<or> y pd\<rightarrow> x
[PROOF STEP]
obtain k' where k': \<open>k' \<le> k + n'\<close> \<open>(\<pi> @\<^bsup>k\<^esup> \<pi>') k' = x\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k'. \<lbrakk>k' \<le> k + n'; (\<pi> @\<^bsup>k\<^esup> \<pi>') k' = x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using xz path'' \<pi>''0 \<pi>''n
[PROOF STATE]
proof (prove)
using this:
x pd\<rightarrow> z
is_path (\<pi> @\<^bsup>k\<^esup> \<pi>')
(\<pi> @\<^bsup>k\<^esup> \<pi>') 0 = z
(\<pi> @\<^bsup>k\<^esup> \<pi>') (k + n') = local.return

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

goal (1 subgoal):
 1. (\<And>k'. \<lbrakk>k' \<le> k + n'; (\<pi> @\<^bsup>k\<^esup> \<pi>') k' = x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
k' \<le> k + n'
(\<pi> @\<^bsup>k\<^esup> \<pi>') k' = x

goal (1 subgoal):
 1. \<pi> k \<noteq> x \<Longrightarrow> x pd\<rightarrow> y \<or> y pd\<rightarrow> x
[PROOF STEP]
have **: \<open>k \<le> k'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k \<le> k'
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> k \<le> k' \<Longrightarrow> False
[PROOF STEP]
assume \<open>\<not> k \<le> k'\<close>
[PROOF STATE]
proof (state)
this:
\<not> k \<le> k'

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

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

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

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

goal (1 subgoal):
 1. \<pi> k' = x
[PROOF STEP]
using k'
[PROOF STATE]
proof (prove)
using this:
k' < k
k' \<le> k + n'
(\<pi> @\<^bsup>k\<^esup> \<pi>') k' = x

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

goal (1 subgoal):
 1. \<not> k \<le> k' \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
k' < k
\<pi> k' = x
[PROOF STEP]
show \<open>False\<close>
[PROOF STATE]
proof (prove)
using this:
k' < k
\<pi> k' = x

goal (1 subgoal):
 1. False
[PROOF STEP]
using k_min
[PROOF STATE]
proof (prove)
using this:
k' < k
\<pi> k' = x
\<pi> ?k'1 = x \<Longrightarrow> k \<le> ?k'1

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
k \<le> k'

goal (1 subgoal):
 1. \<pi> k \<noteq> x \<Longrightarrow> x pd\<rightarrow> y \<or> y pd\<rightarrow> x
[PROOF STEP]
hence \<open>\<pi>' (k' - k) = x\<close>
[PROOF STATE]
proof (prove)
using this:
k \<le> k'

goal (1 subgoal):
 1. \<pi>' (k' - k) = x
[PROOF STEP]
using k' \<pi>'0 ky
[PROOF STATE]
proof (prove)
using this:
k \<le> k'
k' \<le> k + n'
(\<pi> @\<^bsup>k\<^esup> \<pi>') k' = x
\<pi>' 0 = y
\<pi> k = y

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

goal (1 subgoal):
 1. \<pi> k \<noteq> x \<Longrightarrow> x pd\<rightarrow> y \<or> y pd\<rightarrow> x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<pi>' (k' - k) = x

goal (1 subgoal):
 1. \<pi> k \<noteq> x \<Longrightarrow> x pd\<rightarrow> y \<or> y pd\<rightarrow> x
[PROOF STEP]
have \<open>(k' - k) \<le> n'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k' - k \<le> n'
[PROOF STEP]
using k'
[PROOF STATE]
proof (prove)
using this:
k' \<le> k + n'
(\<pi> @\<^bsup>k\<^esup> \<pi>') k' = x

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

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

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

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

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

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

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

goal (1 subgoal):
 1. 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))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x pd\<rightarrow> y

goal (1 subgoal):
 1. \<pi> k \<noteq> x \<Longrightarrow> x pd\<rightarrow> y \<or> y pd\<rightarrow> x
[PROOF STEP]
thus \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
x pd\<rightarrow> y

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x pd\<rightarrow> y \<or> y pd\<rightarrow> x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pds_finite: \<open>finite {y . (x,y) \<in> pdt}\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {y. (x, y) \<in> pdt}
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> finite {y. (x, y) \<in> pdt}
 2. \<not> ?P \<Longrightarrow> finite {y. (x, y) \<in> pdt}
[PROOF STEP]
assume \<open>x \<in> nodes\<close>
[PROOF STATE]
proof (state)
this:
x \<in> local.nodes

goal (2 subgoals):
 1. ?P \<Longrightarrow> finite {y. (x, y) \<in> pdt}
 2. \<not> ?P \<Longrightarrow> finite {y. (x, y) \<in> pdt}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> local.nodes
[PROOF STEP]
obtain \<pi> n where \<pi>:\<open>is_path \<pi>\<close> \<open>\<pi> 0 = x\<close> \<open>\<pi> n = return\<close>
[PROOF STATE]
proof (prove)
using this:
x \<in> local.nodes

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 reaching_ret
[PROOF STATE]
proof (prove)
using this:
x \<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 = x; \<pi> n = local.return\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
is_path \<pi>
\<pi> 0 = x
\<pi> n = local.return

goal (2 subgoals):
 1. ?P \<Longrightarrow> finite {y. (x, y) \<in> pdt}
 2. \<not> ?P \<Longrightarrow> finite {y. (x, y) \<in> pdt}
[PROOF STEP]
have *: \<open>\<forall> y \<in> {y. (x,y)\<in> pdt}. y pd\<rightarrow> x\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>y\<in>{y. (x, y) \<in> pdt}. y pd\<rightarrow> x
[PROOF STEP]
using pdt_def
[PROOF STATE]
proof (prove)
using this:
pdt = {(x, y). x \<noteq> y \<and> y pd\<rightarrow> x}

goal (1 subgoal):
 1. \<forall>y\<in>{y. (x, y) \<in> pdt}. y pd\<rightarrow> x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>y\<in>{y. (x, y) \<in> pdt}. y pd\<rightarrow> x

goal (2 subgoals):
 1. ?P \<Longrightarrow> finite {y. (x, y) \<in> pdt}
 2. \<not> ?P \<Longrightarrow> finite {y. (x, y) \<in> pdt}
[PROOF STEP]
have \<open>\<forall> y \<in> {y. (x,y)\<in> pdt}. \<exists> k \<le> n. \<pi> k = y\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>y\<in>{y. (x, y) \<in> pdt}. \<exists>k\<le>n. \<pi> k = y
[PROOF STEP]
using * \<pi> is_pd_def
[PROOF STATE]
proof (prove)
using this:
\<forall>y\<in>{y. (x, y) \<in> pdt}. y pd\<rightarrow> x
is_path \<pi>
\<pi> 0 = x
\<pi> n = local.return
(?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. \<forall>y\<in>{y. (x, y) \<in> pdt}. \<exists>k\<le>n. \<pi> k = y
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>y\<in>{y. (x, y) \<in> pdt}. \<exists>k\<le>n. \<pi> k = y

goal (2 subgoals):
 1. ?P \<Longrightarrow> finite {y. (x, y) \<in> pdt}
 2. \<not> ?P \<Longrightarrow> finite {y. (x, y) \<in> pdt}
[PROOF STEP]
hence \<open>{y. (x,y)\<in> pdt} \<subseteq> \<pi> ` {..n}\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>y\<in>{y. (x, y) \<in> pdt}. \<exists>k\<le>n. \<pi> k = y

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> finite {y. (x, y) \<in> pdt}
 2. \<not> ?P \<Longrightarrow> finite {y. (x, y) \<in> pdt}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{y. (x, y) \<in> pdt} \<subseteq> \<pi> ` {..n}
[PROOF STEP]
show \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
{y. (x, y) \<in> pdt} \<subseteq> \<pi> ` {..n}

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

goal (1 subgoal):
 1. finite {y. (x, y) \<in> pdt}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite {y. (x, y) \<in> pdt}

goal (1 subgoal):
 1. x \<notin> local.nodes \<Longrightarrow> finite {y. (x, y) \<in> pdt}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<notin> local.nodes \<Longrightarrow> finite {y. (x, y) \<in> pdt}
[PROOF STEP]
assume \<open>\<not> x\<in> nodes\<close>
[PROOF STATE]
proof (state)
this:
x \<notin> local.nodes

goal (1 subgoal):
 1. x \<notin> local.nodes \<Longrightarrow> finite {y. (x, y) \<in> pdt}
[PROOF STEP]
hence \<open>{y. (x,y)\<in>pdt} = {}\<close>
[PROOF STATE]
proof (prove)
using this:
x \<notin> local.nodes

goal (1 subgoal):
 1. {y. (x, y) \<in> pdt} = {}
[PROOF STEP]
unfolding pdt_def is_pd_def
[PROOF STATE]
proof (prove)
using this:
x \<notin> local.nodes

goal (1 subgoal):
 1. {y. (x, y) \<in> {(x, y). x \<noteq> y \<and> 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))}} = {}
[PROOF STEP]
using path_nodes reaching_ret
[PROOF STATE]
proof (prove)
using this:
x \<notin> local.nodes
is_path ?\<pi> \<Longrightarrow> ?\<pi> ?k \<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. {y. (x, y) \<in> {(x, y). x \<noteq> y \<and> 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))}} = {}
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
{y. (x, y) \<in> pdt} = {}

goal (1 subgoal):
 1. x \<notin> local.nodes \<Longrightarrow> finite {y. (x, y) \<in> pdt}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{y. (x, y) \<in> pdt} = {}
[PROOF STEP]
show \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
{y. (x, y) \<in> pdt} = {}

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ipd_exists: assumes node: \<open>x \<in> nodes\<close> and not_ret: \<open>x\<noteq>return\<close> shows \<open>\<exists>y. y ipd\<rightarrow> x\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>y. y ipd\<rightarrow> x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>y. y ipd\<rightarrow> x
[PROOF STEP]
let \<open>?Q\<close> = \<open>{y. x\<noteq>y \<and> y pd\<rightarrow> x}\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>y. y ipd\<rightarrow> x
[PROOF STEP]
have *: \<open>return \<in> ?Q\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.return \<in> {y. x \<noteq> y \<and> y pd\<rightarrow> x}
[PROOF STEP]
using assms return_pd
[PROOF STATE]
proof (prove)
using this:
x \<in> local.nodes
x \<noteq> local.return
?x \<in> local.nodes \<Longrightarrow> local.return pd\<rightarrow> ?x

goal (1 subgoal):
 1. local.return \<in> {y. x \<noteq> y \<and> y pd\<rightarrow> x}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
local.return \<in> {y. x \<noteq> y \<and> y pd\<rightarrow> x}

goal (1 subgoal):
 1. \<exists>y. y ipd\<rightarrow> x
[PROOF STEP]
hence **: \<open>\<exists> x. x\<in> ?Q\<close>
[PROOF STATE]
proof (prove)
using this:
local.return \<in> {y. x \<noteq> y \<and> y pd\<rightarrow> x}

goal (1 subgoal):
 1. \<exists>xa. xa \<in> {y. x \<noteq> y \<and> y pd\<rightarrow> x}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>xa. xa \<in> {y. x \<noteq> y \<and> y pd\<rightarrow> x}

goal (1 subgoal):
 1. \<exists>y. y ipd\<rightarrow> x
[PROOF STEP]
have fin: \<open>finite ?Q\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {y. x \<noteq> y \<and> y pd\<rightarrow> x}
[PROOF STEP]
using pds_finite
[PROOF STATE]
proof (prove)
using this:
finite {y. (?x, y) \<in> pdt}

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

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

goal (1 subgoal):
 1. \<exists>y. y ipd\<rightarrow> x
[PROOF STEP]
have tot: \<open>\<forall> y z. y\<in>?Q \<and> z \<in> ?Q \<longrightarrow> z pd\<rightarrow> y \<or> y pd\<rightarrow> z\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>y z. y \<in> {y. x \<noteq> y \<and> y pd\<rightarrow> x} \<and> z \<in> {y. x \<noteq> y \<and> y pd\<rightarrow> x} \<longrightarrow> z pd\<rightarrow> y \<or> y pd\<rightarrow> z
[PROOF STEP]
using pd_total
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x pd\<rightarrow> ?z; ?y pd\<rightarrow> ?z\<rbrakk> \<Longrightarrow> ?x pd\<rightarrow> ?y \<or> ?y pd\<rightarrow> ?x

goal (1 subgoal):
 1. \<forall>y z. y \<in> {y. x \<noteq> y \<and> y pd\<rightarrow> x} \<and> z \<in> {y. x \<noteq> y \<and> y pd\<rightarrow> x} \<longrightarrow> z pd\<rightarrow> y \<or> y pd\<rightarrow> z
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>y z. y \<in> {y. x \<noteq> y \<and> y pd\<rightarrow> x} \<and> z \<in> {y. x \<noteq> y \<and> y pd\<rightarrow> x} \<longrightarrow> z pd\<rightarrow> y \<or> y pd\<rightarrow> z

goal (1 subgoal):
 1. \<exists>y. y ipd\<rightarrow> x
[PROOF STEP]
obtain y where ymax: \<open>y\<in> ?Q\<close> \<open>\<forall> z\<in>?Q. z = y \<or> z pd\<rightarrow> y\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> {y. x \<noteq> y \<and> y pd\<rightarrow> x}; \<forall>z\<in>{y. x \<noteq> y \<and> y pd\<rightarrow> x}. z = y \<or> z pd\<rightarrow> y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using fin ** tot
[PROOF STATE]
proof (prove)
using this:
finite {y. x \<noteq> y \<and> y pd\<rightarrow> x}
\<exists>xa. xa \<in> {y. x \<noteq> y \<and> y pd\<rightarrow> x}
\<forall>y z. y \<in> {y. x \<noteq> y \<and> y pd\<rightarrow> x} \<and> z \<in> {y. x \<noteq> y \<and> y pd\<rightarrow> x} \<longrightarrow> z pd\<rightarrow> y \<or> y pd\<rightarrow> z

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> {y. x \<noteq> y \<and> y pd\<rightarrow> x}; \<forall>z\<in>{y. x \<noteq> y \<and> y pd\<rightarrow> x}. z = y \<or> z pd\<rightarrow> y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof (induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<And>y. \<lbrakk>y \<in> {}; \<forall>z\<in>{}. z = y \<or> z pd\<rightarrow> y\<rbrakk> \<Longrightarrow> thesis; \<exists>x. x \<in> {}; \<forall>y z. y \<in> {} \<and> z \<in> {} \<longrightarrow> z pd\<rightarrow> y \<or> y pd\<rightarrow> z\<rbrakk> \<Longrightarrow> thesis
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>\<And>y. \<lbrakk>y \<in> F; \<forall>z\<in>F. z = y \<or> z pd\<rightarrow> y\<rbrakk> \<Longrightarrow> thesis; \<exists>x. x \<in> F; \<forall>y z. y \<in> F \<and> z \<in> F \<longrightarrow> z pd\<rightarrow> y \<or> y pd\<rightarrow> z\<rbrakk> \<Longrightarrow> thesis; \<And>y. \<lbrakk>y \<in> insert x F; \<forall>z\<in>insert x F. z = y \<or> z pd\<rightarrow> y\<rbrakk> \<Longrightarrow> thesis; \<exists>xa. xa \<in> insert x F; \<forall>y z. y \<in> insert x F \<and> z \<in> insert x F \<longrightarrow> z pd\<rightarrow> y \<or> y pd\<rightarrow> z\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
case empty
[PROOF STATE]
proof (state)
this:
\<lbrakk>?y1 \<in> {}; \<forall>z\<in>{}. z = ?y1 \<or> z pd\<rightarrow> ?y1\<rbrakk> \<Longrightarrow> thesis
\<exists>x. x \<in> {}
\<forall>y z. y \<in> {} \<and> z \<in> {} \<longrightarrow> z pd\<rightarrow> y \<or> y pd\<rightarrow> z

goal (2 subgoals):
 1. \<lbrakk>\<And>y. \<lbrakk>y \<in> {}; \<forall>z\<in>{}. z = y \<or> z pd\<rightarrow> y\<rbrakk> \<Longrightarrow> thesis; \<exists>x. x \<in> {}; \<forall>y z. y \<in> {} \<and> z \<in> {} \<longrightarrow> z pd\<rightarrow> y \<or> y pd\<rightarrow> z\<rbrakk> \<Longrightarrow> thesis
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>\<And>y. \<lbrakk>y \<in> F; \<forall>z\<in>F. z = y \<or> z pd\<rightarrow> y\<rbrakk> \<Longrightarrow> thesis; \<exists>x. x \<in> F; \<forall>y z. y \<in> F \<and> z \<in> F \<longrightarrow> z pd\<rightarrow> y \<or> y pd\<rightarrow> z\<rbrakk> \<Longrightarrow> thesis; \<And>y. \<lbrakk>y \<in> insert x F; \<forall>z\<in>insert x F. z = y \<or> z pd\<rightarrow> y\<rbrakk> \<Longrightarrow> thesis; \<exists>xa. xa \<in> insert x F; \<forall>y z. y \<in> insert x F \<and> z \<in> insert x F \<longrightarrow> z pd\<rightarrow> y \<or> y pd\<rightarrow> z\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?y1 \<in> {}; \<forall>z\<in>{}. z = ?y1 \<or> z pd\<rightarrow> ?y1\<rbrakk> \<Longrightarrow> thesis
\<exists>x. x \<in> {}
\<forall>y z. y \<in> {} \<and> z \<in> {} \<longrightarrow> z pd\<rightarrow> y \<or> y pd\<rightarrow> z
[PROOF STEP]
show \<open>?case\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?y1 \<in> {}; \<forall>z\<in>{}. z = ?y1 \<or> z pd\<rightarrow> ?y1\<rbrakk> \<Longrightarrow> thesis
\<exists>x. x \<in> {}
\<forall>y z. y \<in> {} \<and> z \<in> {} \<longrightarrow> z pd\<rightarrow> y \<or> y pd\<rightarrow> z

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

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>\<And>y. \<lbrakk>y \<in> F; \<forall>z\<in>F. z = y \<or> z pd\<rightarrow> y\<rbrakk> \<Longrightarrow> thesis; \<exists>x. x \<in> F; \<forall>y z. y \<in> F \<and> z \<in> F \<longrightarrow> z pd\<rightarrow> y \<or> y pd\<rightarrow> z\<rbrakk> \<Longrightarrow> thesis; \<And>y. \<lbrakk>y \<in> insert x F; \<forall>z\<in>insert x F. z = y \<or> z pd\<rightarrow> y\<rbrakk> \<Longrightarrow> thesis; \<exists>xa. xa \<in> insert x F; \<forall>y z. y \<in> insert x F \<and> z \<in> insert x F \<longrightarrow> z pd\<rightarrow> y \<or> y pd\<rightarrow> z\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>\<And>y. \<lbrakk>y \<in> F; \<forall>z\<in>F. z = y \<or> z pd\<rightarrow> y\<rbrakk> \<Longrightarrow> thesis; \<exists>x. x \<in> F; \<forall>y z. y \<in> F \<and> z \<in> F \<longrightarrow> z pd\<rightarrow> y \<or> y pd\<rightarrow> z\<rbrakk> \<Longrightarrow> thesis; \<And>y. \<lbrakk>y \<in> insert x F; \<forall>z\<in>insert x F. z = y \<or> z pd\<rightarrow> y\<rbrakk> \<Longrightarrow> thesis; \<exists>xa. xa \<in> insert x F; \<forall>y z. y \<in> insert x F \<and> z \<in> insert x F \<longrightarrow> z pd\<rightarrow> y \<or> y pd\<rightarrow> z\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
case (insert x F)
[PROOF STATE]
proof (state)
this:
finite F
x \<notin> F
\<lbrakk>\<And>y. \<lbrakk>y \<in> F; \<forall>z\<in>F. z = y \<or> z pd\<rightarrow> y\<rbrakk> \<Longrightarrow> thesis; \<exists>x. x \<in> F; \<forall>y z. y \<in> F \<and> z \<in> F \<longrightarrow> z pd\<rightarrow> y \<or> y pd\<rightarrow> z\<rbrakk> \<Longrightarrow> thesis
\<lbrakk>?y1 \<in> insert x F; \<forall>z\<in>insert x F. z = ?y1 \<or> z pd\<rightarrow> ?y1\<rbrakk> \<Longrightarrow> thesis
\<exists>x. x \<in> insert x F
\<forall>y z. y \<in> insert x F \<and> z \<in> insert x F \<longrightarrow> z pd\<rightarrow> y \<or> y pd\<rightarrow> z

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>\<And>y. \<lbrakk>y \<in> F; \<forall>z\<in>F. z = y \<or> z pd\<rightarrow> y\<rbrakk> \<Longrightarrow> thesis; \<exists>x. x \<in> F; \<forall>y z. y \<in> F \<and> z \<in> F \<longrightarrow> z pd\<rightarrow> y \<or> y pd\<rightarrow> z\<rbrakk> \<Longrightarrow> thesis; \<And>y. \<lbrakk>y \<in> insert x F; \<forall>z\<in>insert x F. z = y \<or> z pd\<rightarrow> y\<rbrakk> \<Longrightarrow> thesis; \<exists>xa. xa \<in> insert x F; \<forall>y z. y \<in> insert x F \<and> z \<in> insert x F \<longrightarrow> z pd\<rightarrow> y \<or> y pd\<rightarrow> z\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
show \<open>thesis\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
proof (cases \<open>F = {}\<close>)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. F = {} \<Longrightarrow> thesis
 2. F \<noteq> {} \<Longrightarrow> thesis
[PROOF STEP]
assume \<open>F = {}\<close>
[PROOF STATE]
proof (state)
this:
F = {}

goal (2 subgoals):
 1. F = {} \<Longrightarrow> thesis
 2. F \<noteq> {} \<Longrightarrow> thesis
[PROOF STEP]
thus \<open>thesis\<close>
[PROOF STATE]
proof (prove)
using this:
F = {}

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using insert(4)[of \<open>x\<close>]
[PROOF STATE]
proof (prove)
using this:
F = {}
\<lbrakk>x \<in> insert x F; \<forall>z\<in>insert x F. z = x \<or> z pd\<rightarrow> x\<rbrakk> \<Longrightarrow> thesis

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

goal (1 subgoal):
 1. F \<noteq> {} \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. F \<noteq> {} \<Longrightarrow> thesis
[PROOF STEP]
assume \<open>F \<noteq> {}\<close>
[PROOF STATE]
proof (state)
this:
F \<noteq> {}

goal (1 subgoal):
 1. F \<noteq> {} \<Longrightarrow> thesis
[PROOF STEP]
hence \<open>\<exists> x. x\<in> F\<close>
[PROOF STATE]
proof (prove)
using this:
F \<noteq> {}

goal (1 subgoal):
 1. \<exists>x. x \<in> F
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>x. x \<in> F

goal (1 subgoal):
 1. F \<noteq> {} \<Longrightarrow> thesis
[PROOF STEP]
have \<open>\<And>y. y \<in> F \<Longrightarrow> \<forall>z\<in>F. z = y \<or> z pd\<rightarrow> y \<Longrightarrow> thesis\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>y \<in> F; \<forall>z\<in>F. z = y \<or> z pd\<rightarrow> y\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>y \<in> F; \<forall>z\<in>F. z = y \<or> z pd\<rightarrow> y\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>y \<in> F; \<forall>z\<in>F. z = y \<or> z pd\<rightarrow> y\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
assume a: \<open>y \<in> F\<close> \<open>\<forall>z\<in>F. z = y \<or> z pd\<rightarrow> y\<close>
[PROOF STATE]
proof (state)
this:
y \<in> F
\<forall>z\<in>F. z = y \<or> z pd\<rightarrow> y

goal (1 subgoal):
 1. \<And>y. \<lbrakk>y \<in> F; \<forall>z\<in>F. z = y \<or> z pd\<rightarrow> y\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have \<open>x \<noteq> y\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<noteq> y
[PROOF STEP]
using insert a
[PROOF STATE]
proof (prove)
using this:
finite F
x \<notin> F
\<lbrakk>\<And>y. \<lbrakk>y \<in> F; \<forall>z\<in>F. z = y \<or> z pd\<rightarrow> y\<rbrakk> \<Longrightarrow> thesis; \<exists>x. x \<in> F; \<forall>y z. y \<in> F \<and> z \<in> F \<longrightarrow> z pd\<rightarrow> y \<or> y pd\<rightarrow> z\<rbrakk> \<Longrightarrow> thesis
\<lbrakk>?y1 \<in> insert x F; \<forall>z\<in>insert x F. z = ?y1 \<or> z pd\<rightarrow> ?y1\<rbrakk> \<Longrightarrow> thesis
\<exists>x. x \<in> insert x F
\<forall>y z. y \<in> insert x F \<and> z \<in> insert x F \<longrightarrow> z pd\<rightarrow> y \<or> y pd\<rightarrow> z
y \<in> F
\<forall>z\<in>F. z = y \<or> z pd\<rightarrow> y

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

goal (1 subgoal):
 1. \<And>y. \<lbrakk>y \<in> F; \<forall>z\<in>F. z = y \<or> z pd\<rightarrow> y\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have \<open>x pd\<rightarrow> y \<or> y pd\<rightarrow> x\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x pd\<rightarrow> y \<or> y pd\<rightarrow> x
[PROOF STEP]
using insert(6) a(1)
[PROOF STATE]
proof (prove)
using this:
\<forall>y z. y \<in> insert x F \<and> z \<in> insert x F \<longrightarrow> z pd\<rightarrow> y \<or> y pd\<rightarrow> z
y \<in> F

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

goal (1 subgoal):
 1. \<And>y. \<lbrakk>y \<in> F; \<forall>z\<in>F. z = y \<or> z pd\<rightarrow> y\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
thus \<open>thesis\<close>
[PROOF STATE]
proof (prove)
using this:
x pd\<rightarrow> y \<or> y pd\<rightarrow> x

goal (1 subgoal):
 1. thesis
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x pd\<rightarrow> y \<Longrightarrow> thesis
 2. y pd\<rightarrow> x \<Longrightarrow> thesis
[PROOF STEP]
assume \<open>x pd\<rightarrow> y\<close>
[PROOF STATE]
proof (state)
this:
x pd\<rightarrow> y

goal (2 subgoals):
 1. x pd\<rightarrow> y \<Longrightarrow> thesis
 2. y pd\<rightarrow> x \<Longrightarrow> thesis
[PROOF STEP]
hence \<open>\<forall>z\<in>insert x F. z = y \<or> z pd\<rightarrow> y\<close>
[PROOF STATE]
proof (prove)
using this:
x pd\<rightarrow> y

goal (1 subgoal):
 1. \<forall>z\<in>insert x F. z = y \<or> z pd\<rightarrow> y
[PROOF STEP]
using a(2)
[PROOF STATE]
proof (prove)
using this:
x pd\<rightarrow> y
\<forall>z\<in>F. z = y \<or> z pd\<rightarrow> y

goal (1 subgoal):
 1. \<forall>z\<in>insert x F. z = y \<or> z pd\<rightarrow> y
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>z\<in>insert x F. z = y \<or> z pd\<rightarrow> y

goal (2 subgoals):
 1. x pd\<rightarrow> y \<Longrightarrow> thesis
 2. y pd\<rightarrow> x \<Longrightarrow> thesis
[PROOF STEP]
thus \<open>thesis\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>z\<in>insert x F. z = y \<or> z pd\<rightarrow> y

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using a(1) insert(4)
[PROOF STATE]
proof (prove)
using this:
\<forall>z\<in>insert x F. z = y \<or> z pd\<rightarrow> y
y \<in> F
\<lbrakk>?y1 \<in> insert x F; \<forall>z\<in>insert x F. z = ?y1 \<or> z pd\<rightarrow> ?y1\<rbrakk> \<Longrightarrow> thesis

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

goal (1 subgoal):
 1. y pd\<rightarrow> x \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. y pd\<rightarrow> x \<Longrightarrow> thesis
[PROOF STEP]
assume \<open>y pd\<rightarrow> x\<close>
[PROOF STATE]
proof (state)
this:
y pd\<rightarrow> x

goal (1 subgoal):
 1. y pd\<rightarrow> x \<Longrightarrow> thesis
[PROOF STEP]
have \<open>\<forall>z\<in>insert x F. z = x \<or> z pd\<rightarrow> x\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>z\<in>insert x F. z = x \<or> z pd\<rightarrow> x
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>z. z \<in> insert x F \<Longrightarrow> z = x \<or> z pd\<rightarrow> x
[PROOF STEP]
fix z
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>z. z \<in> insert x F \<Longrightarrow> z = x \<or> z pd\<rightarrow> x
[PROOF STEP]
assume \<open>z\<in> insert x F\<close>
[PROOF STATE]
proof (state)
this:
z \<in> insert x F

goal (1 subgoal):
 1. \<And>z. z \<in> insert x F \<Longrightarrow> z = x \<or> z pd\<rightarrow> x
[PROOF STEP]
thus \<open>z = x \<or> z pd\<rightarrow> x\<close>
[PROOF STATE]
proof (prove)
using this:
z \<in> insert x F

goal (1 subgoal):
 1. z = x \<or> z pd\<rightarrow> x
[PROOF STEP]
proof(rule,simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. z \<in> F \<Longrightarrow> z = x \<or> z pd\<rightarrow> x
[PROOF STEP]
assume \<open>z\<in>F\<close>
[PROOF STATE]
proof (state)
this:
z \<in> F

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

goal (1 subgoal):
 1. z = y \<or> z pd\<rightarrow> y
[PROOF STEP]
using a(2)
[PROOF STATE]
proof (prove)
using this:
z \<in> F
\<forall>z\<in>F. z = y \<or> z pd\<rightarrow> y

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

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

goal (1 subgoal):
 1. z = x \<or> z pd\<rightarrow> x
[PROOF STEP]
proof(rule,simp add: \<open>y pd\<rightarrow> x\<close>)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. z pd\<rightarrow> y \<Longrightarrow> z = x \<or> z pd\<rightarrow> x
[PROOF STEP]
assume \<open>z pd\<rightarrow> y\<close>
[PROOF STATE]
proof (state)
this:
z pd\<rightarrow> y

goal (1 subgoal):
 1. z pd\<rightarrow> y \<Longrightarrow> z = x \<or> z pd\<rightarrow> x
[PROOF STEP]
show \<open>z = x \<or> z pd\<rightarrow> x\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z = x \<or> z pd\<rightarrow> x
[PROOF STEP]
using \<open>y pd\<rightarrow> x\<close> \<open>z pd\<rightarrow> y\<close> pd_trans
[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 = x \<or> z pd\<rightarrow> x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
z = x \<or> z pd\<rightarrow> x

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>z\<in>insert x F. z = x \<or> z pd\<rightarrow> x

goal (1 subgoal):
 1. y pd\<rightarrow> x \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>z\<in>insert x F. z = x \<or> z pd\<rightarrow> x
[PROOF STEP]
show \<open>thesis\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>z\<in>insert x F. z = x \<or> z pd\<rightarrow> x

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using insert
[PROOF STATE]
proof (prove)
using this:
\<forall>z\<in>insert x F. z = x \<or> z pd\<rightarrow> x
finite F
x \<notin> F
\<lbrakk>\<And>y. \<lbrakk>y \<in> F; \<forall>z\<in>F. z = y \<or> z pd\<rightarrow> y\<rbrakk> \<Longrightarrow> thesis; \<exists>x. x \<in> F; \<forall>y z. y \<in> F \<and> z \<in> F \<longrightarrow> z pd\<rightarrow> y \<or> y pd\<rightarrow> z\<rbrakk> \<Longrightarrow> thesis
\<lbrakk>?y1 \<in> insert x F; \<forall>z\<in>insert x F. z = ?y1 \<or> z pd\<rightarrow> ?y1\<rbrakk> \<Longrightarrow> thesis
\<exists>x. x \<in> insert x F
\<forall>y z. y \<in> insert x F \<and> z \<in> insert x F \<longrightarrow> z pd\<rightarrow> y \<or> y pd\<rightarrow> z

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?y1 \<in> F; \<forall>z\<in>F. z = ?y1 \<or> z pd\<rightarrow> ?y1\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. F \<noteq> {} \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?y1 \<in> F; \<forall>z\<in>F. z = ?y1 \<or> z pd\<rightarrow> ?y1\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
show \<open>thesis\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?y1 \<in> F; \<forall>z\<in>F. z = ?y1 \<or> z pd\<rightarrow> ?y1\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using insert
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?y1 \<in> F; \<forall>z\<in>F. z = ?y1 \<or> z pd\<rightarrow> ?y1\<rbrakk> \<Longrightarrow> thesis
finite F
x \<notin> F
\<lbrakk>\<And>y. \<lbrakk>y \<in> F; \<forall>z\<in>F. z = y \<or> z pd\<rightarrow> y\<rbrakk> \<Longrightarrow> thesis; \<exists>x. x \<in> F; \<forall>y z. y \<in> F \<and> z \<in> F \<longrightarrow> z pd\<rightarrow> y \<or> y pd\<rightarrow> z\<rbrakk> \<Longrightarrow> thesis
\<lbrakk>?y1 \<in> insert x F; \<forall>z\<in>insert x F. z = ?y1 \<or> z pd\<rightarrow> ?y1\<rbrakk> \<Longrightarrow> thesis
\<exists>x. x \<in> insert x F
\<forall>y z. y \<in> insert x F \<and> z \<in> insert x F \<longrightarrow> z pd\<rightarrow> y \<or> y pd\<rightarrow> z

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
y \<in> {y. x \<noteq> y \<and> y pd\<rightarrow> x}
\<forall>z\<in>{y. x \<noteq> y \<and> y pd\<rightarrow> x}. z = y \<or> z pd\<rightarrow> y

goal (1 subgoal):
 1. \<exists>y. y ipd\<rightarrow> x
[PROOF STEP]
hence ***: \<open>y pd\<rightarrow> x\<close> \<open>x\<noteq>y\<close>
[PROOF STATE]
proof (prove)
using this:
y \<in> {y. x \<noteq> y \<and> y pd\<rightarrow> x}
\<forall>z\<in>{y. x \<noteq> y \<and> y pd\<rightarrow> x}. z = y \<or> z pd\<rightarrow> y

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

goal (1 subgoal):
 1. \<exists>y. y ipd\<rightarrow> x
[PROOF STEP]
have \<open>\<forall> z. z \<noteq> x \<and> z pd\<rightarrow> x \<longrightarrow> z pd\<rightarrow> y\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>z. z \<noteq> x \<and> z pd\<rightarrow> x \<longrightarrow> z pd\<rightarrow> y
[PROOF STEP]
proof (rule,rule)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>z. z \<noteq> x \<and> z pd\<rightarrow> x \<Longrightarrow> z pd\<rightarrow> y
[PROOF STEP]
fix z
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>z. z \<noteq> x \<and> z pd\<rightarrow> x \<Longrightarrow> z pd\<rightarrow> y
[PROOF STEP]
assume a: \<open> z \<noteq> x \<and> z pd\<rightarrow> x\<close>
[PROOF STATE]
proof (state)
this:
z \<noteq> x \<and> z pd\<rightarrow> x

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

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

goal (1 subgoal):
 1. \<And>z. z \<noteq> x \<and> z pd\<rightarrow> x \<Longrightarrow> z pd\<rightarrow> y
[PROOF STEP]
have \<open>y pd\<rightarrow> z \<or> z pd\<rightarrow> y\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y pd\<rightarrow> z \<or> z pd\<rightarrow> y
[PROOF STEP]
using pd_total ***(1) a
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x pd\<rightarrow> ?z; ?y pd\<rightarrow> ?z\<rbrakk> \<Longrightarrow> ?x pd\<rightarrow> ?y \<or> ?y pd\<rightarrow> ?x
y pd\<rightarrow> x
z \<noteq> x \<and> z pd\<rightarrow> x

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

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

goal (1 subgoal):
 1. z pd\<rightarrow> y
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. y pd\<rightarrow> z \<Longrightarrow> z pd\<rightarrow> y
 2. z pd\<rightarrow> y \<Longrightarrow> z pd\<rightarrow> y
[PROOF STEP]
assume c: \<open>y pd\<rightarrow> z\<close>
[PROOF STATE]
proof (state)
this:
y pd\<rightarrow> z

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

goal (1 subgoal):
 1. y = z
[PROOF STEP]
using b ymax pdt_def pd_antisym
[PROOF STATE]
proof (prove)
using this:
y pd\<rightarrow> z
z \<in> {y. x \<noteq> y \<and> y pd\<rightarrow> x}
y \<in> {y. x \<noteq> y \<and> y pd\<rightarrow> x}
\<forall>z\<in>{y. x \<noteq> y \<and> y pd\<rightarrow> x}. z = y \<or> z pd\<rightarrow> y
pdt = {(x, y). x \<noteq> y \<and> y pd\<rightarrow> x}
\<lbrakk>?x pd\<rightarrow> ?y; ?y pd\<rightarrow> ?x\<rbrakk> \<Longrightarrow> ?x = ?y

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

goal (2 subgoals):
 1. y pd\<rightarrow> z \<Longrightarrow> z pd\<rightarrow> y
 2. z pd\<rightarrow> y \<Longrightarrow> z pd\<rightarrow> y
[PROOF STEP]
thus \<open>z pd\<rightarrow> y\<close>
[PROOF STATE]
proof (prove)
using this:
y = z

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>z. z \<noteq> x \<and> z pd\<rightarrow> x \<longrightarrow> z pd\<rightarrow> y

goal (1 subgoal):
 1. \<exists>y. y ipd\<rightarrow> x
[PROOF STEP]
with ***
[PROOF STATE]
proof (chain)
picking this:
y pd\<rightarrow> x
x \<noteq> y
\<forall>z. z \<noteq> x \<and> z pd\<rightarrow> x \<longrightarrow> z pd\<rightarrow> y
[PROOF STEP]
have  \<open>y ipd\<rightarrow> x\<close>
[PROOF STATE]
proof (prove)
using this:
y pd\<rightarrow> x
x \<noteq> y
\<forall>z. z \<noteq> x \<and> z pd\<rightarrow> x \<longrightarrow> z pd\<rightarrow> y

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

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

goal (1 subgoal):
 1. \<exists>y. y ipd\<rightarrow> x
[PROOF STEP]
thus \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
y ipd\<rightarrow> x

goal (1 subgoal):
 1. \<exists>y. y ipd\<rightarrow> x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>y. y ipd\<rightarrow> x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ipd_unique: assumes yipd: \<open>y ipd\<rightarrow> x\<close> and y'ipd: \<open>y' ipd\<rightarrow> x\<close> shows \<open>y = y'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y = y'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. y = y'
[PROOF STEP]
have 1: \<open>y pd\<rightarrow> y'\<close> and  2: \<open>y' pd\<rightarrow> y\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y pd\<rightarrow> y' &&& y' pd\<rightarrow> y
[PROOF STEP]
using yipd y'ipd
[PROOF STATE]
proof (prove)
using this:
y ipd\<rightarrow> x
y' ipd\<rightarrow> x

goal (1 subgoal):
 1. y pd\<rightarrow> y' &&& y' pd\<rightarrow> y
[PROOF STEP]
unfolding is_ipd_def
[PROOF STATE]
proof (prove)
using this:
x \<noteq> y \<and> y pd\<rightarrow> x \<and> (\<forall>z. z \<noteq> x \<and> z pd\<rightarrow> x \<longrightarrow> z pd\<rightarrow> y)
x \<noteq> y' \<and> y' pd\<rightarrow> x \<and> (\<forall>z. z \<noteq> x \<and> z pd\<rightarrow> x \<longrightarrow> z pd\<rightarrow> y')

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

goal (1 subgoal):
 1. y = y'
[PROOF STEP]
show \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y = y'
[PROOF STEP]
using pd_antisym[OF 1 2]
[PROOF STATE]
proof (prove)
using this:
y = y'

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ipd_is_ipd: assumes \<open>x \<in> nodes\<close> and \<open>x\<noteq>return\<close> shows \<open>ipd x ipd\<rightarrow> x\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ipd x ipd\<rightarrow> x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ipd x ipd\<rightarrow> x
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
x \<in> local.nodes
x \<noteq> local.return
[PROOF STEP]
obtain y where \<open>y ipd\<rightarrow> x\<close>
[PROOF STATE]
proof (prove)
using this:
x \<in> local.nodes
x \<noteq> local.return

goal (1 subgoal):
 1. (\<And>y. y ipd\<rightarrow> x \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using ipd_exists
[PROOF STATE]
proof (prove)
using this:
x \<in> local.nodes
x \<noteq> local.return
\<lbrakk>?x \<in> local.nodes; ?x \<noteq> local.return\<rbrakk> \<Longrightarrow> \<exists>y. y ipd\<rightarrow> ?x

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

goal (1 subgoal):
 1. ipd x ipd\<rightarrow> x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
y ipd\<rightarrow> x

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

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

goal (1 subgoal):
 1. \<And>z. z ipd\<rightarrow> x \<Longrightarrow> z = y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
?z1 ipd\<rightarrow> x \<Longrightarrow> ?z1 = y

goal (1 subgoal):
 1. ipd x ipd\<rightarrow> x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
y ipd\<rightarrow> x
?z1 ipd\<rightarrow> x \<Longrightarrow> ?z1 = y
[PROOF STEP]
show \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
y ipd\<rightarrow> x
?z1 ipd\<rightarrow> x \<Longrightarrow> ?z1 = y

goal (1 subgoal):
 1. ipd x ipd\<rightarrow> x
[PROOF STEP]
unfolding ipd_def
[PROOF STATE]
proof (prove)
using this:
y ipd\<rightarrow> x
?z1 ipd\<rightarrow> x \<Longrightarrow> ?z1 = y

goal (1 subgoal):
 1. (THE y. y ipd\<rightarrow> x) ipd\<rightarrow> x
[PROOF STEP]
by (auto intro: theI2)
[PROOF STATE]
proof (state)
this:
ipd x ipd\<rightarrow> x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_ipd_in_pdt: \<open>y ipd\<rightarrow> x \<Longrightarrow> (x,y) \<in> pdt\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y ipd\<rightarrow> x \<Longrightarrow> (x, y) \<in> pdt
[PROOF STEP]
unfolding is_ipd_def pdt_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<noteq> y \<and> y pd\<rightarrow> x \<and> (\<forall>z. z \<noteq> x \<and> z pd\<rightarrow> x \<longrightarrow> z pd\<rightarrow> y) \<Longrightarrow> (x, y) \<in> {(x, y). x \<noteq> y \<and> y pd\<rightarrow> x}
[PROOF STEP]
by auto


[STATEMENT]
lemma ipd_in_pdt: \<open>x \<in> nodes \<Longrightarrow> x\<noteq>return \<Longrightarrow> (x,ipd x) \<in> pdt\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> local.nodes; x \<noteq> local.return\<rbrakk> \<Longrightarrow> (x, ipd x) \<in> pdt
[PROOF STEP]
by (metis ipd_is_ipd is_ipd_in_pdt)


[STATEMENT]
lemma no_pd_path: assumes \<open>x \<in> nodes\<close> and \<open>\<not> y pd\<rightarrow> x\<close>
obtains \<pi> n where \<open>is_path \<pi>\<close> and \<open>\<pi> 0 = x\<close> and \<open>\<pi> n = return\<close> and \<open>\<forall> k \<le> n. \<pi> k \<noteq> y\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<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) \<Longrightarrow> thesis
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<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; \<not> thesis\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume \<open>\<not> thesis\<close>
[PROOF STATE]
proof (state)
this:
\<not> thesis

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

goal (1 subgoal):
 1. \<forall>\<pi> n. is_path \<pi> \<and> \<pi> 0 = x \<and> \<pi> n = local.return \<longrightarrow> (\<exists>k\<le>n. \<pi> k = y)
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
\<not> thesis
\<lbrakk>is_path ?\<pi>1; ?\<pi>1 0 = x; ?\<pi>1 ?n1 = local.return; \<forall>k\<le>?n1. ?\<pi>1 k \<noteq> y\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. \<forall>\<pi> n. is_path \<pi> \<and> \<pi> 0 = x \<and> \<pi> n = local.return \<longrightarrow> (\<exists>k\<le>n. \<pi> k = y)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<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. \<lbrakk>\<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; \<not> thesis\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
thus \<open>False\<close>
[PROOF STATE]
proof (prove)
using this:
\<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. False
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<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
\<not> y pd\<rightarrow> x

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pd_pd_ipd: assumes \<open>x \<in> nodes\<close> \<open>x\<noteq>return\<close> \<open>y\<noteq>x\<close> \<open>y pd\<rightarrow> x\<close> shows \<open>y pd\<rightarrow> ipd x\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y pd\<rightarrow> ipd x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. y pd\<rightarrow> ipd x
[PROOF STEP]
have \<open>ipd x pd\<rightarrow> x\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ipd x pd\<rightarrow> x
[PROOF STEP]
by (metis assms(1,2) ipd_is_ipd is_ipd_def)
[PROOF STATE]
proof (state)
this:
ipd x pd\<rightarrow> x

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

goal (1 subgoal):
 1. y pd\<rightarrow> ipd x \<or> ipd x pd\<rightarrow> y
[PROOF STEP]
by (metis assms(4) pd_total)
[PROOF STATE]
proof (state)
this:
y pd\<rightarrow> ipd x \<or> ipd x pd\<rightarrow> y

goal (1 subgoal):
 1. y pd\<rightarrow> ipd x
[PROOF STEP]
thus \<open>?thesis\<close>
[PROOF STATE]
proof (prove)
using this:
y pd\<rightarrow> ipd x \<or> ipd x pd\<rightarrow> y

goal (1 subgoal):
 1. y pd\<rightarrow> ipd x
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. y pd\<rightarrow> ipd x \<Longrightarrow> y pd\<rightarrow> ipd x
 2. ipd x pd\<rightarrow> y \<Longrightarrow> y pd\<rightarrow> ipd x
[PROOF STEP]
have 1: \<open>ipd x ipd\<rightarrow> x\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ipd x ipd\<rightarrow> x
[PROOF STEP]
by (metis assms(1,2) ipd_is_ipd)
[PROOF STATE]
proof (state)
this:
ipd x ipd\<rightarrow> x

goal (2 subgoals):
 1. y pd\<rightarrow> ipd x \<Longrightarrow> y pd\<rightarrow> ipd x
 2. ipd x pd\<rightarrow> y \<Longrightarrow> y pd\<rightarrow> ipd x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ipd x ipd\<rightarrow> x

goal (2 subgoals):
 1. y pd\<rightarrow> ipd x \<Longrightarrow> y pd\<rightarrow> ipd x
 2. ipd x pd\<rightarrow> y \<Longrightarrow> y pd\<rightarrow> ipd x
[PROOF STEP]
assume \<open>ipd x pd\<rightarrow> y\<close>
[PROOF STATE]
proof (state)
this:
ipd x pd\<rightarrow> y

goal (2 subgoals):
 1. y pd\<rightarrow> ipd x \<Longrightarrow> y pd\<rightarrow> ipd x
 2. ipd x pd\<rightarrow> y \<Longrightarrow> y pd\<rightarrow> ipd x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ipd x ipd\<rightarrow> x
ipd x pd\<rightarrow> y
[PROOF STEP]
show \<open>y pd\<rightarrow> ipd x\<close>
[PROOF STATE]
proof (prove)
using this:
ipd x ipd\<rightarrow> x
ipd x pd\<rightarrow> y

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

goal (1 subgoal):
 1. y pd\<rightarrow> ipd x
[PROOF STEP]
using assms(3,4)
[PROOF STATE]
proof (prove)
using this:
x \<noteq> ipd x \<and> ipd x pd\<rightarrow> x \<and> (\<forall>z. z \<noteq> x \<and> z pd\<rightarrow> x \<longrightarrow> z pd\<rightarrow> ipd x)
ipd x pd\<rightarrow> y
y \<noteq> x
y pd\<rightarrow> x

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

goal (1 subgoal):
 1. y pd\<rightarrow> ipd x \<Longrightarrow> y pd\<rightarrow> ipd x
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
y pd\<rightarrow> ipd x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pd_nodes: assumes \<open>y pd\<rightarrow> x\<close> shows pd_node1: \<open>y \<in> nodes\<close> and pd_node2: \<open>x \<in> nodes\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<in> local.nodes &&& x \<in> local.nodes
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. y \<in> local.nodes
 2. x \<in> local.nodes
[PROOF STEP]
obtain \<pi> k where \<open>is_path \<pi>\<close> \<open>\<pi> k = y\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<pi> k. \<lbrakk>is_path \<pi>; \<pi> k = y\<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> k. \<lbrakk>is_path \<pi>; \<pi> k = y\<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> k. \<lbrakk>is_path \<pi>; \<pi> k = y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using reaching_ret
[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> k. \<lbrakk>is_path \<pi>; \<pi> k = y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
is_path \<pi>
\<pi> k = y

goal (2 subgoals):
 1. y \<in> local.nodes
 2. x \<in> local.nodes
[PROOF STEP]
thus \<open>y \<in> nodes\<close>
[PROOF STATE]
proof (prove)
using this:
is_path \<pi>
\<pi> k = y

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

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

goal (1 subgoal):
 1. x \<in> local.nodes
[PROOF STEP]
show \<open>x \<in> nodes\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> local.nodes
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
y pd\<rightarrow> x

goal (1 subgoal):
 1. x \<in> local.nodes
[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. x \<in> local.nodes
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<in> local.nodes

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pd_ret_is_ret: \<open>x pd\<rightarrow> return \<Longrightarrow> x = return\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x pd\<rightarrow> local.return \<Longrightarrow> x = local.return
[PROOF STEP]
by (metis pd_antisym pd_node1 return_pd)


[STATEMENT]
lemma ret_path_none_pd: 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. \<not> x pd\<rightarrow> \<pi> i\<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. \<not> x pd\<rightarrow> \<pi> i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof(rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>\<pi> n. \<lbrakk>is_path \<pi>; \<pi> 0 = x; \<pi> n = local.return; \<forall>i>0. \<not> x pd\<rightarrow> \<pi> i\<rbrakk> \<Longrightarrow> thesis; \<not> thesis\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume \<open>\<not>thesis\<close>
[PROOF STATE]
proof (state)
this:
\<not> thesis

goal (1 subgoal):
 1. \<lbrakk>\<And>\<pi> n. \<lbrakk>is_path \<pi>; \<pi> 0 = x; \<pi> n = local.return; \<forall>i>0. \<not> x pd\<rightarrow> \<pi> i\<rbrakk> \<Longrightarrow> thesis; \<not> thesis\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence *: \<open>\<And> \<pi> n. \<lbrakk>is_path \<pi>; \<pi> 0 = x; \<pi> n = return\<rbrakk> \<Longrightarrow> \<exists>i>0. x pd\<rightarrow> \<pi> i\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> thesis

goal (1 subgoal):
 1. \<And>\<pi> n. \<lbrakk>is_path \<pi>; \<pi> 0 = x; \<pi> n = local.return\<rbrakk> \<Longrightarrow> \<exists>i>0. x pd\<rightarrow> \<pi> i
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
\<not> thesis
\<lbrakk>is_path ?\<pi>1; ?\<pi>1 0 = x; ?\<pi>1 ?n1 = local.return; \<forall>i>0. \<not> x pd\<rightarrow> ?\<pi>1 i\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. \<And>\<pi> n. \<lbrakk>is_path \<pi>; \<pi> 0 = x; \<pi> n = local.return\<rbrakk> \<Longrightarrow> \<exists>i>0. x pd\<rightarrow> \<pi> i
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>is_path ?\<pi>1; ?\<pi>1 0 = x; ?\<pi>1 ?n1 = local.return\<rbrakk> \<Longrightarrow> \<exists>i>0. x pd\<rightarrow> ?\<pi>1 i

goal (1 subgoal):
 1. \<lbrakk>\<And>\<pi> n. \<lbrakk>is_path \<pi>; \<pi> 0 = x; \<pi> n = local.return; \<forall>i>0. \<not> x pd\<rightarrow> \<pi> i\<rbrakk> \<Longrightarrow> thesis; \<not> thesis\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
obtain \<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 assms]
[PROOF STATE]
proof (prove)
using this:
(\<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

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 metis
[PROOF STATE]
proof (state)
this:
is_path \<pi>
\<pi> 0 = x
\<pi> n = local.return
\<forall>i>0. \<pi> i \<noteq> x

goal (1 subgoal):
 1. \<lbrakk>\<And>\<pi> n. \<lbrakk>is_path \<pi>; \<pi> 0 = x; \<pi> n = local.return; \<forall>i>0. \<not> x pd\<rightarrow> \<pi> i\<rbrakk> \<Longrightarrow> thesis; \<not> thesis\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_path \<pi>
\<pi> 0 = x
\<pi> n = local.return
\<forall>i>0. \<pi> i \<noteq> x
[PROOF STEP]
obtain i where ***: \<open>i>0\<close> \<open>x pd\<rightarrow> \<pi> i\<close>
[PROOF STATE]
proof (prove)
using this:
is_path \<pi>
\<pi> 0 = x
\<pi> n = local.return
\<forall>i>0. \<pi> i \<noteq> x

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

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

goal (1 subgoal):
 1. \<lbrakk>\<And>\<pi> n. \<lbrakk>is_path \<pi>; \<pi> 0 = x; \<pi> n = local.return; \<forall>i>0. \<not> x pd\<rightarrow> \<pi> i\<rbrakk> \<Longrightarrow> thesis; \<not> thesis\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence \<open>\<pi> i \<noteq> return\<close>
[PROOF STATE]
proof (prove)
using this:
0 < i
x pd\<rightarrow> \<pi> i

goal (1 subgoal):
 1. \<pi> i \<noteq> local.return
[PROOF STEP]
using pd_ret_is_ret assms(2)
[PROOF STATE]
proof (prove)
using this:
0 < i
x pd\<rightarrow> \<pi> i
?x pd\<rightarrow> local.return \<Longrightarrow> ?x = local.return
x \<noteq> local.return

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

goal (1 subgoal):
 1. \<lbrakk>\<And>\<pi> n. \<lbrakk>is_path \<pi>; \<pi> 0 = x; \<pi> n = local.return; \<forall>i>0. \<not> x pd\<rightarrow> \<pi> i\<rbrakk> \<Longrightarrow> thesis; \<not> thesis\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence \<open>i < n\<close>
[PROOF STATE]
proof (prove)
using this:
\<pi> i \<noteq> local.return

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

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

goal (1 subgoal):
 1. \<lbrakk>\<And>\<pi> n. \<lbrakk>is_path \<pi>; \<pi> 0 = x; \<pi> n = local.return; \<forall>i>0. \<not> x pd\<rightarrow> \<pi> i\<rbrakk> \<Longrightarrow> thesis; \<not> thesis\<rbrakk> \<Longrightarrow> False
[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 **(3)
[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. \<lbrakk>\<And>\<pi> n. \<lbrakk>is_path \<pi>; \<pi> 0 = x; \<pi> n = local.return; \<forall>i>0. \<not> x pd\<rightarrow> \<pi> i\<rbrakk> \<Longrightarrow> thesis; \<not> thesis\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<pi> \<guillemotleft> i) (n - i) = local.return

goal (1 subgoal):
 1. \<lbrakk>\<And>\<pi> n. \<lbrakk>is_path \<pi>; \<pi> 0 = x; \<pi> n = local.return; \<forall>i>0. \<not> x pd\<rightarrow> \<pi> i\<rbrakk> \<Longrightarrow> thesis; \<not> thesis\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have \<open>(\<pi>\<guillemotleft>i) (0) = \<pi> i\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<pi> \<guillemotleft> i) 0 = \<pi> i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<pi> \<guillemotleft> i) 0 = \<pi> i

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

goal (1 subgoal):
 1. \<lbrakk>\<And>\<pi> n. \<lbrakk>is_path \<pi>; \<pi> 0 = x; \<pi> n = local.return; \<forall>i>0. \<not> x pd\<rightarrow> \<pi> i\<rbrakk> \<Longrightarrow> thesis; \<not> thesis\<rbrakk> \<Longrightarrow> False
[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 **(1) path_path_shift
[PROOF STATE]
proof (prove)
using this:
is_path \<pi>
is_path ?\<pi> \<Longrightarrow> is_path (?\<pi> \<guillemotleft> ?m)

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

goal (1 subgoal):
 1. \<lbrakk>\<And>\<pi> n. \<lbrakk>is_path \<pi>; \<pi> 0 = x; \<pi> n = local.return; \<forall>i>0. \<not> x pd\<rightarrow> \<pi> i\<rbrakk> \<Longrightarrow> thesis; \<not> thesis\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<pi> \<guillemotleft> i) (n - i) = local.return
(\<pi> \<guillemotleft> i) 0 = \<pi> i
is_path (\<pi> \<guillemotleft> i)
[PROOF STEP]
obtain k where \<open>(\<pi>\<guillemotleft>i) k = x\<close>
[PROOF STATE]
proof (prove)
using this:
(\<pi> \<guillemotleft> i) (n - i) = local.return
(\<pi> \<guillemotleft> i) 0 = \<pi> i
is_path (\<pi> \<guillemotleft> i)

goal (1 subgoal):
 1. (\<And>k. (\<pi> \<guillemotleft> i) k = x \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using ***(2)
[PROOF STATE]
proof (prove)
using this:
(\<pi> \<guillemotleft> i) (n - i) = local.return
(\<pi> \<guillemotleft> i) 0 = \<pi> i
is_path (\<pi> \<guillemotleft> i)
x pd\<rightarrow> \<pi> i

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

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

goal (1 subgoal):
 1. \<lbrakk>\<And>\<pi> n. \<lbrakk>is_path \<pi>; \<pi> 0 = x; \<pi> n = local.return; \<forall>i>0. \<not> x pd\<rightarrow> \<pi> i\<rbrakk> \<Longrightarrow> thesis; \<not> thesis\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence \<open>\<pi> (i + k) = x\<close>
[PROOF STATE]
proof (prove)
using this:
(\<pi> \<guillemotleft> i) k = x

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

goal (1 subgoal):
 1. \<lbrakk>\<And>\<pi> n. \<lbrakk>is_path \<pi>; \<pi> 0 = x; \<pi> n = local.return; \<forall>i>0. \<not> x pd\<rightarrow> \<pi> i\<rbrakk> \<Longrightarrow> thesis; \<not> thesis\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
thus \<open>False\<close>
[PROOF STATE]
proof (prove)
using this:
\<pi> (i + k) = x

goal (1 subgoal):
 1. False
[PROOF STEP]
using **(4) \<open>i>0\<close>
[PROOF STATE]
proof (prove)
using this:
\<pi> (i + k) = x
\<forall>i>0. \<pi> i \<noteq> x
0 < i

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma path_pd_ipd0': assumes \<open>is_path \<pi>\<close> and \<open>\<pi> n \<noteq> return\<close> \<open>\<pi> n \<noteq> \<pi> 0\<close> and \<open>\<pi> n pd\<rightarrow> \<pi> 0\<close>
obtains k where \<open>k \<le> n\<close> and \<open>\<pi> k = ipd(\<pi> 0)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k. \<lbrakk>k \<le> n; \<pi> k = ipd (\<pi> 0)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof(rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>k. \<lbrakk>k \<le> n; \<pi> k = ipd (\<pi> 0)\<rbrakk> \<Longrightarrow> thesis; \<not> thesis\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have *: \<open>\<pi> n pd\<rightarrow> ipd (\<pi> 0)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> n pd\<rightarrow> ipd (\<pi> 0)
[PROOF STEP]
by (metis is_pd_def assms(3,4) pd_pd_ipd pd_ret_is_ret)
[PROOF STATE]
proof (state)
this:
\<pi> n pd\<rightarrow> ipd (\<pi> 0)

goal (1 subgoal):
 1. \<lbrakk>\<And>k. \<lbrakk>k \<le> n; \<pi> k = ipd (\<pi> 0)\<rbrakk> \<Longrightarrow> thesis; \<not> thesis\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
obtain \<pi>' n' where **: \<open>is_path \<pi>'\<close> \<open>\<pi>' 0 = \<pi> n\<close> \<open>\<pi>' n' = return\<close> \<open>\<forall> i>0. \<not> \<pi> n pd\<rightarrow> \<pi>' i\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<pi>' n'. \<lbrakk>is_path \<pi>'; \<pi>' 0 = \<pi> n; \<pi>' n' = local.return; \<forall>i>0. \<not> \<pi> n pd\<rightarrow> \<pi>' i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis assms(2) assms(4) pd_node1 ret_path_none_pd)
[PROOF STATE]
proof (state)
this:
is_path \<pi>'
\<pi>' 0 = \<pi> n
\<pi>' n' = local.return
\<forall>i>0. \<not> \<pi> n pd\<rightarrow> \<pi>' i

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

goal (1 subgoal):
 1. \<forall>i>0. \<pi>' i \<noteq> ipd (\<pi> 0)
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
is_path \<pi>'
\<pi>' 0 = \<pi> n
\<pi>' n' = local.return
\<forall>i>0. \<not> \<pi> n pd\<rightarrow> \<pi>' i
\<pi> n pd\<rightarrow> ipd (\<pi> 0)

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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<forall>i. (\<pi> @\<^bsup>n\<^esup> \<pi>') i \<noteq> ipd (\<pi> 0)
[PROOF STEP]
by (metis diff_is_0_eq neq0_conv path_append_def)
[PROOF STATE]
proof (state)
this:
\<forall>i. (\<pi> @\<^bsup>n\<^esup> \<pi>') i \<noteq> ipd (\<pi> 0)

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

goal (1 subgoal):
 1. \<lbrakk>\<And>k. \<lbrakk>k \<le> n; \<pi> k = ipd (\<pi> 0)\<rbrakk> \<Longrightarrow> thesis; \<not> thesis\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have \<open>(\<pi>@\<^bsup>n\<^esup>  \<pi>') (n + n') = return\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<pi> @\<^bsup>n\<^esup> \<pi>') (n + n') = local.return
[PROOF STEP]
by (metis \<open>\<pi>' 0 = \<pi> n\<close> \<open>\<pi>' n' = return\<close> add_diff_cancel_left' assms(2) diff_is_0_eq path_append_def)
[PROOF STATE]
proof (state)
this:
(\<pi> @\<^bsup>n\<^esup> \<pi>') (n + n') = local.return

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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<lbrakk>\<And>k. \<lbrakk>k \<le> n; \<pi> k = ipd (\<pi> 0)\<rbrakk> \<Longrightarrow> thesis; \<not> thesis\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have \<open>\<pi> 0 \<in> nodes\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi> 0 \<in> local.nodes
[PROOF STEP]
by (metis assms(1) path_nodes)
[PROOF STATE]
proof (state)
this:
\<pi> 0 \<in> local.nodes

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

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding is_pd_def
[PROOF STATE]
proof (prove)
using this:
\<forall>i. (\<pi> @\<^bsup>n\<^esup> \<pi>') i \<noteq> ipd (\<pi> 0)
(\<pi> @\<^bsup>n\<^esup> \<pi>') (n + n') = local.return
(\<pi> @\<^bsup>n\<^esup> \<pi>') 0 = \<pi> 0
is_path (\<pi> @\<^bsup>n\<^esup> \<pi>')
\<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)))
\<pi> 0 \<in> local.nodes

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

goal:
No subgoals!
[PROOF STEP]
qed