[STATEMENT]
lemma i_edges_basic:
    "is_invar edges_basic"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_invar edges_basic
[PROOF STEP]
unfolding edges_basic_def[abs_def]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_invar (\<lambda>s. Field (back_edges s) \<subseteq> dom (discovered s) \<and> back_edges s \<subseteq> E - pending s \<and> Field (cross_edges s) \<subseteq> dom (discovered s) \<and> cross_edges s \<subseteq> E - pending s \<and> Field (tree_edges s) \<subseteq> dom (discovered s) \<and> tree_edges s \<subseteq> E - pending s \<and> back_edges s \<inter> cross_edges s = {} \<and> back_edges s \<inter> tree_edges s = {} \<and> cross_edges s \<inter> tree_edges s = {})
[PROOF STEP]
proof (induct rule: is_invarI_full)
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>e. Field (back_edges (empty_state e)) \<subseteq> dom (discovered (empty_state e)) \<and> back_edges (empty_state e) \<subseteq> E - pending (empty_state e) \<and> Field (cross_edges (empty_state e)) \<subseteq> dom (discovered (empty_state e)) \<and> cross_edges (empty_state e) \<subseteq> E - pending (empty_state e) \<and> Field (tree_edges (empty_state e)) \<subseteq> dom (discovered (empty_state e)) \<and> tree_edges (empty_state e) \<subseteq> E - pending (empty_state e) \<and> back_edges (empty_state e) \<inter> cross_edges (empty_state e) = {} \<and> back_edges (empty_state e) \<inter> tree_edges (empty_state e) = {} \<and> cross_edges (empty_state e) \<inter> tree_edges (empty_state e) = {}
 2. \<And>s s' v0 e. \<lbrakk>Field (back_edges s) \<subseteq> dom (discovered s) \<and> back_edges s \<subseteq> E - pending s \<and> Field (cross_edges s) \<subseteq> dom (discovered s) \<and> cross_edges s \<subseteq> E - pending s \<and> Field (tree_edges s) \<subseteq> dom (discovered s) \<and> tree_edges s \<subseteq> E - pending s \<and> back_edges s \<inter> cross_edges s = {} \<and> back_edges s \<inter> tree_edges s = {} \<and> cross_edges s \<inter> 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> Field (back_edges s') \<subseteq> dom (discovered s') \<and> back_edges s' \<subseteq> E - pending s' \<and> Field (cross_edges s') \<subseteq> dom (discovered s') \<and> cross_edges s' \<subseteq> E - pending s' \<and> Field (tree_edges s') \<subseteq> dom (discovered s') \<and> tree_edges s' \<subseteq> E - pending s' \<and> back_edges s' \<inter> cross_edges s' = {} \<and> back_edges s' \<inter> tree_edges s' = {} \<and> cross_edges s' \<inter> tree_edges s' = {}
 3. \<And>s s' u e. \<lbrakk>Field (back_edges s) \<subseteq> dom (discovered s) \<and> back_edges s \<subseteq> E - pending s \<and> Field (cross_edges s) \<subseteq> dom (discovered s) \<and> cross_edges s \<subseteq> E - pending s \<and> Field (tree_edges s) \<subseteq> dom (discovered s) \<and> tree_edges s \<subseteq> E - pending s \<and> back_edges s \<inter> cross_edges s = {} \<and> back_edges s \<inter> tree_edges s = {} \<and> cross_edges s \<inter> 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> Field (back_edges s') \<subseteq> dom (discovered s') \<and> back_edges s' \<subseteq> E - pending s' \<and> Field (cross_edges s') \<subseteq> dom (discovered s') \<and> cross_edges s' \<subseteq> E - pending s' \<and> Field (tree_edges s') \<subseteq> dom (discovered s') \<and> tree_edges s' \<subseteq> E - pending s' \<and> back_edges s' \<inter> cross_edges s' = {} \<and> back_edges s' \<inter> tree_edges s' = {} \<and> cross_edges s' \<inter> tree_edges s' = {}
 4. \<And>s s' u v e. \<lbrakk>Field (back_edges s) \<subseteq> dom (discovered s) \<and> back_edges s \<subseteq> E - pending s \<and> Field (cross_edges s) \<subseteq> dom (discovered s) \<and> cross_edges s \<subseteq> E - pending s \<and> Field (tree_edges s) \<subseteq> dom (discovered s) \<and> tree_edges s \<subseteq> E - pending s \<and> back_edges s \<inter> cross_edges s = {} \<and> back_edges s \<inter> tree_edges s = {} \<and> cross_edges s \<inter> 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); v \<in> dom (finished s); u = hd (stack s); s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> Field (back_edges s') \<subseteq> dom (discovered s') \<and> back_edges s' \<subseteq> E - pending s' \<and> Field (cross_edges s') \<subseteq> dom (discovered s') \<and> cross_edges s' \<subseteq> E - pending s' \<and> Field (tree_edges s') \<subseteq> dom (discovered s') \<and> tree_edges s' \<subseteq> E - pending s' \<and> back_edges s' \<inter> cross_edges s' = {} \<and> back_edges s' \<inter> tree_edges s' = {} \<and> cross_edges s' \<inter> tree_edges s' = {}
 5. \<And>s s' u v e. \<lbrakk>Field (back_edges s) \<subseteq> dom (discovered s) \<and> back_edges s \<subseteq> E - pending s \<and> Field (cross_edges s) \<subseteq> dom (discovered s) \<and> cross_edges s \<subseteq> E - pending s \<and> Field (tree_edges s) \<subseteq> dom (discovered s) \<and> tree_edges s \<subseteq> E - pending s \<and> back_edges s \<inter> cross_edges s = {} \<and> back_edges s \<inter> tree_edges s = {} \<and> cross_edges s \<inter> 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); v \<notin> dom (finished s); u = hd (stack s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> Field (back_edges s') \<subseteq> dom (discovered s') \<and> back_edges s' \<subseteq> E - pending s' \<and> Field (cross_edges s') \<subseteq> dom (discovered s') \<and> cross_edges s' \<subseteq> E - pending s' \<and> Field (tree_edges s') \<subseteq> dom (discovered s') \<and> tree_edges s' \<subseteq> E - pending s' \<and> back_edges s' \<inter> cross_edges s' = {} \<and> back_edges s' \<inter> tree_edges s' = {} \<and> cross_edges s' \<inter> tree_edges s' = {}
 6. \<And>s s' u v e. \<lbrakk>Field (back_edges s) \<subseteq> dom (discovered s) \<and> back_edges s \<subseteq> E - pending s \<and> Field (cross_edges s) \<subseteq> dom (discovered s) \<and> cross_edges s \<subseteq> E - pending s \<and> Field (tree_edges s) \<subseteq> dom (discovered s) \<and> tree_edges s \<subseteq> E - pending s \<and> back_edges s \<inter> cross_edges s = {} \<and> back_edges s \<inter> tree_edges s = {} \<and> cross_edges s \<inter> 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> Field (back_edges s') \<subseteq> dom (discovered s') \<and> back_edges s' \<subseteq> E - pending s' \<and> Field (cross_edges s') \<subseteq> dom (discovered s') \<and> cross_edges s' \<subseteq> E - pending s' \<and> Field (tree_edges s') \<subseteq> dom (discovered s') \<and> tree_edges s' \<subseteq> E - pending s' \<and> back_edges s' \<inter> cross_edges s' = {} \<and> back_edges s' \<inter> tree_edges s' = {} \<and> cross_edges s' \<inter> tree_edges s' = {}
[PROOF STEP]
case (back_edge s)
[PROOF STATE]
proof (state)
this:
Field (back_edges s) \<subseteq> dom (discovered s) \<and> back_edges s \<subseteq> E - pending s \<and> Field (cross_edges s) \<subseteq> dom (discovered s) \<and> cross_edges s \<subseteq> E - pending s \<and> Field (tree_edges s) \<subseteq> dom (discovered s) \<and> tree_edges s \<subseteq> E - pending s \<and> back_edges s \<inter> cross_edges s = {} \<and> back_edges s \<inter> tree_edges s = {} \<and> cross_edges s \<inter> 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)
v_ \<notin> dom (finished s)
u_ = hd (stack s)
s'_ = back_edge u_ v_ (s\<lparr>pending := pending s - {(u_, v_)}\<rparr>)\<lparr>state.more := e_\<rparr>

goal (6 subgoals):
 1. \<And>e. Field (back_edges (empty_state e)) \<subseteq> dom (discovered (empty_state e)) \<and> back_edges (empty_state e) \<subseteq> E - pending (empty_state e) \<and> Field (cross_edges (empty_state e)) \<subseteq> dom (discovered (empty_state e)) \<and> cross_edges (empty_state e) \<subseteq> E - pending (empty_state e) \<and> Field (tree_edges (empty_state e)) \<subseteq> dom (discovered (empty_state e)) \<and> tree_edges (empty_state e) \<subseteq> E - pending (empty_state e) \<and> back_edges (empty_state e) \<inter> cross_edges (empty_state e) = {} \<and> back_edges (empty_state e) \<inter> tree_edges (empty_state e) = {} \<and> cross_edges (empty_state e) \<inter> tree_edges (empty_state e) = {}
 2. \<And>s s' v0 e. \<lbrakk>Field (back_edges s) \<subseteq> dom (discovered s) \<and> back_edges s \<subseteq> E - pending s \<and> Field (cross_edges s) \<subseteq> dom (discovered s) \<and> cross_edges s \<subseteq> E - pending s \<and> Field (tree_edges s) \<subseteq> dom (discovered s) \<and> tree_edges s \<subseteq> E - pending s \<and> back_edges s \<inter> cross_edges s = {} \<and> back_edges s \<inter> tree_edges s = {} \<and> cross_edges s \<inter> 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> Field (back_edges s') \<subseteq> dom (discovered s') \<and> back_edges s' \<subseteq> E - pending s' \<and> Field (cross_edges s') \<subseteq> dom (discovered s') \<and> cross_edges s' \<subseteq> E - pending s' \<and> Field (tree_edges s') \<subseteq> dom (discovered s') \<and> tree_edges s' \<subseteq> E - pending s' \<and> back_edges s' \<inter> cross_edges s' = {} \<and> back_edges s' \<inter> tree_edges s' = {} \<and> cross_edges s' \<inter> tree_edges s' = {}
 3. \<And>s s' u e. \<lbrakk>Field (back_edges s) \<subseteq> dom (discovered s) \<and> back_edges s \<subseteq> E - pending s \<and> Field (cross_edges s) \<subseteq> dom (discovered s) \<and> cross_edges s \<subseteq> E - pending s \<and> Field (tree_edges s) \<subseteq> dom (discovered s) \<and> tree_edges s \<subseteq> E - pending s \<and> back_edges s \<inter> cross_edges s = {} \<and> back_edges s \<inter> tree_edges s = {} \<and> cross_edges s \<inter> 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> Field (back_edges s') \<subseteq> dom (discovered s') \<and> back_edges s' \<subseteq> E - pending s' \<and> Field (cross_edges s') \<subseteq> dom (discovered s') \<and> cross_edges s' \<subseteq> E - pending s' \<and> Field (tree_edges s') \<subseteq> dom (discovered s') \<and> tree_edges s' \<subseteq> E - pending s' \<and> back_edges s' \<inter> cross_edges s' = {} \<and> back_edges s' \<inter> tree_edges s' = {} \<and> cross_edges s' \<inter> tree_edges s' = {}
 4. \<And>s s' u v e. \<lbrakk>Field (back_edges s) \<subseteq> dom (discovered s) \<and> back_edges s \<subseteq> E - pending s \<and> Field (cross_edges s) \<subseteq> dom (discovered s) \<and> cross_edges s \<subseteq> E - pending s \<and> Field (tree_edges s) \<subseteq> dom (discovered s) \<and> tree_edges s \<subseteq> E - pending s \<and> back_edges s \<inter> cross_edges s = {} \<and> back_edges s \<inter> tree_edges s = {} \<and> cross_edges s \<inter> 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); v \<in> dom (finished s); u = hd (stack s); s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> Field (back_edges s') \<subseteq> dom (discovered s') \<and> back_edges s' \<subseteq> E - pending s' \<and> Field (cross_edges s') \<subseteq> dom (discovered s') \<and> cross_edges s' \<subseteq> E - pending s' \<and> Field (tree_edges s') \<subseteq> dom (discovered s') \<and> tree_edges s' \<subseteq> E - pending s' \<and> back_edges s' \<inter> cross_edges s' = {} \<and> back_edges s' \<inter> tree_edges s' = {} \<and> cross_edges s' \<inter> tree_edges s' = {}
 5. \<And>s s' u v e. \<lbrakk>Field (back_edges s) \<subseteq> dom (discovered s) \<and> back_edges s \<subseteq> E - pending s \<and> Field (cross_edges s) \<subseteq> dom (discovered s) \<and> cross_edges s \<subseteq> E - pending s \<and> Field (tree_edges s) \<subseteq> dom (discovered s) \<and> tree_edges s \<subseteq> E - pending s \<and> back_edges s \<inter> cross_edges s = {} \<and> back_edges s \<inter> tree_edges s = {} \<and> cross_edges s \<inter> 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); v \<notin> dom (finished s); u = hd (stack s); s' = back_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> Field (back_edges s') \<subseteq> dom (discovered s') \<and> back_edges s' \<subseteq> E - pending s' \<and> Field (cross_edges s') \<subseteq> dom (discovered s') \<and> cross_edges s' \<subseteq> E - pending s' \<and> Field (tree_edges s') \<subseteq> dom (discovered s') \<and> tree_edges s' \<subseteq> E - pending s' \<and> back_edges s' \<inter> cross_edges s' = {} \<and> back_edges s' \<inter> tree_edges s' = {} \<and> cross_edges s' \<inter> tree_edges s' = {}
 6. \<And>s s' u v e. \<lbrakk>Field (back_edges s) \<subseteq> dom (discovered s) \<and> back_edges s \<subseteq> E - pending s \<and> Field (cross_edges s) \<subseteq> dom (discovered s) \<and> cross_edges s \<subseteq> E - pending s \<and> Field (tree_edges s) \<subseteq> dom (discovered s) \<and> tree_edges s \<subseteq> E - pending s \<and> back_edges s \<inter> cross_edges s = {} \<and> back_edges s \<inter> tree_edges s = {} \<and> cross_edges s \<inter> 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> Field (back_edges s') \<subseteq> dom (discovered s') \<and> back_edges s' \<subseteq> E - pending s' \<and> Field (cross_edges s') \<subseteq> dom (discovered s') \<and> cross_edges s' \<subseteq> E - pending s' \<and> Field (tree_edges s') \<subseteq> dom (discovered s') \<and> tree_edges s' \<subseteq> E - pending s' \<and> back_edges s' \<inter> cross_edges s' = {} \<and> back_edges s' \<inter> tree_edges s' = {} \<and> cross_edges s' \<inter> tree_edges s' = {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Field (back_edges s) \<subseteq> dom (discovered s) \<and> back_edges s \<subseteq> E - pending s \<and> Field (cross_edges s) \<subseteq> dom (discovered s) \<and> cross_edges s \<subseteq> E - pending s \<and> Field (tree_edges s) \<subseteq> dom (discovered s) \<and> tree_edges s \<subseteq> E - pending s \<and> back_edges s \<inter> cross_edges s = {} \<and> back_edges s \<inter> tree_edges s = {} \<and> cross_edges s \<inter> 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)
v_ \<notin> dom (finished s)
u_ = hd (stack s)
s'_ = back_edge u_ v_ (s\<lparr>pending := pending s - {(u_, v_)}\<rparr>)\<lparr>state.more := e_\<rparr>
[PROOF STEP]
interpret DFS_invar where s=s
[PROOF STATE]
proof (prove)
using this:
Field (back_edges s) \<subseteq> dom (discovered s) \<and> back_edges s \<subseteq> E - pending s \<and> Field (cross_edges s) \<subseteq> dom (discovered s) \<and> cross_edges s \<subseteq> E - pending s \<and> Field (tree_edges s) \<subseteq> dom (discovered s) \<and> tree_edges s \<subseteq> E - pending s \<and> back_edges s \<inter> cross_edges s = {} \<and> back_edges s \<inter> tree_edges s = {} \<and> cross_edges s \<inter> 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)
v_ \<notin> dom (finished s)
u_ = hd (stack s)
s'_ = back_edge u_ v_ (s\<lparr>pending := pending s - {(u_, v_)}\<rparr>)\<lparr>state.more := e_\<rparr>

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

goal (1 subgoal):
 1. Field (back_edges s'_) \<subseteq> dom (discovered s'_) \<and> back_edges s'_ \<subseteq> E - pending s'_ \<and> Field (cross_edges s'_) \<subseteq> dom (discovered s'_) \<and> cross_edges s'_ \<subseteq> E - pending s'_ \<and> Field (tree_edges s'_) \<subseteq> dom (discovered s'_) \<and> tree_edges s'_ \<subseteq> E - pending s'_ \<and> back_edges s'_ \<inter> cross_edges s'_ = {} \<and> back_edges s'_ \<inter> tree_edges s'_ = {} \<and> cross_edges s'_ \<inter> tree_edges s'_ = {}
[PROOF STEP]
by (auto dest: pendingD)
[PROOF STATE]
proof (state)
this:
Field (back_edges s'_) \<subseteq> dom (discovered s'_) \<and> back_edges s'_ \<subseteq> E - pending s'_ \<and> Field (cross_edges s'_) \<subseteq> dom (discovered s'_) \<and> cross_edges s'_ \<subseteq> E - pending s'_ \<and> Field (tree_edges s'_) \<subseteq> dom (discovered s'_) \<and> tree_edges s'_ \<subseteq> E - pending s'_ \<and> back_edges s'_ \<inter> cross_edges s'_ = {} \<and> back_edges s'_ \<inter> tree_edges s'_ = {} \<and> cross_edges s'_ \<inter> tree_edges s'_ = {}

goal (5 subgoals):
 1. \<And>e. Field (back_edges (empty_state e)) \<subseteq> dom (discovered (empty_state e)) \<and> back_edges (empty_state e) \<subseteq> E - pending (empty_state e) \<and> Field (cross_edges (empty_state e)) \<subseteq> dom (discovered (empty_state e)) \<and> cross_edges (empty_state e) \<subseteq> E - pending (empty_state e) \<and> Field (tree_edges (empty_state e)) \<subseteq> dom (discovered (empty_state e)) \<and> tree_edges (empty_state e) \<subseteq> E - pending (empty_state e) \<and> back_edges (empty_state e) \<inter> cross_edges (empty_state e) = {} \<and> back_edges (empty_state e) \<inter> tree_edges (empty_state e) = {} \<and> cross_edges (empty_state e) \<inter> tree_edges (empty_state e) = {}
 2. \<And>s s' v0 e. \<lbrakk>Field (back_edges s) \<subseteq> dom (discovered s) \<and> back_edges s \<subseteq> E - pending s \<and> Field (cross_edges s) \<subseteq> dom (discovered s) \<and> cross_edges s \<subseteq> E - pending s \<and> Field (tree_edges s) \<subseteq> dom (discovered s) \<and> tree_edges s \<subseteq> E - pending s \<and> back_edges s \<inter> cross_edges s = {} \<and> back_edges s \<inter> tree_edges s = {} \<and> cross_edges s \<inter> 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> Field (back_edges s') \<subseteq> dom (discovered s') \<and> back_edges s' \<subseteq> E - pending s' \<and> Field (cross_edges s') \<subseteq> dom (discovered s') \<and> cross_edges s' \<subseteq> E - pending s' \<and> Field (tree_edges s') \<subseteq> dom (discovered s') \<and> tree_edges s' \<subseteq> E - pending s' \<and> back_edges s' \<inter> cross_edges s' = {} \<and> back_edges s' \<inter> tree_edges s' = {} \<and> cross_edges s' \<inter> tree_edges s' = {}
 3. \<And>s s' u e. \<lbrakk>Field (back_edges s) \<subseteq> dom (discovered s) \<and> back_edges s \<subseteq> E - pending s \<and> Field (cross_edges s) \<subseteq> dom (discovered s) \<and> cross_edges s \<subseteq> E - pending s \<and> Field (tree_edges s) \<subseteq> dom (discovered s) \<and> tree_edges s \<subseteq> E - pending s \<and> back_edges s \<inter> cross_edges s = {} \<and> back_edges s \<inter> tree_edges s = {} \<and> cross_edges s \<inter> 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> Field (back_edges s') \<subseteq> dom (discovered s') \<and> back_edges s' \<subseteq> E - pending s' \<and> Field (cross_edges s') \<subseteq> dom (discovered s') \<and> cross_edges s' \<subseteq> E - pending s' \<and> Field (tree_edges s') \<subseteq> dom (discovered s') \<and> tree_edges s' \<subseteq> E - pending s' \<and> back_edges s' \<inter> cross_edges s' = {} \<and> back_edges s' \<inter> tree_edges s' = {} \<and> cross_edges s' \<inter> tree_edges s' = {}
 4. \<And>s s' u v e. \<lbrakk>Field (back_edges s) \<subseteq> dom (discovered s) \<and> back_edges s \<subseteq> E - pending s \<and> Field (cross_edges s) \<subseteq> dom (discovered s) \<and> cross_edges s \<subseteq> E - pending s \<and> Field (tree_edges s) \<subseteq> dom (discovered s) \<and> tree_edges s \<subseteq> E - pending s \<and> back_edges s \<inter> cross_edges s = {} \<and> back_edges s \<inter> tree_edges s = {} \<and> cross_edges s \<inter> 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); v \<in> dom (finished s); u = hd (stack s); s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> Field (back_edges s') \<subseteq> dom (discovered s') \<and> back_edges s' \<subseteq> E - pending s' \<and> Field (cross_edges s') \<subseteq> dom (discovered s') \<and> cross_edges s' \<subseteq> E - pending s' \<and> Field (tree_edges s') \<subseteq> dom (discovered s') \<and> tree_edges s' \<subseteq> E - pending s' \<and> back_edges s' \<inter> cross_edges s' = {} \<and> back_edges s' \<inter> tree_edges s' = {} \<and> cross_edges s' \<inter> tree_edges s' = {}
 5. \<And>s s' u v e. \<lbrakk>Field (back_edges s) \<subseteq> dom (discovered s) \<and> back_edges s \<subseteq> E - pending s \<and> Field (cross_edges s) \<subseteq> dom (discovered s) \<and> cross_edges s \<subseteq> E - pending s \<and> Field (tree_edges s) \<subseteq> dom (discovered s) \<and> tree_edges s \<subseteq> E - pending s \<and> back_edges s \<inter> cross_edges s = {} \<and> back_edges s \<inter> tree_edges s = {} \<and> cross_edges s \<inter> 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> Field (back_edges s') \<subseteq> dom (discovered s') \<and> back_edges s' \<subseteq> E - pending s' \<and> Field (cross_edges s') \<subseteq> dom (discovered s') \<and> cross_edges s' \<subseteq> E - pending s' \<and> Field (tree_edges s') \<subseteq> dom (discovered s') \<and> tree_edges s' \<subseteq> E - pending s' \<and> back_edges s' \<inter> cross_edges s' = {} \<and> back_edges s' \<inter> tree_edges s' = {} \<and> cross_edges s' \<inter> tree_edges s' = {}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>e. Field (back_edges (empty_state e)) \<subseteq> dom (discovered (empty_state e)) \<and> back_edges (empty_state e) \<subseteq> E - pending (empty_state e) \<and> Field (cross_edges (empty_state e)) \<subseteq> dom (discovered (empty_state e)) \<and> cross_edges (empty_state e) \<subseteq> E - pending (empty_state e) \<and> Field (tree_edges (empty_state e)) \<subseteq> dom (discovered (empty_state e)) \<and> tree_edges (empty_state e) \<subseteq> E - pending (empty_state e) \<and> back_edges (empty_state e) \<inter> cross_edges (empty_state e) = {} \<and> back_edges (empty_state e) \<inter> tree_edges (empty_state e) = {} \<and> cross_edges (empty_state e) \<inter> tree_edges (empty_state e) = {}
 2. \<And>s s' v0 e. \<lbrakk>Field (back_edges s) \<subseteq> dom (discovered s) \<and> back_edges s \<subseteq> E - pending s \<and> Field (cross_edges s) \<subseteq> dom (discovered s) \<and> cross_edges s \<subseteq> E - pending s \<and> Field (tree_edges s) \<subseteq> dom (discovered s) \<and> tree_edges s \<subseteq> E - pending s \<and> back_edges s \<inter> cross_edges s = {} \<and> back_edges s \<inter> tree_edges s = {} \<and> cross_edges s \<inter> 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> Field (back_edges s') \<subseteq> dom (discovered s') \<and> back_edges s' \<subseteq> E - pending s' \<and> Field (cross_edges s') \<subseteq> dom (discovered s') \<and> cross_edges s' \<subseteq> E - pending s' \<and> Field (tree_edges s') \<subseteq> dom (discovered s') \<and> tree_edges s' \<subseteq> E - pending s' \<and> back_edges s' \<inter> cross_edges s' = {} \<and> back_edges s' \<inter> tree_edges s' = {} \<and> cross_edges s' \<inter> tree_edges s' = {}
 3. \<And>s s' u e. \<lbrakk>Field (back_edges s) \<subseteq> dom (discovered s) \<and> back_edges s \<subseteq> E - pending s \<and> Field (cross_edges s) \<subseteq> dom (discovered s) \<and> cross_edges s \<subseteq> E - pending s \<and> Field (tree_edges s) \<subseteq> dom (discovered s) \<and> tree_edges s \<subseteq> E - pending s \<and> back_edges s \<inter> cross_edges s = {} \<and> back_edges s \<inter> tree_edges s = {} \<and> cross_edges s \<inter> 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> Field (back_edges s') \<subseteq> dom (discovered s') \<and> back_edges s' \<subseteq> E - pending s' \<and> Field (cross_edges s') \<subseteq> dom (discovered s') \<and> cross_edges s' \<subseteq> E - pending s' \<and> Field (tree_edges s') \<subseteq> dom (discovered s') \<and> tree_edges s' \<subseteq> E - pending s' \<and> back_edges s' \<inter> cross_edges s' = {} \<and> back_edges s' \<inter> tree_edges s' = {} \<and> cross_edges s' \<inter> tree_edges s' = {}
 4. \<And>s s' u v e. \<lbrakk>Field (back_edges s) \<subseteq> dom (discovered s) \<and> back_edges s \<subseteq> E - pending s \<and> Field (cross_edges s) \<subseteq> dom (discovered s) \<and> cross_edges s \<subseteq> E - pending s \<and> Field (tree_edges s) \<subseteq> dom (discovered s) \<and> tree_edges s \<subseteq> E - pending s \<and> back_edges s \<inter> cross_edges s = {} \<and> back_edges s \<inter> tree_edges s = {} \<and> cross_edges s \<inter> 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); v \<in> dom (finished s); u = hd (stack s); s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> Field (back_edges s') \<subseteq> dom (discovered s') \<and> back_edges s' \<subseteq> E - pending s' \<and> Field (cross_edges s') \<subseteq> dom (discovered s') \<and> cross_edges s' \<subseteq> E - pending s' \<and> Field (tree_edges s') \<subseteq> dom (discovered s') \<and> tree_edges s' \<subseteq> E - pending s' \<and> back_edges s' \<inter> cross_edges s' = {} \<and> back_edges s' \<inter> tree_edges s' = {} \<and> cross_edges s' \<inter> tree_edges s' = {}
 5. \<And>s s' u v e. \<lbrakk>Field (back_edges s) \<subseteq> dom (discovered s) \<and> back_edges s \<subseteq> E - pending s \<and> Field (cross_edges s) \<subseteq> dom (discovered s) \<and> cross_edges s \<subseteq> E - pending s \<and> Field (tree_edges s) \<subseteq> dom (discovered s) \<and> tree_edges s \<subseteq> E - pending s \<and> back_edges s \<inter> cross_edges s = {} \<and> back_edges s \<inter> tree_edges s = {} \<and> cross_edges s \<inter> 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> Field (back_edges s') \<subseteq> dom (discovered s') \<and> back_edges s' \<subseteq> E - pending s' \<and> Field (cross_edges s') \<subseteq> dom (discovered s') \<and> cross_edges s' \<subseteq> E - pending s' \<and> Field (tree_edges s') \<subseteq> dom (discovered s') \<and> tree_edges s' \<subseteq> E - pending s' \<and> back_edges s' \<inter> cross_edges s' = {} \<and> back_edges s' \<inter> tree_edges s' = {} \<and> cross_edges s' \<inter> tree_edges s' = {}
[PROOF STEP]
case (cross_edge s)
[PROOF STATE]
proof (state)
this:
Field (back_edges s) \<subseteq> dom (discovered s) \<and> back_edges s \<subseteq> E - pending s \<and> Field (cross_edges s) \<subseteq> dom (discovered s) \<and> cross_edges s \<subseteq> E - pending s \<and> Field (tree_edges s) \<subseteq> dom (discovered s) \<and> tree_edges s \<subseteq> E - pending s \<and> back_edges s \<inter> cross_edges s = {} \<and> back_edges s \<inter> tree_edges s = {} \<and> cross_edges s \<inter> 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)
v_ \<in> dom (finished s)
u_ = hd (stack s)
s'_ = cross_edge u_ v_ (s\<lparr>pending := pending s - {(u_, v_)}\<rparr>)\<lparr>state.more := e_\<rparr>

goal (5 subgoals):
 1. \<And>e. Field (back_edges (empty_state e)) \<subseteq> dom (discovered (empty_state e)) \<and> back_edges (empty_state e) \<subseteq> E - pending (empty_state e) \<and> Field (cross_edges (empty_state e)) \<subseteq> dom (discovered (empty_state e)) \<and> cross_edges (empty_state e) \<subseteq> E - pending (empty_state e) \<and> Field (tree_edges (empty_state e)) \<subseteq> dom (discovered (empty_state e)) \<and> tree_edges (empty_state e) \<subseteq> E - pending (empty_state e) \<and> back_edges (empty_state e) \<inter> cross_edges (empty_state e) = {} \<and> back_edges (empty_state e) \<inter> tree_edges (empty_state e) = {} \<and> cross_edges (empty_state e) \<inter> tree_edges (empty_state e) = {}
 2. \<And>s s' v0 e. \<lbrakk>Field (back_edges s) \<subseteq> dom (discovered s) \<and> back_edges s \<subseteq> E - pending s \<and> Field (cross_edges s) \<subseteq> dom (discovered s) \<and> cross_edges s \<subseteq> E - pending s \<and> Field (tree_edges s) \<subseteq> dom (discovered s) \<and> tree_edges s \<subseteq> E - pending s \<and> back_edges s \<inter> cross_edges s = {} \<and> back_edges s \<inter> tree_edges s = {} \<and> cross_edges s \<inter> 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> Field (back_edges s') \<subseteq> dom (discovered s') \<and> back_edges s' \<subseteq> E - pending s' \<and> Field (cross_edges s') \<subseteq> dom (discovered s') \<and> cross_edges s' \<subseteq> E - pending s' \<and> Field (tree_edges s') \<subseteq> dom (discovered s') \<and> tree_edges s' \<subseteq> E - pending s' \<and> back_edges s' \<inter> cross_edges s' = {} \<and> back_edges s' \<inter> tree_edges s' = {} \<and> cross_edges s' \<inter> tree_edges s' = {}
 3. \<And>s s' u e. \<lbrakk>Field (back_edges s) \<subseteq> dom (discovered s) \<and> back_edges s \<subseteq> E - pending s \<and> Field (cross_edges s) \<subseteq> dom (discovered s) \<and> cross_edges s \<subseteq> E - pending s \<and> Field (tree_edges s) \<subseteq> dom (discovered s) \<and> tree_edges s \<subseteq> E - pending s \<and> back_edges s \<inter> cross_edges s = {} \<and> back_edges s \<inter> tree_edges s = {} \<and> cross_edges s \<inter> 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> Field (back_edges s') \<subseteq> dom (discovered s') \<and> back_edges s' \<subseteq> E - pending s' \<and> Field (cross_edges s') \<subseteq> dom (discovered s') \<and> cross_edges s' \<subseteq> E - pending s' \<and> Field (tree_edges s') \<subseteq> dom (discovered s') \<and> tree_edges s' \<subseteq> E - pending s' \<and> back_edges s' \<inter> cross_edges s' = {} \<and> back_edges s' \<inter> tree_edges s' = {} \<and> cross_edges s' \<inter> tree_edges s' = {}
 4. \<And>s s' u v e. \<lbrakk>Field (back_edges s) \<subseteq> dom (discovered s) \<and> back_edges s \<subseteq> E - pending s \<and> Field (cross_edges s) \<subseteq> dom (discovered s) \<and> cross_edges s \<subseteq> E - pending s \<and> Field (tree_edges s) \<subseteq> dom (discovered s) \<and> tree_edges s \<subseteq> E - pending s \<and> back_edges s \<inter> cross_edges s = {} \<and> back_edges s \<inter> tree_edges s = {} \<and> cross_edges s \<inter> 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); v \<in> dom (finished s); u = hd (stack s); s' = cross_edge u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> Field (back_edges s') \<subseteq> dom (discovered s') \<and> back_edges s' \<subseteq> E - pending s' \<and> Field (cross_edges s') \<subseteq> dom (discovered s') \<and> cross_edges s' \<subseteq> E - pending s' \<and> Field (tree_edges s') \<subseteq> dom (discovered s') \<and> tree_edges s' \<subseteq> E - pending s' \<and> back_edges s' \<inter> cross_edges s' = {} \<and> back_edges s' \<inter> tree_edges s' = {} \<and> cross_edges s' \<inter> tree_edges s' = {}
 5. \<And>s s' u v e. \<lbrakk>Field (back_edges s) \<subseteq> dom (discovered s) \<and> back_edges s \<subseteq> E - pending s \<and> Field (cross_edges s) \<subseteq> dom (discovered s) \<and> cross_edges s \<subseteq> E - pending s \<and> Field (tree_edges s) \<subseteq> dom (discovered s) \<and> tree_edges s \<subseteq> E - pending s \<and> back_edges s \<inter> cross_edges s = {} \<and> back_edges s \<inter> tree_edges s = {} \<and> cross_edges s \<inter> 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> Field (back_edges s') \<subseteq> dom (discovered s') \<and> back_edges s' \<subseteq> E - pending s' \<and> Field (cross_edges s') \<subseteq> dom (discovered s') \<and> cross_edges s' \<subseteq> E - pending s' \<and> Field (tree_edges s') \<subseteq> dom (discovered s') \<and> tree_edges s' \<subseteq> E - pending s' \<and> back_edges s' \<inter> cross_edges s' = {} \<and> back_edges s' \<inter> tree_edges s' = {} \<and> cross_edges s' \<inter> tree_edges s' = {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Field (back_edges s) \<subseteq> dom (discovered s) \<and> back_edges s \<subseteq> E - pending s \<and> Field (cross_edges s) \<subseteq> dom (discovered s) \<and> cross_edges s \<subseteq> E - pending s \<and> Field (tree_edges s) \<subseteq> dom (discovered s) \<and> tree_edges s \<subseteq> E - pending s \<and> back_edges s \<inter> cross_edges s = {} \<and> back_edges s \<inter> tree_edges s = {} \<and> cross_edges s \<inter> 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)
v_ \<in> dom (finished s)
u_ = hd (stack s)
s'_ = cross_edge u_ v_ (s\<lparr>pending := pending s - {(u_, v_)}\<rparr>)\<lparr>state.more := e_\<rparr>
[PROOF STEP]
interpret DFS_invar where s=s
[PROOF STATE]
proof (prove)
using this:
Field (back_edges s) \<subseteq> dom (discovered s) \<and> back_edges s \<subseteq> E - pending s \<and> Field (cross_edges s) \<subseteq> dom (discovered s) \<and> cross_edges s \<subseteq> E - pending s \<and> Field (tree_edges s) \<subseteq> dom (discovered s) \<and> tree_edges s \<subseteq> E - pending s \<and> back_edges s \<inter> cross_edges s = {} \<and> back_edges s \<inter> tree_edges s = {} \<and> cross_edges s \<inter> 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)
v_ \<in> dom (finished s)
u_ = hd (stack s)
s'_ = cross_edge u_ v_ (s\<lparr>pending := pending s - {(u_, v_)}\<rparr>)\<lparr>state.more := e_\<rparr>

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

goal (1 subgoal):
 1. Field (back_edges s'_) \<subseteq> dom (discovered s'_) \<and> back_edges s'_ \<subseteq> E - pending s'_ \<and> Field (cross_edges s'_) \<subseteq> dom (discovered s'_) \<and> cross_edges s'_ \<subseteq> E - pending s'_ \<and> Field (tree_edges s'_) \<subseteq> dom (discovered s'_) \<and> tree_edges s'_ \<subseteq> E - pending s'_ \<and> back_edges s'_ \<inter> cross_edges s'_ = {} \<and> back_edges s'_ \<inter> tree_edges s'_ = {} \<and> cross_edges s'_ \<inter> tree_edges s'_ = {}
[PROOF STEP]
by (auto dest: pendingD)
[PROOF STATE]
proof (state)
this:
Field (back_edges s'_) \<subseteq> dom (discovered s'_) \<and> back_edges s'_ \<subseteq> E - pending s'_ \<and> Field (cross_edges s'_) \<subseteq> dom (discovered s'_) \<and> cross_edges s'_ \<subseteq> E - pending s'_ \<and> Field (tree_edges s'_) \<subseteq> dom (discovered s'_) \<and> tree_edges s'_ \<subseteq> E - pending s'_ \<and> back_edges s'_ \<inter> cross_edges s'_ = {} \<and> back_edges s'_ \<inter> tree_edges s'_ = {} \<and> cross_edges s'_ \<inter> tree_edges s'_ = {}

goal (4 subgoals):
 1. \<And>e. Field (back_edges (empty_state e)) \<subseteq> dom (discovered (empty_state e)) \<and> back_edges (empty_state e) \<subseteq> E - pending (empty_state e) \<and> Field (cross_edges (empty_state e)) \<subseteq> dom (discovered (empty_state e)) \<and> cross_edges (empty_state e) \<subseteq> E - pending (empty_state e) \<and> Field (tree_edges (empty_state e)) \<subseteq> dom (discovered (empty_state e)) \<and> tree_edges (empty_state e) \<subseteq> E - pending (empty_state e) \<and> back_edges (empty_state e) \<inter> cross_edges (empty_state e) = {} \<and> back_edges (empty_state e) \<inter> tree_edges (empty_state e) = {} \<and> cross_edges (empty_state e) \<inter> tree_edges (empty_state e) = {}
 2. \<And>s s' v0 e. \<lbrakk>Field (back_edges s) \<subseteq> dom (discovered s) \<and> back_edges s \<subseteq> E - pending s \<and> Field (cross_edges s) \<subseteq> dom (discovered s) \<and> cross_edges s \<subseteq> E - pending s \<and> Field (tree_edges s) \<subseteq> dom (discovered s) \<and> tree_edges s \<subseteq> E - pending s \<and> back_edges s \<inter> cross_edges s = {} \<and> back_edges s \<inter> tree_edges s = {} \<and> cross_edges s \<inter> 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> Field (back_edges s') \<subseteq> dom (discovered s') \<and> back_edges s' \<subseteq> E - pending s' \<and> Field (cross_edges s') \<subseteq> dom (discovered s') \<and> cross_edges s' \<subseteq> E - pending s' \<and> Field (tree_edges s') \<subseteq> dom (discovered s') \<and> tree_edges s' \<subseteq> E - pending s' \<and> back_edges s' \<inter> cross_edges s' = {} \<and> back_edges s' \<inter> tree_edges s' = {} \<and> cross_edges s' \<inter> tree_edges s' = {}
 3. \<And>s s' u e. \<lbrakk>Field (back_edges s) \<subseteq> dom (discovered s) \<and> back_edges s \<subseteq> E - pending s \<and> Field (cross_edges s) \<subseteq> dom (discovered s) \<and> cross_edges s \<subseteq> E - pending s \<and> Field (tree_edges s) \<subseteq> dom (discovered s) \<and> tree_edges s \<subseteq> E - pending s \<and> back_edges s \<inter> cross_edges s = {} \<and> back_edges s \<inter> tree_edges s = {} \<and> cross_edges s \<inter> 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> Field (back_edges s') \<subseteq> dom (discovered s') \<and> back_edges s' \<subseteq> E - pending s' \<and> Field (cross_edges s') \<subseteq> dom (discovered s') \<and> cross_edges s' \<subseteq> E - pending s' \<and> Field (tree_edges s') \<subseteq> dom (discovered s') \<and> tree_edges s' \<subseteq> E - pending s' \<and> back_edges s' \<inter> cross_edges s' = {} \<and> back_edges s' \<inter> tree_edges s' = {} \<and> cross_edges s' \<inter> tree_edges s' = {}
 4. \<And>s s' u v e. \<lbrakk>Field (back_edges s) \<subseteq> dom (discovered s) \<and> back_edges s \<subseteq> E - pending s \<and> Field (cross_edges s) \<subseteq> dom (discovered s) \<and> cross_edges s \<subseteq> E - pending s \<and> Field (tree_edges s) \<subseteq> dom (discovered s) \<and> tree_edges s \<subseteq> E - pending s \<and> back_edges s \<inter> cross_edges s = {} \<and> back_edges s \<inter> tree_edges s = {} \<and> cross_edges s \<inter> 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> Field (back_edges s') \<subseteq> dom (discovered s') \<and> back_edges s' \<subseteq> E - pending s' \<and> Field (cross_edges s') \<subseteq> dom (discovered s') \<and> cross_edges s' \<subseteq> E - pending s' \<and> Field (tree_edges s') \<subseteq> dom (discovered s') \<and> tree_edges s' \<subseteq> E - pending s' \<and> back_edges s' \<inter> cross_edges s' = {} \<and> back_edges s' \<inter> tree_edges s' = {} \<and> cross_edges s' \<inter> tree_edges s' = {}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>e. Field (back_edges (empty_state e)) \<subseteq> dom (discovered (empty_state e)) \<and> back_edges (empty_state e) \<subseteq> E - pending (empty_state e) \<and> Field (cross_edges (empty_state e)) \<subseteq> dom (discovered (empty_state e)) \<and> cross_edges (empty_state e) \<subseteq> E - pending (empty_state e) \<and> Field (tree_edges (empty_state e)) \<subseteq> dom (discovered (empty_state e)) \<and> tree_edges (empty_state e) \<subseteq> E - pending (empty_state e) \<and> back_edges (empty_state e) \<inter> cross_edges (empty_state e) = {} \<and> back_edges (empty_state e) \<inter> tree_edges (empty_state e) = {} \<and> cross_edges (empty_state e) \<inter> tree_edges (empty_state e) = {}
 2. \<And>s s' v0 e. \<lbrakk>Field (back_edges s) \<subseteq> dom (discovered s) \<and> back_edges s \<subseteq> E - pending s \<and> Field (cross_edges s) \<subseteq> dom (discovered s) \<and> cross_edges s \<subseteq> E - pending s \<and> Field (tree_edges s) \<subseteq> dom (discovered s) \<and> tree_edges s \<subseteq> E - pending s \<and> back_edges s \<inter> cross_edges s = {} \<and> back_edges s \<inter> tree_edges s = {} \<and> cross_edges s \<inter> 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> Field (back_edges s') \<subseteq> dom (discovered s') \<and> back_edges s' \<subseteq> E - pending s' \<and> Field (cross_edges s') \<subseteq> dom (discovered s') \<and> cross_edges s' \<subseteq> E - pending s' \<and> Field (tree_edges s') \<subseteq> dom (discovered s') \<and> tree_edges s' \<subseteq> E - pending s' \<and> back_edges s' \<inter> cross_edges s' = {} \<and> back_edges s' \<inter> tree_edges s' = {} \<and> cross_edges s' \<inter> tree_edges s' = {}
 3. \<And>s s' u e. \<lbrakk>Field (back_edges s) \<subseteq> dom (discovered s) \<and> back_edges s \<subseteq> E - pending s \<and> Field (cross_edges s) \<subseteq> dom (discovered s) \<and> cross_edges s \<subseteq> E - pending s \<and> Field (tree_edges s) \<subseteq> dom (discovered s) \<and> tree_edges s \<subseteq> E - pending s \<and> back_edges s \<inter> cross_edges s = {} \<and> back_edges s \<inter> tree_edges s = {} \<and> cross_edges s \<inter> 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> Field (back_edges s') \<subseteq> dom (discovered s') \<and> back_edges s' \<subseteq> E - pending s' \<and> Field (cross_edges s') \<subseteq> dom (discovered s') \<and> cross_edges s' \<subseteq> E - pending s' \<and> Field (tree_edges s') \<subseteq> dom (discovered s') \<and> tree_edges s' \<subseteq> E - pending s' \<and> back_edges s' \<inter> cross_edges s' = {} \<and> back_edges s' \<inter> tree_edges s' = {} \<and> cross_edges s' \<inter> tree_edges s' = {}
 4. \<And>s s' u v e. \<lbrakk>Field (back_edges s) \<subseteq> dom (discovered s) \<and> back_edges s \<subseteq> E - pending s \<and> Field (cross_edges s) \<subseteq> dom (discovered s) \<and> cross_edges s \<subseteq> E - pending s \<and> Field (tree_edges s) \<subseteq> dom (discovered s) \<and> tree_edges s \<subseteq> E - pending s \<and> back_edges s \<inter> cross_edges s = {} \<and> back_edges s \<inter> tree_edges s = {} \<and> cross_edges s \<inter> 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> Field (back_edges s') \<subseteq> dom (discovered s') \<and> back_edges s' \<subseteq> E - pending s' \<and> Field (cross_edges s') \<subseteq> dom (discovered s') \<and> cross_edges s' \<subseteq> E - pending s' \<and> Field (tree_edges s') \<subseteq> dom (discovered s') \<and> tree_edges s' \<subseteq> E - pending s' \<and> back_edges s' \<inter> cross_edges s' = {} \<and> back_edges s' \<inter> tree_edges s' = {} \<and> cross_edges s' \<inter> tree_edges s' = {}
[PROOF STEP]
case (discover s)
[PROOF STATE]
proof (state)
this:
Field (back_edges s) \<subseteq> dom (discovered s) \<and> back_edges s \<subseteq> E - pending s \<and> Field (cross_edges s) \<subseteq> dom (discovered s) \<and> cross_edges s \<subseteq> E - pending s \<and> Field (tree_edges s) \<subseteq> dom (discovered s) \<and> tree_edges s \<subseteq> E - pending s \<and> back_edges s \<inter> cross_edges s = {} \<and> back_edges s \<inter> tree_edges s = {} \<and> cross_edges s \<inter> 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 (4 subgoals):
 1. \<And>e. Field (back_edges (empty_state e)) \<subseteq> dom (discovered (empty_state e)) \<and> back_edges (empty_state e) \<subseteq> E - pending (empty_state e) \<and> Field (cross_edges (empty_state e)) \<subseteq> dom (discovered (empty_state e)) \<and> cross_edges (empty_state e) \<subseteq> E - pending (empty_state e) \<and> Field (tree_edges (empty_state e)) \<subseteq> dom (discovered (empty_state e)) \<and> tree_edges (empty_state e) \<subseteq> E - pending (empty_state e) \<and> back_edges (empty_state e) \<inter> cross_edges (empty_state e) = {} \<and> back_edges (empty_state e) \<inter> tree_edges (empty_state e) = {} \<and> cross_edges (empty_state e) \<inter> tree_edges (empty_state e) = {}
 2. \<And>s s' v0 e. \<lbrakk>Field (back_edges s) \<subseteq> dom (discovered s) \<and> back_edges s \<subseteq> E - pending s \<and> Field (cross_edges s) \<subseteq> dom (discovered s) \<and> cross_edges s \<subseteq> E - pending s \<and> Field (tree_edges s) \<subseteq> dom (discovered s) \<and> tree_edges s \<subseteq> E - pending s \<and> back_edges s \<inter> cross_edges s = {} \<and> back_edges s \<inter> tree_edges s = {} \<and> cross_edges s \<inter> 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> Field (back_edges s') \<subseteq> dom (discovered s') \<and> back_edges s' \<subseteq> E - pending s' \<and> Field (cross_edges s') \<subseteq> dom (discovered s') \<and> cross_edges s' \<subseteq> E - pending s' \<and> Field (tree_edges s') \<subseteq> dom (discovered s') \<and> tree_edges s' \<subseteq> E - pending s' \<and> back_edges s' \<inter> cross_edges s' = {} \<and> back_edges s' \<inter> tree_edges s' = {} \<and> cross_edges s' \<inter> tree_edges s' = {}
 3. \<And>s s' u e. \<lbrakk>Field (back_edges s) \<subseteq> dom (discovered s) \<and> back_edges s \<subseteq> E - pending s \<and> Field (cross_edges s) \<subseteq> dom (discovered s) \<and> cross_edges s \<subseteq> E - pending s \<and> Field (tree_edges s) \<subseteq> dom (discovered s) \<and> tree_edges s \<subseteq> E - pending s \<and> back_edges s \<inter> cross_edges s = {} \<and> back_edges s \<inter> tree_edges s = {} \<and> cross_edges s \<inter> 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> Field (back_edges s') \<subseteq> dom (discovered s') \<and> back_edges s' \<subseteq> E - pending s' \<and> Field (cross_edges s') \<subseteq> dom (discovered s') \<and> cross_edges s' \<subseteq> E - pending s' \<and> Field (tree_edges s') \<subseteq> dom (discovered s') \<and> tree_edges s' \<subseteq> E - pending s' \<and> back_edges s' \<inter> cross_edges s' = {} \<and> back_edges s' \<inter> tree_edges s' = {} \<and> cross_edges s' \<inter> tree_edges s' = {}
 4. \<And>s s' u v e. \<lbrakk>Field (back_edges s) \<subseteq> dom (discovered s) \<and> back_edges s \<subseteq> E - pending s \<and> Field (cross_edges s) \<subseteq> dom (discovered s) \<and> cross_edges s \<subseteq> E - pending s \<and> Field (tree_edges s) \<subseteq> dom (discovered s) \<and> tree_edges s \<subseteq> E - pending s \<and> back_edges s \<inter> cross_edges s = {} \<and> back_edges s \<inter> tree_edges s = {} \<and> cross_edges s \<inter> 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> Field (back_edges s') \<subseteq> dom (discovered s') \<and> back_edges s' \<subseteq> E - pending s' \<and> Field (cross_edges s') \<subseteq> dom (discovered s') \<and> cross_edges s' \<subseteq> E - pending s' \<and> Field (tree_edges s') \<subseteq> dom (discovered s') \<and> tree_edges s' \<subseteq> E - pending s' \<and> back_edges s' \<inter> cross_edges s' = {} \<and> back_edges s' \<inter> tree_edges s' = {} \<and> cross_edges s' \<inter> tree_edges s' = {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Field (back_edges s) \<subseteq> dom (discovered s) \<and> back_edges s \<subseteq> E - pending s \<and> Field (cross_edges s) \<subseteq> dom (discovered s) \<and> cross_edges s \<subseteq> E - pending s \<and> Field (tree_edges s) \<subseteq> dom (discovered s) \<and> tree_edges s \<subseteq> E - pending s \<and> back_edges s \<inter> cross_edges s = {} \<and> back_edges s \<inter> tree_edges s = {} \<and> cross_edges s \<inter> 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:
Field (back_edges s) \<subseteq> dom (discovered s) \<and> back_edges s \<subseteq> E - pending s \<and> Field (cross_edges s) \<subseteq> dom (discovered s) \<and> cross_edges s \<subseteq> E - pending s \<and> Field (tree_edges s) \<subseteq> dom (discovered s) \<and> tree_edges s \<subseteq> E - pending s \<and> back_edges s \<inter> cross_edges s = {} \<and> back_edges s \<inter> tree_edges s = {} \<and> cross_edges s \<inter> 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 (4 subgoals):
 1. \<And>e. Field (back_edges (empty_state e)) \<subseteq> dom (discovered (empty_state e)) \<and> back_edges (empty_state e) \<subseteq> E - pending (empty_state e) \<and> Field (cross_edges (empty_state e)) \<subseteq> dom (discovered (empty_state e)) \<and> cross_edges (empty_state e) \<subseteq> E - pending (empty_state e) \<and> Field (tree_edges (empty_state e)) \<subseteq> dom (discovered (empty_state e)) \<and> tree_edges (empty_state e) \<subseteq> E - pending (empty_state e) \<and> back_edges (empty_state e) \<inter> cross_edges (empty_state e) = {} \<and> back_edges (empty_state e) \<inter> tree_edges (empty_state e) = {} \<and> cross_edges (empty_state e) \<inter> tree_edges (empty_state e) = {}
 2. \<And>s s' v0 e. \<lbrakk>Field (back_edges s) \<subseteq> dom (discovered s) \<and> back_edges s \<subseteq> E - pending s \<and> Field (cross_edges s) \<subseteq> dom (discovered s) \<and> cross_edges s \<subseteq> E - pending s \<and> Field (tree_edges s) \<subseteq> dom (discovered s) \<and> tree_edges s \<subseteq> E - pending s \<and> back_edges s \<inter> cross_edges s = {} \<and> back_edges s \<inter> tree_edges s = {} \<and> cross_edges s \<inter> 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> Field (back_edges s') \<subseteq> dom (discovered s') \<and> back_edges s' \<subseteq> E - pending s' \<and> Field (cross_edges s') \<subseteq> dom (discovered s') \<and> cross_edges s' \<subseteq> E - pending s' \<and> Field (tree_edges s') \<subseteq> dom (discovered s') \<and> tree_edges s' \<subseteq> E - pending s' \<and> back_edges s' \<inter> cross_edges s' = {} \<and> back_edges s' \<inter> tree_edges s' = {} \<and> cross_edges s' \<inter> tree_edges s' = {}
 3. \<And>s s' u e. \<lbrakk>Field (back_edges s) \<subseteq> dom (discovered s) \<and> back_edges s \<subseteq> E - pending s \<and> Field (cross_edges s) \<subseteq> dom (discovered s) \<and> cross_edges s \<subseteq> E - pending s \<and> Field (tree_edges s) \<subseteq> dom (discovered s) \<and> tree_edges s \<subseteq> E - pending s \<and> back_edges s \<inter> cross_edges s = {} \<and> back_edges s \<inter> tree_edges s = {} \<and> cross_edges s \<inter> 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> Field (back_edges s') \<subseteq> dom (discovered s') \<and> back_edges s' \<subseteq> E - pending s' \<and> Field (cross_edges s') \<subseteq> dom (discovered s') \<and> cross_edges s' \<subseteq> E - pending s' \<and> Field (tree_edges s') \<subseteq> dom (discovered s') \<and> tree_edges s' \<subseteq> E - pending s' \<and> back_edges s' \<inter> cross_edges s' = {} \<and> back_edges s' \<inter> tree_edges s' = {} \<and> cross_edges s' \<inter> tree_edges s' = {}
 4. \<And>s s' u v e. \<lbrakk>Field (back_edges s) \<subseteq> dom (discovered s) \<and> back_edges s \<subseteq> E - pending s \<and> Field (cross_edges s) \<subseteq> dom (discovered s) \<and> cross_edges s \<subseteq> E - pending s \<and> Field (tree_edges s) \<subseteq> dom (discovered s) \<and> tree_edges s \<subseteq> E - pending s \<and> back_edges s \<inter> cross_edges s = {} \<and> back_edges s \<inter> tree_edges s = {} \<and> cross_edges s \<inter> 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> Field (back_edges s') \<subseteq> dom (discovered s') \<and> back_edges s' \<subseteq> E - pending s' \<and> Field (cross_edges s') \<subseteq> dom (discovered s') \<and> cross_edges s' \<subseteq> E - pending s' \<and> Field (tree_edges s') \<subseteq> dom (discovered s') \<and> tree_edges s' \<subseteq> E - pending s' \<and> back_edges s' \<inter> cross_edges s' = {} \<and> back_edges s' \<inter> tree_edges s' = {} \<and> cross_edges s' \<inter> tree_edges s' = {}
[PROOF STEP]
from discover
[PROOF STATE]
proof (chain)
picking this:
Field (back_edges s) \<subseteq> dom (discovered s) \<and> back_edges s \<subseteq> E - pending s \<and> Field (cross_edges s) \<subseteq> dom (discovered s) \<and> cross_edges s \<subseteq> E - pending s \<and> Field (tree_edges s) \<subseteq> dom (discovered s) \<and> tree_edges s \<subseteq> E - pending s \<and> back_edges s \<inter> cross_edges s = {} \<and> back_edges s \<inter> tree_edges s = {} \<and> cross_edges s \<inter> 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]
show ?case
[PROOF STATE]
proof (prove)
using this:
Field (back_edges s) \<subseteq> dom (discovered s) \<and> back_edges s \<subseteq> E - pending s \<and> Field (cross_edges s) \<subseteq> dom (discovered s) \<and> cross_edges s \<subseteq> E - pending s \<and> Field (tree_edges s) \<subseteq> dom (discovered s) \<and> tree_edges s \<subseteq> E - pending s \<and> back_edges s \<inter> cross_edges s = {} \<and> back_edges s \<inter> tree_edges s = {} \<and> cross_edges s \<inter> 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. Field (back_edges s'_) \<subseteq> dom (discovered s'_) \<and> back_edges s'_ \<subseteq> E - pending s'_ \<and> Field (cross_edges s'_) \<subseteq> dom (discovered s'_) \<and> cross_edges s'_ \<subseteq> E - pending s'_ \<and> Field (tree_edges s'_) \<subseteq> dom (discovered s'_) \<and> tree_edges s'_ \<subseteq> E - pending s'_ \<and> back_edges s'_ \<inter> cross_edges s'_ = {} \<and> back_edges s'_ \<inter> tree_edges s'_ = {} \<and> cross_edges s'_ \<inter> tree_edges s'_ = {}
[PROOF STEP]
(* Speed optimized proof, using only auto takes too long *)
[PROOF STATE]
proof (prove)
using this:
Field (back_edges s) \<subseteq> dom (discovered s) \<and> back_edges s \<subseteq> E - pending s \<and> Field (cross_edges s) \<subseteq> dom (discovered s) \<and> cross_edges s \<subseteq> E - pending s \<and> Field (tree_edges s) \<subseteq> dom (discovered s) \<and> tree_edges s \<subseteq> E - pending s \<and> back_edges s \<inter> cross_edges s = {} \<and> back_edges s \<inter> tree_edges s = {} \<and> cross_edges s \<inter> 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. Field (back_edges s'_) \<subseteq> dom (discovered s'_) \<and> back_edges s'_ \<subseteq> E - pending s'_ \<and> Field (cross_edges s'_) \<subseteq> dom (discovered s'_) \<and> cross_edges s'_ \<subseteq> E - pending s'_ \<and> Field (tree_edges s'_) \<subseteq> dom (discovered s'_) \<and> tree_edges s'_ \<subseteq> E - pending s'_ \<and> back_edges s'_ \<inter> cross_edges s'_ = {} \<and> back_edges s'_ \<inter> tree_edges s'_ = {} \<and> cross_edges s'_ \<inter> tree_edges s'_ = {}
[PROOF STEP]
apply (simp add: Field_def Range_def Domain_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Collect (Domainp (\<lambda>x xa. (x, xa) \<in> back_edges s)) \<subseteq> dom (discovered s) \<and> Collect (Rangep (\<lambda>x xa. (x, xa) \<in> back_edges s)) \<subseteq> dom (discovered s) \<and> back_edges s \<subseteq> E - pending s \<and> Collect (Domainp (\<lambda>x xa. (x, xa) \<in> cross_edges s)) \<subseteq> dom (discovered s) \<and> Collect (Rangep (\<lambda>x xa. (x, xa) \<in> cross_edges s)) \<subseteq> dom (discovered s) \<and> cross_edges s \<subseteq> E - pending s \<and> Collect (Domainp (\<lambda>x xa. (x, xa) \<in> tree_edges s)) \<subseteq> dom (discovered s) \<and> Collect (Rangep (\<lambda>x xa. (x, xa) \<in> tree_edges s)) \<subseteq> dom (discovered s) \<and> tree_edges s \<subseteq> E - pending s \<and> back_edges s \<inter> cross_edges s = {} \<and> back_edges s \<inter> tree_edges s = {} \<and> cross_edges s \<inter> 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>); stack s \<noteq> []; (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> Collect (Domainp (\<lambda>x xa. (x, xa) \<in> back_edges s)) \<subseteq> insert v_ (dom (discovered s)) \<and> Collect (Rangep (\<lambda>x xa. (x, xa) \<in> back_edges s)) \<subseteq> insert v_ (dom (discovered s)) \<and> back_edges s \<subseteq> E - (pending s - {(hd (stack s), v_)} \<union> {v_} \<times> E `` {v_}) \<and> Collect (Domainp (\<lambda>x xa. (x, xa) \<in> cross_edges s)) \<subseteq> insert v_ (dom (discovered s)) \<and> Collect (Rangep (\<lambda>x xa. (x, xa) \<in> cross_edges s)) \<subseteq> insert v_ (dom (discovered s)) \<and> cross_edges s \<subseteq> E - (pending s - {(hd (stack s), v_)} \<union> {v_} \<times> E `` {v_}) \<and> Collect (Domainp (\<lambda>x xa. x = hd (stack s) \<and> xa = v_ \<or> (x, xa) \<in> tree_edges s)) \<subseteq> insert v_ (dom (discovered s)) \<and> Collect (Rangep (\<lambda>x xa. x = hd (stack s) \<and> xa = v_ \<or> (x, xa) \<in> tree_edges s)) \<subseteq> insert v_ (dom (discovered s)) \<and> (hd (stack s), v_) \<in> E \<and> (hd (stack s) = v_ \<longrightarrow> (v_, v_) \<notin> E) \<and> tree_edges s \<subseteq> E - (pending s - {(hd (stack s), v_)} \<union> {v_} \<times> E `` {v_}) \<and> (hd (stack s), v_) \<notin> back_edges s \<and> (hd (stack s), v_) \<notin> cross_edges s
[PROOF STEP]
apply (drule pendingD)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Collect (Domainp (\<lambda>x xa. (x, xa) \<in> back_edges s)) \<subseteq> dom (discovered s) \<and> Collect (Rangep (\<lambda>x xa. (x, xa) \<in> back_edges s)) \<subseteq> dom (discovered s) \<and> back_edges s \<subseteq> E - pending s \<and> Collect (Domainp (\<lambda>x xa. (x, xa) \<in> cross_edges s)) \<subseteq> dom (discovered s) \<and> Collect (Rangep (\<lambda>x xa. (x, xa) \<in> cross_edges s)) \<subseteq> dom (discovered s) \<and> cross_edges s \<subseteq> E - pending s \<and> Collect (Domainp (\<lambda>x xa. (x, xa) \<in> tree_edges s)) \<subseteq> dom (discovered s) \<and> Collect (Rangep (\<lambda>x xa. (x, xa) \<in> tree_edges s)) \<subseteq> dom (discovered s) \<and> tree_edges s \<subseteq> E - pending s \<and> back_edges s \<inter> cross_edges s = {} \<and> back_edges s \<inter> tree_edges s = {} \<and> cross_edges s \<inter> 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>); stack s \<noteq> []; 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>; (hd (stack s), v_) \<in> E \<and> hd (stack s) \<in> dom (discovered s)\<rbrakk> \<Longrightarrow> Collect (Domainp (\<lambda>x xa. (x, xa) \<in> back_edges s)) \<subseteq> insert v_ (dom (discovered s)) \<and> Collect (Rangep (\<lambda>x xa. (x, xa) \<in> back_edges s)) \<subseteq> insert v_ (dom (discovered s)) \<and> back_edges s \<subseteq> E - (pending s - {(hd (stack s), v_)} \<union> {v_} \<times> E `` {v_}) \<and> Collect (Domainp (\<lambda>x xa. (x, xa) \<in> cross_edges s)) \<subseteq> insert v_ (dom (discovered s)) \<and> Collect (Rangep (\<lambda>x xa. (x, xa) \<in> cross_edges s)) \<subseteq> insert v_ (dom (discovered s)) \<and> cross_edges s \<subseteq> E - (pending s - {(hd (stack s), v_)} \<union> {v_} \<times> E `` {v_}) \<and> Collect (Domainp (\<lambda>x xa. x = hd (stack s) \<and> xa = v_ \<or> (x, xa) \<in> tree_edges s)) \<subseteq> insert v_ (dom (discovered s)) \<and> Collect (Rangep (\<lambda>x xa. x = hd (stack s) \<and> xa = v_ \<or> (x, xa) \<in> tree_edges s)) \<subseteq> insert v_ (dom (discovered s)) \<and> (hd (stack s), v_) \<in> E \<and> (hd (stack s) = v_ \<longrightarrow> (v_, v_) \<notin> E) \<and> tree_edges s \<subseteq> E - (pending s - {(hd (stack s), v_)} \<union> {v_} \<times> E `` {v_}) \<and> (hd (stack s), v_) \<notin> back_edges s \<and> (hd (stack s), v_) \<notin> cross_edges s
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Collect (Domainp (\<lambda>x xa. (x, xa) \<in> back_edges s)) \<subseteq> dom (discovered s) \<and> Collect (Rangep (\<lambda>x xa. (x, xa) \<in> back_edges s)) \<subseteq> dom (discovered s) \<and> back_edges s \<subseteq> E - pending s \<and> Collect (Domainp (\<lambda>x xa. (x, xa) \<in> cross_edges s)) \<subseteq> dom (discovered s) \<and> Collect (Rangep (\<lambda>x xa. (x, xa) \<in> cross_edges s)) \<subseteq> dom (discovered s) \<and> cross_edges s \<subseteq> E - pending s \<and> Collect (Domainp (\<lambda>x xa. (x, xa) \<in> tree_edges s)) \<subseteq> dom (discovered s) \<and> Collect (Rangep (\<lambda>x xa. (x, xa) \<in> tree_edges s)) \<subseteq> dom (discovered s) \<and> tree_edges s \<subseteq> E - pending s \<and> back_edges s \<inter> cross_edges s = {} \<and> back_edges s \<inter> tree_edges s = {} \<and> cross_edges s \<inter> 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>); stack s \<noteq> []; 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>; (hd (stack s), v_) \<in> E \<and> hd (stack s) \<in> dom (discovered s)\<rbrakk> \<Longrightarrow> Collect (Domainp (\<lambda>x xa. (x, xa) \<in> back_edges s)) \<subseteq> insert v_ (dom (discovered s)) \<and> Collect (Rangep (\<lambda>x xa. (x, xa) \<in> back_edges s)) \<subseteq> insert v_ (dom (discovered s)) \<and> back_edges s \<subseteq> E - (pending s - {(hd (stack s), v_)} \<union> {v_} \<times> E `` {v_}) \<and> Collect (Domainp (\<lambda>x xa. (x, xa) \<in> cross_edges s)) \<subseteq> insert v_ (dom (discovered s)) \<and> Collect (Rangep (\<lambda>x xa. (x, xa) \<in> cross_edges s)) \<subseteq> insert v_ (dom (discovered s)) \<and> cross_edges s \<subseteq> E - (pending s - {(hd (stack s), v_)} \<union> {v_} \<times> E `` {v_}) \<and> Collect (Domainp (\<lambda>x xa. x = hd (stack s) \<and> xa = v_ \<or> (x, xa) \<in> tree_edges s)) \<subseteq> insert v_ (dom (discovered s)) \<and> Collect (Rangep (\<lambda>x xa. x = hd (stack s) \<and> xa = v_ \<or> (x, xa) \<in> tree_edges s)) \<subseteq> insert v_ (dom (discovered s)) \<and> (hd (stack s) = v_ \<longrightarrow> (v_, v_) \<notin> E) \<and> tree_edges s \<subseteq> E - (pending s - {(hd (stack s), v_)} \<union> {v_} \<times> E `` {v_}) \<and> (hd (stack s), v_) \<notin> back_edges s \<and> (hd (stack s), v_) \<notin> cross_edges s
[PROOF STEP]
by (blast)
[PROOF STATE]
proof (state)
this:
Field (back_edges s'_) \<subseteq> dom (discovered s'_) \<and> back_edges s'_ \<subseteq> E - pending s'_ \<and> Field (cross_edges s'_) \<subseteq> dom (discovered s'_) \<and> cross_edges s'_ \<subseteq> E - pending s'_ \<and> Field (tree_edges s'_) \<subseteq> dom (discovered s'_) \<and> tree_edges s'_ \<subseteq> E - pending s'_ \<and> back_edges s'_ \<inter> cross_edges s'_ = {} \<and> back_edges s'_ \<inter> tree_edges s'_ = {} \<and> cross_edges s'_ \<inter> tree_edges s'_ = {}

goal (3 subgoals):
 1. \<And>e. Field (back_edges (empty_state e)) \<subseteq> dom (discovered (empty_state e)) \<and> back_edges (empty_state e) \<subseteq> E - pending (empty_state e) \<and> Field (cross_edges (empty_state e)) \<subseteq> dom (discovered (empty_state e)) \<and> cross_edges (empty_state e) \<subseteq> E - pending (empty_state e) \<and> Field (tree_edges (empty_state e)) \<subseteq> dom (discovered (empty_state e)) \<and> tree_edges (empty_state e) \<subseteq> E - pending (empty_state e) \<and> back_edges (empty_state e) \<inter> cross_edges (empty_state e) = {} \<and> back_edges (empty_state e) \<inter> tree_edges (empty_state e) = {} \<and> cross_edges (empty_state e) \<inter> tree_edges (empty_state e) = {}
 2. \<And>s s' v0 e. \<lbrakk>Field (back_edges s) \<subseteq> dom (discovered s) \<and> back_edges s \<subseteq> E - pending s \<and> Field (cross_edges s) \<subseteq> dom (discovered s) \<and> cross_edges s \<subseteq> E - pending s \<and> Field (tree_edges s) \<subseteq> dom (discovered s) \<and> tree_edges s \<subseteq> E - pending s \<and> back_edges s \<inter> cross_edges s = {} \<and> back_edges s \<inter> tree_edges s = {} \<and> cross_edges s \<inter> 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> Field (back_edges s') \<subseteq> dom (discovered s') \<and> back_edges s' \<subseteq> E - pending s' \<and> Field (cross_edges s') \<subseteq> dom (discovered s') \<and> cross_edges s' \<subseteq> E - pending s' \<and> Field (tree_edges s') \<subseteq> dom (discovered s') \<and> tree_edges s' \<subseteq> E - pending s' \<and> back_edges s' \<inter> cross_edges s' = {} \<and> back_edges s' \<inter> tree_edges s' = {} \<and> cross_edges s' \<inter> tree_edges s' = {}
 3. \<And>s s' u e. \<lbrakk>Field (back_edges s) \<subseteq> dom (discovered s) \<and> back_edges s \<subseteq> E - pending s \<and> Field (cross_edges s) \<subseteq> dom (discovered s) \<and> cross_edges s \<subseteq> E - pending s \<and> Field (tree_edges s) \<subseteq> dom (discovered s) \<and> tree_edges s \<subseteq> E - pending s \<and> back_edges s \<inter> cross_edges s = {} \<and> back_edges s \<inter> tree_edges s = {} \<and> cross_edges s \<inter> 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> Field (back_edges s') \<subseteq> dom (discovered s') \<and> back_edges s' \<subseteq> E - pending s' \<and> Field (cross_edges s') \<subseteq> dom (discovered s') \<and> cross_edges s' \<subseteq> E - pending s' \<and> Field (tree_edges s') \<subseteq> dom (discovered s') \<and> tree_edges s' \<subseteq> E - pending s' \<and> back_edges s' \<inter> cross_edges s' = {} \<and> back_edges s' \<inter> tree_edges s' = {} \<and> cross_edges s' \<inter> tree_edges s' = {}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>e. Field (back_edges (empty_state e)) \<subseteq> dom (discovered (empty_state e)) \<and> back_edges (empty_state e) \<subseteq> E - pending (empty_state e) \<and> Field (cross_edges (empty_state e)) \<subseteq> dom (discovered (empty_state e)) \<and> cross_edges (empty_state e) \<subseteq> E - pending (empty_state e) \<and> Field (tree_edges (empty_state e)) \<subseteq> dom (discovered (empty_state e)) \<and> tree_edges (empty_state e) \<subseteq> E - pending (empty_state e) \<and> back_edges (empty_state e) \<inter> cross_edges (empty_state e) = {} \<and> back_edges (empty_state e) \<inter> tree_edges (empty_state e) = {} \<and> cross_edges (empty_state e) \<inter> tree_edges (empty_state e) = {}
 2. \<And>s s' v0 e. \<lbrakk>Field (back_edges s) \<subseteq> dom (discovered s) \<and> back_edges s \<subseteq> E - pending s \<and> Field (cross_edges s) \<subseteq> dom (discovered s) \<and> cross_edges s \<subseteq> E - pending s \<and> Field (tree_edges s) \<subseteq> dom (discovered s) \<and> tree_edges s \<subseteq> E - pending s \<and> back_edges s \<inter> cross_edges s = {} \<and> back_edges s \<inter> tree_edges s = {} \<and> cross_edges s \<inter> 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> Field (back_edges s') \<subseteq> dom (discovered s') \<and> back_edges s' \<subseteq> E - pending s' \<and> Field (cross_edges s') \<subseteq> dom (discovered s') \<and> cross_edges s' \<subseteq> E - pending s' \<and> Field (tree_edges s') \<subseteq> dom (discovered s') \<and> tree_edges s' \<subseteq> E - pending s' \<and> back_edges s' \<inter> cross_edges s' = {} \<and> back_edges s' \<inter> tree_edges s' = {} \<and> cross_edges s' \<inter> tree_edges s' = {}
 3. \<And>s s' u e. \<lbrakk>Field (back_edges s) \<subseteq> dom (discovered s) \<and> back_edges s \<subseteq> E - pending s \<and> Field (cross_edges s) \<subseteq> dom (discovered s) \<and> cross_edges s \<subseteq> E - pending s \<and> Field (tree_edges s) \<subseteq> dom (discovered s) \<and> tree_edges s \<subseteq> E - pending s \<and> back_edges s \<inter> cross_edges s = {} \<and> back_edges s \<inter> tree_edges s = {} \<and> cross_edges s \<inter> 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> Field (back_edges s') \<subseteq> dom (discovered s') \<and> back_edges s' \<subseteq> E - pending s' \<and> Field (cross_edges s') \<subseteq> dom (discovered s') \<and> cross_edges s' \<subseteq> E - pending s' \<and> Field (tree_edges s') \<subseteq> dom (discovered s') \<and> tree_edges s' \<subseteq> E - pending s' \<and> back_edges s' \<inter> cross_edges s' = {} \<and> back_edges s' \<inter> tree_edges s' = {} \<and> cross_edges s' \<inter> tree_edges s' = {}
[PROOF STEP]
case (new_root s)
[PROOF STATE]
proof (state)
this:
Field (back_edges s) \<subseteq> dom (discovered s) \<and> back_edges s \<subseteq> E - pending s \<and> Field (cross_edges s) \<subseteq> dom (discovered s) \<and> cross_edges s \<subseteq> E - pending s \<and> Field (tree_edges s) \<subseteq> dom (discovered s) \<and> tree_edges s \<subseteq> E - pending s \<and> back_edges s \<inter> cross_edges s = {} \<and> back_edges s \<inter> tree_edges s = {} \<and> cross_edges s \<inter> 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>

goal (3 subgoals):
 1. \<And>e. Field (back_edges (empty_state e)) \<subseteq> dom (discovered (empty_state e)) \<and> back_edges (empty_state e) \<subseteq> E - pending (empty_state e) \<and> Field (cross_edges (empty_state e)) \<subseteq> dom (discovered (empty_state e)) \<and> cross_edges (empty_state e) \<subseteq> E - pending (empty_state e) \<and> Field (tree_edges (empty_state e)) \<subseteq> dom (discovered (empty_state e)) \<and> tree_edges (empty_state e) \<subseteq> E - pending (empty_state e) \<and> back_edges (empty_state e) \<inter> cross_edges (empty_state e) = {} \<and> back_edges (empty_state e) \<inter> tree_edges (empty_state e) = {} \<and> cross_edges (empty_state e) \<inter> tree_edges (empty_state e) = {}
 2. \<And>s s' v0 e. \<lbrakk>Field (back_edges s) \<subseteq> dom (discovered s) \<and> back_edges s \<subseteq> E - pending s \<and> Field (cross_edges s) \<subseteq> dom (discovered s) \<and> cross_edges s \<subseteq> E - pending s \<and> Field (tree_edges s) \<subseteq> dom (discovered s) \<and> tree_edges s \<subseteq> E - pending s \<and> back_edges s \<inter> cross_edges s = {} \<and> back_edges s \<inter> tree_edges s = {} \<and> cross_edges s \<inter> 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> Field (back_edges s') \<subseteq> dom (discovered s') \<and> back_edges s' \<subseteq> E - pending s' \<and> Field (cross_edges s') \<subseteq> dom (discovered s') \<and> cross_edges s' \<subseteq> E - pending s' \<and> Field (tree_edges s') \<subseteq> dom (discovered s') \<and> tree_edges s' \<subseteq> E - pending s' \<and> back_edges s' \<inter> cross_edges s' = {} \<and> back_edges s' \<inter> tree_edges s' = {} \<and> cross_edges s' \<inter> tree_edges s' = {}
 3. \<And>s s' u e. \<lbrakk>Field (back_edges s) \<subseteq> dom (discovered s) \<and> back_edges s \<subseteq> E - pending s \<and> Field (cross_edges s) \<subseteq> dom (discovered s) \<and> cross_edges s \<subseteq> E - pending s \<and> Field (tree_edges s) \<subseteq> dom (discovered s) \<and> tree_edges s \<subseteq> E - pending s \<and> back_edges s \<inter> cross_edges s = {} \<and> back_edges s \<inter> tree_edges s = {} \<and> cross_edges s \<inter> 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> Field (back_edges s') \<subseteq> dom (discovered s') \<and> back_edges s' \<subseteq> E - pending s' \<and> Field (cross_edges s') \<subseteq> dom (discovered s') \<and> cross_edges s' \<subseteq> E - pending s' \<and> Field (tree_edges s') \<subseteq> dom (discovered s') \<and> tree_edges s' \<subseteq> E - pending s' \<and> back_edges s' \<inter> cross_edges s' = {} \<and> back_edges s' \<inter> tree_edges s' = {} \<and> cross_edges s' \<inter> tree_edges s' = {}
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
Field (back_edges s) \<subseteq> dom (discovered s) \<and> back_edges s \<subseteq> E - pending s \<and> Field (cross_edges s) \<subseteq> dom (discovered s) \<and> cross_edges s \<subseteq> E - pending s \<and> Field (tree_edges s) \<subseteq> dom (discovered s) \<and> tree_edges s \<subseteq> E - pending s \<and> back_edges s \<inter> cross_edges s = {} \<and> back_edges s \<inter> tree_edges s = {} \<and> cross_edges s \<inter> 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>

goal (1 subgoal):
 1. Field (back_edges s'_) \<subseteq> dom (discovered s'_) \<and> back_edges s'_ \<subseteq> E - pending s'_ \<and> Field (cross_edges s'_) \<subseteq> dom (discovered s'_) \<and> cross_edges s'_ \<subseteq> E - pending s'_ \<and> Field (tree_edges s'_) \<subseteq> dom (discovered s'_) \<and> tree_edges s'_ \<subseteq> E - pending s'_ \<and> back_edges s'_ \<inter> cross_edges s'_ = {} \<and> back_edges s'_ \<inter> tree_edges s'_ = {} \<and> cross_edges s'_ \<inter> tree_edges s'_ = {}
[PROOF STEP]
by (simp add: Field_def) blast
[PROOF STATE]
proof (state)
this:
Field (back_edges s'_) \<subseteq> dom (discovered s'_) \<and> back_edges s'_ \<subseteq> E - pending s'_ \<and> Field (cross_edges s'_) \<subseteq> dom (discovered s'_) \<and> cross_edges s'_ \<subseteq> E - pending s'_ \<and> Field (tree_edges s'_) \<subseteq> dom (discovered s'_) \<and> tree_edges s'_ \<subseteq> E - pending s'_ \<and> back_edges s'_ \<inter> cross_edges s'_ = {} \<and> back_edges s'_ \<inter> tree_edges s'_ = {} \<and> cross_edges s'_ \<inter> tree_edges s'_ = {}

goal (2 subgoals):
 1. \<And>e. Field (back_edges (empty_state e)) \<subseteq> dom (discovered (empty_state e)) \<and> back_edges (empty_state e) \<subseteq> E - pending (empty_state e) \<and> Field (cross_edges (empty_state e)) \<subseteq> dom (discovered (empty_state e)) \<and> cross_edges (empty_state e) \<subseteq> E - pending (empty_state e) \<and> Field (tree_edges (empty_state e)) \<subseteq> dom (discovered (empty_state e)) \<and> tree_edges (empty_state e) \<subseteq> E - pending (empty_state e) \<and> back_edges (empty_state e) \<inter> cross_edges (empty_state e) = {} \<and> back_edges (empty_state e) \<inter> tree_edges (empty_state e) = {} \<and> cross_edges (empty_state e) \<inter> tree_edges (empty_state e) = {}
 2. \<And>s s' u e. \<lbrakk>Field (back_edges s) \<subseteq> dom (discovered s) \<and> back_edges s \<subseteq> E - pending s \<and> Field (cross_edges s) \<subseteq> dom (discovered s) \<and> cross_edges s \<subseteq> E - pending s \<and> Field (tree_edges s) \<subseteq> dom (discovered s) \<and> tree_edges s \<subseteq> E - pending s \<and> back_edges s \<inter> cross_edges s = {} \<and> back_edges s \<inter> tree_edges s = {} \<and> cross_edges s \<inter> 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> Field (back_edges s') \<subseteq> dom (discovered s') \<and> back_edges s' \<subseteq> E - pending s' \<and> Field (cross_edges s') \<subseteq> dom (discovered s') \<and> cross_edges s' \<subseteq> E - pending s' \<and> Field (tree_edges s') \<subseteq> dom (discovered s') \<and> tree_edges s' \<subseteq> E - pending s' \<and> back_edges s' \<inter> cross_edges s' = {} \<and> back_edges s' \<inter> tree_edges s' = {} \<and> cross_edges s' \<inter> tree_edges s' = {}
[PROOF STEP]
qed auto