[STATEMENT]
lemma timing_common_inv:
    "is_invar timing_common_inv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_invar timing_common_inv
[PROOF STEP]
proof (induction rule: is_invarI)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>e. timing_common_inv (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>timing_common_inv 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> timing_common_inv s'
 3. \<And>s s' u e. \<lbrakk>timing_common_inv 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> timing_common_inv s'
 4. \<And>s s' u v e c b. \<lbrakk>timing_common_inv 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); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> timing_common_inv s'
 5. \<And>s s' u v e. \<lbrakk>timing_common_inv 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> timing_common_inv s'
[PROOF STEP]
case (finish s s')
[PROOF STATE]
proof (state)
this:
timing_common_inv 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>

goal (5 subgoals):
 1. \<And>e. timing_common_inv (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>timing_common_inv 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> timing_common_inv s'
 3. \<And>s s' u e. \<lbrakk>timing_common_inv 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> timing_common_inv s'
 4. \<And>s s' u v e c b. \<lbrakk>timing_common_inv 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); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> timing_common_inv s'
 5. \<And>s s' u v e. \<lbrakk>timing_common_inv 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> timing_common_inv s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
timing_common_inv 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>
[PROOF STEP]
interpret DFS_invar where s=s
[PROOF STATE]
proof (prove)
using this:
timing_common_inv 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>

goal (1 subgoal):
 1. DFS_invar G param s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>e. timing_common_inv (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>timing_common_inv 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> timing_common_inv s'
 3. \<And>s s' u e. \<lbrakk>timing_common_inv 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> timing_common_inv s'
 4. \<And>s s' u v e c b. \<lbrakk>timing_common_inv 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); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> timing_common_inv s'
 5. \<And>s s' u v e. \<lbrakk>timing_common_inv 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> timing_common_inv s'
[PROOF STEP]
from finish
[PROOF STATE]
proof (chain)
picking this:
timing_common_inv 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>
[PROOF STEP]
have NE: "stack s \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
timing_common_inv 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>

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

goal (5 subgoals):
 1. \<And>e. timing_common_inv (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>timing_common_inv 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> timing_common_inv s'
 3. \<And>s s' u e. \<lbrakk>timing_common_inv 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> timing_common_inv s'
 4. \<And>s s' u v e c b. \<lbrakk>timing_common_inv 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); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> timing_common_inv s'
 5. \<And>s s' u v e. \<lbrakk>timing_common_inv 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> timing_common_inv s'
[PROOF STEP]
have *: "hd (stack s) \<notin> dom (finished s)" "hd (stack s) \<in> dom (discovered s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hd (stack s) \<notin> dom (finished s) &&& hd (stack s) \<in> dom (discovered s)
[PROOF STEP]
using stack_not_finished stack_discovered hd_in_set[OF NE]
[PROOF STATE]
proof (prove)
using this:
?x \<in> set (stack s) \<Longrightarrow> ?x \<notin> dom (finished s)
set (stack s) \<subseteq> dom (discovered s)
hd (stack s) \<in> set (stack s)

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

goal (5 subgoals):
 1. \<And>e. timing_common_inv (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>timing_common_inv 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> timing_common_inv s'
 3. \<And>s s' u e. \<lbrakk>timing_common_inv 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> timing_common_inv s'
 4. \<And>s s' u v e c b. \<lbrakk>timing_common_inv 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); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> timing_common_inv s'
 5. \<And>s s' u v e. \<lbrakk>timing_common_inv 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> timing_common_inv s'
[PROOF STEP]
from discovered_closed
[PROOF STATE]
proof (chain)
picking this:
discovered_closed s
[PROOF STEP]
have
      "(E - pending s) `` {hd (stack s)} \<subseteq> dom (discovered s)"
[PROOF STATE]
proof (prove)
using this:
discovered_closed s

goal (1 subgoal):
 1. (E - pending s) `` {hd (stack s)} \<subseteq> dom (discovered s)
[PROOF STEP]
using hd_in_set[OF NE]
[PROOF STATE]
proof (prove)
using this:
discovered_closed s
hd (stack s) \<in> set (stack s)

goal (1 subgoal):
 1. (E - pending s) `` {hd (stack s)} \<subseteq> dom (discovered s)
[PROOF STEP]
by (auto simp add: discovered_closed_def)
[PROOF STATE]
proof (state)
this:
(E - pending s) `` {hd (stack s)} \<subseteq> dom (discovered s)

goal (5 subgoals):
 1. \<And>e. timing_common_inv (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>timing_common_inv 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> timing_common_inv s'
 3. \<And>s s' u e. \<lbrakk>timing_common_inv 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> timing_common_inv s'
 4. \<And>s s' u v e c b. \<lbrakk>timing_common_inv 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); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> timing_common_inv s'
 5. \<And>s s' u v e. \<lbrakk>timing_common_inv 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> timing_common_inv s'
[PROOF STEP]
hence succ_hd: "pending s `` {hd (stack s)} = {}
      \<Longrightarrow> succ (hd (stack s)) \<subseteq> dom (discovered s)"
[PROOF STATE]
proof (prove)
using this:
(E - pending s) `` {hd (stack s)} \<subseteq> dom (discovered s)

goal (1 subgoal):
 1. pending s `` {hd (stack s)} = {} \<Longrightarrow> E `` {hd (stack s)} \<subseteq> dom (discovered s)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
pending s `` {hd (stack s)} = {} \<Longrightarrow> E `` {hd (stack s)} \<subseteq> dom (discovered s)

goal (5 subgoals):
 1. \<And>e. timing_common_inv (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>timing_common_inv 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> timing_common_inv s'
 3. \<And>s s' u e. \<lbrakk>timing_common_inv 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> timing_common_inv s'
 4. \<And>s s' u v e c b. \<lbrakk>timing_common_inv 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); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> timing_common_inv s'
 5. \<And>s s' u v e. \<lbrakk>timing_common_inv 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> timing_common_inv s'
[PROOF STEP]
from finish
[PROOF STATE]
proof (chain)
picking this:
timing_common_inv 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>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
timing_common_inv 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>

goal (1 subgoal):
 1. timing_common_inv s'
[PROOF STEP]
apply (simp add: timing_common_inv_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>); stack s \<noteq> []; pending s `` {hd (stack s)} = {}; u_ = hd (stack s); s' = finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>\<rbrakk> \<Longrightarrow> \<delta> s (hd (stack s)) < counter s \<and> (hd (stack s) \<in> dom (finished s) \<longrightarrow> \<delta> s (hd (stack s)) < counter s) \<and> (\<forall>w\<in>dom (finished s). hd (stack s) \<noteq> w \<longrightarrow> counter s \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (finished s). (v = hd (stack s) \<longrightarrow> (\<forall>w\<in>dom (finished s). hd (stack s) \<noteq> w \<longrightarrow> counter s \<noteq> \<phi> s w)) \<and> (v \<noteq> hd (stack s) \<longrightarrow> \<phi> s v \<noteq> counter s \<and> (hd (stack s) \<in> dom (finished s) \<longrightarrow> \<phi> s v \<noteq> counter s))) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < Suc (counter s)) \<and> (\<forall>v\<in>dom (finished s). v \<noteq> hd (stack s) \<longrightarrow> \<phi> s v < Suc (counter s)) \<and> (\<forall>w\<in>E `` {hd (stack s)}. \<delta> s w < counter s) \<and> (hd (stack s) \<in> dom (finished s) \<longrightarrow> (\<forall>w\<in>E `` {hd (stack s)}. \<delta> s w < counter s))
[PROOF STEP]
apply (intro conjI)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>); stack s \<noteq> []; pending s `` {hd (stack s)} = {}; u_ = hd (stack s); s' = finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>\<rbrakk> \<Longrightarrow> \<delta> s (hd (stack s)) < counter s
 2. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>); stack s \<noteq> []; pending s `` {hd (stack s)} = {}; u_ = hd (stack s); s' = finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>\<rbrakk> \<Longrightarrow> hd (stack s) \<in> dom (finished s) \<longrightarrow> \<delta> s (hd (stack s)) < counter s
 3. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>); stack s \<noteq> []; pending s `` {hd (stack s)} = {}; u_ = hd (stack s); s' = finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>\<rbrakk> \<Longrightarrow> \<forall>w\<in>dom (finished s). hd (stack s) \<noteq> w \<longrightarrow> counter s \<noteq> \<phi> s w
 4. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>); stack s \<noteq> []; pending s `` {hd (stack s)} = {}; u_ = hd (stack s); s' = finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (finished s). (v = hd (stack s) \<longrightarrow> (\<forall>w\<in>dom (finished s). hd (stack s) \<noteq> w \<longrightarrow> counter s \<noteq> \<phi> s w)) \<and> (v \<noteq> hd (stack s) \<longrightarrow> \<phi> s v \<noteq> counter s \<and> (hd (stack s) \<in> dom (finished s) \<longrightarrow> \<phi> s v \<noteq> counter s))
 5. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>); stack s \<noteq> []; pending s `` {hd (stack s)} = {}; u_ = hd (stack s); s' = finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (discovered s). \<delta> s v < Suc (counter s)
 6. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>); stack s \<noteq> []; pending s `` {hd (stack s)} = {}; u_ = hd (stack s); s' = finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (finished s). v \<noteq> hd (stack s) \<longrightarrow> \<phi> s v < Suc (counter s)
 7. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>); stack s \<noteq> []; pending s `` {hd (stack s)} = {}; u_ = hd (stack s); s' = finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>\<rbrakk> \<Longrightarrow> \<forall>w\<in>E `` {hd (stack s)}. \<delta> s w < counter s
 8. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>); stack s \<noteq> []; pending s `` {hd (stack s)} = {}; u_ = hd (stack s); s' = finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>\<rbrakk> \<Longrightarrow> hd (stack s) \<in> dom (finished s) \<longrightarrow> (\<forall>w\<in>E `` {hd (stack s)}. \<delta> s w < counter s)
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
hd (stack s) \<notin> dom (finished s)
hd (stack s) \<in> dom (discovered s)

goal (8 subgoals):
 1. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>); stack s \<noteq> []; pending s `` {hd (stack s)} = {}; u_ = hd (stack s); s' = finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>\<rbrakk> \<Longrightarrow> \<delta> s (hd (stack s)) < counter s
 2. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>); stack s \<noteq> []; pending s `` {hd (stack s)} = {}; u_ = hd (stack s); s' = finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>\<rbrakk> \<Longrightarrow> hd (stack s) \<in> dom (finished s) \<longrightarrow> \<delta> s (hd (stack s)) < counter s
 3. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>); stack s \<noteq> []; pending s `` {hd (stack s)} = {}; u_ = hd (stack s); s' = finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>\<rbrakk> \<Longrightarrow> \<forall>w\<in>dom (finished s). hd (stack s) \<noteq> w \<longrightarrow> counter s \<noteq> \<phi> s w
 4. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>); stack s \<noteq> []; pending s `` {hd (stack s)} = {}; u_ = hd (stack s); s' = finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (finished s). (v = hd (stack s) \<longrightarrow> (\<forall>w\<in>dom (finished s). hd (stack s) \<noteq> w \<longrightarrow> counter s \<noteq> \<phi> s w)) \<and> (v \<noteq> hd (stack s) \<longrightarrow> \<phi> s v \<noteq> counter s \<and> (hd (stack s) \<in> dom (finished s) \<longrightarrow> \<phi> s v \<noteq> counter s))
 5. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>); stack s \<noteq> []; pending s `` {hd (stack s)} = {}; u_ = hd (stack s); s' = finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (discovered s). \<delta> s v < Suc (counter s)
 6. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>); stack s \<noteq> []; pending s `` {hd (stack s)} = {}; u_ = hd (stack s); s' = finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (finished s). v \<noteq> hd (stack s) \<longrightarrow> \<phi> s v < Suc (counter s)
 7. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>); stack s \<noteq> []; pending s `` {hd (stack s)} = {}; u_ = hd (stack s); s' = finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>\<rbrakk> \<Longrightarrow> \<forall>w\<in>E `` {hd (stack s)}. \<delta> s w < counter s
 8. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>); stack s \<noteq> []; pending s `` {hd (stack s)} = {}; u_ = hd (stack s); s' = finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>\<rbrakk> \<Longrightarrow> hd (stack s) \<in> dom (finished s) \<longrightarrow> (\<forall>w\<in>E `` {hd (stack s)}. \<delta> s w < counter s)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>); stack s \<noteq> []; pending s `` {hd (stack s)} = {}; u_ = hd (stack s); s' = finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>\<rbrakk> \<Longrightarrow> hd (stack s) \<in> dom (finished s) \<longrightarrow> \<delta> s (hd (stack s)) < counter s
 2. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>); stack s \<noteq> []; pending s `` {hd (stack s)} = {}; u_ = hd (stack s); s' = finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>\<rbrakk> \<Longrightarrow> \<forall>w\<in>dom (finished s). hd (stack s) \<noteq> w \<longrightarrow> counter s \<noteq> \<phi> s w
 3. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>); stack s \<noteq> []; pending s `` {hd (stack s)} = {}; u_ = hd (stack s); s' = finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (finished s). (v = hd (stack s) \<longrightarrow> (\<forall>w\<in>dom (finished s). hd (stack s) \<noteq> w \<longrightarrow> counter s \<noteq> \<phi> s w)) \<and> (v \<noteq> hd (stack s) \<longrightarrow> \<phi> s v \<noteq> counter s \<and> (hd (stack s) \<in> dom (finished s) \<longrightarrow> \<phi> s v \<noteq> counter s))
 4. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>); stack s \<noteq> []; pending s `` {hd (stack s)} = {}; u_ = hd (stack s); s' = finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (discovered s). \<delta> s v < Suc (counter s)
 5. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>); stack s \<noteq> []; pending s `` {hd (stack s)} = {}; u_ = hd (stack s); s' = finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (finished s). v \<noteq> hd (stack s) \<longrightarrow> \<phi> s v < Suc (counter s)
 6. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>); stack s \<noteq> []; pending s `` {hd (stack s)} = {}; u_ = hd (stack s); s' = finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>\<rbrakk> \<Longrightarrow> \<forall>w\<in>E `` {hd (stack s)}. \<delta> s w < counter s
 7. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>); stack s \<noteq> []; pending s `` {hd (stack s)} = {}; u_ = hd (stack s); s' = finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>\<rbrakk> \<Longrightarrow> hd (stack s) \<in> dom (finished s) \<longrightarrow> (\<forall>w\<in>E `` {hd (stack s)}. \<delta> s w < counter s)
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
hd (stack s) \<notin> dom (finished s)
hd (stack s) \<in> dom (discovered s)

goal (7 subgoals):
 1. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>); stack s \<noteq> []; pending s `` {hd (stack s)} = {}; u_ = hd (stack s); s' = finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>\<rbrakk> \<Longrightarrow> hd (stack s) \<in> dom (finished s) \<longrightarrow> \<delta> s (hd (stack s)) < counter s
 2. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>); stack s \<noteq> []; pending s `` {hd (stack s)} = {}; u_ = hd (stack s); s' = finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>\<rbrakk> \<Longrightarrow> \<forall>w\<in>dom (finished s). hd (stack s) \<noteq> w \<longrightarrow> counter s \<noteq> \<phi> s w
 3. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>); stack s \<noteq> []; pending s `` {hd (stack s)} = {}; u_ = hd (stack s); s' = finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (finished s). (v = hd (stack s) \<longrightarrow> (\<forall>w\<in>dom (finished s). hd (stack s) \<noteq> w \<longrightarrow> counter s \<noteq> \<phi> s w)) \<and> (v \<noteq> hd (stack s) \<longrightarrow> \<phi> s v \<noteq> counter s \<and> (hd (stack s) \<in> dom (finished s) \<longrightarrow> \<phi> s v \<noteq> counter s))
 4. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>); stack s \<noteq> []; pending s `` {hd (stack s)} = {}; u_ = hd (stack s); s' = finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (discovered s). \<delta> s v < Suc (counter s)
 5. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>); stack s \<noteq> []; pending s `` {hd (stack s)} = {}; u_ = hd (stack s); s' = finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (finished s). v \<noteq> hd (stack s) \<longrightarrow> \<phi> s v < Suc (counter s)
 6. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>); stack s \<noteq> []; pending s `` {hd (stack s)} = {}; u_ = hd (stack s); s' = finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>\<rbrakk> \<Longrightarrow> \<forall>w\<in>E `` {hd (stack s)}. \<delta> s w < counter s
 7. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>); stack s \<noteq> []; pending s `` {hd (stack s)} = {}; u_ = hd (stack s); s' = finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>\<rbrakk> \<Longrightarrow> hd (stack s) \<in> dom (finished s) \<longrightarrow> (\<forall>w\<in>E `` {hd (stack s)}. \<delta> s w < counter s)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>); stack s \<noteq> []; pending s `` {hd (stack s)} = {}; u_ = hd (stack s); s' = finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>\<rbrakk> \<Longrightarrow> \<forall>w\<in>dom (finished s). hd (stack s) \<noteq> w \<longrightarrow> counter s \<noteq> \<phi> s w
 2. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>); stack s \<noteq> []; pending s `` {hd (stack s)} = {}; u_ = hd (stack s); s' = finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (finished s). (v = hd (stack s) \<longrightarrow> (\<forall>w\<in>dom (finished s). hd (stack s) \<noteq> w \<longrightarrow> counter s \<noteq> \<phi> s w)) \<and> (v \<noteq> hd (stack s) \<longrightarrow> \<phi> s v \<noteq> counter s \<and> (hd (stack s) \<in> dom (finished s) \<longrightarrow> \<phi> s v \<noteq> counter s))
 3. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>); stack s \<noteq> []; pending s `` {hd (stack s)} = {}; u_ = hd (stack s); s' = finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (discovered s). \<delta> s v < Suc (counter s)
 4. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>); stack s \<noteq> []; pending s `` {hd (stack s)} = {}; u_ = hd (stack s); s' = finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (finished s). v \<noteq> hd (stack s) \<longrightarrow> \<phi> s v < Suc (counter s)
 5. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>); stack s \<noteq> []; pending s `` {hd (stack s)} = {}; u_ = hd (stack s); s' = finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>\<rbrakk> \<Longrightarrow> \<forall>w\<in>E `` {hd (stack s)}. \<delta> s w < counter s
 6. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>); stack s \<noteq> []; pending s `` {hd (stack s)} = {}; u_ = hd (stack s); s' = finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>\<rbrakk> \<Longrightarrow> hd (stack s) \<in> dom (finished s) \<longrightarrow> (\<forall>w\<in>E `` {hd (stack s)}. \<delta> s w < counter s)
[PROOF STEP]
apply (metis less_irrefl)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>); stack s \<noteq> []; pending s `` {hd (stack s)} = {}; u_ = hd (stack s); s' = finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (finished s). (v = hd (stack s) \<longrightarrow> (\<forall>w\<in>dom (finished s). hd (stack s) \<noteq> w \<longrightarrow> counter s \<noteq> \<phi> s w)) \<and> (v \<noteq> hd (stack s) \<longrightarrow> \<phi> s v \<noteq> counter s \<and> (hd (stack s) \<in> dom (finished s) \<longrightarrow> \<phi> s v \<noteq> counter s))
 2. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>); stack s \<noteq> []; pending s `` {hd (stack s)} = {}; u_ = hd (stack s); s' = finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (discovered s). \<delta> s v < Suc (counter s)
 3. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>); stack s \<noteq> []; pending s `` {hd (stack s)} = {}; u_ = hd (stack s); s' = finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (finished s). v \<noteq> hd (stack s) \<longrightarrow> \<phi> s v < Suc (counter s)
 4. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>); stack s \<noteq> []; pending s `` {hd (stack s)} = {}; u_ = hd (stack s); s' = finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>\<rbrakk> \<Longrightarrow> \<forall>w\<in>E `` {hd (stack s)}. \<delta> s w < counter s
 5. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>); stack s \<noteq> []; pending s `` {hd (stack s)} = {}; u_ = hd (stack s); s' = finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>\<rbrakk> \<Longrightarrow> hd (stack s) \<in> dom (finished s) \<longrightarrow> (\<forall>w\<in>E `` {hd (stack s)}. \<delta> s w < counter s)
[PROOF STEP]
apply (metis less_irrefl)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>); stack s \<noteq> []; pending s `` {hd (stack s)} = {}; u_ = hd (stack s); s' = finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (discovered s). \<delta> s v < Suc (counter s)
 2. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>); stack s \<noteq> []; pending s `` {hd (stack s)} = {}; u_ = hd (stack s); s' = finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (finished s). v \<noteq> hd (stack s) \<longrightarrow> \<phi> s v < Suc (counter s)
 3. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>); stack s \<noteq> []; pending s `` {hd (stack s)} = {}; u_ = hd (stack s); s' = finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>\<rbrakk> \<Longrightarrow> \<forall>w\<in>E `` {hd (stack s)}. \<delta> s w < counter s
 4. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>); stack s \<noteq> []; pending s `` {hd (stack s)} = {}; u_ = hd (stack s); s' = finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>\<rbrakk> \<Longrightarrow> hd (stack s) \<in> dom (finished s) \<longrightarrow> (\<forall>w\<in>E `` {hd (stack s)}. \<delta> s w < counter s)
[PROOF STEP]
apply (metis less_SucI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>); stack s \<noteq> []; pending s `` {hd (stack s)} = {}; u_ = hd (stack s); s' = finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (finished s). v \<noteq> hd (stack s) \<longrightarrow> \<phi> s v < Suc (counter s)
 2. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>); stack s \<noteq> []; pending s `` {hd (stack s)} = {}; u_ = hd (stack s); s' = finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>\<rbrakk> \<Longrightarrow> \<forall>w\<in>E `` {hd (stack s)}. \<delta> s w < counter s
 3. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>); stack s \<noteq> []; pending s `` {hd (stack s)} = {}; u_ = hd (stack s); s' = finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>\<rbrakk> \<Longrightarrow> hd (stack s) \<in> dom (finished s) \<longrightarrow> (\<forall>w\<in>E `` {hd (stack s)}. \<delta> s w < counter s)
[PROOF STEP]
apply (metis less_SucI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>); stack s \<noteq> []; pending s `` {hd (stack s)} = {}; u_ = hd (stack s); s' = finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>\<rbrakk> \<Longrightarrow> \<forall>w\<in>E `` {hd (stack s)}. \<delta> s w < counter s
 2. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>); stack s \<noteq> []; pending s `` {hd (stack s)} = {}; u_ = hd (stack s); s' = finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>\<rbrakk> \<Longrightarrow> hd (stack s) \<in> dom (finished s) \<longrightarrow> (\<forall>w\<in>E `` {hd (stack s)}. \<delta> s w < counter s)
[PROOF STEP]
apply (blast dest!: succ_hd)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>); stack s \<noteq> []; pending s `` {hd (stack s)} = {}; u_ = hd (stack s); s' = finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>\<rbrakk> \<Longrightarrow> hd (stack s) \<in> dom (finished s) \<longrightarrow> (\<forall>w\<in>E `` {hd (stack s)}. \<delta> s w < counter s)
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
hd (stack s) \<notin> dom (finished s)
hd (stack s) \<in> dom (discovered s)

goal (1 subgoal):
 1. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>); stack s \<noteq> []; pending s `` {hd (stack s)} = {}; u_ = hd (stack s); s' = finish (hd (stack s)) s\<lparr>state.more := e_\<rparr>\<rbrakk> \<Longrightarrow> hd (stack s) \<in> dom (finished s) \<longrightarrow> (\<forall>w\<in>E `` {hd (stack s)}. \<delta> s w < counter s)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
timing_common_inv s'

goal (4 subgoals):
 1. \<And>e. timing_common_inv (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>timing_common_inv 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> timing_common_inv s'
 3. \<And>s s' u v e c b. \<lbrakk>timing_common_inv 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); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> timing_common_inv s'
 4. \<And>s s' u v e. \<lbrakk>timing_common_inv 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> timing_common_inv s'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>e. timing_common_inv (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>timing_common_inv 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> timing_common_inv s'
 3. \<And>s s' u v e c b. \<lbrakk>timing_common_inv 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); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> timing_common_inv s'
 4. \<And>s s' u v e. \<lbrakk>timing_common_inv 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> timing_common_inv s'
[PROOF STEP]
case (discover s)
[PROOF STATE]
proof (state)
this:
timing_common_inv s
cond s
DFS_invar G param s
DFS_invar G param s'_
s'_ = discover u_ v_ (s\<lparr>pending := pending s - {(u_, v_)}\<rparr>)\<lparr>state.more := e_\<rparr>
stack s \<noteq> []
v_ \<in> pending s `` {u_}
v_ \<notin> dom (discovered s)
u_ = hd (stack s)

goal (4 subgoals):
 1. \<And>e. timing_common_inv (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>timing_common_inv 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> timing_common_inv s'
 3. \<And>s s' u v e c b. \<lbrakk>timing_common_inv 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); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> timing_common_inv s'
 4. \<And>s s' u v e. \<lbrakk>timing_common_inv 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> timing_common_inv s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
timing_common_inv s
cond s
DFS_invar G param s
DFS_invar G param s'_
s'_ = discover u_ v_ (s\<lparr>pending := pending s - {(u_, v_)}\<rparr>)\<lparr>state.more := e_\<rparr>
stack s \<noteq> []
v_ \<in> pending s `` {u_}
v_ \<notin> dom (discovered s)
u_ = hd (stack s)
[PROOF STEP]
interpret DFS_invar where s=s
[PROOF STATE]
proof (prove)
using this:
timing_common_inv s
cond s
DFS_invar G param s
DFS_invar G param s'_
s'_ = discover u_ v_ (s\<lparr>pending := pending s - {(u_, v_)}\<rparr>)\<lparr>state.more := e_\<rparr>
stack s \<noteq> []
v_ \<in> pending s `` {u_}
v_ \<notin> dom (discovered s)
u_ = hd (stack s)

goal (1 subgoal):
 1. DFS_invar G param s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>e. timing_common_inv (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>timing_common_inv 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> timing_common_inv s'
 3. \<And>s s' u v e c b. \<lbrakk>timing_common_inv 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); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> timing_common_inv s'
 4. \<And>s s' u v e. \<lbrakk>timing_common_inv 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> timing_common_inv s'
[PROOF STEP]
from discover
[PROOF STATE]
proof (chain)
picking this:
timing_common_inv s
cond s
DFS_invar G param s
DFS_invar G param s'_
s'_ = discover u_ v_ (s\<lparr>pending := pending s - {(u_, v_)}\<rparr>)\<lparr>state.more := e_\<rparr>
stack s \<noteq> []
v_ \<in> pending s `` {u_}
v_ \<notin> dom (discovered s)
u_ = hd (stack s)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
timing_common_inv s
cond s
DFS_invar G param s
DFS_invar G param s'_
s'_ = discover u_ v_ (s\<lparr>pending := pending s - {(u_, v_)}\<rparr>)\<lparr>state.more := e_\<rparr>
stack s \<noteq> []
v_ \<in> pending s `` {u_}
v_ \<notin> dom (discovered s)
u_ = hd (stack s)

goal (1 subgoal):
 1. timing_common_inv s'_
[PROOF STEP]
apply (simp add: timing_common_inv_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (discover (hd (stack s)) v_ (s\<lparr>pending := pending s - {(hd (stack s), v_)}\<rparr>)\<lparr>state.more := e_\<rparr>); s'_ = discover (hd (stack s)) v_ (s\<lparr>pending := pending s - {(hd (stack s), v_)}\<rparr>)\<lparr>state.more := e_\<rparr>; stack s \<noteq> []; (hd (stack s), v_) \<in> pending s; v_ \<notin> dom (discovered s); u_ = hd (stack s)\<rbrakk> \<Longrightarrow> (v_ \<in> dom (finished s) \<longrightarrow> counter s < \<phi> s v_) \<and> (\<forall>w\<in>dom (discovered s). v_ \<noteq> w \<longrightarrow> counter s \<noteq> \<delta> s w) \<and> (\<forall>va\<in>dom (discovered s). (va = v_ \<longrightarrow> (\<forall>w\<in>dom (discovered s). v_ \<noteq> w \<longrightarrow> counter s \<noteq> \<delta> s w)) \<and> (va \<noteq> v_ \<longrightarrow> \<delta> s va \<noteq> counter s)) \<and> (\<forall>va\<in>dom (discovered s). va \<noteq> v_ \<longrightarrow> \<delta> s va < Suc (counter s)) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < Suc (counter s)) \<and> (\<forall>va\<in>dom (finished s). (va, v_) \<in> E \<longrightarrow> counter s < \<phi> s va)
[PROOF STEP]
apply (intro conjI)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (discover (hd (stack s)) v_ (s\<lparr>pending := pending s - {(hd (stack s), v_)}\<rparr>)\<lparr>state.more := e_\<rparr>); s'_ = discover (hd (stack s)) v_ (s\<lparr>pending := pending s - {(hd (stack s), v_)}\<rparr>)\<lparr>state.more := e_\<rparr>; stack s \<noteq> []; (hd (stack s), v_) \<in> pending s; v_ \<notin> dom (discovered s); u_ = hd (stack s)\<rbrakk> \<Longrightarrow> v_ \<in> dom (finished s) \<longrightarrow> counter s < \<phi> s v_
 2. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (discover (hd (stack s)) v_ (s\<lparr>pending := pending s - {(hd (stack s), v_)}\<rparr>)\<lparr>state.more := e_\<rparr>); s'_ = discover (hd (stack s)) v_ (s\<lparr>pending := pending s - {(hd (stack s), v_)}\<rparr>)\<lparr>state.more := e_\<rparr>; stack s \<noteq> []; (hd (stack s), v_) \<in> pending s; v_ \<notin> dom (discovered s); u_ = hd (stack s)\<rbrakk> \<Longrightarrow> \<forall>w\<in>dom (discovered s). v_ \<noteq> w \<longrightarrow> counter s \<noteq> \<delta> s w
 3. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (discover (hd (stack s)) v_ (s\<lparr>pending := pending s - {(hd (stack s), v_)}\<rparr>)\<lparr>state.more := e_\<rparr>); s'_ = discover (hd (stack s)) v_ (s\<lparr>pending := pending s - {(hd (stack s), v_)}\<rparr>)\<lparr>state.more := e_\<rparr>; stack s \<noteq> []; (hd (stack s), v_) \<in> pending s; v_ \<notin> dom (discovered s); u_ = hd (stack s)\<rbrakk> \<Longrightarrow> \<forall>va\<in>dom (discovered s). (va = v_ \<longrightarrow> (\<forall>w\<in>dom (discovered s). v_ \<noteq> w \<longrightarrow> counter s \<noteq> \<delta> s w)) \<and> (va \<noteq> v_ \<longrightarrow> \<delta> s va \<noteq> counter s)
 4. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (discover (hd (stack s)) v_ (s\<lparr>pending := pending s - {(hd (stack s), v_)}\<rparr>)\<lparr>state.more := e_\<rparr>); s'_ = discover (hd (stack s)) v_ (s\<lparr>pending := pending s - {(hd (stack s), v_)}\<rparr>)\<lparr>state.more := e_\<rparr>; stack s \<noteq> []; (hd (stack s), v_) \<in> pending s; v_ \<notin> dom (discovered s); u_ = hd (stack s)\<rbrakk> \<Longrightarrow> \<forall>va\<in>dom (discovered s). va \<noteq> v_ \<longrightarrow> \<delta> s va < Suc (counter s)
 5. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (discover (hd (stack s)) v_ (s\<lparr>pending := pending s - {(hd (stack s), v_)}\<rparr>)\<lparr>state.more := e_\<rparr>); s'_ = discover (hd (stack s)) v_ (s\<lparr>pending := pending s - {(hd (stack s), v_)}\<rparr>)\<lparr>state.more := e_\<rparr>; stack s \<noteq> []; (hd (stack s), v_) \<in> pending s; v_ \<notin> dom (discovered s); u_ = hd (stack s)\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (finished s). \<phi> s v < Suc (counter s)
 6. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (discover (hd (stack s)) v_ (s\<lparr>pending := pending s - {(hd (stack s), v_)}\<rparr>)\<lparr>state.more := e_\<rparr>); s'_ = discover (hd (stack s)) v_ (s\<lparr>pending := pending s - {(hd (stack s), v_)}\<rparr>)\<lparr>state.more := e_\<rparr>; stack s \<noteq> []; (hd (stack s), v_) \<in> pending s; v_ \<notin> dom (discovered s); u_ = hd (stack s)\<rbrakk> \<Longrightarrow> \<forall>va\<in>dom (finished s). (va, v_) \<in> E \<longrightarrow> counter s < \<phi> s va
[PROOF STEP]
using finished_discovered
[PROOF STATE]
proof (prove)
using this:
dom (finished s) \<subseteq> dom (discovered s)

goal (6 subgoals):
 1. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (discover (hd (stack s)) v_ (s\<lparr>pending := pending s - {(hd (stack s), v_)}\<rparr>)\<lparr>state.more := e_\<rparr>); s'_ = discover (hd (stack s)) v_ (s\<lparr>pending := pending s - {(hd (stack s), v_)}\<rparr>)\<lparr>state.more := e_\<rparr>; stack s \<noteq> []; (hd (stack s), v_) \<in> pending s; v_ \<notin> dom (discovered s); u_ = hd (stack s)\<rbrakk> \<Longrightarrow> v_ \<in> dom (finished s) \<longrightarrow> counter s < \<phi> s v_
 2. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (discover (hd (stack s)) v_ (s\<lparr>pending := pending s - {(hd (stack s), v_)}\<rparr>)\<lparr>state.more := e_\<rparr>); s'_ = discover (hd (stack s)) v_ (s\<lparr>pending := pending s - {(hd (stack s), v_)}\<rparr>)\<lparr>state.more := e_\<rparr>; stack s \<noteq> []; (hd (stack s), v_) \<in> pending s; v_ \<notin> dom (discovered s); u_ = hd (stack s)\<rbrakk> \<Longrightarrow> \<forall>w\<in>dom (discovered s). v_ \<noteq> w \<longrightarrow> counter s \<noteq> \<delta> s w
 3. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (discover (hd (stack s)) v_ (s\<lparr>pending := pending s - {(hd (stack s), v_)}\<rparr>)\<lparr>state.more := e_\<rparr>); s'_ = discover (hd (stack s)) v_ (s\<lparr>pending := pending s - {(hd (stack s), v_)}\<rparr>)\<lparr>state.more := e_\<rparr>; stack s \<noteq> []; (hd (stack s), v_) \<in> pending s; v_ \<notin> dom (discovered s); u_ = hd (stack s)\<rbrakk> \<Longrightarrow> \<forall>va\<in>dom (discovered s). (va = v_ \<longrightarrow> (\<forall>w\<in>dom (discovered s). v_ \<noteq> w \<longrightarrow> counter s \<noteq> \<delta> s w)) \<and> (va \<noteq> v_ \<longrightarrow> \<delta> s va \<noteq> counter s)
 4. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (discover (hd (stack s)) v_ (s\<lparr>pending := pending s - {(hd (stack s), v_)}\<rparr>)\<lparr>state.more := e_\<rparr>); s'_ = discover (hd (stack s)) v_ (s\<lparr>pending := pending s - {(hd (stack s), v_)}\<rparr>)\<lparr>state.more := e_\<rparr>; stack s \<noteq> []; (hd (stack s), v_) \<in> pending s; v_ \<notin> dom (discovered s); u_ = hd (stack s)\<rbrakk> \<Longrightarrow> \<forall>va\<in>dom (discovered s). va \<noteq> v_ \<longrightarrow> \<delta> s va < Suc (counter s)
 5. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (discover (hd (stack s)) v_ (s\<lparr>pending := pending s - {(hd (stack s), v_)}\<rparr>)\<lparr>state.more := e_\<rparr>); s'_ = discover (hd (stack s)) v_ (s\<lparr>pending := pending s - {(hd (stack s), v_)}\<rparr>)\<lparr>state.more := e_\<rparr>; stack s \<noteq> []; (hd (stack s), v_) \<in> pending s; v_ \<notin> dom (discovered s); u_ = hd (stack s)\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (finished s). \<phi> s v < Suc (counter s)
 6. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (discover (hd (stack s)) v_ (s\<lparr>pending := pending s - {(hd (stack s), v_)}\<rparr>)\<lparr>state.more := e_\<rparr>); s'_ = discover (hd (stack s)) v_ (s\<lparr>pending := pending s - {(hd (stack s), v_)}\<rparr>)\<lparr>state.more := e_\<rparr>; stack s \<noteq> []; (hd (stack s), v_) \<in> pending s; v_ \<notin> dom (discovered s); u_ = hd (stack s)\<rbrakk> \<Longrightarrow> \<forall>va\<in>dom (finished s). (va, v_) \<in> E \<longrightarrow> counter s < \<phi> s va
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (discover (hd (stack s)) v_ (s\<lparr>pending := pending s - {(hd (stack s), v_)}\<rparr>)\<lparr>state.more := e_\<rparr>); s'_ = discover (hd (stack s)) v_ (s\<lparr>pending := pending s - {(hd (stack s), v_)}\<rparr>)\<lparr>state.more := e_\<rparr>; stack s \<noteq> []; (hd (stack s), v_) \<in> pending s; v_ \<notin> dom (discovered s); u_ = hd (stack s)\<rbrakk> \<Longrightarrow> \<forall>w\<in>dom (discovered s). v_ \<noteq> w \<longrightarrow> counter s \<noteq> \<delta> s w
 2. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (discover (hd (stack s)) v_ (s\<lparr>pending := pending s - {(hd (stack s), v_)}\<rparr>)\<lparr>state.more := e_\<rparr>); s'_ = discover (hd (stack s)) v_ (s\<lparr>pending := pending s - {(hd (stack s), v_)}\<rparr>)\<lparr>state.more := e_\<rparr>; stack s \<noteq> []; (hd (stack s), v_) \<in> pending s; v_ \<notin> dom (discovered s); u_ = hd (stack s)\<rbrakk> \<Longrightarrow> \<forall>va\<in>dom (discovered s). (va = v_ \<longrightarrow> (\<forall>w\<in>dom (discovered s). v_ \<noteq> w \<longrightarrow> counter s \<noteq> \<delta> s w)) \<and> (va \<noteq> v_ \<longrightarrow> \<delta> s va \<noteq> counter s)
 3. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (discover (hd (stack s)) v_ (s\<lparr>pending := pending s - {(hd (stack s), v_)}\<rparr>)\<lparr>state.more := e_\<rparr>); s'_ = discover (hd (stack s)) v_ (s\<lparr>pending := pending s - {(hd (stack s), v_)}\<rparr>)\<lparr>state.more := e_\<rparr>; stack s \<noteq> []; (hd (stack s), v_) \<in> pending s; v_ \<notin> dom (discovered s); u_ = hd (stack s)\<rbrakk> \<Longrightarrow> \<forall>va\<in>dom (discovered s). va \<noteq> v_ \<longrightarrow> \<delta> s va < Suc (counter s)
 4. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (discover (hd (stack s)) v_ (s\<lparr>pending := pending s - {(hd (stack s), v_)}\<rparr>)\<lparr>state.more := e_\<rparr>); s'_ = discover (hd (stack s)) v_ (s\<lparr>pending := pending s - {(hd (stack s), v_)}\<rparr>)\<lparr>state.more := e_\<rparr>; stack s \<noteq> []; (hd (stack s), v_) \<in> pending s; v_ \<notin> dom (discovered s); u_ = hd (stack s)\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (finished s). \<phi> s v < Suc (counter s)
 5. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (discover (hd (stack s)) v_ (s\<lparr>pending := pending s - {(hd (stack s), v_)}\<rparr>)\<lparr>state.more := e_\<rparr>); s'_ = discover (hd (stack s)) v_ (s\<lparr>pending := pending s - {(hd (stack s), v_)}\<rparr>)\<lparr>state.more := e_\<rparr>; stack s \<noteq> []; (hd (stack s), v_) \<in> pending s; v_ \<notin> dom (discovered s); u_ = hd (stack s)\<rbrakk> \<Longrightarrow> \<forall>va\<in>dom (finished s). (va, v_) \<in> E \<longrightarrow> counter s < \<phi> s va
[PROOF STEP]
apply (metis less_irrefl)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (discover (hd (stack s)) v_ (s\<lparr>pending := pending s - {(hd (stack s), v_)}\<rparr>)\<lparr>state.more := e_\<rparr>); s'_ = discover (hd (stack s)) v_ (s\<lparr>pending := pending s - {(hd (stack s), v_)}\<rparr>)\<lparr>state.more := e_\<rparr>; stack s \<noteq> []; (hd (stack s), v_) \<in> pending s; v_ \<notin> dom (discovered s); u_ = hd (stack s)\<rbrakk> \<Longrightarrow> \<forall>va\<in>dom (discovered s). (va = v_ \<longrightarrow> (\<forall>w\<in>dom (discovered s). v_ \<noteq> w \<longrightarrow> counter s \<noteq> \<delta> s w)) \<and> (va \<noteq> v_ \<longrightarrow> \<delta> s va \<noteq> counter s)
 2. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (discover (hd (stack s)) v_ (s\<lparr>pending := pending s - {(hd (stack s), v_)}\<rparr>)\<lparr>state.more := e_\<rparr>); s'_ = discover (hd (stack s)) v_ (s\<lparr>pending := pending s - {(hd (stack s), v_)}\<rparr>)\<lparr>state.more := e_\<rparr>; stack s \<noteq> []; (hd (stack s), v_) \<in> pending s; v_ \<notin> dom (discovered s); u_ = hd (stack s)\<rbrakk> \<Longrightarrow> \<forall>va\<in>dom (discovered s). va \<noteq> v_ \<longrightarrow> \<delta> s va < Suc (counter s)
 3. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (discover (hd (stack s)) v_ (s\<lparr>pending := pending s - {(hd (stack s), v_)}\<rparr>)\<lparr>state.more := e_\<rparr>); s'_ = discover (hd (stack s)) v_ (s\<lparr>pending := pending s - {(hd (stack s), v_)}\<rparr>)\<lparr>state.more := e_\<rparr>; stack s \<noteq> []; (hd (stack s), v_) \<in> pending s; v_ \<notin> dom (discovered s); u_ = hd (stack s)\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (finished s). \<phi> s v < Suc (counter s)
 4. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (discover (hd (stack s)) v_ (s\<lparr>pending := pending s - {(hd (stack s), v_)}\<rparr>)\<lparr>state.more := e_\<rparr>); s'_ = discover (hd (stack s)) v_ (s\<lparr>pending := pending s - {(hd (stack s), v_)}\<rparr>)\<lparr>state.more := e_\<rparr>; stack s \<noteq> []; (hd (stack s), v_) \<in> pending s; v_ \<notin> dom (discovered s); u_ = hd (stack s)\<rbrakk> \<Longrightarrow> \<forall>va\<in>dom (finished s). (va, v_) \<in> E \<longrightarrow> counter s < \<phi> s va
[PROOF STEP]
apply (metis less_irrefl)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (discover (hd (stack s)) v_ (s\<lparr>pending := pending s - {(hd (stack s), v_)}\<rparr>)\<lparr>state.more := e_\<rparr>); s'_ = discover (hd (stack s)) v_ (s\<lparr>pending := pending s - {(hd (stack s), v_)}\<rparr>)\<lparr>state.more := e_\<rparr>; stack s \<noteq> []; (hd (stack s), v_) \<in> pending s; v_ \<notin> dom (discovered s); u_ = hd (stack s)\<rbrakk> \<Longrightarrow> \<forall>va\<in>dom (discovered s). va \<noteq> v_ \<longrightarrow> \<delta> s va < Suc (counter s)
 2. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (discover (hd (stack s)) v_ (s\<lparr>pending := pending s - {(hd (stack s), v_)}\<rparr>)\<lparr>state.more := e_\<rparr>); s'_ = discover (hd (stack s)) v_ (s\<lparr>pending := pending s - {(hd (stack s), v_)}\<rparr>)\<lparr>state.more := e_\<rparr>; stack s \<noteq> []; (hd (stack s), v_) \<in> pending s; v_ \<notin> dom (discovered s); u_ = hd (stack s)\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (finished s). \<phi> s v < Suc (counter s)
 3. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (discover (hd (stack s)) v_ (s\<lparr>pending := pending s - {(hd (stack s), v_)}\<rparr>)\<lparr>state.more := e_\<rparr>); s'_ = discover (hd (stack s)) v_ (s\<lparr>pending := pending s - {(hd (stack s), v_)}\<rparr>)\<lparr>state.more := e_\<rparr>; stack s \<noteq> []; (hd (stack s), v_) \<in> pending s; v_ \<notin> dom (discovered s); u_ = hd (stack s)\<rbrakk> \<Longrightarrow> \<forall>va\<in>dom (finished s). (va, v_) \<in> E \<longrightarrow> counter s < \<phi> s va
[PROOF STEP]
apply (metis less_SucI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (discover (hd (stack s)) v_ (s\<lparr>pending := pending s - {(hd (stack s), v_)}\<rparr>)\<lparr>state.more := e_\<rparr>); s'_ = discover (hd (stack s)) v_ (s\<lparr>pending := pending s - {(hd (stack s), v_)}\<rparr>)\<lparr>state.more := e_\<rparr>; stack s \<noteq> []; (hd (stack s), v_) \<in> pending s; v_ \<notin> dom (discovered s); u_ = hd (stack s)\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (finished s). \<phi> s v < Suc (counter s)
 2. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (discover (hd (stack s)) v_ (s\<lparr>pending := pending s - {(hd (stack s), v_)}\<rparr>)\<lparr>state.more := e_\<rparr>); s'_ = discover (hd (stack s)) v_ (s\<lparr>pending := pending s - {(hd (stack s), v_)}\<rparr>)\<lparr>state.more := e_\<rparr>; stack s \<noteq> []; (hd (stack s), v_) \<in> pending s; v_ \<notin> dom (discovered s); u_ = hd (stack s)\<rbrakk> \<Longrightarrow> \<forall>va\<in>dom (finished s). (va, v_) \<in> E \<longrightarrow> counter s < \<phi> s va
[PROOF STEP]
apply (metis less_SucI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (discover (hd (stack s)) v_ (s\<lparr>pending := pending s - {(hd (stack s), v_)}\<rparr>)\<lparr>state.more := e_\<rparr>); s'_ = discover (hd (stack s)) v_ (s\<lparr>pending := pending s - {(hd (stack s), v_)}\<rparr>)\<lparr>state.more := e_\<rparr>; stack s \<noteq> []; (hd (stack s), v_) \<in> pending s; v_ \<notin> dom (discovered s); u_ = hd (stack s)\<rbrakk> \<Longrightarrow> \<forall>va\<in>dom (finished s). (va, v_) \<in> E \<longrightarrow> counter s < \<phi> s va
[PROOF STEP]
using finished_imp_succ_discovered
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?v \<in> dom (finished s); ?w \<in> E `` {?v}\<rbrakk> \<Longrightarrow> ?w \<in> dom (discovered s)

goal (1 subgoal):
 1. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (discover (hd (stack s)) v_ (s\<lparr>pending := pending s - {(hd (stack s), v_)}\<rparr>)\<lparr>state.more := e_\<rparr>); s'_ = discover (hd (stack s)) v_ (s\<lparr>pending := pending s - {(hd (stack s), v_)}\<rparr>)\<lparr>state.more := e_\<rparr>; stack s \<noteq> []; (hd (stack s), v_) \<in> pending s; v_ \<notin> dom (discovered s); u_ = hd (stack s)\<rbrakk> \<Longrightarrow> \<forall>va\<in>dom (finished s). (va, v_) \<in> E \<longrightarrow> counter s < \<phi> s va
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
timing_common_inv s'_

goal (3 subgoals):
 1. \<And>e. timing_common_inv (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>timing_common_inv 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> timing_common_inv s'
 3. \<And>s s' u v e c b. \<lbrakk>timing_common_inv 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); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> timing_common_inv s'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>e. timing_common_inv (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>timing_common_inv 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> timing_common_inv s'
 3. \<And>s s' u v e c b. \<lbrakk>timing_common_inv 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); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> timing_common_inv s'
[PROOF STEP]
case (new_root s s' v0)
[PROOF STATE]
proof (state)
this:
timing_common_inv s
cond s
DFS_invar G param s
DFS_invar G param s'
v0 \<in> V0
s' = new_root v0 s\<lparr>state.more := e_\<rparr>
stack s = []
v0 \<notin> dom (discovered s)

goal (3 subgoals):
 1. \<And>e. timing_common_inv (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>timing_common_inv 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> timing_common_inv s'
 3. \<And>s s' u v e c b. \<lbrakk>timing_common_inv 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); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> timing_common_inv s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
timing_common_inv s
cond s
DFS_invar G param s
DFS_invar G param s'
v0 \<in> V0
s' = new_root v0 s\<lparr>state.more := e_\<rparr>
stack s = []
v0 \<notin> dom (discovered s)
[PROOF STEP]
interpret DFS_invar where s=s
[PROOF STATE]
proof (prove)
using this:
timing_common_inv s
cond s
DFS_invar G param s
DFS_invar G param s'
v0 \<in> V0
s' = new_root v0 s\<lparr>state.more := e_\<rparr>
stack s = []
v0 \<notin> dom (discovered s)

goal (1 subgoal):
 1. DFS_invar G param s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>e. timing_common_inv (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>timing_common_inv 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> timing_common_inv s'
 3. \<And>s s' u v e c b. \<lbrakk>timing_common_inv 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); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> timing_common_inv s'
[PROOF STEP]
from new_root
[PROOF STATE]
proof (chain)
picking this:
timing_common_inv s
cond s
DFS_invar G param s
DFS_invar G param s'
v0 \<in> V0
s' = new_root v0 s\<lparr>state.more := e_\<rparr>
stack s = []
v0 \<notin> dom (discovered s)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
timing_common_inv s
cond s
DFS_invar G param s
DFS_invar G param s'
v0 \<in> V0
s' = new_root v0 s\<lparr>state.more := e_\<rparr>
stack s = []
v0 \<notin> dom (discovered s)

goal (1 subgoal):
 1. timing_common_inv s'
[PROOF STEP]
apply (simp add: timing_common_inv_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (new_root v0 s\<lparr>state.more := e_\<rparr>); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e_\<rparr>; stack s = []; v0 \<notin> dom (discovered s)\<rbrakk> \<Longrightarrow> (v0 \<in> dom (finished s) \<longrightarrow> counter s < \<phi> s v0) \<and> (\<forall>w\<in>dom (discovered s). v0 \<noteq> w \<longrightarrow> counter s \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (discovered s). (v = v0 \<longrightarrow> (\<forall>w\<in>dom (discovered s). v0 \<noteq> w \<longrightarrow> counter s \<noteq> \<delta> s w)) \<and> (v \<noteq> v0 \<longrightarrow> \<delta> s v \<noteq> counter s)) \<and> (\<forall>v\<in>dom (discovered s). v \<noteq> v0 \<longrightarrow> \<delta> s v < Suc (counter s)) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < Suc (counter s)) \<and> (\<forall>v\<in>dom (finished s). (v, v0) \<in> E \<longrightarrow> counter s < \<phi> s v)
[PROOF STEP]
apply (intro conjI)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (new_root v0 s\<lparr>state.more := e_\<rparr>); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e_\<rparr>; stack s = []; v0 \<notin> dom (discovered s)\<rbrakk> \<Longrightarrow> v0 \<in> dom (finished s) \<longrightarrow> counter s < \<phi> s v0
 2. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (new_root v0 s\<lparr>state.more := e_\<rparr>); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e_\<rparr>; stack s = []; v0 \<notin> dom (discovered s)\<rbrakk> \<Longrightarrow> \<forall>w\<in>dom (discovered s). v0 \<noteq> w \<longrightarrow> counter s \<noteq> \<delta> s w
 3. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (new_root v0 s\<lparr>state.more := e_\<rparr>); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e_\<rparr>; stack s = []; v0 \<notin> dom (discovered s)\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (discovered s). (v = v0 \<longrightarrow> (\<forall>w\<in>dom (discovered s). v0 \<noteq> w \<longrightarrow> counter s \<noteq> \<delta> s w)) \<and> (v \<noteq> v0 \<longrightarrow> \<delta> s v \<noteq> counter s)
 4. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (new_root v0 s\<lparr>state.more := e_\<rparr>); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e_\<rparr>; stack s = []; v0 \<notin> dom (discovered s)\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (discovered s). v \<noteq> v0 \<longrightarrow> \<delta> s v < Suc (counter s)
 5. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (new_root v0 s\<lparr>state.more := e_\<rparr>); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e_\<rparr>; stack s = []; v0 \<notin> dom (discovered s)\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (finished s). \<phi> s v < Suc (counter s)
 6. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (new_root v0 s\<lparr>state.more := e_\<rparr>); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e_\<rparr>; stack s = []; v0 \<notin> dom (discovered s)\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (finished s). (v, v0) \<in> E \<longrightarrow> counter s < \<phi> s v
[PROOF STEP]
using finished_discovered
[PROOF STATE]
proof (prove)
using this:
dom (finished s) \<subseteq> dom (discovered s)

goal (6 subgoals):
 1. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (new_root v0 s\<lparr>state.more := e_\<rparr>); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e_\<rparr>; stack s = []; v0 \<notin> dom (discovered s)\<rbrakk> \<Longrightarrow> v0 \<in> dom (finished s) \<longrightarrow> counter s < \<phi> s v0
 2. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (new_root v0 s\<lparr>state.more := e_\<rparr>); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e_\<rparr>; stack s = []; v0 \<notin> dom (discovered s)\<rbrakk> \<Longrightarrow> \<forall>w\<in>dom (discovered s). v0 \<noteq> w \<longrightarrow> counter s \<noteq> \<delta> s w
 3. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (new_root v0 s\<lparr>state.more := e_\<rparr>); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e_\<rparr>; stack s = []; v0 \<notin> dom (discovered s)\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (discovered s). (v = v0 \<longrightarrow> (\<forall>w\<in>dom (discovered s). v0 \<noteq> w \<longrightarrow> counter s \<noteq> \<delta> s w)) \<and> (v \<noteq> v0 \<longrightarrow> \<delta> s v \<noteq> counter s)
 4. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (new_root v0 s\<lparr>state.more := e_\<rparr>); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e_\<rparr>; stack s = []; v0 \<notin> dom (discovered s)\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (discovered s). v \<noteq> v0 \<longrightarrow> \<delta> s v < Suc (counter s)
 5. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (new_root v0 s\<lparr>state.more := e_\<rparr>); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e_\<rparr>; stack s = []; v0 \<notin> dom (discovered s)\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (finished s). \<phi> s v < Suc (counter s)
 6. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (new_root v0 s\<lparr>state.more := e_\<rparr>); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e_\<rparr>; stack s = []; v0 \<notin> dom (discovered s)\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (finished s). (v, v0) \<in> E \<longrightarrow> counter s < \<phi> s v
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (new_root v0 s\<lparr>state.more := e_\<rparr>); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e_\<rparr>; stack s = []; v0 \<notin> dom (discovered s)\<rbrakk> \<Longrightarrow> \<forall>w\<in>dom (discovered s). v0 \<noteq> w \<longrightarrow> counter s \<noteq> \<delta> s w
 2. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (new_root v0 s\<lparr>state.more := e_\<rparr>); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e_\<rparr>; stack s = []; v0 \<notin> dom (discovered s)\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (discovered s). (v = v0 \<longrightarrow> (\<forall>w\<in>dom (discovered s). v0 \<noteq> w \<longrightarrow> counter s \<noteq> \<delta> s w)) \<and> (v \<noteq> v0 \<longrightarrow> \<delta> s v \<noteq> counter s)
 3. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (new_root v0 s\<lparr>state.more := e_\<rparr>); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e_\<rparr>; stack s = []; v0 \<notin> dom (discovered s)\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (discovered s). v \<noteq> v0 \<longrightarrow> \<delta> s v < Suc (counter s)
 4. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (new_root v0 s\<lparr>state.more := e_\<rparr>); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e_\<rparr>; stack s = []; v0 \<notin> dom (discovered s)\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (finished s). \<phi> s v < Suc (counter s)
 5. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (new_root v0 s\<lparr>state.more := e_\<rparr>); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e_\<rparr>; stack s = []; v0 \<notin> dom (discovered s)\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (finished s). (v, v0) \<in> E \<longrightarrow> counter s < \<phi> s v
[PROOF STEP]
apply (metis less_irrefl)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (new_root v0 s\<lparr>state.more := e_\<rparr>); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e_\<rparr>; stack s = []; v0 \<notin> dom (discovered s)\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (discovered s). (v = v0 \<longrightarrow> (\<forall>w\<in>dom (discovered s). v0 \<noteq> w \<longrightarrow> counter s \<noteq> \<delta> s w)) \<and> (v \<noteq> v0 \<longrightarrow> \<delta> s v \<noteq> counter s)
 2. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (new_root v0 s\<lparr>state.more := e_\<rparr>); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e_\<rparr>; stack s = []; v0 \<notin> dom (discovered s)\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (discovered s). v \<noteq> v0 \<longrightarrow> \<delta> s v < Suc (counter s)
 3. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (new_root v0 s\<lparr>state.more := e_\<rparr>); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e_\<rparr>; stack s = []; v0 \<notin> dom (discovered s)\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (finished s). \<phi> s v < Suc (counter s)
 4. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (new_root v0 s\<lparr>state.more := e_\<rparr>); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e_\<rparr>; stack s = []; v0 \<notin> dom (discovered s)\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (finished s). (v, v0) \<in> E \<longrightarrow> counter s < \<phi> s v
[PROOF STEP]
apply (metis less_irrefl)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (new_root v0 s\<lparr>state.more := e_\<rparr>); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e_\<rparr>; stack s = []; v0 \<notin> dom (discovered s)\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (discovered s). v \<noteq> v0 \<longrightarrow> \<delta> s v < Suc (counter s)
 2. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (new_root v0 s\<lparr>state.more := e_\<rparr>); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e_\<rparr>; stack s = []; v0 \<notin> dom (discovered s)\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (finished s). \<phi> s v < Suc (counter s)
 3. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (new_root v0 s\<lparr>state.more := e_\<rparr>); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e_\<rparr>; stack s = []; v0 \<notin> dom (discovered s)\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (finished s). (v, v0) \<in> E \<longrightarrow> counter s < \<phi> s v
[PROOF STEP]
apply (metis less_SucI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (new_root v0 s\<lparr>state.more := e_\<rparr>); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e_\<rparr>; stack s = []; v0 \<notin> dom (discovered s)\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (finished s). \<phi> s v < Suc (counter s)
 2. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (new_root v0 s\<lparr>state.more := e_\<rparr>); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e_\<rparr>; stack s = []; v0 \<notin> dom (discovered s)\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (finished s). (v, v0) \<in> E \<longrightarrow> counter s < \<phi> s v
[PROOF STEP]
apply (metis less_SucI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (new_root v0 s\<lparr>state.more := e_\<rparr>); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e_\<rparr>; stack s = []; v0 \<notin> dom (discovered s)\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (finished s). (v, v0) \<in> E \<longrightarrow> counter s < \<phi> s v
[PROOF STEP]
using finished_imp_succ_discovered
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?v \<in> dom (finished s); ?w \<in> E `` {?v}\<rbrakk> \<Longrightarrow> ?w \<in> dom (discovered s)

goal (1 subgoal):
 1. \<lbrakk>(\<forall>v\<in>dom (finished s). \<delta> s v < \<phi> s v) \<and> (\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). v \<noteq> w \<longrightarrow> \<delta> s v \<noteq> \<delta> s w) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>dom (finished s). v \<noteq> w \<longrightarrow> \<phi> s v \<noteq> \<phi> s w) \<and> (\<forall>v\<in>dom (discovered s). \<delta> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<phi> s v < counter s) \<and> (\<forall>v\<in>dom (finished s). \<forall>w\<in>E `` {v}. \<delta> s w < \<phi> s v); cond s; DFS_invar G param s; DFS_invar G param (new_root v0 s\<lparr>state.more := e_\<rparr>); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e_\<rparr>; stack s = []; v0 \<notin> dom (discovered s)\<rbrakk> \<Longrightarrow> \<forall>v\<in>dom (finished s). (v, v0) \<in> E \<longrightarrow> counter s < \<phi> s v
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
timing_common_inv s'

goal (2 subgoals):
 1. \<And>e. timing_common_inv (empty_state e)
 2. \<And>s s' u v e c b. \<lbrakk>timing_common_inv 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); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> timing_common_inv s'
[PROOF STEP]
qed (simp_all add: timing_common_inv_def)