[STATEMENT]
theorem dfs_dfss_termination:
  "\<lbrakk>v \<in> vertices ; pre_dfs v e\<rbrakk> \<Longrightarrow> dfs_dfss_dom(Inl(v, e))"
  "\<lbrakk>v \<in> vertices ; pre_dfss v e\<rbrakk> \<Longrightarrow> dfs_dfss_dom(Inr(v, e))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>v \<in> vertices; pre_dfs v e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inl (v, e))) &&& (\<lbrakk>v \<in> vertices; pre_dfss v e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>v \<in> vertices; pre_dfs v e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inl (v, e))
 2. \<lbrakk>v \<in> vertices; pre_dfss v e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>v \<in> vertices; pre_dfs v e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inl (v, e))
 2. \<lbrakk>v \<in> vertices; pre_dfss v e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e))
[PROOF STEP]
fix args
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>v \<in> vertices; pre_dfs v e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inl (v, e))
 2. \<lbrakk>v \<in> vertices; pre_dfss v e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e))
[PROOF STEP]
have "(case args
          of Inl(v,e) \<Rightarrow>
            v \<in> vertices \<and> pre_dfs v e
          |  Inr(v,e) \<Rightarrow>
             v \<in> vertices \<and> pre_dfss v e)
        \<longrightarrow> dfs_dfss_dom args" (is "?P args \<longrightarrow> ?Q args")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case args of Inl (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfs v e | Inr (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfss v e) \<longrightarrow> dfs_dfss_dom args
[PROOF STEP]
proof (rule wf_induct[OF wf_term])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<forall>y. (y, x) \<in> dfs_dfss_term \<longrightarrow> (case y of Inl (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfs v e | Inr (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfss v e) \<longrightarrow> dfs_dfss_dom y \<Longrightarrow> (case x of Inl (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfs v e | Inr (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfss v e) \<longrightarrow> dfs_dfss_dom x
[PROOF STEP]
fix arg :: "('v \<times> 'v env) + ('v \<times> 'v env)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<forall>y. (y, x) \<in> dfs_dfss_term \<longrightarrow> (case y of Inl (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfs v e | Inr (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfss v e) \<longrightarrow> dfs_dfss_dom y \<Longrightarrow> (case x of Inl (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfs v e | Inr (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfss v e) \<longrightarrow> dfs_dfss_dom x
[PROOF STEP]
assume ih: "\<forall> arg'. (arg', arg) \<in> dfs_dfss_term \<longrightarrow> (?P arg' \<longrightarrow> ?Q arg')"
[PROOF STATE]
proof (state)
this:
\<forall>arg'. (arg', arg) \<in> dfs_dfss_term \<longrightarrow> (case arg' of Inl (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfs v e | Inr (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfss v e) \<longrightarrow> dfs_dfss_dom arg'

goal (1 subgoal):
 1. \<And>x. \<forall>y. (y, x) \<in> dfs_dfss_term \<longrightarrow> (case y of Inl (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfs v e | Inr (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfss v e) \<longrightarrow> dfs_dfss_dom y \<Longrightarrow> (case x of Inl (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfs v e | Inr (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfss v e) \<longrightarrow> dfs_dfss_dom x
[PROOF STEP]
show "?P arg \<longrightarrow> ?Q arg"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case arg of Inl (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfs v e | Inr (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfss v e) \<longrightarrow> dfs_dfss_dom arg
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. case arg of Inl (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfs v e | Inr (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfss v e \<Longrightarrow> dfs_dfss_dom arg
[PROOF STEP]
assume P: "?P arg"
[PROOF STATE]
proof (state)
this:
case arg of Inl (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfs v e | Inr (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfss v e

goal (1 subgoal):
 1. case arg of Inl (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfs v e | Inr (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfss v e \<Longrightarrow> dfs_dfss_dom arg
[PROOF STEP]
show "?Q arg"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dfs_dfss_dom arg
[PROOF STEP]
proof (cases arg)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a. arg = Inl a \<Longrightarrow> dfs_dfss_dom arg
 2. \<And>b. arg = Inr b \<Longrightarrow> dfs_dfss_dom arg
[PROOF STEP]
case (Inl a)
[PROOF STATE]
proof (state)
this:
arg = Inl a

goal (2 subgoals):
 1. \<And>a. arg = Inl a \<Longrightarrow> dfs_dfss_dom arg
 2. \<And>b. arg = Inr b \<Longrightarrow> dfs_dfss_dom arg
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
arg = Inl a
[PROOF STEP]
obtain v e where a: "arg = Inl(v, e)"
[PROOF STATE]
proof (prove)
using this:
arg = Inl a

goal (1 subgoal):
 1. (\<And>v e. arg = Inl (v, e) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using dfs.cases
[PROOF STATE]
proof (prove)
using this:
arg = Inl a
(\<And>v e. ?x = (v, e) \<Longrightarrow> ?P) \<Longrightarrow> ?P

goal (1 subgoal):
 1. (\<And>v e. arg = Inl (v, e) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
arg = Inl (v, e)

goal (2 subgoals):
 1. \<And>a. arg = Inl a \<Longrightarrow> dfs_dfss_dom arg
 2. \<And>b. arg = Inr b \<Longrightarrow> dfs_dfss_dom arg
[PROOF STEP]
with P
[PROOF STATE]
proof (chain)
picking this:
case arg of Inl (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfs v e | Inr (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfss v e
arg = Inl (v, e)
[PROOF STEP]
have pre: "v \<in> vertices \<and> pre_dfs v e"
[PROOF STATE]
proof (prove)
using this:
case arg of Inl (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfs v e | Inr (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfss v e
arg = Inl (v, e)

goal (1 subgoal):
 1. v \<in> vertices \<and> pre_dfs v e
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
v \<in> vertices \<and> pre_dfs v e

goal (2 subgoals):
 1. \<And>a. arg = Inl a \<Longrightarrow> dfs_dfss_dom arg
 2. \<And>b. arg = Inr b \<Longrightarrow> dfs_dfss_dom arg
[PROOF STEP]
let ?e1 = "e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a. arg = Inl a \<Longrightarrow> dfs_dfss_dom arg
 2. \<And>b. arg = Inr b \<Longrightarrow> dfs_dfss_dom arg
[PROOF STEP]
let ?recarg = "Inr(v, ?e1)"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a. arg = Inl a \<Longrightarrow> dfs_dfss_dom arg
 2. \<And>b. arg = Inr b \<Longrightarrow> dfs_dfss_dom arg
[PROOF STEP]
from a pre
[PROOF STATE]
proof (chain)
picking this:
arg = Inl (v, e)
v \<in> vertices \<and> pre_dfs v e
[PROOF STEP]
have "(?recarg, arg) \<in> dfs_dfss_term"
[PROOF STATE]
proof (prove)
using this:
arg = Inl (v, e)
v \<in> vertices \<and> pre_dfs v e

goal (1 subgoal):
 1. (Inr (v, e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>), arg) \<in> dfs_dfss_term
[PROOF STEP]
by (auto simp: pre_dfs_def dfs_dfss_term_def)
[PROOF STATE]
proof (state)
this:
(Inr (v, e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>), arg) \<in> dfs_dfss_term

goal (2 subgoals):
 1. \<And>a. arg = Inl a \<Longrightarrow> dfs_dfss_dom arg
 2. \<And>b. arg = Inr b \<Longrightarrow> dfs_dfss_dom arg
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(Inr (v, e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>), arg) \<in> dfs_dfss_term

goal (2 subgoals):
 1. \<And>a. arg = Inl a \<Longrightarrow> dfs_dfss_dom arg
 2. \<And>b. arg = Inr b \<Longrightarrow> dfs_dfss_dom arg
[PROOF STEP]
from pre
[PROOF STATE]
proof (chain)
picking this:
v \<in> vertices \<and> pre_dfs v e
[PROOF STEP]
have "?P ?recarg"
[PROOF STATE]
proof (prove)
using this:
v \<in> vertices \<and> pre_dfs v e

goal (1 subgoal):
 1. case Inr (v, e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) of Inl (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfs v e | Inr (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfss v e
[PROOF STEP]
by (auto dest: pre_dfs_pre_dfss)
[PROOF STATE]
proof (state)
this:
case Inr (v, e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) of Inl (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfs v e | Inr (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfss v e

goal (2 subgoals):
 1. \<And>a. arg = Inl a \<Longrightarrow> dfs_dfss_dom arg
 2. \<And>b. arg = Inr b \<Longrightarrow> dfs_dfss_dom arg
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(Inr (v, e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>), arg) \<in> dfs_dfss_term
case Inr (v, e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) of Inl (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfs v e | Inr (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfss v e
[PROOF STEP]
have "?Q ?recarg"
[PROOF STATE]
proof (prove)
using this:
(Inr (v, e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>), arg) \<in> dfs_dfss_term
case Inr (v, e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) of Inl (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfs v e | Inr (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfss v e

goal (1 subgoal):
 1. dfs_dfss_dom (Inr (v, e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>))
[PROOF STEP]
using ih a
[PROOF STATE]
proof (prove)
using this:
(Inr (v, e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>), arg) \<in> dfs_dfss_term
case Inr (v, e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) of Inl (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfs v e | Inr (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfss v e
\<forall>arg'. (arg', arg) \<in> dfs_dfss_term \<longrightarrow> (case arg' of Inl (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfs v e | Inr (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfss v e) \<longrightarrow> dfs_dfss_dom arg'
arg = Inl (v, e)

goal (1 subgoal):
 1. dfs_dfss_dom (Inr (v, e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dfs_dfss_dom (Inr (v, e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>))

goal (2 subgoals):
 1. \<And>a. arg = Inl a \<Longrightarrow> dfs_dfss_dom arg
 2. \<And>b. arg = Inr b \<Longrightarrow> dfs_dfss_dom arg
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dfs_dfss_dom (Inr (v, e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>))
[PROOF STEP]
have "?Q (Inl(v, e))"
[PROOF STATE]
proof (prove)
using this:
dfs_dfss_dom (Inr (v, e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>))

goal (1 subgoal):
 1. dfs_dfss_dom (Inl (v, e))
[PROOF STEP]
by (auto intro: dfs_dfss.domintros)
[PROOF STATE]
proof (state)
this:
dfs_dfss_dom (Inl (v, e))

goal (2 subgoals):
 1. \<And>a. arg = Inl a \<Longrightarrow> dfs_dfss_dom arg
 2. \<And>b. arg = Inr b \<Longrightarrow> dfs_dfss_dom arg
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dfs_dfss_dom (Inl (v, e))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dfs_dfss_dom (Inl (v, e))

goal (1 subgoal):
 1. dfs_dfss_dom arg
[PROOF STEP]
by (simp add: a)
[PROOF STATE]
proof (state)
this:
dfs_dfss_dom arg

goal (1 subgoal):
 1. \<And>b. arg = Inr b \<Longrightarrow> dfs_dfss_dom arg
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>b. arg = Inr b \<Longrightarrow> dfs_dfss_dom arg
[PROOF STEP]
case (Inr b)
[PROOF STATE]
proof (state)
this:
arg = Inr b

goal (1 subgoal):
 1. \<And>b. arg = Inr b \<Longrightarrow> dfs_dfss_dom arg
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
arg = Inr b
[PROOF STEP]
obtain v e where b: "arg = Inr(v, e)"
[PROOF STATE]
proof (prove)
using this:
arg = Inr b

goal (1 subgoal):
 1. (\<And>v e. arg = Inr (v, e) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using dfs.cases
[PROOF STATE]
proof (prove)
using this:
arg = Inr b
(\<And>v e. ?x = (v, e) \<Longrightarrow> ?P) \<Longrightarrow> ?P

goal (1 subgoal):
 1. (\<And>v e. arg = Inr (v, e) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
arg = Inr (v, e)

goal (1 subgoal):
 1. \<And>b. arg = Inr b \<Longrightarrow> dfs_dfss_dom arg
[PROOF STEP]
with P
[PROOF STATE]
proof (chain)
picking this:
case arg of Inl (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfs v e | Inr (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfss v e
arg = Inr (v, e)
[PROOF STEP]
have pre: "v \<in> vertices \<and> pre_dfss v e"
[PROOF STATE]
proof (prove)
using this:
case arg of Inl (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfs v e | Inr (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfss v e
arg = Inr (v, e)

goal (1 subgoal):
 1. v \<in> vertices \<and> pre_dfss v e
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
v \<in> vertices \<and> pre_dfss v e

goal (1 subgoal):
 1. \<And>b. arg = Inr b \<Longrightarrow> dfs_dfss_dom arg
[PROOF STEP]
let ?sw = "SOME w. w \<in> successors v \<and> w \<notin> vsuccs e v"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>b. arg = Inr b \<Longrightarrow> dfs_dfss_dom arg
[PROOF STEP]
have "?Q (Inr(v, e))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dfs_dfss_dom (Inr (v, e))
[PROOF STEP]
proof (rule dfs_dfss.domintros)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>xb. \<lbrakk>(SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> visited e; \<not> dfs_dfss_dom (Inl (SOME x. edge v x \<and> x \<notin> vsuccs e v, e)); edge v xb\<rbrakk> \<Longrightarrow> xb \<in> vsuccs e v
 2. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 3. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
 4. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 5. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
[PROOF STEP]
fix w
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>xb. \<lbrakk>(SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> visited e; \<not> dfs_dfss_dom (Inl (SOME x. edge v x \<and> x \<notin> vsuccs e v, e)); edge v xb\<rbrakk> \<Longrightarrow> xb \<in> vsuccs e v
 2. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 3. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
 4. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 5. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
[PROOF STEP]
assume "w \<in> successors v"
                   "?sw \<notin> explored e"
                   "?sw \<notin> visited e"
                   "\<not> dfs_dfss_dom (Inl (?sw, e))"
[PROOF STATE]
proof (state)
this:
edge v w
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<notin> explored e
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<notin> visited e
\<not> dfs_dfss_dom (Inl (SOME w. edge v w \<and> w \<notin> vsuccs e v, e))

goal (5 subgoals):
 1. \<And>xb. \<lbrakk>(SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> visited e; \<not> dfs_dfss_dom (Inl (SOME x. edge v x \<and> x \<notin> vsuccs e v, e)); edge v xb\<rbrakk> \<Longrightarrow> xb \<in> vsuccs e v
 2. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 3. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
 4. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 5. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
[PROOF STEP]
show "w \<in> vsuccs e v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w \<in> vsuccs e v
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. w \<notin> vsuccs e v \<Longrightarrow> False
[PROOF STEP]
assume "w \<notin> vsuccs e v"
[PROOF STATE]
proof (state)
this:
w \<notin> vsuccs e v

goal (1 subgoal):
 1. w \<notin> vsuccs e v \<Longrightarrow> False
[PROOF STEP]
with \<open>w \<in> successors v\<close>
[PROOF STATE]
proof (chain)
picking this:
edge v w
w \<notin> vsuccs e v
[PROOF STEP]
have sw: "?sw \<in> successors v - vsuccs e v"
[PROOF STATE]
proof (prove)
using this:
edge v w
w \<notin> vsuccs e v

goal (1 subgoal):
 1. (SOME w. edge v w \<and> w \<notin> vsuccs e v) \<in> successors v - vsuccs e v
[PROOF STEP]
by (metis (mono_tags, lifting) Diff_iff some_eq_imp)
[PROOF STATE]
proof (state)
this:
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<in> successors v - vsuccs e v

goal (1 subgoal):
 1. w \<notin> vsuccs e v \<Longrightarrow> False
[PROOF STEP]
with pre \<open>?sw \<notin> visited e\<close>
[PROOF STATE]
proof (chain)
picking this:
v \<in> vertices \<and> pre_dfss v e
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<notin> visited e
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<in> successors v - vsuccs e v
[PROOF STEP]
have "pre_dfs ?sw e"
[PROOF STATE]
proof (prove)
using this:
v \<in> vertices \<and> pre_dfss v e
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<notin> visited e
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<in> successors v - vsuccs e v

goal (1 subgoal):
 1. pre_dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e
[PROOF STEP]
by (blast intro: pre_dfss_pre_dfs)
[PROOF STATE]
proof (state)
this:
pre_dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e

goal (1 subgoal):
 1. w \<notin> vsuccs e v \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
pre_dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e

goal (1 subgoal):
 1. w \<notin> vsuccs e v \<Longrightarrow> False
[PROOF STEP]
from pre sw sclosed
[PROOF STATE]
proof (chain)
picking this:
v \<in> vertices \<and> pre_dfss v e
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<in> successors v - vsuccs e v
\<forall>x\<in>vertices. successors x \<subseteq> vertices
[PROOF STEP]
have "?sw \<in> vertices"
[PROOF STATE]
proof (prove)
using this:
v \<in> vertices \<and> pre_dfss v e
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<in> successors v - vsuccs e v
\<forall>x\<in>vertices. successors x \<subseteq> vertices

goal (1 subgoal):
 1. (SOME w. edge v w \<and> w \<notin> vsuccs e v) \<in> vertices
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<in> vertices

goal (1 subgoal):
 1. w \<notin> vsuccs e v \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<in> vertices

goal (1 subgoal):
 1. w \<notin> vsuccs e v \<Longrightarrow> False
[PROOF STEP]
from pre
[PROOF STATE]
proof (chain)
picking this:
v \<in> vertices \<and> pre_dfss v e
[PROOF STEP]
have "(Inl(?sw,e), Inr(v,e)) \<in> dfs_dfss_term"
[PROOF STATE]
proof (prove)
using this:
v \<in> vertices \<and> pre_dfss v e

goal (1 subgoal):
 1. (Inl (SOME w. edge v w \<and> w \<notin> vsuccs e v, e), Inr (v, e)) \<in> dfs_dfss_term
[PROOF STEP]
by (simp add: dfs_dfss_term_def)
[PROOF STATE]
proof (state)
this:
(Inl (SOME w. edge v w \<and> w \<notin> vsuccs e v, e), Inr (v, e)) \<in> dfs_dfss_term

goal (1 subgoal):
 1. w \<notin> vsuccs e v \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
pre_dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<in> vertices
(Inl (SOME w. edge v w \<and> w \<notin> vsuccs e v, e), Inr (v, e)) \<in> dfs_dfss_term
[PROOF STEP]
have "dfs_dfss_dom (Inl(?sw,e))"
[PROOF STATE]
proof (prove)
using this:
pre_dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<in> vertices
(Inl (SOME w. edge v w \<and> w \<notin> vsuccs e v, e), Inr (v, e)) \<in> dfs_dfss_term

goal (1 subgoal):
 1. dfs_dfss_dom (Inl (SOME w. edge v w \<and> w \<notin> vsuccs e v, e))
[PROOF STEP]
using ih b
[PROOF STATE]
proof (prove)
using this:
pre_dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<in> vertices
(Inl (SOME w. edge v w \<and> w \<notin> vsuccs e v, e), Inr (v, e)) \<in> dfs_dfss_term
\<forall>arg'. (arg', arg) \<in> dfs_dfss_term \<longrightarrow> (case arg' of Inl (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfs v e | Inr (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfss v e) \<longrightarrow> dfs_dfss_dom arg'
arg = Inr (v, e)

goal (1 subgoal):
 1. dfs_dfss_dom (Inl (SOME w. edge v w \<and> w \<notin> vsuccs e v, e))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dfs_dfss_dom (Inl (SOME w. edge v w \<and> w \<notin> vsuccs e v, e))

goal (1 subgoal):
 1. w \<notin> vsuccs e v \<Longrightarrow> False
[PROOF STEP]
with \<open>\<not> dfs_dfss_dom (Inl (?sw, e))\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> dfs_dfss_dom (Inl (SOME w. edge v w \<and> w \<notin> vsuccs e v, e))
dfs_dfss_dom (Inl (SOME w. edge v w \<and> w \<notin> vsuccs e v, e))
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
\<not> dfs_dfss_dom (Inl (SOME w. edge v w \<and> w \<notin> vsuccs e v, e))
dfs_dfss_dom (Inl (SOME w. edge v w \<and> w \<notin> vsuccs e v, e))

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
w \<in> vsuccs e v

goal (4 subgoals):
 1. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 2. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
 3. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 4. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 2. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
 3. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 4. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
[PROOF STEP]
let ?e' = "dfs ?sw e"
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 2. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
 3. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 4. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
[PROOF STEP]
let ?e''= "?e'\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs ?e' v \<union> {?sw}
                                         else vsuccs ?e' x\<rparr>"
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 2. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
 3. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 4. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
[PROOF STEP]
fix w
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 2. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
 3. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 4. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
[PROOF STEP]
assume asm: "w \<in> successors v" "w \<notin> vsuccs e v"
                        "?sw \<notin> visited e" "?sw \<notin> explored e"
[PROOF STATE]
proof (state)
this:
edge v w
w \<notin> vsuccs e v
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<notin> visited e
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<notin> explored e

goal (4 subgoals):
 1. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 2. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
 3. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 4. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
[PROOF STEP]
from \<open>w \<in> successors v\<close> \<open>w \<notin> vsuccs e v\<close>
[PROOF STATE]
proof (chain)
picking this:
edge v w
w \<notin> vsuccs e v
[PROOF STEP]
have sw: "?sw \<in> successors v - vsuccs e v"
[PROOF STATE]
proof (prove)
using this:
edge v w
w \<notin> vsuccs e v

goal (1 subgoal):
 1. (SOME w. edge v w \<and> w \<notin> vsuccs e v) \<in> successors v - vsuccs e v
[PROOF STEP]
by (metis (no_types, lifting) Diff_iff some_eq_imp)
[PROOF STATE]
proof (state)
this:
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<in> successors v - vsuccs e v

goal (4 subgoals):
 1. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 2. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
 3. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 4. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
[PROOF STEP]
with pre \<open>?sw \<notin> visited e\<close>
[PROOF STATE]
proof (chain)
picking this:
v \<in> vertices \<and> pre_dfss v e
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<notin> visited e
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<in> successors v - vsuccs e v
[PROOF STEP]
have "pre_dfs ?sw e"
[PROOF STATE]
proof (prove)
using this:
v \<in> vertices \<and> pre_dfss v e
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<notin> visited e
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<in> successors v - vsuccs e v

goal (1 subgoal):
 1. pre_dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e
[PROOF STEP]
by (blast intro: pre_dfss_pre_dfs)
[PROOF STATE]
proof (state)
this:
pre_dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e

goal (4 subgoals):
 1. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 2. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
 3. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 4. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
pre_dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e

goal (4 subgoals):
 1. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 2. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
 3. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 4. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
[PROOF STEP]
from pre sw sclosed
[PROOF STATE]
proof (chain)
picking this:
v \<in> vertices \<and> pre_dfss v e
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<in> successors v - vsuccs e v
\<forall>x\<in>vertices. successors x \<subseteq> vertices
[PROOF STEP]
have "?sw \<in> vertices"
[PROOF STATE]
proof (prove)
using this:
v \<in> vertices \<and> pre_dfss v e
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<in> successors v - vsuccs e v
\<forall>x\<in>vertices. successors x \<subseteq> vertices

goal (1 subgoal):
 1. (SOME w. edge v w \<and> w \<notin> vsuccs e v) \<in> vertices
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<in> vertices

goal (4 subgoals):
 1. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 2. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
 3. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 4. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<in> vertices

goal (4 subgoals):
 1. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 2. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
 3. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 4. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
[PROOF STEP]
from pre
[PROOF STATE]
proof (chain)
picking this:
v \<in> vertices \<and> pre_dfss v e
[PROOF STEP]
have "(Inl(?sw, e), Inr(v,e)) \<in> dfs_dfss_term"
[PROOF STATE]
proof (prove)
using this:
v \<in> vertices \<and> pre_dfss v e

goal (1 subgoal):
 1. (Inl (SOME w. edge v w \<and> w \<notin> vsuccs e v, e), Inr (v, e)) \<in> dfs_dfss_term
[PROOF STEP]
by (simp add: dfs_dfss_term_def)
[PROOF STATE]
proof (state)
this:
(Inl (SOME w. edge v w \<and> w \<notin> vsuccs e v, e), Inr (v, e)) \<in> dfs_dfss_term

goal (4 subgoals):
 1. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 2. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
 3. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 4. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
pre_dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<in> vertices
(Inl (SOME w. edge v w \<and> w \<notin> vsuccs e v, e), Inr (v, e)) \<in> dfs_dfss_term
[PROOF STEP]
have "dfs_dfss_dom (Inl(?sw, e))"
[PROOF STATE]
proof (prove)
using this:
pre_dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<in> vertices
(Inl (SOME w. edge v w \<and> w \<notin> vsuccs e v, e), Inr (v, e)) \<in> dfs_dfss_term

goal (1 subgoal):
 1. dfs_dfss_dom (Inl (SOME w. edge v w \<and> w \<notin> vsuccs e v, e))
[PROOF STEP]
using ih b
[PROOF STATE]
proof (prove)
using this:
pre_dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<in> vertices
(Inl (SOME w. edge v w \<and> w \<notin> vsuccs e v, e), Inr (v, e)) \<in> dfs_dfss_term
\<forall>arg'. (arg', arg) \<in> dfs_dfss_term \<longrightarrow> (case arg' of Inl (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfs v e | Inr (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfss v e) \<longrightarrow> dfs_dfss_dom arg'
arg = Inr (v, e)

goal (1 subgoal):
 1. dfs_dfss_dom (Inl (SOME w. edge v w \<and> w \<notin> vsuccs e v, e))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dfs_dfss_dom (Inl (SOME w. edge v w \<and> w \<notin> vsuccs e v, e))

goal (4 subgoals):
 1. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 2. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
 3. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 4. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
[PROOF STEP]
from this \<open>pre_dfs ?sw e\<close>
[PROOF STATE]
proof (chain)
picking this:
dfs_dfss_dom (Inl (SOME w. edge v w \<and> w \<notin> vsuccs e v, e))
pre_dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e
[PROOF STEP]
have post: "post_dfs ?sw e ?e'"
[PROOF STATE]
proof (prove)
using this:
dfs_dfss_dom (Inl (SOME w. edge v w \<and> w \<notin> vsuccs e v, e))
pre_dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e

goal (1 subgoal):
 1. post_dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e)
[PROOF STEP]
by (rule pre_post)
[PROOF STATE]
proof (state)
this:
post_dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e)

goal (4 subgoals):
 1. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 2. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
 3. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 4. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
[PROOF STEP]
hence "sub_env e ?e'"
[PROOF STATE]
proof (prove)
using this:
post_dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e)

goal (1 subgoal):
 1. sub_env e (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e)
[PROOF STEP]
by (simp add: post_dfs_def)
[PROOF STATE]
proof (state)
this:
sub_env e (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e)

goal (4 subgoals):
 1. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 2. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
 3. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 4. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sub_env e (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e)

goal (4 subgoals):
 1. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 2. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
 3. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 4. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
[PROOF STEP]
have "sub_env ?e' ?e''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sub_env (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) x\<rparr>)
[PROOF STEP]
by (auto simp: sub_env_def)
[PROOF STATE]
proof (state)
this:
sub_env (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) x\<rparr>)

goal (4 subgoals):
 1. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 2. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
 3. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 4. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
sub_env e (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e)
sub_env (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) x\<rparr>)
[PROOF STEP]
have "sub_env e ?e''"
[PROOF STATE]
proof (prove)
using this:
sub_env e (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e)
sub_env (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) x\<rparr>)

goal (1 subgoal):
 1. sub_env e (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) x\<rparr>)
[PROOF STEP]
by (rule sub_env_trans)
[PROOF STATE]
proof (state)
this:
sub_env e (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) x\<rparr>)

goal (4 subgoals):
 1. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 2. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
 3. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 4. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
[PROOF STEP]
with pre \<open>?sw \<in> vertices\<close> sw
[PROOF STATE]
proof (chain)
picking this:
v \<in> vertices \<and> pre_dfss v e
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<in> vertices
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<in> successors v - vsuccs e v
sub_env e (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) x\<rparr>)
[PROOF STEP]
have "(Inr(v, ?e''), Inr(v, e)) \<in> dfs_dfss_term"
[PROOF STATE]
proof (prove)
using this:
v \<in> vertices \<and> pre_dfss v e
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<in> vertices
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<in> successors v - vsuccs e v
sub_env e (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) x\<rparr>)

goal (1 subgoal):
 1. (Inr (v, dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) x\<rparr>), Inr (v, e)) \<in> dfs_dfss_term
[PROOF STEP]
by (auto simp: dfs_dfss_term_def)
[PROOF STATE]
proof (state)
this:
(Inr (v, dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) x\<rparr>), Inr (v, e)) \<in> dfs_dfss_term

goal (4 subgoals):
 1. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 2. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
 3. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 4. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(Inr (v, dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) x\<rparr>), Inr (v, e)) \<in> dfs_dfss_term

goal (4 subgoals):
 1. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 2. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
 3. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 4. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
[PROOF STEP]
from pre post sw \<open>?sw \<notin> visited e\<close>
[PROOF STATE]
proof (chain)
picking this:
v \<in> vertices \<and> pre_dfss v e
post_dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e)
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<in> successors v - vsuccs e v
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<notin> visited e
[PROOF STEP]
have "pre_dfss v ?e''"
[PROOF STATE]
proof (prove)
using this:
v \<in> vertices \<and> pre_dfss v e
post_dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e)
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<in> successors v - vsuccs e v
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<notin> visited e

goal (1 subgoal):
 1. pre_dfss v (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) x\<rparr>)
[PROOF STEP]
by (blast intro: pre_dfss_post_dfs_pre_dfss)
[PROOF STATE]
proof (state)
this:
pre_dfss v (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) x\<rparr>)

goal (4 subgoals):
 1. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 2. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
 3. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 4. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(Inr (v, dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) x\<rparr>), Inr (v, e)) \<in> dfs_dfss_term
pre_dfss v (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) x\<rparr>)
[PROOF STEP]
show "dfs_dfss_dom(Inr(v, ?e''))"
[PROOF STATE]
proof (prove)
using this:
(Inr (v, dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) x\<rparr>), Inr (v, e)) \<in> dfs_dfss_term
pre_dfss v (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) x\<rparr>)

goal (1 subgoal):
 1. dfs_dfss_dom (Inr (v, dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) x\<rparr>))
[PROOF STEP]
using pre ih b
[PROOF STATE]
proof (prove)
using this:
(Inr (v, dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) x\<rparr>), Inr (v, e)) \<in> dfs_dfss_term
pre_dfss v (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) x\<rparr>)
v \<in> vertices \<and> pre_dfss v e
\<forall>arg'. (arg', arg) \<in> dfs_dfss_term \<longrightarrow> (case arg' of Inl (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfs v e | Inr (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfss v e) \<longrightarrow> dfs_dfss_dom arg'
arg = Inr (v, e)

goal (1 subgoal):
 1. dfs_dfss_dom (Inr (v, dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) x\<rparr>))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dfs_dfss_dom (Inr (v, dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs (dfs (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) x\<rparr>))

goal (3 subgoals):
 1. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 2. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 3. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 2. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 3. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
[PROOF STEP]
let ?e'' =  "e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {?sw} else vsuccs e x\<rparr>"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 2. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 3. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
[PROOF STEP]
fix w
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 2. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 3. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
[PROOF STEP]
assume "w \<in> successors v" "w \<notin> vsuccs e v"
                   "?sw \<notin> visited e" "?sw \<in> explored e"
[PROOF STATE]
proof (state)
this:
edge v w
w \<notin> vsuccs e v
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<notin> visited e
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<in> explored e

goal (3 subgoals):
 1. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 2. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 3. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
[PROOF STEP]
with pre
[PROOF STATE]
proof (chain)
picking this:
v \<in> vertices \<and> pre_dfss v e
edge v w
w \<notin> vsuccs e v
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<notin> visited e
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<in> explored e
[PROOF STEP]
have "False"
[PROOF STATE]
proof (prove)
using this:
v \<in> vertices \<and> pre_dfss v e
edge v w
w \<notin> vsuccs e v
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<notin> visited e
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<in> explored e

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding pre_dfss_def wf_env_def
[PROOF STATE]
proof (prove)
using this:
v \<in> vertices \<and> ((\<forall>n\<in>visited e. reachable (root e) n) \<and> distinct (stack e) \<and> distinct (cstack e) \<and> (\<forall>n m. n \<preceq> m in stack e \<longrightarrow> n \<preceq> m in cstack e) \<and> (\<forall>n m. n \<preceq> m in stack e \<longrightarrow> reachable m n) \<and> explored e \<subseteq> visited e \<and> set (cstack e) \<subseteq> visited e \<and> (\<forall>n\<in>explored e. \<forall>m. reachable n m \<longrightarrow> m \<in> explored e) \<and> (\<forall>n. vsuccs e n \<subseteq> successors n \<inter> visited e) \<and> (\<forall>n. n \<notin> visited e \<longrightarrow> vsuccs e n = {}) \<and> (\<forall>n\<in>explored e. vsuccs e n = successors n) \<and> (\<forall>n\<in>visited e - set (cstack e). vsuccs e n = successors n) \<and> (\<forall>n m. (m \<in> \<S> e n) = (\<S> e n = \<S> e m)) \<and> (\<forall>n. n \<notin> visited e \<longrightarrow> \<S> e n = {n}) \<and> (\<forall>n\<in>set (stack e). \<forall>m\<in>set (stack e). n \<noteq> m \<longrightarrow> \<S> e n \<inter> \<S> e m = {}) \<and> \<Union> {\<S> e n |n. n \<in> set (stack e)} = visited e - explored e \<and> (\<forall>n\<in>set (stack e). \<forall>m\<in>\<S> e n. m \<in> set (cstack e) \<longrightarrow> m \<preceq> n in cstack e) \<and> (\<forall>n m. n \<preceq> m in stack e \<and> n \<noteq> m \<longrightarrow> (\<forall>u\<in>\<S> e n. \<not> reachable_avoiding u m (unvisited e n))) \<and> (\<forall>n. is_subscc (\<S> e n)) \<and> Ball (sccs e) is_scc \<and> \<Union> (sccs e) = explored e) \<and> v \<in> visited e \<and> stack e \<noteq> [] \<and> v \<in> \<S> e (hd (stack e)) \<and> (\<forall>w\<in>vsuccs e v. w \<in> explored e \<union> \<S> e (hd (stack e))) \<and> (\<forall>n\<in>set (stack e). reachable n v) \<and> (\<exists>ns. cstack e = v # ns)
edge v w
w \<notin> vsuccs e v
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<notin> visited e
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<in> explored e

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

goal (3 subgoals):
 1. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 2. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 3. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
[PROOF STEP]
thus "?Q (Inr(v, ?e''))"
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs e x\<rparr>))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs e x\<rparr>))

goal (2 subgoals):
 1. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 2. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 2. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
[PROOF STEP]
fix w
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 2. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
[PROOF STEP]
assume asm: "w \<in> successors v" "w \<notin> vsuccs e v"
                        "?sw \<in> visited e" "?sw \<in> explored e"
[PROOF STATE]
proof (state)
this:
edge v w
w \<notin> vsuccs e v
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<in> visited e
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<in> explored e

goal (2 subgoals):
 1. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 2. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
[PROOF STEP]
let ?e'' =  "e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {?sw} else vsuccs e x\<rparr>"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 2. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
[PROOF STEP]
let ?recarg = "Inr(v, ?e'')"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 2. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
[PROOF STEP]
from \<open>w \<in> successors v\<close> \<open>w \<notin> vsuccs e v\<close>
[PROOF STATE]
proof (chain)
picking this:
edge v w
w \<notin> vsuccs e v
[PROOF STEP]
have sw: "?sw \<in> successors v - vsuccs e v"
[PROOF STATE]
proof (prove)
using this:
edge v w
w \<notin> vsuccs e v

goal (1 subgoal):
 1. (SOME w. edge v w \<and> w \<notin> vsuccs e v) \<in> successors v - vsuccs e v
[PROOF STEP]
by (metis (no_types, lifting) Diff_iff some_eq_imp)
[PROOF STATE]
proof (state)
this:
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<in> successors v - vsuccs e v

goal (2 subgoals):
 1. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 2. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
[PROOF STEP]
have "(?recarg, arg) \<in> dfs_dfss_term"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs e x\<rparr>), arg) \<in> dfs_dfss_term
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs e x\<rparr>), arg) \<in> dfs_dfss_term
[PROOF STEP]
have "sub_env e ?e''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sub_env e (e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs e x\<rparr>)
[PROOF STEP]
by (auto simp: sub_env_def)
[PROOF STATE]
proof (state)
this:
sub_env e (e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs e x\<rparr>)

goal (1 subgoal):
 1. (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs e x\<rparr>), arg) \<in> dfs_dfss_term
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sub_env e (e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs e x\<rparr>)

goal (1 subgoal):
 1. (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs e x\<rparr>), arg) \<in> dfs_dfss_term
[PROOF STEP]
from sw pre sclosed
[PROOF STATE]
proof (chain)
picking this:
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<in> successors v - vsuccs e v
v \<in> vertices \<and> pre_dfss v e
\<forall>x\<in>vertices. successors x \<subseteq> vertices
[PROOF STEP]
have "\<exists>u \<in> vertices. u \<notin> vsuccs e v \<and> u \<in> vsuccs ?e'' v"
[PROOF STATE]
proof (prove)
using this:
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<in> successors v - vsuccs e v
v \<in> vertices \<and> pre_dfss v e
\<forall>x\<in>vertices. successors x \<subseteq> vertices

goal (1 subgoal):
 1. \<exists>u\<in>vertices. u \<notin> vsuccs e v \<and> u \<in> vsuccs (e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs e x\<rparr>) v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>u\<in>vertices. u \<notin> vsuccs e v \<and> u \<in> vsuccs (e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs e x\<rparr>) v

goal (1 subgoal):
 1. (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs e x\<rparr>), arg) \<in> dfs_dfss_term
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
sub_env e (e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs e x\<rparr>)
\<exists>u\<in>vertices. u \<notin> vsuccs e v \<and> u \<in> vsuccs (e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs e x\<rparr>) v
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sub_env e (e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs e x\<rparr>)
\<exists>u\<in>vertices. u \<notin> vsuccs e v \<and> u \<in> vsuccs (e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs e x\<rparr>) v

goal (1 subgoal):
 1. (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs e x\<rparr>), arg) \<in> dfs_dfss_term
[PROOF STEP]
using pre b
[PROOF STATE]
proof (prove)
using this:
sub_env e (e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs e x\<rparr>)
\<exists>u\<in>vertices. u \<notin> vsuccs e v \<and> u \<in> vsuccs (e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs e x\<rparr>) v
v \<in> vertices \<and> pre_dfss v e
arg = Inr (v, e)

goal (1 subgoal):
 1. (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs e x\<rparr>), arg) \<in> dfs_dfss_term
[PROOF STEP]
unfolding dfs_dfss_term_def
[PROOF STATE]
proof (prove)
using this:
sub_env e (e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs e x\<rparr>)
\<exists>u\<in>vertices. u \<notin> vsuccs e v \<and> u \<in> vsuccs (e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs e x\<rparr>) v
v \<in> vertices \<and> pre_dfss v e
arg = Inr (v, e)

goal (1 subgoal):
 1. (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs e x\<rparr>), arg) \<in> {(Inr (v, e1), Inl (v, e)) |v e e1. v \<in> vertices - visited e \<and> visited e1 = visited e \<union> {v}} \<union> {(Inl (w, e), Inr (v, e)) |v w e. v \<in> vertices} \<union> {(Inr (v, e''), Inr (v, e)) |v e e''. v \<in> vertices \<and> sub_env e e'' \<and> (\<exists>w\<in>vertices. w \<notin> vsuccs e v \<and> w \<in> vsuccs e'' v)}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs e x\<rparr>), arg) \<in> dfs_dfss_term

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs e x\<rparr>), arg) \<in> dfs_dfss_term

goal (2 subgoals):
 1. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 2. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs e x\<rparr>), arg) \<in> dfs_dfss_term

goal (2 subgoals):
 1. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 2. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
[PROOF STEP]
from pre sw \<open>?sw \<in> explored e\<close>
[PROOF STATE]
proof (chain)
picking this:
v \<in> vertices \<and> pre_dfss v e
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<in> successors v - vsuccs e v
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<in> explored e
[PROOF STEP]
have "?P ?recarg"
[PROOF STATE]
proof (prove)
using this:
v \<in> vertices \<and> pre_dfss v e
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<in> successors v - vsuccs e v
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<in> explored e

goal (1 subgoal):
 1. case Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs e x\<rparr>) of Inl (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfs v e | Inr (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfss v e
[PROOF STEP]
by (auto dest: pre_dfss_explored_pre_dfss)
[PROOF STATE]
proof (state)
this:
case Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs e x\<rparr>) of Inl (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfs v e | Inr (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfss v e

goal (2 subgoals):
 1. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>))
 2. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs e x\<rparr>), arg) \<in> dfs_dfss_term
case Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs e x\<rparr>) of Inl (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfs v e | Inr (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfss v e
[PROOF STEP]
show "?Q ?recarg"
[PROOF STATE]
proof (prove)
using this:
(Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs e x\<rparr>), arg) \<in> dfs_dfss_term
case Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs e x\<rparr>) of Inl (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfs v e | Inr (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfss v e

goal (1 subgoal):
 1. dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs e x\<rparr>))
[PROOF STEP]
using ih b
[PROOF STATE]
proof (prove)
using this:
(Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs e x\<rparr>), arg) \<in> dfs_dfss_term
case Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs e x\<rparr>) of Inl (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfs v e | Inr (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfss v e
\<forall>arg'. (arg', arg) \<in> dfs_dfss_term \<longrightarrow> (case arg' of Inl (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfs v e | Inr (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfss v e) \<longrightarrow> dfs_dfss_dom arg'
arg = Inr (v, e)

goal (1 subgoal):
 1. dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs e x\<rparr>))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
dfs_dfss_dom (Inr (v, e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs e x\<rparr>))

goal (1 subgoal):
 1. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
[PROOF STEP]
fix w
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
[PROOF STEP]
assume asm: "w \<in> successors v" "w \<notin> vsuccs e v"
                        "?sw \<in> visited e" "?sw \<notin> explored e"
[PROOF STATE]
proof (state)
this:
edge v w
w \<notin> vsuccs e v
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<in> visited e
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<notin> explored e

goal (1 subgoal):
 1. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
[PROOF STEP]
let ?eu = "unite v ?sw e"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
[PROOF STEP]
let ?e'' = "?eu\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs ?eu v \<union> {?sw} else vsuccs ?eu x\<rparr>"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
[PROOF STEP]
let ?recarg = "Inr(v, ?e'')"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
[PROOF STEP]
from \<open>w \<in> successors v\<close> \<open>w \<notin> vsuccs e v\<close>
[PROOF STATE]
proof (chain)
picking this:
edge v w
w \<notin> vsuccs e v
[PROOF STEP]
have sw: "?sw \<in> successors v - vsuccs e v"
[PROOF STATE]
proof (prove)
using this:
edge v w
w \<notin> vsuccs e v

goal (1 subgoal):
 1. (SOME w. edge v w \<and> w \<notin> vsuccs e v) \<in> successors v - vsuccs e v
[PROOF STEP]
by (metis (no_types, lifting) Diff_iff some_eq_imp)
[PROOF STATE]
proof (state)
this:
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<in> successors v - vsuccs e v

goal (1 subgoal):
 1. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
[PROOF STEP]
have "(?recarg, arg) \<in> dfs_dfss_term"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Inr (v, unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) x\<rparr>), arg) \<in> dfs_dfss_term
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (Inr (v, unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) x\<rparr>), arg) \<in> dfs_dfss_term
[PROOF STEP]
from pre asm sw
[PROOF STATE]
proof (chain)
picking this:
v \<in> vertices \<and> pre_dfss v e
edge v w
w \<notin> vsuccs e v
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<in> visited e
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<notin> explored e
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<in> successors v - vsuccs e v
[PROOF STEP]
have "sub_env e ?eu"
[PROOF STATE]
proof (prove)
using this:
v \<in> vertices \<and> pre_dfss v e
edge v w
w \<notin> vsuccs e v
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<in> visited e
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<notin> explored e
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<in> successors v - vsuccs e v

goal (1 subgoal):
 1. sub_env e (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e)
[PROOF STEP]
by (blast dest: unite_sub_env)
[PROOF STATE]
proof (state)
this:
sub_env e (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e)

goal (1 subgoal):
 1. (Inr (v, unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) x\<rparr>), arg) \<in> dfs_dfss_term
[PROOF STEP]
hence "sub_env e ?e''"
[PROOF STATE]
proof (prove)
using this:
sub_env e (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e)

goal (1 subgoal):
 1. sub_env e (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) x\<rparr>)
[PROOF STEP]
by (auto simp: sub_env_def)
[PROOF STATE]
proof (state)
this:
sub_env e (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) x\<rparr>)

goal (1 subgoal):
 1. (Inr (v, unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) x\<rparr>), arg) \<in> dfs_dfss_term
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sub_env e (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) x\<rparr>)

goal (1 subgoal):
 1. (Inr (v, unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) x\<rparr>), arg) \<in> dfs_dfss_term
[PROOF STEP]
from sw pre sclosed
[PROOF STATE]
proof (chain)
picking this:
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<in> successors v - vsuccs e v
v \<in> vertices \<and> pre_dfss v e
\<forall>x\<in>vertices. successors x \<subseteq> vertices
[PROOF STEP]
have "\<exists>u \<in> vertices. u \<notin> vsuccs e v \<and> u \<in> vsuccs ?e'' v"
[PROOF STATE]
proof (prove)
using this:
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<in> successors v - vsuccs e v
v \<in> vertices \<and> pre_dfss v e
\<forall>x\<in>vertices. successors x \<subseteq> vertices

goal (1 subgoal):
 1. \<exists>u\<in>vertices. u \<notin> vsuccs e v \<and> u \<in> vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) x\<rparr>) v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>u\<in>vertices. u \<notin> vsuccs e v \<and> u \<in> vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) x\<rparr>) v

goal (1 subgoal):
 1. (Inr (v, unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) x\<rparr>), arg) \<in> dfs_dfss_term
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
sub_env e (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) x\<rparr>)
\<exists>u\<in>vertices. u \<notin> vsuccs e v \<and> u \<in> vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) x\<rparr>) v
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sub_env e (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) x\<rparr>)
\<exists>u\<in>vertices. u \<notin> vsuccs e v \<and> u \<in> vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) x\<rparr>) v

goal (1 subgoal):
 1. (Inr (v, unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) x\<rparr>), arg) \<in> dfs_dfss_term
[PROOF STEP]
using pre b
[PROOF STATE]
proof (prove)
using this:
sub_env e (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) x\<rparr>)
\<exists>u\<in>vertices. u \<notin> vsuccs e v \<and> u \<in> vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) x\<rparr>) v
v \<in> vertices \<and> pre_dfss v e
arg = Inr (v, e)

goal (1 subgoal):
 1. (Inr (v, unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) x\<rparr>), arg) \<in> dfs_dfss_term
[PROOF STEP]
unfolding dfs_dfss_term_def
[PROOF STATE]
proof (prove)
using this:
sub_env e (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) x\<rparr>)
\<exists>u\<in>vertices. u \<notin> vsuccs e v \<and> u \<in> vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) x\<rparr>) v
v \<in> vertices \<and> pre_dfss v e
arg = Inr (v, e)

goal (1 subgoal):
 1. (Inr (v, unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) x\<rparr>), arg) \<in> {(Inr (v, e1), Inl (v, e)) |v e e1. v \<in> vertices - visited e \<and> visited e1 = visited e \<union> {v}} \<union> {(Inl (w, e), Inr (v, e)) |v w e. v \<in> vertices} \<union> {(Inr (v, e''), Inr (v, e)) |v e e''. v \<in> vertices \<and> sub_env e e'' \<and> (\<exists>w\<in>vertices. w \<notin> vsuccs e v \<and> w \<in> vsuccs e'' v)}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(Inr (v, unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) x\<rparr>), arg) \<in> dfs_dfss_term

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(Inr (v, unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) x\<rparr>), arg) \<in> dfs_dfss_term

goal (1 subgoal):
 1. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(Inr (v, unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) x\<rparr>), arg) \<in> dfs_dfss_term

goal (1 subgoal):
 1. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
[PROOF STEP]
from pre sw \<open>?sw \<in> visited e\<close> \<open>?sw \<notin> explored e\<close>
[PROOF STATE]
proof (chain)
picking this:
v \<in> vertices \<and> pre_dfss v e
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<in> successors v - vsuccs e v
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<in> visited e
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<notin> explored e
[PROOF STEP]
have "?P ?recarg"
[PROOF STATE]
proof (prove)
using this:
v \<in> vertices \<and> pre_dfss v e
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<in> successors v - vsuccs e v
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<in> visited e
(SOME w. edge v w \<and> w \<notin> vsuccs e v) \<notin> explored e

goal (1 subgoal):
 1. case Inr (v, unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) x\<rparr>) of Inl (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfs v e | Inr (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfss v e
[PROOF STEP]
by (auto dest: pre_dfss_unite_pre_dfss)
[PROOF STATE]
proof (state)
this:
case Inr (v, unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) x\<rparr>) of Inl (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfs v e | Inr (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfss v e

goal (1 subgoal):
 1. \<And>xd. \<lbrakk>edge v xd; xd \<notin> vsuccs e v; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e; (SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(Inr (v, unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) x\<rparr>), arg) \<in> dfs_dfss_term
case Inr (v, unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) x\<rparr>) of Inl (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfs v e | Inr (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfss v e
[PROOF STEP]
show "?Q ?recarg"
[PROOF STATE]
proof (prove)
using this:
(Inr (v, unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) x\<rparr>), arg) \<in> dfs_dfss_term
case Inr (v, unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) x\<rparr>) of Inl (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfs v e | Inr (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfss v e

goal (1 subgoal):
 1. dfs_dfss_dom (Inr (v, unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) x\<rparr>))
[PROOF STEP]
using ih b
[PROOF STATE]
proof (prove)
using this:
(Inr (v, unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) x\<rparr>), arg) \<in> dfs_dfss_term
case Inr (v, unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) x\<rparr>) of Inl (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfs v e | Inr (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfss v e
\<forall>arg'. (arg', arg) \<in> dfs_dfss_term \<longrightarrow> (case arg' of Inl (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfs v e | Inr (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfss v e) \<longrightarrow> dfs_dfss_dom arg'
arg = Inr (v, e)

goal (1 subgoal):
 1. dfs_dfss_dom (Inr (v, unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) x\<rparr>))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dfs_dfss_dom (Inr (v, unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) v \<union> {SOME w. edge v w \<and> w \<notin> vsuccs e v} else vsuccs (unite v (SOME w. edge v w \<and> w \<notin> vsuccs e v) e) x\<rparr>))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
dfs_dfss_dom (Inr (v, e))

goal (1 subgoal):
 1. \<And>b. arg = Inr b \<Longrightarrow> dfs_dfss_dom arg
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dfs_dfss_dom (Inr (v, e))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dfs_dfss_dom (Inr (v, e))

goal (1 subgoal):
 1. dfs_dfss_dom arg
[PROOF STEP]
by (simp add: b)
[PROOF STATE]
proof (state)
this:
dfs_dfss_dom arg

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
dfs_dfss_dom arg

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(case arg of Inl (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfs v e | Inr (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfss v e) \<longrightarrow> dfs_dfss_dom arg

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(case args of Inl (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfs v e | Inr (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfss v e) \<longrightarrow> dfs_dfss_dom args

goal (2 subgoals):
 1. \<lbrakk>v \<in> vertices; pre_dfs v e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inl (v, e))
 2. \<lbrakk>v \<in> vertices; pre_dfss v e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(case ?args8 of Inl (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfs v e | Inr (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfss v e) \<longrightarrow> dfs_dfss_dom ?args8

goal (2 subgoals):
 1. \<lbrakk>v \<in> vertices; pre_dfs v e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inl (v, e))
 2. \<lbrakk>v \<in> vertices; pre_dfss v e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e))
[PROOF STEP]
note dom=this
[PROOF STATE]
proof (state)
this:
(case ?args8 of Inl (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfs v e | Inr (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfss v e) \<longrightarrow> dfs_dfss_dom ?args8

goal (2 subgoals):
 1. \<lbrakk>v \<in> vertices; pre_dfs v e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inl (v, e))
 2. \<lbrakk>v \<in> vertices; pre_dfss v e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e))
[PROOF STEP]
from dom
[PROOF STATE]
proof (chain)
picking this:
(case ?args8 of Inl (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfs v e | Inr (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfss v e) \<longrightarrow> dfs_dfss_dom ?args8
[PROOF STEP]
show "\<lbrakk> v \<in> vertices ; pre_dfs v e\<rbrakk> \<Longrightarrow> dfs_dfss_dom(Inl(v, e))"
[PROOF STATE]
proof (prove)
using this:
(case ?args8 of Inl (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfs v e | Inr (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfss v e) \<longrightarrow> dfs_dfss_dom ?args8

goal (1 subgoal):
 1. \<lbrakk>v \<in> vertices; pre_dfs v e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inl (v, e))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>v \<in> vertices; pre_dfs v e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inl (v, e))

goal (1 subgoal):
 1. \<lbrakk>v \<in> vertices; pre_dfss v e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e))
[PROOF STEP]
from dom
[PROOF STATE]
proof (chain)
picking this:
(case ?args8 of Inl (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfs v e | Inr (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfss v e) \<longrightarrow> dfs_dfss_dom ?args8
[PROOF STEP]
show "\<lbrakk> v \<in> vertices ; pre_dfss v e\<rbrakk> \<Longrightarrow> dfs_dfss_dom(Inr(v, e))"
[PROOF STATE]
proof (prove)
using this:
(case ?args8 of Inl (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfs v e | Inr (v, e) \<Rightarrow> v \<in> vertices \<and> pre_dfss v e) \<longrightarrow> dfs_dfss_dom ?args8

goal (1 subgoal):
 1. \<lbrakk>v \<in> vertices; pre_dfss v e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>v \<in> vertices; pre_dfss v e\<rbrakk> \<Longrightarrow> dfs_dfss_dom (Inr (v, e))

goal:
No subgoals!
[PROOF STEP]
qed