[STATEMENT]
lemma pre_dfss_explored_pre_dfss:
  fixes e v w
  defines "e'' \<equiv> e\<lparr>vsuccs := (\<lambda>x. if x=v then vsuccs e v \<union> {w} else vsuccs e x)\<rparr>"
  assumes 1: "pre_dfss v e" and 2: "w \<in> successors v" and 3: "w \<in> explored e"
  shows "pre_dfss v e''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pre_dfss v e''
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pre_dfss v e''
[PROOF STEP]
from 1
[PROOF STATE]
proof (chain)
picking this:
pre_dfss v e
[PROOF STEP]
have v: "v \<in> visited e"
[PROOF STATE]
proof (prove)
using this:
pre_dfss v e

goal (1 subgoal):
 1. v \<in> visited e
[PROOF STEP]
by (simp add: pre_dfss_def)
[PROOF STATE]
proof (state)
this:
v \<in> visited e

goal (1 subgoal):
 1. pre_dfss v e''
[PROOF STEP]
have "wf_env e''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_env e''
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wf_env e''
[PROOF STEP]
from 1
[PROOF STATE]
proof (chain)
picking this:
pre_dfss v e
[PROOF STEP]
have wf: "wf_env e"
[PROOF STATE]
proof (prove)
using this:
pre_dfss v e

goal (1 subgoal):
 1. wf_env e
[PROOF STEP]
by (simp add: pre_dfss_def)
[PROOF STATE]
proof (state)
this:
wf_env e

goal (1 subgoal):
 1. wf_env e''
[PROOF STEP]
hence "\<forall>v \<in> visited e''. reachable (root e'') v"
          "distinct (stack e'')"
          "distinct (cstack e'')"
          "\<forall>n m. n \<preceq> m in stack e'' \<longrightarrow> n \<preceq> m in cstack e''"
          "\<forall>n m. n \<preceq> m in stack e'' \<longrightarrow> reachable m n"
          "explored e'' \<subseteq> visited e''"
          "set (cstack e'') \<subseteq> visited e''"
          "\<forall>n \<in> explored e''. \<forall>m. reachable n m \<longrightarrow> m \<in> explored e''"
          "\<forall>n m. m \<in> \<S> e'' n \<longleftrightarrow> (\<S> e'' n = \<S> e'' m)"
          "\<forall>n. n \<notin> visited e'' \<longrightarrow> \<S> e'' n = {n}"
          "\<forall>n \<in> set (stack e''). \<forall> m \<in> set (stack e'').
                n \<noteq> m \<longrightarrow> \<S> e'' n \<inter> \<S> e'' m = {}"
          "\<Union> {\<S> e'' n | n. n \<in> set (stack e'')} = visited e'' - explored e''"
          "\<forall>n \<in> set (stack e''). \<forall>m \<in> \<S> e'' n.
              m \<in> set (cstack e'') \<longrightarrow> m \<preceq> n in cstack e''"
          "\<forall>n. is_subscc (\<S> e'' n)"
          "\<forall>S \<in> sccs e''. is_scc S"
          "\<Union> (sccs e'') = explored e''"
[PROOF STATE]
proof (prove)
using this:
wf_env e

goal (1 subgoal):
 1. (((\<forall>v\<in>visited e''. reachable (root e'') v &&& distinct (stack e'')) &&& distinct (cstack e'') &&& \<forall>n m. n \<preceq> m in stack e'' \<longrightarrow> n \<preceq> m in cstack e'') &&& (\<forall>n m. n \<preceq> m in stack e'' \<longrightarrow> reachable m n &&& explored e'' \<subseteq> visited e'') &&& set (cstack e'') \<subseteq> visited e'' &&& \<forall>n\<in>explored e''. \<forall>m. reachable n m \<longrightarrow> m \<in> explored e'') &&& ((\<forall>n m. (m \<in> \<S> e'' n) = (\<S> e'' n = \<S> e'' m) &&& \<forall>n. n \<notin> visited e'' \<longrightarrow> \<S> e'' n = {n}) &&& \<forall>n\<in>set (stack e''). \<forall>m\<in>set (stack e''). n \<noteq> m \<longrightarrow> \<S> e'' n \<inter> \<S> e'' m = {} &&& \<Union> {\<S> e'' n |n. n \<in> set (stack e'')} = visited e'' - explored e'') &&& (\<forall>n\<in>set (stack e''). \<forall>m\<in>\<S> e'' n. m \<in> set (cstack e'') \<longrightarrow> m \<preceq> n in cstack e'' &&& \<forall>n. is_subscc (\<S> e'' n)) &&& Ball (sccs e'') is_scc &&& \<Union> (sccs e'') = explored e''
[PROOF STEP]
by (auto simp: wf_env_def e''_def)
[PROOF STATE]
proof (state)
this:
\<forall>v\<in>visited e''. reachable (root e'') v
distinct (stack e'')
distinct (cstack e'')
\<forall>n m. n \<preceq> m in stack e'' \<longrightarrow> n \<preceq> m in cstack e''
\<forall>n m. n \<preceq> m in stack e'' \<longrightarrow> reachable m n
explored e'' \<subseteq> visited e''
set (cstack e'') \<subseteq> visited e''
\<forall>n\<in>explored e''. \<forall>m. reachable n m \<longrightarrow> m \<in> explored e''
\<forall>n m. (m \<in> \<S> e'' n) = (\<S> e'' n = \<S> e'' m)
\<forall>n. n \<notin> visited e'' \<longrightarrow> \<S> e'' n = {n}
\<forall>n\<in>set (stack e''). \<forall>m\<in>set (stack e''). n \<noteq> m \<longrightarrow> \<S> e'' n \<inter> \<S> e'' m = {}
\<Union> {\<S> e'' n |n. n \<in> set (stack e'')} = visited e'' - explored e''
\<forall>n\<in>set (stack e''). \<forall>m\<in>\<S> e'' n. m \<in> set (cstack e'') \<longrightarrow> m \<preceq> n in cstack e''
\<forall>n. is_subscc (\<S> e'' n)
Ball (sccs e'') is_scc
\<Union> (sccs e'') = explored e''

goal (1 subgoal):
 1. wf_env e''
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>v\<in>visited e''. reachable (root e'') v
distinct (stack e'')
distinct (cstack e'')
\<forall>n m. n \<preceq> m in stack e'' \<longrightarrow> n \<preceq> m in cstack e''
\<forall>n m. n \<preceq> m in stack e'' \<longrightarrow> reachable m n
explored e'' \<subseteq> visited e''
set (cstack e'') \<subseteq> visited e''
\<forall>n\<in>explored e''. \<forall>m. reachable n m \<longrightarrow> m \<in> explored e''
\<forall>n m. (m \<in> \<S> e'' n) = (\<S> e'' n = \<S> e'' m)
\<forall>n. n \<notin> visited e'' \<longrightarrow> \<S> e'' n = {n}
\<forall>n\<in>set (stack e''). \<forall>m\<in>set (stack e''). n \<noteq> m \<longrightarrow> \<S> e'' n \<inter> \<S> e'' m = {}
\<Union> {\<S> e'' n |n. n \<in> set (stack e'')} = visited e'' - explored e''
\<forall>n\<in>set (stack e''). \<forall>m\<in>\<S> e'' n. m \<in> set (cstack e'') \<longrightarrow> m \<preceq> n in cstack e''
\<forall>n. is_subscc (\<S> e'' n)
Ball (sccs e'') is_scc
\<Union> (sccs e'') = explored e''

goal (1 subgoal):
 1. wf_env e''
[PROOF STEP]
from wf 2 3
[PROOF STATE]
proof (chain)
picking this:
wf_env e
edge v w
w \<in> explored e
[PROOF STEP]
have "\<forall>v. vsuccs e'' v \<subseteq> successors v \<inter> visited e''"
[PROOF STATE]
proof (prove)
using this:
wf_env e
edge v w
w \<in> explored e

goal (1 subgoal):
 1. \<forall>v. vsuccs e'' v \<subseteq> successors v \<inter> visited e''
[PROOF STEP]
by (auto simp: wf_env_def e''_def)
[PROOF STATE]
proof (state)
this:
\<forall>v. vsuccs e'' v \<subseteq> successors v \<inter> visited e''

goal (1 subgoal):
 1. wf_env e''
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>v. vsuccs e'' v \<subseteq> successors v \<inter> visited e''

goal (1 subgoal):
 1. wf_env e''
[PROOF STEP]
from wf v
[PROOF STATE]
proof (chain)
picking this:
wf_env e
v \<in> visited e
[PROOF STEP]
have "\<forall>n. n \<notin> visited e'' \<longrightarrow> vsuccs e'' n = {}"
[PROOF STATE]
proof (prove)
using this:
wf_env e
v \<in> visited e

goal (1 subgoal):
 1. \<forall>n. n \<notin> visited e'' \<longrightarrow> vsuccs e'' n = {}
[PROOF STEP]
by (auto simp: wf_env_def e''_def)
[PROOF STATE]
proof (state)
this:
\<forall>n. n \<notin> visited e'' \<longrightarrow> vsuccs e'' n = {}

goal (1 subgoal):
 1. wf_env e''
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>n. n \<notin> visited e'' \<longrightarrow> vsuccs e'' n = {}

goal (1 subgoal):
 1. wf_env e''
[PROOF STEP]
from wf 2
[PROOF STATE]
proof (chain)
picking this:
wf_env e
edge v w
[PROOF STEP]
have "\<forall>v. v \<in> explored e'' \<longrightarrow> vsuccs e'' v = successors v"
[PROOF STATE]
proof (prove)
using this:
wf_env e
edge v w

goal (1 subgoal):
 1. \<forall>v. v \<in> explored e'' \<longrightarrow> vsuccs e'' v = successors v
[PROOF STEP]
by (auto simp: wf_env_def e''_def)
[PROOF STATE]
proof (state)
this:
\<forall>v. v \<in> explored e'' \<longrightarrow> vsuccs e'' v = successors v

goal (1 subgoal):
 1. wf_env e''
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>v. v \<in> explored e'' \<longrightarrow> vsuccs e'' v = successors v

goal (1 subgoal):
 1. wf_env e''
[PROOF STEP]
have "\<forall>x y. x \<preceq> y in stack e'' \<and> x \<noteq> y \<longrightarrow>
             (\<forall>u \<in> \<S> e'' x. \<not> reachable_avoiding u y (unvisited e'' x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x y. x \<preceq> y in stack e'' \<and> x \<noteq> y \<longrightarrow> (\<forall>u\<in>\<S> e'' x. \<not> reachable_avoiding u y (unvisited e'' x))
[PROOF STEP]
proof (clarify)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y u. \<lbrakk>u \<in> \<S> e'' x; x \<preceq> y in stack e''; x \<noteq> y; reachable_avoiding u y (unvisited e'' x)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
fix x y u
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y u. \<lbrakk>u \<in> \<S> e'' x; x \<preceq> y in stack e''; x \<noteq> y; reachable_avoiding u y (unvisited e'' x)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "x \<preceq> y in stack e''" "x \<noteq> y"
             "u \<in> \<S> e'' x"
             "reachable_avoiding u y (unvisited e'' x)"
[PROOF STATE]
proof (state)
this:
x \<preceq> y in stack e''
x \<noteq> y
u \<in> \<S> e'' x
reachable_avoiding u y (unvisited e'' x)

goal (1 subgoal):
 1. \<And>x y u. \<lbrakk>u \<in> \<S> e'' x; x \<preceq> y in stack e''; x \<noteq> y; reachable_avoiding u y (unvisited e'' x)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence prec: "x \<preceq> y in stack e" "u \<in> \<S> e x"
[PROOF STATE]
proof (prove)
using this:
x \<preceq> y in stack e''
x \<noteq> y
u \<in> \<S> e'' x
reachable_avoiding u y (unvisited e'' x)

goal (1 subgoal):
 1. x \<preceq> y in stack e &&& u \<in> \<S> e x
[PROOF STEP]
by (auto simp: e''_def)
[PROOF STATE]
proof (state)
this:
x \<preceq> y in stack e
u \<in> \<S> e x

goal (1 subgoal):
 1. \<And>x y u. \<lbrakk>u \<in> \<S> e'' x; x \<preceq> y in stack e''; x \<noteq> y; reachable_avoiding u y (unvisited e'' x)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with stack_unexplored[OF wf]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?n \<in> set (stack e); ?n \<in> explored e\<rbrakk> \<Longrightarrow> ?P
x \<preceq> y in stack e
u \<in> \<S> e x
[PROOF STEP]
have "y \<notin> explored e"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?n \<in> set (stack e); ?n \<in> explored e\<rbrakk> \<Longrightarrow> ?P
x \<preceq> y in stack e
u \<in> \<S> e x

goal (1 subgoal):
 1. y \<notin> explored e
[PROOF STEP]
by (blast dest: precedes_mem)
[PROOF STATE]
proof (state)
this:
y \<notin> explored e

goal (1 subgoal):
 1. \<And>x y u. \<lbrakk>u \<in> \<S> e'' x; x \<preceq> y in stack e''; x \<noteq> y; reachable_avoiding u y (unvisited e'' x)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "(unvisited e x = unvisited e'' x)
          \<or> (unvisited e x = unvisited e'' x \<union> {(v,w)})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unvisited e x = unvisited e'' x \<or> unvisited e x = unvisited e'' x \<union> {(v, w)}
[PROOF STEP]
by (auto simp: e''_def unvisited_def split: if_splits)
[PROOF STATE]
proof (state)
this:
unvisited e x = unvisited e'' x \<or> unvisited e x = unvisited e'' x \<union> {(v, w)}

goal (1 subgoal):
 1. \<And>x y u. \<lbrakk>u \<in> \<S> e'' x; x \<preceq> y in stack e''; x \<noteq> y; reachable_avoiding u y (unvisited e'' x)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
thus "False"
[PROOF STATE]
proof (prove)
using this:
unvisited e x = unvisited e'' x \<or> unvisited e x = unvisited e'' x \<union> {(v, w)}

goal (1 subgoal):
 1. False
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. unvisited e x = unvisited e'' x \<Longrightarrow> False
 2. unvisited e x = unvisited e'' x \<union> {(v, w)} \<Longrightarrow> False
[PROOF STEP]
assume "unvisited e x = unvisited e'' x"
[PROOF STATE]
proof (state)
this:
unvisited e x = unvisited e'' x

goal (2 subgoals):
 1. unvisited e x = unvisited e'' x \<Longrightarrow> False
 2. unvisited e x = unvisited e'' x \<union> {(v, w)} \<Longrightarrow> False
[PROOF STEP]
with prec \<open>x \<noteq> y\<close> \<open>reachable_avoiding u y (unvisited e'' x)\<close> wf
[PROOF STATE]
proof (chain)
picking this:
x \<preceq> y in stack e
u \<in> \<S> e x
x \<noteq> y
reachable_avoiding u y (unvisited e'' x)
wf_env e
unvisited e x = unvisited e'' x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<preceq> y in stack e
u \<in> \<S> e x
x \<noteq> y
reachable_avoiding u y (unvisited e'' x)
wf_env e
unvisited e x = unvisited e'' x

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding wf_env_def
[PROOF STATE]
proof (prove)
using this:
x \<preceq> y in stack e
u \<in> \<S> e x
x \<noteq> y
reachable_avoiding u y (unvisited e'' x)
(\<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
unvisited e x = unvisited e'' x

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

goal (1 subgoal):
 1. unvisited e x = unvisited e'' x \<union> {(v, w)} \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. unvisited e x = unvisited e'' x \<union> {(v, w)} \<Longrightarrow> False
[PROOF STEP]
assume "unvisited e x = unvisited e'' x \<union> {(v,w)}"
[PROOF STATE]
proof (state)
this:
unvisited e x = unvisited e'' x \<union> {(v, w)}

goal (1 subgoal):
 1. unvisited e x = unvisited e'' x \<union> {(v, w)} \<Longrightarrow> False
[PROOF STEP]
with wf \<open>reachable_avoiding u y (unvisited e'' x)\<close>
             \<open>y \<notin> explored e\<close> \<open>w \<in> explored e\<close> prec \<open>x \<noteq> y\<close>
[PROOF STATE]
proof (chain)
picking this:
wf_env e
reachable_avoiding u y (unvisited e'' x)
y \<notin> explored e
w \<in> explored e
x \<preceq> y in stack e
u \<in> \<S> e x
x \<noteq> y
unvisited e x = unvisited e'' x \<union> {(v, w)}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
wf_env e
reachable_avoiding u y (unvisited e'' x)
y \<notin> explored e
w \<in> explored e
x \<preceq> y in stack e
u \<in> \<S> e x
x \<noteq> y
unvisited e x = unvisited e'' x \<union> {(v, w)}

goal (1 subgoal):
 1. False
[PROOF STEP]
using avoiding_explored[OF wf]
[PROOF STATE]
proof (prove)
using this:
wf_env e
reachable_avoiding u y (unvisited e'' x)
y \<notin> explored e
w \<in> explored e
x \<preceq> y in stack e
u \<in> \<S> e x
x \<noteq> y
unvisited e x = unvisited e'' x \<union> {(v, w)}
\<lbrakk>reachable_avoiding ?x ?y ?E; ?y \<notin> explored e; ?w \<in> explored e\<rbrakk> \<Longrightarrow> reachable_avoiding ?x ?y (?E \<union> {(?v, ?w)})

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding wf_env_def
[PROOF STATE]
proof (prove)
using this:
(\<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
reachable_avoiding u y (unvisited e'' x)
y \<notin> explored e
w \<in> explored e
x \<preceq> y in stack e
u \<in> \<S> e x
x \<noteq> y
unvisited e x = unvisited e'' x \<union> {(v, w)}
\<lbrakk>reachable_avoiding ?x ?y ?E; ?y \<notin> explored e; ?w \<in> explored e\<rbrakk> \<Longrightarrow> reachable_avoiding ?x ?y (?E \<union> {(?v, ?w)})

goal (1 subgoal):
 1. False
[PROOF STEP]
by (metis (no_types, lifting))
[PROOF STATE]
proof (state)
this:
False

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>x y. x \<preceq> y in stack e'' \<and> x \<noteq> y \<longrightarrow> (\<forall>u\<in>\<S> e'' x. \<not> reachable_avoiding u y (unvisited e'' x))

goal (1 subgoal):
 1. wf_env e''
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>x y. x \<preceq> y in stack e'' \<and> x \<noteq> y \<longrightarrow> (\<forall>u\<in>\<S> e'' x. \<not> reachable_avoiding u y (unvisited e'' x))

goal (1 subgoal):
 1. wf_env e''
[PROOF STEP]
from wf 2
[PROOF STATE]
proof (chain)
picking this:
wf_env e
edge v w
[PROOF STEP]
have "\<forall>n \<in> visited e'' - set (cstack e''). vsuccs e'' n = successors n"
[PROOF STATE]
proof (prove)
using this:
wf_env e
edge v w

goal (1 subgoal):
 1. \<forall>n\<in>visited e'' - set (cstack e''). vsuccs e'' n = successors n
[PROOF STEP]
by (auto simp: e''_def wf_env_def)
[PROOF STATE]
proof (state)
this:
\<forall>n\<in>visited e'' - set (cstack e''). vsuccs e'' n = successors n

goal (1 subgoal):
 1. wf_env e''
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>v\<in>visited e''. reachable (root e'') v
distinct (stack e'')
distinct (cstack e'')
\<forall>n m. n \<preceq> m in stack e'' \<longrightarrow> n \<preceq> m in cstack e''
\<forall>n m. n \<preceq> m in stack e'' \<longrightarrow> reachable m n
explored e'' \<subseteq> visited e''
set (cstack e'') \<subseteq> visited e''
\<forall>n\<in>explored e''. \<forall>m. reachable n m \<longrightarrow> m \<in> explored e''
\<forall>n m. (m \<in> \<S> e'' n) = (\<S> e'' n = \<S> e'' m)
\<forall>n. n \<notin> visited e'' \<longrightarrow> \<S> e'' n = {n}
\<forall>n\<in>set (stack e''). \<forall>m\<in>set (stack e''). n \<noteq> m \<longrightarrow> \<S> e'' n \<inter> \<S> e'' m = {}
\<Union> {\<S> e'' n |n. n \<in> set (stack e'')} = visited e'' - explored e''
\<forall>n\<in>set (stack e''). \<forall>m\<in>\<S> e'' n. m \<in> set (cstack e'') \<longrightarrow> m \<preceq> n in cstack e''
\<forall>n. is_subscc (\<S> e'' n)
Ball (sccs e'') is_scc
\<Union> (sccs e'') = explored e''
\<forall>v. vsuccs e'' v \<subseteq> successors v \<inter> visited e''
\<forall>n. n \<notin> visited e'' \<longrightarrow> vsuccs e'' n = {}
\<forall>v. v \<in> explored e'' \<longrightarrow> vsuccs e'' v = successors v
\<forall>x y. x \<preceq> y in stack e'' \<and> x \<noteq> y \<longrightarrow> (\<forall>u\<in>\<S> e'' x. \<not> reachable_avoiding u y (unvisited e'' x))
\<forall>n\<in>visited e'' - set (cstack e''). vsuccs e'' n = successors n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>v\<in>visited e''. reachable (root e'') v
distinct (stack e'')
distinct (cstack e'')
\<forall>n m. n \<preceq> m in stack e'' \<longrightarrow> n \<preceq> m in cstack e''
\<forall>n m. n \<preceq> m in stack e'' \<longrightarrow> reachable m n
explored e'' \<subseteq> visited e''
set (cstack e'') \<subseteq> visited e''
\<forall>n\<in>explored e''. \<forall>m. reachable n m \<longrightarrow> m \<in> explored e''
\<forall>n m. (m \<in> \<S> e'' n) = (\<S> e'' n = \<S> e'' m)
\<forall>n. n \<notin> visited e'' \<longrightarrow> \<S> e'' n = {n}
\<forall>n\<in>set (stack e''). \<forall>m\<in>set (stack e''). n \<noteq> m \<longrightarrow> \<S> e'' n \<inter> \<S> e'' m = {}
\<Union> {\<S> e'' n |n. n \<in> set (stack e'')} = visited e'' - explored e''
\<forall>n\<in>set (stack e''). \<forall>m\<in>\<S> e'' n. m \<in> set (cstack e'') \<longrightarrow> m \<preceq> n in cstack e''
\<forall>n. is_subscc (\<S> e'' n)
Ball (sccs e'') is_scc
\<Union> (sccs e'') = explored e''
\<forall>v. vsuccs e'' v \<subseteq> successors v \<inter> visited e''
\<forall>n. n \<notin> visited e'' \<longrightarrow> vsuccs e'' n = {}
\<forall>v. v \<in> explored e'' \<longrightarrow> vsuccs e'' v = successors v
\<forall>x y. x \<preceq> y in stack e'' \<and> x \<noteq> y \<longrightarrow> (\<forall>u\<in>\<S> e'' x. \<not> reachable_avoiding u y (unvisited e'' x))
\<forall>n\<in>visited e'' - set (cstack e''). vsuccs e'' n = successors n

goal (1 subgoal):
 1. wf_env e''
[PROOF STEP]
unfolding wf_env_def
[PROOF STATE]
proof (prove)
using this:
\<forall>v\<in>visited e''. reachable (root e'') v
distinct (stack e'')
distinct (cstack e'')
\<forall>n m. n \<preceq> m in stack e'' \<longrightarrow> n \<preceq> m in cstack e''
\<forall>n m. n \<preceq> m in stack e'' \<longrightarrow> reachable m n
explored e'' \<subseteq> visited e''
set (cstack e'') \<subseteq> visited e''
\<forall>n\<in>explored e''. \<forall>m. reachable n m \<longrightarrow> m \<in> explored e''
\<forall>n m. (m \<in> \<S> e'' n) = (\<S> e'' n = \<S> e'' m)
\<forall>n. n \<notin> visited e'' \<longrightarrow> \<S> e'' n = {n}
\<forall>n\<in>set (stack e''). \<forall>m\<in>set (stack e''). n \<noteq> m \<longrightarrow> \<S> e'' n \<inter> \<S> e'' m = {}
\<Union> {\<S> e'' n |n. n \<in> set (stack e'')} = visited e'' - explored e''
\<forall>n\<in>set (stack e''). \<forall>m\<in>\<S> e'' n. m \<in> set (cstack e'') \<longrightarrow> m \<preceq> n in cstack e''
\<forall>n. is_subscc (\<S> e'' n)
Ball (sccs e'') is_scc
\<Union> (sccs e'') = explored e''
\<forall>v. vsuccs e'' v \<subseteq> successors v \<inter> visited e''
\<forall>n. n \<notin> visited e'' \<longrightarrow> vsuccs e'' n = {}
\<forall>v. v \<in> explored e'' \<longrightarrow> vsuccs e'' v = successors v
\<forall>x y. x \<preceq> y in stack e'' \<and> x \<noteq> y \<longrightarrow> (\<forall>u\<in>\<S> e'' x. \<not> reachable_avoiding u y (unvisited e'' x))
\<forall>n\<in>visited e'' - set (cstack e''). vsuccs e'' n = successors n

goal (1 subgoal):
 1. (\<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''
[PROOF STEP]
by meson
[PROOF STATE]
proof (state)
this:
wf_env e''

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
wf_env e''

goal (1 subgoal):
 1. pre_dfss v e''
[PROOF STEP]
with 1 3
[PROOF STATE]
proof (chain)
picking this:
pre_dfss v e
w \<in> explored e
wf_env e''
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
pre_dfss v e
w \<in> explored e
wf_env e''

goal (1 subgoal):
 1. pre_dfss v e''
[PROOF STEP]
by (auto simp: pre_dfss_def e''_def)
[PROOF STATE]
proof (state)
this:
pre_dfss v e''

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pre_dfss_post_dfs_pre_dfss:
  fixes e v w
  defines "e' \<equiv> dfs w e"
  defines "e'' \<equiv> e'\<lparr>vsuccs := (\<lambda>x. if x=v then vsuccs e' v \<union> {w} else vsuccs e' x)\<rparr>"
  assumes pre: "pre_dfss v e"
      and w: "w \<in> successors v" "w \<notin> visited e"
      and post: "post_dfs w e e'"
  shows "pre_dfss v e''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pre_dfss v e''
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pre_dfss v e''
[PROOF STEP]
from pre
[PROOF STATE]
proof (chain)
picking this:
pre_dfss v e
[PROOF STEP]
have "wf_env e" "v \<in> visited e" "stack e \<noteq> []" "v \<in> \<S> e (hd (stack e))"
[PROOF STATE]
proof (prove)
using this:
pre_dfss v e

goal (1 subgoal):
 1. (wf_env e &&& v \<in> visited e) &&& stack e \<noteq> [] &&& v \<in> \<S> e (hd (stack e))
[PROOF STEP]
by (auto simp: pre_dfss_def)
[PROOF STATE]
proof (state)
this:
wf_env e
v \<in> visited e
stack e \<noteq> []
v \<in> \<S> e (hd (stack e))

goal (1 subgoal):
 1. pre_dfss v e''
[PROOF STEP]
with post
[PROOF STATE]
proof (chain)
picking this:
post_dfs w e e'
wf_env e
v \<in> visited e
stack e \<noteq> []
v \<in> \<S> e (hd (stack e))
[PROOF STEP]
have "stack e' \<noteq> []" "v \<in> \<S> e' (hd (stack e'))"
[PROOF STATE]
proof (prove)
using this:
post_dfs w e e'
wf_env e
v \<in> visited e
stack e \<noteq> []
v \<in> \<S> e (hd (stack e))

goal (1 subgoal):
 1. stack e' \<noteq> [] &&& v \<in> \<S> e' (hd (stack e'))
[PROOF STEP]
by (auto dest: dfs_S_hd_stack)
[PROOF STATE]
proof (state)
this:
stack e' \<noteq> []
v \<in> \<S> e' (hd (stack e'))

goal (1 subgoal):
 1. pre_dfss v e''
[PROOF STEP]
from post
[PROOF STATE]
proof (chain)
picking this:
post_dfs w e e'
[PROOF STEP]
have "w \<in> visited e'"
[PROOF STATE]
proof (prove)
using this:
post_dfs w e e'

goal (1 subgoal):
 1. w \<in> visited e'
[PROOF STEP]
by (simp add: post_dfs_def)
[PROOF STATE]
proof (state)
this:
w \<in> visited e'

goal (1 subgoal):
 1. pre_dfss v e''
[PROOF STEP]
have "wf_env e''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_env e''
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wf_env e''
[PROOF STEP]
from post
[PROOF STATE]
proof (chain)
picking this:
post_dfs w e e'
[PROOF STEP]
have wf': "wf_env e'"
[PROOF STATE]
proof (prove)
using this:
post_dfs w e e'

goal (1 subgoal):
 1. wf_env e'
[PROOF STEP]
by (simp add: post_dfs_def)
[PROOF STATE]
proof (state)
this:
wf_env e'

goal (1 subgoal):
 1. wf_env e''
[PROOF STEP]
hence "\<forall>n \<in> visited e''. reachable (root e'') n"
          "distinct (stack e'')"
          "distinct (cstack e'')"
          "\<forall>n m. n \<preceq> m in stack e'' \<longrightarrow> n \<preceq> m in cstack e''"
          "\<forall>n m. n \<preceq> m in stack e'' \<longrightarrow> reachable m n"
          "explored e'' \<subseteq> visited e''"
          "set (cstack e'') \<subseteq> visited e''"
          "\<forall>n \<in> explored e''. \<forall>m. reachable n m \<longrightarrow> m \<in> explored e''"
          "\<forall>n m. m \<in> \<S> e'' n \<longleftrightarrow> (\<S> e'' n = \<S> e'' m)"
          "\<forall>n. n \<notin> visited e'' \<longrightarrow> \<S> e'' n = {n}"
          "\<forall>n \<in> set (stack e''). \<forall> m \<in> set (stack e'').
              n \<noteq> m \<longrightarrow> \<S> e'' n \<inter> \<S> e'' m = {}"
          "\<Union> {\<S> e'' n | n. n \<in> set (stack e'')} = visited e'' - explored e''"
          "\<forall>n \<in> set (stack e''). \<forall> m \<in> \<S> e'' n. m \<in> set (cstack e'') \<longrightarrow> m \<preceq> n in cstack e''"
          "\<forall>n. is_subscc (\<S> e'' n)"
          "\<forall>S \<in> sccs e''. is_scc S"
          "\<Union> (sccs e'') = explored e''"
[PROOF STATE]
proof (prove)
using this:
wf_env e'

goal (1 subgoal):
 1. (((\<forall>n\<in>visited e''. reachable (root e'') n &&& distinct (stack e'')) &&& distinct (cstack e'') &&& \<forall>n m. n \<preceq> m in stack e'' \<longrightarrow> n \<preceq> m in cstack e'') &&& (\<forall>n m. n \<preceq> m in stack e'' \<longrightarrow> reachable m n &&& explored e'' \<subseteq> visited e'') &&& set (cstack e'') \<subseteq> visited e'' &&& \<forall>n\<in>explored e''. \<forall>m. reachable n m \<longrightarrow> m \<in> explored e'') &&& ((\<forall>n m. (m \<in> \<S> e'' n) = (\<S> e'' n = \<S> e'' m) &&& \<forall>n. n \<notin> visited e'' \<longrightarrow> \<S> e'' n = {n}) &&& \<forall>n\<in>set (stack e''). \<forall>m\<in>set (stack e''). n \<noteq> m \<longrightarrow> \<S> e'' n \<inter> \<S> e'' m = {} &&& \<Union> {\<S> e'' n |n. n \<in> set (stack e'')} = visited e'' - explored e'') &&& (\<forall>n\<in>set (stack e''). \<forall>m\<in>\<S> e'' n. m \<in> set (cstack e'') \<longrightarrow> m \<preceq> n in cstack e'' &&& \<forall>n. is_subscc (\<S> e'' n)) &&& Ball (sccs e'') is_scc &&& \<Union> (sccs e'') = explored e''
[PROOF STEP]
by (auto simp: wf_env_def e''_def)
[PROOF STATE]
proof (state)
this:
\<forall>n\<in>visited e''. reachable (root e'') n
distinct (stack e'')
distinct (cstack e'')
\<forall>n m. n \<preceq> m in stack e'' \<longrightarrow> n \<preceq> m in cstack e''
\<forall>n m. n \<preceq> m in stack e'' \<longrightarrow> reachable m n
explored e'' \<subseteq> visited e''
set (cstack e'') \<subseteq> visited e''
\<forall>n\<in>explored e''. \<forall>m. reachable n m \<longrightarrow> m \<in> explored e''
\<forall>n m. (m \<in> \<S> e'' n) = (\<S> e'' n = \<S> e'' m)
\<forall>n. n \<notin> visited e'' \<longrightarrow> \<S> e'' n = {n}
\<forall>n\<in>set (stack e''). \<forall>m\<in>set (stack e''). n \<noteq> m \<longrightarrow> \<S> e'' n \<inter> \<S> e'' m = {}
\<Union> {\<S> e'' n |n. n \<in> set (stack e'')} = visited e'' - explored e''
\<forall>n\<in>set (stack e''). \<forall>m\<in>\<S> e'' n. m \<in> set (cstack e'') \<longrightarrow> m \<preceq> n in cstack e''
\<forall>n. is_subscc (\<S> e'' n)
Ball (sccs e'') is_scc
\<Union> (sccs e'') = explored e''

goal (1 subgoal):
 1. wf_env e''
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>n\<in>visited e''. reachable (root e'') n
distinct (stack e'')
distinct (cstack e'')
\<forall>n m. n \<preceq> m in stack e'' \<longrightarrow> n \<preceq> m in cstack e''
\<forall>n m. n \<preceq> m in stack e'' \<longrightarrow> reachable m n
explored e'' \<subseteq> visited e''
set (cstack e'') \<subseteq> visited e''
\<forall>n\<in>explored e''. \<forall>m. reachable n m \<longrightarrow> m \<in> explored e''
\<forall>n m. (m \<in> \<S> e'' n) = (\<S> e'' n = \<S> e'' m)
\<forall>n. n \<notin> visited e'' \<longrightarrow> \<S> e'' n = {n}
\<forall>n\<in>set (stack e''). \<forall>m\<in>set (stack e''). n \<noteq> m \<longrightarrow> \<S> e'' n \<inter> \<S> e'' m = {}
\<Union> {\<S> e'' n |n. n \<in> set (stack e'')} = visited e'' - explored e''
\<forall>n\<in>set (stack e''). \<forall>m\<in>\<S> e'' n. m \<in> set (cstack e'') \<longrightarrow> m \<preceq> n in cstack e''
\<forall>n. is_subscc (\<S> e'' n)
Ball (sccs e'') is_scc
\<Union> (sccs e'') = explored e''

goal (1 subgoal):
 1. wf_env e''
[PROOF STEP]
from wf' w
[PROOF STATE]
proof (chain)
picking this:
wf_env e'
edge v w
w \<notin> visited e
[PROOF STEP]
have "\<forall>n. vsuccs e'' n \<subseteq> successors n"
[PROOF STATE]
proof (prove)
using this:
wf_env e'
edge v w
w \<notin> visited e

goal (1 subgoal):
 1. \<forall>n. vsuccs e'' n \<subseteq> successors n
[PROOF STEP]
by (auto simp: wf_env_def e''_def)
[PROOF STATE]
proof (state)
this:
\<forall>n. vsuccs e'' n \<subseteq> successors n

goal (1 subgoal):
 1. wf_env e''
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>n. vsuccs e'' n \<subseteq> successors n

goal (1 subgoal):
 1. wf_env e''
[PROOF STEP]
from wf' \<open>w \<in> visited e'\<close>
[PROOF STATE]
proof (chain)
picking this:
wf_env e'
w \<in> visited e'
[PROOF STEP]
have "\<forall>n. vsuccs e'' n \<subseteq> visited e''"
[PROOF STATE]
proof (prove)
using this:
wf_env e'
w \<in> visited e'

goal (1 subgoal):
 1. \<forall>n. vsuccs e'' n \<subseteq> visited e''
[PROOF STEP]
by (auto simp: wf_env_def e''_def)
[PROOF STATE]
proof (state)
this:
\<forall>n. vsuccs e'' n \<subseteq> visited e''

goal (1 subgoal):
 1. wf_env e''
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>n. vsuccs e'' n \<subseteq> visited e''

goal (1 subgoal):
 1. wf_env e''
[PROOF STEP]
from post \<open>v \<in> visited e\<close>
[PROOF STATE]
proof (chain)
picking this:
post_dfs w e e'
v \<in> visited e
[PROOF STEP]
have "\<forall>n. n \<notin> visited e'' \<longrightarrow> vsuccs e'' n = {}"
[PROOF STATE]
proof (prove)
using this:
post_dfs w e e'
v \<in> visited e

goal (1 subgoal):
 1. \<forall>n. n \<notin> visited e'' \<longrightarrow> vsuccs e'' n = {}
[PROOF STEP]
apply (simp add: post_dfs_def wf_env_def sub_env_def e''_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<forall>x\<in>visited e'. reachable (root e') x) \<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 \<and> vsuccs e' n \<subseteq> 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> w \<in> visited e' \<and> root e' = root e \<and> visited e \<subseteq> visited e' \<and> explored e \<subseteq> explored e' \<and> (\<forall>v. vsuccs e v \<subseteq> vsuccs e' v) \<and> (\<forall>v. \<S> e v \<subseteq> \<S> e' v) \<and> \<Union> {\<S> e v |v. v \<in> set (stack e)} \<subseteq> \<Union> {\<S> e' v |v. v \<in> set (stack e')} \<and> vsuccs e' w = successors w \<and> (\<forall>w\<in>visited e. vsuccs e' w = vsuccs e w) \<and> (\<forall>n\<in>set (stack e'). reachable n w) \<and> (\<exists>ns. stack e = ns @ stack e') \<and> (w \<in> explored e' \<and> stack e' = stack e \<and> (\<forall>n\<in>set (stack e'). \<S> e' n = \<S> e n) \<or> stack e' \<noteq> [] \<and> w \<in> \<S> e' (hd (stack e')) \<and> (\<forall>n\<in>set (tl (stack e')). \<S> e' n = \<S> e n)) \<and> cstack e' = cstack e; v \<in> visited e\<rbrakk> \<Longrightarrow> v \<in> visited e'
[PROOF STEP]
by (meson subsetD)
[PROOF STATE]
proof (state)
this:
\<forall>n. n \<notin> visited e'' \<longrightarrow> vsuccs e'' n = {}

goal (1 subgoal):
 1. wf_env e''
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>n. n \<notin> visited e'' \<longrightarrow> vsuccs e'' n = {}

goal (1 subgoal):
 1. wf_env e''
[PROOF STEP]
from wf' w
[PROOF STATE]
proof (chain)
picking this:
wf_env e'
edge v w
w \<notin> visited e
[PROOF STEP]
have "\<forall>n \<in> explored e''. vsuccs e'' n = successors n"
[PROOF STATE]
proof (prove)
using this:
wf_env e'
edge v w
w \<notin> visited e

goal (1 subgoal):
 1. \<forall>n\<in>explored e''. vsuccs e'' n = successors n
[PROOF STEP]
by (auto simp: wf_env_def e''_def)
[PROOF STATE]
proof (state)
this:
\<forall>n\<in>explored e''. vsuccs e'' n = successors n

goal (1 subgoal):
 1. wf_env e''
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>n\<in>explored e''. vsuccs e'' n = successors n

goal (1 subgoal):
 1. wf_env e''
[PROOF STEP]
have "\<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))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<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))
[PROOF STEP]
proof (clarify)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n m u. \<lbrakk>u \<in> \<S> e'' n; n \<preceq> m in stack e''; n \<noteq> m; reachable_avoiding u m (unvisited e'' n)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
fix x y u
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n m u. \<lbrakk>u \<in> \<S> e'' n; n \<preceq> m in stack e''; n \<noteq> m; reachable_avoiding u m (unvisited e'' n)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "x \<preceq> y in stack e''" "x \<noteq> y"
             "u \<in> \<S> e'' x"
             "reachable_avoiding u y (unvisited e'' x)"
[PROOF STATE]
proof (state)
this:
x \<preceq> y in stack e''
x \<noteq> y
u \<in> \<S> e'' x
reachable_avoiding u y (unvisited e'' x)

goal (1 subgoal):
 1. \<And>n m u. \<lbrakk>u \<in> \<S> e'' n; n \<preceq> m in stack e''; n \<noteq> m; reachable_avoiding u m (unvisited e'' n)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence 1: "x \<preceq> y in stack e'" "u \<in> \<S> e' x"
[PROOF STATE]
proof (prove)
using this:
x \<preceq> y in stack e''
x \<noteq> y
u \<in> \<S> e'' x
reachable_avoiding u y (unvisited e'' x)

goal (1 subgoal):
 1. x \<preceq> y in stack e' &&& u \<in> \<S> e' x
[PROOF STEP]
by (auto simp: e''_def)
[PROOF STATE]
proof (state)
this:
x \<preceq> y in stack e'
u \<in> \<S> e' x

goal (1 subgoal):
 1. \<And>n m u. \<lbrakk>u \<in> \<S> e'' n; n \<preceq> m in stack e''; n \<noteq> m; reachable_avoiding u m (unvisited e'' n)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with stack_unexplored[OF wf']
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?n \<in> set (stack e'); ?n \<in> explored e'\<rbrakk> \<Longrightarrow> ?P
x \<preceq> y in stack e'
u \<in> \<S> e' x
[PROOF STEP]
have "y \<notin> explored e'"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?n \<in> set (stack e'); ?n \<in> explored e'\<rbrakk> \<Longrightarrow> ?P
x \<preceq> y in stack e'
u \<in> \<S> e' x

goal (1 subgoal):
 1. y \<notin> explored e'
[PROOF STEP]
by (auto dest: precedes_mem)
[PROOF STATE]
proof (state)
this:
y \<notin> explored e'

goal (1 subgoal):
 1. \<And>n m u. \<lbrakk>u \<in> \<S> e'' n; n \<preceq> m in stack e''; n \<noteq> m; reachable_avoiding u m (unvisited e'' n)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "(unvisited e' x = unvisited e'' x)
          \<or> (unvisited e' x = unvisited e'' x \<union> {(v,w)})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unvisited e' x = unvisited e'' x \<or> unvisited e' x = unvisited e'' x \<union> {(v, w)}
[PROOF STEP]
by (auto simp: e''_def unvisited_def split: if_splits)
[PROOF STATE]
proof (state)
this:
unvisited e' x = unvisited e'' x \<or> unvisited e' x = unvisited e'' x \<union> {(v, w)}

goal (1 subgoal):
 1. \<And>n m u. \<lbrakk>u \<in> \<S> e'' n; n \<preceq> m in stack e''; n \<noteq> m; reachable_avoiding u m (unvisited e'' n)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
thus "False"
[PROOF STATE]
proof (prove)
using this:
unvisited e' x = unvisited e'' x \<or> unvisited e' x = unvisited e'' x \<union> {(v, w)}

goal (1 subgoal):
 1. False
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. unvisited e' x = unvisited e'' x \<Longrightarrow> False
 2. unvisited e' x = unvisited e'' x \<union> {(v, w)} \<Longrightarrow> False
[PROOF STEP]
assume "unvisited e' x = unvisited e'' x"
[PROOF STATE]
proof (state)
this:
unvisited e' x = unvisited e'' x

goal (2 subgoals):
 1. unvisited e' x = unvisited e'' x \<Longrightarrow> False
 2. unvisited e' x = unvisited e'' x \<union> {(v, w)} \<Longrightarrow> False
[PROOF STEP]
with 1 \<open>x \<noteq> y\<close> \<open>reachable_avoiding u y (unvisited e'' x)\<close> wf'
[PROOF STATE]
proof (chain)
picking this:
x \<preceq> y in stack e'
u \<in> \<S> e' x
x \<noteq> y
reachable_avoiding u y (unvisited e'' x)
wf_env e'
unvisited e' x = unvisited e'' x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<preceq> y in stack e'
u \<in> \<S> e' x
x \<noteq> y
reachable_avoiding u y (unvisited e'' x)
wf_env e'
unvisited e' x = unvisited e'' x

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding wf_env_def
[PROOF STATE]
proof (prove)
using this:
x \<preceq> y in stack e'
u \<in> \<S> e' x
x \<noteq> y
reachable_avoiding u y (unvisited e'' x)
(\<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'
unvisited e' x = unvisited e'' x

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

goal (1 subgoal):
 1. unvisited e' x = unvisited e'' x \<union> {(v, w)} \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. unvisited e' x = unvisited e'' x \<union> {(v, w)} \<Longrightarrow> False
[PROOF STEP]
assume unv: "unvisited e' x = unvisited e'' x \<union> {(v,w)}"
[PROOF STATE]
proof (state)
this:
unvisited e' x = unvisited e'' x \<union> {(v, w)}

goal (1 subgoal):
 1. unvisited e' x = unvisited e'' x \<union> {(v, w)} \<Longrightarrow> False
[PROOF STEP]
from post
[PROOF STATE]
proof (chain)
picking this:
post_dfs w e e'
[PROOF STEP]
have "w \<in> explored e'
           \<or> (w \<in> \<S> e' (hd (stack e')) \<and> (\<forall>n \<in> set (tl (stack e')). \<S> e' n = \<S> e n))"
[PROOF STATE]
proof (prove)
using this:
post_dfs w e e'

goal (1 subgoal):
 1. w \<in> explored e' \<or> w \<in> \<S> e' (hd (stack e')) \<and> (\<forall>n\<in>set (tl (stack e')). \<S> e' n = \<S> e n)
[PROOF STEP]
by (auto simp: post_dfs_def)
[PROOF STATE]
proof (state)
this:
w \<in> explored e' \<or> w \<in> \<S> e' (hd (stack e')) \<and> (\<forall>n\<in>set (tl (stack e')). \<S> e' n = \<S> e n)

goal (1 subgoal):
 1. unvisited e' x = unvisited e'' x \<union> {(v, w)} \<Longrightarrow> False
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
w \<in> explored e' \<or> w \<in> \<S> e' (hd (stack e')) \<and> (\<forall>n\<in>set (tl (stack e')). \<S> e' n = \<S> e n)

goal (1 subgoal):
 1. False
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. w \<in> explored e' \<Longrightarrow> False
 2. w \<in> \<S> e' (hd (stack e')) \<and> (\<forall>n\<in>set (tl (stack e')). \<S> e' n = \<S> e n) \<Longrightarrow> False
[PROOF STEP]
assume "w \<in> explored e'"
[PROOF STATE]
proof (state)
this:
w \<in> explored e'

goal (2 subgoals):
 1. w \<in> explored e' \<Longrightarrow> False
 2. w \<in> \<S> e' (hd (stack e')) \<and> (\<forall>n\<in>set (tl (stack e')). \<S> e' n = \<S> e n) \<Longrightarrow> False
[PROOF STEP]
with wf' unv \<open>reachable_avoiding u y (unvisited e'' x)\<close>
               \<open>y \<notin> explored e'\<close> 1 \<open>x \<noteq> y\<close>
[PROOF STATE]
proof (chain)
picking this:
wf_env e'
unvisited e' x = unvisited e'' x \<union> {(v, w)}
reachable_avoiding u y (unvisited e'' x)
y \<notin> explored e'
x \<preceq> y in stack e'
u \<in> \<S> e' x
x \<noteq> y
w \<in> explored e'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
wf_env e'
unvisited e' x = unvisited e'' x \<union> {(v, w)}
reachable_avoiding u y (unvisited e'' x)
y \<notin> explored e'
x \<preceq> y in stack e'
u \<in> \<S> e' x
x \<noteq> y
w \<in> explored e'

goal (1 subgoal):
 1. False
[PROOF STEP]
using avoiding_explored[OF wf']
[PROOF STATE]
proof (prove)
using this:
wf_env e'
unvisited e' x = unvisited e'' x \<union> {(v, w)}
reachable_avoiding u y (unvisited e'' x)
y \<notin> explored e'
x \<preceq> y in stack e'
u \<in> \<S> e' x
x \<noteq> y
w \<in> explored e'
\<lbrakk>reachable_avoiding ?x ?y ?E; ?y \<notin> explored e'; ?w \<in> explored e'\<rbrakk> \<Longrightarrow> reachable_avoiding ?x ?y (?E \<union> {(?v, ?w)})

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding wf_env_def
[PROOF STATE]
proof (prove)
using this:
(\<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'
unvisited e' x = unvisited e'' x \<union> {(v, w)}
reachable_avoiding u y (unvisited e'' x)
y \<notin> explored e'
x \<preceq> y in stack e'
u \<in> \<S> e' x
x \<noteq> y
w \<in> explored e'
\<lbrakk>reachable_avoiding ?x ?y ?E; ?y \<notin> explored e'; ?w \<in> explored e'\<rbrakk> \<Longrightarrow> reachable_avoiding ?x ?y (?E \<union> {(?v, ?w)})

goal (1 subgoal):
 1. False
[PROOF STEP]
by (metis (no_types, lifting))
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. w \<in> \<S> e' (hd (stack e')) \<and> (\<forall>n\<in>set (tl (stack e')). \<S> e' n = \<S> e n) \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. w \<in> \<S> e' (hd (stack e')) \<and> (\<forall>n\<in>set (tl (stack e')). \<S> e' n = \<S> e n) \<Longrightarrow> False
[PROOF STEP]
assume w: "w \<in> \<S> e' (hd (stack e'))
                  \<and> (\<forall>n \<in> set (tl (stack e')). \<S> e' n = \<S> e n)"
[PROOF STATE]
proof (state)
this:
w \<in> \<S> e' (hd (stack e')) \<and> (\<forall>n\<in>set (tl (stack e')). \<S> e' n = \<S> e n)

goal (1 subgoal):
 1. w \<in> \<S> e' (hd (stack e')) \<and> (\<forall>n\<in>set (tl (stack e')). \<S> e' n = \<S> e n) \<Longrightarrow> False
[PROOF STEP]
from \<open>reachable_avoiding u y (unvisited e'' x)\<close>[THEN ra_add_edge]
               unv
[PROOF STATE]
proof (chain)
picking this:
reachable_avoiding u y (unvisited e'' x \<union> {(?v, ?w)}) \<or> reachable_avoiding u ?v (unvisited e'' x \<union> {(?v, ?w)}) \<and> reachable_avoiding ?w y (unvisited e'' x \<union> {(?v, ?w)})
unvisited e' x = unvisited e'' x \<union> {(v, w)}
[PROOF STEP]
have "reachable_avoiding u y (unvisited e' x)
              \<or> reachable_avoiding w y (unvisited e' x)"
[PROOF STATE]
proof (prove)
using this:
reachable_avoiding u y (unvisited e'' x \<union> {(?v, ?w)}) \<or> reachable_avoiding u ?v (unvisited e'' x \<union> {(?v, ?w)}) \<and> reachable_avoiding ?w y (unvisited e'' x \<union> {(?v, ?w)})
unvisited e' x = unvisited e'' x \<union> {(v, w)}

goal (1 subgoal):
 1. reachable_avoiding u y (unvisited e' x) \<or> reachable_avoiding w y (unvisited e' x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
reachable_avoiding u y (unvisited e' x) \<or> reachable_avoiding w y (unvisited e' x)

goal (1 subgoal):
 1. w \<in> \<S> e' (hd (stack e')) \<and> (\<forall>n\<in>set (tl (stack e')). \<S> e' n = \<S> e n) \<Longrightarrow> False
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
reachable_avoiding u y (unvisited e' x) \<or> reachable_avoiding w y (unvisited e' x)

goal (1 subgoal):
 1. False
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. reachable_avoiding u y (unvisited e' x) \<Longrightarrow> False
 2. reachable_avoiding w y (unvisited e' x) \<Longrightarrow> False
[PROOF STEP]
assume "reachable_avoiding u y (unvisited e' x)"
[PROOF STATE]
proof (state)
this:
reachable_avoiding u y (unvisited e' x)

goal (2 subgoals):
 1. reachable_avoiding u y (unvisited e' x) \<Longrightarrow> False
 2. reachable_avoiding w y (unvisited e' x) \<Longrightarrow> False
[PROOF STEP]
with \<open>x \<preceq> y in stack e''\<close> \<open>x \<noteq> y\<close> \<open>u \<in> \<S> e'' x\<close> wf'
[PROOF STATE]
proof (chain)
picking this:
x \<preceq> y in stack e''
x \<noteq> y
u \<in> \<S> e'' x
wf_env e'
reachable_avoiding u y (unvisited e' x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<preceq> y in stack e''
x \<noteq> y
u \<in> \<S> e'' x
wf_env e'
reachable_avoiding u y (unvisited e' x)

goal (1 subgoal):
 1. False
[PROOF STEP]
by (auto simp: e''_def wf_env_def)
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. reachable_avoiding w y (unvisited e' x) \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. reachable_avoiding w y (unvisited e' x) \<Longrightarrow> False
[PROOF STEP]
assume "reachable_avoiding w y (unvisited e' x)"
[PROOF STATE]
proof (state)
this:
reachable_avoiding w y (unvisited e' x)

goal (1 subgoal):
 1. reachable_avoiding w y (unvisited e' x) \<Longrightarrow> False
[PROOF STEP]
from unv
[PROOF STATE]
proof (chain)
picking this:
unvisited e' x = unvisited e'' x \<union> {(v, w)}
[PROOF STEP]
have "v \<in> \<S> e' x"
[PROOF STATE]
proof (prove)
using this:
unvisited e' x = unvisited e'' x \<union> {(v, w)}

goal (1 subgoal):
 1. v \<in> \<S> e' x
[PROOF STEP]
by (auto simp: unvisited_def)
[PROOF STATE]
proof (state)
this:
v \<in> \<S> e' x

goal (1 subgoal):
 1. reachable_avoiding w y (unvisited e' x) \<Longrightarrow> False
[PROOF STEP]
from \<open>x \<preceq> y in stack e''\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<preceq> y in stack e''
[PROOF STEP]
have "x \<in> set (stack e')"
[PROOF STATE]
proof (prove)
using this:
x \<preceq> y in stack e''

goal (1 subgoal):
 1. x \<in> set (stack e')
[PROOF STEP]
by (simp add: e''_def precedes_mem)
[PROOF STATE]
proof (state)
this:
x \<in> set (stack e')

goal (1 subgoal):
 1. reachable_avoiding w y (unvisited e' x) \<Longrightarrow> False
[PROOF STEP]
have "x = hd (stack e')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = hd (stack e')
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<noteq> hd (stack e') \<Longrightarrow> False
[PROOF STEP]
assume "x \<noteq> hd (stack e')"
[PROOF STATE]
proof (state)
this:
x \<noteq> hd (stack e')

goal (1 subgoal):
 1. x \<noteq> hd (stack e') \<Longrightarrow> False
[PROOF STEP]
with \<open>x \<in> set (stack e')\<close> \<open>stack e' \<noteq> []\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<in> set (stack e')
stack e' \<noteq> []
x \<noteq> hd (stack e')
[PROOF STEP]
have "x \<in> set (tl (stack e'))"
[PROOF STATE]
proof (prove)
using this:
x \<in> set (stack e')
stack e' \<noteq> []
x \<noteq> hd (stack e')

goal (1 subgoal):
 1. x \<in> set (tl (stack e'))
[PROOF STEP]
by (metis hd_Cons_tl set_ConsD)
[PROOF STATE]
proof (state)
this:
x \<in> set (tl (stack e'))

goal (1 subgoal):
 1. x \<noteq> hd (stack e') \<Longrightarrow> False
[PROOF STEP]
with w \<open>v \<in> \<S> e' x\<close>
[PROOF STATE]
proof (chain)
picking this:
w \<in> \<S> e' (hd (stack e')) \<and> (\<forall>n\<in>set (tl (stack e')). \<S> e' n = \<S> e n)
v \<in> \<S> e' x
x \<in> set (tl (stack e'))
[PROOF STEP]
have "v \<in> \<S> e x"
[PROOF STATE]
proof (prove)
using this:
w \<in> \<S> e' (hd (stack e')) \<and> (\<forall>n\<in>set (tl (stack e')). \<S> e' n = \<S> e n)
v \<in> \<S> e' x
x \<in> set (tl (stack e'))

goal (1 subgoal):
 1. v \<in> \<S> e x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v \<in> \<S> e x

goal (1 subgoal):
 1. x \<noteq> hd (stack e') \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
v \<in> \<S> e x

goal (1 subgoal):
 1. x \<noteq> hd (stack e') \<Longrightarrow> False
[PROOF STEP]
from post \<open>stack e' \<noteq> []\<close> \<open>x \<in> set (stack e')\<close> \<open>x \<in> set (tl (stack e'))\<close>
[PROOF STATE]
proof (chain)
picking this:
post_dfs w e e'
stack e' \<noteq> []
x \<in> set (stack e')
x \<in> set (tl (stack e'))
[PROOF STEP]
have "x \<in> set (tl (stack e))"
[PROOF STATE]
proof (prove)
using this:
post_dfs w e e'
stack e' \<noteq> []
x \<in> set (stack e')
x \<in> set (tl (stack e'))

goal (1 subgoal):
 1. x \<in> set (tl (stack e))
[PROOF STEP]
unfolding post_dfs_def
[PROOF STATE]
proof (prove)
using this:
wf_env e' \<and> w \<in> visited e' \<and> sub_env e e' \<and> vsuccs e' w = successors w \<and> (\<forall>w\<in>visited e. vsuccs e' w = vsuccs e w) \<and> (\<forall>n\<in>set (stack e'). reachable n w) \<and> (\<exists>ns. stack e = ns @ stack e') \<and> (w \<in> explored e' \<and> stack e' = stack e \<and> (\<forall>n\<in>set (stack e'). \<S> e' n = \<S> e n) \<or> stack e' \<noteq> [] \<and> w \<in> \<S> e' (hd (stack e')) \<and> (\<forall>n\<in>set (tl (stack e')). \<S> e' n = \<S> e n)) \<and> cstack e' = cstack e
stack e' \<noteq> []
x \<in> set (stack e')
x \<in> set (tl (stack e'))

goal (1 subgoal):
 1. x \<in> set (tl (stack e))
[PROOF STEP]
by (metis Un_iff self_append_conv2 set_append tl_append2)
[PROOF STATE]
proof (state)
this:
x \<in> set (tl (stack e))

goal (1 subgoal):
 1. x \<noteq> hd (stack e') \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<in> set (tl (stack e))

goal (1 subgoal):
 1. x \<noteq> hd (stack e') \<Longrightarrow> False
[PROOF STEP]
from pre
[PROOF STATE]
proof (chain)
picking this:
pre_dfss v e
[PROOF STEP]
have "wf_env e" "stack e \<noteq> []" "v \<in> \<S> e (hd (stack e))"
[PROOF STATE]
proof (prove)
using this:
pre_dfss v e

goal (1 subgoal):
 1. wf_env e &&& stack e \<noteq> [] &&& v \<in> \<S> e (hd (stack e))
[PROOF STEP]
by (auto simp: pre_dfss_def)
[PROOF STATE]
proof (state)
this:
wf_env e
stack e \<noteq> []
v \<in> \<S> e (hd (stack e))

goal (1 subgoal):
 1. x \<noteq> hd (stack e') \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
v \<in> \<S> e x
x \<in> set (tl (stack e))
wf_env e
stack e \<noteq> []
v \<in> \<S> e (hd (stack e))
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
v \<in> \<S> e x
x \<in> set (tl (stack e))
wf_env e
stack e \<noteq> []
v \<in> \<S> e (hd (stack e))

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding wf_env_def
[PROOF STATE]
proof (prove)
using this:
v \<in> \<S> e x
x \<in> set (tl (stack e))
(\<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
stack e \<noteq> []
v \<in> \<S> e (hd (stack e))

goal (1 subgoal):
 1. False
[PROOF STEP]
by (metis (no_types, lifting) distinct.simps(2) hd_Cons_tl insert_disjoint(2)
                          list.set_sel(1) list.set_sel(2) mk_disjoint_insert)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x = hd (stack e')

goal (1 subgoal):
 1. reachable_avoiding w y (unvisited e' x) \<Longrightarrow> False
[PROOF STEP]
with \<open>reachable_avoiding w y (unvisited e' x)\<close>
                 \<open>x \<preceq> y in stack e''\<close> \<open>x \<noteq> y\<close> w wf'
[PROOF STATE]
proof (chain)
picking this:
reachable_avoiding w y (unvisited e' x)
x \<preceq> y in stack e''
x \<noteq> y
w \<in> \<S> e' (hd (stack e')) \<and> (\<forall>n\<in>set (tl (stack e')). \<S> e' n = \<S> e n)
wf_env e'
x = hd (stack e')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
reachable_avoiding w y (unvisited e' x)
x \<preceq> y in stack e''
x \<noteq> y
w \<in> \<S> e' (hd (stack e')) \<and> (\<forall>n\<in>set (tl (stack e')). \<S> e' n = \<S> e n)
wf_env e'
x = hd (stack e')

goal (1 subgoal):
 1. False
[PROOF STEP]
by (auto simp add: e''_def wf_env_def)
[PROOF STATE]
proof (state)
this:
False

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<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))

goal (1 subgoal):
 1. wf_env e''
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<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))

goal (1 subgoal):
 1. wf_env e''
[PROOF STEP]
from wf' \<open>\<forall>n. vsuccs e'' n \<subseteq> successors n\<close>
[PROOF STATE]
proof (chain)
picking this:
wf_env e'
\<forall>n. vsuccs e'' n \<subseteq> successors n
[PROOF STEP]
have "\<forall>n \<in> visited e'' - set (cstack e''). vsuccs e'' n = successors n"
[PROOF STATE]
proof (prove)
using this:
wf_env e'
\<forall>n. vsuccs e'' n \<subseteq> successors n

goal (1 subgoal):
 1. \<forall>n\<in>visited e'' - set (cstack e''). vsuccs e'' n = successors n
[PROOF STEP]
by (auto simp: wf_env_def e''_def split: if_splits)
[PROOF STATE]
proof (state)
this:
\<forall>n\<in>visited e'' - set (cstack e''). vsuccs e'' n = successors n

goal (1 subgoal):
 1. wf_env e''
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>n\<in>visited e''. reachable (root e'') n
distinct (stack e'')
distinct (cstack e'')
\<forall>n m. n \<preceq> m in stack e'' \<longrightarrow> n \<preceq> m in cstack e''
\<forall>n m. n \<preceq> m in stack e'' \<longrightarrow> reachable m n
explored e'' \<subseteq> visited e''
set (cstack e'') \<subseteq> visited e''
\<forall>n\<in>explored e''. \<forall>m. reachable n m \<longrightarrow> m \<in> explored e''
\<forall>n m. (m \<in> \<S> e'' n) = (\<S> e'' n = \<S> e'' m)
\<forall>n. n \<notin> visited e'' \<longrightarrow> \<S> e'' n = {n}
\<forall>n\<in>set (stack e''). \<forall>m\<in>set (stack e''). n \<noteq> m \<longrightarrow> \<S> e'' n \<inter> \<S> e'' m = {}
\<Union> {\<S> e'' n |n. n \<in> set (stack e'')} = visited e'' - explored e''
\<forall>n\<in>set (stack e''). \<forall>m\<in>\<S> e'' n. m \<in> set (cstack e'') \<longrightarrow> m \<preceq> n in cstack e''
\<forall>n. is_subscc (\<S> e'' n)
Ball (sccs e'') is_scc
\<Union> (sccs e'') = explored e''
\<forall>n. vsuccs e'' n \<subseteq> successors n
\<forall>n. vsuccs e'' n \<subseteq> visited e''
\<forall>n. n \<notin> visited e'' \<longrightarrow> vsuccs e'' n = {}
\<forall>n\<in>explored e''. vsuccs e'' n = successors n
\<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))
\<forall>n\<in>visited e'' - set (cstack e''). vsuccs e'' n = successors n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>n\<in>visited e''. reachable (root e'') n
distinct (stack e'')
distinct (cstack e'')
\<forall>n m. n \<preceq> m in stack e'' \<longrightarrow> n \<preceq> m in cstack e''
\<forall>n m. n \<preceq> m in stack e'' \<longrightarrow> reachable m n
explored e'' \<subseteq> visited e''
set (cstack e'') \<subseteq> visited e''
\<forall>n\<in>explored e''. \<forall>m. reachable n m \<longrightarrow> m \<in> explored e''
\<forall>n m. (m \<in> \<S> e'' n) = (\<S> e'' n = \<S> e'' m)
\<forall>n. n \<notin> visited e'' \<longrightarrow> \<S> e'' n = {n}
\<forall>n\<in>set (stack e''). \<forall>m\<in>set (stack e''). n \<noteq> m \<longrightarrow> \<S> e'' n \<inter> \<S> e'' m = {}
\<Union> {\<S> e'' n |n. n \<in> set (stack e'')} = visited e'' - explored e''
\<forall>n\<in>set (stack e''). \<forall>m\<in>\<S> e'' n. m \<in> set (cstack e'') \<longrightarrow> m \<preceq> n in cstack e''
\<forall>n. is_subscc (\<S> e'' n)
Ball (sccs e'') is_scc
\<Union> (sccs e'') = explored e''
\<forall>n. vsuccs e'' n \<subseteq> successors n
\<forall>n. vsuccs e'' n \<subseteq> visited e''
\<forall>n. n \<notin> visited e'' \<longrightarrow> vsuccs e'' n = {}
\<forall>n\<in>explored e''. vsuccs e'' n = successors n
\<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))
\<forall>n\<in>visited e'' - set (cstack e''). vsuccs e'' n = successors n

goal (1 subgoal):
 1. wf_env e''
[PROOF STEP]
unfolding wf_env_def
[PROOF STATE]
proof (prove)
using this:
\<forall>n\<in>visited e''. reachable (root e'') n
distinct (stack e'')
distinct (cstack e'')
\<forall>n m. n \<preceq> m in stack e'' \<longrightarrow> n \<preceq> m in cstack e''
\<forall>n m. n \<preceq> m in stack e'' \<longrightarrow> reachable m n
explored e'' \<subseteq> visited e''
set (cstack e'') \<subseteq> visited e''
\<forall>n\<in>explored e''. \<forall>m. reachable n m \<longrightarrow> m \<in> explored e''
\<forall>n m. (m \<in> \<S> e'' n) = (\<S> e'' n = \<S> e'' m)
\<forall>n. n \<notin> visited e'' \<longrightarrow> \<S> e'' n = {n}
\<forall>n\<in>set (stack e''). \<forall>m\<in>set (stack e''). n \<noteq> m \<longrightarrow> \<S> e'' n \<inter> \<S> e'' m = {}
\<Union> {\<S> e'' n |n. n \<in> set (stack e'')} = visited e'' - explored e''
\<forall>n\<in>set (stack e''). \<forall>m\<in>\<S> e'' n. m \<in> set (cstack e'') \<longrightarrow> m \<preceq> n in cstack e''
\<forall>n. is_subscc (\<S> e'' n)
Ball (sccs e'') is_scc
\<Union> (sccs e'') = explored e''
\<forall>n. vsuccs e'' n \<subseteq> successors n
\<forall>n. vsuccs e'' n \<subseteq> visited e''
\<forall>n. n \<notin> visited e'' \<longrightarrow> vsuccs e'' n = {}
\<forall>n\<in>explored e''. vsuccs e'' n = successors n
\<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))
\<forall>n\<in>visited e'' - set (cstack e''). vsuccs e'' n = successors n

goal (1 subgoal):
 1. (\<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''
[PROOF STEP]
by (meson le_inf_iff)
[PROOF STATE]
proof (state)
this:
wf_env e''

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
wf_env e''

goal (1 subgoal):
 1. pre_dfss v e''
[PROOF STEP]
show "pre_dfss v e''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pre_dfss v e''
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pre_dfss v e''
[PROOF STEP]
from pre post
[PROOF STATE]
proof (chain)
picking this:
pre_dfss v e
post_dfs w e e'
[PROOF STEP]
have "v \<in> visited e''"
[PROOF STATE]
proof (prove)
using this:
pre_dfss v e
post_dfs w e e'

goal (1 subgoal):
 1. v \<in> visited e''
[PROOF STEP]
by (auto simp: pre_dfss_def post_dfs_def sub_env_def e''_def)
[PROOF STATE]
proof (state)
this:
v \<in> visited e''

goal (1 subgoal):
 1. pre_dfss v e''
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
v \<in> visited e''

goal (1 subgoal):
 1. pre_dfss v e''
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
v \<in> visited e''

goal (1 subgoal):
 1. pre_dfss v e''
[PROOF STEP]
fix u
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pre_dfss v e''
[PROOF STEP]
assume u: "u \<in> vsuccs e'' v"
[PROOF STATE]
proof (state)
this:
u \<in> vsuccs e'' v

goal (1 subgoal):
 1. pre_dfss v e''
[PROOF STEP]
have "u \<in> explored e'' \<union> \<S> e'' (hd (stack e''))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<in> explored e'' \<union> \<S> e'' (hd (stack e''))
[PROOF STEP]
proof (cases "u = w")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. u = w \<Longrightarrow> u \<in> explored e'' \<union> \<S> e'' (hd (stack e''))
 2. u \<noteq> w \<Longrightarrow> u \<in> explored e'' \<union> \<S> e'' (hd (stack e''))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
u = w

goal (2 subgoals):
 1. u = w \<Longrightarrow> u \<in> explored e'' \<union> \<S> e'' (hd (stack e''))
 2. u \<noteq> w \<Longrightarrow> u \<in> explored e'' \<union> \<S> e'' (hd (stack e''))
[PROOF STEP]
with post
[PROOF STATE]
proof (chain)
picking this:
post_dfs w e e'
u = w
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
post_dfs w e e'
u = w

goal (1 subgoal):
 1. u \<in> explored e'' \<union> \<S> e'' (hd (stack e''))
[PROOF STEP]
by (auto simp: post_dfs_def e''_def)
[PROOF STATE]
proof (state)
this:
u \<in> explored e'' \<union> \<S> e'' (hd (stack e''))

goal (1 subgoal):
 1. u \<noteq> w \<Longrightarrow> u \<in> explored e'' \<union> \<S> e'' (hd (stack e''))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. u \<noteq> w \<Longrightarrow> u \<in> explored e'' \<union> \<S> e'' (hd (stack e''))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
u \<noteq> w

goal (1 subgoal):
 1. u \<noteq> w \<Longrightarrow> u \<in> explored e'' \<union> \<S> e'' (hd (stack e''))
[PROOF STEP]
with u pre post
[PROOF STATE]
proof (chain)
picking this:
u \<in> vsuccs e'' v
pre_dfss v e
post_dfs w e e'
u \<noteq> w
[PROOF STEP]
have "u \<in> explored e \<union> \<S> e (hd (stack e))"
[PROOF STATE]
proof (prove)
using this:
u \<in> vsuccs e'' v
pre_dfss v e
post_dfs w e e'
u \<noteq> w

goal (1 subgoal):
 1. u \<in> explored e \<union> \<S> e (hd (stack e))
[PROOF STEP]
by (auto simp: pre_dfss_def post_dfs_def e''_def)
[PROOF STATE]
proof (state)
this:
u \<in> explored e \<union> \<S> e (hd (stack e))

goal (1 subgoal):
 1. u \<noteq> w \<Longrightarrow> u \<in> explored e'' \<union> \<S> e'' (hd (stack e''))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
u \<in> explored e \<union> \<S> e (hd (stack e))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
u \<in> explored e \<union> \<S> e (hd (stack e))

goal (1 subgoal):
 1. u \<in> explored e'' \<union> \<S> e'' (hd (stack e''))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. u \<in> explored e \<Longrightarrow> u \<in> explored e'' \<union> \<S> e'' (hd (stack e''))
 2. u \<in> \<S> e (hd (stack e)) \<Longrightarrow> u \<in> explored e'' \<union> \<S> e'' (hd (stack e''))
[PROOF STEP]
assume "u \<in> explored e"
[PROOF STATE]
proof (state)
this:
u \<in> explored e

goal (2 subgoals):
 1. u \<in> explored e \<Longrightarrow> u \<in> explored e'' \<union> \<S> e'' (hd (stack e''))
 2. u \<in> \<S> e (hd (stack e)) \<Longrightarrow> u \<in> explored e'' \<union> \<S> e'' (hd (stack e''))
[PROOF STEP]
with post
[PROOF STATE]
proof (chain)
picking this:
post_dfs w e e'
u \<in> explored e
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
post_dfs w e e'
u \<in> explored e

goal (1 subgoal):
 1. u \<in> explored e'' \<union> \<S> e'' (hd (stack e''))
[PROOF STEP]
by (auto simp: post_dfs_def sub_env_def e''_def)
[PROOF STATE]
proof (state)
this:
u \<in> explored e'' \<union> \<S> e'' (hd (stack e''))

goal (1 subgoal):
 1. u \<in> \<S> e (hd (stack e)) \<Longrightarrow> u \<in> explored e'' \<union> \<S> e'' (hd (stack e''))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. u \<in> \<S> e (hd (stack e)) \<Longrightarrow> u \<in> explored e'' \<union> \<S> e'' (hd (stack e''))
[PROOF STEP]
assume "u \<in> \<S> e (hd (stack e))"
[PROOF STATE]
proof (state)
this:
u \<in> \<S> e (hd (stack e))

goal (1 subgoal):
 1. u \<in> \<S> e (hd (stack e)) \<Longrightarrow> u \<in> explored e'' \<union> \<S> e'' (hd (stack e''))
[PROOF STEP]
with \<open>wf_env e\<close> post \<open>stack e \<noteq> []\<close>
[PROOF STATE]
proof (chain)
picking this:
wf_env e
post_dfs w e e'
stack e \<noteq> []
u \<in> \<S> e (hd (stack e))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
wf_env e
post_dfs w e e'
stack e \<noteq> []
u \<in> \<S> e (hd (stack e))

goal (1 subgoal):
 1. u \<in> explored e'' \<union> \<S> e'' (hd (stack e''))
[PROOF STEP]
by (auto simp: e''_def dest: dfs_S_hd_stack)
[PROOF STATE]
proof (state)
this:
u \<in> explored e'' \<union> \<S> e'' (hd (stack e''))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
u \<in> explored e'' \<union> \<S> e'' (hd (stack e''))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
u \<in> explored e'' \<union> \<S> e'' (hd (stack e''))

goal (1 subgoal):
 1. pre_dfss v e''
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?u8 \<in> vsuccs e'' v \<Longrightarrow> ?u8 \<in> explored e'' \<union> \<S> e'' (hd (stack e''))

goal (1 subgoal):
 1. pre_dfss v e''
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?u8 \<in> vsuccs e'' v \<Longrightarrow> ?u8 \<in> explored e'' \<union> \<S> e'' (hd (stack e''))

goal (1 subgoal):
 1. pre_dfss v e''
[PROOF STEP]
from pre post
[PROOF STATE]
proof (chain)
picking this:
pre_dfss v e
post_dfs w e e'
[PROOF STEP]
have "\<forall>n \<in> set (stack e''). reachable n v"
[PROOF STATE]
proof (prove)
using this:
pre_dfss v e
post_dfs w e e'

goal (1 subgoal):
 1. \<forall>n\<in>set (stack e''). reachable n v
[PROOF STEP]
unfolding pre_dfss_def post_dfs_def
[PROOF STATE]
proof (prove)
using this:
wf_env 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)
wf_env e' \<and> w \<in> visited e' \<and> sub_env e e' \<and> vsuccs e' w = successors w \<and> (\<forall>w\<in>visited e. vsuccs e' w = vsuccs e w) \<and> (\<forall>n\<in>set (stack e'). reachable n w) \<and> (\<exists>ns. stack e = ns @ stack e') \<and> (w \<in> explored e' \<and> stack e' = stack e \<and> (\<forall>n\<in>set (stack e'). \<S> e' n = \<S> e n) \<or> stack e' \<noteq> [] \<and> w \<in> \<S> e' (hd (stack e')) \<and> (\<forall>n\<in>set (tl (stack e')). \<S> e' n = \<S> e n)) \<and> cstack e' = cstack e

goal (1 subgoal):
 1. \<forall>n\<in>set (stack e''). reachable n v
[PROOF STEP]
using e''_def
[PROOF STATE]
proof (prove)
using this:
wf_env 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)
wf_env e' \<and> w \<in> visited e' \<and> sub_env e e' \<and> vsuccs e' w = successors w \<and> (\<forall>w\<in>visited e. vsuccs e' w = vsuccs e w) \<and> (\<forall>n\<in>set (stack e'). reachable n w) \<and> (\<exists>ns. stack e = ns @ stack e') \<and> (w \<in> explored e' \<and> stack e' = stack e \<and> (\<forall>n\<in>set (stack e'). \<S> e' n = \<S> e n) \<or> stack e' \<noteq> [] \<and> w \<in> \<S> e' (hd (stack e')) \<and> (\<forall>n\<in>set (tl (stack e')). \<S> e' n = \<S> e n)) \<and> cstack e' = cstack e
e'' \<equiv> e'\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e' v \<union> {w} else vsuccs e' x\<rparr>

goal (1 subgoal):
 1. \<forall>n\<in>set (stack e''). reachable n v
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<forall>n\<in>set (stack e''). reachable n v

goal (1 subgoal):
 1. pre_dfss v e''
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>n\<in>set (stack e''). reachable n v

goal (1 subgoal):
 1. pre_dfss v e''
[PROOF STEP]
from \<open>stack e' \<noteq> []\<close>
[PROOF STATE]
proof (chain)
picking this:
stack e' \<noteq> []
[PROOF STEP]
have "stack e'' \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
stack e' \<noteq> []

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

goal (1 subgoal):
 1. pre_dfss v e''
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
stack e'' \<noteq> []

goal (1 subgoal):
 1. pre_dfss v e''
[PROOF STEP]
from \<open>v \<in> \<S> e' (hd (stack e'))\<close>
[PROOF STATE]
proof (chain)
picking this:
v \<in> \<S> e' (hd (stack e'))
[PROOF STEP]
have "v \<in> \<S> e'' (hd (stack e''))"
[PROOF STATE]
proof (prove)
using this:
v \<in> \<S> e' (hd (stack e'))

goal (1 subgoal):
 1. v \<in> \<S> e'' (hd (stack e''))
[PROOF STEP]
by (simp add: e''_def)
[PROOF STATE]
proof (state)
this:
v \<in> \<S> e'' (hd (stack e''))

goal (1 subgoal):
 1. pre_dfss v e''
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
v \<in> \<S> e'' (hd (stack e''))

goal (1 subgoal):
 1. pre_dfss v e''
[PROOF STEP]
from pre post
[PROOF STATE]
proof (chain)
picking this:
pre_dfss v e
post_dfs w e e'
[PROOF STEP]
have "\<exists>ns. cstack e'' = v # ns"
[PROOF STATE]
proof (prove)
using this:
pre_dfss v e
post_dfs w e e'

goal (1 subgoal):
 1. \<exists>ns. cstack e'' = v # ns
[PROOF STEP]
by (auto simp: pre_dfss_def post_dfs_def e''_def)
[PROOF STATE]
proof (state)
this:
\<exists>ns. cstack e'' = v # ns

goal (1 subgoal):
 1. pre_dfss v e''
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
v \<in> visited e''
?u8 \<in> vsuccs e'' v \<Longrightarrow> ?u8 \<in> explored e'' \<union> \<S> e'' (hd (stack e''))
\<forall>n\<in>set (stack e''). reachable n v
stack e'' \<noteq> []
v \<in> \<S> e'' (hd (stack e''))
\<exists>ns. cstack e'' = v # ns
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
v \<in> visited e''
?u8 \<in> vsuccs e'' v \<Longrightarrow> ?u8 \<in> explored e'' \<union> \<S> e'' (hd (stack e''))
\<forall>n\<in>set (stack e''). reachable n v
stack e'' \<noteq> []
v \<in> \<S> e'' (hd (stack e''))
\<exists>ns. cstack e'' = v # ns

goal (1 subgoal):
 1. pre_dfss v e''
[PROOF STEP]
using \<open>wf_env e''\<close>
[PROOF STATE]
proof (prove)
using this:
v \<in> visited e''
?u8 \<in> vsuccs e'' v \<Longrightarrow> ?u8 \<in> explored e'' \<union> \<S> e'' (hd (stack e''))
\<forall>n\<in>set (stack e''). reachable n v
stack e'' \<noteq> []
v \<in> \<S> e'' (hd (stack e''))
\<exists>ns. cstack e'' = v # ns
wf_env e''

goal (1 subgoal):
 1. pre_dfss v e''
[PROOF STEP]
unfolding pre_dfss_def
[PROOF STATE]
proof (prove)
using this:
v \<in> visited e''
?u8 \<in> vsuccs e'' v \<Longrightarrow> ?u8 \<in> explored e'' \<union> \<S> e'' (hd (stack e''))
\<forall>n\<in>set (stack e''). reachable n v
stack e'' \<noteq> []
v \<in> \<S> e'' (hd (stack e''))
\<exists>ns. cstack e'' = v # ns
wf_env e''

goal (1 subgoal):
 1. wf_env 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)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
pre_dfss v e''

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
pre_dfss v e''

goal:
No subgoals!
[PROOF STEP]
qed