[STATEMENT]
lemma i_parenthesis: "is_invar parenthesis"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_invar parenthesis
[PROOF STEP]
proof (induct rule: is_invarI)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>e. parenthesis (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>parenthesis 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> parenthesis s'
 3. \<And>s s' u e. \<lbrakk>parenthesis 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> parenthesis s'
 4. \<And>s s' u v e c b. \<lbrakk>parenthesis 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> parenthesis s'
 5. \<And>s s' u v e. \<lbrakk>parenthesis 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> parenthesis s'
[PROOF STEP]
case (finish s s')
[PROOF STATE]
proof (state)
this:
parenthesis 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>

goal (5 subgoals):
 1. \<And>e. parenthesis (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>parenthesis 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> parenthesis s'
 3. \<And>s s' u e. \<lbrakk>parenthesis 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> parenthesis s'
 4. \<And>s s' u v e c b. \<lbrakk>parenthesis 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> parenthesis s'
 5. \<And>s s' u v e. \<lbrakk>parenthesis 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> parenthesis s'
[PROOF STEP]
hence EQ[simp]: "discovered s' = discovered s"
                    "counter s' = Suc (counter s)"
                    "finished s' = finished s(hd (stack s) \<mapsto> counter s)"
[PROOF STATE]
proof (prove)
using this:
parenthesis 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>

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

goal (5 subgoals):
 1. \<And>e. parenthesis (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>parenthesis 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> parenthesis s'
 3. \<And>s s' u e. \<lbrakk>parenthesis 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> parenthesis s'
 4. \<And>s s' u v e c b. \<lbrakk>parenthesis 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> parenthesis s'
 5. \<And>s s' u v e. \<lbrakk>parenthesis 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> parenthesis s'
[PROOF STEP]
from finish
[PROOF STATE]
proof (chain)
picking this:
parenthesis 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>
[PROOF STEP]
interpret DFS_invar where s=s
[PROOF STATE]
proof (prove)
using this:
parenthesis 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>

goal (1 subgoal):
 1. DFS_invar G param s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>e. parenthesis (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>parenthesis 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> parenthesis s'
 3. \<And>s s' u e. \<lbrakk>parenthesis 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> parenthesis s'
 4. \<And>s s' u v e c b. \<lbrakk>parenthesis 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> parenthesis s'
 5. \<And>s s' u v e. \<lbrakk>parenthesis 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> parenthesis s'
[PROOF STEP]
from finish
[PROOF STATE]
proof (chain)
picking this:
parenthesis 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>
[PROOF STEP]
have NE[simp]: "stack s \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
parenthesis 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>

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

goal (5 subgoals):
 1. \<And>e. parenthesis (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>parenthesis 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> parenthesis s'
 3. \<And>s s' u e. \<lbrakk>parenthesis 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> parenthesis s'
 4. \<And>s s' u v e c b. \<lbrakk>parenthesis 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> parenthesis s'
 5. \<And>s s' u v e. \<lbrakk>parenthesis 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> parenthesis s'
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
stack s \<noteq> []

goal (5 subgoals):
 1. \<And>e. parenthesis (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>parenthesis 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> parenthesis s'
 3. \<And>s s' u e. \<lbrakk>parenthesis 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> parenthesis s'
 4. \<And>s s' u v e c b. \<lbrakk>parenthesis 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> parenthesis s'
 5. \<And>s s' u v e. \<lbrakk>parenthesis 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> parenthesis s'
[PROOF STEP]
fix x y
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>e. parenthesis (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>parenthesis 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> parenthesis s'
 3. \<And>s s' u e. \<lbrakk>parenthesis 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> parenthesis s'
 4. \<And>s s' u v e c b. \<lbrakk>parenthesis 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> parenthesis s'
 5. \<And>s s' u v e. \<lbrakk>parenthesis 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> parenthesis s'
[PROOF STEP]
assume  dom: "x \<in> dom (discovered s')" "y \<in> dom (discovered s')"
        and \<delta>: "\<delta> s' x < \<delta> s' y"
        and f: "x \<in> dom (finished s')"
[PROOF STATE]
proof (state)
this:
x \<in> dom (discovered s')
y \<in> dom (discovered s')
\<delta> s' x < \<delta> s' y
x \<in> dom (finished s')

goal (5 subgoals):
 1. \<And>e. parenthesis (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>parenthesis 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> parenthesis s'
 3. \<And>s s' u e. \<lbrakk>parenthesis 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> parenthesis s'
 4. \<And>s s' u v e c b. \<lbrakk>parenthesis 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> parenthesis s'
 5. \<And>s s' u v e. \<lbrakk>parenthesis 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> parenthesis s'
[PROOF STEP]
hence neq: "x \<noteq> y"
[PROOF STATE]
proof (prove)
using this:
x \<in> dom (discovered s')
y \<in> dom (discovered s')
\<delta> s' x < \<delta> s' y
x \<in> dom (finished s')

goal (1 subgoal):
 1. x \<noteq> y
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
x \<noteq> y

goal (5 subgoals):
 1. \<And>e. parenthesis (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>parenthesis 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> parenthesis s'
 3. \<And>s s' u e. \<lbrakk>parenthesis 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> parenthesis s'
 4. \<And>s s' u v e c b. \<lbrakk>parenthesis 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> parenthesis s'
 5. \<And>s s' u v e. \<lbrakk>parenthesis 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> parenthesis s'
[PROOF STEP]
note assms = dom \<delta> f EQ
[PROOF STATE]
proof (state)
this:
x \<in> dom (discovered s')
y \<in> dom (discovered s')
\<delta> s' x < \<delta> s' y
x \<in> dom (finished s')
discovered s' = discovered s
counter s' = Suc (counter s)
finished s' = finished s(hd (stack s) \<mapsto> counter s)

goal (5 subgoals):
 1. \<And>e. parenthesis (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>parenthesis 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> parenthesis s'
 3. \<And>s s' u e. \<lbrakk>parenthesis 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> parenthesis s'
 4. \<And>s s' u v e c b. \<lbrakk>parenthesis 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> parenthesis s'
 5. \<And>s s' u v e. \<lbrakk>parenthesis 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> parenthesis s'
[PROOF STEP]
let ?DISJ = "\<phi> s' x < \<delta> s' y"
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>e. parenthesis (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>parenthesis 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> parenthesis s'
 3. \<And>s s' u e. \<lbrakk>parenthesis 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> parenthesis s'
 4. \<And>s s' u v e c b. \<lbrakk>parenthesis 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> parenthesis s'
 5. \<And>s s' u v e. \<lbrakk>parenthesis 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> parenthesis s'
[PROOF STEP]
let ?IN = "\<delta> s' y < \<phi> s' x \<and> y \<in> dom (finished s') \<and> \<phi> s' y < \<phi> s' x"
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>e. parenthesis (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>parenthesis 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> parenthesis s'
 3. \<And>s s' u e. \<lbrakk>parenthesis 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> parenthesis s'
 4. \<And>s s' u v e c b. \<lbrakk>parenthesis 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> parenthesis s'
 5. \<And>s s' u v e. \<lbrakk>parenthesis 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> parenthesis s'
[PROOF STEP]
have "?DISJ \<or> ?IN"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> s' x < \<delta> s' y \<or> \<delta> s' y < \<phi> s' x \<and> y \<in> dom (finished s') \<and> \<phi> s' y < \<phi> s' x
[PROOF STEP]
proof (cases "x = hd (stack s)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = hd (stack s) \<Longrightarrow> \<phi> s' x < \<delta> s' y \<or> \<delta> s' y < \<phi> s' x \<and> y \<in> dom (finished s') \<and> \<phi> s' y < \<phi> s' x
 2. x \<noteq> hd (stack s) \<Longrightarrow> \<phi> s' x < \<delta> s' y \<or> \<delta> s' y < \<phi> s' x \<and> y \<in> dom (finished s') \<and> \<phi> s' y < \<phi> s' x
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x = hd (stack s)

goal (2 subgoals):
 1. x = hd (stack s) \<Longrightarrow> \<phi> s' x < \<delta> s' y \<or> \<delta> s' y < \<phi> s' x \<and> y \<in> dom (finished s') \<and> \<phi> s' y < \<phi> s' x
 2. x \<noteq> hd (stack s) \<Longrightarrow> \<phi> s' x < \<delta> s' y \<or> \<delta> s' y < \<phi> s' x \<and> y \<in> dom (finished s') \<and> \<phi> s' y < \<phi> s' x
[PROOF STEP]
note x_is_hd = this
[PROOF STATE]
proof (state)
this:
x = hd (stack s)

goal (2 subgoals):
 1. x = hd (stack s) \<Longrightarrow> \<phi> s' x < \<delta> s' y \<or> \<delta> s' y < \<phi> s' x \<and> y \<in> dom (finished s') \<and> \<phi> s' y < \<phi> s' x
 2. x \<noteq> hd (stack s) \<Longrightarrow> \<phi> s' x < \<delta> s' y \<or> \<delta> s' y < \<phi> s' x \<and> y \<in> dom (finished s') \<and> \<phi> s' y < \<phi> s' x
[PROOF STEP]
hence \<phi>x: "\<phi> s' x = counter s"
[PROOF STATE]
proof (prove)
using this:
x = hd (stack s)

goal (1 subgoal):
 1. \<phi> s' x = counter s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<phi> s' x = counter s

goal (2 subgoals):
 1. x = hd (stack s) \<Longrightarrow> \<phi> s' x < \<delta> s' y \<or> \<delta> s' y < \<phi> s' x \<and> y \<in> dom (finished s') \<and> \<phi> s' y < \<phi> s' x
 2. x \<noteq> hd (stack s) \<Longrightarrow> \<phi> s' x < \<delta> s' y \<or> \<delta> s' y < \<phi> s' x \<and> y \<in> dom (finished s') \<and> \<phi> s' y < \<phi> s' x
[PROOF STEP]
from x_is_hd neq
[PROOF STATE]
proof (chain)
picking this:
x = hd (stack s)
x \<noteq> y
[PROOF STEP]
have y_not_hd: "y \<noteq> hd (stack s)"
[PROOF STATE]
proof (prove)
using this:
x = hd (stack s)
x \<noteq> y

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

goal (2 subgoals):
 1. x = hd (stack s) \<Longrightarrow> \<phi> s' x < \<delta> s' y \<or> \<delta> s' y < \<phi> s' x \<and> y \<in> dom (finished s') \<and> \<phi> s' y < \<phi> s' x
 2. x \<noteq> hd (stack s) \<Longrightarrow> \<phi> s' x < \<delta> s' y \<or> \<delta> s' y < \<phi> s' x \<and> y \<in> dom (finished s') \<and> \<phi> s' y < \<phi> s' x
[PROOF STEP]
have "\<delta> s y < \<phi> s' x \<and> y \<in> dom (finished s) \<and> \<phi> s y < \<phi> s' x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<delta> s y < \<phi> s' x \<and> y \<in> dom (finished s) \<and> \<phi> s y < \<phi> s' x
[PROOF STEP]
proof (cases "y \<in> set (stack s)")
          \<comment> \<open>y on stack is not possible: According to @{thm [display] \<delta>} it is discovered after @{text "x (= hd (stack s))"}\<close>
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. y \<in> set (stack s) \<Longrightarrow> \<delta> s y < \<phi> s' x \<and> y \<in> dom (finished s) \<and> \<phi> s y < \<phi> s' x
 2. y \<notin> set (stack s) \<Longrightarrow> \<delta> s y < \<phi> s' x \<and> y \<in> dom (finished s) \<and> \<phi> s y < \<phi> s' x
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
y \<in> set (stack s)

goal (2 subgoals):
 1. y \<in> set (stack s) \<Longrightarrow> \<delta> s y < \<phi> s' x \<and> y \<in> dom (finished s) \<and> \<phi> s y < \<phi> s' x
 2. y \<notin> set (stack s) \<Longrightarrow> \<delta> s y < \<phi> s' x \<and> y \<in> dom (finished s) \<and> \<phi> s y < \<phi> s' x
[PROOF STEP]
with y_not_hd
[PROOF STATE]
proof (chain)
picking this:
y \<noteq> hd (stack s)
y \<in> set (stack s)
[PROOF STEP]
have "y \<in> set (tl (stack s))"
[PROOF STATE]
proof (prove)
using this:
y \<noteq> hd (stack s)
y \<in> set (stack s)

goal (1 subgoal):
 1. y \<in> set (tl (stack s))
[PROOF STEP]
by (cases "stack s") simp_all
[PROOF STATE]
proof (state)
this:
y \<in> set (tl (stack s))

goal (2 subgoals):
 1. y \<in> set (stack s) \<Longrightarrow> \<delta> s y < \<phi> s' x \<and> y \<in> dom (finished s) \<and> \<phi> s y < \<phi> s' x
 2. y \<notin> set (stack s) \<Longrightarrow> \<delta> s y < \<phi> s' x \<and> y \<in> dom (finished s) \<and> \<phi> s y < \<phi> s' x
[PROOF STEP]
with tl_lt_stack_hd_discover[OF NE] \<delta> x_is_hd
[PROOF STATE]
proof (chain)
picking this:
?x \<in> set (tl (stack s)) \<Longrightarrow> \<delta> s ?x < \<delta> s (hd (stack s))
\<delta> s' x < \<delta> s' y
x = hd (stack s)
y \<in> set (tl (stack s))
[PROOF STEP]
have "\<delta> s y < \<delta> s x"
[PROOF STATE]
proof (prove)
using this:
?x \<in> set (tl (stack s)) \<Longrightarrow> \<delta> s ?x < \<delta> s (hd (stack s))
\<delta> s' x < \<delta> s' y
x = hd (stack s)
y \<in> set (tl (stack s))

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

goal (2 subgoals):
 1. y \<in> set (stack s) \<Longrightarrow> \<delta> s y < \<phi> s' x \<and> y \<in> dom (finished s) \<and> \<phi> s y < \<phi> s' x
 2. y \<notin> set (stack s) \<Longrightarrow> \<delta> s y < \<phi> s' x \<and> y \<in> dom (finished s) \<and> \<phi> s y < \<phi> s' x
[PROOF STEP]
with \<delta>
[PROOF STATE]
proof (chain)
picking this:
\<delta> s' x < \<delta> s' y
\<delta> s y < \<delta> s x
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
\<delta> s' x < \<delta> s' y
\<delta> s y < \<delta> s x

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

goal (2 subgoals):
 1. y \<in> set (stack s) \<Longrightarrow> \<delta> s y < \<phi> s' x \<and> y \<in> dom (finished s) \<and> \<phi> s y < \<phi> s' x
 2. y \<notin> set (stack s) \<Longrightarrow> \<delta> s y < \<phi> s' x \<and> y \<in> dom (finished s) \<and> \<phi> s y < \<phi> s' x
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. \<delta> s y < \<phi> s' x \<and> y \<in> dom (finished s) \<and> \<phi> s y < \<phi> s' x
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<delta> s y < \<phi> s' x \<and> y \<in> dom (finished s) \<and> \<phi> s y < \<phi> s' x

goal (1 subgoal):
 1. y \<notin> set (stack s) \<Longrightarrow> \<delta> s y < \<phi> s' x \<and> y \<in> dom (finished s) \<and> \<phi> s y < \<phi> s' x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. y \<notin> set (stack s) \<Longrightarrow> \<delta> s y < \<phi> s' x \<and> y \<in> dom (finished s) \<and> \<phi> s y < \<phi> s' x
[PROOF STEP]
case False \<comment> \<open>y must be a successor of @{text "x (= (hd (stack s)))"}\<close>
[PROOF STATE]
proof (state)
this:
y \<notin> set (stack s)

goal (1 subgoal):
 1. y \<notin> set (stack s) \<Longrightarrow> \<delta> s y < \<phi> s' x \<and> y \<in> dom (finished s) \<and> \<phi> s y < \<phi> s' x
[PROOF STEP]
from dom
[PROOF STATE]
proof (chain)
picking this:
x \<in> dom (discovered s')
y \<in> dom (discovered s')
[PROOF STEP]
have "y \<in> dom (discovered s)"
[PROOF STATE]
proof (prove)
using this:
x \<in> dom (discovered s')
y \<in> dom (discovered s')

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

goal (1 subgoal):
 1. y \<notin> set (stack s) \<Longrightarrow> \<delta> s y < \<phi> s' x \<and> y \<in> dom (finished s) \<and> \<phi> s y < \<phi> s' x
[PROOF STEP]
with False discovered_not_stack_imp_finished
[PROOF STATE]
proof (chain)
picking this:
y \<notin> set (stack s)
\<lbrakk>?x \<in> dom (discovered s); ?x \<notin> set (stack s)\<rbrakk> \<Longrightarrow> ?x \<in> dom (finished s)
y \<in> dom (discovered s)
[PROOF STEP]
have *:
            "y \<in> dom (finished s)"
[PROOF STATE]
proof (prove)
using this:
y \<notin> set (stack s)
\<lbrakk>?x \<in> dom (discovered s); ?x \<notin> set (stack s)\<rbrakk> \<Longrightarrow> ?x \<in> dom (finished s)
y \<in> dom (discovered s)

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

goal (1 subgoal):
 1. y \<notin> set (stack s) \<Longrightarrow> \<delta> s y < \<phi> s' x \<and> y \<in> dom (finished s) \<and> \<phi> s y < \<phi> s' x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
y \<in> dom (finished s)

goal (1 subgoal):
 1. y \<notin> set (stack s) \<Longrightarrow> \<delta> s y < \<phi> s' x \<and> y \<in> dom (finished s) \<and> \<phi> s y < \<phi> s' x
[PROOF STEP]
with timing_less_counter \<phi>x
[PROOF STATE]
proof (chain)
picking this:
?v \<in> dom (discovered s) \<Longrightarrow> \<delta> s ?v < counter s
?v \<in> dom (finished s) \<Longrightarrow> \<phi> s ?v < counter s
\<phi> s' x = counter s
y \<in> dom (finished s)
[PROOF STEP]
have "\<phi> s y < \<phi> s' x"
[PROOF STATE]
proof (prove)
using this:
?v \<in> dom (discovered s) \<Longrightarrow> \<delta> s ?v < counter s
?v \<in> dom (finished s) \<Longrightarrow> \<phi> s ?v < counter s
\<phi> s' x = counter s
y \<in> dom (finished s)

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

goal (1 subgoal):
 1. y \<notin> set (stack s) \<Longrightarrow> \<delta> s y < \<phi> s' x \<and> y \<in> dom (finished s) \<and> \<phi> s y < \<phi> s' x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<phi> s y < \<phi> s' x

goal (1 subgoal):
 1. y \<notin> set (stack s) \<Longrightarrow> \<delta> s y < \<phi> s' x \<and> y \<in> dom (finished s) \<and> \<phi> s y < \<phi> s' x
[PROOF STEP]
with * disc_lt_fin \<phi>x
[PROOF STATE]
proof (chain)
picking this:
y \<in> dom (finished s)
?v \<in> dom (finished s) \<Longrightarrow> \<delta> s ?v < \<phi> s ?v
\<phi> s' x = counter s
\<phi> s y < \<phi> s' x
[PROOF STEP]
have "\<delta> s y < \<phi> s' x"
[PROOF STATE]
proof (prove)
using this:
y \<in> dom (finished s)
?v \<in> dom (finished s) \<Longrightarrow> \<delta> s ?v < \<phi> s ?v
\<phi> s' x = counter s
\<phi> s y < \<phi> s' x

goal (1 subgoal):
 1. \<delta> s y < \<phi> s' x
[PROOF STEP]
by (metis less_trans)
[PROOF STATE]
proof (state)
this:
\<delta> s y < \<phi> s' x

goal (1 subgoal):
 1. y \<notin> set (stack s) \<Longrightarrow> \<delta> s y < \<phi> s' x \<and> y \<in> dom (finished s) \<and> \<phi> s y < \<phi> s' x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
y \<in> dom (finished s)
\<phi> s y < \<phi> s' x
\<delta> s y < \<phi> s' x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
y \<in> dom (finished s)
\<phi> s y < \<phi> s' x
\<delta> s y < \<phi> s' x

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<delta> s y < \<phi> s' x \<and> y \<in> dom (finished s) \<and> \<phi> s y < \<phi> s' x

goal (2 subgoals):
 1. x = hd (stack s) \<Longrightarrow> \<phi> s' x < \<delta> s' y \<or> \<delta> s' y < \<phi> s' x \<and> y \<in> dom (finished s') \<and> \<phi> s' y < \<phi> s' x
 2. x \<noteq> hd (stack s) \<Longrightarrow> \<phi> s' x < \<delta> s' y \<or> \<delta> s' y < \<phi> s' x \<and> y \<in> dom (finished s') \<and> \<phi> s' y < \<phi> s' x
[PROOF STEP]
with y_not_hd
[PROOF STATE]
proof (chain)
picking this:
y \<noteq> hd (stack s)
\<delta> s y < \<phi> s' x \<and> y \<in> dom (finished s) \<and> \<phi> s y < \<phi> s' x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
y \<noteq> hd (stack s)
\<delta> s y < \<phi> s' x \<and> y \<in> dom (finished s) \<and> \<phi> s y < \<phi> s' x

goal (1 subgoal):
 1. \<phi> s' x < \<delta> s' y \<or> \<delta> s' y < \<phi> s' x \<and> y \<in> dom (finished s') \<and> \<phi> s' y < \<phi> s' x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<phi> s' x < \<delta> s' y \<or> \<delta> s' y < \<phi> s' x \<and> y \<in> dom (finished s') \<and> \<phi> s' y < \<phi> s' x

goal (1 subgoal):
 1. x \<noteq> hd (stack s) \<Longrightarrow> \<phi> s' x < \<delta> s' y \<or> \<delta> s' y < \<phi> s' x \<and> y \<in> dom (finished s') \<and> \<phi> s' y < \<phi> s' x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<noteq> hd (stack s) \<Longrightarrow> \<phi> s' x < \<delta> s' y \<or> \<delta> s' y < \<phi> s' x \<and> y \<in> dom (finished s') \<and> \<phi> s' y < \<phi> s' x
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
x \<noteq> hd (stack s)

goal (1 subgoal):
 1. x \<noteq> hd (stack s) \<Longrightarrow> \<phi> s' x < \<delta> s' y \<or> \<delta> s' y < \<phi> s' x \<and> y \<in> dom (finished s') \<and> \<phi> s' y < \<phi> s' x
[PROOF STEP]
note [simp] = this
[PROOF STATE]
proof (state)
this:
x \<noteq> hd (stack s)

goal (1 subgoal):
 1. x \<noteq> hd (stack s) \<Longrightarrow> \<phi> s' x < \<delta> s' y \<or> \<delta> s' y < \<phi> s' x \<and> y \<in> dom (finished s') \<and> \<phi> s' y < \<phi> s' x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> s' x < \<delta> s' y \<or> \<delta> s' y < \<phi> s' x \<and> y \<in> dom (finished s') \<and> \<phi> s' y < \<phi> s' x
[PROOF STEP]
proof (cases "y = hd (stack s)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. y = hd (stack s) \<Longrightarrow> \<phi> s' x < \<delta> s' y \<or> \<delta> s' y < \<phi> s' x \<and> y \<in> dom (finished s') \<and> \<phi> s' y < \<phi> s' x
 2. y \<noteq> hd (stack s) \<Longrightarrow> \<phi> s' x < \<delta> s' y \<or> \<delta> s' y < \<phi> s' x \<and> y \<in> dom (finished s') \<and> \<phi> s' y < \<phi> s' x
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
y \<noteq> hd (stack s)

goal (2 subgoals):
 1. y = hd (stack s) \<Longrightarrow> \<phi> s' x < \<delta> s' y \<or> \<delta> s' y < \<phi> s' x \<and> y \<in> dom (finished s') \<and> \<phi> s' y < \<phi> s' x
 2. y \<noteq> hd (stack s) \<Longrightarrow> \<phi> s' x < \<delta> s' y \<or> \<delta> s' y < \<phi> s' x \<and> y \<in> dom (finished s') \<and> \<phi> s' y < \<phi> s' x
[PROOF STEP]
with finish assms
[PROOF STATE]
proof (chain)
picking this:
parenthesis 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>
x \<in> dom (discovered s')
y \<in> dom (discovered s')
\<delta> s' x < \<delta> s' y
x \<in> dom (finished s')
discovered s' = discovered s
counter s' = Suc (counter s)
finished s' = finished s(hd (stack s) \<mapsto> counter s)
y \<noteq> hd (stack s)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
parenthesis 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>
x \<in> dom (discovered s')
y \<in> dom (discovered s')
\<delta> s' x < \<delta> s' y
x \<in> dom (finished s')
discovered s' = discovered s
counter s' = Suc (counter s)
finished s' = finished s(hd (stack s) \<mapsto> counter s)
y \<noteq> hd (stack s)

goal (1 subgoal):
 1. \<phi> s' x < \<delta> s' y \<or> \<delta> s' y < \<phi> s' x \<and> y \<in> dom (finished s') \<and> \<phi> s' y < \<phi> s' x
[PROOF STEP]
by (simp add: parenthesis_def)
[PROOF STATE]
proof (state)
this:
\<phi> s' x < \<delta> s' y \<or> \<delta> s' y < \<phi> s' x \<and> y \<in> dom (finished s') \<and> \<phi> s' y < \<phi> s' x

goal (1 subgoal):
 1. y = hd (stack s) \<Longrightarrow> \<phi> s' x < \<delta> s' y \<or> \<delta> s' y < \<phi> s' x \<and> y \<in> dom (finished s') \<and> \<phi> s' y < \<phi> s' x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. y = hd (stack s) \<Longrightarrow> \<phi> s' x < \<delta> s' y \<or> \<delta> s' y < \<phi> s' x \<and> y \<in> dom (finished s') \<and> \<phi> s' y < \<phi> s' x
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
y = hd (stack s)

goal (1 subgoal):
 1. y = hd (stack s) \<Longrightarrow> \<phi> s' x < \<delta> s' y \<or> \<delta> s' y < \<phi> s' x \<and> y \<in> dom (finished s') \<and> \<phi> s' y < \<phi> s' x
[PROOF STEP]
with stack_not_finished
[PROOF STATE]
proof (chain)
picking this:
?x \<in> set (stack s) \<Longrightarrow> ?x \<notin> dom (finished s)
y = hd (stack s)
[PROOF STEP]
have "y \<notin> dom (finished s)"
[PROOF STATE]
proof (prove)
using this:
?x \<in> set (stack s) \<Longrightarrow> ?x \<notin> dom (finished s)
y = hd (stack s)

goal (1 subgoal):
 1. y \<notin> dom (finished s)
[PROOF STEP]
using hd_in_set[OF NE]
[PROOF STATE]
proof (prove)
using this:
?x \<in> set (stack s) \<Longrightarrow> ?x \<notin> dom (finished s)
y = hd (stack s)
hd (stack s) \<in> set (stack s)

goal (1 subgoal):
 1. y \<notin> dom (finished s)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<notin> dom (finished s)

goal (1 subgoal):
 1. y = hd (stack s) \<Longrightarrow> \<phi> s' x < \<delta> s' y \<or> \<delta> s' y < \<phi> s' x \<and> y \<in> dom (finished s') \<and> \<phi> s' y < \<phi> s' x
[PROOF STEP]
with finish assms
[PROOF STATE]
proof (chain)
picking this:
parenthesis 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>
x \<in> dom (discovered s')
y \<in> dom (discovered s')
\<delta> s' x < \<delta> s' y
x \<in> dom (finished s')
discovered s' = discovered s
counter s' = Suc (counter s)
finished s' = finished s(hd (stack s) \<mapsto> counter s)
y \<notin> dom (finished s)
[PROOF STEP]
have "\<phi> s x < \<delta> s y"
[PROOF STATE]
proof (prove)
using this:
parenthesis 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>
x \<in> dom (discovered s')
y \<in> dom (discovered s')
\<delta> s' x < \<delta> s' y
x \<in> dom (finished s')
discovered s' = discovered s
counter s' = Suc (counter s)
finished s' = finished s(hd (stack s) \<mapsto> counter s)
y \<notin> dom (finished s)

goal (1 subgoal):
 1. \<phi> s x < \<delta> s y
[PROOF STEP]
unfolding parenthesis_def
[PROOF STATE]
proof (prove)
using this:
\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). \<delta> s v < \<delta> s w \<and> v \<in> dom (finished s) \<longrightarrow> \<phi> s v < \<delta> s w \<or> \<delta> s w < \<phi> s v \<and> w \<in> dom (finished s) \<and> \<phi> s w < \<phi> s v
cond s
DFS_invar G param s
DFS_invar G param s'
stack s \<noteq> []
pending s `` {u_} = {}
u_ = hd (stack s)
s' = finish u_ s\<lparr>state.more := e_\<rparr>
x \<in> dom (discovered s')
y \<in> dom (discovered s')
\<delta> s' x < \<delta> s' y
x \<in> dom (finished s')
discovered s' = discovered s
counter s' = Suc (counter s)
finished s' = finished s(hd (stack s) \<mapsto> counter s)
y \<notin> dom (finished s)

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

goal (1 subgoal):
 1. y = hd (stack s) \<Longrightarrow> \<phi> s' x < \<delta> s' y \<or> \<delta> s' y < \<phi> s' x \<and> y \<in> dom (finished s') \<and> \<phi> s' y < \<phi> s' x
[PROOF STEP]
hence ?DISJ
[PROOF STATE]
proof (prove)
using this:
\<phi> s x < \<delta> s y

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

goal (1 subgoal):
 1. y = hd (stack s) \<Longrightarrow> \<phi> s' x < \<delta> s' y \<or> \<delta> s' y < \<phi> s' x \<and> y \<in> dom (finished s') \<and> \<phi> s' y < \<phi> s' x
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<phi> s' x < \<delta> s' y

goal (1 subgoal):
 1. \<phi> s' x < \<delta> s' y \<or> \<delta> s' y < \<phi> s' x \<and> y \<in> dom (finished s') \<and> \<phi> s' y < \<phi> s' x
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<phi> s' x < \<delta> s' y \<or> \<delta> s' y < \<phi> s' x \<and> y \<in> dom (finished s') \<and> \<phi> s' y < \<phi> s' x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<phi> s' x < \<delta> s' y \<or> \<delta> s' y < \<phi> s' x \<and> y \<in> dom (finished s') \<and> \<phi> s' y < \<phi> s' x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<phi> s' x < \<delta> s' y \<or> \<delta> s' y < \<phi> s' x \<and> y \<in> dom (finished s') \<and> \<phi> s' y < \<phi> s' x

goal (5 subgoals):
 1. \<And>e. parenthesis (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>parenthesis 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> parenthesis s'
 3. \<And>s s' u e. \<lbrakk>parenthesis 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> parenthesis s'
 4. \<And>s s' u v e c b. \<lbrakk>parenthesis 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> parenthesis s'
 5. \<And>s s' u v e. \<lbrakk>parenthesis 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> parenthesis s'
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x7 \<in> dom (discovered s'); ?y7 \<in> dom (discovered s'); \<delta> s' ?x7 < \<delta> s' ?y7; ?x7 \<in> dom (finished s')\<rbrakk> \<Longrightarrow> \<phi> s' ?x7 < \<delta> s' ?y7 \<or> \<delta> s' ?y7 < \<phi> s' ?x7 \<and> ?y7 \<in> dom (finished s') \<and> \<phi> s' ?y7 < \<phi> s' ?x7

goal (5 subgoals):
 1. \<And>e. parenthesis (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>parenthesis 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> parenthesis s'
 3. \<And>s s' u e. \<lbrakk>parenthesis 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> parenthesis s'
 4. \<And>s s' u v e c b. \<lbrakk>parenthesis 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> parenthesis s'
 5. \<And>s s' u v e. \<lbrakk>parenthesis 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> parenthesis s'
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x7 \<in> dom (discovered s'); ?y7 \<in> dom (discovered s'); \<delta> s' ?x7 < \<delta> s' ?y7; ?x7 \<in> dom (finished s')\<rbrakk> \<Longrightarrow> \<phi> s' ?x7 < \<delta> s' ?y7 \<or> \<delta> s' ?y7 < \<phi> s' ?x7 \<and> ?y7 \<in> dom (finished s') \<and> \<phi> s' ?y7 < \<phi> s' ?x7

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

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

goal (4 subgoals):
 1. \<And>e. parenthesis (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>parenthesis 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> parenthesis s'
 3. \<And>s s' u v e c b. \<lbrakk>parenthesis 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> parenthesis s'
 4. \<And>s s' u v e. \<lbrakk>parenthesis 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> parenthesis s'
[PROOF STEP]
hence EQ[simp]: "discovered s' = (discovered s)(v \<mapsto> counter s)"
                    "finished s' = finished s"
                    "counter s' = Suc (counter s)"
[PROOF STATE]
proof (prove)
using this:
parenthesis 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. discovered s' = discovered s(v \<mapsto> counter s) &&& finished s' = finished s &&& counter s' = Suc (counter s)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
discovered s' = discovered s(v \<mapsto> counter s)
finished s' = finished s
counter s' = Suc (counter s)

goal (4 subgoals):
 1. \<And>e. parenthesis (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>parenthesis 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> parenthesis s'
 3. \<And>s s' u v e c b. \<lbrakk>parenthesis 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> parenthesis s'
 4. \<And>s s' u v e. \<lbrakk>parenthesis 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> parenthesis s'
[PROOF STEP]
from discover
[PROOF STATE]
proof (chain)
picking this:
parenthesis 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:
parenthesis s
cond s
DFS_invar G param s
DFS_invar G param s'
stack s \<noteq> []
v \<in> pending s `` {u}
v \<notin> dom (discovered s)
u = hd (stack s)
s' = discover u v (s\<lparr>pending := pending s - {(u, v)}\<rparr>)\<lparr>state.more := e_\<rparr>

goal (1 subgoal):
 1. DFS_invar G param s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>e. parenthesis (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>parenthesis 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> parenthesis s'
 3. \<And>s s' u v e c b. \<lbrakk>parenthesis 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> parenthesis s'
 4. \<And>s s' u v e. \<lbrakk>parenthesis 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> parenthesis s'
[PROOF STEP]
from discover finished_discovered
[PROOF STATE]
proof (chain)
picking this:
parenthesis 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>
dom (finished s) \<subseteq> dom (discovered s)
[PROOF STEP]
have
      V': "v \<notin> dom (discovered s)" "v \<notin> dom (finished s)"
[PROOF STATE]
proof (prove)
using this:
parenthesis 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>
dom (finished s) \<subseteq> dom (discovered s)

goal (1 subgoal):
 1. v \<notin> dom (discovered s) &&& v \<notin> dom (finished s)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v \<notin> dom (discovered s)
v \<notin> dom (finished s)

goal (4 subgoals):
 1. \<And>e. parenthesis (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>parenthesis 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> parenthesis s'
 3. \<And>s s' u v e c b. \<lbrakk>parenthesis 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> parenthesis s'
 4. \<And>s s' u v e. \<lbrakk>parenthesis 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> parenthesis s'
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
v \<notin> dom (discovered s)
v \<notin> dom (finished s)

goal (4 subgoals):
 1. \<And>e. parenthesis (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>parenthesis 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> parenthesis s'
 3. \<And>s s' u v e c b. \<lbrakk>parenthesis 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> parenthesis s'
 4. \<And>s s' u v e. \<lbrakk>parenthesis 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> parenthesis s'
[PROOF STEP]
fix x y
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>e. parenthesis (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>parenthesis 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> parenthesis s'
 3. \<And>s s' u v e c b. \<lbrakk>parenthesis 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> parenthesis s'
 4. \<And>s s' u v e. \<lbrakk>parenthesis 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> parenthesis s'
[PROOF STEP]
assume  dom: "x \<in> dom (discovered s')" "y \<in> dom (discovered s')"
        and \<delta>: "\<delta> s' x < \<delta> s' y"
        and f: "x \<in> dom (finished s')"
[PROOF STATE]
proof (state)
this:
x \<in> dom (discovered s')
y \<in> dom (discovered s')
\<delta> s' x < \<delta> s' y
x \<in> dom (finished s')

goal (4 subgoals):
 1. \<And>e. parenthesis (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>parenthesis 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> parenthesis s'
 3. \<And>s s' u v e c b. \<lbrakk>parenthesis 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> parenthesis s'
 4. \<And>s s' u v e. \<lbrakk>parenthesis 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> parenthesis s'
[PROOF STEP]
let ?DISJ = "\<phi> s' x < \<delta> s' y"
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>e. parenthesis (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>parenthesis 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> parenthesis s'
 3. \<And>s s' u v e c b. \<lbrakk>parenthesis 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> parenthesis s'
 4. \<And>s s' u v e. \<lbrakk>parenthesis 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> parenthesis s'
[PROOF STEP]
let ?IN = "\<delta> s' y < \<phi> s' x \<and> y \<in> dom (finished s') \<and> \<phi> s' y < \<phi> s' x"
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>e. parenthesis (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>parenthesis 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> parenthesis s'
 3. \<And>s s' u v e c b. \<lbrakk>parenthesis 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> parenthesis s'
 4. \<And>s s' u v e. \<lbrakk>parenthesis 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> parenthesis s'
[PROOF STEP]
from dom V' f
[PROOF STATE]
proof (chain)
picking this:
x \<in> dom (discovered s')
y \<in> dom (discovered s')
v \<notin> dom (discovered s)
v \<notin> dom (finished s)
x \<in> dom (finished s')
[PROOF STEP]
have x: "x \<in> dom (discovered s)""x \<noteq> v"
[PROOF STATE]
proof (prove)
using this:
x \<in> dom (discovered s')
y \<in> dom (discovered s')
v \<notin> dom (discovered s)
v \<notin> dom (finished s)
x \<in> dom (finished s')

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

goal (4 subgoals):
 1. \<And>e. parenthesis (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>parenthesis 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> parenthesis s'
 3. \<And>s s' u v e c b. \<lbrakk>parenthesis 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> parenthesis s'
 4. \<And>s s' u v e. \<lbrakk>parenthesis 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> parenthesis s'
[PROOF STEP]
have "?DISJ \<or> ?IN"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> s' x < \<delta> s' y \<or> \<delta> s' y < \<phi> s' x \<and> y \<in> dom (finished s') \<and> \<phi> s' y < \<phi> s' x
[PROOF STEP]
proof (cases "y = v")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. y = v \<Longrightarrow> \<phi> s' x < \<delta> s' y \<or> \<delta> s' y < \<phi> s' x \<and> y \<in> dom (finished s') \<and> \<phi> s' y < \<phi> s' x
 2. y \<noteq> v \<Longrightarrow> \<phi> s' x < \<delta> s' y \<or> \<delta> s' y < \<phi> s' x \<and> y \<in> dom (finished s') \<and> \<phi> s' y < \<phi> s' x
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
y = v

goal (2 subgoals):
 1. y = v \<Longrightarrow> \<phi> s' x < \<delta> s' y \<or> \<delta> s' y < \<phi> s' x \<and> y \<in> dom (finished s') \<and> \<phi> s' y < \<phi> s' x
 2. y \<noteq> v \<Longrightarrow> \<phi> s' x < \<delta> s' y \<or> \<delta> s' y < \<phi> s' x \<and> y \<in> dom (finished s') \<and> \<phi> s' y < \<phi> s' x
[PROOF STEP]
hence "\<delta> s' y = counter s"
[PROOF STATE]
proof (prove)
using this:
y = v

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

goal (2 subgoals):
 1. y = v \<Longrightarrow> \<phi> s' x < \<delta> s' y \<or> \<delta> s' y < \<phi> s' x \<and> y \<in> dom (finished s') \<and> \<phi> s' y < \<phi> s' x
 2. y \<noteq> v \<Longrightarrow> \<phi> s' x < \<delta> s' y \<or> \<delta> s' y < \<phi> s' x \<and> y \<in> dom (finished s') \<and> \<phi> s' y < \<phi> s' x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<delta> s' y = counter s

goal (2 subgoals):
 1. y = v \<Longrightarrow> \<phi> s' x < \<delta> s' y \<or> \<delta> s' y < \<phi> s' x \<and> y \<in> dom (finished s') \<and> \<phi> s' y < \<phi> s' x
 2. y \<noteq> v \<Longrightarrow> \<phi> s' x < \<delta> s' y \<or> \<delta> s' y < \<phi> s' x \<and> y \<in> dom (finished s') \<and> \<phi> s' y < \<phi> s' x
[PROOF STEP]
from timing_less_counter x f
[PROOF STATE]
proof (chain)
picking this:
?v \<in> dom (discovered s) \<Longrightarrow> \<delta> s ?v < counter s
?v \<in> dom (finished s) \<Longrightarrow> \<phi> s ?v < counter s
x \<in> dom (discovered s)
x \<noteq> v
x \<in> dom (finished s')
[PROOF STEP]
have "\<phi> s' x < counter s"
[PROOF STATE]
proof (prove)
using this:
?v \<in> dom (discovered s) \<Longrightarrow> \<delta> s ?v < counter s
?v \<in> dom (finished s) \<Longrightarrow> \<phi> s ?v < counter s
x \<in> dom (discovered s)
x \<noteq> v
x \<in> dom (finished s')

goal (1 subgoal):
 1. \<phi> s' x < counter s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<phi> s' x < counter s

goal (2 subgoals):
 1. y = v \<Longrightarrow> \<phi> s' x < \<delta> s' y \<or> \<delta> s' y < \<phi> s' x \<and> y \<in> dom (finished s') \<and> \<phi> s' y < \<phi> s' x
 2. y \<noteq> v \<Longrightarrow> \<phi> s' x < \<delta> s' y \<or> \<delta> s' y < \<phi> s' x \<and> y \<in> dom (finished s') \<and> \<phi> s' y < \<phi> s' x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<delta> s' y = counter s
\<phi> s' x < counter s
[PROOF STEP]
have "?DISJ"
[PROOF STATE]
proof (prove)
using this:
\<delta> s' y = counter s
\<phi> s' x < counter s

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

goal (2 subgoals):
 1. y = v \<Longrightarrow> \<phi> s' x < \<delta> s' y \<or> \<delta> s' y < \<phi> s' x \<and> y \<in> dom (finished s') \<and> \<phi> s' y < \<phi> s' x
 2. y \<noteq> v \<Longrightarrow> \<phi> s' x < \<delta> s' y \<or> \<delta> s' y < \<phi> s' x \<and> y \<in> dom (finished s') \<and> \<phi> s' y < \<phi> s' x
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<phi> s' x < \<delta> s' y

goal (1 subgoal):
 1. \<phi> s' x < \<delta> s' y \<or> \<delta> s' y < \<phi> s' x \<and> y \<in> dom (finished s') \<and> \<phi> s' y < \<phi> s' x
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<phi> s' x < \<delta> s' y \<or> \<delta> s' y < \<phi> s' x \<and> y \<in> dom (finished s') \<and> \<phi> s' y < \<phi> s' x

goal (1 subgoal):
 1. y \<noteq> v \<Longrightarrow> \<phi> s' x < \<delta> s' y \<or> \<delta> s' y < \<phi> s' x \<and> y \<in> dom (finished s') \<and> \<phi> s' y < \<phi> s' x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. y \<noteq> v \<Longrightarrow> \<phi> s' x < \<delta> s' y \<or> \<delta> s' y < \<phi> s' x \<and> y \<in> dom (finished s') \<and> \<phi> s' y < \<phi> s' x
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
y \<noteq> v

goal (1 subgoal):
 1. y \<noteq> v \<Longrightarrow> \<phi> s' x < \<delta> s' y \<or> \<delta> s' y < \<phi> s' x \<and> y \<in> dom (finished s') \<and> \<phi> s' y < \<phi> s' x
[PROOF STEP]
with dom
[PROOF STATE]
proof (chain)
picking this:
x \<in> dom (discovered s')
y \<in> dom (discovered s')
y \<noteq> v
[PROOF STEP]
have "y \<in> dom (discovered s)"
[PROOF STATE]
proof (prove)
using this:
x \<in> dom (discovered s')
y \<in> dom (discovered s')
y \<noteq> v

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

goal (1 subgoal):
 1. y \<noteq> v \<Longrightarrow> \<phi> s' x < \<delta> s' y \<or> \<delta> s' y < \<phi> s' x \<and> y \<in> dom (finished s') \<and> \<phi> s' y < \<phi> s' x
[PROOF STEP]
with discover False \<delta> f x
[PROOF STATE]
proof (chain)
picking this:
parenthesis 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>
y \<noteq> v
\<delta> s' x < \<delta> s' y
x \<in> dom (finished s')
x \<in> dom (discovered s)
x \<noteq> v
y \<in> dom (discovered s)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
parenthesis 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>
y \<noteq> v
\<delta> s' x < \<delta> s' y
x \<in> dom (finished s')
x \<in> dom (discovered s)
x \<noteq> v
y \<in> dom (discovered s)

goal (1 subgoal):
 1. \<phi> s' x < \<delta> s' y \<or> \<delta> s' y < \<phi> s' x \<and> y \<in> dom (finished s') \<and> \<phi> s' y < \<phi> s' x
[PROOF STEP]
by (simp add: parenthesis_def)
[PROOF STATE]
proof (state)
this:
\<phi> s' x < \<delta> s' y \<or> \<delta> s' y < \<phi> s' x \<and> y \<in> dom (finished s') \<and> \<phi> s' y < \<phi> s' x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<phi> s' x < \<delta> s' y \<or> \<delta> s' y < \<phi> s' x \<and> y \<in> dom (finished s') \<and> \<phi> s' y < \<phi> s' x

goal (4 subgoals):
 1. \<And>e. parenthesis (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>parenthesis 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> parenthesis s'
 3. \<And>s s' u v e c b. \<lbrakk>parenthesis 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> parenthesis s'
 4. \<And>s s' u v e. \<lbrakk>parenthesis 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> parenthesis s'
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x7 \<in> dom (discovered s'); ?y7 \<in> dom (discovered s'); \<delta> s' ?x7 < \<delta> s' ?y7; ?x7 \<in> dom (finished s')\<rbrakk> \<Longrightarrow> \<phi> s' ?x7 < \<delta> s' ?y7 \<or> \<delta> s' ?y7 < \<phi> s' ?x7 \<and> ?y7 \<in> dom (finished s') \<and> \<phi> s' ?y7 < \<phi> s' ?x7

goal (4 subgoals):
 1. \<And>e. parenthesis (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>parenthesis 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> parenthesis s'
 3. \<And>s s' u v e c b. \<lbrakk>parenthesis 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> parenthesis s'
 4. \<And>s s' u v e. \<lbrakk>parenthesis 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> parenthesis s'
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x7 \<in> dom (discovered s'); ?y7 \<in> dom (discovered s'); \<delta> s' ?x7 < \<delta> s' ?y7; ?x7 \<in> dom (finished s')\<rbrakk> \<Longrightarrow> \<phi> s' ?x7 < \<delta> s' ?y7 \<or> \<delta> s' ?y7 < \<phi> s' ?x7 \<and> ?y7 \<in> dom (finished s') \<and> \<phi> s' ?y7 < \<phi> s' ?x7

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

goal (3 subgoals):
 1. \<And>e. parenthesis (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>parenthesis 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> parenthesis s'
 3. \<And>s s' u v e c b. \<lbrakk>parenthesis 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> parenthesis s'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>e. parenthesis (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>parenthesis 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> parenthesis s'
 3. \<And>s s' u v e c b. \<lbrakk>parenthesis 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> parenthesis s'
[PROOF STEP]
case (new_root s s' v0)
[PROOF STATE]
proof (state)
this:
parenthesis s
cond s
DFS_invar G param s
DFS_invar G param s'
stack s = []
v0 \<notin> dom (discovered s)
v0 \<in> V0
s' = new_root v0 s\<lparr>state.more := e_\<rparr>

goal (3 subgoals):
 1. \<And>e. parenthesis (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>parenthesis 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> parenthesis s'
 3. \<And>s s' u v e c b. \<lbrakk>parenthesis 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> parenthesis s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
parenthesis 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>
[PROOF STEP]
interpret DFS_invar where s=s
[PROOF STATE]
proof (prove)
using this:
parenthesis s
cond s
DFS_invar G param s
DFS_invar G param s'
stack s = []
v0 \<notin> dom (discovered s)
v0 \<in> V0
s' = new_root v0 s\<lparr>state.more := e_\<rparr>

goal (1 subgoal):
 1. DFS_invar G param s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>e. parenthesis (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>parenthesis 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> parenthesis s'
 3. \<And>s s' u v e c b. \<lbrakk>parenthesis 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> parenthesis s'
[PROOF STEP]
from finished_discovered new_root
[PROOF STATE]
proof (chain)
picking this:
dom (finished s) \<subseteq> dom (discovered s)
parenthesis 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>
[PROOF STEP]
have "v0 \<notin> dom (finished s')"
[PROOF STATE]
proof (prove)
using this:
dom (finished s) \<subseteq> dom (discovered s)
parenthesis s
cond s
DFS_invar G param s
DFS_invar G param s'
stack s = []
v0 \<notin> dom (discovered s)
v0 \<in> V0
s' = new_root v0 s\<lparr>state.more := e_\<rparr>

goal (1 subgoal):
 1. v0 \<notin> dom (finished s')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v0 \<notin> dom (finished s')

goal (3 subgoals):
 1. \<And>e. parenthesis (empty_state e)
 2. \<And>s s' v0 e. \<lbrakk>parenthesis 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> parenthesis s'
 3. \<And>s s' u v e c b. \<lbrakk>parenthesis 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> parenthesis s'
[PROOF STEP]
with new_root timing_less_counter
[PROOF STATE]
proof (chain)
picking this:
parenthesis 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>
?v \<in> dom (discovered s) \<Longrightarrow> \<delta> s ?v < counter s
?v \<in> dom (finished s) \<Longrightarrow> \<phi> s ?v < counter s
v0 \<notin> dom (finished s')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
parenthesis 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>
?v \<in> dom (discovered s) \<Longrightarrow> \<delta> s ?v < counter s
?v \<in> dom (finished s) \<Longrightarrow> \<phi> s ?v < counter s
v0 \<notin> dom (finished s')

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

goal (2 subgoals):
 1. \<And>e. parenthesis (empty_state e)
 2. \<And>s s' u v e c b. \<lbrakk>parenthesis 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> parenthesis s'
[PROOF STEP]
qed (simp_all add: parenthesis_def)


[STATEMENT]
lemma parenthesis:
    assumes "v \<in> dom (finished s)" "w \<in> dom (discovered s)"
    and "\<delta> s v < \<delta> s w"
    shows "\<phi> s v < \<delta> s w \<comment> \<open>disjoint\<close>
           \<or> (\<phi> s v > \<delta> s w \<and> w \<in> dom (finished s) \<and> \<phi> s w < \<phi> s v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> s v < \<delta> s w \<or> \<delta> s w < \<phi> s v \<and> w \<in> dom (finished s) \<and> \<phi> s w < \<phi> s v
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
v \<in> dom (finished s)
w \<in> dom (discovered s)
\<delta> s v < \<delta> s w

goal (1 subgoal):
 1. \<phi> s v < \<delta> s w \<or> \<delta> s w < \<phi> s v \<and> w \<in> dom (finished s) \<and> \<phi> s w < \<phi> s v
[PROOF STEP]
using i_parenthesis[THEN make_invar_thm]
[PROOF STATE]
proof (prove)
using this:
v \<in> dom (finished s)
w \<in> dom (discovered s)
\<delta> s v < \<delta> s w
parenthesis s

goal (1 subgoal):
 1. \<phi> s v < \<delta> s w \<or> \<delta> s w < \<phi> s v \<and> w \<in> dom (finished s) \<and> \<phi> s w < \<phi> s v
[PROOF STEP]
using finished_discovered
[PROOF STATE]
proof (prove)
using this:
v \<in> dom (finished s)
w \<in> dom (discovered s)
\<delta> s v < \<delta> s w
parenthesis s
dom (finished s) \<subseteq> dom (discovered s)

goal (1 subgoal):
 1. \<phi> s v < \<delta> s w \<or> \<delta> s w < \<phi> s v \<and> w \<in> dom (finished s) \<and> \<phi> s w < \<phi> s v
[PROOF STEP]
unfolding parenthesis_def
[PROOF STATE]
proof (prove)
using this:
v \<in> dom (finished s)
w \<in> dom (discovered s)
\<delta> s v < \<delta> s w
\<forall>v\<in>dom (discovered s). \<forall>w\<in>dom (discovered s). \<delta> s v < \<delta> s w \<and> v \<in> dom (finished s) \<longrightarrow> \<phi> s v < \<delta> s w \<or> \<delta> s w < \<phi> s v \<and> w \<in> dom (finished s) \<and> \<phi> s w < \<phi> s v
dom (finished s) \<subseteq> dom (discovered s)

goal (1 subgoal):
 1. \<phi> s v < \<delta> s w \<or> \<delta> s w < \<phi> s v \<and> w \<in> dom (finished s) \<and> \<phi> s w < \<phi> s v
[PROOF STEP]
by blast


[STATEMENT]
lemma parenthesis_contained:
    assumes "v \<in> dom (finished s)" "w \<in> dom (discovered s)"
    and "\<delta> s v < \<delta> s w" "\<phi> s v > \<delta> s w"
    shows "w \<in> dom (finished s) \<and> \<phi> s w < \<phi> s v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w \<in> dom (finished s) \<and> \<phi> s w < \<phi> s v
[PROOF STEP]
using parenthesis assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?v \<in> dom (finished s); ?w \<in> dom (discovered s); \<delta> s ?v < \<delta> s ?w\<rbrakk> \<Longrightarrow> \<phi> s ?v < \<delta> s ?w \<or> \<delta> s ?w < \<phi> s ?v \<and> ?w \<in> dom (finished s) \<and> \<phi> s ?w < \<phi> s ?v
v \<in> dom (finished s)
w \<in> dom (discovered s)
\<delta> s v < \<delta> s w
\<delta> s w < \<phi> s v

goal (1 subgoal):
 1. w \<in> dom (finished s) \<and> \<phi> s w < \<phi> s v
[PROOF STEP]
by force


[STATEMENT]
lemma parenthesis_disjoint:
    assumes "v \<in> dom (finished s)" "w \<in> dom (discovered s)"
    and "\<delta> s v < \<delta> s w" "\<phi> s w > \<phi> s v"
    shows "\<phi> s v < \<delta> s w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> s v < \<delta> s w
[PROOF STEP]
using parenthesis assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?v \<in> dom (finished s); ?w \<in> dom (discovered s); \<delta> s ?v < \<delta> s ?w\<rbrakk> \<Longrightarrow> \<phi> s ?v < \<delta> s ?w \<or> \<delta> s ?w < \<phi> s ?v \<and> ?w \<in> dom (finished s) \<and> \<phi> s ?w < \<phi> s ?v
v \<in> dom (finished s)
w \<in> dom (discovered s)
\<delta> s v < \<delta> s w
\<phi> s v < \<phi> s w

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


[STATEMENT]
lemma finished_succ_contained:
    assumes "v \<in> dom (finished s)"
    and "w \<in> succ v"
    and "\<delta> s v < \<delta> s w"
    shows "w \<in> dom (finished s) \<and> \<phi> s w < \<phi> s v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w \<in> dom (finished s) \<and> \<phi> s w < \<phi> s v
[PROOF STEP]
using finished_succ_fin finished_imp_succ_discovered parenthesis_contained
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?v \<in> dom (finished s); ?w \<in> E `` {?v}\<rbrakk> \<Longrightarrow> \<delta> s ?w < \<phi> s ?v
\<lbrakk>?v \<in> dom (finished s); ?w \<in> E `` {?v}\<rbrakk> \<Longrightarrow> ?w \<in> dom (discovered s)
\<lbrakk>?v \<in> dom (finished s); ?w \<in> dom (discovered s); \<delta> s ?v < \<delta> s ?w; \<delta> s ?w < \<phi> s ?v\<rbrakk> \<Longrightarrow> ?w \<in> dom (finished s) \<and> \<phi> s ?w < \<phi> s ?v

goal (1 subgoal):
 1. w \<in> dom (finished s) \<and> \<phi> s w < \<phi> s v
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?v \<in> dom (finished s); ?w \<in> E `` {?v}\<rbrakk> \<Longrightarrow> \<delta> s ?w < \<phi> s ?v
\<lbrakk>?v \<in> dom (finished s); ?w \<in> E `` {?v}\<rbrakk> \<Longrightarrow> ?w \<in> dom (discovered s)
\<lbrakk>?v \<in> dom (finished s); ?w \<in> dom (discovered s); \<delta> s ?v < \<delta> s ?w; \<delta> s ?w < \<phi> s ?v\<rbrakk> \<Longrightarrow> ?w \<in> dom (finished s) \<and> \<phi> s ?w < \<phi> s ?v
v \<in> dom (finished s)
w \<in> E `` {v}
\<delta> s v < \<delta> s w

goal (1 subgoal):
 1. w \<in> dom (finished s) \<and> \<phi> s w < \<phi> s v
[PROOF STEP]
by metis


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


[STATEMENT]
lemma edgesE_CB:
    assumes "x \<in> edges s"
    and "x \<in> tree_edges s \<Longrightarrow> P"
    and "x \<in> cross_edges s \<union> back_edges s \<Longrightarrow> P"
    shows "P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in> tree_edges s \<union> cross_edges s \<union> back_edges s
x \<in> tree_edges s \<Longrightarrow> P
x \<in> cross_edges s \<union> back_edges s \<Longrightarrow> P

goal (1 subgoal):
 1. P
[PROOF STEP]
by auto