[STATEMENT]
lemma i_tree_one_predecessor:
    "is_invar (\<lambda>s. \<forall>(v,v') \<in> tree_edges s. \<forall>y. y \<noteq> v \<longrightarrow> (y,v') \<notin> tree_edges s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_invar (\<lambda>s. \<forall>(v, v')\<in>tree_edges s. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s)
[PROOF STEP]
proof (induct rule: is_invarI)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>e. \<forall>(v, v')\<in>tree_edges (empty_state e). \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>\<forall>(v, v')\<in>tree_edges s. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, v')\<in>tree_edges s'. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s'
 3. \<And>s s' u e. \<lbrakk>\<forall>(v, v')\<in>tree_edges s. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; pending s `` {u} = {}; u = hd (stack s); s' = finish u s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, v')\<in>tree_edges s'. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s'
 4. \<And>s s' u v e c b. \<lbrakk>\<forall>(v, v')\<in>tree_edges s. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges 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> \<forall>(v, v')\<in>tree_edges s'. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s'
 5. \<And>s s' u v e. \<lbrakk>\<forall>(v, v')\<in>tree_edges s. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<notin> dom (discovered s); u = hd (stack s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, v')\<in>tree_edges s'. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s'
[PROOF STEP]
case (discover s s' u v)
[PROOF STATE]
proof (state)
this:
\<forall>(v, v')\<in>tree_edges s. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s
cond s
DFS_invar G param s
DFS_invar G param s'
stack s \<noteq> []
v \<in> pending s `` {u}
v \<notin> dom (discovered s)
u = hd (stack s)
s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e_\<rparr>

goal (5 subgoals):
 1. \<And>e. \<forall>(v, v')\<in>tree_edges (empty_state e). \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>\<forall>(v, v')\<in>tree_edges s. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, v')\<in>tree_edges s'. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s'
 3. \<And>s s' u e. \<lbrakk>\<forall>(v, v')\<in>tree_edges s. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; pending s `` {u} = {}; u = hd (stack s); s' = finish u s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, v')\<in>tree_edges s'. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s'
 4. \<And>s s' u v e c b. \<lbrakk>\<forall>(v, v')\<in>tree_edges s. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges 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> \<forall>(v, v')\<in>tree_edges s'. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s'
 5. \<And>s s' u v e. \<lbrakk>\<forall>(v, v')\<in>tree_edges s. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<notin> dom (discovered s); u = hd (stack s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, v')\<in>tree_edges s'. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s'
[PROOF STEP]
hence EQ[simp]: "tree_edges s' = insert (hd (stack s),v) (tree_edges s)"
[PROOF STATE]
proof (prove)
using this:
\<forall>(v, v')\<in>tree_edges s. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s
cond s
DFS_invar G param s
DFS_invar G param s'
stack s \<noteq> []
v \<in> pending s `` {u}
v \<notin> dom (discovered s)
u = hd (stack s)
s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e_\<rparr>

goal (1 subgoal):
 1. tree_edges s' = insert (hd (stack s), v) (tree_edges s)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
tree_edges s' = insert (hd (stack s), v) (tree_edges s)

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

goal (1 subgoal):
 1. DFS_invar G param s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>e. \<forall>(v, v')\<in>tree_edges (empty_state e). \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>\<forall>(v, v')\<in>tree_edges s. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, v')\<in>tree_edges s'. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s'
 3. \<And>s s' u e. \<lbrakk>\<forall>(v, v')\<in>tree_edges s. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; pending s `` {u} = {}; u = hd (stack s); s' = finish u s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, v')\<in>tree_edges s'. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s'
 4. \<And>s s' u v e c b. \<lbrakk>\<forall>(v, v')\<in>tree_edges s. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges 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> \<forall>(v, v')\<in>tree_edges s'. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s'
 5. \<And>s s' u v e. \<lbrakk>\<forall>(v, v')\<in>tree_edges s. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<notin> dom (discovered s); u = hd (stack s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, v')\<in>tree_edges s'. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s'
[PROOF STEP]
from discover
[PROOF STATE]
proof (chain)
picking this:
\<forall>(v, v')\<in>tree_edges s. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s
cond s
DFS_invar G param s
DFS_invar G param s'
stack s \<noteq> []
v \<in> pending s `` {u}
v \<notin> dom (discovered s)
u = hd (stack s)
s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e_\<rparr>
[PROOF STEP]
have NE[simp]: "stack s \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
\<forall>(v, v')\<in>tree_edges s. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s
cond s
DFS_invar G param s
DFS_invar G param s'
stack s \<noteq> []
v \<in> pending s `` {u}
v \<notin> dom (discovered s)
u = hd (stack s)
s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e_\<rparr>

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

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

goal (5 subgoals):
 1. \<And>e. \<forall>(v, v')\<in>tree_edges (empty_state e). \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>\<forall>(v, v')\<in>tree_edges s. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, v')\<in>tree_edges s'. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s'
 3. \<And>s s' u e. \<lbrakk>\<forall>(v, v')\<in>tree_edges s. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; pending s `` {u} = {}; u = hd (stack s); s' = finish u s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, v')\<in>tree_edges s'. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s'
 4. \<And>s s' u v e c b. \<lbrakk>\<forall>(v, v')\<in>tree_edges s. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges 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> \<forall>(v, v')\<in>tree_edges s'. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s'
 5. \<And>s s' u v e. \<lbrakk>\<forall>(v, v')\<in>tree_edges s. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<notin> dom (discovered s); u = hd (stack s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, v')\<in>tree_edges s'. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s'
[PROOF STEP]
fix w w' y
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>e. \<forall>(v, v')\<in>tree_edges (empty_state e). \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>\<forall>(v, v')\<in>tree_edges s. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, v')\<in>tree_edges s'. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s'
 3. \<And>s s' u e. \<lbrakk>\<forall>(v, v')\<in>tree_edges s. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; pending s `` {u} = {}; u = hd (stack s); s' = finish u s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, v')\<in>tree_edges s'. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s'
 4. \<And>s s' u v e c b. \<lbrakk>\<forall>(v, v')\<in>tree_edges s. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges 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> \<forall>(v, v')\<in>tree_edges s'. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s'
 5. \<And>s s' u v e. \<lbrakk>\<forall>(v, v')\<in>tree_edges s. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<notin> dom (discovered s); u = hd (stack s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, v')\<in>tree_edges s'. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s'
[PROOF STEP]
assume *: "(w,w') \<in> tree_edges s'"
        and  "y \<noteq> w"
[PROOF STATE]
proof (state)
this:
(w, w') \<in> tree_edges s'
y \<noteq> w

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

goal (1 subgoal):
 1. hd (stack s) \<noteq> v
[PROOF STEP]
using hd_in_set[OF NE]
[PROOF STATE]
proof (prove)
using this:
\<forall>(v, v')\<in>tree_edges s. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges 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>
set (stack s) \<subseteq> dom (discovered s)
hd (stack s) \<in> set (stack s)

goal (1 subgoal):
 1. hd (stack s) \<noteq> v
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
hd (stack s) \<noteq> v

goal (5 subgoals):
 1. \<And>e. \<forall>(v, v')\<in>tree_edges (empty_state e). \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>\<forall>(v, v')\<in>tree_edges s. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, v')\<in>tree_edges s'. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s'
 3. \<And>s s' u e. \<lbrakk>\<forall>(v, v')\<in>tree_edges s. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; pending s `` {u} = {}; u = hd (stack s); s' = finish u s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, v')\<in>tree_edges s'. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s'
 4. \<And>s s' u v e c b. \<lbrakk>\<forall>(v, v')\<in>tree_edges s. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges 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> \<forall>(v, v')\<in>tree_edges s'. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s'
 5. \<And>s s' u v e. \<lbrakk>\<forall>(v, v')\<in>tree_edges s. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<notin> dom (discovered s); u = hd (stack s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, v')\<in>tree_edges s'. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s'
[PROOF STEP]
from discover tree_edges_discovered
[PROOF STATE]
proof (chain)
picking this:
\<forall>(v, v')\<in>tree_edges s. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges 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>
Field (tree_edges s) \<subseteq> dom (discovered s)
[PROOF STEP]
have
        v_notin_tree: "\<forall>(x,x') \<in> tree_edges s. x \<noteq> v \<and> x' \<noteq> v"
[PROOF STATE]
proof (prove)
using this:
\<forall>(v, v')\<in>tree_edges s. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges 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>
Field (tree_edges s) \<subseteq> dom (discovered s)

goal (1 subgoal):
 1. \<forall>(x, x')\<in>tree_edges s. x \<noteq> v \<and> x' \<noteq> v
[PROOF STEP]
by (blast intro!: Field_not_elem)
[PROOF STATE]
proof (state)
this:
\<forall>(x, x')\<in>tree_edges s. x \<noteq> v \<and> x' \<noteq> v

goal (5 subgoals):
 1. \<And>e. \<forall>(v, v')\<in>tree_edges (empty_state e). \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>\<forall>(v, v')\<in>tree_edges s. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, v')\<in>tree_edges s'. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s'
 3. \<And>s s' u e. \<lbrakk>\<forall>(v, v')\<in>tree_edges s. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; pending s `` {u} = {}; u = hd (stack s); s' = finish u s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, v')\<in>tree_edges s'. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s'
 4. \<And>s s' u v e c b. \<lbrakk>\<forall>(v, v')\<in>tree_edges s. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges 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> \<forall>(v, v')\<in>tree_edges s'. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s'
 5. \<And>s s' u v e. \<lbrakk>\<forall>(v, v')\<in>tree_edges s. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<notin> dom (discovered s); u = hd (stack s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, v')\<in>tree_edges s'. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s'
[PROOF STEP]
have "(y,w') \<notin> tree_edges s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (y, w') \<notin> tree_edges s'
[PROOF STEP]
proof (cases "w = hd (stack s)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. w = hd (stack s) \<Longrightarrow> (y, w') \<notin> tree_edges s'
 2. w \<noteq> hd (stack s) \<Longrightarrow> (y, w') \<notin> tree_edges s'
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
w = hd (stack s)

goal (2 subgoals):
 1. w = hd (stack s) \<Longrightarrow> (y, w') \<notin> tree_edges s'
 2. w \<noteq> hd (stack s) \<Longrightarrow> (y, w') \<notin> tree_edges s'
[PROOF STEP]
have "(y,v) \<notin> tree_edges s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (y, v) \<notin> tree_edges s'
[PROOF STEP]
proof (rule notI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (y, v) \<in> tree_edges s' \<Longrightarrow> False
[PROOF STEP]
assume "(y,v) \<in> tree_edges s'"
[PROOF STATE]
proof (state)
this:
(y, v) \<in> tree_edges s'

goal (1 subgoal):
 1. (y, v) \<in> tree_edges s' \<Longrightarrow> False
[PROOF STEP]
with True \<open>y\<noteq>w\<close>
[PROOF STATE]
proof (chain)
picking this:
w = hd (stack s)
y \<noteq> w
(y, v) \<in> tree_edges s'
[PROOF STEP]
have "(y,v) \<in> tree_edges s"
[PROOF STATE]
proof (prove)
using this:
w = hd (stack s)
y \<noteq> w
(y, v) \<in> tree_edges s'

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

goal (1 subgoal):
 1. (y, v) \<in> tree_edges s' \<Longrightarrow> False
[PROOF STEP]
with v_notin_tree
[PROOF STATE]
proof (chain)
picking this:
\<forall>(x, x')\<in>tree_edges s. x \<noteq> v \<and> x' \<noteq> v
(y, v) \<in> tree_edges s
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<forall>(x, x')\<in>tree_edges s. x \<noteq> v \<and> x' \<noteq> v
(y, v) \<in> tree_edges s

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(y, v) \<notin> tree_edges s'

goal (2 subgoals):
 1. w = hd (stack s) \<Longrightarrow> (y, w') \<notin> tree_edges s'
 2. w \<noteq> hd (stack s) \<Longrightarrow> (y, w') \<notin> tree_edges s'
[PROOF STEP]
with True * \<open>y\<noteq>w\<close> v_hd
[PROOF STATE]
proof (chain)
picking this:
w = hd (stack s)
(w, w') \<in> tree_edges s'
y \<noteq> w
hd (stack s) \<noteq> v
(y, v) \<notin> tree_edges s'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
w = hd (stack s)
(w, w') \<in> tree_edges s'
y \<noteq> w
hd (stack s) \<noteq> v
(y, v) \<notin> tree_edges s'

goal (1 subgoal):
 1. (y, w') \<notin> tree_edges s'
[PROOF STEP]
apply (cases "w = v")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>w = hd (stack s); (w, w') \<in> tree_edges s'; y \<noteq> w; hd (stack s) \<noteq> v; (y, v) \<notin> tree_edges s'; w = v\<rbrakk> \<Longrightarrow> (y, w') \<notin> tree_edges s'
 2. \<lbrakk>w = hd (stack s); (w, w') \<in> tree_edges s'; y \<noteq> w; hd (stack s) \<noteq> v; (y, v) \<notin> tree_edges s'; w \<noteq> v\<rbrakk> \<Longrightarrow> (y, w') \<notin> tree_edges s'
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>w = hd (stack s); (w, w') \<in> tree_edges s'; y \<noteq> w; hd (stack s) \<noteq> v; (y, v) \<notin> tree_edges s'; w \<noteq> v\<rbrakk> \<Longrightarrow> (y, w') \<notin> tree_edges s'
[PROOF STEP]
using discover
[PROOF STATE]
proof (prove)
using this:
\<forall>(v, v')\<in>tree_edges s. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s
cond s
DFS_invar G param s
DFS_invar G param s'
stack s \<noteq> []
v \<in> pending s `` {u}
v \<notin> dom (discovered s)
u = hd (stack s)
s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e_\<rparr>

goal (1 subgoal):
 1. \<lbrakk>w = hd (stack s); (w, w') \<in> tree_edges s'; y \<noteq> w; hd (stack s) \<noteq> v; (y, v) \<notin> tree_edges s'; w \<noteq> v\<rbrakk> \<Longrightarrow> (y, w') \<notin> tree_edges s'
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>w = hd (stack s); w' = v \<or> (hd (stack s), w') \<in> tree_edges s; y \<noteq> hd (stack s); hd (stack s) \<noteq> v; (y, v) \<notin> tree_edges s; \<forall>x\<in>tree_edges s. case x of (v, v') \<Rightarrow> \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s; 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>); (hd (stack s), v) \<in> pending s; v \<notin> dom (discovered s); u = hd (stack s); s' = discover (hd (stack s)) v (s\<lparr>pending := pending s - {(hd (stack s), v)}\<rparr>)\<lparr>state.more := e_\<rparr>\<rbrakk> \<Longrightarrow> (y, w') \<notin> tree_edges s
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(y, w') \<notin> tree_edges s'

goal (1 subgoal):
 1. w \<noteq> hd (stack s) \<Longrightarrow> (y, w') \<notin> tree_edges s'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. w \<noteq> hd (stack s) \<Longrightarrow> (y, w') \<notin> tree_edges s'
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
w \<noteq> hd (stack s)

goal (1 subgoal):
 1. w \<noteq> hd (stack s) \<Longrightarrow> (y, w') \<notin> tree_edges s'
[PROOF STEP]
with v_notin_tree * \<open>y\<noteq>w\<close> v_hd
[PROOF STATE]
proof (chain)
picking this:
\<forall>(x, x')\<in>tree_edges s. x \<noteq> v \<and> x' \<noteq> v
(w, w') \<in> tree_edges s'
y \<noteq> w
hd (stack s) \<noteq> v
w \<noteq> hd (stack s)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>(x, x')\<in>tree_edges s. x \<noteq> v \<and> x' \<noteq> v
(w, w') \<in> tree_edges s'
y \<noteq> w
hd (stack s) \<noteq> v
w \<noteq> hd (stack s)

goal (1 subgoal):
 1. (y, w') \<notin> tree_edges s'
[PROOF STEP]
apply (cases "w' = v")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>(x, x')\<in>tree_edges s. x \<noteq> v \<and> x' \<noteq> v; (w, w') \<in> tree_edges s'; y \<noteq> w; hd (stack s) \<noteq> v; w \<noteq> hd (stack s); w' = v\<rbrakk> \<Longrightarrow> (y, w') \<notin> tree_edges s'
 2. \<lbrakk>\<forall>(x, x')\<in>tree_edges s. x \<noteq> v \<and> x' \<noteq> v; (w, w') \<in> tree_edges s'; y \<noteq> w; hd (stack s) \<noteq> v; w \<noteq> hd (stack s); w' \<noteq> v\<rbrakk> \<Longrightarrow> (y, w') \<notin> tree_edges s'
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>x\<in>tree_edges s. case x of (x, x') \<Rightarrow> x \<noteq> v \<and> x' \<noteq> v; (w, v) \<in> tree_edges s; y \<noteq> w; hd (stack s) \<noteq> v; w \<noteq> hd (stack s); w' = v\<rbrakk> \<Longrightarrow> y \<noteq> hd (stack s) \<and> (y, v) \<notin> tree_edges s
 2. \<lbrakk>\<forall>(x, x')\<in>tree_edges s. x \<noteq> v \<and> x' \<noteq> v; (w, w') \<in> tree_edges s'; y \<noteq> w; hd (stack s) \<noteq> v; w \<noteq> hd (stack s); w' \<noteq> v\<rbrakk> \<Longrightarrow> (y, w') \<notin> tree_edges s'
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>(x, x')\<in>tree_edges s. x \<noteq> v \<and> x' \<noteq> v; (w, w') \<in> tree_edges s'; y \<noteq> w; hd (stack s) \<noteq> v; w \<noteq> hd (stack s); w' \<noteq> v\<rbrakk> \<Longrightarrow> (y, w') \<notin> tree_edges s'
[PROOF STEP]
using discover
[PROOF STATE]
proof (prove)
using this:
\<forall>(v, v')\<in>tree_edges s. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s
cond s
DFS_invar G param s
DFS_invar G param s'
stack s \<noteq> []
v \<in> pending s `` {u}
v \<notin> dom (discovered s)
u = hd (stack s)
s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e_\<rparr>

goal (1 subgoal):
 1. \<lbrakk>\<forall>(x, x')\<in>tree_edges s. x \<noteq> v \<and> x' \<noteq> v; (w, w') \<in> tree_edges s'; y \<noteq> w; hd (stack s) \<noteq> v; w \<noteq> hd (stack s); w' \<noteq> v\<rbrakk> \<Longrightarrow> (y, w') \<notin> tree_edges s'
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>tree_edges s. case x of (x, x') \<Rightarrow> x \<noteq> v \<and> x' \<noteq> v; (w, w') \<in> tree_edges s; y \<noteq> w; hd (stack s) \<noteq> v; w \<noteq> hd (stack s); w' \<noteq> v; \<forall>x\<in>tree_edges s. case x of (v, v') \<Rightarrow> \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s; 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>); (hd (stack s), v) \<in> pending s; v \<notin> dom (discovered s); u = hd (stack s); s' = discover (hd (stack s)) v (s\<lparr>pending := pending s - {(hd (stack s), v)}\<rparr>)\<lparr>state.more := e_\<rparr>\<rbrakk> \<Longrightarrow> (y, w') \<notin> tree_edges s
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(y, w') \<notin> tree_edges s'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(y, w') \<notin> tree_edges s'

goal (5 subgoals):
 1. \<And>e. \<forall>(v, v')\<in>tree_edges (empty_state e). \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>\<forall>(v, v')\<in>tree_edges s. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, v')\<in>tree_edges s'. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s'
 3. \<And>s s' u e. \<lbrakk>\<forall>(v, v')\<in>tree_edges s. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; pending s `` {u} = {}; u = hd (stack s); s' = finish u s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, v')\<in>tree_edges s'. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s'
 4. \<And>s s' u v e c b. \<lbrakk>\<forall>(v, v')\<in>tree_edges s. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges 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> \<forall>(v, v')\<in>tree_edges s'. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s'
 5. \<And>s s' u v e. \<lbrakk>\<forall>(v, v')\<in>tree_edges s. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<notin> dom (discovered s); u = hd (stack s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, v')\<in>tree_edges s'. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s'
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?w9, ?w'9) \<in> tree_edges s'; ?y9 \<noteq> ?w9\<rbrakk> \<Longrightarrow> (?y9, ?w'9) \<notin> tree_edges s'

goal (5 subgoals):
 1. \<And>e. \<forall>(v, v')\<in>tree_edges (empty_state e). \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>\<forall>(v, v')\<in>tree_edges s. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, v')\<in>tree_edges s'. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s'
 3. \<And>s s' u e. \<lbrakk>\<forall>(v, v')\<in>tree_edges s. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; pending s `` {u} = {}; u = hd (stack s); s' = finish u s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, v')\<in>tree_edges s'. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s'
 4. \<And>s s' u v e c b. \<lbrakk>\<forall>(v, v')\<in>tree_edges s. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges 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> \<forall>(v, v')\<in>tree_edges s'. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s'
 5. \<And>s s' u v e. \<lbrakk>\<forall>(v, v')\<in>tree_edges s. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<notin> dom (discovered s); u = hd (stack s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, v')\<in>tree_edges s'. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s'
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?w9, ?w'9) \<in> tree_edges s'; ?y9 \<noteq> ?w9\<rbrakk> \<Longrightarrow> (?y9, ?w'9) \<notin> tree_edges s'

goal (1 subgoal):
 1. \<forall>(v, v')\<in>tree_edges s'. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>(v, v')\<in>tree_edges s'. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s'

goal (4 subgoals):
 1. \<And>e. \<forall>(v, v')\<in>tree_edges (empty_state e). \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>\<forall>(v, v')\<in>tree_edges s. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, v')\<in>tree_edges s'. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s'
 3. \<And>s s' u e. \<lbrakk>\<forall>(v, v')\<in>tree_edges s. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; pending s `` {u} = {}; u = hd (stack s); s' = finish u s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, v')\<in>tree_edges s'. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s'
 4. \<And>s s' u v e c b. \<lbrakk>\<forall>(v, v')\<in>tree_edges s. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges 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> \<forall>(v, v')\<in>tree_edges s'. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s'
[PROOF STEP]
qed simp_all


[STATEMENT]
lemma (in DFS_invar) tree_one_predecessor:
    assumes "(v,w) \<in> tree_edges s"
    and "a \<noteq> v"
    shows "(a,w) \<notin> tree_edges s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a, w) \<notin> tree_edges s
[PROOF STEP]
using assms make_invar_thm[OF i_tree_one_predecessor]
[PROOF STATE]
proof (prove)
using this:
(v, w) \<in> tree_edges s
a \<noteq> v
\<forall>(v, v')\<in>tree_edges s. \<forall>y. y \<noteq> v \<longrightarrow> (y, v') \<notin> tree_edges s

goal (1 subgoal):
 1. (a, w) \<notin> tree_edges s
[PROOF STEP]
by blast


[STATEMENT]
lemma (in DFS_invar) tree_eq_rule:
    "\<lbrakk>(v,w) \<in> tree_edges s; (u,w) \<in> tree_edges s\<rbrakk> \<Longrightarrow> v=u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(v, w) \<in> tree_edges s; (u, w) \<in> tree_edges s\<rbrakk> \<Longrightarrow> v = u
[PROOF STEP]
using tree_one_predecessor
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?v, ?w) \<in> tree_edges s; ?a \<noteq> ?v\<rbrakk> \<Longrightarrow> (?a, ?w) \<notin> tree_edges s

goal (1 subgoal):
 1. \<lbrakk>(v, w) \<in> tree_edges s; (u, w) \<in> tree_edges s\<rbrakk> \<Longrightarrow> v = u
[PROOF STEP]
by blast


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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<forall>(x, x')\<in>tree_edges s. x \<noteq> v \<and> x' \<noteq> v
[PROOF STEP]
by (blast intro!: Field_not_elem)
[PROOF STATE]
proof (state)
this:
\<forall>(x, x')\<in>tree_edges s. x \<noteq> v \<and> x' \<noteq> v

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

goal (1 subgoal):
 1. hd (stack s) \<noteq> v
[PROOF STEP]
using hd_in_set[OF NE]
[PROOF STATE]
proof (prove)
using this:
\<forall>(v, v')\<in>tree_edges s. \<delta> s v < \<delta> s v'
cond s
DFS_invar G param s
DFS_invar G param s'
stack s \<noteq> []
v \<in> pending s `` {u}
v \<notin> dom (discovered s)
u = hd (stack s)
s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e_\<rparr>
set (stack s) \<subseteq> dom (discovered s)
hd (stack s) \<in> set (stack s)

goal (1 subgoal):
 1. hd (stack s) \<noteq> v
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
hd (stack s) \<noteq> v

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

goal (5 subgoals):
 1. \<And>e. \<forall>(v, v')\<in>tree_edges (empty_state e). \<delta> (empty_state e) v < \<delta> (empty_state e) v'
 2. \<And>s s' v0 e. \<lbrakk>\<forall>(v, v')\<in>tree_edges s. \<delta> s v < \<delta> s v'; cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, v')\<in>tree_edges s'. \<delta> s' v < \<delta> s' v'
 3. \<And>s s' u e. \<lbrakk>\<forall>(v, v')\<in>tree_edges s. \<delta> s v < \<delta> s v'; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; pending s `` {u} = {}; u = hd (stack s); s' = finish u s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, v')\<in>tree_edges s'. \<delta> s' v < \<delta> s' v'
 4. \<And>s s' u v e c b. \<lbrakk>\<forall>(v, v')\<in>tree_edges s. \<delta> s v < \<delta> s v'; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, v')\<in>tree_edges s'. \<delta> s' v < \<delta> s' v'
 5. \<And>s s' u v e. \<lbrakk>\<forall>(v, v')\<in>tree_edges s. \<delta> s v < \<delta> s v'; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<notin> dom (discovered s); u = hd (stack s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, v')\<in>tree_edges s'. \<delta> s' v < \<delta> s' v'
[PROOF STEP]
fix a b
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>e. \<forall>(v, v')\<in>tree_edges (empty_state e). \<delta> (empty_state e) v < \<delta> (empty_state e) v'
 2. \<And>s s' v0 e. \<lbrakk>\<forall>(v, v')\<in>tree_edges s. \<delta> s v < \<delta> s v'; cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, v')\<in>tree_edges s'. \<delta> s' v < \<delta> s' v'
 3. \<And>s s' u e. \<lbrakk>\<forall>(v, v')\<in>tree_edges s. \<delta> s v < \<delta> s v'; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; pending s `` {u} = {}; u = hd (stack s); s' = finish u s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, v')\<in>tree_edges s'. \<delta> s' v < \<delta> s' v'
 4. \<And>s s' u v e c b. \<lbrakk>\<forall>(v, v')\<in>tree_edges s. \<delta> s v < \<delta> s v'; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, v')\<in>tree_edges s'. \<delta> s' v < \<delta> s' v'
 5. \<And>s s' u v e. \<lbrakk>\<forall>(v, v')\<in>tree_edges s. \<delta> s v < \<delta> s v'; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<notin> dom (discovered s); u = hd (stack s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, v')\<in>tree_edges s'. \<delta> s' v < \<delta> s' v'
[PROOF STEP]
assume T: "(a,b) \<in> tree_edges s'"
[PROOF STATE]
proof (state)
this:
(a, b) \<in> tree_edges s'

goal (5 subgoals):
 1. \<And>e. \<forall>(v, v')\<in>tree_edges (empty_state e). \<delta> (empty_state e) v < \<delta> (empty_state e) v'
 2. \<And>s s' v0 e. \<lbrakk>\<forall>(v, v')\<in>tree_edges s. \<delta> s v < \<delta> s v'; cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, v')\<in>tree_edges s'. \<delta> s' v < \<delta> s' v'
 3. \<And>s s' u e. \<lbrakk>\<forall>(v, v')\<in>tree_edges s. \<delta> s v < \<delta> s v'; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; pending s `` {u} = {}; u = hd (stack s); s' = finish u s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, v')\<in>tree_edges s'. \<delta> s' v < \<delta> s' v'
 4. \<And>s s' u v e c b. \<lbrakk>\<forall>(v, v')\<in>tree_edges s. \<delta> s v < \<delta> s v'; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, v')\<in>tree_edges s'. \<delta> s' v < \<delta> s' v'
 5. \<And>s s' u v e. \<lbrakk>\<forall>(v, v')\<in>tree_edges s. \<delta> s v < \<delta> s v'; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<notin> dom (discovered s); u = hd (stack s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, v')\<in>tree_edges s'. \<delta> s' v < \<delta> s' v'
[PROOF STEP]
have "\<delta> s' a < \<delta> s' b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<delta> s' a < \<delta> s' b
[PROOF STEP]
proof (cases "b = v")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. b = v \<Longrightarrow> \<delta> s' a < \<delta> s' b
 2. b \<noteq> v \<Longrightarrow> \<delta> s' a < \<delta> s' b
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
b = v

goal (2 subgoals):
 1. b = v \<Longrightarrow> \<delta> s' a < \<delta> s' b
 2. b \<noteq> v \<Longrightarrow> \<delta> s' a < \<delta> s' b
[PROOF STEP]
with T v_notin_tree
[PROOF STATE]
proof (chain)
picking this:
(a, b) \<in> tree_edges s'
\<forall>(x, x')\<in>tree_edges s. x \<noteq> v \<and> x' \<noteq> v
b = v
[PROOF STEP]
have [simp]: "a = hd (stack s)"
[PROOF STATE]
proof (prove)
using this:
(a, b) \<in> tree_edges s'
\<forall>(x, x')\<in>tree_edges s. x \<noteq> v \<and> x' \<noteq> v
b = v

goal (1 subgoal):
 1. a = hd (stack s)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a = hd (stack s)

goal (2 subgoals):
 1. b = v \<Longrightarrow> \<delta> s' a < \<delta> s' b
 2. b \<noteq> v \<Longrightarrow> \<delta> s' a < \<delta> s' b
[PROOF STEP]
with stack_discovered
[PROOF STATE]
proof (chain)
picking this:
set (stack s) \<subseteq> dom (discovered s)
a = hd (stack s)
[PROOF STEP]
have "a \<in> dom (discovered s)"
[PROOF STATE]
proof (prove)
using this:
set (stack s) \<subseteq> dom (discovered s)
a = hd (stack s)

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

goal (2 subgoals):
 1. b = v \<Longrightarrow> \<delta> s' a < \<delta> s' b
 2. b \<noteq> v \<Longrightarrow> \<delta> s' a < \<delta> s' b
[PROOF STEP]
with v_hd True timing_less_counter
[PROOF STATE]
proof (chain)
picking this:
hd (stack s) \<noteq> v
b = v
?v \<in> dom (discovered s) \<Longrightarrow> \<delta> s ?v < counter s
?v \<in> dom (finished s) \<Longrightarrow> \<phi> s ?v < counter s
a \<in> dom (discovered s)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
hd (stack s) \<noteq> v
b = v
?v \<in> dom (discovered s) \<Longrightarrow> \<delta> s ?v < counter s
?v \<in> dom (finished s) \<Longrightarrow> \<phi> s ?v < counter s
a \<in> dom (discovered s)

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

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

goal (1 subgoal):
 1. b \<noteq> v \<Longrightarrow> \<delta> s' a < \<delta> s' b
[PROOF STEP]
with v_notin_tree T
[PROOF STATE]
proof (chain)
picking this:
\<forall>(x, x')\<in>tree_edges s. x \<noteq> v \<and> x' \<noteq> v
(a, b) \<in> tree_edges s'
b \<noteq> v
[PROOF STEP]
have "(a,b) \<in> tree_edges s" "a \<noteq> v"
[PROOF STATE]
proof (prove)
using this:
\<forall>(x, x')\<in>tree_edges s. x \<noteq> v \<and> x' \<noteq> v
(a, b) \<in> tree_edges s'
b \<noteq> v

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

goal (1 subgoal):
 1. b \<noteq> v \<Longrightarrow> \<delta> s' a < \<delta> s' b
[PROOF STEP]
with discover
[PROOF STATE]
proof (chain)
picking this:
\<forall>(v, v')\<in>tree_edges s. \<delta> s v < \<delta> s v'
cond s
DFS_invar G param s
DFS_invar G param s'
stack s \<noteq> []
v \<in> pending s `` {u}
v \<notin> dom (discovered s)
u = hd (stack s)
s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e_\<rparr>
(a, b) \<in> tree_edges s
a \<noteq> v
[PROOF STEP]
have "\<delta> s a < \<delta> s b"
[PROOF STATE]
proof (prove)
using this:
\<forall>(v, v')\<in>tree_edges s. \<delta> s v < \<delta> s v'
cond s
DFS_invar G param s
DFS_invar G param s'
stack s \<noteq> []
v \<in> pending s `` {u}
v \<notin> dom (discovered s)
u = hd (stack s)
s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e_\<rparr>
(a, b) \<in> tree_edges s
a \<noteq> v

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

goal (1 subgoal):
 1. b \<noteq> v \<Longrightarrow> \<delta> s' a < \<delta> s' b
[PROOF STEP]
with False \<open>a\<noteq>v\<close>
[PROOF STATE]
proof (chain)
picking this:
b \<noteq> v
a \<noteq> v
\<delta> s a < \<delta> s b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
b \<noteq> v
a \<noteq> v
\<delta> s a < \<delta> s b

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<delta> s' a < \<delta> s' b

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

goal (5 subgoals):
 1. \<And>e. \<forall>(v, v')\<in>tree_edges (empty_state e). \<delta> (empty_state e) v < \<delta> (empty_state e) v'
 2. \<And>s s' v0 e. \<lbrakk>\<forall>(v, v')\<in>tree_edges s. \<delta> s v < \<delta> s v'; cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, v')\<in>tree_edges s'. \<delta> s' v < \<delta> s' v'
 3. \<And>s s' u e. \<lbrakk>\<forall>(v, v')\<in>tree_edges s. \<delta> s v < \<delta> s v'; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; pending s `` {u} = {}; u = hd (stack s); s' = finish u s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, v')\<in>tree_edges s'. \<delta> s' v < \<delta> s' v'
 4. \<And>s s' u v e c b. \<lbrakk>\<forall>(v, v')\<in>tree_edges s. \<delta> s v < \<delta> s v'; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, v')\<in>tree_edges s'. \<delta> s' v < \<delta> s' v'
 5. \<And>s s' u v e. \<lbrakk>\<forall>(v, v')\<in>tree_edges s. \<delta> s v < \<delta> s v'; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<notin> dom (discovered s); u = hd (stack s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> \<forall>(v, v')\<in>tree_edges s'. \<delta> s' v < \<delta> s' v'
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
(?a9, ?b9) \<in> tree_edges s' \<Longrightarrow> \<delta> s' ?a9 < \<delta> s' ?b9

goal (1 subgoal):
 1. \<forall>(v, v')\<in>tree_edges s'. \<delta> s' v < \<delta> s' v'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>(v, v')\<in>tree_edges s'. \<delta> s' v < \<delta> s' v'

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

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

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

goal (1 subgoal):
 1. tree_edges s' = tree_edges s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
tree_edges s' = tree_edges s

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

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

goal (1 subgoal):
 1. \<forall>(v, v')\<in>tree_edges s. v \<noteq> v0 \<and> v' \<noteq> v0
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>(v, v')\<in>tree_edges s. v \<noteq> v0 \<and> v' \<noteq> v0

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

goal (1 subgoal):
 1. \<forall>(v, v')\<in>tree_edges s'. \<delta> s' v < \<delta> s' v'
[PROOF STEP]
using new_root
[PROOF STATE]
proof (prove)
using this:
tree_edges s' = tree_edges s
\<forall>(v, v')\<in>tree_edges s. v \<noteq> v0 \<and> v' \<noteq> v0
\<forall>(v, v')\<in>tree_edges s. \<delta> s v < \<delta> s v'
cond s
DFS_invar G param s
DFS_invar G param s'
stack s = []
v0 \<notin> dom (discovered s)
v0 \<in> V0
s' = new_root v0 s\<lparr>state.more := e_\<rparr>

goal (1 subgoal):
 1. \<forall>(v, v')\<in>tree_edges s'. \<delta> s' v < \<delta> s' v'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>(v, v')\<in>tree_edges s'. \<delta> s' v < \<delta> s' v'

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


[STATEMENT]
lemma tree_edge_disc:
    "(v,w) \<in> tree_edges s \<Longrightarrow> \<delta> s v < \<delta> s w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (v, w) \<in> tree_edges s \<Longrightarrow> \<delta> s v < \<delta> s w
[PROOF STEP]
using i_tree_edge_disc[THEN make_invar_thm]
[PROOF STATE]
proof (prove)
using this:
\<forall>(v, v')\<in>tree_edges s. \<delta> s v < \<delta> s v'

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


[STATEMENT]
lemma tree_path_disc:
    "(v,w) \<in> (tree_edges s)\<^sup>+ \<Longrightarrow> \<delta> s v < \<delta> s w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (v, w) \<in> (tree_edges s)\<^sup>+ \<Longrightarrow> \<delta> s v < \<delta> s w
[PROOF STEP]
by (auto elim!: trancl_induct dest: tree_edge_disc)


[STATEMENT]
lemma no_loop_in_tree:
    "(v,v) \<notin> (tree_edges s)\<^sup>+"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (v, v) \<notin> (tree_edges s)\<^sup>+
[PROOF STEP]
using tree_path_disc
[PROOF STATE]
proof (prove)
using this:
(?v, ?w) \<in> (tree_edges s)\<^sup>+ \<Longrightarrow> \<delta> s ?v < \<delta> s ?w

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


[STATEMENT]
lemma tree_acyclic:
    "acyclic (tree_edges s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. acyclic (tree_edges s)
[PROOF STEP]
by (metis acyclicI no_loop_in_tree)


[STATEMENT]
lemma no_self_loop_in_tree:
    "(v,v) \<notin> tree_edges s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (v, v) \<notin> tree_edges s
[PROOF STEP]
using tree_edge_disc
[PROOF STATE]
proof (prove)
using this:
(?v, ?w) \<in> tree_edges s \<Longrightarrow> \<delta> s ?v < \<delta> s ?w

goal (1 subgoal):
 1. (v, v) \<notin> tree_edges s
[PROOF STEP]
by auto


[STATEMENT]
lemma tree_edge_unequal:
    "(v,w) \<in> tree_edges s \<Longrightarrow> v \<noteq> w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (v, w) \<in> tree_edges s \<Longrightarrow> v \<noteq> w
[PROOF STEP]
by (metis no_self_loop_in_tree)


[STATEMENT]
lemma tree_path_unequal:
    "(v,w) \<in> (tree_edges s)\<^sup>+ \<Longrightarrow> v \<noteq> w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (v, w) \<in> (tree_edges s)\<^sup>+ \<Longrightarrow> v \<noteq> w
[PROOF STEP]
by (metis no_loop_in_tree)