[STATEMENT]
lemma paren_imp_tree_reach:
    "is_invar paren_imp_tree_reach"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_invar paren_imp_tree_reach
[PROOF STEP]
unfolding paren_imp_tree_reach_def[abs_def]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_invar (\<lambda>s. \<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+)
[PROOF STEP]
proof (induct rule: is_invarI)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>e. \<forall>v\<in>dom (discovered (empty_state e)). \<forall>w\<in>dom (finished (empty_state e)). \<delta> (empty_state e) v < \<delta> (empty_state e) w \<and> (v \<notin> dom (finished (empty_state e)) \<or> \<phi> (empty_state e) w < \<phi> (empty_state e) v) \<longrightarrow> (v, w) \<in> (tree_edges (empty_state e))\<^sup>+
 2. \<And>s s' v0 e. \<lbrakk>\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+; 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\<in>dom (discovered s'). \<forall>w\<in>dom (finished s'). \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v) \<longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+
 3. \<And>s s' u e. \<lbrakk>\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+; 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\<in>dom (discovered s'). \<forall>w\<in>dom (finished s'). \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v) \<longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+
 4. \<And>s s' u v e c b. \<lbrakk>\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+; 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); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (discovered s'). \<forall>w\<in>dom (finished s'). \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v) \<longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+
 5. \<And>s s' u v e. \<lbrakk>\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+; 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\<in>dom (discovered s'). \<forall>w\<in>dom (finished s'). \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v) \<longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+
[PROOF STEP]
case (discover s s' u v)
[PROOF STATE]
proof (state)
this:
\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+
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\<in>dom (discovered (empty_state e)). \<forall>w\<in>dom (finished (empty_state e)). \<delta> (empty_state e) v < \<delta> (empty_state e) w \<and> (v \<notin> dom (finished (empty_state e)) \<or> \<phi> (empty_state e) w < \<phi> (empty_state e) v) \<longrightarrow> (v, w) \<in> (tree_edges (empty_state e))\<^sup>+
 2. \<And>s s' v0 e. \<lbrakk>\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+; 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\<in>dom (discovered s'). \<forall>w\<in>dom (finished s'). \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v) \<longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+
 3. \<And>s s' u e. \<lbrakk>\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+; 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\<in>dom (discovered s'). \<forall>w\<in>dom (finished s'). \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v) \<longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+
 4. \<And>s s' u v e c b. \<lbrakk>\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+; 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); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (discovered s'). \<forall>w\<in>dom (finished s'). \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v) \<longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+
 5. \<And>s s' u v e. \<lbrakk>\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+; 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\<in>dom (discovered s'). \<forall>w\<in>dom (finished s'). \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v) \<longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+
[PROOF STEP]
hence EQ[simp]: "tree_edges s' = insert (hd (stack s), v) (tree_edges s)"
                    "finished s' = finished s"
                    "discovered s' = (discovered s)(v \<mapsto> counter s)"
[PROOF STATE]
proof (prove)
using this:
\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+
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. tree_edges s' = insert (hd (stack s), v) (tree_edges s) &&& finished s' = finished s &&& discovered s' = discovered s(v \<mapsto> counter s)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
tree_edges s' = insert (hd (stack s), v) (tree_edges s)
finished s' = finished s
discovered s' = discovered s(v \<mapsto> counter s)

goal (5 subgoals):
 1. \<And>e. \<forall>v\<in>dom (discovered (empty_state e)). \<forall>w\<in>dom (finished (empty_state e)). \<delta> (empty_state e) v < \<delta> (empty_state e) w \<and> (v \<notin> dom (finished (empty_state e)) \<or> \<phi> (empty_state e) w < \<phi> (empty_state e) v) \<longrightarrow> (v, w) \<in> (tree_edges (empty_state e))\<^sup>+
 2. \<And>s s' v0 e. \<lbrakk>\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+; 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\<in>dom (discovered s'). \<forall>w\<in>dom (finished s'). \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v) \<longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+
 3. \<And>s s' u e. \<lbrakk>\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+; 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\<in>dom (discovered s'). \<forall>w\<in>dom (finished s'). \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v) \<longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+
 4. \<And>s s' u v e c b. \<lbrakk>\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+; 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); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (discovered s'). \<forall>w\<in>dom (finished s'). \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v) \<longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+
 5. \<And>s s' u v e. \<lbrakk>\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+; 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\<in>dom (discovered s'). \<forall>w\<in>dom (finished s'). \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v) \<longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+
[PROOF STEP]
from discover
[PROOF STATE]
proof (chain)
picking this:
\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+
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>
[PROOF STEP]
interpret DFS_invar where s=s
[PROOF STATE]
proof (prove)
using this:
\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+
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. DFS_invar G param s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>e. \<forall>v\<in>dom (discovered (empty_state e)). \<forall>w\<in>dom (finished (empty_state e)). \<delta> (empty_state e) v < \<delta> (empty_state e) w \<and> (v \<notin> dom (finished (empty_state e)) \<or> \<phi> (empty_state e) w < \<phi> (empty_state e) v) \<longrightarrow> (v, w) \<in> (tree_edges (empty_state e))\<^sup>+
 2. \<And>s s' v0 e. \<lbrakk>\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+; 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\<in>dom (discovered s'). \<forall>w\<in>dom (finished s'). \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v) \<longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+
 3. \<And>s s' u e. \<lbrakk>\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+; 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\<in>dom (discovered s'). \<forall>w\<in>dom (finished s'). \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v) \<longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+
 4. \<And>s s' u v e c b. \<lbrakk>\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+; 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); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (discovered s'). \<forall>w\<in>dom (finished s'). \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v) \<longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+
 5. \<And>s s' u v e. \<lbrakk>\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+; 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\<in>dom (discovered s'). \<forall>w\<in>dom (finished s'). \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v) \<longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+
[PROOF STEP]
from discover
[PROOF STATE]
proof (chain)
picking this:
\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+
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>
[PROOF STEP]
have NE[simp]: "stack s \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+
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. stack s \<noteq> []
[PROOF STEP]
by (simp add: cond_alt)
[PROOF STATE]
proof (state)
this:
stack s \<noteq> []

goal (5 subgoals):
 1. \<And>e. \<forall>v\<in>dom (discovered (empty_state e)). \<forall>w\<in>dom (finished (empty_state e)). \<delta> (empty_state e) v < \<delta> (empty_state e) w \<and> (v \<notin> dom (finished (empty_state e)) \<or> \<phi> (empty_state e) w < \<phi> (empty_state e) v) \<longrightarrow> (v, w) \<in> (tree_edges (empty_state e))\<^sup>+
 2. \<And>s s' v0 e. \<lbrakk>\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+; 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\<in>dom (discovered s'). \<forall>w\<in>dom (finished s'). \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v) \<longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+
 3. \<And>s s' u e. \<lbrakk>\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+; 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\<in>dom (discovered s'). \<forall>w\<in>dom (finished s'). \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v) \<longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+
 4. \<And>s s' u v e c b. \<lbrakk>\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+; 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); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (discovered s'). \<forall>w\<in>dom (finished s'). \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v) \<longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+
 5. \<And>s s' u v e. \<lbrakk>\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+; 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\<in>dom (discovered s'). \<forall>w\<in>dom (finished s'). \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v) \<longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>v\<in>dom (discovered s'). \<forall>w\<in>dom (finished s'). \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v) \<longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+
[PROOF STEP]
proof (intro ballI impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>v w. \<lbrakk>v \<in> dom (discovered s'); w \<in> dom (finished s'); \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v)\<rbrakk> \<Longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+
[PROOF STEP]
fix a b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>v w. \<lbrakk>v \<in> dom (discovered s'); w \<in> dom (finished s'); \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v)\<rbrakk> \<Longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+
[PROOF STEP]
assume F:"a \<in> dom (discovered s')" "b \<in> dom (finished s')"
        and D: "\<delta> s' a < \<delta> s' b \<and> (a \<notin> dom (finished s') \<or> \<phi> s' a > \<phi> s' b)"
[PROOF STATE]
proof (state)
this:
a \<in> dom (discovered s')
b \<in> dom (finished s')
\<delta> s' a < \<delta> s' b \<and> (a \<notin> dom (finished s') \<or> \<phi> s' b < \<phi> s' a)

goal (1 subgoal):
 1. \<And>v w. \<lbrakk>v \<in> dom (discovered s'); w \<in> dom (finished s'); \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v)\<rbrakk> \<Longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+
[PROOF STEP]
from F finished_discovered discover
[PROOF STATE]
proof (chain)
picking this:
a \<in> dom (discovered s')
b \<in> dom (finished s')
dom (finished s) \<subseteq> dom (discovered s)
\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+
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>
[PROOF STEP]
have "b \<noteq> v"
[PROOF STATE]
proof (prove)
using this:
a \<in> dom (discovered s')
b \<in> dom (finished s')
dom (finished s) \<subseteq> dom (discovered s)
\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+
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. b \<noteq> v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
b \<noteq> v

goal (1 subgoal):
 1. \<And>v w. \<lbrakk>v \<in> dom (discovered s'); w \<in> dom (finished s'); \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v)\<rbrakk> \<Longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+
[PROOF STEP]
show "(a,b) \<in> (tree_edges s')\<^sup>+"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a, b) \<in> (tree_edges s')\<^sup>+
[PROOF STEP]
proof (cases "a = v")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a = v \<Longrightarrow> (a, b) \<in> (tree_edges s')\<^sup>+
 2. a \<noteq> v \<Longrightarrow> (a, b) \<in> (tree_edges s')\<^sup>+
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
a = v

goal (2 subgoals):
 1. a = v \<Longrightarrow> (a, b) \<in> (tree_edges s')\<^sup>+
 2. a \<noteq> v \<Longrightarrow> (a, b) \<in> (tree_edges s')\<^sup>+
[PROOF STEP]
with D \<open>b\<noteq>v\<close>
[PROOF STATE]
proof (chain)
picking this:
\<delta> s' a < \<delta> s' b \<and> (a \<notin> dom (finished s') \<or> \<phi> s' b < \<phi> s' a)
b \<noteq> v
a = v
[PROOF STEP]
have "counter s < \<delta> s b"
[PROOF STATE]
proof (prove)
using this:
\<delta> s' a < \<delta> s' b \<and> (a \<notin> dom (finished s') \<or> \<phi> s' b < \<phi> s' a)
b \<noteq> v
a = v

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

goal (2 subgoals):
 1. a = v \<Longrightarrow> (a, b) \<in> (tree_edges s')\<^sup>+
 2. a \<noteq> v \<Longrightarrow> (a, b) \<in> (tree_edges s')\<^sup>+
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
counter s < \<delta> s b

goal (2 subgoals):
 1. a = v \<Longrightarrow> (a, b) \<in> (tree_edges s')\<^sup>+
 2. a \<noteq> v \<Longrightarrow> (a, b) \<in> (tree_edges s')\<^sup>+
[PROOF STEP]
from F
[PROOF STATE]
proof (chain)
picking this:
a \<in> dom (discovered s')
b \<in> dom (finished s')
[PROOF STEP]
have "b \<in> dom (discovered s)"
[PROOF STATE]
proof (prove)
using this:
a \<in> dom (discovered s')
b \<in> dom (finished s')

goal (1 subgoal):
 1. b \<in> dom (discovered s)
[PROOF STEP]
using finished_discovered
[PROOF STATE]
proof (prove)
using this:
a \<in> dom (discovered s')
b \<in> dom (finished s')
dom (finished s) \<subseteq> dom (discovered s)

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

goal (2 subgoals):
 1. a = v \<Longrightarrow> (a, b) \<in> (tree_edges s')\<^sup>+
 2. a \<noteq> v \<Longrightarrow> (a, b) \<in> (tree_edges s')\<^sup>+
[PROOF STEP]
with timing_less_counter
[PROOF STATE]
proof (chain)
picking this:
?v \<in> dom (discovered s) \<Longrightarrow> \<delta> s ?v < counter s
?v \<in> dom (finished s) \<Longrightarrow> \<phi> s ?v < counter s
b \<in> dom (discovered s)
[PROOF STEP]
have "\<delta> s b < counter s"
[PROOF STATE]
proof (prove)
using this:
?v \<in> dom (discovered s) \<Longrightarrow> \<delta> s ?v < counter s
?v \<in> dom (finished s) \<Longrightarrow> \<phi> s ?v < counter s
b \<in> dom (discovered s)

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

goal (2 subgoals):
 1. a = v \<Longrightarrow> (a, b) \<in> (tree_edges s')\<^sup>+
 2. a \<noteq> v \<Longrightarrow> (a, b) \<in> (tree_edges s')\<^sup>+
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
?P
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
?P

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

goal (2 subgoals):
 1. a = v \<Longrightarrow> (a, b) \<in> (tree_edges s')\<^sup>+
 2. a \<noteq> v \<Longrightarrow> (a, b) \<in> (tree_edges s')\<^sup>+
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. (a, b) \<in> (tree_edges s')\<^sup>+
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(a, b) \<in> (tree_edges s')\<^sup>+

goal (1 subgoal):
 1. a \<noteq> v \<Longrightarrow> (a, b) \<in> (tree_edges s')\<^sup>+
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<noteq> v \<Longrightarrow> (a, b) \<in> (tree_edges s')\<^sup>+
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
a \<noteq> v

goal (1 subgoal):
 1. a \<noteq> v \<Longrightarrow> (a, b) \<in> (tree_edges s')\<^sup>+
[PROOF STEP]
with \<open>b\<noteq>v\<close> F D discover
[PROOF STATE]
proof (chain)
picking this:
b \<noteq> v
a \<in> dom (discovered s')
b \<in> dom (finished s')
\<delta> s' a < \<delta> s' b \<and> (a \<notin> dom (finished s') \<or> \<phi> s' b < \<phi> s' a)
\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+
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>
a \<noteq> v
[PROOF STEP]
have "(a,b) \<in> (tree_edges s)\<^sup>+"
[PROOF STATE]
proof (prove)
using this:
b \<noteq> v
a \<in> dom (discovered s')
b \<in> dom (finished s')
\<delta> s' a < \<delta> s' b \<and> (a \<notin> dom (finished s') \<or> \<phi> s' b < \<phi> s' a)
\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+
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>
a \<noteq> v

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

goal (1 subgoal):
 1. a \<noteq> v \<Longrightarrow> (a, b) \<in> (tree_edges s')\<^sup>+
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(a, b) \<in> (tree_edges s)\<^sup>+

goal (1 subgoal):
 1. (a, b) \<in> (tree_edges s')\<^sup>+
[PROOF STEP]
by (auto intro: trancl_mono_mp)
[PROOF STATE]
proof (state)
this:
(a, b) \<in> (tree_edges s')\<^sup>+

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>v\<in>dom (discovered s'). \<forall>w\<in>dom (finished s'). \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v) \<longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+

goal (4 subgoals):
 1. \<And>e. \<forall>v\<in>dom (discovered (empty_state e)). \<forall>w\<in>dom (finished (empty_state e)). \<delta> (empty_state e) v < \<delta> (empty_state e) w \<and> (v \<notin> dom (finished (empty_state e)) \<or> \<phi> (empty_state e) w < \<phi> (empty_state e) v) \<longrightarrow> (v, w) \<in> (tree_edges (empty_state e))\<^sup>+
 2. \<And>s s' v0 e. \<lbrakk>\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+; 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\<in>dom (discovered s'). \<forall>w\<in>dom (finished s'). \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v) \<longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+
 3. \<And>s s' u e. \<lbrakk>\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+; 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\<in>dom (discovered s'). \<forall>w\<in>dom (finished s'). \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v) \<longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+
 4. \<And>s s' u v e c b. \<lbrakk>\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+; 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); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (discovered s'). \<forall>w\<in>dom (finished s'). \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v) \<longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>e. \<forall>v\<in>dom (discovered (empty_state e)). \<forall>w\<in>dom (finished (empty_state e)). \<delta> (empty_state e) v < \<delta> (empty_state e) w \<and> (v \<notin> dom (finished (empty_state e)) \<or> \<phi> (empty_state e) w < \<phi> (empty_state e) v) \<longrightarrow> (v, w) \<in> (tree_edges (empty_state e))\<^sup>+
 2. \<And>s s' v0 e. \<lbrakk>\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+; 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\<in>dom (discovered s'). \<forall>w\<in>dom (finished s'). \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v) \<longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+
 3. \<And>s s' u e. \<lbrakk>\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+; 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\<in>dom (discovered s'). \<forall>w\<in>dom (finished s'). \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v) \<longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+
 4. \<And>s s' u v e c b. \<lbrakk>\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+; 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); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (discovered s'). \<forall>w\<in>dom (finished s'). \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v) \<longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+
[PROOF STEP]
case (finish s s' u)
[PROOF STATE]
proof (state)
this:
\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+
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 (4 subgoals):
 1. \<And>e. \<forall>v\<in>dom (discovered (empty_state e)). \<forall>w\<in>dom (finished (empty_state e)). \<delta> (empty_state e) v < \<delta> (empty_state e) w \<and> (v \<notin> dom (finished (empty_state e)) \<or> \<phi> (empty_state e) w < \<phi> (empty_state e) v) \<longrightarrow> (v, w) \<in> (tree_edges (empty_state e))\<^sup>+
 2. \<And>s s' v0 e. \<lbrakk>\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+; 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\<in>dom (discovered s'). \<forall>w\<in>dom (finished s'). \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v) \<longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+
 3. \<And>s s' u e. \<lbrakk>\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+; 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\<in>dom (discovered s'). \<forall>w\<in>dom (finished s'). \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v) \<longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+
 4. \<And>s s' u v e c b. \<lbrakk>\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+; 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); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (discovered s'). \<forall>w\<in>dom (finished s'). \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v) \<longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+
[PROOF STEP]
hence EQ[simp]: "tree_edges s' = tree_edges s"
                    "finished s' = (finished s)(hd (stack s) \<mapsto> counter s)"
                    "discovered s' = discovered s"
                    "stack s' = tl (stack s)"
[PROOF STATE]
proof (prove)
using this:
\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+
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 (1 subgoal):
 1. (tree_edges s' = tree_edges s &&& finished s' = finished s(hd (stack s) \<mapsto> counter s)) &&& discovered s' = discovered s &&& stack s' = tl (stack s)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
tree_edges s' = tree_edges s
finished s' = finished s(hd (stack s) \<mapsto> counter s)
discovered s' = discovered s
stack s' = tl (stack s)

goal (4 subgoals):
 1. \<And>e. \<forall>v\<in>dom (discovered (empty_state e)). \<forall>w\<in>dom (finished (empty_state e)). \<delta> (empty_state e) v < \<delta> (empty_state e) w \<and> (v \<notin> dom (finished (empty_state e)) \<or> \<phi> (empty_state e) w < \<phi> (empty_state e) v) \<longrightarrow> (v, w) \<in> (tree_edges (empty_state e))\<^sup>+
 2. \<And>s s' v0 e. \<lbrakk>\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+; 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\<in>dom (discovered s'). \<forall>w\<in>dom (finished s'). \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v) \<longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+
 3. \<And>s s' u e. \<lbrakk>\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+; 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\<in>dom (discovered s'). \<forall>w\<in>dom (finished s'). \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v) \<longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+
 4. \<And>s s' u v e c b. \<lbrakk>\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+; 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); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (discovered s'). \<forall>w\<in>dom (finished s'). \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v) \<longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+
[PROOF STEP]
from finish
[PROOF STATE]
proof (chain)
picking this:
\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+
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>
[PROOF STEP]
interpret DFS_invar where s=s
[PROOF STATE]
proof (prove)
using this:
\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+
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 (1 subgoal):
 1. DFS_invar G param s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>e. \<forall>v\<in>dom (discovered (empty_state e)). \<forall>w\<in>dom (finished (empty_state e)). \<delta> (empty_state e) v < \<delta> (empty_state e) w \<and> (v \<notin> dom (finished (empty_state e)) \<or> \<phi> (empty_state e) w < \<phi> (empty_state e) v) \<longrightarrow> (v, w) \<in> (tree_edges (empty_state e))\<^sup>+
 2. \<And>s s' v0 e. \<lbrakk>\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+; 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\<in>dom (discovered s'). \<forall>w\<in>dom (finished s'). \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v) \<longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+
 3. \<And>s s' u e. \<lbrakk>\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+; 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\<in>dom (discovered s'). \<forall>w\<in>dom (finished s'). \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v) \<longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+
 4. \<And>s s' u v e c b. \<lbrakk>\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+; 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); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (discovered s'). \<forall>w\<in>dom (finished s'). \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v) \<longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+
[PROOF STEP]
from finish
[PROOF STATE]
proof (chain)
picking this:
\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+
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>
[PROOF STEP]
have NE[simp]: "stack s \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+
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 (1 subgoal):
 1. stack s \<noteq> []
[PROOF STEP]
by (simp add: cond_alt)
[PROOF STATE]
proof (state)
this:
stack s \<noteq> []

goal (4 subgoals):
 1. \<And>e. \<forall>v\<in>dom (discovered (empty_state e)). \<forall>w\<in>dom (finished (empty_state e)). \<delta> (empty_state e) v < \<delta> (empty_state e) w \<and> (v \<notin> dom (finished (empty_state e)) \<or> \<phi> (empty_state e) w < \<phi> (empty_state e) v) \<longrightarrow> (v, w) \<in> (tree_edges (empty_state e))\<^sup>+
 2. \<And>s s' v0 e. \<lbrakk>\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+; 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\<in>dom (discovered s'). \<forall>w\<in>dom (finished s'). \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v) \<longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+
 3. \<And>s s' u e. \<lbrakk>\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+; 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\<in>dom (discovered s'). \<forall>w\<in>dom (finished s'). \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v) \<longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+
 4. \<And>s s' u v e c b. \<lbrakk>\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+; 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); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (discovered s'). \<forall>w\<in>dom (finished s'). \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v) \<longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>v\<in>dom (discovered s'). \<forall>w\<in>dom (finished s'). \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v) \<longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+
[PROOF STEP]
proof (intro ballI impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>v w. \<lbrakk>v \<in> dom (discovered s'); w \<in> dom (finished s'); \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v)\<rbrakk> \<Longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+
[PROOF STEP]
fix a b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>v w. \<lbrakk>v \<in> dom (discovered s'); w \<in> dom (finished s'); \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v)\<rbrakk> \<Longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+
[PROOF STEP]
assume F: "a \<in> dom (discovered s')" "b \<in> dom (finished s')"
        and paren: "\<delta> s' a < \<delta> s' b \<and> (a \<notin> dom (finished s') \<or> \<phi> s' a > \<phi> s' b)"
[PROOF STATE]
proof (state)
this:
a \<in> dom (discovered s')
b \<in> dom (finished s')
\<delta> s' a < \<delta> s' b \<and> (a \<notin> dom (finished s') \<or> \<phi> s' b < \<phi> s' a)

goal (1 subgoal):
 1. \<And>v w. \<lbrakk>v \<in> dom (discovered s'); w \<in> dom (finished s'); \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v)\<rbrakk> \<Longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+
[PROOF STEP]
hence "a \<noteq> b"
[PROOF STATE]
proof (prove)
using this:
a \<in> dom (discovered s')
b \<in> dom (finished s')
\<delta> s' a < \<delta> s' b \<and> (a \<notin> dom (finished s') \<or> \<phi> s' b < \<phi> s' a)

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

goal (1 subgoal):
 1. \<And>v w. \<lbrakk>v \<in> dom (discovered s'); w \<in> dom (finished s'); \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v)\<rbrakk> \<Longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+
[PROOF STEP]
show "(a,b) \<in> (tree_edges s')\<^sup>+"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a, b) \<in> (tree_edges s')\<^sup>+
[PROOF STEP]
proof (cases "b = hd (stack s)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. b = hd (stack s) \<Longrightarrow> (a, b) \<in> (tree_edges s')\<^sup>+
 2. b \<noteq> hd (stack s) \<Longrightarrow> (a, b) \<in> (tree_edges s')\<^sup>+
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
b = hd (stack s)

goal (2 subgoals):
 1. b = hd (stack s) \<Longrightarrow> (a, b) \<in> (tree_edges s')\<^sup>+
 2. b \<noteq> hd (stack s) \<Longrightarrow> (a, b) \<in> (tree_edges s')\<^sup>+
[PROOF STEP]
hence \<phi>b: "\<phi> s' b = counter s"
[PROOF STATE]
proof (prove)
using this:
b = hd (stack s)

goal (1 subgoal):
 1. \<phi> s' b = counter s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<phi> s' b = counter s

goal (2 subgoals):
 1. b = hd (stack s) \<Longrightarrow> (a, b) \<in> (tree_edges s')\<^sup>+
 2. b \<noteq> hd (stack s) \<Longrightarrow> (a, b) \<in> (tree_edges s')\<^sup>+
[PROOF STEP]
have "a \<in> set (stack s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in> set (stack s)
[PROOF STEP]
unfolding stack_set_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in> dom (discovered s) - dom (finished s)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a \<in> dom (discovered s)
 2. a \<notin> dom (finished s)
[PROOF STEP]
from F
[PROOF STATE]
proof (chain)
picking this:
a \<in> dom (discovered s')
b \<in> dom (finished s')
[PROOF STEP]
show "a \<in> dom (discovered s)"
[PROOF STATE]
proof (prove)
using this:
a \<in> dom (discovered s')
b \<in> dom (finished s')

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

goal (1 subgoal):
 1. a \<notin> dom (finished s)
[PROOF STEP]
from True \<open>a\<noteq>b\<close> \<phi>b paren
[PROOF STATE]
proof (chain)
picking this:
b = hd (stack s)
a \<noteq> b
\<phi> s' b = counter s
\<delta> s' a < \<delta> s' b \<and> (a \<notin> dom (finished s') \<or> \<phi> s' b < \<phi> s' a)
[PROOF STEP]
have "a \<in> dom (finished s) \<longrightarrow> \<phi> s a > counter s"
[PROOF STATE]
proof (prove)
using this:
b = hd (stack s)
a \<noteq> b
\<phi> s' b = counter s
\<delta> s' a < \<delta> s' b \<and> (a \<notin> dom (finished s') \<or> \<phi> s' b < \<phi> s' a)

goal (1 subgoal):
 1. a \<in> dom (finished s) \<longrightarrow> counter s < \<phi> s a
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
a \<in> dom (finished s) \<longrightarrow> counter s < \<phi> s a

goal (1 subgoal):
 1. a \<notin> dom (finished s)
[PROOF STEP]
with timing_less_counter
[PROOF STATE]
proof (chain)
picking this:
?v \<in> dom (discovered s) \<Longrightarrow> \<delta> s ?v < counter s
?v \<in> dom (finished s) \<Longrightarrow> \<phi> s ?v < counter s
a \<in> dom (finished s) \<longrightarrow> counter s < \<phi> s a
[PROOF STEP]
show "a \<notin> dom (finished s)"
[PROOF STATE]
proof (prove)
using this:
?v \<in> dom (discovered s) \<Longrightarrow> \<delta> s ?v < counter s
?v \<in> dom (finished s) \<Longrightarrow> \<phi> s ?v < counter s
a \<in> dom (finished s) \<longrightarrow> counter s < \<phi> s a

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
a \<in> set (stack s)

goal (2 subgoals):
 1. b = hd (stack s) \<Longrightarrow> (a, b) \<in> (tree_edges s')\<^sup>+
 2. b \<noteq> hd (stack s) \<Longrightarrow> (a, b) \<in> (tree_edges s')\<^sup>+
[PROOF STEP]
with paren True on_stack_is_tree_path
[PROOF STATE]
proof (chain)
picking this:
\<delta> s' a < \<delta> s' b \<and> (a \<notin> dom (finished s') \<or> \<phi> s' b < \<phi> s' a)
b = hd (stack s)
\<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>+
a \<in> set (stack s)
[PROOF STEP]
have "(a,b) \<in> (tree_edges s)\<^sup>+"
[PROOF STATE]
proof (prove)
using this:
\<delta> s' a < \<delta> s' b \<and> (a \<notin> dom (finished s') \<or> \<phi> s' b < \<phi> s' a)
b = hd (stack s)
\<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>+
a \<in> set (stack s)

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

goal (2 subgoals):
 1. b = hd (stack s) \<Longrightarrow> (a, b) \<in> (tree_edges s')\<^sup>+
 2. b \<noteq> hd (stack s) \<Longrightarrow> (a, b) \<in> (tree_edges s')\<^sup>+
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(a, b) \<in> (tree_edges s)\<^sup>+

goal (1 subgoal):
 1. (a, b) \<in> (tree_edges s')\<^sup>+
[PROOF STEP]
by (auto intro: trancl_mono_mp)
[PROOF STATE]
proof (state)
this:
(a, b) \<in> (tree_edges s')\<^sup>+

goal (1 subgoal):
 1. b \<noteq> hd (stack s) \<Longrightarrow> (a, b) \<in> (tree_edges s')\<^sup>+
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. b \<noteq> hd (stack s) \<Longrightarrow> (a, b) \<in> (tree_edges s')\<^sup>+
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
b \<noteq> hd (stack s)

goal (1 subgoal):
 1. b \<noteq> hd (stack s) \<Longrightarrow> (a, b) \<in> (tree_edges s')\<^sup>+
[PROOF STEP]
note b_not_hd = this
[PROOF STATE]
proof (state)
this:
b \<noteq> hd (stack s)

goal (1 subgoal):
 1. b \<noteq> hd (stack s) \<Longrightarrow> (a, b) \<in> (tree_edges s')\<^sup>+
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a, b) \<in> (tree_edges s')\<^sup>+
[PROOF STEP]
proof (cases "a = hd (stack s)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a = hd (stack s) \<Longrightarrow> (a, b) \<in> (tree_edges s')\<^sup>+
 2. a \<noteq> hd (stack s) \<Longrightarrow> (a, b) \<in> (tree_edges s')\<^sup>+
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
a \<noteq> hd (stack s)

goal (2 subgoals):
 1. a = hd (stack s) \<Longrightarrow> (a, b) \<in> (tree_edges s')\<^sup>+
 2. a \<noteq> hd (stack s) \<Longrightarrow> (a, b) \<in> (tree_edges s')\<^sup>+
[PROOF STEP]
with b_not_hd F paren finish
[PROOF STATE]
proof (chain)
picking this:
b \<noteq> hd (stack s)
a \<in> dom (discovered s')
b \<in> dom (finished s')
\<delta> s' a < \<delta> s' b \<and> (a \<notin> dom (finished s') \<or> \<phi> s' b < \<phi> s' a)
\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+
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>
a \<noteq> hd (stack s)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
b \<noteq> hd (stack s)
a \<in> dom (discovered s')
b \<in> dom (finished s')
\<delta> s' a < \<delta> s' b \<and> (a \<notin> dom (finished s') \<or> \<phi> s' b < \<phi> s' a)
\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+
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>
a \<noteq> hd (stack s)

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

goal (1 subgoal):
 1. a = hd (stack s) \<Longrightarrow> (a, b) \<in> (tree_edges s')\<^sup>+
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a = hd (stack s) \<Longrightarrow> (a, b) \<in> (tree_edges s')\<^sup>+
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
a = hd (stack s)

goal (1 subgoal):
 1. a = hd (stack s) \<Longrightarrow> (a, b) \<in> (tree_edges s')\<^sup>+
[PROOF STEP]
with paren b_not_hd F
[PROOF STATE]
proof (chain)
picking this:
\<delta> s' a < \<delta> s' b \<and> (a \<notin> dom (finished s') \<or> \<phi> s' b < \<phi> s' a)
b \<noteq> hd (stack s)
a \<in> dom (discovered s')
b \<in> dom (finished s')
a = hd (stack s)
[PROOF STEP]
have
            "a \<in> dom (discovered s)" "b \<in> dom (finished s)"  "\<delta> s a < \<delta> s b"
[PROOF STATE]
proof (prove)
using this:
\<delta> s' a < \<delta> s' b \<and> (a \<notin> dom (finished s') \<or> \<phi> s' b < \<phi> s' a)
b \<noteq> hd (stack s)
a \<in> dom (discovered s')
b \<in> dom (finished s')
a = hd (stack s)

goal (1 subgoal):
 1. a \<in> dom (discovered s) &&& b \<in> dom (finished s) &&& \<delta> s a < \<delta> s b
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
a \<in> dom (discovered s)
b \<in> dom (finished s)
\<delta> s a < \<delta> s b

goal (1 subgoal):
 1. a = hd (stack s) \<Longrightarrow> (a, b) \<in> (tree_edges s')\<^sup>+
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
a \<in> dom (discovered s)
b \<in> dom (finished s)
\<delta> s a < \<delta> s b

goal (1 subgoal):
 1. a = hd (stack s) \<Longrightarrow> (a, b) \<in> (tree_edges s')\<^sup>+
[PROOF STEP]
from True stack_not_finished
[PROOF STATE]
proof (chain)
picking this:
a = hd (stack s)
?x \<in> set (stack s) \<Longrightarrow> ?x \<notin> dom (finished s)
[PROOF STEP]
have "a \<notin> dom (finished s)"
[PROOF STATE]
proof (prove)
using this:
a = hd (stack s)
?x \<in> set (stack s) \<Longrightarrow> ?x \<notin> dom (finished s)

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

goal (1 subgoal):
 1. a = hd (stack s) \<Longrightarrow> (a, b) \<in> (tree_edges s')\<^sup>+
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
a \<in> dom (discovered s)
b \<in> dom (finished s)
\<delta> s a < \<delta> s b
a \<notin> dom (finished s)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a \<in> dom (discovered s)
b \<in> dom (finished s)
\<delta> s a < \<delta> s b
a \<notin> dom (finished s)

goal (1 subgoal):
 1. (a, b) \<in> (tree_edges s')\<^sup>+
[PROOF STEP]
by (simp add: finish)
[PROOF STATE]
proof (state)
this:
(a, b) \<in> (tree_edges s')\<^sup>+

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>v\<in>dom (discovered s'). \<forall>w\<in>dom (finished s'). \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v) \<longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+

goal (3 subgoals):
 1. \<And>e. \<forall>v\<in>dom (discovered (empty_state e)). \<forall>w\<in>dom (finished (empty_state e)). \<delta> (empty_state e) v < \<delta> (empty_state e) w \<and> (v \<notin> dom (finished (empty_state e)) \<or> \<phi> (empty_state e) w < \<phi> (empty_state e) v) \<longrightarrow> (v, w) \<in> (tree_edges (empty_state e))\<^sup>+
 2. \<And>s s' v0 e. \<lbrakk>\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+; 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\<in>dom (discovered s'). \<forall>w\<in>dom (finished s'). \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v) \<longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+
 3. \<And>s s' u v e c b. \<lbrakk>\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+; 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); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (discovered s'). \<forall>w\<in>dom (finished s'). \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v) \<longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>e. \<forall>v\<in>dom (discovered (empty_state e)). \<forall>w\<in>dom (finished (empty_state e)). \<delta> (empty_state e) v < \<delta> (empty_state e) w \<and> (v \<notin> dom (finished (empty_state e)) \<or> \<phi> (empty_state e) w < \<phi> (empty_state e) v) \<longrightarrow> (v, w) \<in> (tree_edges (empty_state e))\<^sup>+
 2. \<And>s s' v0 e. \<lbrakk>\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+; 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\<in>dom (discovered s'). \<forall>w\<in>dom (finished s'). \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v) \<longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+
 3. \<And>s s' u v e c b. \<lbrakk>\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+; 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); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (discovered s'). \<forall>w\<in>dom (finished s'). \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v) \<longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+
[PROOF STEP]
case (new_root s s' v0)
[PROOF STATE]
proof (state)
this:
\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+
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>

goal (3 subgoals):
 1. \<And>e. \<forall>v\<in>dom (discovered (empty_state e)). \<forall>w\<in>dom (finished (empty_state e)). \<delta> (empty_state e) v < \<delta> (empty_state e) w \<and> (v \<notin> dom (finished (empty_state e)) \<or> \<phi> (empty_state e) w < \<phi> (empty_state e) v) \<longrightarrow> (v, w) \<in> (tree_edges (empty_state e))\<^sup>+
 2. \<And>s s' v0 e. \<lbrakk>\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+; 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\<in>dom (discovered s'). \<forall>w\<in>dom (finished s'). \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v) \<longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+
 3. \<And>s s' u v e c b. \<lbrakk>\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+; 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); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (discovered s'). \<forall>w\<in>dom (finished s'). \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v) \<longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+
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>
[PROOF STEP]
interpret DFS_invar where s=s
[PROOF STATE]
proof (prove)
using this:
\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+
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>

goal (1 subgoal):
 1. DFS_invar G param s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>e. \<forall>v\<in>dom (discovered (empty_state e)). \<forall>w\<in>dom (finished (empty_state e)). \<delta> (empty_state e) v < \<delta> (empty_state e) w \<and> (v \<notin> dom (finished (empty_state e)) \<or> \<phi> (empty_state e) w < \<phi> (empty_state e) v) \<longrightarrow> (v, w) \<in> (tree_edges (empty_state e))\<^sup>+
 2. \<And>s s' v0 e. \<lbrakk>\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+; 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\<in>dom (discovered s'). \<forall>w\<in>dom (finished s'). \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v) \<longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+
 3. \<And>s s' u v e c b. \<lbrakk>\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+; 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); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (discovered s'). \<forall>w\<in>dom (finished s'). \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v) \<longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+
[PROOF STEP]
from new_root finished_discovered
[PROOF STATE]
proof (chain)
picking this:
\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+
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>
dom (finished s) \<subseteq> dom (discovered s)
[PROOF STEP]
have "v0 \<notin> dom (finished s)"
[PROOF STATE]
proof (prove)
using this:
\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+
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>
dom (finished s) \<subseteq> dom (discovered s)

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

goal (3 subgoals):
 1. \<And>e. \<forall>v\<in>dom (discovered (empty_state e)). \<forall>w\<in>dom (finished (empty_state e)). \<delta> (empty_state e) v < \<delta> (empty_state e) w \<and> (v \<notin> dom (finished (empty_state e)) \<or> \<phi> (empty_state e) w < \<phi> (empty_state e) v) \<longrightarrow> (v, w) \<in> (tree_edges (empty_state e))\<^sup>+
 2. \<And>s s' v0 e. \<lbrakk>\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+; 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\<in>dom (discovered s'). \<forall>w\<in>dom (finished s'). \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v) \<longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+
 3. \<And>s s' u v e c b. \<lbrakk>\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+; 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); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (discovered s'). \<forall>w\<in>dom (finished s'). \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v) \<longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
v0 \<notin> dom (finished s)

goal (3 subgoals):
 1. \<And>e. \<forall>v\<in>dom (discovered (empty_state e)). \<forall>w\<in>dom (finished (empty_state e)). \<delta> (empty_state e) v < \<delta> (empty_state e) w \<and> (v \<notin> dom (finished (empty_state e)) \<or> \<phi> (empty_state e) w < \<phi> (empty_state e) v) \<longrightarrow> (v, w) \<in> (tree_edges (empty_state e))\<^sup>+
 2. \<And>s s' v0 e. \<lbrakk>\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+; 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\<in>dom (discovered s'). \<forall>w\<in>dom (finished s'). \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v) \<longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+
 3. \<And>s s' u v e c b. \<lbrakk>\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+; 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); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (discovered s'). \<forall>w\<in>dom (finished s'). \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v) \<longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+
[PROOF STEP]
note timing_less_counter finished_discovered
[PROOF STATE]
proof (state)
this:
?v \<in> dom (discovered s) \<Longrightarrow> \<delta> s ?v < counter s
?v \<in> dom (finished s) \<Longrightarrow> \<phi> s ?v < counter s
dom (finished s) \<subseteq> dom (discovered s)

goal (3 subgoals):
 1. \<And>e. \<forall>v\<in>dom (discovered (empty_state e)). \<forall>w\<in>dom (finished (empty_state e)). \<delta> (empty_state e) v < \<delta> (empty_state e) w \<and> (v \<notin> dom (finished (empty_state e)) \<or> \<phi> (empty_state e) w < \<phi> (empty_state e) v) \<longrightarrow> (v, w) \<in> (tree_edges (empty_state e))\<^sup>+
 2. \<And>s s' v0 e. \<lbrakk>\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+; 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\<in>dom (discovered s'). \<forall>w\<in>dom (finished s'). \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v) \<longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+
 3. \<And>s s' u v e c b. \<lbrakk>\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+; 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); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (discovered s'). \<forall>w\<in>dom (finished s'). \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v) \<longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
v0 \<notin> dom (finished s)
?v \<in> dom (discovered s) \<Longrightarrow> \<delta> s ?v < counter s
?v \<in> dom (finished s) \<Longrightarrow> \<phi> s ?v < counter s
dom (finished s) \<subseteq> dom (discovered s)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
v0 \<notin> dom (finished s)
?v \<in> dom (discovered s) \<Longrightarrow> \<delta> s ?v < counter s
?v \<in> dom (finished s) \<Longrightarrow> \<phi> s ?v < counter s
dom (finished s) \<subseteq> dom (discovered s)

goal (1 subgoal):
 1. \<forall>v\<in>dom (discovered s'). \<forall>w\<in>dom (finished s'). \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v) \<longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+
[PROOF STEP]
using new_root
[PROOF STATE]
proof (prove)
using this:
v0 \<notin> dom (finished s)
?v \<in> dom (discovered s) \<Longrightarrow> \<delta> s ?v < counter s
?v \<in> dom (finished s) \<Longrightarrow> \<phi> s ?v < counter s
dom (finished s) \<subseteq> dom (discovered s)
\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+
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>

goal (1 subgoal):
 1. \<forall>v\<in>dom (discovered s'). \<forall>w\<in>dom (finished s'). \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v) \<longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+
[PROOF STEP]
by clarsimp force
[PROOF STATE]
proof (state)
this:
\<forall>v\<in>dom (discovered s'). \<forall>w\<in>dom (finished s'). \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v) \<longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+

goal (2 subgoals):
 1. \<And>e. \<forall>v\<in>dom (discovered (empty_state e)). \<forall>w\<in>dom (finished (empty_state e)). \<delta> (empty_state e) v < \<delta> (empty_state e) w \<and> (v \<notin> dom (finished (empty_state e)) \<or> \<phi> (empty_state e) w < \<phi> (empty_state e) v) \<longrightarrow> (v, w) \<in> (tree_edges (empty_state e))\<^sup>+
 2. \<And>s s' u v e c b. \<lbrakk>\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (finished s). \<delta> s v < \<delta> s w \<and> (v \<notin> dom (finished s) \<or> \<phi> s w < \<phi> s v) \<longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+; 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); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (discovered s'). \<forall>w\<in>dom (finished s'). \<delta> s' v < \<delta> s' w \<and> (v \<notin> dom (finished s') \<or> \<phi> s' w < \<phi> s' v) \<longrightarrow> (v, w) \<in> (tree_edges s')\<^sup>+
[PROOF STEP]
qed simp_all


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

goal (1 subgoal):
 1. (v, w) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
by (auto simp add: paren_imp_tree_reach_def)


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

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

goal (1 subgoal):
 1. (v, w) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
using s_paren_imp_tree_reach assms
[PROOF STATE]
proof (prove)
using this:
v \<in> dom (finished s)
w \<in> dom (finished s)
\<delta> s v < \<delta> s w
\<phi> s w < \<phi> s v
v \<in> dom (discovered s)
paren_imp_tree_reach s
v \<in> dom (finished s)
w \<in> dom (finished s)
\<delta> s v < \<delta> s w
\<phi> s w < \<phi> s v

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

goal:
No subgoals!
[PROOF STEP]
qed


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

goal (1 subgoal):
 1. ((v, w) \<in> (tree_edges s)\<^sup>+) = (\<delta> s v < \<delta> s w \<and> \<phi> s w < \<phi> s v)
[PROOF STEP]
by (metis parenthesis_impl_tree_path tree_path_impl_parenthesis)


[STATEMENT]
lemma no_pending_succ_impl_path_in_tree:
    assumes v: "v \<in> dom (discovered s)" "pending s `` {v} = {}"
    and w: "w \<in> succ v"
    and \<delta>: "\<delta> s v < \<delta> s w"
    shows "(v,w) \<in> (tree_edges s)\<^sup>+"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (v, w) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
proof (cases "v \<in> dom (finished s)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. v \<in> dom (finished s) \<Longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+
 2. v \<notin> dom (finished s) \<Longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+
[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, w) \<in> (tree_edges s)\<^sup>+
 2. v \<notin> dom (finished s) \<Longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
with assms assms
[PROOF STATE]
proof (chain)
picking this:
v \<in> dom (discovered s)
pending s `` {v} = {}
w \<in> E `` {v}
\<delta> s v < \<delta> s w
v \<in> dom (discovered s)
pending s `` {v} = {}
w \<in> E `` {v}
\<delta> s v < \<delta> s w
v \<in> dom (finished s)
[PROOF STEP]
have "\<delta> s w < \<phi> s v" "w \<in> dom (discovered s)"
[PROOF STATE]
proof (prove)
using this:
v \<in> dom (discovered s)
pending s `` {v} = {}
w \<in> E `` {v}
\<delta> s v < \<delta> s w
v \<in> dom (discovered s)
pending s `` {v} = {}
w \<in> E `` {v}
\<delta> s v < \<delta> s w
v \<in> dom (finished s)

goal (1 subgoal):
 1. \<delta> s w < \<phi> s v &&& w \<in> dom (discovered s)
[PROOF STEP]
using finished_succ_fin finished_imp_succ_discovered
[PROOF STATE]
proof (prove)
using this:
v \<in> dom (discovered s)
pending s `` {v} = {}
w \<in> E `` {v}
\<delta> s v < \<delta> s w
v \<in> dom (discovered s)
pending s `` {v} = {}
w \<in> E `` {v}
\<delta> s v < \<delta> s w
v \<in> dom (finished s)
\<lbrakk>?v \<in> dom (finished s); ?w \<in> E `` {?v}\<rbrakk> \<Longrightarrow> \<delta> s ?w < \<phi> s ?v
\<lbrakk>?v \<in> dom (finished s); ?w \<in> E `` {?v}\<rbrakk> \<Longrightarrow> ?w \<in> dom (discovered s)

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

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

goal (1 subgoal):
 1. (v, w) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
using parenthesis_contained parenthesis_impl_tree_path
[PROOF STATE]
proof (prove)
using this:
v \<in> dom (finished s)
\<delta> s v < \<delta> s w
\<delta> s w < \<phi> s v
w \<in> dom (discovered s)
\<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
\<lbrakk>?v \<in> dom (finished s); ?w \<in> dom (finished s); \<delta> s ?v < \<delta> s ?w; \<phi> s ?w < \<phi> s ?v\<rbrakk> \<Longrightarrow> (?v, ?w) \<in> (tree_edges s)\<^sup>+

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

goal (1 subgoal):
 1. v \<notin> dom (finished s) \<Longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. v \<notin> dom (finished s) \<Longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+
[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, w) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (v, w) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
proof (cases "w \<in> dom (finished s)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. w \<in> dom (finished s) \<Longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+
 2. w \<notin> dom (finished s) \<Longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
w \<in> dom (finished s)

goal (2 subgoals):
 1. w \<in> dom (finished s) \<Longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+
 2. w \<notin> dom (finished s) \<Longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
with False v \<delta>
[PROOF STATE]
proof (chain)
picking this:
v \<notin> dom (finished s)
v \<in> dom (discovered s)
pending s `` {v} = {}
\<delta> s v < \<delta> s w
w \<in> dom (finished s)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
v \<notin> dom (finished s)
v \<in> dom (discovered s)
pending s `` {v} = {}
\<delta> s v < \<delta> s w
w \<in> dom (finished s)

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

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

goal (1 subgoal):
 1. w \<notin> dom (finished s) \<Longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
with \<open>v \<notin> dom (finished s)\<close> no_pending_imp_succ_discovered v w
[PROOF STATE]
proof (chain)
picking this:
v \<notin> dom (finished s)
\<lbrakk>?u \<in> dom (discovered s); pending s `` {?u} = {}; ?v \<in> E `` {?u}\<rbrakk> \<Longrightarrow> ?v \<in> dom (discovered s)
v \<in> dom (discovered s)
pending s `` {v} = {}
w \<in> E `` {v}
w \<notin> dom (finished s)
[PROOF STEP]
have
        "v \<in> set (stack s)" "w \<in> set (stack s)"
[PROOF STATE]
proof (prove)
using this:
v \<notin> dom (finished s)
\<lbrakk>?u \<in> dom (discovered s); pending s `` {?u} = {}; ?v \<in> E `` {?u}\<rbrakk> \<Longrightarrow> ?v \<in> dom (discovered s)
v \<in> dom (discovered s)
pending s `` {v} = {}
w \<in> E `` {v}
w \<notin> dom (finished s)

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

goal (1 subgoal):
 1. w \<notin> dom (finished s) \<Longrightarrow> (v, w) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
with on_stack_is_tree_path \<delta>
[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>+
\<delta> s v < \<delta> s w
v \<in> set (stack s)
w \<in> set (stack s)
[PROOF STEP]
show ?thesis
[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>+
\<delta> s v < \<delta> s w
v \<in> set (stack s)
w \<in> set (stack s)

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma finished_succ_impl_path_in_tree:
    assumes f:  "v \<in> dom (finished s)"
    and s: "w \<in> succ v"
    and \<delta>: "\<delta> s v < \<delta> s w"
    shows "(v,w) \<in> (tree_edges s)\<^sup>+"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (v, w) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
using no_pending_succ_impl_path_in_tree finished_no_pending finished_discovered
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?v \<in> dom (discovered s); pending s `` {?v} = {}; ?w \<in> E `` {?v}; \<delta> s ?v < \<delta> s ?w\<rbrakk> \<Longrightarrow> (?v, ?w) \<in> (tree_edges s)\<^sup>+
?v \<in> dom (finished s) \<Longrightarrow> pending s `` {?v} = {}
dom (finished s) \<subseteq> dom (discovered s)

goal (1 subgoal):
 1. (v, w) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?v \<in> dom (discovered s); pending s `` {?v} = {}; ?w \<in> E `` {?v}; \<delta> s ?v < \<delta> s ?w\<rbrakk> \<Longrightarrow> (?v, ?w) \<in> (tree_edges s)\<^sup>+
?v \<in> dom (finished s) \<Longrightarrow> pending s `` {?v} = {}
dom (finished s) \<subseteq> dom (discovered s)
v \<in> dom (finished s)
w \<in> E `` {v}
\<delta> s v < \<delta> s w

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