[STATEMENT]
lemma i_edges_covered:
    "is_invar (\<lambda>s. (E \<inter> dom (discovered s) \<times> UNIV) - pending s = edges s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_invar (\<lambda>s. E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_edges s)
[PROOF STEP]
proof (induction rule: is_invarI_full)
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>e. E \<inter> dom (discovered (empty_state e)) \<times> UNIV - pending (empty_state e) = tree_edges (empty_state e) \<union> cross_edges (empty_state e) \<union> back_edges (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
 3. \<And>s s' u e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
 4. \<And>s s' u v e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
 5. \<And>s s' u v e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
 6. \<And>s s' u v e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
[PROOF STEP]
case (new_root s s' v0)
[PROOF STATE]
proof (state)
this:
E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_edges s
cond s
DFS_invar G param s
DFS_invar G param s'
v0 \<in> V0
s' = new_root v0 s\<lparr>state.more := e_\<rparr>
stack s = []
v0 \<notin> dom (discovered s)

goal (6 subgoals):
 1. \<And>e. E \<inter> dom (discovered (empty_state e)) \<times> UNIV - pending (empty_state e) = tree_edges (empty_state e) \<union> cross_edges (empty_state e) \<union> back_edges (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
 3. \<And>s s' u e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
 4. \<And>s s' u v e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
 5. \<And>s s' u v e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
 6. \<And>s s' u v e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
[PROOF STEP]
interpret DFS_invar G param s
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. DFS_invar G param s
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>e. E \<inter> dom (discovered (empty_state e)) \<times> UNIV - pending (empty_state e) = tree_edges (empty_state e) \<union> cross_edges (empty_state e) \<union> back_edges (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
 3. \<And>s s' u e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
 4. \<And>s s' u v e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
 5. \<And>s s' u v e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
 6. \<And>s s' u v e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
[PROOF STEP]
from new_root empty_stack_imp_empty_pending
[PROOF STATE]
proof (chain)
picking this:
E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_edges s
cond s
DFS_invar G param s
DFS_invar G param s'
v0 \<in> V0
s' = new_root v0 s\<lparr>state.more := e_\<rparr>
stack s = []
v0 \<notin> dom (discovered s)
stack s = [] \<Longrightarrow> pending s = {}
[PROOF STEP]
have [simp]: "pending s = {}"
[PROOF STATE]
proof (prove)
using this:
E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_edges s
cond s
DFS_invar G param s
DFS_invar G param s'
v0 \<in> V0
s' = new_root v0 s\<lparr>state.more := e_\<rparr>
stack s = []
v0 \<notin> dom (discovered s)
stack s = [] \<Longrightarrow> pending s = {}

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

goal (6 subgoals):
 1. \<And>e. E \<inter> dom (discovered (empty_state e)) \<times> UNIV - pending (empty_state e) = tree_edges (empty_state e) \<union> cross_edges (empty_state e) \<union> back_edges (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
 3. \<And>s s' u e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
 4. \<And>s s' u v e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
 5. \<And>s s' u v e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
 6. \<And>s s' u v e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
[PROOF STEP]
from \<open>v0 \<notin> dom (discovered s)\<close>
[PROOF STATE]
proof (chain)
picking this:
v0 \<notin> dom (discovered s)
[PROOF STEP]
have [simp]: "E \<inter> insert v0 (dom (discovered s)) \<times> UNIV - {v0} \<times> succ v0
      = E \<inter> dom (discovered s) \<times> UNIV"
[PROOF STATE]
proof (prove)
using this:
v0 \<notin> dom (discovered s)

goal (1 subgoal):
 1. E \<inter> insert v0 (dom (discovered s)) \<times> UNIV - {v0} \<times> E `` {v0} = E \<inter> dom (discovered s) \<times> UNIV
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
E \<inter> insert v0 (dom (discovered s)) \<times> UNIV - {v0} \<times> E `` {v0} = E \<inter> dom (discovered s) \<times> UNIV

goal (6 subgoals):
 1. \<And>e. E \<inter> dom (discovered (empty_state e)) \<times> UNIV - pending (empty_state e) = tree_edges (empty_state e) \<union> cross_edges (empty_state e) \<union> back_edges (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
 3. \<And>s s' u e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
 4. \<And>s s' u v e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
 5. \<And>s s' u v e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
 6. \<And>s s' u v e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
[PROOF STEP]
from new_root
[PROOF STATE]
proof (chain)
picking this:
E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_edges s
cond s
DFS_invar G param s
DFS_invar G param s'
v0 \<in> V0
s' = new_root v0 s\<lparr>state.more := e_\<rparr>
stack s = []
v0 \<notin> dom (discovered s)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_edges s
cond s
DFS_invar G param s
DFS_invar G param s'
v0 \<in> V0
s' = new_root v0 s\<lparr>state.more := e_\<rparr>
stack s = []
v0 \<notin> dom (discovered s)

goal (1 subgoal):
 1. E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'

goal (5 subgoals):
 1. \<And>e. E \<inter> dom (discovered (empty_state e)) \<times> UNIV - pending (empty_state e) = tree_edges (empty_state e) \<union> cross_edges (empty_state e) \<union> back_edges (empty_state e)
 2. \<And>s s' u e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
 3. \<And>s s' u v e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
 4. \<And>s s' u v e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
 5. \<And>s s' u v e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>e. E \<inter> dom (discovered (empty_state e)) \<times> UNIV - pending (empty_state e) = tree_edges (empty_state e) \<union> cross_edges (empty_state e) \<union> back_edges (empty_state e)
 2. \<And>s s' u e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
 3. \<And>s s' u v e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
 4. \<And>s s' u v e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
 5. \<And>s s' u v e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
[PROOF STEP]
case (cross_edge s s' u v)
[PROOF STATE]
proof (state)
this:
E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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. E \<inter> dom (discovered (empty_state e)) \<times> UNIV - pending (empty_state e) = tree_edges (empty_state e) \<union> cross_edges (empty_state e) \<union> back_edges (empty_state e)
 2. \<And>s s' u e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
 3. \<And>s s' u v e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
 4. \<And>s s' u v e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
 5. \<And>s s' u v e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
[PROOF STEP]
interpret DFS_invar G param s
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. DFS_invar G param s
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>e. E \<inter> dom (discovered (empty_state e)) \<times> UNIV - pending (empty_state e) = tree_edges (empty_state e) \<union> cross_edges (empty_state e) \<union> back_edges (empty_state e)
 2. \<And>s s' u e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
 3. \<And>s s' u v e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
 4. \<And>s s' u v e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
 5. \<And>s s' u v e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
[PROOF STEP]
from cross_edge stack_discovered
[PROOF STATE]
proof (chain)
picking this:
E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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>
set (stack s) \<subseteq> dom (discovered s)
[PROOF STEP]
have "u \<in> dom (discovered s)"
[PROOF STATE]
proof (prove)
using this:
E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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>
set (stack s) \<subseteq> dom (discovered s)

goal (1 subgoal):
 1. u \<in> dom (discovered s)
[PROOF STEP]
by (cases "stack s") auto
[PROOF STATE]
proof (state)
this:
u \<in> dom (discovered s)

goal (5 subgoals):
 1. \<And>e. E \<inter> dom (discovered (empty_state e)) \<times> UNIV - pending (empty_state e) = tree_edges (empty_state e) \<union> cross_edges (empty_state e) \<union> back_edges (empty_state e)
 2. \<And>s s' u e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
 3. \<And>s s' u v e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
 4. \<And>s s' u v e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
 5. \<And>s s' u v e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
[PROOF STEP]
with cross_edge(2-) pending_ssE
[PROOF STATE]
proof (chain)
picking this:
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>
pending s \<subseteq> E
u \<in> dom (discovered s)
[PROOF STEP]
have
      "E \<inter> dom (discovered s) \<times> UNIV - (pending s - {(hd (stack s), v)})
      = insert (hd (stack s), v) (E \<inter> dom (discovered s) \<times> UNIV - pending s)"
[PROOF STATE]
proof (prove)
using this:
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>
pending s \<subseteq> E
u \<in> dom (discovered s)

goal (1 subgoal):
 1. E \<inter> dom (discovered s) \<times> UNIV - (pending s - {(hd (stack s), v)}) = insert (hd (stack s), v) (E \<inter> dom (discovered s) \<times> UNIV - pending s)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
E \<inter> dom (discovered s) \<times> UNIV - (pending s - {(hd (stack s), v)}) = insert (hd (stack s), v) (E \<inter> dom (discovered s) \<times> UNIV - pending s)

goal (5 subgoals):
 1. \<And>e. E \<inter> dom (discovered (empty_state e)) \<times> UNIV - pending (empty_state e) = tree_edges (empty_state e) \<union> cross_edges (empty_state e) \<union> back_edges (empty_state e)
 2. \<And>s s' u e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
 3. \<And>s s' u v e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
 4. \<And>s s' u v e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
 5. \<And>s s' u v e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
E \<inter> dom (discovered s) \<times> UNIV - (pending s - {(hd (stack s), v)}) = insert (hd (stack s), v) (E \<inter> dom (discovered s) \<times> UNIV - pending s)

goal (1 subgoal):
 1. E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
[PROOF STEP]
using cross_edge
[PROOF STATE]
proof (prove)
using this:
E \<inter> dom (discovered s) \<times> UNIV - (pending s - {(hd (stack s), v)}) = insert (hd (stack s), v) (E \<inter> dom (discovered s) \<times> UNIV - pending s)
E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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. E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'

goal (4 subgoals):
 1. \<And>e. E \<inter> dom (discovered (empty_state e)) \<times> UNIV - pending (empty_state e) = tree_edges (empty_state e) \<union> cross_edges (empty_state e) \<union> back_edges (empty_state e)
 2. \<And>s s' u e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
 3. \<And>s s' u v e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
 4. \<And>s s' u v e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>e. E \<inter> dom (discovered (empty_state e)) \<times> UNIV - pending (empty_state e) = tree_edges (empty_state e) \<union> cross_edges (empty_state e) \<union> back_edges (empty_state e)
 2. \<And>s s' u e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
 3. \<And>s s' u v e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
 4. \<And>s s' u v e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
[PROOF STEP]
case (back_edge s s' u v)
[PROOF STATE]
proof (state)
this:
E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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 (4 subgoals):
 1. \<And>e. E \<inter> dom (discovered (empty_state e)) \<times> UNIV - pending (empty_state e) = tree_edges (empty_state e) \<union> cross_edges (empty_state e) \<union> back_edges (empty_state e)
 2. \<And>s s' u e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
 3. \<And>s s' u v e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
 4. \<And>s s' u v e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
[PROOF STEP]
interpret DFS_invar G param s
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. DFS_invar G param s
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>e. E \<inter> dom (discovered (empty_state e)) \<times> UNIV - pending (empty_state e) = tree_edges (empty_state e) \<union> cross_edges (empty_state e) \<union> back_edges (empty_state e)
 2. \<And>s s' u e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
 3. \<And>s s' u v e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
 4. \<And>s s' u v e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
[PROOF STEP]
from back_edge stack_discovered
[PROOF STATE]
proof (chain)
picking this:
E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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>
set (stack s) \<subseteq> dom (discovered s)
[PROOF STEP]
have "u \<in> dom (discovered s)"
[PROOF STATE]
proof (prove)
using this:
E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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>
set (stack s) \<subseteq> dom (discovered s)

goal (1 subgoal):
 1. u \<in> dom (discovered s)
[PROOF STEP]
by (cases "stack s") auto
[PROOF STATE]
proof (state)
this:
u \<in> dom (discovered s)

goal (4 subgoals):
 1. \<And>e. E \<inter> dom (discovered (empty_state e)) \<times> UNIV - pending (empty_state e) = tree_edges (empty_state e) \<union> cross_edges (empty_state e) \<union> back_edges (empty_state e)
 2. \<And>s s' u e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
 3. \<And>s s' u v e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
 4. \<And>s s' u v e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
[PROOF STEP]
with back_edge(2-) pending_ssE
[PROOF STATE]
proof (chain)
picking this:
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>
pending s \<subseteq> E
u \<in> dom (discovered s)
[PROOF STEP]
have
      "E \<inter> dom (discovered s) \<times> UNIV - (pending s - {(hd (stack s), v)})
      = insert (hd (stack s), v) (E \<inter> dom (discovered s) \<times> UNIV - pending s)"
[PROOF STATE]
proof (prove)
using this:
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>
pending s \<subseteq> E
u \<in> dom (discovered s)

goal (1 subgoal):
 1. E \<inter> dom (discovered s) \<times> UNIV - (pending s - {(hd (stack s), v)}) = insert (hd (stack s), v) (E \<inter> dom (discovered s) \<times> UNIV - pending s)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
E \<inter> dom (discovered s) \<times> UNIV - (pending s - {(hd (stack s), v)}) = insert (hd (stack s), v) (E \<inter> dom (discovered s) \<times> UNIV - pending s)

goal (4 subgoals):
 1. \<And>e. E \<inter> dom (discovered (empty_state e)) \<times> UNIV - pending (empty_state e) = tree_edges (empty_state e) \<union> cross_edges (empty_state e) \<union> back_edges (empty_state e)
 2. \<And>s s' u e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
 3. \<And>s s' u v e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
 4. \<And>s s' u v e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
E \<inter> dom (discovered s) \<times> UNIV - (pending s - {(hd (stack s), v)}) = insert (hd (stack s), v) (E \<inter> dom (discovered s) \<times> UNIV - pending s)

goal (1 subgoal):
 1. E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
[PROOF STEP]
using back_edge
[PROOF STATE]
proof (prove)
using this:
E \<inter> dom (discovered s) \<times> UNIV - (pending s - {(hd (stack s), v)}) = insert (hd (stack s), v) (E \<inter> dom (discovered s) \<times> UNIV - pending s)
E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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. E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'

goal (3 subgoals):
 1. \<And>e. E \<inter> dom (discovered (empty_state e)) \<times> UNIV - pending (empty_state e) = tree_edges (empty_state e) \<union> cross_edges (empty_state e) \<union> back_edges (empty_state e)
 2. \<And>s s' u e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
 3. \<And>s s' u v e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>e. E \<inter> dom (discovered (empty_state e)) \<times> UNIV - pending (empty_state e) = tree_edges (empty_state e) \<union> cross_edges (empty_state e) \<union> back_edges (empty_state e)
 2. \<And>s s' u e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
 3. \<And>s s' u v e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
[PROOF STEP]
case (discover s s' u v)
[PROOF STATE]
proof (state)
this:
E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_edges s
cond s
DFS_invar G param s
DFS_invar G param s'
s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e_\<rparr>
stack s \<noteq> []
v \<in> pending s `` {u}
v \<notin> dom (discovered s)
u = hd (stack s)

goal (3 subgoals):
 1. \<And>e. E \<inter> dom (discovered (empty_state e)) \<times> UNIV - pending (empty_state e) = tree_edges (empty_state e) \<union> cross_edges (empty_state e) \<union> back_edges (empty_state e)
 2. \<And>s s' u e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
 3. \<And>s s' u v e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
[PROOF STEP]
interpret DFS_invar G param s
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. DFS_invar G param s
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>e. E \<inter> dom (discovered (empty_state e)) \<times> UNIV - pending (empty_state e) = tree_edges (empty_state e) \<union> cross_edges (empty_state e) \<union> back_edges (empty_state e)
 2. \<And>s s' u e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
 3. \<And>s s' u v e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
[PROOF STEP]
from discover stack_discovered
[PROOF STATE]
proof (chain)
picking this:
E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_edges s
cond s
DFS_invar G param s
DFS_invar G param s'
s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e_\<rparr>
stack s \<noteq> []
v \<in> pending s `` {u}
v \<notin> dom (discovered s)
u = hd (stack s)
set (stack s) \<subseteq> dom (discovered s)
[PROOF STEP]
have "u \<in> dom (discovered s)"
[PROOF STATE]
proof (prove)
using this:
E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_edges s
cond s
DFS_invar G param s
DFS_invar G param s'
s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e_\<rparr>
stack s \<noteq> []
v \<in> pending s `` {u}
v \<notin> dom (discovered s)
u = hd (stack s)
set (stack s) \<subseteq> dom (discovered s)

goal (1 subgoal):
 1. u \<in> dom (discovered s)
[PROOF STEP]
by (cases "stack s") auto
[PROOF STATE]
proof (state)
this:
u \<in> dom (discovered s)

goal (3 subgoals):
 1. \<And>e. E \<inter> dom (discovered (empty_state e)) \<times> UNIV - pending (empty_state e) = tree_edges (empty_state e) \<union> cross_edges (empty_state e) \<union> back_edges (empty_state e)
 2. \<And>s s' u e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
 3. \<And>s s' u v e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
[PROOF STEP]
with discover(2-) pending_ssE
[PROOF STATE]
proof (chain)
picking this:
cond s
DFS_invar G param s
DFS_invar G param s'
s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e_\<rparr>
stack s \<noteq> []
v \<in> pending s `` {u}
v \<notin> dom (discovered s)
u = hd (stack s)
pending s \<subseteq> E
u \<in> dom (discovered s)
[PROOF STEP]
have
      "E \<inter> insert v (dom (discovered s)) \<times> UNIV
        - (pending s - {(hd (stack s), v)} \<union> {v} \<times> succ v)
      = insert (hd (stack s), v) (E \<inter> dom (discovered s) \<times> UNIV - pending s)"
[PROOF STATE]
proof (prove)
using this:
cond s
DFS_invar G param s
DFS_invar G param s'
s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e_\<rparr>
stack s \<noteq> []
v \<in> pending s `` {u}
v \<notin> dom (discovered s)
u = hd (stack s)
pending s \<subseteq> E
u \<in> dom (discovered s)

goal (1 subgoal):
 1. E \<inter> insert v (dom (discovered s)) \<times> UNIV - (pending s - {(hd (stack s), v)} \<union> {v} \<times> E `` {v}) = insert (hd (stack s), v) (E \<inter> dom (discovered s) \<times> UNIV - pending s)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
E \<inter> insert v (dom (discovered s)) \<times> UNIV - (pending s - {(hd (stack s), v)} \<union> {v} \<times> E `` {v}) = insert (hd (stack s), v) (E \<inter> dom (discovered s) \<times> UNIV - pending s)

goal (3 subgoals):
 1. \<And>e. E \<inter> dom (discovered (empty_state e)) \<times> UNIV - pending (empty_state e) = tree_edges (empty_state e) \<union> cross_edges (empty_state e) \<union> back_edges (empty_state e)
 2. \<And>s s' u e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
 3. \<And>s s' u v e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
E \<inter> insert v (dom (discovered s)) \<times> UNIV - (pending s - {(hd (stack s), v)} \<union> {v} \<times> E `` {v}) = insert (hd (stack s), v) (E \<inter> dom (discovered s) \<times> UNIV - pending s)

goal (1 subgoal):
 1. E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
[PROOF STEP]
using discover
[PROOF STATE]
proof (prove)
using this:
E \<inter> insert v (dom (discovered s)) \<times> UNIV - (pending s - {(hd (stack s), v)} \<union> {v} \<times> E `` {v}) = insert (hd (stack s), v) (E \<inter> dom (discovered s) \<times> UNIV - pending s)
E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_edges s
cond s
DFS_invar G param s
DFS_invar G param s'
s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e_\<rparr>
stack s \<noteq> []
v \<in> pending s `` {u}
v \<notin> dom (discovered s)
u = hd (stack s)

goal (1 subgoal):
 1. E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'

goal (2 subgoals):
 1. \<And>e. E \<inter> dom (discovered (empty_state e)) \<times> UNIV - pending (empty_state e) = tree_edges (empty_state e) \<union> cross_edges (empty_state e) \<union> back_edges (empty_state e)
 2. \<And>s s' u e. \<lbrakk>E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_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> E \<inter> dom (discovered s') \<times> UNIV - pending s' = tree_edges s' \<union> cross_edges s' \<union> back_edges s'
[PROOF STEP]
qed simp_all


[STATEMENT]
lemma edges_ss_reachable_edges:
    "edges s \<subseteq> E \<inter> reachable \<times> UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tree_edges s \<union> cross_edges s \<union> back_edges s \<subseteq> E \<inter> reachable \<times> UNIV
[PROOF STEP]
using edges_covered discovered_reachable
[PROOF STATE]
proof (prove)
using this:
E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_edges s
dom (discovered s) \<subseteq> reachable

goal (1 subgoal):
 1. tree_edges s \<union> cross_edges s \<union> back_edges s \<subseteq> E \<inter> reachable \<times> UNIV
[PROOF STEP]
by (fast intro: rtrancl_image_advance_rtrancl)


[STATEMENT]
lemma nc_edges_covered:
    assumes "\<not>cond s" "\<not>is_break param s"
    shows "E \<inter> reachable \<times> UNIV = edges s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. E \<inter> reachable \<times> UNIV = tree_edges s \<union> cross_edges s \<union> back_edges s
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. E \<inter> reachable \<times> UNIV = tree_edges s \<union> cross_edges s \<union> back_edges s
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<not> cond s
\<not> is_break param s
[PROOF STEP]
have [simp]: "stack s = []"
[PROOF STATE]
proof (prove)
using this:
\<not> cond s
\<not> is_break param s

goal (1 subgoal):
 1. stack s = []
[PROOF STEP]
unfolding cond_def
[PROOF STATE]
proof (prove)
using this:
\<not> ((V0 \<subseteq> {v. is_discovered v s} \<longrightarrow> \<not> is_empty_stack s) \<and> \<not> is_break param s)
\<not> is_break param s

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

goal (1 subgoal):
 1. E \<inter> reachable \<times> UNIV = tree_edges s \<union> cross_edges s \<union> back_edges s
[PROOF STEP]
hence [simp]: "pending s = {}"
[PROOF STATE]
proof (prove)
using this:
stack s = []

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

goal (1 subgoal):
 1. E \<inter> reachable \<times> UNIV = tree_edges s \<union> cross_edges s \<union> back_edges s
[PROOF STEP]
from edges_covered nc_discovered_eq_reachable[OF assms]
[PROOF STATE]
proof (chain)
picking this:
E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_edges s
dom (discovered s) = reachable
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
E \<inter> dom (discovered s) \<times> UNIV - pending s = tree_edges s \<union> cross_edges s \<union> back_edges s
dom (discovered s) = reachable

goal (1 subgoal):
 1. E \<inter> reachable \<times> UNIV = tree_edges s \<union> cross_edges s \<union> back_edges s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
E \<inter> reachable \<times> UNIV = tree_edges s \<union> cross_edges s \<union> back_edges s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma
    tree_edges_ssE: "tree_edges s \<subseteq> E" and
    tree_edges_not_pending: "tree_edges s \<subseteq> - pending s" and
    tree_edge_is_succ: "(v,w) \<in> tree_edges s \<Longrightarrow> w \<in> succ v" and
    tree_edges_discovered: "Field (tree_edges s) \<subseteq> dom (discovered s)" and

    cross_edges_ssE: "cross_edges s \<subseteq> E" and
    cross_edges_not_pending: "cross_edges s \<subseteq> - pending s" and
    cross_edge_is_succ: "(v,w) \<in> cross_edges s \<Longrightarrow> w \<in> succ v" and
    cross_edges_discovered: "Field (cross_edges s) \<subseteq> dom (discovered s)" and

    back_edges_ssE: "back_edges s \<subseteq> E" and
    back_edges_not_pending: "back_edges s \<subseteq> - pending s" and
    back_edge_is_succ: "(v,w) \<in> back_edges s \<Longrightarrow> w \<in> succ v" and
    back_edges_discovered: "Field (back_edges s) \<subseteq> dom (discovered s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((tree_edges s \<subseteq> E &&& tree_edges s \<subseteq> - pending s &&& ((v, w) \<in> tree_edges s \<Longrightarrow> w \<in> E `` {v})) &&& Field (tree_edges s) \<subseteq> dom (discovered s) &&& cross_edges s \<subseteq> E &&& cross_edges s \<subseteq> - pending s) &&& (((v, w) \<in> cross_edges s \<Longrightarrow> w \<in> E `` {v}) &&& Field (cross_edges s) \<subseteq> dom (discovered s) &&& back_edges s \<subseteq> E) &&& back_edges s \<subseteq> - pending s &&& ((v, w) \<in> back_edges s \<Longrightarrow> w \<in> E `` {v}) &&& Field (back_edges s) \<subseteq> dom (discovered s)
[PROOF STEP]
using edges_basic
[PROOF STATE]
proof (prove)
using this:
edges_basic s

goal (1 subgoal):
 1. ((tree_edges s \<subseteq> E &&& tree_edges s \<subseteq> - pending s &&& ((v, w) \<in> tree_edges s \<Longrightarrow> w \<in> E `` {v})) &&& Field (tree_edges s) \<subseteq> dom (discovered s) &&& cross_edges s \<subseteq> E &&& cross_edges s \<subseteq> - pending s) &&& (((v, w) \<in> cross_edges s \<Longrightarrow> w \<in> E `` {v}) &&& Field (cross_edges s) \<subseteq> dom (discovered s) &&& back_edges s \<subseteq> E) &&& back_edges s \<subseteq> - pending s &&& ((v, w) \<in> back_edges s \<Longrightarrow> w \<in> E `` {v}) &&& Field (back_edges s) \<subseteq> dom (discovered s)
[PROOF STEP]
unfolding edges_basic_def
[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 = {}

goal (1 subgoal):
 1. ((tree_edges s \<subseteq> E &&& tree_edges s \<subseteq> - pending s &&& ((v, w) \<in> tree_edges s \<Longrightarrow> w \<in> E `` {v})) &&& Field (tree_edges s) \<subseteq> dom (discovered s) &&& cross_edges s \<subseteq> E &&& cross_edges s \<subseteq> - pending s) &&& (((v, w) \<in> cross_edges s \<Longrightarrow> w \<in> E `` {v}) &&& Field (cross_edges s) \<subseteq> dom (discovered s) &&& back_edges s \<subseteq> E) &&& back_edges s \<subseteq> - pending s &&& ((v, w) \<in> back_edges s \<Longrightarrow> w \<in> E `` {v}) &&& Field (back_edges s) \<subseteq> dom (discovered s)
[PROOF STEP]
by auto


[STATEMENT]
lemma edges_disjoint:
   "back_edges s \<inter> cross_edges s = {}"
   "back_edges s \<inter> tree_edges s = {}"
   "cross_edges s \<inter> tree_edges s = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. back_edges s \<inter> cross_edges s = {} &&& back_edges s \<inter> tree_edges s = {} &&& cross_edges s \<inter> tree_edges s = {}
[PROOF STEP]
using edges_basic
[PROOF STATE]
proof (prove)
using this:
edges_basic s

goal (1 subgoal):
 1. back_edges s \<inter> cross_edges s = {} &&& back_edges s \<inter> tree_edges s = {} &&& cross_edges s \<inter> tree_edges s = {}
[PROOF STEP]
unfolding edges_basic_def
[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 = {}

goal (1 subgoal):
 1. back_edges s \<inter> cross_edges s = {} &&& back_edges s \<inter> tree_edges s = {} &&& cross_edges s \<inter> tree_edges s = {}
[PROOF STEP]
by auto


[STATEMENT]
lemma tree_edge_imp_discovered:
    "(v,w) \<in> tree_edges s \<Longrightarrow> v \<in> dom (discovered s)"
    "(v,w) \<in> tree_edges s \<Longrightarrow> w \<in> dom (discovered s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((v, w) \<in> tree_edges s \<Longrightarrow> v \<in> dom (discovered s)) &&& ((v, w) \<in> tree_edges s \<Longrightarrow> w \<in> dom (discovered s))
[PROOF STEP]
using tree_edges_discovered
[PROOF STATE]
proof (prove)
using this:
Field (tree_edges s) \<subseteq> dom (discovered s)

goal (1 subgoal):
 1. ((v, w) \<in> tree_edges s \<Longrightarrow> v \<in> dom (discovered s)) &&& ((v, w) \<in> tree_edges s \<Longrightarrow> w \<in> dom (discovered s))
[PROOF STEP]
by (auto simp add: Field_def)


[STATEMENT]
lemma back_edge_imp_discovered:
    "(v,w) \<in> back_edges s \<Longrightarrow> v \<in> dom (discovered s)"
    "(v,w) \<in> back_edges s \<Longrightarrow> w \<in> dom (discovered s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((v, w) \<in> back_edges s \<Longrightarrow> v \<in> dom (discovered s)) &&& ((v, w) \<in> back_edges s \<Longrightarrow> w \<in> dom (discovered s))
[PROOF STEP]
using back_edges_discovered
[PROOF STATE]
proof (prove)
using this:
Field (back_edges s) \<subseteq> dom (discovered s)

goal (1 subgoal):
 1. ((v, w) \<in> back_edges s \<Longrightarrow> v \<in> dom (discovered s)) &&& ((v, w) \<in> back_edges s \<Longrightarrow> w \<in> dom (discovered s))
[PROOF STEP]
by (auto simp add: Field_def)


[STATEMENT]
lemma cross_edge_imp_discovered:
    "(v,w) \<in> cross_edges s \<Longrightarrow> v \<in> dom (discovered s)"
    "(v,w) \<in> cross_edges s \<Longrightarrow> w \<in> dom (discovered s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((v, w) \<in> cross_edges s \<Longrightarrow> v \<in> dom (discovered s)) &&& ((v, w) \<in> cross_edges s \<Longrightarrow> w \<in> dom (discovered s))
[PROOF STEP]
using cross_edges_discovered
[PROOF STATE]
proof (prove)
using this:
Field (cross_edges s) \<subseteq> dom (discovered s)

goal (1 subgoal):
 1. ((v, w) \<in> cross_edges s \<Longrightarrow> v \<in> dom (discovered s)) &&& ((v, w) \<in> cross_edges s \<Longrightarrow> w \<in> dom (discovered s))
[PROOF STEP]
by (auto simp add: Field_def)


[STATEMENT]
lemma edge_imp_discovered:
    "(v,w) \<in> edges s \<Longrightarrow> v \<in> dom (discovered s)"
    "(v,w) \<in> edges s \<Longrightarrow> w \<in> dom (discovered s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((v, w) \<in> tree_edges s \<union> cross_edges s \<union> back_edges s \<Longrightarrow> v \<in> dom (discovered s)) &&& ((v, w) \<in> tree_edges s \<union> cross_edges s \<union> back_edges s \<Longrightarrow> w \<in> dom (discovered s))
[PROOF STEP]
using tree_edge_imp_discovered cross_edge_imp_discovered back_edge_imp_discovered
[PROOF STATE]
proof (prove)
using this:
(?v, ?w) \<in> tree_edges s \<Longrightarrow> ?v \<in> dom (discovered s)
(?v, ?w) \<in> tree_edges s \<Longrightarrow> ?w \<in> dom (discovered s)
(?v, ?w) \<in> cross_edges s \<Longrightarrow> ?v \<in> dom (discovered s)
(?v, ?w) \<in> cross_edges s \<Longrightarrow> ?w \<in> dom (discovered s)
(?v, ?w) \<in> back_edges s \<Longrightarrow> ?v \<in> dom (discovered s)
(?v, ?w) \<in> back_edges s \<Longrightarrow> ?w \<in> dom (discovered s)

goal (1 subgoal):
 1. ((v, w) \<in> tree_edges s \<union> cross_edges s \<union> back_edges s \<Longrightarrow> v \<in> dom (discovered s)) &&& ((v, w) \<in> tree_edges s \<union> cross_edges s \<union> back_edges s \<Longrightarrow> w \<in> dom (discovered s))
[PROOF STEP]
by blast+


[STATEMENT]
lemma tree_edges_finite[simp, intro!]: "finite (tree_edges s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (tree_edges s)
[PROOF STEP]
using finite_subset[OF tree_edges_discovered discovered_finite]
[PROOF STATE]
proof (prove)
using this:
finite (Field (tree_edges s))

goal (1 subgoal):
 1. finite (tree_edges s)
[PROOF STEP]
by simp


[STATEMENT]
lemma cross_edges_finite[simp, intro!]: "finite (cross_edges s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (cross_edges s)
[PROOF STEP]
using finite_subset[OF cross_edges_discovered discovered_finite]
[PROOF STATE]
proof (prove)
using this:
finite (Field (cross_edges s))

goal (1 subgoal):
 1. finite (cross_edges s)
[PROOF STEP]
by simp


[STATEMENT]
lemma edges_finite: "finite (edges s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (tree_edges s \<union> cross_edges s \<union> back_edges s)
[PROOF STEP]
by auto


[STATEMENT]
lemma tree_edge_disc_lt_fin:
    "(v,w) \<in> tree_edges s \<Longrightarrow> v \<in> dom (finished s) \<Longrightarrow> \<delta> s w < \<phi> s v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(v, w) \<in> tree_edges s; v \<in> dom (finished s)\<rbrakk> \<Longrightarrow> \<delta> s w < \<phi> s v
[PROOF STEP]
by (metis finished_succ_fin tree_edge_is_succ)


[STATEMENT]
lemma back_edge_disc_lt_fin:
    "(v,w) \<in> back_edges s \<Longrightarrow> v \<in> dom (finished s) \<Longrightarrow> \<delta> s w < \<phi> s v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(v, w) \<in> back_edges s; v \<in> dom (finished s)\<rbrakk> \<Longrightarrow> \<delta> s w < \<phi> s v
[PROOF STEP]
by (metis finished_succ_fin back_edge_is_succ)


[STATEMENT]
lemma cross_edge_disc_lt_fin:
    "(v,w) \<in> cross_edges s \<Longrightarrow> v \<in> dom (finished s) \<Longrightarrow> \<delta> s w < \<phi> s v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(v, w) \<in> cross_edges s; v \<in> dom (finished s)\<rbrakk> \<Longrightarrow> \<delta> s w < \<phi> s v
[PROOF STEP]
by (metis finished_succ_fin cross_edge_is_succ)