[STATEMENT]
lemma tree_subpath':
    assumes x: "(x,v) \<in> (tree_edges s)\<^sup>+"
    and y: "(y,v) \<in> (tree_edges s)\<^sup>+"
    and "x \<noteq> y"
    shows "(x,y) \<in> (tree_edges s)\<^sup>+ \<or> (y,x) \<in> (tree_edges s)\<^sup>+"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
from x
[PROOF STATE]
proof (chain)
picking this:
(x, v) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
obtain px where px: "path (tree_edges s) x px v" and "px \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
(x, v) \<in> (tree_edges s)\<^sup>+

goal (1 subgoal):
 1. (\<And>px. \<lbrakk>path (tree_edges s) x px v; px \<noteq> []\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using trancl_is_path
[PROOF STATE]
proof (prove)
using this:
(x, v) \<in> (tree_edges s)\<^sup>+
\<lbrakk>(?u, ?v) \<in> ?E\<^sup>+; \<And>l. \<lbrakk>l \<noteq> []; path ?E ?u l ?v\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>px. \<lbrakk>path (tree_edges s) x px v; px \<noteq> []\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
path (tree_edges s) x px v
px \<noteq> []

goal (1 subgoal):
 1. (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
from y
[PROOF STATE]
proof (chain)
picking this:
(y, v) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
obtain py where py: "path (tree_edges s) y py v" and "py \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
(y, v) \<in> (tree_edges s)\<^sup>+

goal (1 subgoal):
 1. (\<And>py. \<lbrakk>path (tree_edges s) y py v; py \<noteq> []\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using trancl_is_path
[PROOF STATE]
proof (prove)
using this:
(y, v) \<in> (tree_edges s)\<^sup>+
\<lbrakk>(?u, ?v) \<in> ?E\<^sup>+; \<And>l. \<lbrakk>l \<noteq> []; path ?E ?u l ?v\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>py. \<lbrakk>path (tree_edges s) y py v; py \<noteq> []\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
path (tree_edges s) y py v
py \<noteq> []

goal (1 subgoal):
 1. (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
from \<open>px \<noteq> []\<close> \<open>py \<noteq> []\<close> px py
[PROOF STATE]
proof (chain)
picking this:
px \<noteq> []
py \<noteq> []
path (tree_edges s) x px v
path (tree_edges s) y py v
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
px \<noteq> []
py \<noteq> []
path (tree_edges s) x px v
path (tree_edges s) y py v

goal (1 subgoal):
 1. (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
proof (induction arbitrary: v rule: rev_nonempty_induct2')
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>xa ya v. \<lbrakk>path (tree_edges s) x [xa] v; path (tree_edges s) y [ya] v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
 2. \<And>xa xs ya v. \<lbrakk>xs \<noteq> []; path (tree_edges s) x (xs @ [xa]) v; path (tree_edges s) y [ya] v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
 3. \<And>xa ya ys v. \<lbrakk>ys \<noteq> []; path (tree_edges s) x [xa] v; path (tree_edges s) y (ys @ [ya]) v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
 4. \<And>xa xs ya ys v. \<lbrakk>\<And>v. \<lbrakk>path (tree_edges s) x xs v; path (tree_edges s) y ys v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+; xs \<noteq> []; ys \<noteq> []; path (tree_edges s) x (xs @ [xa]) v; path (tree_edges s) y (ys @ [ya]) v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
case (single)
[PROOF STATE]
proof (state)
this:
path (tree_edges s) x [x_] v
path (tree_edges s) y [y_] v

goal (4 subgoals):
 1. \<And>xa ya v. \<lbrakk>path (tree_edges s) x [xa] v; path (tree_edges s) y [ya] v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
 2. \<And>xa xs ya v. \<lbrakk>xs \<noteq> []; path (tree_edges s) x (xs @ [xa]) v; path (tree_edges s) y [ya] v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
 3. \<And>xa ya ys v. \<lbrakk>ys \<noteq> []; path (tree_edges s) x [xa] v; path (tree_edges s) y (ys @ [ya]) v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
 4. \<And>xa xs ya ys v. \<lbrakk>\<And>v. \<lbrakk>path (tree_edges s) x xs v; path (tree_edges s) y ys v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+; xs \<noteq> []; ys \<noteq> []; path (tree_edges s) x (xs @ [xa]) v; path (tree_edges s) y (ys @ [ya]) v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
hence "(x,v) \<in> tree_edges s" "(y,v) \<in> tree_edges s"
[PROOF STATE]
proof (prove)
using this:
path (tree_edges s) x [x_] v
path (tree_edges s) y [y_] v

goal (1 subgoal):
 1. (x, v) \<in> tree_edges s &&& (y, v) \<in> tree_edges s
[PROOF STEP]
by (simp_all add: path_simps)
[PROOF STATE]
proof (state)
this:
(x, v) \<in> tree_edges s
(y, v) \<in> tree_edges s

goal (4 subgoals):
 1. \<And>xa ya v. \<lbrakk>path (tree_edges s) x [xa] v; path (tree_edges s) y [ya] v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
 2. \<And>xa xs ya v. \<lbrakk>xs \<noteq> []; path (tree_edges s) x (xs @ [xa]) v; path (tree_edges s) y [ya] v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
 3. \<And>xa ya ys v. \<lbrakk>ys \<noteq> []; path (tree_edges s) x [xa] v; path (tree_edges s) y (ys @ [ya]) v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
 4. \<And>xa xs ya ys v. \<lbrakk>\<And>v. \<lbrakk>path (tree_edges s) x xs v; path (tree_edges s) y ys v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+; xs \<noteq> []; ys \<noteq> []; path (tree_edges s) x (xs @ [xa]) v; path (tree_edges s) y (ys @ [ya]) v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
with tree_eq_rule
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>(?v, ?w) \<in> tree_edges s; (?u, ?w) \<in> tree_edges s\<rbrakk> \<Longrightarrow> ?v = ?u
(x, v) \<in> tree_edges s
(y, v) \<in> tree_edges s
[PROOF STEP]
have "x=y"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?v, ?w) \<in> tree_edges s; (?u, ?w) \<in> tree_edges s\<rbrakk> \<Longrightarrow> ?v = ?u
(x, v) \<in> tree_edges s
(y, v) \<in> tree_edges s

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

goal (4 subgoals):
 1. \<And>xa ya v. \<lbrakk>path (tree_edges s) x [xa] v; path (tree_edges s) y [ya] v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
 2. \<And>xa xs ya v. \<lbrakk>xs \<noteq> []; path (tree_edges s) x (xs @ [xa]) v; path (tree_edges s) y [ya] v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
 3. \<And>xa ya ys v. \<lbrakk>ys \<noteq> []; path (tree_edges s) x [xa] v; path (tree_edges s) y (ys @ [ya]) v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
 4. \<And>xa xs ya ys v. \<lbrakk>\<And>v. \<lbrakk>path (tree_edges s) x xs v; path (tree_edges s) y ys v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+; xs \<noteq> []; ys \<noteq> []; path (tree_edges s) x (xs @ [xa]) v; path (tree_edges s) y (ys @ [ya]) v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
with \<open>x\<noteq>y\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> y
x = y
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
x \<noteq> y
x = y

goal (1 subgoal):
 1. (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
by contradiction
[PROOF STATE]
proof (state)
this:
(x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+

goal (3 subgoals):
 1. \<And>xa xs ya v. \<lbrakk>xs \<noteq> []; path (tree_edges s) x (xs @ [xa]) v; path (tree_edges s) y [ya] v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
 2. \<And>xa ya ys v. \<lbrakk>ys \<noteq> []; path (tree_edges s) x [xa] v; path (tree_edges s) y (ys @ [ya]) v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
 3. \<And>xa xs ya ys v. \<lbrakk>\<And>v. \<lbrakk>path (tree_edges s) x xs v; path (tree_edges s) y ys v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+; xs \<noteq> []; ys \<noteq> []; path (tree_edges s) x (xs @ [xa]) v; path (tree_edges s) y (ys @ [ya]) v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>xa xs ya v. \<lbrakk>xs \<noteq> []; path (tree_edges s) x (xs @ [xa]) v; path (tree_edges s) y [ya] v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
 2. \<And>xa ya ys v. \<lbrakk>ys \<noteq> []; path (tree_edges s) x [xa] v; path (tree_edges s) y (ys @ [ya]) v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
 3. \<And>xa xs ya ys v. \<lbrakk>\<And>v. \<lbrakk>path (tree_edges s) x xs v; path (tree_edges s) y ys v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+; xs \<noteq> []; ys \<noteq> []; path (tree_edges s) x (xs @ [xa]) v; path (tree_edges s) y (ys @ [ya]) v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
case (snocl a as)
[PROOF STATE]
proof (state)
this:
as \<noteq> []
path (tree_edges s) x (as @ [a]) v
path (tree_edges s) y [y_] v

goal (3 subgoals):
 1. \<And>xa xs ya v. \<lbrakk>xs \<noteq> []; path (tree_edges s) x (xs @ [xa]) v; path (tree_edges s) y [ya] v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
 2. \<And>xa ya ys v. \<lbrakk>ys \<noteq> []; path (tree_edges s) x [xa] v; path (tree_edges s) y (ys @ [ya]) v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
 3. \<And>xa xs ya ys v. \<lbrakk>\<And>v. \<lbrakk>path (tree_edges s) x xs v; path (tree_edges s) y ys v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+; xs \<noteq> []; ys \<noteq> []; path (tree_edges s) x (xs @ [xa]) v; path (tree_edges s) y (ys @ [ya]) v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
hence "(y,v) \<in> tree_edges s"
[PROOF STATE]
proof (prove)
using this:
as \<noteq> []
path (tree_edges s) x (as @ [a]) v
path (tree_edges s) y [y_] v

goal (1 subgoal):
 1. (y, v) \<in> tree_edges s
[PROOF STEP]
by (simp add: path_simps)
[PROOF STATE]
proof (state)
this:
(y, v) \<in> tree_edges s

goal (3 subgoals):
 1. \<And>xa xs ya v. \<lbrakk>xs \<noteq> []; path (tree_edges s) x (xs @ [xa]) v; path (tree_edges s) y [ya] v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
 2. \<And>xa ya ys v. \<lbrakk>ys \<noteq> []; path (tree_edges s) x [xa] v; path (tree_edges s) y (ys @ [ya]) v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
 3. \<And>xa xs ya ys v. \<lbrakk>\<And>v. \<lbrakk>path (tree_edges s) x xs v; path (tree_edges s) y ys v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+; xs \<noteq> []; ys \<noteq> []; path (tree_edges s) x (xs @ [xa]) v; path (tree_edges s) y (ys @ [ya]) v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(y, v) \<in> tree_edges s

goal (3 subgoals):
 1. \<And>xa xs ya v. \<lbrakk>xs \<noteq> []; path (tree_edges s) x (xs @ [xa]) v; path (tree_edges s) y [ya] v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
 2. \<And>xa ya ys v. \<lbrakk>ys \<noteq> []; path (tree_edges s) x [xa] v; path (tree_edges s) y (ys @ [ya]) v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
 3. \<And>xa xs ya ys v. \<lbrakk>\<And>v. \<lbrakk>path (tree_edges s) x xs v; path (tree_edges s) y ys v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+; xs \<noteq> []; ys \<noteq> []; path (tree_edges s) x (xs @ [xa]) v; path (tree_edges s) y (ys @ [ya]) v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
from snocl
[PROOF STATE]
proof (chain)
picking this:
as \<noteq> []
path (tree_edges s) x (as @ [a]) v
path (tree_edges s) y [y_] v
[PROOF STEP]
have "path (tree_edges s) x as a" "(a,v) \<in> tree_edges s"
[PROOF STATE]
proof (prove)
using this:
as \<noteq> []
path (tree_edges s) x (as @ [a]) v
path (tree_edges s) y [y_] v

goal (1 subgoal):
 1. path (tree_edges s) x as a &&& (a, v) \<in> tree_edges s
[PROOF STEP]
by (simp_all add: path_simps)
[PROOF STATE]
proof (state)
this:
path (tree_edges s) x as a
(a, v) \<in> tree_edges s

goal (3 subgoals):
 1. \<And>xa xs ya v. \<lbrakk>xs \<noteq> []; path (tree_edges s) x (xs @ [xa]) v; path (tree_edges s) y [ya] v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
 2. \<And>xa ya ys v. \<lbrakk>ys \<noteq> []; path (tree_edges s) x [xa] v; path (tree_edges s) y (ys @ [ya]) v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
 3. \<And>xa xs ya ys v. \<lbrakk>\<And>v. \<lbrakk>path (tree_edges s) x xs v; path (tree_edges s) y ys v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+; xs \<noteq> []; ys \<noteq> []; path (tree_edges s) x (xs @ [xa]) v; path (tree_edges s) y (ys @ [ya]) v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(y, v) \<in> tree_edges s
path (tree_edges s) x as a
(a, v) \<in> tree_edges s
[PROOF STEP]
have "path (tree_edges s) x as y"
[PROOF STATE]
proof (prove)
using this:
(y, v) \<in> tree_edges s
path (tree_edges s) x as a
(a, v) \<in> tree_edges s

goal (1 subgoal):
 1. path (tree_edges s) x as y
[PROOF STEP]
using tree_eq_rule
[PROOF STATE]
proof (prove)
using this:
(y, v) \<in> tree_edges s
path (tree_edges s) x as a
(a, v) \<in> tree_edges s
\<lbrakk>(?v, ?w) \<in> tree_edges s; (?u, ?w) \<in> tree_edges s\<rbrakk> \<Longrightarrow> ?v = ?u

goal (1 subgoal):
 1. path (tree_edges s) x as y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
path (tree_edges s) x as y

goal (3 subgoals):
 1. \<And>xa xs ya v. \<lbrakk>xs \<noteq> []; path (tree_edges s) x (xs @ [xa]) v; path (tree_edges s) y [ya] v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
 2. \<And>xa ya ys v. \<lbrakk>ys \<noteq> []; path (tree_edges s) x [xa] v; path (tree_edges s) y (ys @ [ya]) v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
 3. \<And>xa xs ya ys v. \<lbrakk>\<And>v. \<lbrakk>path (tree_edges s) x xs v; path (tree_edges s) y ys v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+; xs \<noteq> []; ys \<noteq> []; path (tree_edges s) x (xs @ [xa]) v; path (tree_edges s) y (ys @ [ya]) v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
with path_is_trancl \<open>as \<noteq> []\<close>
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>path ?E ?u ?l ?v; ?l \<noteq> []\<rbrakk> \<Longrightarrow> (?u, ?v) \<in> ?E\<^sup>+
as \<noteq> []
path (tree_edges s) x as y
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>path ?E ?u ?l ?v; ?l \<noteq> []\<rbrakk> \<Longrightarrow> (?u, ?v) \<in> ?E\<^sup>+
as \<noteq> []
path (tree_edges s) x as y

goal (1 subgoal):
 1. (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+

goal (2 subgoals):
 1. \<And>xa ya ys v. \<lbrakk>ys \<noteq> []; path (tree_edges s) x [xa] v; path (tree_edges s) y (ys @ [ya]) v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
 2. \<And>xa xs ya ys v. \<lbrakk>\<And>v. \<lbrakk>path (tree_edges s) x xs v; path (tree_edges s) y ys v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+; xs \<noteq> []; ys \<noteq> []; path (tree_edges s) x (xs @ [xa]) v; path (tree_edges s) y (ys @ [ya]) v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xa ya ys v. \<lbrakk>ys \<noteq> []; path (tree_edges s) x [xa] v; path (tree_edges s) y (ys @ [ya]) v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
 2. \<And>xa xs ya ys v. \<lbrakk>\<And>v. \<lbrakk>path (tree_edges s) x xs v; path (tree_edges s) y ys v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+; xs \<noteq> []; ys \<noteq> []; path (tree_edges s) x (xs @ [xa]) v; path (tree_edges s) y (ys @ [ya]) v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
case (snocr _ a as)
[PROOF STATE]
proof (state)
this:
as \<noteq> []
path (tree_edges s) x [x_] v
path (tree_edges s) y (as @ [a]) v

goal (2 subgoals):
 1. \<And>xa ya ys v. \<lbrakk>ys \<noteq> []; path (tree_edges s) x [xa] v; path (tree_edges s) y (ys @ [ya]) v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
 2. \<And>xa xs ya ys v. \<lbrakk>\<And>v. \<lbrakk>path (tree_edges s) x xs v; path (tree_edges s) y ys v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+; xs \<noteq> []; ys \<noteq> []; path (tree_edges s) x (xs @ [xa]) v; path (tree_edges s) y (ys @ [ya]) v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
hence "(x,v) \<in> tree_edges s"
[PROOF STATE]
proof (prove)
using this:
as \<noteq> []
path (tree_edges s) x [x_] v
path (tree_edges s) y (as @ [a]) v

goal (1 subgoal):
 1. (x, v) \<in> tree_edges s
[PROOF STEP]
by (simp add: path_simps)
[PROOF STATE]
proof (state)
this:
(x, v) \<in> tree_edges s

goal (2 subgoals):
 1. \<And>xa ya ys v. \<lbrakk>ys \<noteq> []; path (tree_edges s) x [xa] v; path (tree_edges s) y (ys @ [ya]) v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
 2. \<And>xa xs ya ys v. \<lbrakk>\<And>v. \<lbrakk>path (tree_edges s) x xs v; path (tree_edges s) y ys v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+; xs \<noteq> []; ys \<noteq> []; path (tree_edges s) x (xs @ [xa]) v; path (tree_edges s) y (ys @ [ya]) v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(x, v) \<in> tree_edges s

goal (2 subgoals):
 1. \<And>xa ya ys v. \<lbrakk>ys \<noteq> []; path (tree_edges s) x [xa] v; path (tree_edges s) y (ys @ [ya]) v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
 2. \<And>xa xs ya ys v. \<lbrakk>\<And>v. \<lbrakk>path (tree_edges s) x xs v; path (tree_edges s) y ys v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+; xs \<noteq> []; ys \<noteq> []; path (tree_edges s) x (xs @ [xa]) v; path (tree_edges s) y (ys @ [ya]) v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
from snocr
[PROOF STATE]
proof (chain)
picking this:
as \<noteq> []
path (tree_edges s) x [x_] v
path (tree_edges s) y (as @ [a]) v
[PROOF STEP]
have "path (tree_edges s) y as a" "(a,v) \<in> tree_edges s"
[PROOF STATE]
proof (prove)
using this:
as \<noteq> []
path (tree_edges s) x [x_] v
path (tree_edges s) y (as @ [a]) v

goal (1 subgoal):
 1. path (tree_edges s) y as a &&& (a, v) \<in> tree_edges s
[PROOF STEP]
by (simp_all add: path_simps)
[PROOF STATE]
proof (state)
this:
path (tree_edges s) y as a
(a, v) \<in> tree_edges s

goal (2 subgoals):
 1. \<And>xa ya ys v. \<lbrakk>ys \<noteq> []; path (tree_edges s) x [xa] v; path (tree_edges s) y (ys @ [ya]) v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
 2. \<And>xa xs ya ys v. \<lbrakk>\<And>v. \<lbrakk>path (tree_edges s) x xs v; path (tree_edges s) y ys v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+; xs \<noteq> []; ys \<noteq> []; path (tree_edges s) x (xs @ [xa]) v; path (tree_edges s) y (ys @ [ya]) v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(x, v) \<in> tree_edges s
path (tree_edges s) y as a
(a, v) \<in> tree_edges s
[PROOF STEP]
have "path (tree_edges s) y as x"
[PROOF STATE]
proof (prove)
using this:
(x, v) \<in> tree_edges s
path (tree_edges s) y as a
(a, v) \<in> tree_edges s

goal (1 subgoal):
 1. path (tree_edges s) y as x
[PROOF STEP]
using tree_eq_rule
[PROOF STATE]
proof (prove)
using this:
(x, v) \<in> tree_edges s
path (tree_edges s) y as a
(a, v) \<in> tree_edges s
\<lbrakk>(?v, ?w) \<in> tree_edges s; (?u, ?w) \<in> tree_edges s\<rbrakk> \<Longrightarrow> ?v = ?u

goal (1 subgoal):
 1. path (tree_edges s) y as x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
path (tree_edges s) y as x

goal (2 subgoals):
 1. \<And>xa ya ys v. \<lbrakk>ys \<noteq> []; path (tree_edges s) x [xa] v; path (tree_edges s) y (ys @ [ya]) v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
 2. \<And>xa xs ya ys v. \<lbrakk>\<And>v. \<lbrakk>path (tree_edges s) x xs v; path (tree_edges s) y ys v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+; xs \<noteq> []; ys \<noteq> []; path (tree_edges s) x (xs @ [xa]) v; path (tree_edges s) y (ys @ [ya]) v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
with path_is_trancl \<open>as \<noteq> []\<close>
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>path ?E ?u ?l ?v; ?l \<noteq> []\<rbrakk> \<Longrightarrow> (?u, ?v) \<in> ?E\<^sup>+
as \<noteq> []
path (tree_edges s) y as x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>path ?E ?u ?l ?v; ?l \<noteq> []\<rbrakk> \<Longrightarrow> (?u, ?v) \<in> ?E\<^sup>+
as \<noteq> []
path (tree_edges s) y as x

goal (1 subgoal):
 1. (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+

goal (1 subgoal):
 1. \<And>xa xs ya ys v. \<lbrakk>\<And>v. \<lbrakk>path (tree_edges s) x xs v; path (tree_edges s) y ys v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+; xs \<noteq> []; ys \<noteq> []; path (tree_edges s) x (xs @ [xa]) v; path (tree_edges s) y (ys @ [ya]) v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa xs ya ys v. \<lbrakk>\<And>v. \<lbrakk>path (tree_edges s) x xs v; path (tree_edges s) y ys v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+; xs \<noteq> []; ys \<noteq> []; path (tree_edges s) x (xs @ [xa]) v; path (tree_edges s) y (ys @ [ya]) v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
case (snoclr a as b bs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>path (tree_edges s) x as ?v7; path (tree_edges s) y bs ?v7\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
as \<noteq> []
bs \<noteq> []
path (tree_edges s) x (as @ [a]) v
path (tree_edges s) y (bs @ [b]) v

goal (1 subgoal):
 1. \<And>xa xs ya ys v. \<lbrakk>\<And>v. \<lbrakk>path (tree_edges s) x xs v; path (tree_edges s) y ys v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+; xs \<noteq> []; ys \<noteq> []; path (tree_edges s) x (xs @ [xa]) v; path (tree_edges s) y (ys @ [ya]) v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
hence
        "path (tree_edges s) x as a" "(a,v) \<in> tree_edges s"
        "path (tree_edges s) y bs b" "(b,v) \<in> tree_edges s"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>path (tree_edges s) x as ?v7; path (tree_edges s) y bs ?v7\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
as \<noteq> []
bs \<noteq> []
path (tree_edges s) x (as @ [a]) v
path (tree_edges s) y (bs @ [b]) v

goal (1 subgoal):
 1. (path (tree_edges s) x as a &&& (a, v) \<in> tree_edges s) &&& path (tree_edges s) y bs b &&& (b, v) \<in> tree_edges s
[PROOF STEP]
by (simp_all add: path_simps)
[PROOF STATE]
proof (state)
this:
path (tree_edges s) x as a
(a, v) \<in> tree_edges s
path (tree_edges s) y bs b
(b, v) \<in> tree_edges s

goal (1 subgoal):
 1. \<And>xa xs ya ys v. \<lbrakk>\<And>v. \<lbrakk>path (tree_edges s) x xs v; path (tree_edges s) y ys v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+; xs \<noteq> []; ys \<noteq> []; path (tree_edges s) x (xs @ [xa]) v; path (tree_edges s) y (ys @ [ya]) v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
path (tree_edges s) x as a
(a, v) \<in> tree_edges s
path (tree_edges s) y bs b
(b, v) \<in> tree_edges s

goal (1 subgoal):
 1. \<And>xa xs ya ys v. \<lbrakk>\<And>v. \<lbrakk>path (tree_edges s) x xs v; path (tree_edges s) y ys v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+; xs \<noteq> []; ys \<noteq> []; path (tree_edges s) x (xs @ [xa]) v; path (tree_edges s) y (ys @ [ya]) v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
hence "a=b"
[PROOF STATE]
proof (prove)
using this:
path (tree_edges s) x as a
(a, v) \<in> tree_edges s
path (tree_edges s) y bs b
(b, v) \<in> tree_edges s

goal (1 subgoal):
 1. a = b
[PROOF STEP]
using tree_eq_rule
[PROOF STATE]
proof (prove)
using this:
path (tree_edges s) x as a
(a, v) \<in> tree_edges s
path (tree_edges s) y bs b
(b, v) \<in> tree_edges s
\<lbrakk>(?v, ?w) \<in> tree_edges s; (?u, ?w) \<in> tree_edges s\<rbrakk> \<Longrightarrow> ?v = ?u

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

goal (1 subgoal):
 1. \<And>xa xs ya ys v. \<lbrakk>\<And>v. \<lbrakk>path (tree_edges s) x xs v; path (tree_edges s) y ys v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+; xs \<noteq> []; ys \<noteq> []; path (tree_edges s) x (xs @ [xa]) v; path (tree_edges s) y (ys @ [ya]) v\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
path (tree_edges s) x as a
(a, v) \<in> tree_edges s
path (tree_edges s) y bs b
(b, v) \<in> tree_edges s
a = b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
path (tree_edges s) x as a
(a, v) \<in> tree_edges s
path (tree_edges s) y bs b
(b, v) \<in> tree_edges s
a = b

goal (1 subgoal):
 1. (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
using snoclr.IH
[PROOF STATE]
proof (prove)
using this:
path (tree_edges s) x as a
(a, v) \<in> tree_edges s
path (tree_edges s) y bs b
(b, v) \<in> tree_edges s
a = b
\<lbrakk>path (tree_edges s) x as ?v7; path (tree_edges s) y bs ?v7\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+

goal (1 subgoal):
 1. (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma tree_subpath:
    assumes "(x,v) \<in> (tree_edges s)\<^sup>+"
    and "(y,v) \<in> (tree_edges s)\<^sup>+"
    and \<delta>: "\<delta> s x < \<delta> s y"
    shows "(x,y) \<in> (tree_edges s)\<^sup>+"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x, y) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (x, y) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
from \<delta>
[PROOF STATE]
proof (chain)
picking this:
\<delta> s x < \<delta> s y
[PROOF STEP]
have "x \<noteq> y"
[PROOF STATE]
proof (prove)
using this:
\<delta> s x < \<delta> s y

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

goal (1 subgoal):
 1. (x, y) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
with assms tree_subpath'
[PROOF STATE]
proof (chain)
picking this:
(x, v) \<in> (tree_edges s)\<^sup>+
(y, v) \<in> (tree_edges s)\<^sup>+
\<delta> s x < \<delta> s y
\<lbrakk>(?x, ?v) \<in> (tree_edges s)\<^sup>+; (?y, ?v) \<in> (tree_edges s)\<^sup>+; ?x \<noteq> ?y\<rbrakk> \<Longrightarrow> (?x, ?y) \<in> (tree_edges s)\<^sup>+ \<or> (?y, ?x) \<in> (tree_edges s)\<^sup>+
x \<noteq> y
[PROOF STEP]
have "(x,y) \<in> (tree_edges s)\<^sup>+ \<or> (y,x) \<in> (tree_edges s)\<^sup>+"
[PROOF STATE]
proof (prove)
using this:
(x, v) \<in> (tree_edges s)\<^sup>+
(y, v) \<in> (tree_edges s)\<^sup>+
\<delta> s x < \<delta> s y
\<lbrakk>(?x, ?v) \<in> (tree_edges s)\<^sup>+; (?y, ?v) \<in> (tree_edges s)\<^sup>+; ?x \<noteq> ?y\<rbrakk> \<Longrightarrow> (?x, ?y) \<in> (tree_edges s)\<^sup>+ \<or> (?y, ?x) \<in> (tree_edges s)\<^sup>+
x \<noteq> y

goal (1 subgoal):
 1. (x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+

goal (1 subgoal):
 1. (x, y) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+

goal (1 subgoal):
 1. (x, y) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
from \<delta> tree_path_disc
[PROOF STATE]
proof (chain)
picking this:
\<delta> s x < \<delta> s y
(?v, ?w) \<in> (tree_edges s)\<^sup>+ \<Longrightarrow> \<delta> s ?v < \<delta> s ?w
[PROOF STEP]
have "(y,x) \<notin> (tree_edges s)\<^sup>+"
[PROOF STATE]
proof (prove)
using this:
\<delta> s x < \<delta> s y
(?v, ?w) \<in> (tree_edges s)\<^sup>+ \<Longrightarrow> \<delta> s ?v < \<delta> s ?w

goal (1 subgoal):
 1. (y, x) \<notin> (tree_edges s)\<^sup>+
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(y, x) \<notin> (tree_edges s)\<^sup>+

goal (1 subgoal):
 1. (x, y) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
(y, x) \<notin> (tree_edges s)\<^sup>+
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> (tree_edges s)\<^sup>+ \<or> (y, x) \<in> (tree_edges s)\<^sup>+
(y, x) \<notin> (tree_edges s)\<^sup>+

goal (1 subgoal):
 1. (x, y) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(x, y) \<in> (tree_edges s)\<^sup>+

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma on_stack_is_tree_path:
    assumes x: "x \<in> set (stack s)"
    and y: "y \<in> set (stack s)"
    and \<delta>: "\<delta> s x < \<delta> s y"
    shows "(x,y) \<in> (tree_edges s)\<^sup>+"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x, y) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (x, y) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
from x
[PROOF STATE]
proof (chain)
picking this:
x \<in> set (stack s)
[PROOF STEP]
obtain i where i: "stack s ! i = x" "i < length (stack s)"
[PROOF STATE]
proof (prove)
using this:
x \<in> set (stack s)

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>stack s ! i = x; i < length (stack s)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis in_set_conv_nth)
[PROOF STATE]
proof (state)
this:
stack s ! i = x
i < length (stack s)

goal (1 subgoal):
 1. (x, y) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
from y
[PROOF STATE]
proof (chain)
picking this:
y \<in> set (stack s)
[PROOF STEP]
obtain j where j: "stack s ! j = y" "j < length (stack s)"
[PROOF STATE]
proof (prove)
using this:
y \<in> set (stack s)

goal (1 subgoal):
 1. (\<And>j. \<lbrakk>stack s ! j = y; j < length (stack s)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis in_set_conv_nth)
[PROOF STATE]
proof (state)
this:
stack s ! j = y
j < length (stack s)

goal (1 subgoal):
 1. (x, y) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
with i \<delta> stack_nth_order
[PROOF STATE]
proof (chain)
picking this:
stack s ! i = x
i < length (stack s)
\<delta> s x < \<delta> s y
\<lbrakk>?i < length (stack s); ?j < length (stack s)\<rbrakk> \<Longrightarrow> (\<delta> s (stack s ! ?i) < \<delta> s (stack s ! ?j)) = (?j < ?i)
stack s ! j = y
j < length (stack s)
[PROOF STEP]
have "j < i"
[PROOF STATE]
proof (prove)
using this:
stack s ! i = x
i < length (stack s)
\<delta> s x < \<delta> s y
\<lbrakk>?i < length (stack s); ?j < length (stack s)\<rbrakk> \<Longrightarrow> (\<delta> s (stack s ! ?i) < \<delta> s (stack s ! ?j)) = (?j < ?i)
stack s ! j = y
j < length (stack s)

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

goal (1 subgoal):
 1. (x, y) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
from x
[PROOF STATE]
proof (chain)
picking this:
x \<in> set (stack s)
[PROOF STEP]
have ne[simp]: "stack s \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
x \<in> set (stack s)

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

goal (1 subgoal):
 1. (x, y) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
from \<open>j<i\<close>
[PROOF STATE]
proof (chain)
picking this:
j < i
[PROOF STEP]
have "x \<in> set (tl (stack s))"
[PROOF STATE]
proof (prove)
using this:
j < i

goal (1 subgoal):
 1. x \<in> set (tl (stack s))
[PROOF STEP]
using nth_mem nth_tl[OF ne, of "i - 1"] i
[PROOF STATE]
proof (prove)
using this:
j < i
?n < length ?xs \<Longrightarrow> ?xs ! ?n \<in> set ?xs
tl (stack s) ! (i - 1) = stack s ! Suc (i - 1)
stack s ! i = x
i < length (stack s)

goal (1 subgoal):
 1. x \<in> set (tl (stack s))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> set (tl (stack s))

goal (1 subgoal):
 1. (x, y) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
with tl_stack_hd_tree_path
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>stack s \<noteq> []; ?v \<in> set (tl (stack s))\<rbrakk> \<Longrightarrow> (?v, hd (stack s)) \<in> (tree_edges s)\<^sup>+
x \<in> set (tl (stack s))
[PROOF STEP]
have
      x_path: "(x, hd (stack s)) \<in> (tree_edges s)\<^sup>+"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>stack s \<noteq> []; ?v \<in> set (tl (stack s))\<rbrakk> \<Longrightarrow> (?v, hd (stack s)) \<in> (tree_edges s)\<^sup>+
x \<in> set (tl (stack s))

goal (1 subgoal):
 1. (x, hd (stack s)) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(x, hd (stack s)) \<in> (tree_edges s)\<^sup>+

goal (1 subgoal):
 1. (x, y) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(x, hd (stack s)) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(x, hd (stack s)) \<in> (tree_edges s)\<^sup>+

goal (1 subgoal):
 1. (x, y) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
proof (cases "j=0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>(x, hd (stack s)) \<in> (tree_edges s)\<^sup>+; j = 0\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+
 2. \<lbrakk>(x, hd (stack s)) \<in> (tree_edges s)\<^sup>+; j \<noteq> 0\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
j = 0

goal (2 subgoals):
 1. \<lbrakk>(x, hd (stack s)) \<in> (tree_edges s)\<^sup>+; j = 0\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+
 2. \<lbrakk>(x, hd (stack s)) \<in> (tree_edges s)\<^sup>+; j \<noteq> 0\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
with j
[PROOF STATE]
proof (chain)
picking this:
stack s ! j = y
j < length (stack s)
j = 0
[PROOF STEP]
have "hd (stack s) = y"
[PROOF STATE]
proof (prove)
using this:
stack s ! j = y
j < length (stack s)
j = 0

goal (1 subgoal):
 1. hd (stack s) = y
[PROOF STEP]
by (metis hd_conv_nth ne)
[PROOF STATE]
proof (state)
this:
hd (stack s) = y

goal (2 subgoals):
 1. \<lbrakk>(x, hd (stack s)) \<in> (tree_edges s)\<^sup>+; j = 0\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+
 2. \<lbrakk>(x, hd (stack s)) \<in> (tree_edges s)\<^sup>+; j \<noteq> 0\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
with x_path
[PROOF STATE]
proof (chain)
picking this:
(x, hd (stack s)) \<in> (tree_edges s)\<^sup>+
hd (stack s) = y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(x, hd (stack s)) \<in> (tree_edges s)\<^sup>+
hd (stack s) = y

goal (1 subgoal):
 1. (x, y) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(x, y) \<in> (tree_edges s)\<^sup>+

goal (1 subgoal):
 1. \<lbrakk>(x, hd (stack s)) \<in> (tree_edges s)\<^sup>+; j \<noteq> 0\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>(x, hd (stack s)) \<in> (tree_edges s)\<^sup>+; j \<noteq> 0\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
j \<noteq> 0

goal (1 subgoal):
 1. \<lbrakk>(x, hd (stack s)) \<in> (tree_edges s)\<^sup>+; j \<noteq> 0\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
hence "y \<in> set (tl (stack s))"
[PROOF STATE]
proof (prove)
using this:
j \<noteq> 0

goal (1 subgoal):
 1. y \<in> set (tl (stack s))
[PROOF STEP]
using nth_mem nth_tl[OF ne, of "j - 1"] j
[PROOF STATE]
proof (prove)
using this:
j \<noteq> 0
?n < length ?xs \<Longrightarrow> ?xs ! ?n \<in> set ?xs
tl (stack s) ! (j - 1) = stack s ! Suc (j - 1)
stack s ! j = y
j < length (stack s)

goal (1 subgoal):
 1. y \<in> set (tl (stack s))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<in> set (tl (stack s))

goal (1 subgoal):
 1. \<lbrakk>(x, hd (stack s)) \<in> (tree_edges s)\<^sup>+; j \<noteq> 0\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
with tl_stack_hd_tree_path
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>stack s \<noteq> []; ?v \<in> set (tl (stack s))\<rbrakk> \<Longrightarrow> (?v, hd (stack s)) \<in> (tree_edges s)\<^sup>+
y \<in> set (tl (stack s))
[PROOF STEP]
have "(y, hd (stack s)) \<in> (tree_edges s)\<^sup>+"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>stack s \<noteq> []; ?v \<in> set (tl (stack s))\<rbrakk> \<Longrightarrow> (?v, hd (stack s)) \<in> (tree_edges s)\<^sup>+
y \<in> set (tl (stack s))

goal (1 subgoal):
 1. (y, hd (stack s)) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(y, hd (stack s)) \<in> (tree_edges s)\<^sup>+

goal (1 subgoal):
 1. \<lbrakk>(x, hd (stack s)) \<in> (tree_edges s)\<^sup>+; j \<noteq> 0\<rbrakk> \<Longrightarrow> (x, y) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
with x_path \<delta>
[PROOF STATE]
proof (chain)
picking this:
(x, hd (stack s)) \<in> (tree_edges s)\<^sup>+
\<delta> s x < \<delta> s y
(y, hd (stack s)) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(x, hd (stack s)) \<in> (tree_edges s)\<^sup>+
\<delta> s x < \<delta> s y
(y, hd (stack s)) \<in> (tree_edges s)\<^sup>+

goal (1 subgoal):
 1. (x, y) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
using tree_subpath
[PROOF STATE]
proof (prove)
using this:
(x, hd (stack s)) \<in> (tree_edges s)\<^sup>+
\<delta> s x < \<delta> s y
(y, hd (stack s)) \<in> (tree_edges s)\<^sup>+
\<lbrakk>(?x, ?v) \<in> (tree_edges s)\<^sup>+; (?y, ?v) \<in> (tree_edges s)\<^sup>+; \<delta> s ?x < \<delta> s ?y\<rbrakk> \<Longrightarrow> (?x, ?y) \<in> (tree_edges s)\<^sup>+

goal (1 subgoal):
 1. (x, y) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(x, y) \<in> (tree_edges s)\<^sup>+

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(x, y) \<in> (tree_edges s)\<^sup>+

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma hd_stack_tree_path_finished:
    assumes "stack s \<noteq> []"
    assumes "(hd (stack s), v) \<in> (tree_edges s)\<^sup>+"
    shows "v \<in> dom (finished s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> dom (finished s)
[PROOF STEP]
proof (cases "v \<in> set (stack s)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. v \<in> set (stack s) \<Longrightarrow> v \<in> dom (finished s)
 2. v \<notin> set (stack s) \<Longrightarrow> v \<in> dom (finished s)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
v \<in> set (stack s)

goal (2 subgoals):
 1. v \<in> set (stack s) \<Longrightarrow> v \<in> dom (finished s)
 2. v \<notin> set (stack s) \<Longrightarrow> v \<in> dom (finished s)
[PROOF STEP]
from assms no_loop_in_tree
[PROOF STATE]
proof (chain)
picking this:
stack s \<noteq> []
(hd (stack s), v) \<in> (tree_edges s)\<^sup>+
(?v, ?v) \<notin> (tree_edges s)\<^sup>+
[PROOF STEP]
have "hd (stack s) \<noteq> v"
[PROOF STATE]
proof (prove)
using this:
stack s \<noteq> []
(hd (stack s), v) \<in> (tree_edges s)\<^sup>+
(?v, ?v) \<notin> (tree_edges s)\<^sup>+

goal (1 subgoal):
 1. hd (stack s) \<noteq> v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
hd (stack s) \<noteq> v

goal (2 subgoals):
 1. v \<in> set (stack s) \<Longrightarrow> v \<in> dom (finished s)
 2. v \<notin> set (stack s) \<Longrightarrow> v \<in> dom (finished s)
[PROOF STEP]
with True
[PROOF STATE]
proof (chain)
picking this:
v \<in> set (stack s)
hd (stack s) \<noteq> v
[PROOF STEP]
have "v \<in> set (tl (stack s))"
[PROOF STATE]
proof (prove)
using this:
v \<in> set (stack s)
hd (stack s) \<noteq> v

goal (1 subgoal):
 1. v \<in> set (tl (stack s))
[PROOF STEP]
by (cases "stack s") auto
[PROOF STATE]
proof (state)
this:
v \<in> set (tl (stack s))

goal (2 subgoals):
 1. v \<in> set (stack s) \<Longrightarrow> v \<in> dom (finished s)
 2. v \<notin> set (stack s) \<Longrightarrow> v \<in> dom (finished s)
[PROOF STEP]
with tl_stack_hd_tree_path assms
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>stack s \<noteq> []; ?v \<in> set (tl (stack s))\<rbrakk> \<Longrightarrow> (?v, hd (stack s)) \<in> (tree_edges s)\<^sup>+
stack s \<noteq> []
(hd (stack s), v) \<in> (tree_edges s)\<^sup>+
v \<in> set (tl (stack s))
[PROOF STEP]
have "(hd (stack s), hd (stack s)) \<in> (tree_edges s)\<^sup>+"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>stack s \<noteq> []; ?v \<in> set (tl (stack s))\<rbrakk> \<Longrightarrow> (?v, hd (stack s)) \<in> (tree_edges s)\<^sup>+
stack s \<noteq> []
(hd (stack s), v) \<in> (tree_edges s)\<^sup>+
v \<in> set (tl (stack s))

goal (1 subgoal):
 1. (hd (stack s), hd (stack s)) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
by (metis trancl_trans)
[PROOF STATE]
proof (state)
this:
(hd (stack s), hd (stack s)) \<in> (tree_edges s)\<^sup>+

goal (2 subgoals):
 1. v \<in> set (stack s) \<Longrightarrow> v \<in> dom (finished s)
 2. v \<notin> set (stack s) \<Longrightarrow> v \<in> dom (finished s)
[PROOF STEP]
with no_loop_in_tree
[PROOF STATE]
proof (chain)
picking this:
(?v, ?v) \<notin> (tree_edges s)\<^sup>+
(hd (stack s), hd (stack s)) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(?v, ?v) \<notin> (tree_edges s)\<^sup>+
(hd (stack s), hd (stack s)) \<in> (tree_edges s)\<^sup>+

goal (1 subgoal):
 1. v \<in> dom (finished s)
[PROOF STEP]
by contradiction
[PROOF STATE]
proof (state)
this:
v \<in> dom (finished s)

goal (1 subgoal):
 1. v \<notin> set (stack s) \<Longrightarrow> v \<in> dom (finished s)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. v \<notin> set (stack s) \<Longrightarrow> v \<in> dom (finished s)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
v \<notin> set (stack s)

goal (1 subgoal):
 1. v \<notin> set (stack s) \<Longrightarrow> v \<in> dom (finished s)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
stack s \<noteq> []
(hd (stack s), v) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
obtain x where "(x,v) \<in> tree_edges s"
[PROOF STATE]
proof (prove)
using this:
stack s \<noteq> []
(hd (stack s), v) \<in> (tree_edges s)\<^sup>+

goal (1 subgoal):
 1. (\<And>x. (x, v) \<in> tree_edges s \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis tranclE)
[PROOF STATE]
proof (state)
this:
(x, v) \<in> tree_edges s

goal (1 subgoal):
 1. v \<notin> set (stack s) \<Longrightarrow> v \<in> dom (finished s)
[PROOF STEP]
with tree_edge_imp_discovered
[PROOF STATE]
proof (chain)
picking this:
(?v, ?w) \<in> tree_edges s \<Longrightarrow> ?v \<in> dom (discovered s)
(?v, ?w) \<in> tree_edges s \<Longrightarrow> ?w \<in> dom (discovered s)
(x, v) \<in> tree_edges s
[PROOF STEP]
have "v \<in> dom (discovered s)"
[PROOF STATE]
proof (prove)
using this:
(?v, ?w) \<in> tree_edges s \<Longrightarrow> ?v \<in> dom (discovered s)
(?v, ?w) \<in> tree_edges s \<Longrightarrow> ?w \<in> dom (discovered s)
(x, v) \<in> tree_edges s

goal (1 subgoal):
 1. v \<in> dom (discovered s)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
v \<in> dom (discovered s)

goal (1 subgoal):
 1. v \<notin> set (stack s) \<Longrightarrow> v \<in> dom (finished s)
[PROOF STEP]
with False
[PROOF STATE]
proof (chain)
picking this:
v \<notin> set (stack s)
v \<in> dom (discovered s)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
v \<notin> set (stack s)
v \<in> dom (discovered s)

goal (1 subgoal):
 1. v \<in> dom (finished s)
[PROOF STEP]
by (simp add: stack_set_def)
[PROOF STATE]
proof (state)
this:
v \<in> dom (finished s)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma tree_edge_impl_parenthesis:
    assumes t: "(v,w) \<in> tree_edges s"
    and f: "v \<in> dom (finished s)"
    shows "w \<in> dom (finished s)
      \<and> \<delta> s v < \<delta> s w
      \<and> \<phi> s w < \<phi> s v "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w \<in> dom (finished s) \<and> \<delta> s v < \<delta> s w \<and> \<phi> s w < \<phi> s v
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. w \<in> dom (finished s) \<and> \<delta> s v < \<delta> s w \<and> \<phi> s w < \<phi> s v
[PROOF STEP]
from tree_edge_disc_lt_fin assms
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>(?v, ?w) \<in> tree_edges s; ?v \<in> dom (finished s)\<rbrakk> \<Longrightarrow> \<delta> s ?w < \<phi> s ?v
(v, w) \<in> tree_edges s
v \<in> dom (finished s)
[PROOF STEP]
have "\<delta> s w < \<phi> s v"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?v, ?w) \<in> tree_edges s; ?v \<in> dom (finished s)\<rbrakk> \<Longrightarrow> \<delta> s ?w < \<phi> s ?v
(v, w) \<in> tree_edges s
v \<in> dom (finished s)

goal (1 subgoal):
 1. \<delta> s w < \<phi> s v
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<delta> s w < \<phi> s v

goal (1 subgoal):
 1. w \<in> dom (finished s) \<and> \<delta> s v < \<delta> s w \<and> \<phi> s w < \<phi> s v
[PROOF STEP]
with f tree_edge_imp_discovered[OF t] tree_edge_disc[OF t]
[PROOF STATE]
proof (chain)
picking this:
v \<in> dom (finished s)
v \<in> dom (discovered s)
w \<in> dom (discovered s)
\<delta> s v < \<delta> s w
\<delta> s w < \<phi> s v
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
v \<in> dom (finished s)
v \<in> dom (discovered s)
w \<in> dom (discovered s)
\<delta> s v < \<delta> s w
\<delta> s w < \<phi> s v

goal (1 subgoal):
 1. w \<in> dom (finished s) \<and> \<delta> s v < \<delta> s w \<and> \<phi> s w < \<phi> s v
[PROOF STEP]
using parenthesis_contained
[PROOF STATE]
proof (prove)
using this:
v \<in> dom (finished s)
v \<in> dom (discovered s)
w \<in> dom (discovered s)
\<delta> s v < \<delta> s w
\<delta> s w < \<phi> s v
\<lbrakk>?v \<in> dom (finished s); ?w \<in> dom (discovered s); \<delta> s ?v < \<delta> s ?w; \<delta> s ?w < \<phi> s ?v\<rbrakk> \<Longrightarrow> ?w \<in> dom (finished s) \<and> \<phi> s ?w < \<phi> s ?v

goal (1 subgoal):
 1. w \<in> dom (finished s) \<and> \<delta> s v < \<delta> s w \<and> \<phi> s w < \<phi> s v
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
w \<in> dom (finished s) \<and> \<delta> s v < \<delta> s w \<and> \<phi> s w < \<phi> s v

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma tree_path_impl_parenthesis:
    assumes "(v,w) \<in> (tree_edges s)\<^sup>+"
    and "v \<in> dom (finished s)"
    shows "w \<in> dom (finished s)
      \<and> \<delta> s v < \<delta> s w
      \<and> \<phi> s w < \<phi> s v "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w \<in> dom (finished s) \<and> \<delta> s v < \<delta> s w \<and> \<phi> s w < \<phi> s v
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(v, w) \<in> (tree_edges s)\<^sup>+
v \<in> dom (finished s)

goal (1 subgoal):
 1. w \<in> dom (finished s) \<and> \<delta> s v < \<delta> s w \<and> \<phi> s w < \<phi> s v
[PROOF STEP]
by (auto elim!: trancl_induct dest: tree_edge_impl_parenthesis)


[STATEMENT]
lemma nc_reachable_v0_parenthesis:
    assumes C: "\<not> cond s" "\<not> is_break param s"
    and v: "v \<in> reachable" "v \<notin> V0"
    obtains v0 where "v0 \<in> V0"
                 and "\<delta> s v0 < \<delta> s v \<and> \<phi> s v < \<phi> s v0 "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>v0. \<lbrakk>v0 \<in> V0; \<delta> s v0 < \<delta> s v \<and> \<phi> s v < \<phi> s v0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>v0. \<lbrakk>v0 \<in> V0; \<delta> s v0 < \<delta> s v \<and> \<phi> s v < \<phi> s v0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from nc_discovered_eq_reachable[OF C] discovered_iff_tree_path v
[PROOF STATE]
proof (chain)
picking this:
dom (discovered s) = reachable
?v \<notin> V0 \<Longrightarrow> (?v \<in> dom (discovered s)) = (\<exists>v0\<in>V0. (v0, ?v) \<in> (tree_edges s)\<^sup>+)
v \<in> reachable
v \<notin> V0
[PROOF STEP]
obtain v0 where "v0 \<in> V0" and
      "(v0,v) \<in> (tree_edges s)\<^sup>+"
[PROOF STATE]
proof (prove)
using this:
dom (discovered s) = reachable
?v \<notin> V0 \<Longrightarrow> (?v \<in> dom (discovered s)) = (\<exists>v0\<in>V0. (v0, ?v) \<in> (tree_edges s)\<^sup>+)
v \<in> reachable
v \<notin> V0

goal (1 subgoal):
 1. (\<And>v0. \<lbrakk>v0 \<in> V0; (v0, v) \<in> (tree_edges s)\<^sup>+\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v0 \<in> V0
(v0, v) \<in> (tree_edges s)\<^sup>+

goal (1 subgoal):
 1. (\<And>v0. \<lbrakk>v0 \<in> V0; \<delta> s v0 < \<delta> s v \<and> \<phi> s v < \<phi> s v0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
v0 \<in> V0
(v0, v) \<in> (tree_edges s)\<^sup>+

goal (1 subgoal):
 1. (\<And>v0. \<lbrakk>v0 \<in> V0; \<delta> s v0 < \<delta> s v \<and> \<phi> s v < \<phi> s v0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with nc_V0_finished[OF C]
[PROOF STATE]
proof (chain)
picking this:
V0 \<subseteq> dom (finished s)
v0 \<in> V0
(v0, v) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
have "v0 \<in> dom (finished s)"
[PROOF STATE]
proof (prove)
using this:
V0 \<subseteq> dom (finished s)
v0 \<in> V0
(v0, v) \<in> (tree_edges s)\<^sup>+

goal (1 subgoal):
 1. v0 \<in> dom (finished s)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v0 \<in> dom (finished s)

goal (1 subgoal):
 1. (\<And>v0. \<lbrakk>v0 \<in> V0; \<delta> s v0 < \<delta> s v \<and> \<phi> s v < \<phi> s v0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
v0 \<in> V0
(v0, v) \<in> (tree_edges s)\<^sup>+
v0 \<in> dom (finished s)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
v0 \<in> V0
(v0, v) \<in> (tree_edges s)\<^sup>+
v0 \<in> dom (finished s)

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using tree_path_impl_parenthesis that[OF \<open>v0 \<in> V0\<close>]
[PROOF STATE]
proof (prove)
using this:
v0 \<in> V0
(v0, v) \<in> (tree_edges s)\<^sup>+
v0 \<in> dom (finished s)
\<lbrakk>(?v, ?w) \<in> (tree_edges s)\<^sup>+; ?v \<in> dom (finished s)\<rbrakk> \<Longrightarrow> ?w \<in> dom (finished s) \<and> \<delta> s ?v < \<delta> s ?w \<and> \<phi> s ?w < \<phi> s ?v
\<delta> s v0 < \<delta> s v \<and> \<phi> s v < \<phi> s v0 \<Longrightarrow> thesis

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

goal:
No subgoals!
[PROOF STEP]
qed