[STATEMENT]
lemma pre_dfs_pre_dfss:
  assumes "pre_dfs v e"
  shows "pre_dfss v (e\<lparr>visited := visited e \<union> {v},
                       stack := v # stack e,
                       cstack := v # cstack e\<rparr>)"
        (is "pre_dfss v ?e'")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pre_dfss v (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pre_dfss v (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
pre_dfs v e
[PROOF STEP]
have wf: "wf_env e"
[PROOF STATE]
proof (prove)
using this:
pre_dfs v e

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

goal (1 subgoal):
 1. pre_dfss v (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
pre_dfs v e
[PROOF STEP]
have v: "v \<notin> visited e"
[PROOF STATE]
proof (prove)
using this:
pre_dfs v e

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

goal (1 subgoal):
 1. pre_dfss v (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)
[PROOF STEP]
from assms stack_visited[OF wf]
[PROOF STATE]
proof (chain)
picking this:
pre_dfs v e
?n \<in> set (stack e) \<Longrightarrow> ?n \<in> visited e
[PROOF STEP]
have "\<forall>n \<in> visited ?e'. reachable (root ?e') n"
       "distinct (stack ?e')"
       "distinct (cstack ?e')"
       "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. vsuccs ?e' n \<subseteq> successors n"
       "\<forall>n \<in> explored ?e'. vsuccs ?e' n = successors n"
       "\<forall>n \<in> visited ?e' - set(cstack ?e'). vsuccs ?e' n = successors n"
       "\<forall>n. n \<notin> visited ?e' \<longrightarrow> vsuccs ?e' n = {}"
       "(\<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. is_subscc (\<S> ?e' n)"
       "\<forall>S \<in> sccs ?e'. is_scc S"
       "\<Union> (sccs ?e') = explored ?e'"
[PROOF STATE]
proof (prove)
using this:
pre_dfs v e
?n \<in> set (stack e) \<Longrightarrow> ?n \<in> visited e

goal (1 subgoal):
 1. ((\<forall>n\<in>visited (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>). reachable (root (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)) n &&& distinct (stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)) &&& distinct (cstack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>))) &&& (explored (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) \<subseteq> visited (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) &&& set (cstack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)) \<subseteq> visited (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)) &&& \<forall>n\<in>explored (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>). \<forall>m. reachable n m \<longrightarrow> m \<in> explored (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) &&& \<forall>n. vsuccs (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) n \<subseteq> successors n) &&& ((\<forall>n\<in>explored (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>). vsuccs (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) n = successors n &&& \<forall>n\<in>visited (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) - set (cstack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)). vsuccs (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) n = successors n) &&& \<forall>n. n \<notin> visited (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) \<longrightarrow> vsuccs (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) n = {} &&& \<forall>n m. (m \<in> \<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) n) = (\<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) n = \<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) m)) &&& (\<forall>n. n \<notin> visited (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) \<longrightarrow> \<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) n = {n} &&& \<forall>n. is_subscc (\<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) n)) &&& Ball (sccs (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)) is_scc &&& \<Union> (sccs (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)) = explored (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)
[PROOF STEP]
by (auto simp: pre_dfs_def wf_env_def)
[PROOF STATE]
proof (state)
this:
\<forall>n\<in>visited (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>). reachable (root (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)) n
distinct (stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>))
distinct (cstack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>))
explored (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) \<subseteq> visited (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)
set (cstack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)) \<subseteq> visited (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)
\<forall>n\<in>explored (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>). \<forall>m. reachable n m \<longrightarrow> m \<in> explored (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)
\<forall>n. vsuccs (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) n \<subseteq> successors n
\<forall>n\<in>explored (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>). vsuccs (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) n = successors n
\<forall>n\<in>visited (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) - set (cstack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)). vsuccs (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) n = successors n
\<forall>n. n \<notin> visited (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) \<longrightarrow> vsuccs (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) n = {}
\<forall>n m. (m \<in> \<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) n) = (\<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) n = \<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) m)
\<forall>n. n \<notin> visited (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) \<longrightarrow> \<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) n = {n}
\<forall>n. is_subscc (\<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) n)
Ball (sccs (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)) is_scc
\<Union> (sccs (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)) = explored (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)

goal (1 subgoal):
 1. pre_dfss v (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>n\<in>visited (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>). reachable (root (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)) n
distinct (stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>))
distinct (cstack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>))
explored (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) \<subseteq> visited (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)
set (cstack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)) \<subseteq> visited (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)
\<forall>n\<in>explored (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>). \<forall>m. reachable n m \<longrightarrow> m \<in> explored (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)
\<forall>n. vsuccs (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) n \<subseteq> successors n
\<forall>n\<in>explored (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>). vsuccs (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) n = successors n
\<forall>n\<in>visited (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) - set (cstack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)). vsuccs (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) n = successors n
\<forall>n. n \<notin> visited (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) \<longrightarrow> vsuccs (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) n = {}
\<forall>n m. (m \<in> \<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) n) = (\<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) n = \<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) m)
\<forall>n. n \<notin> visited (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) \<longrightarrow> \<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) n = {n}
\<forall>n. is_subscc (\<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) n)
Ball (sccs (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)) is_scc
\<Union> (sccs (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)) = explored (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)

goal (1 subgoal):
 1. pre_dfss v (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)
[PROOF STEP]
have "\<forall>n m. n \<preceq> m in stack ?e' \<longrightarrow> reachable m n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n m. n \<preceq> m in stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) \<longrightarrow> reachable m n
[PROOF STEP]
proof (clarify)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n m. n \<preceq> m in stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) \<Longrightarrow> reachable m n
[PROOF STEP]
fix x y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n m. n \<preceq> m in stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) \<Longrightarrow> reachable m n
[PROOF STEP]
assume "x \<preceq> y in stack ?e'"
[PROOF STATE]
proof (state)
this:
x \<preceq> y in stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)

goal (1 subgoal):
 1. \<And>n m. n \<preceq> m in stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) \<Longrightarrow> reachable m n
[PROOF STEP]
show "reachable y x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reachable y x
[PROOF STEP]
proof (cases "x=v")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = v \<Longrightarrow> reachable y x
 2. x \<noteq> v \<Longrightarrow> reachable y x
[PROOF STEP]
assume "x=v"
[PROOF STATE]
proof (state)
this:
x = v

goal (2 subgoals):
 1. x = v \<Longrightarrow> reachable y x
 2. x \<noteq> v \<Longrightarrow> reachable y x
[PROOF STEP]
with \<open>x \<preceq> y in stack ?e'\<close> assms
[PROOF STATE]
proof (chain)
picking this:
x \<preceq> y in stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)
pre_dfs v e
x = v
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<preceq> y in stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)
pre_dfs v e
x = v

goal (1 subgoal):
 1. reachable y x
[PROOF STEP]
apply (simp add: pre_dfs_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>v \<preceq> y in (v # stack e); wf_env e \<and> v \<notin> visited e \<and> reachable (root e) v \<and> vsuccs e v = {} \<and> (\<forall>n\<in>set (stack e). reachable n v); x = v\<rbrakk> \<Longrightarrow> reachable y v
[PROOF STEP]
by (metis insert_iff list.simps(15) precedes_mem(2) reachable_refl)
[PROOF STATE]
proof (state)
this:
reachable y x

goal (1 subgoal):
 1. x \<noteq> v \<Longrightarrow> reachable y x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<noteq> v \<Longrightarrow> reachable y x
[PROOF STEP]
assume "x \<noteq> v"
[PROOF STATE]
proof (state)
this:
x \<noteq> v

goal (1 subgoal):
 1. x \<noteq> v \<Longrightarrow> reachable y x
[PROOF STEP]
with \<open>x \<preceq> y in stack ?e'\<close> wf
[PROOF STATE]
proof (chain)
picking this:
x \<preceq> y in stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)
wf_env e
x \<noteq> v
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<preceq> y in stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)
wf_env e
x \<noteq> v

goal (1 subgoal):
 1. reachable y x
[PROOF STEP]
by (simp add: pre_dfs_def wf_env_def precedes_in_tail)
[PROOF STATE]
proof (state)
this:
reachable y x

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>n m. n \<preceq> m in stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) \<longrightarrow> reachable m n

goal (1 subgoal):
 1. pre_dfss v (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>n m. n \<preceq> m in stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) \<longrightarrow> reachable m n

goal (1 subgoal):
 1. pre_dfss v (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)
[PROOF STEP]
from wf v
[PROOF STATE]
proof (chain)
picking this:
wf_env e
v \<notin> visited e
[PROOF STEP]
have "\<forall>n. vsuccs ?e' n \<subseteq> visited ?e'"
[PROOF STATE]
proof (prove)
using this:
wf_env e
v \<notin> visited e

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

goal (1 subgoal):
 1. pre_dfss v (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>n. vsuccs (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) n \<subseteq> visited (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)

goal (1 subgoal):
 1. pre_dfss v (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)
[PROOF STEP]
from wf v
[PROOF STATE]
proof (chain)
picking this:
wf_env e
v \<notin> visited e
[PROOF STEP]
have "(\<forall>n \<in> set (stack ?e'). \<forall> m \<in> set (stack ?e'). n \<noteq> m \<longrightarrow> \<S> ?e' n \<inter> \<S> ?e' m = {})"
[PROOF STATE]
proof (prove)
using this:
wf_env e
v \<notin> visited e

goal (1 subgoal):
 1. \<forall>n\<in>set (stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)). \<forall>m\<in>set (stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)). n \<noteq> m \<longrightarrow> \<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) n \<inter> \<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) m = {}
[PROOF STEP]
apply (simp add: wf_env_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<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 \<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; v \<notin> visited e\<rbrakk> \<Longrightarrow> (\<forall>m\<in>set (stack e). v \<noteq> m \<longrightarrow> \<S> e m \<noteq> {v}) \<and> (\<forall>n\<in>set (stack e). n \<noteq> v \<longrightarrow> \<S> e n \<noteq> {v})
[PROOF STEP]
by (metis singletonD)
[PROOF STATE]
proof (state)
this:
\<forall>n\<in>set (stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)). \<forall>m\<in>set (stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)). n \<noteq> m \<longrightarrow> \<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) n \<inter> \<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) m = {}

goal (1 subgoal):
 1. pre_dfss v (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>n\<in>set (stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)). \<forall>m\<in>set (stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)). n \<noteq> m \<longrightarrow> \<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) n \<inter> \<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) m = {}

goal (1 subgoal):
 1. pre_dfss v (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)
[PROOF STEP]
have "\<Union> {\<S> ?e' v | v . v \<in> set (stack ?e')} = visited ?e' - explored ?e'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> {\<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) va |va. va \<in> set (stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>))} = visited (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) - explored (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Union> {\<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) va |va. va \<in> set (stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>))} = visited (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) - explored (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)
[PROOF STEP]
have "\<Union> {\<S> ?e' v | v . v \<in> set (stack ?e')} =
          (\<Union> {\<S> e v | v . v \<in> set (stack e)}) \<union> \<S> e v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> {\<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) va |va. va \<in> set (stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>))} = \<Union> {\<S> e v |v. v \<in> set (stack e)} \<union> \<S> e v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Union> {\<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) va |va. va \<in> set (stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>))} = \<Union> {\<S> e v |v. v \<in> set (stack e)} \<union> \<S> e v

goal (1 subgoal):
 1. \<Union> {\<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) va |va. va \<in> set (stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>))} = visited (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) - explored (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<Union> {\<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) va |va. va \<in> set (stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>))} = \<Union> {\<S> e v |v. v \<in> set (stack e)} \<union> \<S> e v

goal (1 subgoal):
 1. \<Union> {\<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) va |va. va \<in> set (stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>))} = visited (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) - explored (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)
[PROOF STEP]
from wf v
[PROOF STATE]
proof (chain)
picking this:
wf_env e
v \<notin> visited e
[PROOF STEP]
have "\<dots> = visited ?e' - explored ?e'"
[PROOF STATE]
proof (prove)
using this:
wf_env e
v \<notin> visited e

goal (1 subgoal):
 1. \<Union> {\<S> e v |v. v \<in> set (stack e)} \<union> \<S> e v = visited (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) - explored (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)
[PROOF STEP]
by (auto simp: wf_env_def)
[PROOF STATE]
proof (state)
this:
\<Union> {\<S> e v |v. v \<in> set (stack e)} \<union> \<S> e v = visited (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) - explored (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)

goal (1 subgoal):
 1. \<Union> {\<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) va |va. va \<in> set (stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>))} = visited (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) - explored (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<Union> {\<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) va |va. va \<in> set (stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>))} = visited (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) - explored (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Union> {\<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) va |va. va \<in> set (stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>))} = visited (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) - explored (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)

goal (1 subgoal):
 1. \<Union> {\<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) va |va. va \<in> set (stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>))} = visited (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) - explored (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<Union> {\<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) va |va. va \<in> set (stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>))} = visited (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) - explored (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Union> {\<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) va |va. va \<in> set (stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>))} = visited (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) - explored (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)

goal (1 subgoal):
 1. pre_dfss v (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Union> {\<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) va |va. va \<in> set (stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>))} = visited (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) - explored (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)

goal (1 subgoal):
 1. pre_dfss v (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)
[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\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) \<and> n \<noteq> m \<longrightarrow> (\<forall>u\<in>\<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) n. \<not> reachable_avoiding u m (unvisited (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) n))
[PROOF STEP]
proof (clarify)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n m u. \<lbrakk>u \<in> \<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) n; n \<preceq> m in stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>); n \<noteq> m; reachable_avoiding u m (unvisited (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) 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\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) n; n \<preceq> m in stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>); n \<noteq> m; reachable_avoiding u m (unvisited (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) n)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume asm: "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\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)
x \<noteq> y
u \<in> \<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) x
reachable_avoiding u y (unvisited (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) x)

goal (1 subgoal):
 1. \<And>n m u. \<lbrakk>u \<in> \<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) n; n \<preceq> m in stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>); n \<noteq> m; reachable_avoiding u m (unvisited (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) n)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
proof (cases "x = v")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = v \<Longrightarrow> False
 2. x \<noteq> v \<Longrightarrow> False
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x = v

goal (2 subgoals):
 1. x = v \<Longrightarrow> False
 2. x \<noteq> v \<Longrightarrow> False
[PROOF STEP]
with wf v \<open>u \<in> \<S> ?e' x\<close>
[PROOF STATE]
proof (chain)
picking this:
wf_env e
v \<notin> visited e
u \<in> \<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) x
x = v
[PROOF STEP]
have "u = v" "vsuccs ?e' v = {}"
[PROOF STATE]
proof (prove)
using this:
wf_env e
v \<notin> visited e
u \<in> \<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) x
x = v

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

goal (2 subgoals):
 1. x = v \<Longrightarrow> False
 2. x \<noteq> v \<Longrightarrow> False
[PROOF STEP]
with \<open>reachable_avoiding u y (unvisited ?e' x)\<close>[THEN ra_cases]
           True \<open>x \<noteq> y\<close> wf
[PROOF STATE]
proof (chain)
picking this:
u = y \<or> (\<exists>z. edge u z \<and> (u, z) \<notin> unvisited (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) x \<and> reachable_avoiding z y (unvisited (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) x))
x = v
x \<noteq> y
wf_env e
u = v
vsuccs (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) v = {}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
u = y \<or> (\<exists>z. edge u z \<and> (u, z) \<notin> unvisited (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) x \<and> reachable_avoiding z y (unvisited (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) x))
x = v
x \<noteq> y
wf_env e
u = v
vsuccs (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) v = {}

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

goal (1 subgoal):
 1. x \<noteq> v \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<noteq> v \<Longrightarrow> False
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
x \<noteq> v

goal (1 subgoal):
 1. x \<noteq> v \<Longrightarrow> False
[PROOF STEP]
with asm wf
[PROOF STATE]
proof (chain)
picking this:
x \<preceq> y in stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)
x \<noteq> y
u \<in> \<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) x
reachable_avoiding u y (unvisited (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) x)
wf_env e
x \<noteq> v
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<preceq> y in stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)
x \<noteq> y
u \<in> \<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) x
reachable_avoiding u y (unvisited (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) x)
wf_env e
x \<noteq> v

goal (1 subgoal):
 1. False
[PROOF STEP]
by (auto simp: precedes_in_tail wf_env_def unvisited_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:
\<forall>n m. n \<preceq> m in stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) \<and> n \<noteq> m \<longrightarrow> (\<forall>u\<in>\<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) n. \<not> reachable_avoiding u m (unvisited (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) n))

goal (1 subgoal):
 1. pre_dfss v (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>n m. n \<preceq> m in stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) \<and> n \<noteq> m \<longrightarrow> (\<forall>u\<in>\<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) n. \<not> reachable_avoiding u m (unvisited (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) n))

goal (1 subgoal):
 1. pre_dfss v (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)
[PROOF STEP]
have "\<forall>n m. n \<preceq> m in stack ?e' \<longrightarrow> n \<preceq> m in cstack ?e'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n m. n \<preceq> m in stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) \<longrightarrow> n \<preceq> m in cstack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)
[PROOF STEP]
proof (clarsimp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n m. n \<preceq> m in (v # stack e) \<Longrightarrow> n \<preceq> m in (v # cstack e)
[PROOF STEP]
fix n m
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n m. n \<preceq> m in (v # stack e) \<Longrightarrow> n \<preceq> m in (v # cstack e)
[PROOF STEP]
assume "n \<preceq> m in (v # stack e)"
[PROOF STATE]
proof (state)
this:
n \<preceq> m in (v # stack e)

goal (1 subgoal):
 1. \<And>n m. n \<preceq> m in (v # stack e) \<Longrightarrow> n \<preceq> m in (v # cstack e)
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
pre_dfs v e
n \<preceq> m in (v # stack e)
[PROOF STEP]
show "n \<preceq> m in (v # cstack e)"
[PROOF STATE]
proof (prove)
using this:
pre_dfs v e
n \<preceq> m in (v # stack e)

goal (1 subgoal):
 1. n \<preceq> m in (v # cstack e)
[PROOF STEP]
unfolding pre_dfs_def 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) \<and> v \<notin> visited e \<and> reachable (root e) v \<and> vsuccs e v = {} \<and> (\<forall>n\<in>set (stack e). reachable n v)
n \<preceq> m in (v # stack e)

goal (1 subgoal):
 1. n \<preceq> m in (v # cstack e)
[PROOF STEP]
by (metis head_precedes insertI1 list.simps(15) precedes_in_tail precedes_mem(2) precedes_refl)
[PROOF STATE]
proof (state)
this:
n \<preceq> m in (v # cstack e)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>n m. n \<preceq> m in stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) \<longrightarrow> n \<preceq> m in cstack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)

goal (1 subgoal):
 1. pre_dfss v (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>n m. n \<preceq> m in stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) \<longrightarrow> n \<preceq> m in cstack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)

goal (1 subgoal):
 1. pre_dfss v (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)
[PROOF STEP]
have "\<forall>n \<in> set (stack ?e'). \<forall>m \<in> \<S> ?e' n. m \<in> set (cstack ?e') \<longrightarrow> m \<preceq> n in cstack ?e'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n\<in>set (stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)). \<forall>m\<in>\<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) n. m \<in> set (cstack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)) \<longrightarrow> m \<preceq> n in cstack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)
[PROOF STEP]
proof (clarify)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n m. \<lbrakk>n \<in> set (stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)); m \<in> \<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) n; m \<in> set (cstack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>))\<rbrakk> \<Longrightarrow> m \<preceq> n in cstack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)
[PROOF STEP]
fix n m
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n m. \<lbrakk>n \<in> set (stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)); m \<in> \<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) n; m \<in> set (cstack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>))\<rbrakk> \<Longrightarrow> m \<preceq> n in cstack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)
[PROOF STEP]
assume "n \<in> set (stack ?e')" "m \<in> \<S> ?e' n" "m \<in> set (cstack ?e')"
[PROOF STATE]
proof (state)
this:
n \<in> set (stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>))
m \<in> \<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) n
m \<in> set (cstack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>))

goal (1 subgoal):
 1. \<And>n m. \<lbrakk>n \<in> set (stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)); m \<in> \<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) n; m \<in> set (cstack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>))\<rbrakk> \<Longrightarrow> m \<preceq> n in cstack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)
[PROOF STEP]
show "m \<preceq> n in cstack ?e'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m \<preceq> n in cstack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)
[PROOF STEP]
proof (cases "n = v")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n = v \<Longrightarrow> m \<preceq> n in cstack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)
 2. n \<noteq> v \<Longrightarrow> m \<preceq> n in cstack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
n = v

goal (2 subgoals):
 1. n = v \<Longrightarrow> m \<preceq> n in cstack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)
 2. n \<noteq> v \<Longrightarrow> m \<preceq> n in cstack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)
[PROOF STEP]
with wf v \<open>m \<in> \<S> ?e' n\<close>
[PROOF STATE]
proof (chain)
picking this:
wf_env e
v \<notin> visited e
m \<in> \<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) n
n = v
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
wf_env e
v \<notin> visited e
m \<in> \<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) n
n = v

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

goal (1 subgoal):
 1. n \<noteq> v \<Longrightarrow> m \<preceq> n in cstack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n \<noteq> v \<Longrightarrow> m \<preceq> n in cstack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
n \<noteq> v

goal (1 subgoal):
 1. n \<noteq> v \<Longrightarrow> m \<preceq> n in cstack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)
[PROOF STEP]
with \<open>n \<in> set (stack ?e')\<close> \<open>m \<in> \<S> ?e' n\<close>
[PROOF STATE]
proof (chain)
picking this:
n \<in> set (stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>))
m \<in> \<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) n
n \<noteq> v
[PROOF STEP]
have "n \<in> set (stack e)" "m \<in> \<S> e n"
[PROOF STATE]
proof (prove)
using this:
n \<in> set (stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>))
m \<in> \<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) n
n \<noteq> v

goal (1 subgoal):
 1. n \<in> set (stack e) &&& m \<in> \<S> e n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n \<in> set (stack e)
m \<in> \<S> e n

goal (1 subgoal):
 1. n \<noteq> v \<Longrightarrow> m \<preceq> n in cstack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)
[PROOF STEP]
with wf v False \<open>m \<in> \<S> e n\<close> \<open>m \<in> set (cstack ?e')\<close>
[PROOF STATE]
proof (chain)
picking this:
wf_env e
v \<notin> visited e
n \<noteq> v
m \<in> \<S> e n
m \<in> set (cstack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>))
n \<in> set (stack e)
m \<in> \<S> e n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
wf_env e
v \<notin> visited e
n \<noteq> v
m \<in> \<S> e n
m \<in> set (cstack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>))
n \<in> set (stack e)
m \<in> \<S> e n

goal (1 subgoal):
 1. m \<preceq> n in cstack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)
[PROOF STEP]
apply (simp add: wf_env_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<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 \<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; v \<notin> visited e; n \<noteq> v; \<S> e n = \<S> e m; m = v \<or> m \<in> set (cstack e); n \<in> set (stack e)\<rbrakk> \<Longrightarrow> m \<preceq> n in (v # cstack e)
[PROOF STEP]
by (metis (mono_tags, lifting) precedes_in_tail singletonD)
[PROOF STATE]
proof (state)
this:
m \<preceq> n in cstack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
m \<preceq> n in cstack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>n\<in>set (stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)). \<forall>m\<in>\<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) n. m \<in> set (cstack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)) \<longrightarrow> m \<preceq> n in cstack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)

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

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

goal (1 subgoal):
 1. (\<forall>n\<in>visited (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>). reachable (root (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)) n) \<and> distinct (stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)) \<and> distinct (cstack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)) \<and> (\<forall>n m. n \<preceq> m in stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) \<longrightarrow> n \<preceq> m in cstack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)) \<and> (\<forall>n m. n \<preceq> m in stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) \<longrightarrow> reachable m n) \<and> explored (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) \<subseteq> visited (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) \<and> set (cstack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)) \<subseteq> visited (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) \<and> (\<forall>n\<in>explored (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>). \<forall>m. reachable n m \<longrightarrow> m \<in> explored (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)) \<and> (\<forall>n. vsuccs (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) n \<subseteq> successors n \<inter> visited (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)) \<and> (\<forall>n. n \<notin> visited (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) \<longrightarrow> vsuccs (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) n = {}) \<and> (\<forall>n\<in>explored (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>). vsuccs (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) n = successors n) \<and> (\<forall>n\<in>visited (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) - set (cstack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)). vsuccs (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) n = successors n) \<and> (\<forall>n m. (m \<in> \<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) n) = (\<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) n = \<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) m)) \<and> (\<forall>n. n \<notin> visited (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) \<longrightarrow> \<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) n = {n}) \<and> (\<forall>n\<in>set (stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)). \<forall>m\<in>set (stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)). n \<noteq> m \<longrightarrow> \<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) n \<inter> \<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) m = {}) \<and> \<Union> {\<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) n |n. n \<in> set (stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>))} = visited (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) - explored (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) \<and> (\<forall>n\<in>set (stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)). \<forall>m\<in>\<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) n. m \<in> set (cstack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)) \<longrightarrow> m \<preceq> n in cstack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)) \<and> (\<forall>n m. n \<preceq> m in stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) \<and> n \<noteq> m \<longrightarrow> (\<forall>u\<in>\<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) n. \<not> reachable_avoiding u m (unvisited (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) n))) \<and> (\<forall>n. is_subscc (\<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) n)) \<and> Ball (sccs (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)) is_scc \<and> \<Union> (sccs (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)) = explored (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)
[PROOF STEP]
by (meson le_inf_iff)
[PROOF STATE]
proof (state)
this:
wf_env (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)

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

goal (1 subgoal):
 1. pre_dfss v (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
pre_dfs v e
[PROOF STEP]
have "\<forall>w \<in> vsuccs ?e' v. w \<in> explored ?e' \<union> \<S> ?e' (hd (stack ?e'))"
[PROOF STATE]
proof (prove)
using this:
pre_dfs v e

goal (1 subgoal):
 1. \<forall>w\<in>vsuccs (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) v. w \<in> explored (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) \<union> \<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) (hd (stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)))
[PROOF STEP]
by (simp add: pre_dfs_def)
[PROOF STATE]
proof (state)
this:
\<forall>w\<in>vsuccs (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) v. w \<in> explored (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) \<union> \<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) (hd (stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)))

goal (1 subgoal):
 1. pre_dfss v (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>w\<in>vsuccs (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) v. w \<in> explored (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) \<union> \<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) (hd (stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)))

goal (1 subgoal):
 1. pre_dfss v (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)
[PROOF STEP]
from \<open>\<forall>n m. n \<preceq> m in stack ?e' \<longrightarrow> reachable m n\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>n m. n \<preceq> m in stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) \<longrightarrow> reachable m n
[PROOF STEP]
have "\<forall>n \<in> set (stack ?e'). reachable n v"
[PROOF STATE]
proof (prove)
using this:
\<forall>n m. n \<preceq> m in stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) \<longrightarrow> reachable m n

goal (1 subgoal):
 1. \<forall>n\<in>set (stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)). reachable n v
[PROOF STEP]
by (simp add: head_precedes)
[PROOF STATE]
proof (state)
this:
\<forall>n\<in>set (stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)). reachable n v

goal (1 subgoal):
 1. pre_dfss v (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>n\<in>set (stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)). reachable n v

goal (1 subgoal):
 1. pre_dfss v (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)
[PROOF STEP]
from wf v
[PROOF STATE]
proof (chain)
picking this:
wf_env e
v \<notin> visited e
[PROOF STEP]
have "\<S> ?e' (hd (stack ?e')) = {v}"
[PROOF STATE]
proof (prove)
using this:
wf_env e
v \<notin> visited e

goal (1 subgoal):
 1. \<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) (hd (stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>))) = {v}
[PROOF STEP]
by (simp add: pre_dfs_def wf_env_def)
[PROOF STATE]
proof (state)
this:
\<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) (hd (stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>))) = {v}

goal (1 subgoal):
 1. pre_dfss v (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
wf_env (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)
\<forall>w\<in>vsuccs (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) v. w \<in> explored (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) \<union> \<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) (hd (stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)))
\<forall>n\<in>set (stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)). reachable n v
\<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) (hd (stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>))) = {v}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
wf_env (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)
\<forall>w\<in>vsuccs (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) v. w \<in> explored (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) \<union> \<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) (hd (stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)))
\<forall>n\<in>set (stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>)). reachable n v
\<S> (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>) (hd (stack (e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>))) = {v}

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pre_dfss_pre_dfs:
  assumes "pre_dfss v e" and "w \<notin> visited e" and "w \<in> successors v"
  shows "pre_dfs w e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pre_dfs w e
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
pre_dfss v e
w \<notin> visited e
edge v w

goal (1 subgoal):
 1. pre_dfs w e
[PROOF STEP]
unfolding pre_dfss_def pre_dfs_def 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) \<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)
w \<notin> visited e
edge v w

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) \<and> w \<notin> visited e \<and> reachable (root e) w \<and> vsuccs e w = {} \<and> (\<forall>n\<in>set (stack e). reachable n w)
[PROOF STEP]
by (meson succ_reachable)