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

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

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

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

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

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

goal (5 subgoals):
 1. \<And>e. tree_discovered_inv (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>tree_discovered_inv s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> tree_discovered_inv s'
 3. \<And>s s' u e. \<lbrakk>tree_discovered_inv s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; pending s `` {u} = {}; u = hd (stack s); s' = finish u s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> tree_discovered_inv s'
 4. \<And>s s' u v e c b. \<lbrakk>tree_discovered_inv s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> tree_discovered_inv s'
 5. \<And>s s' u v e. \<lbrakk>tree_discovered_inv s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<notin> dom (discovered s); u = hd (stack s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> tree_discovered_inv s'
[PROOF STEP]
note TDI = \<open>tree_discovered_inv s\<close>[unfolded tree_discovered_inv_def]
[PROOF STATE]
proof (state)
this:
(tree_edges s = {} \<longrightarrow> dom (discovered s) \<subseteq> V0 \<and> (stack s = [] \<or> (\<exists>v0\<in>V0. stack s = [v0]))) \<and> (tree_edges s \<noteq> {} \<longrightarrow> (tree_edges s)\<^sup>+ `` V0 \<union> V0 = dom (discovered s) \<union> V0)

goal (5 subgoals):
 1. \<And>e. tree_discovered_inv (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>tree_discovered_inv s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s = []; v0 \<notin> dom (discovered s); v0 \<in> V0; s' = new_root v0 s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> tree_discovered_inv s'
 3. \<And>s s' u e. \<lbrakk>tree_discovered_inv s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; pending s `` {u} = {}; u = hd (stack s); s' = finish u s\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> tree_discovered_inv s'
 4. \<And>s s' u v e c b. \<lbrakk>tree_discovered_inv s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<in> dom (discovered s); u = hd (stack s); cross_edges s \<subseteq> c; back_edges s \<subseteq> b; s' = s\<lparr>pending := pending s - {(u, v)}, state.more := e, cross_edges := c, back_edges := b\<rparr>\<rbrakk> \<Longrightarrow> tree_discovered_inv s'
 5. \<And>s s' u v e. \<lbrakk>tree_discovered_inv s; cond s; DFS_invar G param s; DFS_invar G param s'; stack s \<noteq> []; v \<in> pending s `` {u}; v \<notin> dom (discovered s); u = hd (stack s); s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e\<rparr>\<rbrakk> \<Longrightarrow> tree_discovered_inv s'
[PROOF STEP]
have "tree_edges s' = {} \<longrightarrow> dom (discovered s') \<subseteq> V0 \<and> (stack s' = [] \<or> (\<exists>v0\<in>V0. stack s' = [v0]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tree_edges s' = {} \<longrightarrow> dom (discovered s') \<subseteq> V0 \<and> (stack s' = [] \<or> (\<exists>v0\<in>V0. stack s' = [v0]))
[PROOF STEP]
by simp \<comment> \<open>@{text "tree_edges s' \<noteq> {}"}\<close>
[PROOF STATE]
proof (state)
this:
tree_edges s' = {} \<longrightarrow> dom (discovered s') \<subseteq> V0 \<and> (stack s' = [] \<or> (\<exists>v0\<in>V0. stack s' = [v0]))

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

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

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

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

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>(y, x) \<in> (tree_edges s')\<^sup>+; y \<in> V0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(y, x) \<in> (tree_edges s')\<^sup>+
y \<in> V0

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

goal (2 subgoals):
 1. tree_edges s = {} \<Longrightarrow> x \<in> dom (discovered s') \<union> V0
 2. tree_edges s \<noteq> {} \<Longrightarrow> x \<in> dom (discovered s') \<union> V0
[PROOF STEP]
with discover A
[PROOF STATE]
proof (chain)
picking this:
tree_discovered_inv s
cond s
DFS_invar G param s
DFS_invar G param s'
stack s \<noteq> []
v \<in> pending s `` {u}
v \<notin> dom (discovered s)
u = hd (stack s)
s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e_\<rparr>
x \<in> (tree_edges s')\<^sup>+ `` V0 \<union> V0
x \<notin> V0
tree_edges s = {}
[PROOF STEP]
have "(tree_edges s')\<^sup>+ = {(hd (stack s), v)}"
[PROOF STATE]
proof (prove)
using this:
tree_discovered_inv s
cond s
DFS_invar G param s
DFS_invar G param s'
stack s \<noteq> []
v \<in> pending s `` {u}
v \<notin> dom (discovered s)
u = hd (stack s)
s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e_\<rparr>
x \<in> (tree_edges s')\<^sup>+ `` V0 \<union> V0
x \<notin> V0
tree_edges s = {}

goal (1 subgoal):
 1. (tree_edges s')\<^sup>+ = {(hd (stack s), v)}
[PROOF STEP]
by (simp add: trancl_single)
[PROOF STATE]
proof (state)
this:
(tree_edges s')\<^sup>+ = {(hd (stack s), v)}

goal (2 subgoals):
 1. tree_edges s = {} \<Longrightarrow> x \<in> dom (discovered s') \<union> V0
 2. tree_edges s \<noteq> {} \<Longrightarrow> x \<in> dom (discovered s') \<union> V0
[PROOF STEP]
with A
[PROOF STATE]
proof (chain)
picking this:
x \<in> (tree_edges s')\<^sup>+ `` V0 \<union> V0
x \<notin> V0
(tree_edges s')\<^sup>+ = {(hd (stack s), v)}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<in> (tree_edges s')\<^sup>+ `` V0 \<union> V0
x \<notin> V0
(tree_edges s')\<^sup>+ = {(hd (stack s), v)}

goal (1 subgoal):
 1. x \<in> dom (discovered s') \<union> V0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> dom (discovered s') \<union> V0

goal (1 subgoal):
 1. tree_edges s \<noteq> {} \<Longrightarrow> x \<in> dom (discovered s') \<union> V0
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. tree_edges s \<noteq> {} \<Longrightarrow> x \<in> dom (discovered s') \<union> V0
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
tree_edges s \<noteq> {}

goal (1 subgoal):
 1. tree_edges s \<noteq> {} \<Longrightarrow> x \<in> dom (discovered s') \<union> V0
[PROOF STEP]
note t_ne = this
[PROOF STATE]
proof (state)
this:
tree_edges s \<noteq> {}

goal (1 subgoal):
 1. tree_edges s \<noteq> {} \<Longrightarrow> x \<in> dom (discovered s') \<union> V0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> dom (discovered s') \<union> V0
[PROOF STEP]
proof (cases "x = v")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = v \<Longrightarrow> x \<in> dom (discovered s') \<union> V0
 2. x \<noteq> v \<Longrightarrow> x \<in> dom (discovered s') \<union> V0
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x = v

goal (2 subgoals):
 1. x = v \<Longrightarrow> x \<in> dom (discovered s') \<union> V0
 2. x \<noteq> v \<Longrightarrow> x \<in> dom (discovered s') \<union> V0
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
x = v

goal (1 subgoal):
 1. x \<in> dom (discovered s') \<union> V0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<in> dom (discovered s') \<union> V0

goal (1 subgoal):
 1. x \<noteq> v \<Longrightarrow> x \<in> dom (discovered s') \<union> V0
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<noteq> v \<Longrightarrow> x \<in> dom (discovered s') \<union> V0
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
x \<noteq> v

goal (1 subgoal):
 1. x \<noteq> v \<Longrightarrow> x \<in> dom (discovered s') \<union> V0
[PROOF STEP]
with y
[PROOF STATE]
proof (chain)
picking this:
(y, x) \<in> (tree_edges s')\<^sup>+
y \<in> V0
x \<noteq> v
[PROOF STEP]
have "(y,x) \<in> (tree_edges s)\<^sup>+"
[PROOF STATE]
proof (prove)
using this:
(y, x) \<in> (tree_edges s')\<^sup>+
y \<in> V0
x \<noteq> v

goal (1 subgoal):
 1. (y, x) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
proof (induct rule: trancl_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ya. \<lbrakk>(y, ya) \<in> tree_edges s'; y \<in> V0; ya \<noteq> v\<rbrakk> \<Longrightarrow> (y, ya) \<in> (tree_edges s)\<^sup>+
 2. \<And>ya z. \<lbrakk>(y, ya) \<in> (tree_edges s')\<^sup>+; (ya, z) \<in> tree_edges s'; \<lbrakk>y \<in> V0; ya \<noteq> v\<rbrakk> \<Longrightarrow> (y, ya) \<in> (tree_edges s)\<^sup>+; y \<in> V0; z \<noteq> v\<rbrakk> \<Longrightarrow> (y, z) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
case (step a b)
[PROOF STATE]
proof (state)
this:
(y, a) \<in> (tree_edges s')\<^sup>+
(a, b) \<in> tree_edges s'
\<lbrakk>y \<in> V0; a \<noteq> v\<rbrakk> \<Longrightarrow> (y, a) \<in> (tree_edges s)\<^sup>+
y \<in> V0
b \<noteq> v

goal (2 subgoals):
 1. \<And>ya. \<lbrakk>(y, ya) \<in> tree_edges s'; y \<in> V0; ya \<noteq> v\<rbrakk> \<Longrightarrow> (y, ya) \<in> (tree_edges s)\<^sup>+
 2. \<And>ya z. \<lbrakk>(y, ya) \<in> (tree_edges s')\<^sup>+; (ya, z) \<in> tree_edges s'; \<lbrakk>y \<in> V0; ya \<noteq> v\<rbrakk> \<Longrightarrow> (y, ya) \<in> (tree_edges s)\<^sup>+; y \<in> V0; z \<noteq> v\<rbrakk> \<Longrightarrow> (y, z) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
hence "(a,b) \<in> tree_edges s"
[PROOF STATE]
proof (prove)
using this:
(y, a) \<in> (tree_edges s')\<^sup>+
(a, b) \<in> tree_edges s'
\<lbrakk>y \<in> V0; a \<noteq> v\<rbrakk> \<Longrightarrow> (y, a) \<in> (tree_edges s)\<^sup>+
y \<in> V0
b \<noteq> v

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

goal (2 subgoals):
 1. \<And>ya. \<lbrakk>(y, ya) \<in> tree_edges s'; y \<in> V0; ya \<noteq> v\<rbrakk> \<Longrightarrow> (y, ya) \<in> (tree_edges s)\<^sup>+
 2. \<And>ya z. \<lbrakk>(y, ya) \<in> (tree_edges s')\<^sup>+; (ya, z) \<in> tree_edges s'; \<lbrakk>y \<in> V0; ya \<noteq> v\<rbrakk> \<Longrightarrow> (y, ya) \<in> (tree_edges s)\<^sup>+; y \<in> V0; z \<noteq> v\<rbrakk> \<Longrightarrow> (y, z) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
with tree_edge_imp_discovered
[PROOF STATE]
proof (chain)
picking this:
(?v, ?w) \<in> tree_edges s \<Longrightarrow> ?v \<in> dom (discovered s)
(?v, ?w) \<in> tree_edges s \<Longrightarrow> ?w \<in> dom (discovered s)
(a, b) \<in> tree_edges s
[PROOF STEP]
have "a \<in> dom (discovered s)"
[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)
(a, b) \<in> tree_edges s

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

goal (2 subgoals):
 1. \<And>ya. \<lbrakk>(y, ya) \<in> tree_edges s'; y \<in> V0; ya \<noteq> v\<rbrakk> \<Longrightarrow> (y, ya) \<in> (tree_edges s)\<^sup>+
 2. \<And>ya z. \<lbrakk>(y, ya) \<in> (tree_edges s')\<^sup>+; (ya, z) \<in> tree_edges s'; \<lbrakk>y \<in> V0; ya \<noteq> v\<rbrakk> \<Longrightarrow> (y, ya) \<in> (tree_edges s)\<^sup>+; y \<in> V0; z \<noteq> v\<rbrakk> \<Longrightarrow> (y, z) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
with discover
[PROOF STATE]
proof (chain)
picking this:
tree_discovered_inv s
cond s
DFS_invar G param s
DFS_invar G param s'
stack s \<noteq> []
v \<in> pending s `` {u}
v \<notin> dom (discovered s)
u = hd (stack s)
s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e_\<rparr>
a \<in> dom (discovered s)
[PROOF STEP]
have "a \<noteq> v"
[PROOF STATE]
proof (prove)
using this:
tree_discovered_inv s
cond s
DFS_invar G param s
DFS_invar G param s'
stack s \<noteq> []
v \<in> pending s `` {u}
v \<notin> dom (discovered s)
u = hd (stack s)
s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e_\<rparr>
a \<in> dom (discovered s)

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

goal (2 subgoals):
 1. \<And>ya. \<lbrakk>(y, ya) \<in> tree_edges s'; y \<in> V0; ya \<noteq> v\<rbrakk> \<Longrightarrow> (y, ya) \<in> (tree_edges s)\<^sup>+
 2. \<And>ya z. \<lbrakk>(y, ya) \<in> (tree_edges s')\<^sup>+; (ya, z) \<in> tree_edges s'; \<lbrakk>y \<in> V0; ya \<noteq> v\<rbrakk> \<Longrightarrow> (y, ya) \<in> (tree_edges s)\<^sup>+; y \<in> V0; z \<noteq> v\<rbrakk> \<Longrightarrow> (y, z) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
with step
[PROOF STATE]
proof (chain)
picking this:
(y, a) \<in> (tree_edges s')\<^sup>+
(a, b) \<in> tree_edges s'
\<lbrakk>y \<in> V0; a \<noteq> v\<rbrakk> \<Longrightarrow> (y, a) \<in> (tree_edges s)\<^sup>+
y \<in> V0
b \<noteq> v
a \<noteq> v
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(y, a) \<in> (tree_edges s')\<^sup>+
(a, b) \<in> tree_edges s'
\<lbrakk>y \<in> V0; a \<noteq> v\<rbrakk> \<Longrightarrow> (y, a) \<in> (tree_edges s)\<^sup>+
y \<in> V0
b \<noteq> v
a \<noteq> v

goal (1 subgoal):
 1. (y, b) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(y, b) \<in> (tree_edges s)\<^sup>+

goal (1 subgoal):
 1. \<And>ya. \<lbrakk>(y, ya) \<in> tree_edges s'; y \<in> V0; ya \<noteq> v\<rbrakk> \<Longrightarrow> (y, ya) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
(y, x) \<in> (tree_edges s)\<^sup>+

goal (1 subgoal):
 1. x \<noteq> v \<Longrightarrow> x \<in> dom (discovered s') \<union> V0
[PROOF STEP]
with \<open>y \<in> V0\<close>
[PROOF STATE]
proof (chain)
picking this:
y \<in> V0
(y, x) \<in> (tree_edges s)\<^sup>+
[PROOF STEP]
have "x \<in> (tree_edges s)\<^sup>+ `` V0"
[PROOF STATE]
proof (prove)
using this:
y \<in> V0
(y, x) \<in> (tree_edges s)\<^sup>+

goal (1 subgoal):
 1. x \<in> (tree_edges s)\<^sup>+ `` V0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> (tree_edges s)\<^sup>+ `` V0

goal (1 subgoal):
 1. x \<noteq> v \<Longrightarrow> x \<in> dom (discovered s') \<union> V0
[PROOF STEP]
with t_ne TDI
[PROOF STATE]
proof (chain)
picking this:
tree_edges s \<noteq> {}
(tree_edges s = {} \<longrightarrow> dom (discovered s) \<subseteq> V0 \<and> (stack s = [] \<or> (\<exists>v0\<in>V0. stack s = [v0]))) \<and> (tree_edges s \<noteq> {} \<longrightarrow> (tree_edges s)\<^sup>+ `` V0 \<union> V0 = dom (discovered s) \<union> V0)
x \<in> (tree_edges s)\<^sup>+ `` V0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
tree_edges s \<noteq> {}
(tree_edges s = {} \<longrightarrow> dom (discovered s) \<subseteq> V0 \<and> (stack s = [] \<or> (\<exists>v0\<in>V0. stack s = [v0]))) \<and> (tree_edges s \<noteq> {} \<longrightarrow> (tree_edges s)\<^sup>+ `` V0 \<union> V0 = dom (discovered s) \<union> V0)
x \<in> (tree_edges s)\<^sup>+ `` V0

goal (1 subgoal):
 1. x \<in> dom (discovered s') \<union> V0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> dom (discovered s') \<union> V0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<in> dom (discovered s') \<union> V0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<in> dom (discovered s') \<union> V0

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

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

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

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

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

goal (1 subgoal):
 1. x \<in> dom (discovered s')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<in> dom (discovered s')

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

goal (2 subgoals):
 1. tree_edges s = {} \<Longrightarrow> x \<in> (tree_edges s')\<^sup>+ `` V0 \<union> V0
 2. tree_edges s \<noteq> {} \<Longrightarrow> x \<in> (tree_edges s')\<^sup>+ `` V0 \<union> V0
[PROOF STEP]
with trancl_single
[PROOF STATE]
proof (chain)
picking this:
{(?a, ?b)}\<^sup>+ = {(?a, ?b)}
tree_edges s = {}
[PROOF STEP]
have "(tree_edges s')\<^sup>+ = {(hd (stack s), v)}"
[PROOF STATE]
proof (prove)
using this:
{(?a, ?b)}\<^sup>+ = {(?a, ?b)}
tree_edges s = {}

goal (1 subgoal):
 1. (tree_edges s')\<^sup>+ = {(hd (stack s), v)}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(tree_edges s')\<^sup>+ = {(hd (stack s), v)}

goal (2 subgoals):
 1. tree_edges s = {} \<Longrightarrow> x \<in> (tree_edges s')\<^sup>+ `` V0 \<union> V0
 2. tree_edges s \<noteq> {} \<Longrightarrow> x \<in> (tree_edges s')\<^sup>+ `` V0 \<union> V0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(tree_edges s')\<^sup>+ = {(hd (stack s), v)}

goal (2 subgoals):
 1. tree_edges s = {} \<Longrightarrow> x \<in> (tree_edges s')\<^sup>+ `` V0 \<union> V0
 2. tree_edges s \<noteq> {} \<Longrightarrow> x \<in> (tree_edges s')\<^sup>+ `` V0 \<union> V0
[PROOF STEP]
from True TDI
[PROOF STATE]
proof (chain)
picking this:
tree_edges s = {}
(tree_edges s = {} \<longrightarrow> dom (discovered s) \<subseteq> V0 \<and> (stack s = [] \<or> (\<exists>v0\<in>V0. stack s = [v0]))) \<and> (tree_edges s \<noteq> {} \<longrightarrow> (tree_edges s)\<^sup>+ `` V0 \<union> V0 = dom (discovered s) \<union> V0)
[PROOF STEP]
have "hd (stack s) \<in> V0" "dom (discovered s) \<subseteq> V0"
[PROOF STATE]
proof (prove)
using this:
tree_edges s = {}
(tree_edges s = {} \<longrightarrow> dom (discovered s) \<subseteq> V0 \<and> (stack s = [] \<or> (\<exists>v0\<in>V0. stack s = [v0]))) \<and> (tree_edges s \<noteq> {} \<longrightarrow> (tree_edges s)\<^sup>+ `` V0 \<union> V0 = dom (discovered s) \<union> V0)

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

goal (2 subgoals):
 1. tree_edges s = {} \<Longrightarrow> x \<in> (tree_edges s')\<^sup>+ `` V0 \<union> V0
 2. tree_edges s \<noteq> {} \<Longrightarrow> x \<in> (tree_edges s')\<^sup>+ `` V0 \<union> V0
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(tree_edges s')\<^sup>+ = {(hd (stack s), v)}
hd (stack s) \<in> V0
dom (discovered s) \<subseteq> V0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(tree_edges s')\<^sup>+ = {(hd (stack s), v)}
hd (stack s) \<in> V0
dom (discovered s) \<subseteq> V0

goal (1 subgoal):
 1. x \<in> (tree_edges s')\<^sup>+ `` V0 \<union> V0
[PROOF STEP]
using A \<open>x\<notin>V0\<close>
[PROOF STATE]
proof (prove)
using this:
(tree_edges s')\<^sup>+ = {(hd (stack s), v)}
hd (stack s) \<in> V0
dom (discovered s) \<subseteq> V0
x \<in> dom (discovered s')
x \<notin> V0

goal (1 subgoal):
 1. x \<in> (tree_edges s')\<^sup>+ `` V0 \<union> V0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> (tree_edges s')\<^sup>+ `` V0 \<union> V0

goal (1 subgoal):
 1. tree_edges s \<noteq> {} \<Longrightarrow> x \<in> (tree_edges s')\<^sup>+ `` V0 \<union> V0
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. tree_edges s \<noteq> {} \<Longrightarrow> x \<in> (tree_edges s')\<^sup>+ `` V0 \<union> V0
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
tree_edges s \<noteq> {}

goal (1 subgoal):
 1. tree_edges s \<noteq> {} \<Longrightarrow> x \<in> (tree_edges s')\<^sup>+ `` V0 \<union> V0
[PROOF STEP]
note t_ne = this
[PROOF STATE]
proof (state)
this:
tree_edges s \<noteq> {}

goal (1 subgoal):
 1. tree_edges s \<noteq> {} \<Longrightarrow> x \<in> (tree_edges s')\<^sup>+ `` V0 \<union> V0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> (tree_edges s')\<^sup>+ `` V0 \<union> V0
[PROOF STEP]
proof (cases "x=v")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = v \<Longrightarrow> x \<in> (tree_edges s')\<^sup>+ `` V0 \<union> V0
 2. x \<noteq> v \<Longrightarrow> x \<in> (tree_edges s')\<^sup>+ `` V0 \<union> V0
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
x \<noteq> v

goal (2 subgoals):
 1. x = v \<Longrightarrow> x \<in> (tree_edges s')\<^sup>+ `` V0 \<union> V0
 2. x \<noteq> v \<Longrightarrow> x \<in> (tree_edges s')\<^sup>+ `` V0 \<union> V0
[PROOF STEP]
with A
[PROOF STATE]
proof (chain)
picking this:
x \<in> dom (discovered s')
x \<noteq> v
[PROOF STEP]
have "x \<in> dom (discovered s)"
[PROOF STATE]
proof (prove)
using this:
x \<in> dom (discovered s')
x \<noteq> v

goal (1 subgoal):
 1. x \<in> dom (discovered s)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<in> dom (discovered s)

goal (2 subgoals):
 1. x = v \<Longrightarrow> x \<in> (tree_edges s')\<^sup>+ `` V0 \<union> V0
 2. x \<noteq> v \<Longrightarrow> x \<in> (tree_edges s')\<^sup>+ `` V0 \<union> V0
[PROOF STEP]
with TDI t_ne \<open>x \<notin> V0\<close>
[PROOF STATE]
proof (chain)
picking this:
(tree_edges s = {} \<longrightarrow> dom (discovered s) \<subseteq> V0 \<and> (stack s = [] \<or> (\<exists>v0\<in>V0. stack s = [v0]))) \<and> (tree_edges s \<noteq> {} \<longrightarrow> (tree_edges s)\<^sup>+ `` V0 \<union> V0 = dom (discovered s) \<union> V0)
tree_edges s \<noteq> {}
x \<notin> V0
x \<in> dom (discovered s)
[PROOF STEP]
have "x \<in> (tree_edges s)\<^sup>+ `` V0"
[PROOF STATE]
proof (prove)
using this:
(tree_edges s = {} \<longrightarrow> dom (discovered s) \<subseteq> V0 \<and> (stack s = [] \<or> (\<exists>v0\<in>V0. stack s = [v0]))) \<and> (tree_edges s \<noteq> {} \<longrightarrow> (tree_edges s)\<^sup>+ `` V0 \<union> V0 = dom (discovered s) \<union> V0)
tree_edges s \<noteq> {}
x \<notin> V0
x \<in> dom (discovered s)

goal (1 subgoal):
 1. x \<in> (tree_edges s)\<^sup>+ `` V0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> (tree_edges s)\<^sup>+ `` V0

goal (2 subgoals):
 1. x = v \<Longrightarrow> x \<in> (tree_edges s')\<^sup>+ `` V0 \<union> V0
 2. x \<noteq> v \<Longrightarrow> x \<in> (tree_edges s')\<^sup>+ `` V0 \<union> V0
[PROOF STEP]
with trancl_sub_insert_trancl
[PROOF STATE]
proof (chain)
picking this:
?R\<^sup>+ \<subseteq> (insert ?x ?R)\<^sup>+
x \<in> (tree_edges s)\<^sup>+ `` V0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?R\<^sup>+ \<subseteq> (insert ?x ?R)\<^sup>+
x \<in> (tree_edges s)\<^sup>+ `` V0

goal (1 subgoal):
 1. x \<in> (tree_edges s')\<^sup>+ `` V0 \<union> V0
[PROOF STEP]
by simp blast
[PROOF STATE]
proof (state)
this:
x \<in> (tree_edges s')\<^sup>+ `` V0 \<union> V0

goal (1 subgoal):
 1. x = v \<Longrightarrow> x \<in> (tree_edges s')\<^sup>+ `` V0 \<union> V0
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x = v \<Longrightarrow> x \<in> (tree_edges s')\<^sup>+ `` V0 \<union> V0
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x = v

goal (1 subgoal):
 1. x = v \<Longrightarrow> x \<in> (tree_edges s')\<^sup>+ `` V0 \<union> V0
[PROOF STEP]
from t_ne TDI
[PROOF STATE]
proof (chain)
picking this:
tree_edges s \<noteq> {}
(tree_edges s = {} \<longrightarrow> dom (discovered s) \<subseteq> V0 \<and> (stack s = [] \<or> (\<exists>v0\<in>V0. stack s = [v0]))) \<and> (tree_edges s \<noteq> {} \<longrightarrow> (tree_edges s)\<^sup>+ `` V0 \<union> V0 = dom (discovered s) \<union> V0)
[PROOF STEP]
have "dom (discovered s) \<union> V0 = (tree_edges s)\<^sup>+ `` V0 \<union> V0"
[PROOF STATE]
proof (prove)
using this:
tree_edges s \<noteq> {}
(tree_edges s = {} \<longrightarrow> dom (discovered s) \<subseteq> V0 \<and> (stack s = [] \<or> (\<exists>v0\<in>V0. stack s = [v0]))) \<and> (tree_edges s \<noteq> {} \<longrightarrow> (tree_edges s)\<^sup>+ `` V0 \<union> V0 = dom (discovered s) \<union> V0)

goal (1 subgoal):
 1. dom (discovered s) \<union> V0 = (tree_edges s)\<^sup>+ `` V0 \<union> V0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dom (discovered s) \<union> V0 = (tree_edges s)\<^sup>+ `` V0 \<union> V0

goal (1 subgoal):
 1. x = v \<Longrightarrow> x \<in> (tree_edges s')\<^sup>+ `` V0 \<union> V0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
dom (discovered s) \<union> V0 = (tree_edges s)\<^sup>+ `` V0 \<union> V0

goal (1 subgoal):
 1. x = v \<Longrightarrow> x \<in> (tree_edges s')\<^sup>+ `` V0 \<union> V0
[PROOF STEP]
from stack_is_tree_path[OF NE]
[PROOF STATE]
proof (chain)
picking this:
\<exists>v0\<in>V0. path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))
[PROOF STEP]
obtain v0 where "v0 \<in> V0" and
            "(v0, hd (stack s)) \<in> (tree_edges s)\<^sup>*"
[PROOF STATE]
proof (prove)
using this:
\<exists>v0\<in>V0. path (tree_edges s) v0 (rev (tl (stack s))) (hd (stack s))

goal (1 subgoal):
 1. (\<And>v0. \<lbrakk>v0 \<in> V0; (v0, hd (stack s)) \<in> (tree_edges s)\<^sup>*\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (blast intro!: path_is_rtrancl)
[PROOF STATE]
proof (state)
this:
v0 \<in> V0
(v0, hd (stack s)) \<in> (tree_edges s)\<^sup>*

goal (1 subgoal):
 1. x = v \<Longrightarrow> x \<in> (tree_edges s')\<^sup>+ `` V0 \<union> V0
[PROOF STEP]
with EQ
[PROOF STATE]
proof (chain)
picking this:
stack s' = v # stack s
tree_edges s' = insert (hd (stack s), v) (tree_edges s)
discovered s' = discovered s(v \<mapsto> counter s)
v0 \<in> V0
(v0, hd (stack s)) \<in> (tree_edges s)\<^sup>*
[PROOF STEP]
have "(v0, hd (stack s)) \<in> (tree_edges s')\<^sup>*"
[PROOF STATE]
proof (prove)
using this:
stack s' = v # stack s
tree_edges s' = insert (hd (stack s), v) (tree_edges s)
discovered s' = discovered s(v \<mapsto> counter s)
v0 \<in> V0
(v0, hd (stack s)) \<in> (tree_edges s)\<^sup>*

goal (1 subgoal):
 1. (v0, hd (stack s)) \<in> (tree_edges s')\<^sup>*
[PROOF STEP]
by (auto intro: rtrancl_mono_mp)
[PROOF STATE]
proof (state)
this:
(v0, hd (stack s)) \<in> (tree_edges s')\<^sup>*

goal (1 subgoal):
 1. x = v \<Longrightarrow> x \<in> (tree_edges s')\<^sup>+ `` V0 \<union> V0
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
dom (discovered s) \<union> V0 = (tree_edges s)\<^sup>+ `` V0 \<union> V0
(v0, hd (stack s)) \<in> (tree_edges s')\<^sup>*
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dom (discovered s) \<union> V0 = (tree_edges s)\<^sup>+ `` V0 \<union> V0
(v0, hd (stack s)) \<in> (tree_edges s')\<^sup>*

goal (1 subgoal):
 1. x \<in> (tree_edges s')\<^sup>+ `` V0 \<union> V0
[PROOF STEP]
using \<open>v0 \<in> V0\<close> True
[PROOF STATE]
proof (prove)
using this:
dom (discovered s) \<union> V0 = (tree_edges s)\<^sup>+ `` V0 \<union> V0
(v0, hd (stack s)) \<in> (tree_edges s')\<^sup>*
v0 \<in> V0
x = v

goal (1 subgoal):
 1. x \<in> (tree_edges s')\<^sup>+ `` V0 \<union> V0
[PROOF STEP]
by (auto elim: rtrancl_into_trancl1)
[PROOF STATE]
proof (state)
this:
x \<in> (tree_edges s')\<^sup>+ `` V0 \<union> V0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<in> (tree_edges s')\<^sup>+ `` V0 \<union> V0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<in> (tree_edges s')\<^sup>+ `` V0 \<union> V0

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

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

goal (1 subgoal):
 1. (tree_edges s')\<^sup>+ `` V0 \<union> V0 = dom (discovered s') \<union> V0
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(tree_edges s')\<^sup>+ `` V0 \<union> V0 = dom (discovered s') \<union> V0

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

goal (1 subgoal):
 1. tree_discovered_inv s'
[PROOF STEP]
by (simp add: tree_discovered_inv_def)
[PROOF STATE]
proof (state)
this:
tree_discovered_inv s'

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


[STATEMENT]
lemma (in DFS_invar) discovered_iff_tree_path:
    "v \<notin> V0 \<Longrightarrow> v \<in> dom (discovered s) \<longleftrightarrow> (\<exists>v0\<in>V0. (v0,v) \<in> (tree_edges s)\<^sup>+)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<notin> V0 \<Longrightarrow> (v \<in> dom (discovered s)) = (\<exists>v0\<in>V0. (v0, v) \<in> (tree_edges s)\<^sup>+)
[PROOF STEP]
using tree_discovered_inv
[PROOF STATE]
proof (prove)
using this:
tree_discovered_inv s

goal (1 subgoal):
 1. v \<notin> V0 \<Longrightarrow> (v \<in> dom (discovered s)) = (\<exists>v0\<in>V0. (v0, v) \<in> (tree_edges s)\<^sup>+)
[PROOF STEP]
by (auto simp add: tree_discovered_inv_def)