[STATEMENT]
lemma i_cross_edges_finished: "is_invar (\<lambda>s. \<forall>(u,v)\<in>cross_edges s.
    v \<in> dom (finished s) \<and> (u \<in> dom (finished s) \<longrightarrow> \<phi> s v < \<phi> s u))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_invar (\<lambda>s. \<forall>(u, v)\<in>cross_edges s. v \<in> dom (finished s) \<and> (u \<in> dom (finished s) \<longrightarrow> \<phi> s v < \<phi> s u))
[PROOF STEP]
proof (induction rule: is_invarI_full)
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>e. \<forall>(u, v)\<in>cross_edges (empty_state e). v \<in> dom (finished (empty_state e)) \<and> (u \<in> dom (finished (empty_state e)) \<longrightarrow> \<phi> (empty_state e) v < \<phi> (empty_state e) u)
 2. \<And>s s' v0 e. \<lbrakk>\<forall>(u, v)\<in>cross_edges s. v \<in> dom (finished s) \<and> (u \<in> dom (finished s) \<longrightarrow> \<phi> s v < \<phi> s u); cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(u, v)\<in>cross_edges s'. v \<in> dom (finished s') \<and> (u \<in> dom (finished s') \<longrightarrow> \<phi> s' v < \<phi> s' u)
 3. \<And>s s' u e. \<lbrakk>\<forall>(u, v)\<in>cross_edges s. v \<in> dom (finished s) \<and> (u \<in> dom (finished s) \<longrightarrow> \<phi> s v < \<phi> s u); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; pending s `` {u} = {}; u = hd (stack s); s' = finish u s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(u, v)\<in>cross_edges s'. v \<in> dom (finished s') \<and> (u \<in> dom (finished s') \<longrightarrow> \<phi> s' v < \<phi> s' u)
 4. \<And>s s' u v e. \<lbrakk>\<forall>(u, v)\<in>cross_edges s. v \<in> dom (finished s) \<and> (u \<in> dom (finished s) \<longrightarrow> \<phi> s v < \<phi> s u); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); v \<in> dom (finished s); u = hd (stack s); s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(u, v)\<in>cross_edges s'. v \<in> dom (finished s') \<and> (u \<in> dom (finished s') \<longrightarrow> \<phi> s' v < \<phi> s' u)
 5. \<And>s s' u v e. \<lbrakk>\<forall>(u, v)\<in>cross_edges s. v \<in> dom (finished s) \<and> (u \<in> dom (finished s) \<longrightarrow> \<phi> s v < \<phi> s u); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); v \<notin> dom (finished s); u = hd (stack s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(u, v)\<in>cross_edges s'. v \<in> dom (finished s') \<and> (u \<in> dom (finished s') \<longrightarrow> \<phi> s' v < \<phi> s' u)
 6. \<And>s s' u v e. \<lbrakk>\<forall>(u, v)\<in>cross_edges s. v \<in> dom (finished s) \<and> (u \<in> dom (finished s) \<longrightarrow> \<phi> s v < \<phi> s u); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<notin> dom (discovered s); u = hd (stack s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(u, v)\<in>cross_edges s'. v \<in> dom (finished s') \<and> (u \<in> dom (finished s') \<longrightarrow> \<phi> s' v < \<phi> s' u)
[PROOF STEP]
case (finish s s' u e)
[PROOF STATE]
proof (state)
this:
\<forall>(u, v)\<in>cross_edges s. v \<in> dom (finished s) \<and> (u \<in> dom (finished s) \<longrightarrow> \<phi> s v < \<phi> s u)
cond s
DFS_invar G param s
DFS_invar G param s'
stack s \<noteq> []
pending s `` {u} = {}
u = hd (stack s)
s' = finish u s\<lparr>state.more := e\<rparr>

goal (6 subgoals):
 1. \<And>e. \<forall>(u, v)\<in>cross_edges (empty_state e). v \<in> dom (finished (empty_state e)) \<and> (u \<in> dom (finished (empty_state e)) \<longrightarrow> \<phi> (empty_state e) v < \<phi> (empty_state e) u)
 2. \<And>s s' v0 e. \<lbrakk>\<forall>(u, v)\<in>cross_edges s. v \<in> dom (finished s) \<and> (u \<in> dom (finished s) \<longrightarrow> \<phi> s v < \<phi> s u); cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(u, v)\<in>cross_edges s'. v \<in> dom (finished s') \<and> (u \<in> dom (finished s') \<longrightarrow> \<phi> s' v < \<phi> s' u)
 3. \<And>s s' u e. \<lbrakk>\<forall>(u, v)\<in>cross_edges s. v \<in> dom (finished s) \<and> (u \<in> dom (finished s) \<longrightarrow> \<phi> s v < \<phi> s u); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; pending s `` {u} = {}; u = hd (stack s); s' = finish u s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(u, v)\<in>cross_edges s'. v \<in> dom (finished s') \<and> (u \<in> dom (finished s') \<longrightarrow> \<phi> s' v < \<phi> s' u)
 4. \<And>s s' u v e. \<lbrakk>\<forall>(u, v)\<in>cross_edges s. v \<in> dom (finished s) \<and> (u \<in> dom (finished s) \<longrightarrow> \<phi> s v < \<phi> s u); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); v \<in> dom (finished s); u = hd (stack s); s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(u, v)\<in>cross_edges s'. v \<in> dom (finished s') \<and> (u \<in> dom (finished s') \<longrightarrow> \<phi> s' v < \<phi> s' u)
 5. \<And>s s' u v e. \<lbrakk>\<forall>(u, v)\<in>cross_edges s. v \<in> dom (finished s) \<and> (u \<in> dom (finished s) \<longrightarrow> \<phi> s v < \<phi> s u); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); v \<notin> dom (finished s); u = hd (stack s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(u, v)\<in>cross_edges s'. v \<in> dom (finished s') \<and> (u \<in> dom (finished s') \<longrightarrow> \<phi> s' v < \<phi> s' u)
 6. \<And>s s' u v e. \<lbrakk>\<forall>(u, v)\<in>cross_edges s. v \<in> dom (finished s) \<and> (u \<in> dom (finished s) \<longrightarrow> \<phi> s v < \<phi> s u); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<notin> dom (discovered s); u = hd (stack s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(u, v)\<in>cross_edges s'. v \<in> dom (finished s') \<and> (u \<in> dom (finished s') \<longrightarrow> \<phi> s' v < \<phi> s' u)
[PROOF STEP]
interpret DFS_invar G param s
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. DFS_invar G param s
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>e. \<forall>(u, v)\<in>cross_edges (empty_state e). v \<in> dom (finished (empty_state e)) \<and> (u \<in> dom (finished (empty_state e)) \<longrightarrow> \<phi> (empty_state e) v < \<phi> (empty_state e) u)
 2. \<And>s s' v0 e. \<lbrakk>\<forall>(u, v)\<in>cross_edges s. v \<in> dom (finished s) \<and> (u \<in> dom (finished s) \<longrightarrow> \<phi> s v < \<phi> s u); cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(u, v)\<in>cross_edges s'. v \<in> dom (finished s') \<and> (u \<in> dom (finished s') \<longrightarrow> \<phi> s' v < \<phi> s' u)
 3. \<And>s s' u e. \<lbrakk>\<forall>(u, v)\<in>cross_edges s. v \<in> dom (finished s) \<and> (u \<in> dom (finished s) \<longrightarrow> \<phi> s v < \<phi> s u); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; pending s `` {u} = {}; u = hd (stack s); s' = finish u s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(u, v)\<in>cross_edges s'. v \<in> dom (finished s') \<and> (u \<in> dom (finished s') \<longrightarrow> \<phi> s' v < \<phi> s' u)
 4. \<And>s s' u v e. \<lbrakk>\<forall>(u, v)\<in>cross_edges s. v \<in> dom (finished s) \<and> (u \<in> dom (finished s) \<longrightarrow> \<phi> s v < \<phi> s u); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); v \<in> dom (finished s); u = hd (stack s); s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(u, v)\<in>cross_edges s'. v \<in> dom (finished s') \<and> (u \<in> dom (finished s') \<longrightarrow> \<phi> s' v < \<phi> s' u)
 5. \<And>s s' u v e. \<lbrakk>\<forall>(u, v)\<in>cross_edges s. v \<in> dom (finished s) \<and> (u \<in> dom (finished s) \<longrightarrow> \<phi> s v < \<phi> s u); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); v \<notin> dom (finished s); u = hd (stack s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(u, v)\<in>cross_edges s'. v \<in> dom (finished s') \<and> (u \<in> dom (finished s') \<longrightarrow> \<phi> s' v < \<phi> s' u)
 6. \<And>s s' u v e. \<lbrakk>\<forall>(u, v)\<in>cross_edges s. v \<in> dom (finished s) \<and> (u \<in> dom (finished s) \<longrightarrow> \<phi> s v < \<phi> s u); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<notin> dom (discovered s); u = hd (stack s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(u, v)\<in>cross_edges s'. v \<in> dom (finished s') \<and> (u \<in> dom (finished s') \<longrightarrow> \<phi> s' v < \<phi> s' u)
[PROOF STEP]
from finish stack_not_finished
[PROOF STATE]
proof (chain)
picking this:
\<forall>(u, v)\<in>cross_edges s. v \<in> dom (finished s) \<and> (u \<in> dom (finished s) \<longrightarrow> \<phi> s v < \<phi> s u)
cond s
DFS_invar G param s
DFS_invar G param s'
stack s \<noteq> []
pending s `` {u} = {}
u = hd (stack s)
s' = finish u s\<lparr>state.more := e\<rparr>
?x \<in> set (stack s) \<Longrightarrow> ?x \<notin> dom (finished s)
[PROOF STEP]
have "u \<notin> dom (finished s)"
[PROOF STATE]
proof (prove)
using this:
\<forall>(u, v)\<in>cross_edges s. v \<in> dom (finished s) \<and> (u \<in> dom (finished s) \<longrightarrow> \<phi> s v < \<phi> s u)
cond s
DFS_invar G param s
DFS_invar G param s'
stack s \<noteq> []
pending s `` {u} = {}
u = hd (stack s)
s' = finish u s\<lparr>state.more := e\<rparr>
?x \<in> set (stack s) \<Longrightarrow> ?x \<notin> dom (finished s)

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

goal (6 subgoals):
 1. \<And>e. \<forall>(u, v)\<in>cross_edges (empty_state e). v \<in> dom (finished (empty_state e)) \<and> (u \<in> dom (finished (empty_state e)) \<longrightarrow> \<phi> (empty_state e) v < \<phi> (empty_state e) u)
 2. \<And>s s' v0 e. \<lbrakk>\<forall>(u, v)\<in>cross_edges s. v \<in> dom (finished s) \<and> (u \<in> dom (finished s) \<longrightarrow> \<phi> s v < \<phi> s u); cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(u, v)\<in>cross_edges s'. v \<in> dom (finished s') \<and> (u \<in> dom (finished s') \<longrightarrow> \<phi> s' v < \<phi> s' u)
 3. \<And>s s' u e. \<lbrakk>\<forall>(u, v)\<in>cross_edges s. v \<in> dom (finished s) \<and> (u \<in> dom (finished s) \<longrightarrow> \<phi> s v < \<phi> s u); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; pending s `` {u} = {}; u = hd (stack s); s' = finish u s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(u, v)\<in>cross_edges s'. v \<in> dom (finished s') \<and> (u \<in> dom (finished s') \<longrightarrow> \<phi> s' v < \<phi> s' u)
 4. \<And>s s' u v e. \<lbrakk>\<forall>(u, v)\<in>cross_edges s. v \<in> dom (finished s) \<and> (u \<in> dom (finished s) \<longrightarrow> \<phi> s v < \<phi> s u); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); v \<in> dom (finished s); u = hd (stack s); s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(u, v)\<in>cross_edges s'. v \<in> dom (finished s') \<and> (u \<in> dom (finished s') \<longrightarrow> \<phi> s' v < \<phi> s' u)
 5. \<And>s s' u v e. \<lbrakk>\<forall>(u, v)\<in>cross_edges s. v \<in> dom (finished s) \<and> (u \<in> dom (finished s) \<longrightarrow> \<phi> s v < \<phi> s u); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); v \<notin> dom (finished s); u = hd (stack s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(u, v)\<in>cross_edges s'. v \<in> dom (finished s') \<and> (u \<in> dom (finished s') \<longrightarrow> \<phi> s' v < \<phi> s' u)
 6. \<And>s s' u v e. \<lbrakk>\<forall>(u, v)\<in>cross_edges s. v \<in> dom (finished s) \<and> (u \<in> dom (finished s) \<longrightarrow> \<phi> s v < \<phi> s u); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<notin> dom (discovered s); u = hd (stack s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(u, v)\<in>cross_edges s'. v \<in> dom (finished s') \<and> (u \<in> dom (finished s') \<longrightarrow> \<phi> s' v < \<phi> s' u)
[PROOF STEP]
with finish
[PROOF STATE]
proof (chain)
picking this:
\<forall>(u, v)\<in>cross_edges s. v \<in> dom (finished s) \<and> (u \<in> dom (finished s) \<longrightarrow> \<phi> s v < \<phi> s u)
cond s
DFS_invar G param s
DFS_invar G param s'
stack s \<noteq> []
pending s `` {u} = {}
u = hd (stack s)
s' = finish u s\<lparr>state.more := e\<rparr>
u \<notin> dom (finished s)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>(u, v)\<in>cross_edges s. v \<in> dom (finished s) \<and> (u \<in> dom (finished s) \<longrightarrow> \<phi> s v < \<phi> s u)
cond s
DFS_invar G param s
DFS_invar G param s'
stack s \<noteq> []
pending s `` {u} = {}
u = hd (stack s)
s' = finish u s\<lparr>state.more := e\<rparr>
u \<notin> dom (finished s)

goal (1 subgoal):
 1. \<forall>(u, v)\<in>cross_edges s'. v \<in> dom (finished s') \<and> (u \<in> dom (finished s') \<longrightarrow> \<phi> s' v < \<phi> s' u)
[PROOF STEP]
by (auto intro: timing_less_counter)
[PROOF STATE]
proof (state)
this:
\<forall>(u, v)\<in>cross_edges s'. v \<in> dom (finished s') \<and> (u \<in> dom (finished s') \<longrightarrow> \<phi> s' v < \<phi> s' u)

goal (5 subgoals):
 1. \<And>e. \<forall>(u, v)\<in>cross_edges (empty_state e). v \<in> dom (finished (empty_state e)) \<and> (u \<in> dom (finished (empty_state e)) \<longrightarrow> \<phi> (empty_state e) v < \<phi> (empty_state e) u)
 2. \<And>s s' v0 e. \<lbrakk>\<forall>(u, v)\<in>cross_edges s. v \<in> dom (finished s) \<and> (u \<in> dom (finished s) \<longrightarrow> \<phi> s v < \<phi> s u); cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(u, v)\<in>cross_edges s'. v \<in> dom (finished s') \<and> (u \<in> dom (finished s') \<longrightarrow> \<phi> s' v < \<phi> s' u)
 3. \<And>s s' u v e. \<lbrakk>\<forall>(u, v)\<in>cross_edges s. v \<in> dom (finished s) \<and> (u \<in> dom (finished s) \<longrightarrow> \<phi> s v < \<phi> s u); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); v \<in> dom (finished s); u = hd (stack s); s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(u, v)\<in>cross_edges s'. v \<in> dom (finished s') \<and> (u \<in> dom (finished s') \<longrightarrow> \<phi> s' v < \<phi> s' u)
 4. \<And>s s' u v e. \<lbrakk>\<forall>(u, v)\<in>cross_edges s. v \<in> dom (finished s) \<and> (u \<in> dom (finished s) \<longrightarrow> \<phi> s v < \<phi> s u); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); v \<notin> dom (finished s); u = hd (stack s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(u, v)\<in>cross_edges s'. v \<in> dom (finished s') \<and> (u \<in> dom (finished s') \<longrightarrow> \<phi> s' v < \<phi> s' u)
 5. \<And>s s' u v e. \<lbrakk>\<forall>(u, v)\<in>cross_edges s. v \<in> dom (finished s) \<and> (u \<in> dom (finished s) \<longrightarrow> \<phi> s v < \<phi> s u); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<notin> dom (discovered s); u = hd (stack s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(u, v)\<in>cross_edges s'. v \<in> dom (finished s') \<and> (u \<in> dom (finished s') \<longrightarrow> \<phi> s' v < \<phi> s' u)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>e. \<forall>(u, v)\<in>cross_edges (empty_state e). v \<in> dom (finished (empty_state e)) \<and> (u \<in> dom (finished (empty_state e)) \<longrightarrow> \<phi> (empty_state e) v < \<phi> (empty_state e) u)
 2. \<And>s s' v0 e. \<lbrakk>\<forall>(u, v)\<in>cross_edges s. v \<in> dom (finished s) \<and> (u \<in> dom (finished s) \<longrightarrow> \<phi> s v < \<phi> s u); cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(u, v)\<in>cross_edges s'. v \<in> dom (finished s') \<and> (u \<in> dom (finished s') \<longrightarrow> \<phi> s' v < \<phi> s' u)
 3. \<And>s s' u v e. \<lbrakk>\<forall>(u, v)\<in>cross_edges s. v \<in> dom (finished s) \<and> (u \<in> dom (finished s) \<longrightarrow> \<phi> s v < \<phi> s u); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); v \<in> dom (finished s); u = hd (stack s); s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(u, v)\<in>cross_edges s'. v \<in> dom (finished s') \<and> (u \<in> dom (finished s') \<longrightarrow> \<phi> s' v < \<phi> s' u)
 4. \<And>s s' u v e. \<lbrakk>\<forall>(u, v)\<in>cross_edges s. v \<in> dom (finished s) \<and> (u \<in> dom (finished s) \<longrightarrow> \<phi> s v < \<phi> s u); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); v \<notin> dom (finished s); u = hd (stack s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(u, v)\<in>cross_edges s'. v \<in> dom (finished s') \<and> (u \<in> dom (finished s') \<longrightarrow> \<phi> s' v < \<phi> s' u)
 5. \<And>s s' u v e. \<lbrakk>\<forall>(u, v)\<in>cross_edges s. v \<in> dom (finished s) \<and> (u \<in> dom (finished s) \<longrightarrow> \<phi> s v < \<phi> s u); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<notin> dom (discovered s); u = hd (stack s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(u, v)\<in>cross_edges s'. v \<in> dom (finished s') \<and> (u \<in> dom (finished s') \<longrightarrow> \<phi> s' v < \<phi> s' u)
[PROOF STEP]
case (cross_edge s s' u v e)
[PROOF STATE]
proof (state)
this:
\<forall>(u, v)\<in>cross_edges s. v \<in> dom (finished s) \<and> (u \<in> dom (finished s) \<longrightarrow> \<phi> s v < \<phi> s u)
cond s
DFS_invar G param s
DFS_invar G param s'
stack s \<noteq> []
v \<in> pending s `` {u}
v \<in> dom (discovered s)
v \<in> dom (finished s)
u = hd (stack s)
s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>

goal (5 subgoals):
 1. \<And>e. \<forall>(u, v)\<in>cross_edges (empty_state e). v \<in> dom (finished (empty_state e)) \<and> (u \<in> dom (finished (empty_state e)) \<longrightarrow> \<phi> (empty_state e) v < \<phi> (empty_state e) u)
 2. \<And>s s' v0 e. \<lbrakk>\<forall>(u, v)\<in>cross_edges s. v \<in> dom (finished s) \<and> (u \<in> dom (finished s) \<longrightarrow> \<phi> s v < \<phi> s u); cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(u, v)\<in>cross_edges s'. v \<in> dom (finished s') \<and> (u \<in> dom (finished s') \<longrightarrow> \<phi> s' v < \<phi> s' u)
 3. \<And>s s' u v e. \<lbrakk>\<forall>(u, v)\<in>cross_edges s. v \<in> dom (finished s) \<and> (u \<in> dom (finished s) \<longrightarrow> \<phi> s v < \<phi> s u); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); v \<in> dom (finished s); u = hd (stack s); s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(u, v)\<in>cross_edges s'. v \<in> dom (finished s') \<and> (u \<in> dom (finished s') \<longrightarrow> \<phi> s' v < \<phi> s' u)
 4. \<And>s s' u v e. \<lbrakk>\<forall>(u, v)\<in>cross_edges s. v \<in> dom (finished s) \<and> (u \<in> dom (finished s) \<longrightarrow> \<phi> s v < \<phi> s u); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); v \<notin> dom (finished s); u = hd (stack s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(u, v)\<in>cross_edges s'. v \<in> dom (finished s') \<and> (u \<in> dom (finished s') \<longrightarrow> \<phi> s' v < \<phi> s' u)
 5. \<And>s s' u v e. \<lbrakk>\<forall>(u, v)\<in>cross_edges s. v \<in> dom (finished s) \<and> (u \<in> dom (finished s) \<longrightarrow> \<phi> s v < \<phi> s u); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<notin> dom (discovered s); u = hd (stack s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(u, v)\<in>cross_edges s'. v \<in> dom (finished s') \<and> (u \<in> dom (finished s') \<longrightarrow> \<phi> s' v < \<phi> s' u)
[PROOF STEP]
interpret DFS_invar G param s
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. DFS_invar G param s
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>e. \<forall>(u, v)\<in>cross_edges (empty_state e). v \<in> dom (finished (empty_state e)) \<and> (u \<in> dom (finished (empty_state e)) \<longrightarrow> \<phi> (empty_state e) v < \<phi> (empty_state e) u)
 2. \<And>s s' v0 e. \<lbrakk>\<forall>(u, v)\<in>cross_edges s. v \<in> dom (finished s) \<and> (u \<in> dom (finished s) \<longrightarrow> \<phi> s v < \<phi> s u); cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(u, v)\<in>cross_edges s'. v \<in> dom (finished s') \<and> (u \<in> dom (finished s') \<longrightarrow> \<phi> s' v < \<phi> s' u)
 3. \<And>s s' u v e. \<lbrakk>\<forall>(u, v)\<in>cross_edges s. v \<in> dom (finished s) \<and> (u \<in> dom (finished s) \<longrightarrow> \<phi> s v < \<phi> s u); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); v \<in> dom (finished s); u = hd (stack s); s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(u, v)\<in>cross_edges s'. v \<in> dom (finished s') \<and> (u \<in> dom (finished s') \<longrightarrow> \<phi> s' v < \<phi> s' u)
 4. \<And>s s' u v e. \<lbrakk>\<forall>(u, v)\<in>cross_edges s. v \<in> dom (finished s) \<and> (u \<in> dom (finished s) \<longrightarrow> \<phi> s v < \<phi> s u); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); v \<notin> dom (finished s); u = hd (stack s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(u, v)\<in>cross_edges s'. v \<in> dom (finished s') \<and> (u \<in> dom (finished s') \<longrightarrow> \<phi> s' v < \<phi> s' u)
 5. \<And>s s' u v e. \<lbrakk>\<forall>(u, v)\<in>cross_edges s. v \<in> dom (finished s) \<and> (u \<in> dom (finished s) \<longrightarrow> \<phi> s v < \<phi> s u); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<notin> dom (discovered s); u = hd (stack s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(u, v)\<in>cross_edges s'. v \<in> dom (finished s') \<and> (u \<in> dom (finished s') \<longrightarrow> \<phi> s' v < \<phi> s' u)
[PROOF STEP]
from cross_edge stack_not_finished
[PROOF STATE]
proof (chain)
picking this:
\<forall>(u, v)\<in>cross_edges s. v \<in> dom (finished s) \<and> (u \<in> dom (finished s) \<longrightarrow> \<phi> s v < \<phi> s u)
cond s
DFS_invar G param s
DFS_invar G param s'
stack s \<noteq> []
v \<in> pending s `` {u}
v \<in> dom (discovered s)
v \<in> dom (finished s)
u = hd (stack s)
s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>
?x \<in> set (stack s) \<Longrightarrow> ?x \<notin> dom (finished s)
[PROOF STEP]
have "u \<notin> dom (finished s)"
[PROOF STATE]
proof (prove)
using this:
\<forall>(u, v)\<in>cross_edges s. v \<in> dom (finished s) \<and> (u \<in> dom (finished s) \<longrightarrow> \<phi> s v < \<phi> s u)
cond s
DFS_invar G param s
DFS_invar G param s'
stack s \<noteq> []
v \<in> pending s `` {u}
v \<in> dom (discovered s)
v \<in> dom (finished s)
u = hd (stack s)
s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>
?x \<in> set (stack s) \<Longrightarrow> ?x \<notin> dom (finished s)

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

goal (5 subgoals):
 1. \<And>e. \<forall>(u, v)\<in>cross_edges (empty_state e). v \<in> dom (finished (empty_state e)) \<and> (u \<in> dom (finished (empty_state e)) \<longrightarrow> \<phi> (empty_state e) v < \<phi> (empty_state e) u)
 2. \<And>s s' v0 e. \<lbrakk>\<forall>(u, v)\<in>cross_edges s. v \<in> dom (finished s) \<and> (u \<in> dom (finished s) \<longrightarrow> \<phi> s v < \<phi> s u); cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(u, v)\<in>cross_edges s'. v \<in> dom (finished s') \<and> (u \<in> dom (finished s') \<longrightarrow> \<phi> s' v < \<phi> s' u)
 3. \<And>s s' u v e. \<lbrakk>\<forall>(u, v)\<in>cross_edges s. v \<in> dom (finished s) \<and> (u \<in> dom (finished s) \<longrightarrow> \<phi> s v < \<phi> s u); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); v \<in> dom (finished s); u = hd (stack s); s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(u, v)\<in>cross_edges s'. v \<in> dom (finished s') \<and> (u \<in> dom (finished s') \<longrightarrow> \<phi> s' v < \<phi> s' u)
 4. \<And>s s' u v e. \<lbrakk>\<forall>(u, v)\<in>cross_edges s. v \<in> dom (finished s) \<and> (u \<in> dom (finished s) \<longrightarrow> \<phi> s v < \<phi> s u); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); v \<notin> dom (finished s); u = hd (stack s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(u, v)\<in>cross_edges s'. v \<in> dom (finished s') \<and> (u \<in> dom (finished s') \<longrightarrow> \<phi> s' v < \<phi> s' u)
 5. \<And>s s' u v e. \<lbrakk>\<forall>(u, v)\<in>cross_edges s. v \<in> dom (finished s) \<and> (u \<in> dom (finished s) \<longrightarrow> \<phi> s v < \<phi> s u); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<notin> dom (discovered s); u = hd (stack s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(u, v)\<in>cross_edges s'. v \<in> dom (finished s') \<and> (u \<in> dom (finished s') \<longrightarrow> \<phi> s' v < \<phi> s' u)
[PROOF STEP]
with cross_edge
[PROOF STATE]
proof (chain)
picking this:
\<forall>(u, v)\<in>cross_edges s. v \<in> dom (finished s) \<and> (u \<in> dom (finished s) \<longrightarrow> \<phi> s v < \<phi> s u)
cond s
DFS_invar G param s
DFS_invar G param s'
stack s \<noteq> []
v \<in> pending s `` {u}
v \<in> dom (discovered s)
v \<in> dom (finished s)
u = hd (stack s)
s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>
u \<notin> dom (finished s)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>(u, v)\<in>cross_edges s. v \<in> dom (finished s) \<and> (u \<in> dom (finished s) \<longrightarrow> \<phi> s v < \<phi> s u)
cond s
DFS_invar G param s
DFS_invar G param s'
stack s \<noteq> []
v \<in> pending s `` {u}
v \<in> dom (discovered s)
v \<in> dom (finished s)
u = hd (stack s)
s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>
u \<notin> dom (finished s)

goal (1 subgoal):
 1. \<forall>(u, v)\<in>cross_edges s'. v \<in> dom (finished s') \<and> (u \<in> dom (finished s') \<longrightarrow> \<phi> s' v < \<phi> s' u)
[PROOF STEP]
by (auto intro: timing_less_counter)
[PROOF STATE]
proof (state)
this:
\<forall>(u, v)\<in>cross_edges s'. v \<in> dom (finished s') \<and> (u \<in> dom (finished s') \<longrightarrow> \<phi> s' v < \<phi> s' u)

goal (4 subgoals):
 1. \<And>e. \<forall>(u, v)\<in>cross_edges (empty_state e). v \<in> dom (finished (empty_state e)) \<and> (u \<in> dom (finished (empty_state e)) \<longrightarrow> \<phi> (empty_state e) v < \<phi> (empty_state e) u)
 2. \<And>s s' v0 e. \<lbrakk>\<forall>(u, v)\<in>cross_edges s. v \<in> dom (finished s) \<and> (u \<in> dom (finished s) \<longrightarrow> \<phi> s v < \<phi> s u); cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(u, v)\<in>cross_edges s'. v \<in> dom (finished s') \<and> (u \<in> dom (finished s') \<longrightarrow> \<phi> s' v < \<phi> s' u)
 3. \<And>s s' u v e. \<lbrakk>\<forall>(u, v)\<in>cross_edges s. v \<in> dom (finished s) \<and> (u \<in> dom (finished s) \<longrightarrow> \<phi> s v < \<phi> s u); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); v \<notin> dom (finished s); u = hd (stack s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(u, v)\<in>cross_edges s'. v \<in> dom (finished s') \<and> (u \<in> dom (finished s') \<longrightarrow> \<phi> s' v < \<phi> s' u)
 4. \<And>s s' u v e. \<lbrakk>\<forall>(u, v)\<in>cross_edges s. v \<in> dom (finished s) \<and> (u \<in> dom (finished s) \<longrightarrow> \<phi> s v < \<phi> s u); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<notin> dom (discovered s); u = hd (stack s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(u, v)\<in>cross_edges s'. v \<in> dom (finished s') \<and> (u \<in> dom (finished s') \<longrightarrow> \<phi> s' v < \<phi> s' u)
[PROOF STEP]
qed simp_all


[STATEMENT]
lemma cross_edges_target_finished:
    "(u,v)\<in>cross_edges s \<Longrightarrow> v \<in> dom (finished s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (u, v) \<in> cross_edges s \<Longrightarrow> v \<in> dom (finished s)
[PROOF STEP]
using cross_edges_finished
[PROOF STATE]
proof (prove)
using this:
\<forall>(u, v)\<in>cross_edges s. v \<in> dom (finished s) \<and> (u \<in> dom (finished s) \<longrightarrow> \<phi> s v < \<phi> s u)

goal (1 subgoal):
 1. (u, v) \<in> cross_edges s \<Longrightarrow> v \<in> dom (finished s)
[PROOF STEP]
by auto


[STATEMENT]
lemma cross_edges_finished_decr:
    "\<lbrakk>(u,v)\<in>cross_edges s; u\<in>dom (finished s)\<rbrakk> \<Longrightarrow> \<phi> s v < \<phi> s u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(u, v) \<in> cross_edges s; u \<in> dom (finished s)\<rbrakk> \<Longrightarrow> \<phi> s v < \<phi> s u
[PROOF STEP]
using cross_edges_finished
[PROOF STATE]
proof (prove)
using this:
\<forall>(u, v)\<in>cross_edges s. v \<in> dom (finished s) \<and> (u \<in> dom (finished s) \<longrightarrow> \<phi> s v < \<phi> s u)

goal (1 subgoal):
 1. \<lbrakk>(u, v) \<in> cross_edges s; u \<in> dom (finished s)\<rbrakk> \<Longrightarrow> \<phi> s v < \<phi> s u
[PROOF STEP]
by auto


[STATEMENT]
lemma cross_edge_unequal:
    assumes cross: "(v,w) \<in> cross_edges s"
    shows "v \<noteq> w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<noteq> w
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. v \<noteq> w
[PROOF STEP]
from cross_edges_target_finished[OF cross]
[PROOF STATE]
proof (chain)
picking this:
w \<in> dom (finished s)
[PROOF STEP]
have
      w_fin: "w \<in> dom (finished s)"
[PROOF STATE]
proof (prove)
using this:
w \<in> dom (finished s)

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

goal (1 subgoal):
 1. v \<noteq> w
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<noteq> w
[PROOF STEP]
proof (cases "v \<in> dom (finished s)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. v \<in> dom (finished s) \<Longrightarrow> v \<noteq> w
 2. v \<notin> dom (finished s) \<Longrightarrow> v \<noteq> w
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
v \<in> dom (finished s)

goal (2 subgoals):
 1. v \<in> dom (finished s) \<Longrightarrow> v \<noteq> w
 2. v \<notin> dom (finished s) \<Longrightarrow> v \<noteq> w
[PROOF STEP]
with cross_edges_finished_decr[OF cross]
[PROOF STATE]
proof (chain)
picking this:
v \<in> dom (finished s) \<Longrightarrow> \<phi> s w < \<phi> s v
v \<in> dom (finished s)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
v \<in> dom (finished s) \<Longrightarrow> \<phi> s w < \<phi> s v
v \<in> dom (finished s)

goal (1 subgoal):
 1. v \<noteq> w
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
v \<noteq> w

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

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

goal (1 subgoal):
 1. v \<noteq> w
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
v \<noteq> w

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma i_back_edge_impl_tree_path:
    "is_invar (\<lambda>s. \<forall>(v,w) \<in> back_edges s. (w,v) \<in> (tree_edges s)\<^sup>+ \<or> w = v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_invar (\<lambda>s. \<forall>(v, w)\<in>back_edges s. (w, v) \<in> (tree_edges s)\<^sup>+ \<or> w = v)
[PROOF STEP]
proof (induct rule: is_invarI_full)
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>e. \<forall>(v, w)\<in>back_edges (empty_state e). (w, v) \<in> (tree_edges (empty_state e))\<^sup>+ \<or> w = v
 2. \<And>s s' v0 e. \<lbrakk>\<forall>(v, w)\<in>back_edges s. (w, v) \<in> (tree_edges s)\<^sup>+ \<or> w = v; cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>back_edges s'. (w, v) \<in> (tree_edges s')\<^sup>+ \<or> w = v
 3. \<And>s s' u e. \<lbrakk>\<forall>(v, w)\<in>back_edges s. (w, v) \<in> (tree_edges s)\<^sup>+ \<or> w = v; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; pending s `` {u} = {}; u = hd (stack s); s' = finish u s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>back_edges s'. (w, v) \<in> (tree_edges s')\<^sup>+ \<or> w = v
 4. \<And>s s' u v e. \<lbrakk>\<forall>(v, w)\<in>back_edges s. (w, v) \<in> (tree_edges s)\<^sup>+ \<or> w = v; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); v \<in> dom (finished s); u = hd (stack s); s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>back_edges s'. (w, v) \<in> (tree_edges s')\<^sup>+ \<or> w = v
 5. \<And>s s' u v e. \<lbrakk>\<forall>(v, w)\<in>back_edges s. (w, v) \<in> (tree_edges s)\<^sup>+ \<or> w = v; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); v \<notin> dom (finished s); u = hd (stack s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>back_edges s'. (w, v) \<in> (tree_edges s')\<^sup>+ \<or> w = v
 6. \<And>s s' u v e. \<lbrakk>\<forall>(v, w)\<in>back_edges s. (w, v) \<in> (tree_edges s)\<^sup>+ \<or> w = v; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<notin> dom (discovered s); u = hd (stack s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>back_edges s'. (w, v) \<in> (tree_edges s')\<^sup>+ \<or> w = v
[PROOF STEP]
case (back_edge s s' u v)
[PROOF STATE]
proof (state)
this:
\<forall>(v, w)\<in>back_edges s. (w, v) \<in> (tree_edges s)\<^sup>+ \<or> w = v
cond s
DFS_invar G param s
DFS_invar G param s'
stack s \<noteq> []
v \<in> pending s `` {u}
v \<in> dom (discovered s)
v \<notin> dom (finished s)
u = hd (stack s)
s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e_\<rparr>

goal (6 subgoals):
 1. \<And>e. \<forall>(v, w)\<in>back_edges (empty_state e). (w, v) \<in> (tree_edges (empty_state e))\<^sup>+ \<or> w = v
 2. \<And>s s' v0 e. \<lbrakk>\<forall>(v, w)\<in>back_edges s. (w, v) \<in> (tree_edges s)\<^sup>+ \<or> w = v; cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>back_edges s'. (w, v) \<in> (tree_edges s')\<^sup>+ \<or> w = v
 3. \<And>s s' u e. \<lbrakk>\<forall>(v, w)\<in>back_edges s. (w, v) \<in> (tree_edges s)\<^sup>+ \<or> w = v; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; pending s `` {u} = {}; u = hd (stack s); s' = finish u s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>back_edges s'. (w, v) \<in> (tree_edges s')\<^sup>+ \<or> w = v
 4. \<And>s s' u v e. \<lbrakk>\<forall>(v, w)\<in>back_edges s. (w, v) \<in> (tree_edges s)\<^sup>+ \<or> w = v; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); v \<in> dom (finished s); u = hd (stack s); s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>back_edges s'. (w, v) \<in> (tree_edges s')\<^sup>+ \<or> w = v
 5. \<And>s s' u v e. \<lbrakk>\<forall>(v, w)\<in>back_edges s. (w, v) \<in> (tree_edges s)\<^sup>+ \<or> w = v; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); v \<notin> dom (finished s); u = hd (stack s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>back_edges s'. (w, v) \<in> (tree_edges s')\<^sup>+ \<or> w = v
 6. \<And>s s' u v e. \<lbrakk>\<forall>(v, w)\<in>back_edges s. (w, v) \<in> (tree_edges s)\<^sup>+ \<or> w = v; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<notin> dom (discovered s); u = hd (stack s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>back_edges s'. (w, v) \<in> (tree_edges s')\<^sup>+ \<or> w = v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>(v, w)\<in>back_edges s. (w, v) \<in> (tree_edges s)\<^sup>+ \<or> w = v
cond s
DFS_invar G param s
DFS_invar G param s'
stack s \<noteq> []
v \<in> pending s `` {u}
v \<in> dom (discovered s)
v \<notin> dom (finished s)
u = hd (stack s)
s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e_\<rparr>
[PROOF STEP]
interpret DFS_invar where s=s
[PROOF STATE]
proof (prove)
using this:
\<forall>(v, w)\<in>back_edges s. (w, v) \<in> (tree_edges s)\<^sup>+ \<or> w = v
cond s
DFS_invar G param s
DFS_invar G param s'
stack s \<noteq> []
v \<in> pending s `` {u}
v \<in> dom (discovered s)
v \<notin> dom (finished s)
u = hd (stack s)
s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e_\<rparr>

goal (1 subgoal):
 1. DFS_invar G param s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>e. \<forall>(v, w)\<in>back_edges (empty_state e). (w, v) \<in> (tree_edges (empty_state e))\<^sup>+ \<or> w = v
 2. \<And>s s' v0 e. \<lbrakk>\<forall>(v, w)\<in>back_edges s. (w, v) \<in> (tree_edges s)\<^sup>+ \<or> w = v; cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>back_edges s'. (w, v) \<in> (tree_edges s')\<^sup>+ \<or> w = v
 3. \<And>s s' u e. \<lbrakk>\<forall>(v, w)\<in>back_edges s. (w, v) \<in> (tree_edges s)\<^sup>+ \<or> w = v; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; pending s `` {u} = {}; u = hd (stack s); s' = finish u s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>back_edges s'. (w, v) \<in> (tree_edges s')\<^sup>+ \<or> w = v
 4. \<And>s s' u v e. \<lbrakk>\<forall>(v, w)\<in>back_edges s. (w, v) \<in> (tree_edges s)\<^sup>+ \<or> w = v; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); v \<in> dom (finished s); u = hd (stack s); s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>back_edges s'. (w, v) \<in> (tree_edges s')\<^sup>+ \<or> w = v
 5. \<And>s s' u v e. \<lbrakk>\<forall>(v, w)\<in>back_edges s. (w, v) \<in> (tree_edges s)\<^sup>+ \<or> w = v; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); v \<notin> dom (finished s); u = hd (stack s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>back_edges s'. (w, v) \<in> (tree_edges s')\<^sup>+ \<or> w = v
 6. \<And>s s' u v e. \<lbrakk>\<forall>(v, w)\<in>back_edges s. (w, v) \<in> (tree_edges s)\<^sup>+ \<or> w = v; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<notin> dom (discovered s); u = hd (stack s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>back_edges s'. (w, v) \<in> (tree_edges s')\<^sup>+ \<or> w = v
[PROOF STEP]
from back_edge
[PROOF STATE]
proof (chain)
picking this:
\<forall>(v, w)\<in>back_edges s. (w, v) \<in> (tree_edges s)\<^sup>+ \<or> w = v
cond s
DFS_invar G param s
DFS_invar G param s'
stack s \<noteq> []
v \<in> pending s `` {u}
v \<in> dom (discovered s)
v \<notin> dom (finished s)
u = hd (stack s)
s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e_\<rparr>
[PROOF STEP]
have st: "v \<in> set (stack s)" "u \<in> set (stack s)"
[PROOF STATE]
proof (prove)
using this:
\<forall>(v, w)\<in>back_edges s. (w, v) \<in> (tree_edges s)\<^sup>+ \<or> w = v
cond s
DFS_invar G param s
DFS_invar G param s'
stack s \<noteq> []
v \<in> pending s `` {u}
v \<in> dom (discovered s)
v \<notin> dom (finished s)
u = hd (stack s)
s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e_\<rparr>

goal (1 subgoal):
 1. v \<in> set (stack s) &&& u \<in> set (stack s)
[PROOF STEP]
using stack_set_def
[PROOF STATE]
proof (prove)
using this:
\<forall>(v, w)\<in>back_edges s. (w, v) \<in> (tree_edges s)\<^sup>+ \<or> w = v
cond s
DFS_invar G param s
DFS_invar G param s'
stack s \<noteq> []
v \<in> pending s `` {u}
v \<in> dom (discovered s)
v \<notin> dom (finished s)
u = hd (stack s)
s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e_\<rparr>
set (stack s) = dom (discovered s) - dom (finished s)

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

goal (6 subgoals):
 1. \<And>e. \<forall>(v, w)\<in>back_edges (empty_state e). (w, v) \<in> (tree_edges (empty_state e))\<^sup>+ \<or> w = v
 2. \<And>s s' v0 e. \<lbrakk>\<forall>(v, w)\<in>back_edges s. (w, v) \<in> (tree_edges s)\<^sup>+ \<or> w = v; cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>back_edges s'. (w, v) \<in> (tree_edges s')\<^sup>+ \<or> w = v
 3. \<And>s s' u e. \<lbrakk>\<forall>(v, w)\<in>back_edges s. (w, v) \<in> (tree_edges s)\<^sup>+ \<or> w = v; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; pending s `` {u} = {}; u = hd (stack s); s' = finish u s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>back_edges s'. (w, v) \<in> (tree_edges s')\<^sup>+ \<or> w = v
 4. \<And>s s' u v e. \<lbrakk>\<forall>(v, w)\<in>back_edges s. (w, v) \<in> (tree_edges s)\<^sup>+ \<or> w = v; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); v \<in> dom (finished s); u = hd (stack s); s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>back_edges s'. (w, v) \<in> (tree_edges s')\<^sup>+ \<or> w = v
 5. \<And>s s' u v e. \<lbrakk>\<forall>(v, w)\<in>back_edges s. (w, v) \<in> (tree_edges s)\<^sup>+ \<or> w = v; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); v \<notin> dom (finished s); u = hd (stack s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>back_edges s'. (w, v) \<in> (tree_edges s')\<^sup>+ \<or> w = v
 6. \<And>s s' u v e. \<lbrakk>\<forall>(v, w)\<in>back_edges s. (w, v) \<in> (tree_edges s)\<^sup>+ \<or> w = v; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<notin> dom (discovered s); u = hd (stack s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>back_edges s'. (w, v) \<in> (tree_edges s')\<^sup>+ \<or> w = v
[PROOF STEP]
have "(v,u) \<in> (tree_edges s)\<^sup>+ \<or> u = v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (v, u) \<in> (tree_edges s)\<^sup>+ \<or> u = v
[PROOF STEP]
proof (rule disjCI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. u \<noteq> v \<Longrightarrow> (v, u) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
assume "u \<noteq> v"
[PROOF STATE]
proof (state)
this:
u \<noteq> v

goal (1 subgoal):
 1. u \<noteq> v \<Longrightarrow> (v, u) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
with st back_edge
[PROOF STATE]
proof (chain)
picking this:
v \<in> set (stack s)
u \<in> set (stack s)
\<forall>(v, w)\<in>back_edges s. (w, v) \<in> (tree_edges s)\<^sup>+ \<or> w = v
cond s
DFS_invar G param s
DFS_invar G param s'
stack s \<noteq> []
v \<in> pending s `` {u}
v \<in> dom (discovered s)
v \<notin> dom (finished s)
u = hd (stack s)
s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e_\<rparr>
u \<noteq> v
[PROOF STEP]
have "v \<in> set (tl (stack s))"
[PROOF STATE]
proof (prove)
using this:
v \<in> set (stack s)
u \<in> set (stack s)
\<forall>(v, w)\<in>back_edges s. (w, v) \<in> (tree_edges s)\<^sup>+ \<or> w = v
cond s
DFS_invar G param s
DFS_invar G param s'
stack s \<noteq> []
v \<in> pending s `` {u}
v \<in> dom (discovered s)
v \<notin> dom (finished s)
u = hd (stack s)
s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e_\<rparr>
u \<noteq> v

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

goal (1 subgoal):
 1. u \<noteq> v \<Longrightarrow> (v, u) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
with tl_lt_stack_hd_discover st back_edge
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>stack s \<noteq> []; ?x \<in> set (tl (stack s))\<rbrakk> \<Longrightarrow> \<delta> s ?x < \<delta> s (hd (stack s))
v \<in> set (stack s)
u \<in> set (stack s)
\<forall>(v, w)\<in>back_edges s. (w, v) \<in> (tree_edges s)\<^sup>+ \<or> w = v
cond s
DFS_invar G param s
DFS_invar G param s'
stack s \<noteq> []
v \<in> pending s `` {u}
v \<in> dom (discovered s)
v \<notin> dom (finished s)
u = hd (stack s)
s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e_\<rparr>
v \<in> set (tl (stack s))
[PROOF STEP]
have "\<delta> s v < \<delta> s u"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>stack s \<noteq> []; ?x \<in> set (tl (stack s))\<rbrakk> \<Longrightarrow> \<delta> s ?x < \<delta> s (hd (stack s))
v \<in> set (stack s)
u \<in> set (stack s)
\<forall>(v, w)\<in>back_edges s. (w, v) \<in> (tree_edges s)\<^sup>+ \<or> w = v
cond s
DFS_invar G param s
DFS_invar G param s'
stack s \<noteq> []
v \<in> pending s `` {u}
v \<in> dom (discovered s)
v \<notin> dom (finished s)
u = hd (stack s)
s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e_\<rparr>
v \<in> set (tl (stack s))

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

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

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

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

goal (6 subgoals):
 1. \<And>e. \<forall>(v, w)\<in>back_edges (empty_state e). (w, v) \<in> (tree_edges (empty_state e))\<^sup>+ \<or> w = v
 2. \<And>s s' v0 e. \<lbrakk>\<forall>(v, w)\<in>back_edges s. (w, v) \<in> (tree_edges s)\<^sup>+ \<or> w = v; cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>back_edges s'. (w, v) \<in> (tree_edges s')\<^sup>+ \<or> w = v
 3. \<And>s s' u e. \<lbrakk>\<forall>(v, w)\<in>back_edges s. (w, v) \<in> (tree_edges s)\<^sup>+ \<or> w = v; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; pending s `` {u} = {}; u = hd (stack s); s' = finish u s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>back_edges s'. (w, v) \<in> (tree_edges s')\<^sup>+ \<or> w = v
 4. \<And>s s' u v e. \<lbrakk>\<forall>(v, w)\<in>back_edges s. (w, v) \<in> (tree_edges s)\<^sup>+ \<or> w = v; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); v \<in> dom (finished s); u = hd (stack s); s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>back_edges s'. (w, v) \<in> (tree_edges s')\<^sup>+ \<or> w = v
 5. \<And>s s' u v e. \<lbrakk>\<forall>(v, w)\<in>back_edges s. (w, v) \<in> (tree_edges s)\<^sup>+ \<or> w = v; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); v \<notin> dom (finished s); u = hd (stack s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>back_edges s'. (w, v) \<in> (tree_edges s')\<^sup>+ \<or> w = v
 6. \<And>s s' u v e. \<lbrakk>\<forall>(v, w)\<in>back_edges s. (w, v) \<in> (tree_edges s)\<^sup>+ \<or> w = v; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<notin> dom (discovered s); u = hd (stack s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>back_edges s'. (w, v) \<in> (tree_edges s')\<^sup>+ \<or> w = v
[PROOF STEP]
with back_edge
[PROOF STATE]
proof (chain)
picking this:
\<forall>(v, w)\<in>back_edges s. (w, v) \<in> (tree_edges s)\<^sup>+ \<or> w = v
cond s
DFS_invar G param s
DFS_invar G param s'
stack s \<noteq> []
v \<in> pending s `` {u}
v \<in> dom (discovered s)
v \<notin> dom (finished s)
u = hd (stack s)
s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e_\<rparr>
(v, u) \<in> (tree_edges s)\<^sup>+ \<or> u = v
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>(v, w)\<in>back_edges s. (w, v) \<in> (tree_edges s)\<^sup>+ \<or> w = v
cond s
DFS_invar G param s
DFS_invar G param s'
stack s \<noteq> []
v \<in> pending s `` {u}
v \<in> dom (discovered s)
v \<notin> dom (finished s)
u = hd (stack s)
s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e_\<rparr>
(v, u) \<in> (tree_edges s)\<^sup>+ \<or> u = v

goal (1 subgoal):
 1. \<forall>(v, w)\<in>back_edges s'. (w, v) \<in> (tree_edges s')\<^sup>+ \<or> w = v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>(v, w)\<in>back_edges s'. (w, v) \<in> (tree_edges s')\<^sup>+ \<or> w = v

goal (5 subgoals):
 1. \<And>e. \<forall>(v, w)\<in>back_edges (empty_state e). (w, v) \<in> (tree_edges (empty_state e))\<^sup>+ \<or> w = v
 2. \<And>s s' v0 e. \<lbrakk>\<forall>(v, w)\<in>back_edges s. (w, v) \<in> (tree_edges s)\<^sup>+ \<or> w = v; cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>back_edges s'. (w, v) \<in> (tree_edges s')\<^sup>+ \<or> w = v
 3. \<And>s s' u e. \<lbrakk>\<forall>(v, w)\<in>back_edges s. (w, v) \<in> (tree_edges s)\<^sup>+ \<or> w = v; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; pending s `` {u} = {}; u = hd (stack s); s' = finish u s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>back_edges s'. (w, v) \<in> (tree_edges s')\<^sup>+ \<or> w = v
 4. \<And>s s' u v e. \<lbrakk>\<forall>(v, w)\<in>back_edges s. (w, v) \<in> (tree_edges s)\<^sup>+ \<or> w = v; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); v \<in> dom (finished s); u = hd (stack s); s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>back_edges s'. (w, v) \<in> (tree_edges s')\<^sup>+ \<or> w = v
 5. \<And>s s' u v e. \<lbrakk>\<forall>(v, w)\<in>back_edges s. (w, v) \<in> (tree_edges s)\<^sup>+ \<or> w = v; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<notin> dom (discovered s); u = hd (stack s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>back_edges s'. (w, v) \<in> (tree_edges s')\<^sup>+ \<or> w = v
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>e. \<forall>(v, w)\<in>back_edges (empty_state e). (w, v) \<in> (tree_edges (empty_state e))\<^sup>+ \<or> w = v
 2. \<And>s s' v0 e. \<lbrakk>\<forall>(v, w)\<in>back_edges s. (w, v) \<in> (tree_edges s)\<^sup>+ \<or> w = v; cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>back_edges s'. (w, v) \<in> (tree_edges s')\<^sup>+ \<or> w = v
 3. \<And>s s' u e. \<lbrakk>\<forall>(v, w)\<in>back_edges s. (w, v) \<in> (tree_edges s)\<^sup>+ \<or> w = v; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; pending s `` {u} = {}; u = hd (stack s); s' = finish u s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>back_edges s'. (w, v) \<in> (tree_edges s')\<^sup>+ \<or> w = v
 4. \<And>s s' u v e. \<lbrakk>\<forall>(v, w)\<in>back_edges s. (w, v) \<in> (tree_edges s)\<^sup>+ \<or> w = v; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); v \<in> dom (finished s); u = hd (stack s); s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>back_edges s'. (w, v) \<in> (tree_edges s')\<^sup>+ \<or> w = v
 5. \<And>s s' u v e. \<lbrakk>\<forall>(v, w)\<in>back_edges s. (w, v) \<in> (tree_edges s)\<^sup>+ \<or> w = v; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<notin> dom (discovered s); u = hd (stack s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>back_edges s'. (w, v) \<in> (tree_edges s')\<^sup>+ \<or> w = v
[PROOF STEP]
case discover
[PROOF STATE]
proof (state)
this:
\<forall>(v, w)\<in>back_edges s_. (w, v) \<in> (tree_edges s_)\<^sup>+ \<or> w = v
cond s_
DFS_invar G param s_
DFS_invar G param s'_
stack s_ \<noteq> []
v_ \<in> pending s_ `` {u_}
v_ \<notin> dom (discovered s_)
u_ = hd (stack s_)
s'_ = discover u_ v_ (s_\<lparr>pending := pending s_ - {(u_, v_)}\<rparr>)\<lparr>state.more := e_\<rparr>

goal (5 subgoals):
 1. \<And>e. \<forall>(v, w)\<in>back_edges (empty_state e). (w, v) \<in> (tree_edges (empty_state e))\<^sup>+ \<or> w = v
 2. \<And>s s' v0 e. \<lbrakk>\<forall>(v, w)\<in>back_edges s. (w, v) \<in> (tree_edges s)\<^sup>+ \<or> w = v; cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>back_edges s'. (w, v) \<in> (tree_edges s')\<^sup>+ \<or> w = v
 3. \<And>s s' u e. \<lbrakk>\<forall>(v, w)\<in>back_edges s. (w, v) \<in> (tree_edges s)\<^sup>+ \<or> w = v; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; pending s `` {u} = {}; u = hd (stack s); s' = finish u s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>back_edges s'. (w, v) \<in> (tree_edges s')\<^sup>+ \<or> w = v
 4. \<And>s s' u v e. \<lbrakk>\<forall>(v, w)\<in>back_edges s. (w, v) \<in> (tree_edges s)\<^sup>+ \<or> w = v; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); v \<in> dom (finished s); u = hd (stack s); s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>back_edges s'. (w, v) \<in> (tree_edges s')\<^sup>+ \<or> w = v
 5. \<And>s s' u v e. \<lbrakk>\<forall>(v, w)\<in>back_edges s. (w, v) \<in> (tree_edges s)\<^sup>+ \<or> w = v; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<notin> dom (discovered s); u = hd (stack s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>back_edges s'. (w, v) \<in> (tree_edges s')\<^sup>+ \<or> w = v
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>(v, w)\<in>back_edges s_. (w, v) \<in> (tree_edges s_)\<^sup>+ \<or> w = v
cond s_
DFS_invar G param s_
DFS_invar G param s'_
stack s_ \<noteq> []
v_ \<in> pending s_ `` {u_}
v_ \<notin> dom (discovered s_)
u_ = hd (stack s_)
s'_ = discover u_ v_ (s_\<lparr>pending := pending s_ - {(u_, v_)}\<rparr>)\<lparr>state.more := e_\<rparr>

goal (1 subgoal):
 1. \<forall>(v, w)\<in>back_edges s'_. (w, v) \<in> (tree_edges s'_)\<^sup>+ \<or> w = v
[PROOF STEP]
using trancl_sub_insert_trancl
[PROOF STATE]
proof (prove)
using this:
\<forall>(v, w)\<in>back_edges s_. (w, v) \<in> (tree_edges s_)\<^sup>+ \<or> w = v
cond s_
DFS_invar G param s_
DFS_invar G param s'_
stack s_ \<noteq> []
v_ \<in> pending s_ `` {u_}
v_ \<notin> dom (discovered s_)
u_ = hd (stack s_)
s'_ = discover u_ v_ (s_\<lparr>pending := pending s_ - {(u_, v_)}\<rparr>)\<lparr>state.more := e_\<rparr>
?R\<^sup>+ \<subseteq> (insert ?x ?R)\<^sup>+

goal (1 subgoal):
 1. \<forall>(v, w)\<in>back_edges s'_. (w, v) \<in> (tree_edges s'_)\<^sup>+ \<or> w = v
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<forall>(v, w)\<in>back_edges s'_. (w, v) \<in> (tree_edges s'_)\<^sup>+ \<or> w = v

goal (4 subgoals):
 1. \<And>e. \<forall>(v, w)\<in>back_edges (empty_state e). (w, v) \<in> (tree_edges (empty_state e))\<^sup>+ \<or> w = v
 2. \<And>s s' v0 e. \<lbrakk>\<forall>(v, w)\<in>back_edges s. (w, v) \<in> (tree_edges s)\<^sup>+ \<or> w = v; cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>back_edges s'. (w, v) \<in> (tree_edges s')\<^sup>+ \<or> w = v
 3. \<And>s s' u e. \<lbrakk>\<forall>(v, w)\<in>back_edges s. (w, v) \<in> (tree_edges s)\<^sup>+ \<or> w = v; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; pending s `` {u} = {}; u = hd (stack s); s' = finish u s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>back_edges s'. (w, v) \<in> (tree_edges s')\<^sup>+ \<or> w = v
 4. \<And>s s' u v e. \<lbrakk>\<forall>(v, w)\<in>back_edges s. (w, v) \<in> (tree_edges s)\<^sup>+ \<or> w = v; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); v \<in> dom (finished s); u = hd (stack s); s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>back_edges s'. (w, v) \<in> (tree_edges s')\<^sup>+ \<or> w = v
[PROOF STEP]
qed simp_all


[STATEMENT]
lemma back_edge_impl_tree_path:
    "\<lbrakk>(v,w) \<in> back_edges s; v \<noteq> w\<rbrakk> \<Longrightarrow> (w,v) \<in> (tree_edges s)\<^sup>+"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(v, w) \<in> back_edges s; v \<noteq> w\<rbrakk> \<Longrightarrow> (w, v) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
using i_back_edge_impl_tree_path[THEN make_invar_thm]
[PROOF STATE]
proof (prove)
using this:
\<forall>(v, w)\<in>back_edges s. (w, v) \<in> (tree_edges s)\<^sup>+ \<or> w = v

goal (1 subgoal):
 1. \<lbrakk>(v, w) \<in> back_edges s; v \<noteq> w\<rbrakk> \<Longrightarrow> (w, v) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
by blast


[STATEMENT]
lemma back_edge_disc:
    assumes "(v,w) \<in> back_edges s"
    shows "\<delta> s w \<le> \<delta> s v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<delta> s w \<le> \<delta> s v
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> \<delta> s w \<le> \<delta> s v
 2. \<not> ?P \<Longrightarrow> \<delta> s w \<le> \<delta> s v
[PROOF STEP]
assume "v\<noteq>w"
[PROOF STATE]
proof (state)
this:
v \<noteq> w

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<delta> s w \<le> \<delta> s v
 2. \<not> ?P \<Longrightarrow> \<delta> s w \<le> \<delta> s v
[PROOF STEP]
with assms back_edge_impl_tree_path
[PROOF STATE]
proof (chain)
picking this:
(v, w) \<in> back_edges s
\<lbrakk>(?v, ?w) \<in> back_edges s; ?v \<noteq> ?w\<rbrakk> \<Longrightarrow> (?w, ?v) \<in> (tree_edges s)\<^sup>+
v \<noteq> w
[PROOF STEP]
have "(w,v) \<in> (tree_edges s)\<^sup>+"
[PROOF STATE]
proof (prove)
using this:
(v, w) \<in> back_edges s
\<lbrakk>(?v, ?w) \<in> back_edges s; ?v \<noteq> ?w\<rbrakk> \<Longrightarrow> (?w, ?v) \<in> (tree_edges s)\<^sup>+
v \<noteq> w

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

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<delta> s w \<le> \<delta> s v
 2. \<not> ?P \<Longrightarrow> \<delta> s w \<le> \<delta> s v
[PROOF STEP]
with tree_path_disc
[PROOF STATE]
proof (chain)
picking this:
(?v, ?w) \<in> (tree_edges s)\<^sup>+ \<Longrightarrow> \<delta> s ?v < \<delta> s ?w
(w, v) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(?v, ?w) \<in> (tree_edges s)\<^sup>+ \<Longrightarrow> \<delta> s ?v < \<delta> s ?w
(w, v) \<in> (tree_edges s)\<^sup>+

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

goal (1 subgoal):
 1. \<not> v \<noteq> w \<Longrightarrow> \<delta> s w \<le> \<delta> s v
[PROOF STEP]
qed simp


[STATEMENT]
lemma back_edges_tree_disjoint:
    "back_edges s \<inter> tree_edges s = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. back_edges s \<inter> tree_edges s = {}
[PROOF STEP]
using back_edge_disc tree_edge_disc
[PROOF STATE]
proof (prove)
using this:
(?v, ?w) \<in> back_edges s \<Longrightarrow> \<delta> s ?w \<le> \<delta> s ?v
(?v, ?w) \<in> tree_edges s \<Longrightarrow> \<delta> s ?v < \<delta> s ?w

goal (1 subgoal):
 1. back_edges s \<inter> tree_edges s = {}
[PROOF STEP]
by force


[STATEMENT]
lemma back_edges_tree_pathes_disjoint:
    "back_edges s \<inter> (tree_edges s)\<^sup>+ = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. back_edges s \<inter> (tree_edges s)\<^sup>+ = {}
[PROOF STEP]
using back_edge_disc tree_path_disc
[PROOF STATE]
proof (prove)
using this:
(?v, ?w) \<in> back_edges s \<Longrightarrow> \<delta> s ?w \<le> \<delta> s ?v
(?v, ?w) \<in> (tree_edges s)\<^sup>+ \<Longrightarrow> \<delta> s ?v < \<delta> s ?w

goal (1 subgoal):
 1. back_edges s \<inter> (tree_edges s)\<^sup>+ = {}
[PROOF STEP]
by force


[STATEMENT]
lemma back_edge_finished:
    assumes "(v,w) \<in> back_edges s"
    and "w \<in> dom (finished s)"
    shows "v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w
[PROOF STEP]
proof (cases "v=w")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. v = w \<Longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w
 2. v \<noteq> w \<Longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
v = w

goal (2 subgoals):
 1. v = w \<Longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w
 2. v \<noteq> w \<Longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
(v, w) \<in> back_edges s
w \<in> dom (finished s)
v = w
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(v, w) \<in> back_edges s
w \<in> dom (finished s)
v = w

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

goal (1 subgoal):
 1. v \<noteq> w \<Longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. v \<noteq> w \<Longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
v \<noteq> w

goal (1 subgoal):
 1. v \<noteq> w \<Longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w
[PROOF STEP]
with back_edge_impl_tree_path assms
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>(?v, ?w) \<in> back_edges s; ?v \<noteq> ?w\<rbrakk> \<Longrightarrow> (?w, ?v) \<in> (tree_edges s)\<^sup>+
(v, w) \<in> back_edges s
w \<in> dom (finished s)
v \<noteq> w
[PROOF STEP]
have "(w,v) \<in> (tree_edges s)\<^sup>+"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?v, ?w) \<in> back_edges s; ?v \<noteq> ?w\<rbrakk> \<Longrightarrow> (?w, ?v) \<in> (tree_edges s)\<^sup>+
(v, w) \<in> back_edges s
w \<in> dom (finished s)
v \<noteq> w

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

goal (1 subgoal):
 1. v \<noteq> w \<Longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w
[PROOF STEP]
with tree_path_impl_parenthesis assms
[PROOF STATE]
proof (chain)
picking this:
\<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
(v, w) \<in> back_edges s
w \<in> dom (finished s)
(w, v) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<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
(v, w) \<in> back_edges s
w \<in> dom (finished s)
(w, v) \<in> (tree_edges s)\<^sup>+

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

goal:
No subgoals!
[PROOF STEP]
qed