[STATEMENT]
lemma timing_less_counter:
    "v \<in> dom (discovered s) \<Longrightarrow> \<delta> s v < counter s"
    "v \<in> dom (finished s) \<Longrightarrow> \<phi> s v < counter s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (v \<in> dom (discovered s) \<Longrightarrow> \<delta> s v < counter s) &&& (v \<in> dom (finished s) \<Longrightarrow> \<phi> s v < counter s)
[PROOF STEP]
using s_timing_common_inv
[PROOF STATE]
proof (prove)
using this:
timing_common_inv s

goal (1 subgoal):
 1. (v \<in> dom (discovered s) \<Longrightarrow> \<delta> s v < counter s) &&& (v \<in> dom (finished s) \<Longrightarrow> \<phi> s v < counter s)
[PROOF STEP]
by (auto simp add: timing_common_inv_def)


[STATEMENT]
lemma disc_lt_fin:
    "v \<in> dom (finished s) \<Longrightarrow> \<delta> s v < \<phi> s v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> dom (finished s) \<Longrightarrow> \<delta> s v < \<phi> s v
[PROOF STEP]
using s_timing_common_inv
[PROOF STATE]
proof (prove)
using this:
timing_common_inv s

goal (1 subgoal):
 1. v \<in> dom (finished s) \<Longrightarrow> \<delta> s v < \<phi> s v
[PROOF STEP]
by (auto simp add: timing_common_inv_def)


[STATEMENT]
lemma disc_unequal:
    assumes "v \<in> dom (discovered s)" "w \<in> dom (discovered s)"
    and "v \<noteq> w"
    shows "\<delta> s v \<noteq> \<delta> s w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<delta> s v \<noteq> \<delta> s w
[PROOF STEP]
using s_timing_common_inv assms
[PROOF STATE]
proof (prove)
using this:
timing_common_inv s
v \<in> dom (discovered s)
w \<in> dom (discovered s)
v \<noteq> w

goal (1 subgoal):
 1. \<delta> s v \<noteq> \<delta> s w
[PROOF STEP]
by (auto simp add: timing_common_inv_def)


[STATEMENT]
lemma fin_unequal:
    assumes "v \<in> dom (finished s)" "w \<in> dom (finished s)"
    and "v \<noteq> w"
    shows "\<phi> s v \<noteq> \<phi> s w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> s v \<noteq> \<phi> s w
[PROOF STEP]
using s_timing_common_inv assms
[PROOF STATE]
proof (prove)
using this:
timing_common_inv s
v \<in> dom (finished s)
w \<in> dom (finished s)
v \<noteq> w

goal (1 subgoal):
 1. \<phi> s v \<noteq> \<phi> s w
[PROOF STEP]
by (auto simp add: timing_common_inv_def)


[STATEMENT]
lemma finished_succ_fin:
    assumes "v \<in> dom (finished s)"
    and "w \<in> succ v"
    shows "\<delta> s w < \<phi> s v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<delta> s w < \<phi> s v
[PROOF STEP]
using assms s_timing_common_inv
[PROOF STATE]
proof (prove)
using this:
v \<in> dom (finished s)
w \<in> E `` {v}
timing_common_inv s

goal (1 subgoal):
 1. \<delta> s w < \<phi> s v
[PROOF STEP]
by (simp add: timing_common_inv_def)


[STATEMENT]
lemma i_prev_stack_discover_all:
    "is_invar (\<lambda>s. \<forall> n < length (stack s). \<forall> v \<in> set (drop (Suc n) (stack s)).
                   \<delta> s (stack s ! n) > \<delta> s v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_invar (\<lambda>s. \<forall>n<length (stack s). \<forall>v\<in>set (drop (Suc n) (stack s)). \<delta> s v < \<delta> s (stack s ! n))
[PROOF STEP]
proof (induct rule: is_invarI)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>e. \<forall>n<length (stack (empty_state e)). \<forall>v\<in>set (drop (Suc n) (stack (empty_state e))). \<delta> (empty_state e) v < \<delta> (empty_state e) (stack (empty_state e) ! n)
 2. \<And>s s' v0 e. \<lbrakk>\<forall>n<length (stack s). \<forall>v\<in>set (drop (Suc n) (stack s)). \<delta> s v < \<delta> s (stack s ! n); cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>n<length (stack s'). \<forall>v\<in>set (drop (Suc n) (stack s')). \<delta> s' v < \<delta> s' (stack s' ! n)
 3. \<And>s s' u e. \<lbrakk>\<forall>n<length (stack s). \<forall>v\<in>set (drop (Suc n) (stack s)). \<delta> s v < \<delta> s (stack s ! n); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; pending s `` {u} = {}; u = hd (stack s); s' = finish u s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>n<length (stack s'). \<forall>v\<in>set (drop (Suc n) (stack s')). \<delta> s' v < \<delta> s' (stack s' ! n)
 4. \<And>s s' u v e c b. \<lbrakk>\<forall>n<length (stack s). \<forall>v\<in>set (drop (Suc n) (stack s)). \<delta> s v < \<delta> s (stack s ! n); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> \<forall>n<length (stack s'). \<forall>v\<in>set (drop (Suc n) (stack s')). \<delta> s' v < \<delta> s' (stack s' ! n)
 5. \<And>s s' u v e. \<lbrakk>\<forall>n<length (stack s). \<forall>v\<in>set (drop (Suc n) (stack s)). \<delta> s v < \<delta> s (stack s ! n); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<notin> dom (discovered s); u = hd (stack s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>n<length (stack s'). \<forall>v\<in>set (drop (Suc n) (stack s')). \<delta> s' v < \<delta> s' (stack s' ! n)
[PROOF STEP]
case (finish s)
[PROOF STATE]
proof (state)
this:
\<forall>n<length (stack s). \<forall>v\<in>set (drop (Suc n) (stack s)). \<delta> s v < \<delta> s (stack s ! n)
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. \<forall>n<length (stack (empty_state e)). \<forall>v\<in>set (drop (Suc n) (stack (empty_state e))). \<delta> (empty_state e) v < \<delta> (empty_state e) (stack (empty_state e) ! n)
 2. \<And>s s' v0 e. \<lbrakk>\<forall>n<length (stack s). \<forall>v\<in>set (drop (Suc n) (stack s)). \<delta> s v < \<delta> s (stack s ! n); cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>n<length (stack s'). \<forall>v\<in>set (drop (Suc n) (stack s')). \<delta> s' v < \<delta> s' (stack s' ! n)
 3. \<And>s s' u e. \<lbrakk>\<forall>n<length (stack s). \<forall>v\<in>set (drop (Suc n) (stack s)). \<delta> s v < \<delta> s (stack s ! n); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; pending s `` {u} = {}; u = hd (stack s); s' = finish u s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>n<length (stack s'). \<forall>v\<in>set (drop (Suc n) (stack s')). \<delta> s' v < \<delta> s' (stack s' ! n)
 4. \<And>s s' u v e c b. \<lbrakk>\<forall>n<length (stack s). \<forall>v\<in>set (drop (Suc n) (stack s)). \<delta> s v < \<delta> s (stack s ! n); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> \<forall>n<length (stack s'). \<forall>v\<in>set (drop (Suc n) (stack s')). \<delta> s' v < \<delta> s' (stack s' ! n)
 5. \<And>s s' u v e. \<lbrakk>\<forall>n<length (stack s). \<forall>v\<in>set (drop (Suc n) (stack s)). \<delta> s v < \<delta> s (stack s ! n); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<notin> dom (discovered s); u = hd (stack s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>n<length (stack s'). \<forall>v\<in>set (drop (Suc n) (stack s')). \<delta> s' v < \<delta> s' (stack s' ! n)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>n<length (stack s). \<forall>v\<in>set (drop (Suc n) (stack s)). \<delta> s v < \<delta> s (stack s ! n)
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. \<forall>n<length (stack s'_). \<forall>v\<in>set (drop (Suc n) (stack s'_)). \<delta> s'_ v < \<delta> s'_ (stack s'_ ! n)
[PROOF STEP]
by (cases "stack s") auto
[PROOF STATE]
proof (state)
this:
\<forall>n<length (stack s'_). \<forall>v\<in>set (drop (Suc n) (stack s'_)). \<delta> s'_ v < \<delta> s'_ (stack s'_ ! n)

goal (4 subgoals):
 1. \<And>e. \<forall>n<length (stack (empty_state e)). \<forall>v\<in>set (drop (Suc n) (stack (empty_state e))). \<delta> (empty_state e) v < \<delta> (empty_state e) (stack (empty_state e) ! n)
 2. \<And>s s' v0 e. \<lbrakk>\<forall>n<length (stack s). \<forall>v\<in>set (drop (Suc n) (stack s)). \<delta> s v < \<delta> s (stack s ! n); cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>n<length (stack s'). \<forall>v\<in>set (drop (Suc n) (stack s')). \<delta> s' v < \<delta> s' (stack s' ! n)
 3. \<And>s s' u v e c b. \<lbrakk>\<forall>n<length (stack s). \<forall>v\<in>set (drop (Suc n) (stack s)). \<delta> s v < \<delta> s (stack s ! n); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> \<forall>n<length (stack s'). \<forall>v\<in>set (drop (Suc n) (stack s')). \<delta> s' v < \<delta> s' (stack s' ! n)
 4. \<And>s s' u v e. \<lbrakk>\<forall>n<length (stack s). \<forall>v\<in>set (drop (Suc n) (stack s)). \<delta> s v < \<delta> s (stack s ! n); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<notin> dom (discovered s); u = hd (stack s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>n<length (stack s'). \<forall>v\<in>set (drop (Suc n) (stack s')). \<delta> s' v < \<delta> s' (stack s' ! n)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>e. \<forall>n<length (stack (empty_state e)). \<forall>v\<in>set (drop (Suc n) (stack (empty_state e))). \<delta> (empty_state e) v < \<delta> (empty_state e) (stack (empty_state e) ! n)
 2. \<And>s s' v0 e. \<lbrakk>\<forall>n<length (stack s). \<forall>v\<in>set (drop (Suc n) (stack s)). \<delta> s v < \<delta> s (stack s ! n); cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>n<length (stack s'). \<forall>v\<in>set (drop (Suc n) (stack s')). \<delta> s' v < \<delta> s' (stack s' ! n)
 3. \<And>s s' u v e c b. \<lbrakk>\<forall>n<length (stack s). \<forall>v\<in>set (drop (Suc n) (stack s)). \<delta> s v < \<delta> s (stack s ! n); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> \<forall>n<length (stack s'). \<forall>v\<in>set (drop (Suc n) (stack s')). \<delta> s' v < \<delta> s' (stack s' ! n)
 4. \<And>s s' u v e. \<lbrakk>\<forall>n<length (stack s). \<forall>v\<in>set (drop (Suc n) (stack s)). \<delta> s v < \<delta> s (stack s ! n); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<notin> dom (discovered s); u = hd (stack s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>n<length (stack s'). \<forall>v\<in>set (drop (Suc n) (stack s')). \<delta> s' v < \<delta> s' (stack s' ! n)
[PROOF STEP]
case (discover s s' u v)
[PROOF STATE]
proof (state)
this:
\<forall>n<length (stack s). \<forall>v\<in>set (drop (Suc n) (stack s)). \<delta> s v < \<delta> s (stack s ! n)
cond s
DFS_invar G param s
DFS_invar G param s'
stack s \<noteq> []
v \<in> pending s `` {u}
v \<notin> dom (discovered s)
u = hd (stack s)
s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e_\<rparr>

goal (4 subgoals):
 1. \<And>e. \<forall>n<length (stack (empty_state e)). \<forall>v\<in>set (drop (Suc n) (stack (empty_state e))). \<delta> (empty_state e) v < \<delta> (empty_state e) (stack (empty_state e) ! n)
 2. \<And>s s' v0 e. \<lbrakk>\<forall>n<length (stack s). \<forall>v\<in>set (drop (Suc n) (stack s)). \<delta> s v < \<delta> s (stack s ! n); cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>n<length (stack s'). \<forall>v\<in>set (drop (Suc n) (stack s')). \<delta> s' v < \<delta> s' (stack s' ! n)
 3. \<And>s s' u v e c b. \<lbrakk>\<forall>n<length (stack s). \<forall>v\<in>set (drop (Suc n) (stack s)). \<delta> s v < \<delta> s (stack s ! n); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> \<forall>n<length (stack s'). \<forall>v\<in>set (drop (Suc n) (stack s')). \<delta> s' v < \<delta> s' (stack s' ! n)
 4. \<And>s s' u v e. \<lbrakk>\<forall>n<length (stack s). \<forall>v\<in>set (drop (Suc n) (stack s)). \<delta> s v < \<delta> s (stack s ! n); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<notin> dom (discovered s); u = hd (stack s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>n<length (stack s'). \<forall>v\<in>set (drop (Suc n) (stack s')). \<delta> s' v < \<delta> s' (stack s' ! n)
[PROOF STEP]
hence EQ[simp]: "discovered s' = (discovered s)(v \<mapsto> counter s)"
                    "stack s' = v#stack s"
[PROOF STATE]
proof (prove)
using this:
\<forall>n<length (stack s). \<forall>v\<in>set (drop (Suc n) (stack s)). \<delta> s v < \<delta> s (stack s ! n)
cond s
DFS_invar G param s
DFS_invar G param s'
stack s \<noteq> []
v \<in> pending s `` {u}
v \<notin> dom (discovered s)
u = hd (stack s)
s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e_\<rparr>

goal (1 subgoal):
 1. discovered s' = discovered s(v \<mapsto> counter s) &&& stack s' = v # stack s
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
discovered s' = discovered s(v \<mapsto> counter s)
stack s' = v # stack s

goal (4 subgoals):
 1. \<And>e. \<forall>n<length (stack (empty_state e)). \<forall>v\<in>set (drop (Suc n) (stack (empty_state e))). \<delta> (empty_state e) v < \<delta> (empty_state e) (stack (empty_state e) ! n)
 2. \<And>s s' v0 e. \<lbrakk>\<forall>n<length (stack s). \<forall>v\<in>set (drop (Suc n) (stack s)). \<delta> s v < \<delta> s (stack s ! n); cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>n<length (stack s'). \<forall>v\<in>set (drop (Suc n) (stack s')). \<delta> s' v < \<delta> s' (stack s' ! n)
 3. \<And>s s' u v e c b. \<lbrakk>\<forall>n<length (stack s). \<forall>v\<in>set (drop (Suc n) (stack s)). \<delta> s v < \<delta> s (stack s ! n); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> \<forall>n<length (stack s'). \<forall>v\<in>set (drop (Suc n) (stack s')). \<delta> s' v < \<delta> s' (stack s' ! n)
 4. \<And>s s' u v e. \<lbrakk>\<forall>n<length (stack s). \<forall>v\<in>set (drop (Suc n) (stack s)). \<delta> s v < \<delta> s (stack s ! n); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<notin> dom (discovered s); u = hd (stack s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>n<length (stack s'). \<forall>v\<in>set (drop (Suc n) (stack s')). \<delta> s' v < \<delta> s' (stack s' ! n)
[PROOF STEP]
from discover
[PROOF STATE]
proof (chain)
picking this:
\<forall>n<length (stack s). \<forall>v\<in>set (drop (Suc n) (stack s)). \<delta> s v < \<delta> s (stack s ! n)
cond s
DFS_invar G param s
DFS_invar G param s'
stack s \<noteq> []
v \<in> pending s `` {u}
v \<notin> dom (discovered s)
u = hd (stack s)
s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e_\<rparr>
[PROOF STEP]
interpret DFS_invar where s=s
[PROOF STATE]
proof (prove)
using this:
\<forall>n<length (stack s). \<forall>v\<in>set (drop (Suc n) (stack s)). \<delta> s v < \<delta> s (stack s ! n)
cond s
DFS_invar G param s
DFS_invar G param s'
stack s \<noteq> []
v \<in> pending s `` {u}
v \<notin> dom (discovered s)
u = hd (stack s)
s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e_\<rparr>

goal (1 subgoal):
 1. DFS_invar G param s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>e. \<forall>n<length (stack (empty_state e)). \<forall>v\<in>set (drop (Suc n) (stack (empty_state e))). \<delta> (empty_state e) v < \<delta> (empty_state e) (stack (empty_state e) ! n)
 2. \<And>s s' v0 e. \<lbrakk>\<forall>n<length (stack s). \<forall>v\<in>set (drop (Suc n) (stack s)). \<delta> s v < \<delta> s (stack s ! n); cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>n<length (stack s'). \<forall>v\<in>set (drop (Suc n) (stack s')). \<delta> s' v < \<delta> s' (stack s' ! n)
 3. \<And>s s' u v e c b. \<lbrakk>\<forall>n<length (stack s). \<forall>v\<in>set (drop (Suc n) (stack s)). \<delta> s v < \<delta> s (stack s ! n); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> \<forall>n<length (stack s'). \<forall>v\<in>set (drop (Suc n) (stack s')). \<delta> s' v < \<delta> s' (stack s' ! n)
 4. \<And>s s' u v e. \<lbrakk>\<forall>n<length (stack s). \<forall>v\<in>set (drop (Suc n) (stack s)). \<delta> s v < \<delta> s (stack s ! n); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<notin> dom (discovered s); u = hd (stack s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>n<length (stack s'). \<forall>v\<in>set (drop (Suc n) (stack s')). \<delta> s' v < \<delta> s' (stack s' ! n)
[PROOF STEP]
from discover stack_discovered
[PROOF STATE]
proof (chain)
picking this:
\<forall>n<length (stack s). \<forall>v\<in>set (drop (Suc n) (stack s)). \<delta> s v < \<delta> s (stack s ! n)
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>
set (stack s) \<subseteq> dom (discovered s)
[PROOF STEP]
have v_ni: "v \<notin> set (stack s)"
[PROOF STATE]
proof (prove)
using this:
\<forall>n<length (stack s). \<forall>v\<in>set (drop (Suc n) (stack s)). \<delta> s v < \<delta> s (stack s ! n)
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>
set (stack s) \<subseteq> dom (discovered s)

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

goal (4 subgoals):
 1. \<And>e. \<forall>n<length (stack (empty_state e)). \<forall>v\<in>set (drop (Suc n) (stack (empty_state e))). \<delta> (empty_state e) v < \<delta> (empty_state e) (stack (empty_state e) ! n)
 2. \<And>s s' v0 e. \<lbrakk>\<forall>n<length (stack s). \<forall>v\<in>set (drop (Suc n) (stack s)). \<delta> s v < \<delta> s (stack s ! n); cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>n<length (stack s'). \<forall>v\<in>set (drop (Suc n) (stack s')). \<delta> s' v < \<delta> s' (stack s' ! n)
 3. \<And>s s' u v e c b. \<lbrakk>\<forall>n<length (stack s). \<forall>v\<in>set (drop (Suc n) (stack s)). \<delta> s v < \<delta> s (stack s ! n); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> \<forall>n<length (stack s'). \<forall>v\<in>set (drop (Suc n) (stack s')). \<delta> s' v < \<delta> s' (stack s' ! n)
 4. \<And>s s' u v e. \<lbrakk>\<forall>n<length (stack s). \<forall>v\<in>set (drop (Suc n) (stack s)). \<delta> s v < \<delta> s (stack s ! n); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<notin> dom (discovered s); u = hd (stack s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>n<length (stack s'). \<forall>v\<in>set (drop (Suc n) (stack s')). \<delta> s' v < \<delta> s' (stack s' ! n)
[PROOF STEP]
from stack_discovered timing_less_counter
[PROOF STATE]
proof (chain)
picking this:
set (stack s) \<subseteq> dom (discovered s)
?v \<in> dom (discovered s) \<Longrightarrow> \<delta> s ?v < counter s
?v \<in> dom (finished s) \<Longrightarrow> \<phi> s ?v < counter s
[PROOF STEP]
have
      "\<And>w. w \<in> set (stack s) \<Longrightarrow> \<delta> s w < counter s"
[PROOF STATE]
proof (prove)
using this:
set (stack s) \<subseteq> dom (discovered s)
?v \<in> dom (discovered s) \<Longrightarrow> \<delta> s ?v < counter s
?v \<in> dom (finished s) \<Longrightarrow> \<phi> s ?v < counter s

goal (1 subgoal):
 1. \<And>w. w \<in> set (stack s) \<Longrightarrow> \<delta> s w < counter s
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
?w5 \<in> set (stack s) \<Longrightarrow> \<delta> s ?w5 < counter s

goal (4 subgoals):
 1. \<And>e. \<forall>n<length (stack (empty_state e)). \<forall>v\<in>set (drop (Suc n) (stack (empty_state e))). \<delta> (empty_state e) v < \<delta> (empty_state e) (stack (empty_state e) ! n)
 2. \<And>s s' v0 e. \<lbrakk>\<forall>n<length (stack s). \<forall>v\<in>set (drop (Suc n) (stack s)). \<delta> s v < \<delta> s (stack s ! n); cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>n<length (stack s'). \<forall>v\<in>set (drop (Suc n) (stack s')). \<delta> s' v < \<delta> s' (stack s' ! n)
 3. \<And>s s' u v e c b. \<lbrakk>\<forall>n<length (stack s). \<forall>v\<in>set (drop (Suc n) (stack s)). \<delta> s v < \<delta> s (stack s ! n); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> \<forall>n<length (stack s'). \<forall>v\<in>set (drop (Suc n) (stack s')). \<delta> s' v < \<delta> s' (stack s' ! n)
 4. \<And>s s' u v e. \<lbrakk>\<forall>n<length (stack s). \<forall>v\<in>set (drop (Suc n) (stack s)). \<delta> s v < \<delta> s (stack s ! n); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<notin> dom (discovered s); u = hd (stack s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>n<length (stack s'). \<forall>v\<in>set (drop (Suc n) (stack s')). \<delta> s' v < \<delta> s' (stack s' ! n)
[PROOF STEP]
with v_ni
[PROOF STATE]
proof (chain)
picking this:
v \<notin> set (stack s)
?w5 \<in> set (stack s) \<Longrightarrow> \<delta> s ?w5 < counter s
[PROOF STEP]
have "\<And>w. w \<in> set (stack s) \<Longrightarrow> \<delta> s' w < \<delta> s' v"
[PROOF STATE]
proof (prove)
using this:
v \<notin> set (stack s)
?w5 \<in> set (stack s) \<Longrightarrow> \<delta> s ?w5 < counter s

goal (1 subgoal):
 1. \<And>w. w \<in> set (stack s) \<Longrightarrow> \<delta> s' w < \<delta> s' v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?w5 \<in> set (stack s) \<Longrightarrow> \<delta> s' ?w5 < \<delta> s' v

goal (4 subgoals):
 1. \<And>e. \<forall>n<length (stack (empty_state e)). \<forall>v\<in>set (drop (Suc n) (stack (empty_state e))). \<delta> (empty_state e) v < \<delta> (empty_state e) (stack (empty_state e) ! n)
 2. \<And>s s' v0 e. \<lbrakk>\<forall>n<length (stack s). \<forall>v\<in>set (drop (Suc n) (stack s)). \<delta> s v < \<delta> s (stack s ! n); cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>n<length (stack s'). \<forall>v\<in>set (drop (Suc n) (stack s')). \<delta> s' v < \<delta> s' (stack s' ! n)
 3. \<And>s s' u v e c b. \<lbrakk>\<forall>n<length (stack s). \<forall>v\<in>set (drop (Suc n) (stack s)). \<delta> s v < \<delta> s (stack s ! n); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> \<forall>n<length (stack s'). \<forall>v\<in>set (drop (Suc n) (stack s')). \<delta> s' v < \<delta> s' (stack s' ! n)
 4. \<And>s s' u v e. \<lbrakk>\<forall>n<length (stack s). \<forall>v\<in>set (drop (Suc n) (stack s)). \<delta> s v < \<delta> s (stack s ! n); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<notin> dom (discovered s); u = hd (stack s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>n<length (stack s'). \<forall>v\<in>set (drop (Suc n) (stack s')). \<delta> s' v < \<delta> s' (stack s' ! n)
[PROOF STEP]
hence "\<And>w. w \<in> set (drop (Suc 0) (stack s')) \<Longrightarrow> \<delta> s' w < \<delta> s' (stack s' ! 0)"
[PROOF STATE]
proof (prove)
using this:
?w5 \<in> set (stack s) \<Longrightarrow> \<delta> s' ?w5 < \<delta> s' v

goal (1 subgoal):
 1. \<And>w. w \<in> set (drop (Suc 0) (stack s')) \<Longrightarrow> \<delta> s' w < \<delta> s' (stack s' ! 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?w5 \<in> set (drop (Suc 0) (stack s')) \<Longrightarrow> \<delta> s' ?w5 < \<delta> s' (stack s' ! 0)

goal (4 subgoals):
 1. \<And>e. \<forall>n<length (stack (empty_state e)). \<forall>v\<in>set (drop (Suc n) (stack (empty_state e))). \<delta> (empty_state e) v < \<delta> (empty_state e) (stack (empty_state e) ! n)
 2. \<And>s s' v0 e. \<lbrakk>\<forall>n<length (stack s). \<forall>v\<in>set (drop (Suc n) (stack s)). \<delta> s v < \<delta> s (stack s ! n); cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>n<length (stack s'). \<forall>v\<in>set (drop (Suc n) (stack s')). \<delta> s' v < \<delta> s' (stack s' ! n)
 3. \<And>s s' u v e c b. \<lbrakk>\<forall>n<length (stack s). \<forall>v\<in>set (drop (Suc n) (stack s)). \<delta> s v < \<delta> s (stack s ! n); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> \<forall>n<length (stack s'). \<forall>v\<in>set (drop (Suc n) (stack s')). \<delta> s' v < \<delta> s' (stack s' ! n)
 4. \<And>s s' u v e. \<lbrakk>\<forall>n<length (stack s). \<forall>v\<in>set (drop (Suc n) (stack s)). \<delta> s v < \<delta> s (stack s ! n); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<notin> dom (discovered s); u = hd (stack s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>n<length (stack s'). \<forall>v\<in>set (drop (Suc n) (stack s')). \<delta> s' v < \<delta> s' (stack s' ! n)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?w5 \<in> set (drop (Suc 0) (stack s')) \<Longrightarrow> \<delta> s' ?w5 < \<delta> s' (stack s' ! 0)

goal (4 subgoals):
 1. \<And>e. \<forall>n<length (stack (empty_state e)). \<forall>v\<in>set (drop (Suc n) (stack (empty_state e))). \<delta> (empty_state e) v < \<delta> (empty_state e) (stack (empty_state e) ! n)
 2. \<And>s s' v0 e. \<lbrakk>\<forall>n<length (stack s). \<forall>v\<in>set (drop (Suc n) (stack s)). \<delta> s v < \<delta> s (stack s ! n); cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>n<length (stack s'). \<forall>v\<in>set (drop (Suc n) (stack s')). \<delta> s' v < \<delta> s' (stack s' ! n)
 3. \<And>s s' u v e c b. \<lbrakk>\<forall>n<length (stack s). \<forall>v\<in>set (drop (Suc n) (stack s)). \<delta> s v < \<delta> s (stack s ! n); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> \<forall>n<length (stack s'). \<forall>v\<in>set (drop (Suc n) (stack s')). \<delta> s' v < \<delta> s' (stack s' ! n)
 4. \<And>s s' u v e. \<lbrakk>\<forall>n<length (stack s). \<forall>v\<in>set (drop (Suc n) (stack s)). \<delta> s v < \<delta> s (stack s ! n); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<notin> dom (discovered s); u = hd (stack s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>n<length (stack s'). \<forall>v\<in>set (drop (Suc n) (stack s')). \<delta> s' v < \<delta> s' (stack s' ! n)
[PROOF STEP]
from v_ni
[PROOF STATE]
proof (chain)
picking this:
v \<notin> set (stack s)
[PROOF STEP]
have
      "\<And>n. \<lbrakk>n < (length (stack s')); n > 0\<rbrakk>
      \<Longrightarrow> \<delta> s' (stack s' ! n) = \<delta> s (stack s' ! n)"
[PROOF STATE]
proof (prove)
using this:
v \<notin> set (stack s)

goal (1 subgoal):
 1. \<And>n. \<lbrakk>n < length (stack s'); 0 < n\<rbrakk> \<Longrightarrow> \<delta> s' (stack s' ! n) = \<delta> s (stack s' ! n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>?n5 < length (stack s'); 0 < ?n5\<rbrakk> \<Longrightarrow> \<delta> s' (stack s' ! ?n5) = \<delta> s (stack s' ! ?n5)

goal (4 subgoals):
 1. \<And>e. \<forall>n<length (stack (empty_state e)). \<forall>v\<in>set (drop (Suc n) (stack (empty_state e))). \<delta> (empty_state e) v < \<delta> (empty_state e) (stack (empty_state e) ! n)
 2. \<And>s s' v0 e. \<lbrakk>\<forall>n<length (stack s). \<forall>v\<in>set (drop (Suc n) (stack s)). \<delta> s v < \<delta> s (stack s ! n); cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>n<length (stack s'). \<forall>v\<in>set (drop (Suc n) (stack s')). \<delta> s' v < \<delta> s' (stack s' ! n)
 3. \<And>s s' u v e c b. \<lbrakk>\<forall>n<length (stack s). \<forall>v\<in>set (drop (Suc n) (stack s)). \<delta> s v < \<delta> s (stack s ! n); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> \<forall>n<length (stack s'). \<forall>v\<in>set (drop (Suc n) (stack s')). \<delta> s' v < \<delta> s' (stack s' ! n)
 4. \<And>s s' u v e. \<lbrakk>\<forall>n<length (stack s). \<forall>v\<in>set (drop (Suc n) (stack s)). \<delta> s v < \<delta> s (stack s ! n); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<notin> dom (discovered s); u = hd (stack s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>n<length (stack s'). \<forall>v\<in>set (drop (Suc n) (stack s')). \<delta> s' v < \<delta> s' (stack s' ! n)
[PROOF STEP]
with discover(1) v_ni
[PROOF STATE]
proof (chain)
picking this:
\<forall>n<length (stack s). \<forall>v\<in>set (drop (Suc n) (stack s)). \<delta> s v < \<delta> s (stack s ! n)
v \<notin> set (stack s)
\<lbrakk>?n5 < length (stack s'); 0 < ?n5\<rbrakk> \<Longrightarrow> \<delta> s' (stack s' ! ?n5) = \<delta> s (stack s' ! ?n5)
[PROOF STEP]
have  "\<And>n. \<lbrakk>n < (length (stack s')) - 1; n > 0\<rbrakk>
      \<Longrightarrow> \<forall> w \<in> set (drop (Suc n) (stack s')). \<delta> s' (stack s' ! n) > \<delta> s' w"
[PROOF STATE]
proof (prove)
using this:
\<forall>n<length (stack s). \<forall>v\<in>set (drop (Suc n) (stack s)). \<delta> s v < \<delta> s (stack s ! n)
v \<notin> set (stack s)
\<lbrakk>?n5 < length (stack s'); 0 < ?n5\<rbrakk> \<Longrightarrow> \<delta> s' (stack s' ! ?n5) = \<delta> s (stack s' ! ?n5)

goal (1 subgoal):
 1. \<And>n. \<lbrakk>n < length (stack s') - 1; 0 < n\<rbrakk> \<Longrightarrow> \<forall>w\<in>set (drop (Suc n) (stack s')). \<delta> s' w < \<delta> s' (stack s' ! n)
[PROOF STEP]
by (auto dest: in_set_dropD)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?n5 < length (stack s') - 1; 0 < ?n5\<rbrakk> \<Longrightarrow> \<forall>w\<in>set (drop (Suc ?n5) (stack s')). \<delta> s' w < \<delta> s' (stack s' ! ?n5)

goal (4 subgoals):
 1. \<And>e. \<forall>n<length (stack (empty_state e)). \<forall>v\<in>set (drop (Suc n) (stack (empty_state e))). \<delta> (empty_state e) v < \<delta> (empty_state e) (stack (empty_state e) ! n)
 2. \<And>s s' v0 e. \<lbrakk>\<forall>n<length (stack s). \<forall>v\<in>set (drop (Suc n) (stack s)). \<delta> s v < \<delta> s (stack s ! n); cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>n<length (stack s'). \<forall>v\<in>set (drop (Suc n) (stack s')). \<delta> s' v < \<delta> s' (stack s' ! n)
 3. \<And>s s' u v e c b. \<lbrakk>\<forall>n<length (stack s). \<forall>v\<in>set (drop (Suc n) (stack s)). \<delta> s v < \<delta> s (stack s ! n); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> \<forall>n<length (stack s'). \<forall>v\<in>set (drop (Suc n) (stack s')). \<delta> s' v < \<delta> s' (stack s' ! n)
 4. \<And>s s' u v e. \<lbrakk>\<forall>n<length (stack s). \<forall>v\<in>set (drop (Suc n) (stack s)). \<delta> s v < \<delta> s (stack s ! n); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<notin> dom (discovered s); u = hd (stack s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>n<length (stack s'). \<forall>v\<in>set (drop (Suc n) (stack s')). \<delta> s' v < \<delta> s' (stack s' ! n)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?w5 \<in> set (drop (Suc 0) (stack s')) \<Longrightarrow> \<delta> s' ?w5 < \<delta> s' (stack s' ! 0)
\<lbrakk>?n5 < length (stack s') - 1; 0 < ?n5\<rbrakk> \<Longrightarrow> \<forall>w\<in>set (drop (Suc ?n5) (stack s')). \<delta> s' w < \<delta> s' (stack s' ! ?n5)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
?w5 \<in> set (drop (Suc 0) (stack s')) \<Longrightarrow> \<delta> s' ?w5 < \<delta> s' (stack s' ! 0)
\<lbrakk>?n5 < length (stack s') - 1; 0 < ?n5\<rbrakk> \<Longrightarrow> \<forall>w\<in>set (drop (Suc ?n5) (stack s')). \<delta> s' w < \<delta> s' (stack s' ! ?n5)

goal (1 subgoal):
 1. \<forall>n<length (stack s'). \<forall>v\<in>set (drop (Suc n) (stack s')). \<delta> s' v < \<delta> s' (stack s' ! n)
[PROOF STEP]
by (metis drop_Suc_Cons length_drop length_pos_if_in_set length_tl
        list.sel(3) neq0_conv nth_Cons_0 EQ(2) zero_less_diff)
[PROOF STATE]
proof (state)
this:
\<forall>n<length (stack s'). \<forall>v\<in>set (drop (Suc n) (stack s')). \<delta> s' v < \<delta> s' (stack s' ! n)

goal (3 subgoals):
 1. \<And>e. \<forall>n<length (stack (empty_state e)). \<forall>v\<in>set (drop (Suc n) (stack (empty_state e))). \<delta> (empty_state e) v < \<delta> (empty_state e) (stack (empty_state e) ! n)
 2. \<And>s s' v0 e. \<lbrakk>\<forall>n<length (stack s). \<forall>v\<in>set (drop (Suc n) (stack s)). \<delta> s v < \<delta> s (stack s ! n); cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>n<length (stack s'). \<forall>v\<in>set (drop (Suc n) (stack s')). \<delta> s' v < \<delta> s' (stack s' ! n)
 3. \<And>s s' u v e c b. \<lbrakk>\<forall>n<length (stack s). \<forall>v\<in>set (drop (Suc n) (stack s)). \<delta> s v < \<delta> s (stack s ! n); cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> \<forall>n<length (stack s'). \<forall>v\<in>set (drop (Suc n) (stack s')). \<delta> s' v < \<delta> s' (stack s' ! n)
[PROOF STEP]
qed simp_all


[STATEMENT]
lemma prev_stack_discover:
    "\<lbrakk>n < length (stack s); v \<in> set (drop (Suc n) (stack s)) \<rbrakk>
     \<Longrightarrow> \<delta> s (stack s ! n) > \<delta> s v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < length (stack s); v \<in> set (drop (Suc n) (stack s))\<rbrakk> \<Longrightarrow> \<delta> s v < \<delta> s (stack s ! n)
[PROOF STEP]
by (metis prev_stack_discover_all)


[STATEMENT]
lemma Suc_stack_discover:
    assumes n: "n < (length (stack s)) - 1"
    shows "\<delta> s (stack s ! n) > \<delta> s (stack s ! Suc n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<delta> s (stack s ! Suc n) < \<delta> s (stack s ! n)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<delta> s (stack s ! Suc n) < \<delta> s (stack s ! n)
[PROOF STEP]
from prev_stack_discover assms
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?n < length (stack s); ?v \<in> set (drop (Suc ?n) (stack s))\<rbrakk> \<Longrightarrow> \<delta> s ?v < \<delta> s (stack s ! ?n)
n < length (stack s) - 1
[PROOF STEP]
have
      "\<And> v. v \<in> set (drop (Suc n) (stack s)) \<Longrightarrow> \<delta> s (stack s ! n) > \<delta> s v"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?n < length (stack s); ?v \<in> set (drop (Suc ?n) (stack s))\<rbrakk> \<Longrightarrow> \<delta> s ?v < \<delta> s (stack s ! ?n)
n < length (stack s) - 1

goal (1 subgoal):
 1. \<And>v. v \<in> set (drop (Suc n) (stack s)) \<Longrightarrow> \<delta> s v < \<delta> s (stack s ! n)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
?v5 \<in> set (drop (Suc n) (stack s)) \<Longrightarrow> \<delta> s ?v5 < \<delta> s (stack s ! n)

goal (1 subgoal):
 1. \<delta> s (stack s ! Suc n) < \<delta> s (stack s ! n)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?v5 \<in> set (drop (Suc n) (stack s)) \<Longrightarrow> \<delta> s ?v5 < \<delta> s (stack s ! n)

goal (1 subgoal):
 1. \<delta> s (stack s ! Suc n) < \<delta> s (stack s ! n)
[PROOF STEP]
from n
[PROOF STATE]
proof (chain)
picking this:
n < length (stack s) - 1
[PROOF STEP]
have "stack s ! Suc n \<in> set (drop (Suc n) (stack s))"
[PROOF STATE]
proof (prove)
using this:
n < length (stack s) - 1

goal (1 subgoal):
 1. stack s ! Suc n \<in> set (drop (Suc n) (stack s))
[PROOF STEP]
using in_set_conv_nth
[PROOF STATE]
proof (prove)
using this:
n < length (stack s) - 1
(?x \<in> set ?xs) = (\<exists>i<length ?xs. ?xs ! i = ?x)

goal (1 subgoal):
 1. stack s ! Suc n \<in> set (drop (Suc n) (stack s))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
stack s ! Suc n \<in> set (drop (Suc n) (stack s))

goal (1 subgoal):
 1. \<delta> s (stack s ! Suc n) < \<delta> s (stack s ! n)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?v5 \<in> set (drop (Suc n) (stack s)) \<Longrightarrow> \<delta> s ?v5 < \<delta> s (stack s ! n)
stack s ! Suc n \<in> set (drop (Suc n) (stack s))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?v5 \<in> set (drop (Suc n) (stack s)) \<Longrightarrow> \<delta> s ?v5 < \<delta> s (stack s ! n)
stack s ! Suc n \<in> set (drop (Suc n) (stack s))

goal (1 subgoal):
 1. \<delta> s (stack s ! Suc n) < \<delta> s (stack s ! n)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<delta> s (stack s ! Suc n) < \<delta> s (stack s ! n)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma tl_lt_stack_hd_discover:
    assumes notempty: "stack s \<noteq> []"
    and "x \<in> set (tl (stack s))"
    shows "\<delta> s x < \<delta> s (hd (stack s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<delta> s x < \<delta> s (hd (stack s))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<delta> s x < \<delta> s (hd (stack s))
[PROOF STEP]
from notempty
[PROOF STATE]
proof (chain)
picking this:
stack s \<noteq> []
[PROOF STEP]
obtain y ys where "stack s = y#ys"
[PROOF STATE]
proof (prove)
using this:
stack s \<noteq> []

goal (1 subgoal):
 1. (\<And>y ys. stack s = y # ys \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis list.exhaust)
[PROOF STATE]
proof (state)
this:
stack s = y # ys

goal (1 subgoal):
 1. \<delta> s x < \<delta> s (hd (stack s))
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
stack s \<noteq> []
x \<in> set (tl (stack s))
stack s = y # ys
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
stack s \<noteq> []
x \<in> set (tl (stack s))
stack s = y # ys

goal (1 subgoal):
 1. \<delta> s x < \<delta> s (hd (stack s))
[PROOF STEP]
using prev_stack_discover
[PROOF STATE]
proof (prove)
using this:
stack s \<noteq> []
x \<in> set (tl (stack s))
stack s = y # ys
\<lbrakk>?n < length (stack s); ?v \<in> set (drop (Suc ?n) (stack s))\<rbrakk> \<Longrightarrow> \<delta> s ?v < \<delta> s (stack s ! ?n)

goal (1 subgoal):
 1. \<delta> s x < \<delta> s (hd (stack s))
[PROOF STEP]
by (cases ys) force+
[PROOF STATE]
proof (state)
this:
\<delta> s x < \<delta> s (hd (stack s))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma stack_nth_order:
    assumes l: "i < length (stack s)" "j < length (stack s)"
    shows "\<delta> s (stack s ! i) < \<delta> s (stack s ! j) \<longleftrightarrow> i > j" (is "\<delta> s ?i < \<delta> s ?j \<longleftrightarrow> _")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<delta> s (stack s ! i) < \<delta> s (stack s ! j)) = (j < i)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<delta> s (stack s ! i) < \<delta> s (stack s ! j) \<Longrightarrow> j < i
 2. j < i \<Longrightarrow> \<delta> s (stack s ! i) < \<delta> s (stack s ! j)
[PROOF STEP]
assume \<delta>: "\<delta> s ?i < \<delta> s ?j"
[PROOF STATE]
proof (state)
this:
\<delta> s (stack s ! i) < \<delta> s (stack s ! j)

goal (2 subgoals):
 1. \<delta> s (stack s ! i) < \<delta> s (stack s ! j) \<Longrightarrow> j < i
 2. j < i \<Longrightarrow> \<delta> s (stack s ! i) < \<delta> s (stack s ! j)
[PROOF STEP]
from l stack_set_def
[PROOF STATE]
proof (chain)
picking this:
i < length (stack s)
j < length (stack s)
set (stack s) = dom (discovered s) - dom (finished s)
[PROOF STEP]
have
      disc: "?i \<in> dom (discovered s)" "?j \<in> dom (discovered s)"
[PROOF STATE]
proof (prove)
using this:
i < length (stack s)
j < length (stack s)
set (stack s) = dom (discovered s) - dom (finished s)

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

goal (2 subgoals):
 1. \<delta> s (stack s ! i) < \<delta> s (stack s ! j) \<Longrightarrow> j < i
 2. j < i \<Longrightarrow> \<delta> s (stack s ! i) < \<delta> s (stack s ! j)
[PROOF STEP]
with disc_unequal[OF disc] \<delta>
[PROOF STATE]
proof (chain)
picking this:
stack s ! i \<noteq> stack s ! j \<Longrightarrow> \<delta> s (stack s ! i) \<noteq> \<delta> s (stack s ! j)
\<delta> s (stack s ! i) < \<delta> s (stack s ! j)
stack s ! i \<in> dom (discovered s)
stack s ! j \<in> dom (discovered s)
[PROOF STEP]
have "i \<noteq> j"
[PROOF STATE]
proof (prove)
using this:
stack s ! i \<noteq> stack s ! j \<Longrightarrow> \<delta> s (stack s ! i) \<noteq> \<delta> s (stack s ! j)
\<delta> s (stack s ! i) < \<delta> s (stack s ! j)
stack s ! i \<in> dom (discovered s)
stack s ! j \<in> dom (discovered s)

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

goal (2 subgoals):
 1. \<delta> s (stack s ! i) < \<delta> s (stack s ! j) \<Longrightarrow> j < i
 2. j < i \<Longrightarrow> \<delta> s (stack s ! i) < \<delta> s (stack s ! j)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
i \<noteq> j

goal (2 subgoals):
 1. \<delta> s (stack s ! i) < \<delta> s (stack s ! j) \<Longrightarrow> j < i
 2. j < i \<Longrightarrow> \<delta> s (stack s ! i) < \<delta> s (stack s ! j)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
i \<noteq> j

goal (2 subgoals):
 1. \<delta> s (stack s ! i) < \<delta> s (stack s ! j) \<Longrightarrow> j < i
 2. j < i \<Longrightarrow> \<delta> s (stack s ! i) < \<delta> s (stack s ! j)
[PROOF STEP]
assume "i < j"
[PROOF STATE]
proof (state)
this:
i < j

goal (2 subgoals):
 1. \<delta> s (stack s ! i) < \<delta> s (stack s ! j) \<Longrightarrow> j < i
 2. j < i \<Longrightarrow> \<delta> s (stack s ! i) < \<delta> s (stack s ! j)
[PROOF STEP]
with l
[PROOF STATE]
proof (chain)
picking this:
i < length (stack s)
j < length (stack s)
i < j
[PROOF STEP]
have "stack s ! j \<in> set (drop (Suc i) (stack s))"
[PROOF STATE]
proof (prove)
using this:
i < length (stack s)
j < length (stack s)
i < j

goal (1 subgoal):
 1. stack s ! j \<in> set (drop (Suc i) (stack s))
[PROOF STEP]
using in_set_drop_conv_nth[of "stack s ! j" "Suc i" "stack s"]
[PROOF STATE]
proof (prove)
using this:
i < length (stack s)
j < length (stack s)
i < j
(stack s ! j \<in> set (drop (Suc i) (stack s))) = (\<exists>ia\<ge>Suc i. ia < length (stack s) \<and> stack s ! j = stack s ! ia)

goal (1 subgoal):
 1. stack s ! j \<in> set (drop (Suc i) (stack s))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
stack s ! j \<in> set (drop (Suc i) (stack s))

goal (2 subgoals):
 1. \<delta> s (stack s ! i) < \<delta> s (stack s ! j) \<Longrightarrow> j < i
 2. j < i \<Longrightarrow> \<delta> s (stack s ! i) < \<delta> s (stack s ! j)
[PROOF STEP]
with prev_stack_discover l
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?n < length (stack s); ?v \<in> set (drop (Suc ?n) (stack s))\<rbrakk> \<Longrightarrow> \<delta> s ?v < \<delta> s (stack s ! ?n)
i < length (stack s)
j < length (stack s)
stack s ! j \<in> set (drop (Suc i) (stack s))
[PROOF STEP]
have "\<delta> s (stack s ! j) < \<delta> s (stack s ! i)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?n < length (stack s); ?v \<in> set (drop (Suc ?n) (stack s))\<rbrakk> \<Longrightarrow> \<delta> s ?v < \<delta> s (stack s ! ?n)
i < length (stack s)
j < length (stack s)
stack s ! j \<in> set (drop (Suc i) (stack s))

goal (1 subgoal):
 1. \<delta> s (stack s ! j) < \<delta> s (stack s ! i)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<delta> s (stack s ! j) < \<delta> s (stack s ! i)

goal (2 subgoals):
 1. \<delta> s (stack s ! i) < \<delta> s (stack s ! j) \<Longrightarrow> j < i
 2. j < i \<Longrightarrow> \<delta> s (stack s ! i) < \<delta> s (stack s ! j)
[PROOF STEP]
with \<delta>
[PROOF STATE]
proof (chain)
picking this:
\<delta> s (stack s ! i) < \<delta> s (stack s ! j)
\<delta> s (stack s ! j) < \<delta> s (stack s ! i)
[PROOF STEP]
have "False"
[PROOF STATE]
proof (prove)
using this:
\<delta> s (stack s ! i) < \<delta> s (stack s ! j)
\<delta> s (stack s ! j) < \<delta> s (stack s ! i)

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

goal (2 subgoals):
 1. \<delta> s (stack s ! i) < \<delta> s (stack s ! j) \<Longrightarrow> j < i
 2. j < i \<Longrightarrow> \<delta> s (stack s ! i) < \<delta> s (stack s ! j)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
i < j \<Longrightarrow> False

goal (2 subgoals):
 1. \<delta> s (stack s ! i) < \<delta> s (stack s ! j) \<Longrightarrow> j < i
 2. j < i \<Longrightarrow> \<delta> s (stack s ! i) < \<delta> s (stack s ! j)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
i \<noteq> j
i < j \<Longrightarrow> False
[PROOF STEP]
show "i > j"
[PROOF STATE]
proof (prove)
using this:
i \<noteq> j
i < j \<Longrightarrow> False

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

goal (1 subgoal):
 1. j < i \<Longrightarrow> \<delta> s (stack s ! i) < \<delta> s (stack s ! j)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. j < i \<Longrightarrow> \<delta> s (stack s ! i) < \<delta> s (stack s ! j)
[PROOF STEP]
assume "i > j"
[PROOF STATE]
proof (state)
this:
j < i

goal (1 subgoal):
 1. j < i \<Longrightarrow> \<delta> s (stack s ! i) < \<delta> s (stack s ! j)
[PROOF STEP]
with l
[PROOF STATE]
proof (chain)
picking this:
i < length (stack s)
j < length (stack s)
j < i
[PROOF STEP]
have "stack s ! i \<in> set (drop (Suc j) (stack s))"
[PROOF STATE]
proof (prove)
using this:
i < length (stack s)
j < length (stack s)
j < i

goal (1 subgoal):
 1. stack s ! i \<in> set (drop (Suc j) (stack s))
[PROOF STEP]
using in_set_drop_conv_nth[of "stack s ! i" "Suc j" "stack s"]
[PROOF STATE]
proof (prove)
using this:
i < length (stack s)
j < length (stack s)
j < i
(stack s ! i \<in> set (drop (Suc j) (stack s))) = (\<exists>ia\<ge>Suc j. ia < length (stack s) \<and> stack s ! i = stack s ! ia)

goal (1 subgoal):
 1. stack s ! i \<in> set (drop (Suc j) (stack s))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
stack s ! i \<in> set (drop (Suc j) (stack s))

goal (1 subgoal):
 1. j < i \<Longrightarrow> \<delta> s (stack s ! i) < \<delta> s (stack s ! j)
[PROOF STEP]
with prev_stack_discover l
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?n < length (stack s); ?v \<in> set (drop (Suc ?n) (stack s))\<rbrakk> \<Longrightarrow> \<delta> s ?v < \<delta> s (stack s ! ?n)
i < length (stack s)
j < length (stack s)
stack s ! i \<in> set (drop (Suc j) (stack s))
[PROOF STEP]
show "\<delta> s ?i < \<delta> s ?j"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?n < length (stack s); ?v \<in> set (drop (Suc ?n) (stack s))\<rbrakk> \<Longrightarrow> \<delta> s ?v < \<delta> s (stack s ! ?n)
i < length (stack s)
j < length (stack s)
stack s ! i \<in> set (drop (Suc j) (stack s))

goal (1 subgoal):
 1. \<delta> s (stack s ! i) < \<delta> s (stack s ! j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<delta> s (stack s ! i) < \<delta> s (stack s ! j)

goal:
No subgoals!
[PROOF STEP]
qed