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

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

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

goal (1 subgoal):
 1. u \<notin> dom (finished s)
[PROOF STEP]
using hd_in_set
[PROOF STATE]
proof (prove)
using this:
\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s
cond s
DFS_invar G param s
DFS_invar G param s'
stack s \<noteq> []
v \<in> pending s `` {u}
v \<in> dom (discovered s)
v \<in> dom (finished s)
u = hd (stack s)
s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e_\<rparr>
u \<in> set (stack s) \<Longrightarrow> u \<notin> dom (finished s)
?xs \<noteq> [] \<Longrightarrow> hd ?xs \<in> set ?xs

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

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

goal (1 subgoal):
 1. \<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'

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

goal (5 subgoals):
 1. \<And>e. \<forall>(v, w)\<in>E. v \<in> dom (discovered (empty_state e)) \<and> w \<in> dom (discovered (empty_state e)) \<and> \<delta> (empty_state e) w \<le> \<delta> (empty_state e) v \<and> (w \<in> dom (finished (empty_state e)) \<longrightarrow> v \<in> dom (finished (empty_state e)) \<and> \<phi> (empty_state e) v \<le> \<phi> (empty_state e) w) \<longrightarrow> (v, w) \<in> back_edges (empty_state e) \<or> (v, w) \<in> pending (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'
 3. \<And>s s' u e. \<lbrakk>\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; pending s `` {u} = {}; u = hd (stack s); s' = finish u s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'
 4. \<And>s s' u v e. \<lbrakk>\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); v \<notin> dom (finished s); u = hd (stack s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'
 5. \<And>s s' u v e. \<lbrakk>\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<notin> dom (discovered s); u = hd (stack s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s
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 := v\<rparr>
[PROOF STEP]
interpret DFS_invar where s=s
[PROOF STATE]
proof (prove)
using this:
\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s
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 := v\<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, w)\<in>E. v \<in> dom (discovered (empty_state e)) \<and> w \<in> dom (discovered (empty_state e)) \<and> \<delta> (empty_state e) w \<le> \<delta> (empty_state e) v \<and> (w \<in> dom (finished (empty_state e)) \<longrightarrow> v \<in> dom (finished (empty_state e)) \<and> \<phi> (empty_state e) v \<le> \<phi> (empty_state e) w) \<longrightarrow> (v, w) \<in> back_edges (empty_state e) \<or> (v, w) \<in> pending (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'
 3. \<And>s s' u e. \<lbrakk>\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; pending s `` {u} = {}; u = hd (stack s); s' = finish u s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'
 4. \<And>s s' u v e. \<lbrakk>\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); v \<notin> dom (finished s); u = hd (stack s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'
 5. \<And>s s' u v e. \<lbrakk>\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<notin> dom (discovered s); u = hd (stack s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'
[PROOF STEP]
from finish
[PROOF STATE]
proof (chain)
picking this:
\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s
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 := v\<rparr>
[PROOF STEP]
have
      IH: "\<And>v w. \<lbrakk>w \<in> succ v; v \<in> dom (discovered s); w \<in> dom (discovered s);
                  \<delta> s w \<le> \<delta> s v;
                  (w \<in> dom (finished s) \<Longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w)\<rbrakk>
                 \<Longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s"
[PROOF STATE]
proof (prove)
using this:
\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s
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 := v\<rparr>

goal (1 subgoal):
 1. \<And>v w. \<lbrakk>w \<in> E `` {v}; v \<in> dom (discovered s); w \<in> dom (discovered s); \<delta> s w \<le> \<delta> s v; w \<in> dom (finished s) \<Longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w\<rbrakk> \<Longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>?w7 \<in> E `` {?v7}; ?v7 \<in> dom (discovered s); ?w7 \<in> dom (discovered s); \<delta> s ?w7 \<le> \<delta> s ?v7; ?w7 \<in> dom (finished s) \<Longrightarrow> ?v7 \<in> dom (finished s) \<and> \<phi> s ?v7 \<le> \<phi> s ?w7\<rbrakk> \<Longrightarrow> (?v7, ?w7) \<in> back_edges s \<or> (?v7, ?w7) \<in> pending s

goal (5 subgoals):
 1. \<And>e. \<forall>(v, w)\<in>E. v \<in> dom (discovered (empty_state e)) \<and> w \<in> dom (discovered (empty_state e)) \<and> \<delta> (empty_state e) w \<le> \<delta> (empty_state e) v \<and> (w \<in> dom (finished (empty_state e)) \<longrightarrow> v \<in> dom (finished (empty_state e)) \<and> \<phi> (empty_state e) v \<le> \<phi> (empty_state e) w) \<longrightarrow> (v, w) \<in> back_edges (empty_state e) \<or> (v, w) \<in> pending (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'
 3. \<And>s s' u e. \<lbrakk>\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; pending s `` {u} = {}; u = hd (stack s); s' = finish u s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'
 4. \<And>s s' u v e. \<lbrakk>\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); v \<notin> dom (finished s); u = hd (stack s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'
 5. \<And>s s' u v e. \<lbrakk>\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<notin> dom (discovered s); u = hd (stack s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'
[PROOF STEP]
from finish
[PROOF STATE]
proof (chain)
picking this:
\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s
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 := v\<rparr>
[PROOF STEP]
have ne[simp]: "stack s \<noteq> []"
                 and p[simp]: "pending s `` {hd (stack s)} = {}"
[PROOF STATE]
proof (prove)
using this:
\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s
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 := v\<rparr>

goal (1 subgoal):
 1. stack s \<noteq> [] &&& pending s `` {hd (stack s)} = {}
[PROOF STEP]
by (simp_all)
[PROOF STATE]
proof (state)
this:
stack s \<noteq> []
pending s `` {hd (stack s)} = {}

goal (5 subgoals):
 1. \<And>e. \<forall>(v, w)\<in>E. v \<in> dom (discovered (empty_state e)) \<and> w \<in> dom (discovered (empty_state e)) \<and> \<delta> (empty_state e) w \<le> \<delta> (empty_state e) v \<and> (w \<in> dom (finished (empty_state e)) \<longrightarrow> v \<in> dom (finished (empty_state e)) \<and> \<phi> (empty_state e) v \<le> \<phi> (empty_state e) w) \<longrightarrow> (v, w) \<in> back_edges (empty_state e) \<or> (v, w) \<in> pending (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'
 3. \<And>s s' u e. \<lbrakk>\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; pending s `` {u} = {}; u = hd (stack s); s' = finish u s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'
 4. \<And>s s' u v e. \<lbrakk>\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); v \<notin> dom (finished s); u = hd (stack s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'
 5. \<And>s s' u v e. \<lbrakk>\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<notin> dom (discovered s); u = hd (stack s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'
[PROOF STEP]
from hd_in_set[OF ne]
[PROOF STATE]
proof (chain)
picking this:
hd (stack s) \<in> set (stack s)
[PROOF STEP]
have disc: "hd (stack s) \<in> dom (discovered s)"
                            and not_fin: "hd (stack s) \<notin> dom (finished s)"
[PROOF STATE]
proof (prove)
using this:
hd (stack s) \<in> set (stack s)

goal (1 subgoal):
 1. hd (stack s) \<in> dom (discovered s) &&& hd (stack s) \<notin> dom (finished s)
[PROOF STEP]
using stack_discovered stack_not_finished
[PROOF STATE]
proof (prove)
using this:
hd (stack s) \<in> set (stack s)
set (stack s) \<subseteq> dom (discovered s)
?x \<in> set (stack s) \<Longrightarrow> ?x \<notin> dom (finished s)

goal (1 subgoal):
 1. hd (stack s) \<in> dom (discovered s) &&& hd (stack s) \<notin> dom (finished s)
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
hd (stack s) \<in> dom (discovered s)
hd (stack s) \<notin> dom (finished s)

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

goal (5 subgoals):
 1. \<And>e. \<forall>(v, w)\<in>E. v \<in> dom (discovered (empty_state e)) \<and> w \<in> dom (discovered (empty_state e)) \<and> \<delta> (empty_state e) w \<le> \<delta> (empty_state e) v \<and> (w \<in> dom (finished (empty_state e)) \<longrightarrow> v \<in> dom (finished (empty_state e)) \<and> \<phi> (empty_state e) v \<le> \<phi> (empty_state e) w) \<longrightarrow> (v, w) \<in> back_edges (empty_state e) \<or> (v, w) \<in> pending (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'
 3. \<And>s s' u e. \<lbrakk>\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; pending s `` {u} = {}; u = hd (stack s); s' = finish u s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'
 4. \<And>s s' u v e. \<lbrakk>\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); v \<notin> dom (finished s); u = hd (stack s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'
 5. \<And>s s' u v e. \<lbrakk>\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<notin> dom (discovered s); u = hd (stack s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'
[PROOF STEP]
fix w
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>e. \<forall>(v, w)\<in>E. v \<in> dom (discovered (empty_state e)) \<and> w \<in> dom (discovered (empty_state e)) \<and> \<delta> (empty_state e) w \<le> \<delta> (empty_state e) v \<and> (w \<in> dom (finished (empty_state e)) \<longrightarrow> v \<in> dom (finished (empty_state e)) \<and> \<phi> (empty_state e) v \<le> \<phi> (empty_state e) w) \<longrightarrow> (v, w) \<in> back_edges (empty_state e) \<or> (v, w) \<in> pending (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'
 3. \<And>s s' u e. \<lbrakk>\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; pending s `` {u} = {}; u = hd (stack s); s' = finish u s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'
 4. \<And>s s' u v e. \<lbrakk>\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); v \<notin> dom (finished s); u = hd (stack s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'
 5. \<And>s s' u v e. \<lbrakk>\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<notin> dom (discovered s); u = hd (stack s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'
[PROOF STEP]
assume w: "w \<in> succ (hd (stack s))" "w \<noteq> hd (stack s)" "w \<in> dom (discovered s)"
        and f: "w \<in> dom (finished s) \<longrightarrow> counter s \<le> \<phi> s w"
        and \<delta>: "\<delta> s w \<le> \<delta> s (hd (stack s))"
[PROOF STATE]
proof (state)
this:
w \<in> E `` {hd (stack s)}
w \<noteq> hd (stack s)
w \<in> dom (discovered s)
w \<in> dom (finished s) \<longrightarrow> counter s \<le> \<phi> s w
\<delta> s w \<le> \<delta> s (hd (stack s))

goal (5 subgoals):
 1. \<And>e. \<forall>(v, w)\<in>E. v \<in> dom (discovered (empty_state e)) \<and> w \<in> dom (discovered (empty_state e)) \<and> \<delta> (empty_state e) w \<le> \<delta> (empty_state e) v \<and> (w \<in> dom (finished (empty_state e)) \<longrightarrow> v \<in> dom (finished (empty_state e)) \<and> \<phi> (empty_state e) v \<le> \<phi> (empty_state e) w) \<longrightarrow> (v, w) \<in> back_edges (empty_state e) \<or> (v, w) \<in> pending (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'
 3. \<And>s s' u e. \<lbrakk>\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; pending s `` {u} = {}; u = hd (stack s); s' = finish u s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'
 4. \<And>s s' u v e. \<lbrakk>\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); v \<notin> dom (finished s); u = hd (stack s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'
 5. \<And>s s' u v e. \<lbrakk>\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<notin> dom (discovered s); u = hd (stack s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending 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
w \<in> E `` {hd (stack s)}
w \<noteq> hd (stack s)
w \<in> dom (discovered s)
w \<in> dom (finished s) \<longrightarrow> counter s \<le> \<phi> s w
\<delta> s w \<le> \<delta> s (hd (stack s))
[PROOF STEP]
have "w \<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
w \<in> E `` {hd (stack s)}
w \<noteq> hd (stack s)
w \<in> dom (discovered s)
w \<in> dom (finished s) \<longrightarrow> counter s \<le> \<phi> s w
\<delta> s w \<le> \<delta> s (hd (stack s))

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

goal (5 subgoals):
 1. \<And>e. \<forall>(v, w)\<in>E. v \<in> dom (discovered (empty_state e)) \<and> w \<in> dom (discovered (empty_state e)) \<and> \<delta> (empty_state e) w \<le> \<delta> (empty_state e) v \<and> (w \<in> dom (finished (empty_state e)) \<longrightarrow> v \<in> dom (finished (empty_state e)) \<and> \<phi> (empty_state e) v \<le> \<phi> (empty_state e) w) \<longrightarrow> (v, w) \<in> back_edges (empty_state e) \<or> (v, w) \<in> pending (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'
 3. \<And>s s' u e. \<lbrakk>\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; pending s `` {u} = {}; u = hd (stack s); s' = finish u s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'
 4. \<And>s s' u v e. \<lbrakk>\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); v \<notin> dom (finished s); u = hd (stack s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'
 5. \<And>s s' u v e. \<lbrakk>\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<notin> dom (discovered s); u = hd (stack s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'
[PROOF STEP]
with finish w \<delta> disc
[PROOF STATE]
proof (chain)
picking this:
\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s
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 := v\<rparr>
w \<in> E `` {hd (stack s)}
w \<noteq> hd (stack s)
w \<in> dom (discovered s)
\<delta> s w \<le> \<delta> s (hd (stack s))
hd (stack s) \<in> dom (discovered s)
w \<notin> dom (finished s)
[PROOF STEP]
have "(hd (stack s), w) \<in> back_edges s"
[PROOF STATE]
proof (prove)
using this:
\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s
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 := v\<rparr>
w \<in> E `` {hd (stack s)}
w \<noteq> hd (stack s)
w \<in> dom (discovered s)
\<delta> s w \<le> \<delta> s (hd (stack s))
hd (stack s) \<in> dom (discovered s)
w \<notin> dom (finished s)

goal (1 subgoal):
 1. (hd (stack s), w) \<in> back_edges s
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(hd (stack s), w) \<in> back_edges s

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

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

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

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

goal (5 subgoals):
 1. \<And>e. \<forall>(v, w)\<in>E. v \<in> dom (discovered (empty_state e)) \<and> w \<in> dom (discovered (empty_state e)) \<and> \<delta> (empty_state e) w \<le> \<delta> (empty_state e) v \<and> (w \<in> dom (finished (empty_state e)) \<longrightarrow> v \<in> dom (finished (empty_state e)) \<and> \<phi> (empty_state e) v \<le> \<phi> (empty_state e) w) \<longrightarrow> (v, w) \<in> back_edges (empty_state e) \<or> (v, w) \<in> pending (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'
 3. \<And>s s' u e. \<lbrakk>\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; pending s `` {u} = {}; u = hd (stack s); s' = finish u s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'
 4. \<And>s s' u v e. \<lbrakk>\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); v \<notin> dom (finished s); u = hd (stack s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'
 5. \<And>s s' u v e. \<lbrakk>\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<notin> dom (discovered s); u = hd (stack s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'
[PROOF STEP]
with IH[of "hd (stack s)" w] disc not_fin
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>hd (stack s) \<in> E `` {w}; w \<in> dom (discovered s); hd (stack s) \<in> dom (discovered s); \<delta> s (hd (stack s)) \<le> \<delta> s w; hd (stack s) \<in> dom (finished s) \<Longrightarrow> w \<in> dom (finished s) \<and> \<phi> s w \<le> \<phi> s (hd (stack s))\<rbrakk> \<Longrightarrow> (w, hd (stack s)) \<in> back_edges s \<or> (w, hd (stack s)) \<in> pending s
hd (stack s) \<in> dom (discovered s)
hd (stack s) \<notin> dom (finished s)
hd (stack s) \<in> E `` {w}
w \<noteq> hd (stack s)
w \<in> dom (finished s)
\<delta> s (hd (stack s)) \<le> \<delta> s w
[PROOF STEP]
have
        "(w, hd (stack s)) \<in> back_edges s"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>hd (stack s) \<in> E `` {w}; w \<in> dom (discovered s); hd (stack s) \<in> dom (discovered s); \<delta> s (hd (stack s)) \<le> \<delta> s w; hd (stack s) \<in> dom (finished s) \<Longrightarrow> w \<in> dom (finished s) \<and> \<phi> s w \<le> \<phi> s (hd (stack s))\<rbrakk> \<Longrightarrow> (w, hd (stack s)) \<in> back_edges s \<or> (w, hd (stack s)) \<in> pending s
hd (stack s) \<in> dom (discovered s)
hd (stack s) \<notin> dom (finished s)
hd (stack s) \<in> E `` {w}
w \<noteq> hd (stack s)
w \<in> dom (finished s)
\<delta> s (hd (stack s)) \<le> \<delta> s w

goal (1 subgoal):
 1. (w, hd (stack s)) \<in> back_edges s
[PROOF STEP]
using finished_discovered finished_no_pending[of w]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>hd (stack s) \<in> E `` {w}; w \<in> dom (discovered s); hd (stack s) \<in> dom (discovered s); \<delta> s (hd (stack s)) \<le> \<delta> s w; hd (stack s) \<in> dom (finished s) \<Longrightarrow> w \<in> dom (finished s) \<and> \<phi> s w \<le> \<phi> s (hd (stack s))\<rbrakk> \<Longrightarrow> (w, hd (stack s)) \<in> back_edges s \<or> (w, hd (stack s)) \<in> pending s
hd (stack s) \<in> dom (discovered s)
hd (stack s) \<notin> dom (finished s)
hd (stack s) \<in> E `` {w}
w \<noteq> hd (stack s)
w \<in> dom (finished s)
\<delta> s (hd (stack s)) \<le> \<delta> s w
dom (finished s) \<subseteq> dom (discovered s)
w \<in> dom (finished s) \<Longrightarrow> pending s `` {w} = {}

goal (1 subgoal):
 1. (w, hd (stack s)) \<in> back_edges s
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(w, hd (stack s)) \<in> back_edges s

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

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

goal (1 subgoal):
 1. \<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'
[PROOF STEP]
using finish
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?w9 \<in> E `` {hd (stack s)}; ?w9 \<noteq> hd (stack s); ?w9 \<in> dom (discovered s); ?w9 \<in> dom (finished s) \<longrightarrow> counter s \<le> \<phi> s ?w9; \<delta> s ?w9 \<le> \<delta> s (hd (stack s))\<rbrakk> \<Longrightarrow> (hd (stack s), ?w9) \<in> back_edges s
\<lbrakk>hd (stack s) \<in> E `` {?w9}; ?w9 \<noteq> hd (stack s); ?w9 \<in> dom (finished s); \<delta> s (hd (stack s)) \<le> \<delta> s ?w9\<rbrakk> \<Longrightarrow> (?w9, hd (stack s)) \<in> back_edges s
\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s
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 := v\<rparr>

goal (1 subgoal):
 1. \<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'
[PROOF STEP]
by clarsimp auto
[PROOF STATE]
proof (state)
this:
\<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'

goal (4 subgoals):
 1. \<And>e. \<forall>(v, w)\<in>E. v \<in> dom (discovered (empty_state e)) \<and> w \<in> dom (discovered (empty_state e)) \<and> \<delta> (empty_state e) w \<le> \<delta> (empty_state e) v \<and> (w \<in> dom (finished (empty_state e)) \<longrightarrow> v \<in> dom (finished (empty_state e)) \<and> \<phi> (empty_state e) v \<le> \<phi> (empty_state e) w) \<longrightarrow> (v, w) \<in> back_edges (empty_state e) \<or> (v, w) \<in> pending (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'
 3. \<And>s s' u v e. \<lbrakk>\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); v \<notin> dom (finished s); u = hd (stack s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'
 4. \<And>s s' u v e. \<lbrakk>\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<notin> dom (discovered s); u = hd (stack s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>e. \<forall>(v, w)\<in>E. v \<in> dom (discovered (empty_state e)) \<and> w \<in> dom (discovered (empty_state e)) \<and> \<delta> (empty_state e) w \<le> \<delta> (empty_state e) v \<and> (w \<in> dom (finished (empty_state e)) \<longrightarrow> v \<in> dom (finished (empty_state e)) \<and> \<phi> (empty_state e) v \<le> \<phi> (empty_state e) w) \<longrightarrow> (v, w) \<in> back_edges (empty_state e) \<or> (v, w) \<in> pending (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'
 3. \<And>s s' u v e. \<lbrakk>\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); v \<notin> dom (finished s); u = hd (stack s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'
 4. \<And>s s' u v e. \<lbrakk>\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<notin> dom (discovered s); u = hd (stack s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'
[PROOF STEP]
case (discover s s' u v)
[PROOF STATE]
proof (state)
this:
\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s
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 (4 subgoals):
 1. \<And>e. \<forall>(v, w)\<in>E. v \<in> dom (discovered (empty_state e)) \<and> w \<in> dom (discovered (empty_state e)) \<and> \<delta> (empty_state e) w \<le> \<delta> (empty_state e) v \<and> (w \<in> dom (finished (empty_state e)) \<longrightarrow> v \<in> dom (finished (empty_state e)) \<and> \<phi> (empty_state e) v \<le> \<phi> (empty_state e) w) \<longrightarrow> (v, w) \<in> back_edges (empty_state e) \<or> (v, w) \<in> pending (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'
 3. \<And>s s' u v e. \<lbrakk>\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); v \<notin> dom (finished s); u = hd (stack s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'
 4. \<And>s s' u v e. \<lbrakk>\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<notin> dom (discovered s); u = hd (stack s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s
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, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s
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 (4 subgoals):
 1. \<And>e. \<forall>(v, w)\<in>E. v \<in> dom (discovered (empty_state e)) \<and> w \<in> dom (discovered (empty_state e)) \<and> \<delta> (empty_state e) w \<le> \<delta> (empty_state e) v \<and> (w \<in> dom (finished (empty_state e)) \<longrightarrow> v \<in> dom (finished (empty_state e)) \<and> \<phi> (empty_state e) v \<le> \<phi> (empty_state e) w) \<longrightarrow> (v, w) \<in> back_edges (empty_state e) \<or> (v, w) \<in> pending (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'
 3. \<And>s s' u v e. \<lbrakk>\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); v \<notin> dom (finished s); u = hd (stack s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'
 4. \<And>s s' u v e. \<lbrakk>\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<notin> dom (discovered s); u = hd (stack s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'
[PROOF STEP]
from discover
[PROOF STATE]
proof (chain)
picking this:
\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s
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]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s
cond s
DFS_invar G param s
DFS_invar G param s'
stack s \<noteq> []
v \<in> pending s `` {u}
v \<notin> dom (discovered s)
u = hd (stack s)
s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e_\<rparr>

goal (1 subgoal):
 1. \<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'
[PROOF STEP]
using timing_less_counter
[PROOF STATE]
proof (prove)
using this:
\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s
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>
?v \<in> dom (discovered s) \<Longrightarrow> \<delta> s ?v < counter s
?v \<in> dom (finished s) \<Longrightarrow> \<phi> s ?v < counter s

goal (1 subgoal):
 1. \<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'
[PROOF STEP]
by clarsimp fastforce
[PROOF STATE]
proof (state)
this:
\<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'

goal (3 subgoals):
 1. \<And>e. \<forall>(v, w)\<in>E. v \<in> dom (discovered (empty_state e)) \<and> w \<in> dom (discovered (empty_state e)) \<and> \<delta> (empty_state e) w \<le> \<delta> (empty_state e) v \<and> (w \<in> dom (finished (empty_state e)) \<longrightarrow> v \<in> dom (finished (empty_state e)) \<and> \<phi> (empty_state e) v \<le> \<phi> (empty_state e) w) \<longrightarrow> (v, w) \<in> back_edges (empty_state e) \<or> (v, w) \<in> pending (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'
 3. \<And>s s' u v e. \<lbrakk>\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); v \<notin> dom (finished s); u = hd (stack s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>e. \<forall>(v, w)\<in>E. v \<in> dom (discovered (empty_state e)) \<and> w \<in> dom (discovered (empty_state e)) \<and> \<delta> (empty_state e) w \<le> \<delta> (empty_state e) v \<and> (w \<in> dom (finished (empty_state e)) \<longrightarrow> v \<in> dom (finished (empty_state e)) \<and> \<phi> (empty_state e) v \<le> \<phi> (empty_state e) w) \<longrightarrow> (v, w) \<in> back_edges (empty_state e) \<or> (v, w) \<in> pending (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'
 3. \<And>s s' u v e. \<lbrakk>\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); v \<notin> dom (finished s); u = hd (stack s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'
[PROOF STEP]
case (new_root s s' v0)
[PROOF STATE]
proof (state)
this:
\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s
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, w)\<in>E. v \<in> dom (discovered (empty_state e)) \<and> w \<in> dom (discovered (empty_state e)) \<and> \<delta> (empty_state e) w \<le> \<delta> (empty_state e) v \<and> (w \<in> dom (finished (empty_state e)) \<longrightarrow> v \<in> dom (finished (empty_state e)) \<and> \<phi> (empty_state e) v \<le> \<phi> (empty_state e) w) \<longrightarrow> (v, w) \<in> back_edges (empty_state e) \<or> (v, w) \<in> pending (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'
 3. \<And>s s' u v e. \<lbrakk>\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); v \<notin> dom (finished s); u = hd (stack s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s
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, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s
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, w)\<in>E. v \<in> dom (discovered (empty_state e)) \<and> w \<in> dom (discovered (empty_state e)) \<and> \<delta> (empty_state e) w \<le> \<delta> (empty_state e) v \<and> (w \<in> dom (finished (empty_state e)) \<longrightarrow> v \<in> dom (finished (empty_state e)) \<and> \<phi> (empty_state e) v \<le> \<phi> (empty_state e) w) \<longrightarrow> (v, w) \<in> back_edges (empty_state e) \<or> (v, w) \<in> pending (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'
 3. \<And>s s' u v e. \<lbrakk>\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); v \<notin> dom (finished s); u = hd (stack s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'
[PROOF STEP]
from new_root empty_stack_imp_empty_pending
[PROOF STATE]
proof (chain)
picking this:
\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s
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>
stack s = [] \<Longrightarrow> pending s = {}
[PROOF STEP]
have "pending s = {}"
[PROOF STATE]
proof (prove)
using this:
\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s
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>
stack s = [] \<Longrightarrow> pending s = {}

goal (1 subgoal):
 1. pending s = {}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
pending s = {}

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

goal (1 subgoal):
 1. \<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'
[PROOF STEP]
using timing_less_counter
[PROOF STATE]
proof (prove)
using this:
\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s
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>
pending s = {}
?v \<in> dom (discovered s) \<Longrightarrow> \<delta> s ?v < counter s
?v \<in> dom (finished s) \<Longrightarrow> \<phi> s ?v < counter s

goal (1 subgoal):
 1. \<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'
[PROOF STEP]
by clarsimp fastforce
[PROOF STATE]
proof (state)
this:
\<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'

goal (2 subgoals):
 1. \<And>e. \<forall>(v, w)\<in>E. v \<in> dom (discovered (empty_state e)) \<and> w \<in> dom (discovered (empty_state e)) \<and> \<delta> (empty_state e) w \<le> \<delta> (empty_state e) v \<and> (w \<in> dom (finished (empty_state e)) \<longrightarrow> v \<in> dom (finished (empty_state e)) \<and> \<phi> (empty_state e) v \<le> \<phi> (empty_state e) w) \<longrightarrow> (v, w) \<in> back_edges (empty_state e) \<or> (v, w) \<in> pending (empty_state e)
 2. \<And>s s' u v e. \<lbrakk>\<forall>(v, w)\<in>E. v \<in> dom (discovered s) \<and> w \<in> dom (discovered s) \<and> \<delta> s w \<le> \<delta> s v \<and> (w \<in> dom (finished s) \<longrightarrow> v \<in> dom (finished s) \<and> \<phi> s v \<le> \<phi> s w) \<longrightarrow> (v, w) \<in> back_edges s \<or> (v, w) \<in> pending s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); v \<notin> dom (finished s); u = hd (stack s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, w)\<in>E. v \<in> dom (discovered s') \<and> w \<in> dom (discovered s') \<and> \<delta> s' w \<le> \<delta> s' v \<and> (w \<in> dom (finished s') \<longrightarrow> v \<in> dom (finished s') \<and> \<phi> s' v \<le> \<phi> s' w) \<longrightarrow> (v, w) \<in> back_edges s' \<or> (v, w) \<in> pending s'
[PROOF STEP]
qed auto