[STATEMENT]
lemma pre_post:
  shows
  "\<lbrakk>dfs_dfss_dom (Inl(v,e)); pre_dfs v e\<rbrakk> \<Longrightarrow> post_dfs v e (dfs v e)"
  "\<lbrakk>dfs_dfss_dom (Inr(v,e)); pre_dfss v e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>dfs_dfss_dom (Inl (v, e)); pre_dfs v e\<rbrakk> \<Longrightarrow> post_dfs v e (dfs v e)) &&& (\<lbrakk>dfs_dfss_dom (Inr (v, e)); pre_dfss v e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e))
[PROOF STEP]
proof (induct rule: dfs_dfss.pinduct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>v e. \<lbrakk>dfs_dfss_dom (Inl (v, e)); \<And>x. \<lbrakk>x = e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>; pre_dfss v x\<rbrakk> \<Longrightarrow> post_dfss v x (dfss v x); pre_dfs v e\<rbrakk> \<Longrightarrow> post_dfs v e (dfs v e)
 2. \<And>v e. \<lbrakk>dfs_dfss_dom (Inr (v, e)); \<And>x xa. \<lbrakk>x = successors v - vsuccs e v; x \<noteq> {}; xa = (SOME xa. xa \<in> x); xa \<notin> explored e; xa \<notin> visited e; pre_dfs xa e\<rbrakk> \<Longrightarrow> post_dfs xa e (dfs xa e); \<And>x xa xb xc. \<lbrakk>x = successors v - vsuccs e v; x \<noteq> {}; xa = (SOME xa. xa \<in> x); xb = (if xa \<in> explored e then e else if xa \<notin> visited e then dfs xa e else unite v xa e); xc = xb\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs xb v \<union> {xa} else vsuccs xb x\<rparr>; pre_dfss v xc\<rbrakk> \<Longrightarrow> post_dfss v xc (dfss v xc); pre_dfss v e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
fix v e
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>v e. \<lbrakk>dfs_dfss_dom (Inl (v, e)); \<And>x. \<lbrakk>x = e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>; pre_dfss v x\<rbrakk> \<Longrightarrow> post_dfss v x (dfss v x); pre_dfs v e\<rbrakk> \<Longrightarrow> post_dfs v e (dfs v e)
 2. \<And>v e. \<lbrakk>dfs_dfss_dom (Inr (v, e)); \<And>x xa. \<lbrakk>x = successors v - vsuccs e v; x \<noteq> {}; xa = (SOME xa. xa \<in> x); xa \<notin> explored e; xa \<notin> visited e; pre_dfs xa e\<rbrakk> \<Longrightarrow> post_dfs xa e (dfs xa e); \<And>x xa xb xc. \<lbrakk>x = successors v - vsuccs e v; x \<noteq> {}; xa = (SOME xa. xa \<in> x); xb = (if xa \<in> explored e then e else if xa \<notin> visited e then dfs xa e else unite v xa e); xc = xb\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs xb v \<union> {xa} else vsuccs xb x\<rparr>; pre_dfss v xc\<rbrakk> \<Longrightarrow> post_dfss v xc (dfss v xc); pre_dfss v e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
assume dom: "dfs_dfss_dom (Inl(v,e))"
     and predfs: "pre_dfs v e"
     and prepostdfss: "\<And>e1. \<lbrakk> e1 = e \<lparr>visited := visited e \<union> {v}, stack := v # stack e,
                                      cstack := v # cstack e\<rparr>; pre_dfss v e1 \<rbrakk>
                            \<Longrightarrow> post_dfss v e1 (dfss v e1)"
[PROOF STATE]
proof (state)
this:
dfs_dfss_dom (Inl (v, e))
pre_dfs v e
\<lbrakk>?e1.6 = e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>; pre_dfss v ?e1.6\<rbrakk> \<Longrightarrow> post_dfss v ?e1.6 (dfss v ?e1.6)

goal (2 subgoals):
 1. \<And>v e. \<lbrakk>dfs_dfss_dom (Inl (v, e)); \<And>x. \<lbrakk>x = e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>; pre_dfss v x\<rbrakk> \<Longrightarrow> post_dfss v x (dfss v x); pre_dfs v e\<rbrakk> \<Longrightarrow> post_dfs v e (dfs v e)
 2. \<And>v e. \<lbrakk>dfs_dfss_dom (Inr (v, e)); \<And>x xa. \<lbrakk>x = successors v - vsuccs e v; x \<noteq> {}; xa = (SOME xa. xa \<in> x); xa \<notin> explored e; xa \<notin> visited e; pre_dfs xa e\<rbrakk> \<Longrightarrow> post_dfs xa e (dfs xa e); \<And>x xa xb xc. \<lbrakk>x = successors v - vsuccs e v; x \<noteq> {}; xa = (SOME xa. xa \<in> x); xb = (if xa \<in> explored e then e else if xa \<notin> visited e then dfs xa e else unite v xa e); xc = xb\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs xb v \<union> {xa} else vsuccs xb x\<rparr>; pre_dfss v xc\<rbrakk> \<Longrightarrow> post_dfss v xc (dfss v xc); pre_dfss v e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dfs_dfss_dom (Inl (v, e))
pre_dfs v e
\<lbrakk>?e1.6 = e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>; pre_dfss v ?e1.6\<rbrakk> \<Longrightarrow> post_dfss v ?e1.6 (dfss v ?e1.6)
[PROOF STEP]
show "post_dfs v e (dfs v e)"
[PROOF STATE]
proof (prove)
using this:
dfs_dfss_dom (Inl (v, e))
pre_dfs v e
\<lbrakk>?e1.6 = e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>; pre_dfss v ?e1.6\<rbrakk> \<Longrightarrow> post_dfss v ?e1.6 (dfss v ?e1.6)

goal (1 subgoal):
 1. post_dfs v e (dfs v e)
[PROOF STEP]
using pre_dfs_implies_post_dfs pre_dfs_pre_dfss
[PROOF STATE]
proof (prove)
using this:
dfs_dfss_dom (Inl (v, e))
pre_dfs v e
\<lbrakk>?e1.6 = e\<lparr>visited := visited e \<union> {v}, stack := v # stack e, cstack := v # cstack e\<rparr>; pre_dfss v ?e1.6\<rbrakk> \<Longrightarrow> post_dfss v ?e1.6 (dfss v ?e1.6)
\<lbrakk>pre_dfs ?v ?e; dfs_dfss_dom (Inl (?v, ?e)); post_dfss ?v (?e\<lparr>visited := visited ?e \<union> {?v}, stack := ?v # stack ?e, cstack := ?v # cstack ?e\<rparr>) (dfss ?v (?e\<lparr>visited := visited ?e \<union> {?v}, stack := ?v # stack ?e, cstack := ?v # cstack ?e\<rparr>))\<rbrakk> \<Longrightarrow> post_dfs ?v ?e (dfs ?v ?e)
pre_dfs ?v ?e \<Longrightarrow> pre_dfss ?v (?e\<lparr>visited := visited ?e \<union> {?v}, stack := ?v # stack ?e, cstack := ?v # cstack ?e\<rparr>)

goal (1 subgoal):
 1. post_dfs v e (dfs v e)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
post_dfs v e (dfs v e)

goal (1 subgoal):
 1. \<And>v e. \<lbrakk>dfs_dfss_dom (Inr (v, e)); \<And>x xa. \<lbrakk>x = successors v - vsuccs e v; x \<noteq> {}; xa = (SOME xa. xa \<in> x); xa \<notin> explored e; xa \<notin> visited e; pre_dfs xa e\<rbrakk> \<Longrightarrow> post_dfs xa e (dfs xa e); \<And>x xa xb xc. \<lbrakk>x = successors v - vsuccs e v; x \<noteq> {}; xa = (SOME xa. xa \<in> x); xb = (if xa \<in> explored e then e else if xa \<notin> visited e then dfs xa e else unite v xa e); xc = xb\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs xb v \<union> {xa} else vsuccs xb x\<rparr>; pre_dfss v xc\<rbrakk> \<Longrightarrow> post_dfss v xc (dfss v xc); pre_dfss v e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>v e. \<lbrakk>dfs_dfss_dom (Inr (v, e)); \<And>x xa. \<lbrakk>x = successors v - vsuccs e v; x \<noteq> {}; xa = (SOME xa. xa \<in> x); xa \<notin> explored e; xa \<notin> visited e; pre_dfs xa e\<rbrakk> \<Longrightarrow> post_dfs xa e (dfs xa e); \<And>x xa xb xc. \<lbrakk>x = successors v - vsuccs e v; x \<noteq> {}; xa = (SOME xa. xa \<in> x); xb = (if xa \<in> explored e then e else if xa \<notin> visited e then dfs xa e else unite v xa e); xc = xb\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs xb v \<union> {xa} else vsuccs xb x\<rparr>; pre_dfss v xc\<rbrakk> \<Longrightarrow> post_dfss v xc (dfss v xc); pre_dfss v e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
fix v e
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>v e. \<lbrakk>dfs_dfss_dom (Inr (v, e)); \<And>x xa. \<lbrakk>x = successors v - vsuccs e v; x \<noteq> {}; xa = (SOME xa. xa \<in> x); xa \<notin> explored e; xa \<notin> visited e; pre_dfs xa e\<rbrakk> \<Longrightarrow> post_dfs xa e (dfs xa e); \<And>x xa xb xc. \<lbrakk>x = successors v - vsuccs e v; x \<noteq> {}; xa = (SOME xa. xa \<in> x); xb = (if xa \<in> explored e then e else if xa \<notin> visited e then dfs xa e else unite v xa e); xc = xb\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs xb v \<union> {xa} else vsuccs xb x\<rparr>; pre_dfss v xc\<rbrakk> \<Longrightarrow> post_dfss v xc (dfss v xc); pre_dfss v e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
assume dom: "dfs_dfss_dom (Inr(v,e))"
     and predfss: "pre_dfss v e"
     and prepostdfs:
           "\<And>vs w.
             \<lbrakk> vs = successors v - vsuccs e v; vs \<noteq> {}; w = (SOME x. x \<in> vs);
               w \<notin> explored e; w \<notin> visited e; pre_dfs w e \<rbrakk>
             \<Longrightarrow> post_dfs w e (dfs w e)"
     and prepostdfss:
           "\<And>vs w e' e''.
             \<lbrakk> vs = successors v - vsuccs e v; vs \<noteq> {}; w = (SOME x. x \<in> vs);
               e' = (if w \<in> explored e then e
                     else if w \<notin> visited e then dfs w e
                     else unite v w e);
               e'' = e'\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e' v \<union> {w}
                                      else vsuccs e' x\<rparr> ;
               pre_dfss v e'' \<rbrakk>
             \<Longrightarrow> post_dfss v e'' (dfss v e'')"
[PROOF STATE]
proof (state)
this:
dfs_dfss_dom (Inr (v, e))
pre_dfss v e
\<lbrakk>?vs6 = successors v - vsuccs e v; ?vs6 \<noteq> {}; ?w6 = (SOME x. x \<in> ?vs6); ?w6 \<notin> explored e; ?w6 \<notin> visited e; pre_dfs ?w6 e\<rbrakk> \<Longrightarrow> post_dfs ?w6 e (dfs ?w6 e)
\<lbrakk>?vs6 = successors v - vsuccs e v; ?vs6 \<noteq> {}; ?w6 = (SOME x. x \<in> ?vs6); ?e'6 = (if ?w6 \<in> explored e then e else if ?w6 \<notin> visited e then dfs ?w6 e else unite v ?w6 e); ?e''6 = ?e'6\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs ?e'6 v \<union> {?w6} else vsuccs ?e'6 x\<rparr>; pre_dfss v ?e''6\<rbrakk> \<Longrightarrow> post_dfss v ?e''6 (dfss v ?e''6)

goal (1 subgoal):
 1. \<And>v e. \<lbrakk>dfs_dfss_dom (Inr (v, e)); \<And>x xa. \<lbrakk>x = successors v - vsuccs e v; x \<noteq> {}; xa = (SOME xa. xa \<in> x); xa \<notin> explored e; xa \<notin> visited e; pre_dfs xa e\<rbrakk> \<Longrightarrow> post_dfs xa e (dfs xa e); \<And>x xa xb xc. \<lbrakk>x = successors v - vsuccs e v; x \<noteq> {}; xa = (SOME xa. xa \<in> x); xb = (if xa \<in> explored e then e else if xa \<notin> visited e then dfs xa e else unite v xa e); xc = xb\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs xb v \<union> {xa} else vsuccs xb x\<rparr>; pre_dfss v xc\<rbrakk> \<Longrightarrow> post_dfss v xc (dfss v xc); pre_dfss v e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
show "post_dfss v e (dfss v e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. post_dfss v e (dfss v e)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. post_dfss v e (dfss v e)
[PROOF STEP]
let ?vs = "successors v - vsuccs e v"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. post_dfss v e (dfss v e)
[PROOF STEP]
from predfss
[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. post_dfss v e (dfss v e)
[PROOF STEP]
from predfss
[PROOF STATE]
proof (chain)
picking this:
pre_dfss v e
[PROOF STEP]
have "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. post_dfss v e (dfss v e)
[PROOF STEP]
from predfss
[PROOF STATE]
proof (chain)
picking this:
pre_dfss v e
[PROOF STEP]
have "v \<notin> explored e"
[PROOF STATE]
proof (prove)
using this:
pre_dfss v e

goal (1 subgoal):
 1. v \<notin> explored e
[PROOF STEP]
by (meson DiffD2 list.set_sel(1) pre_dfss_def stack_class)
[PROOF STATE]
proof (state)
this:
v \<notin> explored e

goal (1 subgoal):
 1. post_dfss v e (dfss v e)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. post_dfss v e (dfss v e)
[PROOF STEP]
proof (cases "?vs = {}")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. successors v - vsuccs e v = {} \<Longrightarrow> post_dfss v e (dfss v e)
 2. successors v - vsuccs e v \<noteq> {} \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
successors v - vsuccs e v = {}

goal (2 subgoals):
 1. successors v - vsuccs e v = {} \<Longrightarrow> post_dfss v e (dfss v e)
 2. successors v - vsuccs e v \<noteq> {} \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
with dom
[PROOF STATE]
proof (chain)
picking this:
dfs_dfss_dom (Inr (v, e))
successors v - vsuccs e v = {}
[PROOF STEP]
have "dfss v e = e"
[PROOF STATE]
proof (prove)
using this:
dfs_dfss_dom (Inr (v, e))
successors v - vsuccs e v = {}

goal (1 subgoal):
 1. dfss v e = e
[PROOF STEP]
by (simp add: dfss.psimps)
[PROOF STATE]
proof (state)
this:
dfss v e = e

goal (2 subgoals):
 1. successors v - vsuccs e v = {} \<Longrightarrow> post_dfss v e (dfss v e)
 2. successors v - vsuccs e v \<noteq> {} \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
dfss v e = e

goal (2 subgoals):
 1. successors v - vsuccs e v = {} \<Longrightarrow> post_dfss v e (dfss v e)
 2. successors v - vsuccs e v \<noteq> {} \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
from True wf
[PROOF STATE]
proof (chain)
picking this:
successors v - vsuccs e v = {}
wf_env e
[PROOF STEP]
have "vsuccs e v = successors v"
[PROOF STATE]
proof (prove)
using this:
successors v - vsuccs e v = {}
wf_env e

goal (1 subgoal):
 1. vsuccs e v = successors v
[PROOF STEP]
unfolding wf_env_def
[PROOF STATE]
proof (prove)
using this:
successors v - vsuccs e v = {}
(\<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

goal (1 subgoal):
 1. vsuccs e v = successors v
[PROOF STEP]
by (meson Diff_eq_empty_iff le_infE subset_antisym)
[PROOF STATE]
proof (state)
this:
vsuccs e v = successors v

goal (2 subgoals):
 1. successors v - vsuccs e v = {} \<Longrightarrow> post_dfss v e (dfss v e)
 2. successors v - vsuccs e v \<noteq> {} \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
vsuccs e v = successors v

goal (2 subgoals):
 1. successors v - vsuccs e v = {} \<Longrightarrow> post_dfss v e (dfss v e)
 2. successors v - vsuccs e v \<noteq> {} \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
have "sub_env e e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sub_env e e
[PROOF STEP]
by (simp add: sub_env_def)
[PROOF STATE]
proof (state)
this:
sub_env e e

goal (2 subgoals):
 1. successors v - vsuccs e v = {} \<Longrightarrow> post_dfss v e (dfss v e)
 2. successors v - vsuccs e v \<noteq> {} \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sub_env e e

goal (2 subgoals):
 1. successors v - vsuccs e v = {} \<Longrightarrow> post_dfss v e (dfss v e)
 2. successors v - vsuccs e v \<noteq> {} \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
from predfss \<open>vsuccs e v = successors v\<close>
[PROOF STATE]
proof (chain)
picking this:
pre_dfss v e
vsuccs e v = successors v
[PROOF STEP]
have "\<forall>w \<in> successors v. w \<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))"
[PROOF STATE]
proof (prove)
using this:
pre_dfss v e
vsuccs e v = successors v

goal (1 subgoal):
 1. (\<forall>w\<in>successors v. w \<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))
[PROOF STEP]
by (auto simp: pre_dfss_def)
[PROOF STATE]
proof (state)
this:
\<forall>w\<in>successors v. w \<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))

goal (2 subgoals):
 1. successors v - vsuccs e v = {} \<Longrightarrow> post_dfss v e (dfss v e)
 2. successors v - vsuccs e v \<noteq> {} \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>w\<in>successors v. w \<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))

goal (2 subgoals):
 1. successors v - vsuccs e v = {} \<Longrightarrow> post_dfss v e (dfss v e)
 2. successors v - vsuccs e v \<noteq> {} \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
have "\<exists>ns. stack e = ns @ (stack e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>ns. stack e = ns @ stack e
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>ns. stack e = ns @ stack e

goal (2 subgoals):
 1. successors v - vsuccs e v = {} \<Longrightarrow> post_dfss v e (dfss v e)
 2. successors v - vsuccs e v \<noteq> {} \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<exists>ns. stack e = ns @ stack e

goal (2 subgoals):
 1. successors v - vsuccs e v = {} \<Longrightarrow> post_dfss v e (dfss v e)
 2. successors v - vsuccs e v \<noteq> {} \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<exists>ns. stack e = ns @ stack e

goal (2 subgoals):
 1. successors v - vsuccs e v = {} \<Longrightarrow> post_dfss v e (dfss v e)
 2. successors v - vsuccs e v \<noteq> {} \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. successors v - vsuccs e v = {} \<Longrightarrow> post_dfss v e (dfss v e)
 2. successors v - vsuccs e v \<noteq> {} \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
assume asm: "hd (stack e) = v"
                    "n \<in> set (tl (stack e))"
                    "reachable v n"
[PROOF STATE]
proof (state)
this:
hd (stack e) = v
n \<in> set (tl (stack e))
reachable v n

goal (2 subgoals):
 1. successors v - vsuccs e v = {} \<Longrightarrow> post_dfss v e (dfss v e)
 2. successors v - vsuccs e v \<noteq> {} \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
with \<open>stack e \<noteq> []\<close>
[PROOF STATE]
proof (chain)
picking this:
stack e \<noteq> []
hd (stack e) = v
n \<in> set (tl (stack e))
reachable v n
[PROOF STEP]
have "v \<preceq> n in stack e"
[PROOF STATE]
proof (prove)
using this:
stack e \<noteq> []
hd (stack e) = v
n \<in> set (tl (stack e))
reachable v n

goal (1 subgoal):
 1. v \<preceq> n in stack e
[PROOF STEP]
by (metis head_precedes hd_Cons_tl list.set_sel(2))
[PROOF STATE]
proof (state)
this:
v \<preceq> n in stack e

goal (2 subgoals):
 1. successors v - vsuccs e v = {} \<Longrightarrow> post_dfss v e (dfss v e)
 2. successors v - vsuccs e v \<noteq> {} \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
v \<preceq> n in stack e

goal (2 subgoals):
 1. successors v - vsuccs e v = {} \<Longrightarrow> post_dfss v e (dfss v e)
 2. successors v - vsuccs e v \<noteq> {} \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
from wf \<open>stack e \<noteq> []\<close> asm
[PROOF STATE]
proof (chain)
picking this:
wf_env e
stack e \<noteq> []
hd (stack e) = v
n \<in> set (tl (stack e))
reachable v n
[PROOF STEP]
have "v \<noteq> n"
[PROOF STATE]
proof (prove)
using this:
wf_env e
stack e \<noteq> []
hd (stack e) = v
n \<in> set (tl (stack e))
reachable v n

goal (1 subgoal):
 1. v \<noteq> n
[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
stack e \<noteq> []
hd (stack e) = v
n \<in> set (tl (stack e))
reachable v n

goal (1 subgoal):
 1. v \<noteq> n
[PROOF STEP]
by (metis distinct.simps(2) list.exhaust_sel)
[PROOF STATE]
proof (state)
this:
v \<noteq> n

goal (2 subgoals):
 1. successors v - vsuccs e v = {} \<Longrightarrow> post_dfss v e (dfss v e)
 2. successors v - vsuccs e v \<noteq> {} \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
v \<noteq> n

goal (2 subgoals):
 1. successors v - vsuccs e v = {} \<Longrightarrow> post_dfss v e (dfss v e)
 2. successors v - vsuccs e v \<noteq> {} \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
from wf
[PROOF STATE]
proof (chain)
picking this:
wf_env e
[PROOF STEP]
have "v \<in> \<S> e v"
[PROOF STATE]
proof (prove)
using this:
wf_env e

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

goal (2 subgoals):
 1. successors v - vsuccs e v = {} \<Longrightarrow> post_dfss v e (dfss v e)
 2. successors v - vsuccs e v \<noteq> {} \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
v \<in> \<S> e v

goal (2 subgoals):
 1. successors v - vsuccs e v = {} \<Longrightarrow> post_dfss v e (dfss v e)
 2. successors v - vsuccs e v \<noteq> {} \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
v \<in> \<S> e v

goal (2 subgoals):
 1. successors v - vsuccs e v = {} \<Longrightarrow> post_dfss v e (dfss v e)
 2. successors v - vsuccs e v \<noteq> {} \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
fix a b
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. successors v - vsuccs e v = {} \<Longrightarrow> post_dfss v e (dfss v e)
 2. successors v - vsuccs e v \<noteq> {} \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
assume "a \<in> \<S> e v" "b \<in> successors a - vsuccs e a"
[PROOF STATE]
proof (state)
this:
a \<in> \<S> e v
b \<in> successors a - vsuccs e a

goal (2 subgoals):
 1. successors v - vsuccs e v = {} \<Longrightarrow> post_dfss v e (dfss v e)
 2. successors v - vsuccs e v \<noteq> {} \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
with \<open>vsuccs e v = successors v\<close>
[PROOF STATE]
proof (chain)
picking this:
vsuccs e v = successors v
a \<in> \<S> e v
b \<in> successors a - vsuccs e a
[PROOF STEP]
have "a \<noteq> v"
[PROOF STATE]
proof (prove)
using this:
vsuccs e v = successors v
a \<in> \<S> e v
b \<in> successors a - vsuccs e a

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

goal (2 subgoals):
 1. successors v - vsuccs e v = {} \<Longrightarrow> post_dfss v e (dfss v e)
 2. successors v - vsuccs e v \<noteq> {} \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
from \<open>stack e \<noteq> []\<close> \<open>hd (stack e) = v\<close>
[PROOF STATE]
proof (chain)
picking this:
stack e \<noteq> []
hd (stack e) = v
[PROOF STEP]
have "v \<in> set (stack e)"
[PROOF STATE]
proof (prove)
using this:
stack e \<noteq> []
hd (stack e) = v

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

goal (2 subgoals):
 1. successors v - vsuccs e v = {} \<Longrightarrow> post_dfss v e (dfss v e)
 2. successors v - vsuccs e v \<noteq> {} \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
with \<open>a \<noteq> v\<close> \<open>a \<in> \<S> e v\<close> wf
[PROOF STATE]
proof (chain)
picking this:
a \<noteq> v
a \<in> \<S> e v
wf_env e
v \<in> set (stack e)
[PROOF STEP]
have "a \<in> visited e"
[PROOF STATE]
proof (prove)
using this:
a \<noteq> v
a \<in> \<S> e v
wf_env e
v \<in> set (stack e)

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

goal (1 subgoal):
 1. a \<in> visited e
[PROOF STEP]
by (metis singletonD)
[PROOF STATE]
proof (state)
this:
a \<in> visited e

goal (2 subgoals):
 1. successors v - vsuccs e v = {} \<Longrightarrow> post_dfss v e (dfss v e)
 2. successors v - vsuccs e v \<noteq> {} \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
have "False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
proof (cases "a \<in> set (cstack e)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a \<in> set (cstack e) \<Longrightarrow> False
 2. a \<notin> set (cstack e) \<Longrightarrow> False
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
a \<in> set (cstack e)

goal (2 subgoals):
 1. a \<in> set (cstack e) \<Longrightarrow> False
 2. a \<notin> set (cstack e) \<Longrightarrow> False
[PROOF STEP]
with \<open>v \<in> set (stack e)\<close> \<open>a \<in> \<S> e v\<close> \<open>wf_env e\<close>
[PROOF STATE]
proof (chain)
picking this:
v \<in> set (stack e)
a \<in> \<S> e v
wf_env e
a \<in> set (cstack e)
[PROOF STEP]
have "a \<preceq> v in cstack e"
[PROOF STATE]
proof (prove)
using this:
v \<in> set (stack e)
a \<in> \<S> e v
wf_env e
a \<in> set (cstack e)

goal (1 subgoal):
 1. a \<preceq> v in cstack e
[PROOF STEP]
by (auto simp: wf_env_def)
[PROOF STATE]
proof (state)
this:
a \<preceq> v in cstack e

goal (2 subgoals):
 1. a \<in> set (cstack e) \<Longrightarrow> False
 2. a \<notin> set (cstack e) \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
a \<preceq> v in cstack e

goal (2 subgoals):
 1. a \<in> set (cstack e) \<Longrightarrow> False
 2. a \<notin> set (cstack e) \<Longrightarrow> False
[PROOF STEP]
from predfss
[PROOF STATE]
proof (chain)
picking this:
pre_dfss v e
[PROOF STEP]
obtain ns where "cstack e = v # ns"
[PROOF STATE]
proof (prove)
using this:
pre_dfss v e

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

goal (2 subgoals):
 1. a \<in> set (cstack e) \<Longrightarrow> False
 2. a \<notin> set (cstack e) \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
cstack e = v # ns

goal (2 subgoals):
 1. a \<in> set (cstack e) \<Longrightarrow> False
 2. a \<notin> set (cstack e) \<Longrightarrow> False
[PROOF STEP]
from wf
[PROOF STATE]
proof (chain)
picking this:
wf_env e
[PROOF STEP]
have "distinct (cstack e)"
[PROOF STATE]
proof (prove)
using this:
wf_env e

goal (1 subgoal):
 1. distinct (cstack e)
[PROOF STEP]
by (simp add: wf_env_def)
[PROOF STATE]
proof (state)
this:
distinct (cstack e)

goal (2 subgoals):
 1. a \<in> set (cstack e) \<Longrightarrow> False
 2. a \<notin> set (cstack e) \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
a \<preceq> v in cstack e
cstack e = v # ns
distinct (cstack e)
[PROOF STEP]
have "a = v"
[PROOF STATE]
proof (prove)
using this:
a \<preceq> v in cstack e
cstack e = v # ns
distinct (cstack e)

goal (1 subgoal):
 1. a = v
[PROOF STEP]
using tail_not_precedes
[PROOF STATE]
proof (prove)
using this:
a \<preceq> v in cstack e
cstack e = v # ns
distinct (cstack e)
\<lbrakk>?y \<preceq> ?x in (?x # ?xs); ?x \<notin> set ?xs\<rbrakk> \<Longrightarrow> ?x = ?y

goal (1 subgoal):
 1. a = v
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
a = v

goal (2 subgoals):
 1. a \<in> set (cstack e) \<Longrightarrow> False
 2. a \<notin> set (cstack e) \<Longrightarrow> False
[PROOF STEP]
with \<open>a \<noteq> v\<close>
[PROOF STATE]
proof (chain)
picking this:
a \<noteq> v
a = v
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a \<noteq> v
a = v

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

goal (1 subgoal):
 1. a \<notin> set (cstack e) \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<notin> set (cstack e) \<Longrightarrow> False
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
a \<notin> set (cstack e)

goal (1 subgoal):
 1. a \<notin> set (cstack e) \<Longrightarrow> False
[PROOF STEP]
with \<open>a \<in> visited e\<close> wf
[PROOF STATE]
proof (chain)
picking this:
a \<in> visited e
wf_env e
a \<notin> set (cstack e)
[PROOF STEP]
have "vsuccs e a = successors a"
[PROOF STATE]
proof (prove)
using this:
a \<in> visited e
wf_env e
a \<notin> set (cstack e)

goal (1 subgoal):
 1. vsuccs e a = successors a
[PROOF STEP]
by (auto simp: wf_env_def)
[PROOF STATE]
proof (state)
this:
vsuccs e a = successors a

goal (1 subgoal):
 1. a \<notin> set (cstack e) \<Longrightarrow> False
[PROOF STEP]
with \<open>b \<in> successors a - vsuccs e a\<close>
[PROOF STATE]
proof (chain)
picking this:
b \<in> successors a - vsuccs e a
vsuccs e a = successors a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
b \<in> successors a - vsuccs e a
vsuccs e a = successors a

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

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

goal (2 subgoals):
 1. successors v - vsuccs e v = {} \<Longrightarrow> post_dfss v e (dfss v e)
 2. successors v - vsuccs e v \<noteq> {} \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?a8 \<in> \<S> e v; ?b8 \<in> successors ?a8 - vsuccs e ?a8\<rbrakk> \<Longrightarrow> False

goal (2 subgoals):
 1. successors v - vsuccs e v = {} \<Longrightarrow> post_dfss v e (dfss v e)
 2. successors v - vsuccs e v \<noteq> {} \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
hence "unvisited e v = {}"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?a8 \<in> \<S> e v; ?b8 \<in> successors ?a8 - vsuccs e ?a8\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. unvisited e v = {}
[PROOF STEP]
by (auto simp: unvisited_def)
[PROOF STATE]
proof (state)
this:
unvisited e v = {}

goal (2 subgoals):
 1. successors v - vsuccs e v = {} \<Longrightarrow> post_dfss v e (dfss v e)
 2. successors v - vsuccs e v \<noteq> {} \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
v \<preceq> n in stack e
v \<noteq> n
v \<in> \<S> e v
unvisited e v = {}
[PROOF STEP]
have "\<not> reachable_avoiding v n {}"
[PROOF STATE]
proof (prove)
using this:
v \<preceq> n in stack e
v \<noteq> n
v \<in> \<S> e v
unvisited e v = {}

goal (1 subgoal):
 1. \<not> reachable_avoiding v n {}
[PROOF STEP]
using wf
[PROOF STATE]
proof (prove)
using this:
v \<preceq> n in stack e
v \<noteq> n
v \<in> \<S> e v
unvisited e v = {}
wf_env e

goal (1 subgoal):
 1. \<not> reachable_avoiding v n {}
[PROOF STEP]
unfolding wf_env_def
[PROOF STATE]
proof (prove)
using this:
v \<preceq> n in stack e
v \<noteq> n
v \<in> \<S> e v
unvisited e v = {}
(\<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

goal (1 subgoal):
 1. \<not> reachable_avoiding v n {}
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<not> reachable_avoiding v n {}

goal (2 subgoals):
 1. successors v - vsuccs e v = {} \<Longrightarrow> post_dfss v e (dfss v e)
 2. successors v - vsuccs e v \<noteq> {} \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
with \<open>reachable v n\<close>
[PROOF STATE]
proof (chain)
picking this:
reachable v n
\<not> reachable_avoiding v n {}
[PROOF STEP]
have "False"
[PROOF STATE]
proof (prove)
using this:
reachable v n
\<not> reachable_avoiding v n {}

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

goal (2 subgoals):
 1. successors v - vsuccs e v = {} \<Longrightarrow> post_dfss v e (dfss v e)
 2. successors v - vsuccs e v \<noteq> {} \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>hd (stack e) = v; ?n8 \<in> set (tl (stack e)); reachable v ?n8\<rbrakk> \<Longrightarrow> False

goal (2 subgoals):
 1. successors v - vsuccs e v = {} \<Longrightarrow> post_dfss v e (dfss v e)
 2. successors v - vsuccs e v \<noteq> {} \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
dfss v e = e
vsuccs e v = successors v
sub_env e e
\<forall>w\<in>successors v. w \<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. stack e = ns @ stack e
\<lbrakk>hd (stack e) = v; ?n8 \<in> set (tl (stack e)); reachable v ?n8\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dfss v e = e
vsuccs e v = successors v
sub_env e e
\<forall>w\<in>successors v. w \<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. stack e = ns @ stack e
\<lbrakk>hd (stack e) = v; ?n8 \<in> set (tl (stack e)); reachable v ?n8\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. post_dfss v e (dfss v e)
[PROOF STEP]
using wf
[PROOF STATE]
proof (prove)
using this:
dfss v e = e
vsuccs e v = successors v
sub_env e e
\<forall>w\<in>successors v. w \<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. stack e = ns @ stack e
\<lbrakk>hd (stack e) = v; ?n8 \<in> set (tl (stack e)); reachable v ?n8\<rbrakk> \<Longrightarrow> False
wf_env e

goal (1 subgoal):
 1. post_dfss v e (dfss v e)
[PROOF STEP]
by (auto simp: post_dfss_def)
[PROOF STATE]
proof (state)
this:
post_dfss v e (dfss v e)

goal (1 subgoal):
 1. successors v - vsuccs e v \<noteq> {} \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. successors v - vsuccs e v \<noteq> {} \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
case vs_case: False
[PROOF STATE]
proof (state)
this:
successors v - vsuccs e v \<noteq> {}

goal (1 subgoal):
 1. successors v - vsuccs e v \<noteq> {} \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
define w where "w = (SOME x. x \<in> ?vs)"
[PROOF STATE]
proof (state)
this:
w = (SOME x. x \<in> successors v - vsuccs e v)

goal (1 subgoal):
 1. successors v - vsuccs e v \<noteq> {} \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
define e' where "e' = (if w \<in> explored e then e
                             else if w \<notin> visited e then dfs w e
                             else unite v w e)"
[PROOF STATE]
proof (state)
this:
e' = (if w \<in> explored e then e else if w \<notin> visited e then dfs w e else unite v w e)

goal (1 subgoal):
 1. successors v - vsuccs e v \<noteq> {} \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
define e'' where "e'' = (e'\<lparr>vsuccs := \<lambda>x. if x=v then vsuccs e' v \<union> {w} else vsuccs e' x\<rparr>)"
[PROOF STATE]
proof (state)
this:
e'' = e'\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e' v \<union> {w} else vsuccs e' x\<rparr>

goal (1 subgoal):
 1. successors v - vsuccs e v \<noteq> {} \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
from dom vs_case
[PROOF STATE]
proof (chain)
picking this:
dfs_dfss_dom (Inr (v, e))
successors v - vsuccs e v \<noteq> {}
[PROOF STEP]
have dfss: "dfss v e = dfss v e''"
[PROOF STATE]
proof (prove)
using this:
dfs_dfss_dom (Inr (v, e))
successors v - vsuccs e v \<noteq> {}

goal (1 subgoal):
 1. dfss v e = dfss v e''
[PROOF STEP]
apply (simp add: dfss.psimps e''_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>dfs_dfss_dom (Inr (v, e)); \<not> successors v \<subseteq> vsuccs e v\<rbrakk> \<Longrightarrow> ((SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> visited e \<longrightarrow> ((SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e \<longrightarrow> dfss v (e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>) = dfss v (e'\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e' v \<union> {w} else vsuccs e' x\<rparr>)) \<and> ((SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e \<longrightarrow> dfss v (dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>) = dfss v (e'\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e' v \<union> {w} else vsuccs e' x\<rparr>))) \<and> ((SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e \<longrightarrow> ((SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e \<longrightarrow> dfss v (e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>) = dfss v (e'\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e' v \<union> {w} else vsuccs e' x\<rparr>)) \<and> ((SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e \<longrightarrow> dfss v (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>) = dfss v (e'\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e' v \<union> {w} else vsuccs e' x\<rparr>)))
[PROOF STEP]
using e'_def w_def
[PROOF STATE]
proof (prove)
using this:
e' = (if w \<in> explored e then e else if w \<notin> visited e then dfs w e else unite v w e)
w = (SOME x. x \<in> successors v - vsuccs e v)

goal (1 subgoal):
 1. \<lbrakk>dfs_dfss_dom (Inr (v, e)); \<not> successors v \<subseteq> vsuccs e v\<rbrakk> \<Longrightarrow> ((SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> visited e \<longrightarrow> ((SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e \<longrightarrow> dfss v (e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>) = dfss v (e'\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e' v \<union> {w} else vsuccs e' x\<rparr>)) \<and> ((SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e \<longrightarrow> dfss v (dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (dfs (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>) = dfss v (e'\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e' v \<union> {w} else vsuccs e' x\<rparr>))) \<and> ((SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> visited e \<longrightarrow> ((SOME x. edge v x \<and> x \<notin> vsuccs e v) \<in> explored e \<longrightarrow> dfss v (e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs e x\<rparr>) = dfss v (e'\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e' v \<union> {w} else vsuccs e' x\<rparr>)) \<and> ((SOME x. edge v x \<and> x \<notin> vsuccs e v) \<notin> explored e \<longrightarrow> dfss v (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) v \<union> {SOME x. edge v x \<and> x \<notin> vsuccs e v} else vsuccs (unite v (SOME x. edge v x \<and> x \<notin> vsuccs e v) e) x\<rparr>) = dfss v (e'\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e' v \<union> {w} else vsuccs e' x\<rparr>)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dfss v e = dfss v e''

goal (1 subgoal):
 1. successors v - vsuccs e v \<noteq> {} \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
from vs_case
[PROOF STATE]
proof (chain)
picking this:
successors v - vsuccs e v \<noteq> {}
[PROOF STEP]
have wvs: "w \<in> ?vs"
[PROOF STATE]
proof (prove)
using this:
successors v - vsuccs e v \<noteq> {}

goal (1 subgoal):
 1. w \<in> successors v - vsuccs e v
[PROOF STEP]
unfolding w_def
[PROOF STATE]
proof (prove)
using this:
successors v - vsuccs e v \<noteq> {}

goal (1 subgoal):
 1. (SOME x. x \<in> successors v - vsuccs e v) \<in> successors v - vsuccs e v
[PROOF STEP]
by (metis some_in_eq)
[PROOF STATE]
proof (state)
this:
w \<in> successors v - vsuccs e v

goal (1 subgoal):
 1. successors v - vsuccs e v \<noteq> {} \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. post_dfss v e (dfss v e)
[PROOF STEP]
proof (cases "w \<in> explored e")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. w \<in> explored e \<Longrightarrow> post_dfss v e (dfss v e)
 2. w \<notin> explored e \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
w \<in> explored e

goal (2 subgoals):
 1. w \<in> explored e \<Longrightarrow> post_dfss v e (dfss v e)
 2. w \<notin> explored e \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
hence e': "e' = e"
[PROOF STATE]
proof (prove)
using this:
w \<in> explored e

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

goal (2 subgoals):
 1. w \<in> explored e \<Longrightarrow> post_dfss v e (dfss v e)
 2. w \<notin> explored e \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
with predfss wvs True
[PROOF STATE]
proof (chain)
picking this:
pre_dfss v e
w \<in> successors v - vsuccs e v
w \<in> explored e
e' = e
[PROOF STEP]
have "pre_dfss v e''"
[PROOF STATE]
proof (prove)
using this:
pre_dfss v e
w \<in> successors v - vsuccs e v
w \<in> explored e
e' = e

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

goal (2 subgoals):
 1. w \<in> explored e \<Longrightarrow> post_dfss v e (dfss v e)
 2. w \<notin> explored e \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
with prepostdfss vs_case
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?vs6 = successors v - vsuccs e v; ?vs6 \<noteq> {}; ?w6 = (SOME x. x \<in> ?vs6); ?e'6 = (if ?w6 \<in> explored e then e else if ?w6 \<notin> visited e then dfs ?w6 e else unite v ?w6 e); ?e''6 = ?e'6\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs ?e'6 v \<union> {?w6} else vsuccs ?e'6 x\<rparr>; pre_dfss v ?e''6\<rbrakk> \<Longrightarrow> post_dfss v ?e''6 (dfss v ?e''6)
successors v - vsuccs e v \<noteq> {}
pre_dfss v e''
[PROOF STEP]
have post'': "post_dfss v e'' (dfss v e'')"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?vs6 = successors v - vsuccs e v; ?vs6 \<noteq> {}; ?w6 = (SOME x. x \<in> ?vs6); ?e'6 = (if ?w6 \<in> explored e then e else if ?w6 \<notin> visited e then dfs ?w6 e else unite v ?w6 e); ?e''6 = ?e'6\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs ?e'6 v \<union> {?w6} else vsuccs ?e'6 x\<rparr>; pre_dfss v ?e''6\<rbrakk> \<Longrightarrow> post_dfss v ?e''6 (dfss v ?e''6)
successors v - vsuccs e v \<noteq> {}
pre_dfss v e''

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

goal (2 subgoals):
 1. w \<in> explored e \<Longrightarrow> post_dfss v e (dfss v e)
 2. w \<notin> explored e \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
post_dfss v e'' (dfss v e'')

goal (2 subgoals):
 1. w \<in> explored e \<Longrightarrow> post_dfss v e (dfss v e)
 2. w \<notin> explored e \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
from post''
[PROOF STATE]
proof (chain)
picking this:
post_dfss v e'' (dfss v e'')
[PROOF STEP]
have "\<forall>u \<in> visited e - {v}. vsuccs (dfss v e'') u = vsuccs e u"
[PROOF STATE]
proof (prove)
using this:
post_dfss v e'' (dfss v e'')

goal (1 subgoal):
 1. \<forall>u\<in>visited e - {v}. vsuccs (dfss v e'') u = vsuccs e u
[PROOF STEP]
by (auto simp: post_dfss_def e' e''_def)
[PROOF STATE]
proof (state)
this:
\<forall>u\<in>visited e - {v}. vsuccs (dfss v e'') u = vsuccs e u

goal (2 subgoals):
 1. w \<in> explored e \<Longrightarrow> post_dfss v e (dfss v e)
 2. w \<notin> explored e \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>u\<in>visited e - {v}. vsuccs (dfss v e'') u = vsuccs e u

goal (2 subgoals):
 1. w \<in> explored e \<Longrightarrow> post_dfss v e (dfss v e)
 2. w \<notin> explored e \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
have "sub_env e e''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sub_env e e''
[PROOF STEP]
by (auto simp: sub_env_def e' e''_def)
[PROOF STATE]
proof (state)
this:
sub_env e e''

goal (2 subgoals):
 1. w \<in> explored e \<Longrightarrow> post_dfss v e (dfss v e)
 2. w \<notin> explored e \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
with post''
[PROOF STATE]
proof (chain)
picking this:
post_dfss v e'' (dfss v e'')
sub_env e e''
[PROOF STEP]
have "sub_env e (dfss v e'')"
[PROOF STATE]
proof (prove)
using this:
post_dfss v e'' (dfss v e'')
sub_env e e''

goal (1 subgoal):
 1. sub_env e (dfss v e'')
[PROOF STEP]
by (auto simp: post_dfss_def elim: sub_env_trans)
[PROOF STATE]
proof (state)
this:
sub_env e (dfss v e'')

goal (2 subgoals):
 1. w \<in> explored e \<Longrightarrow> post_dfss v e (dfss v e)
 2. w \<notin> explored e \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sub_env e (dfss v e'')

goal (2 subgoals):
 1. w \<in> explored e \<Longrightarrow> post_dfss v e (dfss v e)
 2. w \<notin> explored e \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
from e'
[PROOF STATE]
proof (chain)
picking this:
e' = e
[PROOF STEP]
have "stack e'' = stack e" "\<S> e'' = \<S> e"
[PROOF STATE]
proof (prove)
using this:
e' = e

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

goal (2 subgoals):
 1. w \<in> explored e \<Longrightarrow> post_dfss v e (dfss v e)
 2. w \<notin> explored e \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
stack e'' = stack e
\<S> e'' = \<S> e

goal (2 subgoals):
 1. w \<in> explored e \<Longrightarrow> post_dfss v e (dfss v e)
 2. w \<notin> explored e \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
have "cstack e'' = cstack e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cstack e'' = cstack e
[PROOF STEP]
by (simp add: e''_def e')
[PROOF STATE]
proof (state)
this:
cstack e'' = cstack e

goal (2 subgoals):
 1. w \<in> explored e \<Longrightarrow> post_dfss v e (dfss v e)
 2. w \<notin> explored e \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
post_dfss v e'' (dfss v e'')
\<forall>u\<in>visited e - {v}. vsuccs (dfss v e'') u = vsuccs e u
sub_env e (dfss v e'')
stack e'' = stack e
\<S> e'' = \<S> e
cstack e'' = cstack e
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
post_dfss v e'' (dfss v e'')
\<forall>u\<in>visited e - {v}. vsuccs (dfss v e'') u = vsuccs e u
sub_env e (dfss v e'')
stack e'' = stack e
\<S> e'' = \<S> e
cstack e'' = cstack e

goal (1 subgoal):
 1. post_dfss v e (dfss v e)
[PROOF STEP]
by (auto simp: dfss post_dfss_def)
[PROOF STATE]
proof (state)
this:
post_dfss v e (dfss v e)

goal (1 subgoal):
 1. w \<notin> explored e \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. w \<notin> explored e \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
case notexplored: False
[PROOF STATE]
proof (state)
this:
w \<notin> explored e

goal (1 subgoal):
 1. w \<notin> explored e \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
w \<notin> explored e
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
w \<notin> explored e

goal (1 subgoal):
 1. post_dfss v e (dfss v e)
[PROOF STEP]
proof (cases "w \<notin> visited e")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>w \<notin> explored e; w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
 2. \<lbrakk>w \<notin> explored e; \<not> w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
w \<notin> visited e

goal (2 subgoals):
 1. \<lbrakk>w \<notin> explored e; w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
 2. \<lbrakk>w \<notin> explored e; \<not> w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
with e'_def notexplored
[PROOF STATE]
proof (chain)
picking this:
e' = (if w \<in> explored e then e else if w \<notin> visited e then dfs w e else unite v w e)
w \<notin> explored e
w \<notin> visited e
[PROOF STEP]
have "e' = dfs w e"
[PROOF STATE]
proof (prove)
using this:
e' = (if w \<in> explored e then e else if w \<notin> visited e then dfs w e else unite v w e)
w \<notin> explored e
w \<notin> visited e

goal (1 subgoal):
 1. e' = dfs w e
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
e' = dfs w e

goal (2 subgoals):
 1. \<lbrakk>w \<notin> explored e; w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
 2. \<lbrakk>w \<notin> explored e; \<not> w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
with True notexplored pre_dfss_pre_dfs predfss
               prepostdfs vs_case w_def
[PROOF STATE]
proof (chain)
picking this:
w \<notin> visited e
w \<notin> explored e
\<lbrakk>pre_dfss ?v ?e; ?w \<notin> visited ?e; edge ?v ?w\<rbrakk> \<Longrightarrow> pre_dfs ?w ?e
pre_dfss v e
\<lbrakk>?vs6 = successors v - vsuccs e v; ?vs6 \<noteq> {}; ?w6 = (SOME x. x \<in> ?vs6); ?w6 \<notin> explored e; ?w6 \<notin> visited e; pre_dfs ?w6 e\<rbrakk> \<Longrightarrow> post_dfs ?w6 e (dfs ?w6 e)
successors v - vsuccs e v \<noteq> {}
w = (SOME x. x \<in> successors v - vsuccs e v)
e' = dfs w e
[PROOF STEP]
have postdfsw: "post_dfs w e e'"
[PROOF STATE]
proof (prove)
using this:
w \<notin> visited e
w \<notin> explored e
\<lbrakk>pre_dfss ?v ?e; ?w \<notin> visited ?e; edge ?v ?w\<rbrakk> \<Longrightarrow> pre_dfs ?w ?e
pre_dfss v e
\<lbrakk>?vs6 = successors v - vsuccs e v; ?vs6 \<noteq> {}; ?w6 = (SOME x. x \<in> ?vs6); ?w6 \<notin> explored e; ?w6 \<notin> visited e; pre_dfs ?w6 e\<rbrakk> \<Longrightarrow> post_dfs ?w6 e (dfs ?w6 e)
successors v - vsuccs e v \<noteq> {}
w = (SOME x. x \<in> successors v - vsuccs e v)
e' = dfs w e

goal (1 subgoal):
 1. post_dfs w e e'
[PROOF STEP]
by (metis DiffD1 some_in_eq)
[PROOF STATE]
proof (state)
this:
post_dfs w e e'

goal (2 subgoals):
 1. \<lbrakk>w \<notin> explored e; w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
 2. \<lbrakk>w \<notin> explored e; \<not> w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
with predfss wvs True \<open>e' = dfs w e\<close>
[PROOF STATE]
proof (chain)
picking this:
pre_dfss v e
w \<in> successors v - vsuccs e v
w \<notin> visited e
e' = dfs w e
post_dfs w e e'
[PROOF STEP]
have "pre_dfss v e''"
[PROOF STATE]
proof (prove)
using this:
pre_dfss v e
w \<in> successors v - vsuccs e v
w \<notin> visited e
e' = dfs w e
post_dfs w e e'

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

goal (2 subgoals):
 1. \<lbrakk>w \<notin> explored e; w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
 2. \<lbrakk>w \<notin> explored e; \<not> w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
with prepostdfss vs_case
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?vs6 = successors v - vsuccs e v; ?vs6 \<noteq> {}; ?w6 = (SOME x. x \<in> ?vs6); ?e'6 = (if ?w6 \<in> explored e then e else if ?w6 \<notin> visited e then dfs ?w6 e else unite v ?w6 e); ?e''6 = ?e'6\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs ?e'6 v \<union> {?w6} else vsuccs ?e'6 x\<rparr>; pre_dfss v ?e''6\<rbrakk> \<Longrightarrow> post_dfss v ?e''6 (dfss v ?e''6)
successors v - vsuccs e v \<noteq> {}
pre_dfss v e''
[PROOF STEP]
have post'': "post_dfss v e'' (dfss v e'')"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?vs6 = successors v - vsuccs e v; ?vs6 \<noteq> {}; ?w6 = (SOME x. x \<in> ?vs6); ?e'6 = (if ?w6 \<in> explored e then e else if ?w6 \<notin> visited e then dfs ?w6 e else unite v ?w6 e); ?e''6 = ?e'6\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs ?e'6 v \<union> {?w6} else vsuccs ?e'6 x\<rparr>; pre_dfss v ?e''6\<rbrakk> \<Longrightarrow> post_dfss v ?e''6 (dfss v ?e''6)
successors v - vsuccs e v \<noteq> {}
pre_dfss v e''

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

goal (2 subgoals):
 1. \<lbrakk>w \<notin> explored e; w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
 2. \<lbrakk>w \<notin> explored e; \<not> w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
post_dfss v e'' (dfss v e'')

goal (2 subgoals):
 1. \<lbrakk>w \<notin> explored e; w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
 2. \<lbrakk>w \<notin> explored e; \<not> w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
have "\<forall>u \<in> visited e - {v}. vsuccs (dfss v e'') u = vsuccs e u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>u\<in>visited e - {v}. vsuccs (dfss v e'') u = vsuccs e u
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u. u \<in> visited e - {v} \<Longrightarrow> vsuccs (dfss v e'') u = vsuccs e u
[PROOF STEP]
fix u
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u. u \<in> visited e - {v} \<Longrightarrow> vsuccs (dfss v e'') u = vsuccs e u
[PROOF STEP]
assume "u \<in> visited e - {v}"
[PROOF STATE]
proof (state)
this:
u \<in> visited e - {v}

goal (1 subgoal):
 1. \<And>u. u \<in> visited e - {v} \<Longrightarrow> vsuccs (dfss v e'') u = vsuccs e u
[PROOF STEP]
with postdfsw
[PROOF STATE]
proof (chain)
picking this:
post_dfs w e e'
u \<in> visited e - {v}
[PROOF STEP]
have u: "vsuccs e' u = vsuccs e u" "u \<in> visited e'' - {v}"
[PROOF STATE]
proof (prove)
using this:
post_dfs w e e'
u \<in> visited e - {v}

goal (1 subgoal):
 1. vsuccs e' u = vsuccs e u &&& u \<in> visited e'' - {v}
[PROOF STEP]
by (auto simp: post_dfs_def sub_env_def e''_def)
[PROOF STATE]
proof (state)
this:
vsuccs e' u = vsuccs e u
u \<in> visited e'' - {v}

goal (1 subgoal):
 1. \<And>u. u \<in> visited e - {v} \<Longrightarrow> vsuccs (dfss v e'') u = vsuccs e u
[PROOF STEP]
with post''
[PROOF STATE]
proof (chain)
picking this:
post_dfss v e'' (dfss v e'')
vsuccs e' u = vsuccs e u
u \<in> visited e'' - {v}
[PROOF STEP]
have "vsuccs (dfss v e'') u = vsuccs e'' u"
[PROOF STATE]
proof (prove)
using this:
post_dfss v e'' (dfss v e'')
vsuccs e' u = vsuccs e u
u \<in> visited e'' - {v}

goal (1 subgoal):
 1. vsuccs (dfss v e'') u = vsuccs e'' u
[PROOF STEP]
by (auto simp: post_dfss_def)
[PROOF STATE]
proof (state)
this:
vsuccs (dfss v e'') u = vsuccs e'' u

goal (1 subgoal):
 1. \<And>u. u \<in> visited e - {v} \<Longrightarrow> vsuccs (dfss v e'') u = vsuccs e u
[PROOF STEP]
with u
[PROOF STATE]
proof (chain)
picking this:
vsuccs e' u = vsuccs e u
u \<in> visited e'' - {v}
vsuccs (dfss v e'') u = vsuccs e'' u
[PROOF STEP]
show "vsuccs (dfss v e'') u = vsuccs e u"
[PROOF STATE]
proof (prove)
using this:
vsuccs e' u = vsuccs e u
u \<in> visited e'' - {v}
vsuccs (dfss v e'') u = vsuccs e'' u

goal (1 subgoal):
 1. vsuccs (dfss v e'') u = vsuccs e u
[PROOF STEP]
by (simp add: e''_def)
[PROOF STATE]
proof (state)
this:
vsuccs (dfss v e'') u = vsuccs e u

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>u\<in>visited e - {v}. vsuccs (dfss v e'') u = vsuccs e u

goal (2 subgoals):
 1. \<lbrakk>w \<notin> explored e; w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
 2. \<lbrakk>w \<notin> explored e; \<not> w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>u\<in>visited e - {v}. vsuccs (dfss v e'') u = vsuccs e u

goal (2 subgoals):
 1. \<lbrakk>w \<notin> explored e; w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
 2. \<lbrakk>w \<notin> explored e; \<not> w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
have "sub_env e (dfss v e'')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sub_env e (dfss v e'')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sub_env e (dfss v e'')
[PROOF STEP]
from postdfsw
[PROOF STATE]
proof (chain)
picking this:
post_dfs w e e'
[PROOF STEP]
have "sub_env e e'"
[PROOF STATE]
proof (prove)
using this:
post_dfs w e e'

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

goal (1 subgoal):
 1. sub_env e (dfss v e'')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sub_env e e'

goal (1 subgoal):
 1. sub_env e (dfss v e'')
[PROOF STEP]
have "sub_env e' e''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sub_env e' e''
[PROOF STEP]
by (auto simp: sub_env_def e''_def)
[PROOF STATE]
proof (state)
this:
sub_env e' e''

goal (1 subgoal):
 1. sub_env e (dfss v e'')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sub_env e' e''

goal (1 subgoal):
 1. sub_env e (dfss v e'')
[PROOF STEP]
from post''
[PROOF STATE]
proof (chain)
picking this:
post_dfss v e'' (dfss v e'')
[PROOF STEP]
have "sub_env e'' (dfss v e'')"
[PROOF STATE]
proof (prove)
using this:
post_dfss v e'' (dfss v e'')

goal (1 subgoal):
 1. sub_env e'' (dfss v e'')
[PROOF STEP]
by (simp add: post_dfss_def)
[PROOF STATE]
proof (state)
this:
sub_env e'' (dfss v e'')

goal (1 subgoal):
 1. sub_env e (dfss v e'')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
sub_env e e'
sub_env e' e''
sub_env e'' (dfss v e'')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sub_env e e'
sub_env e' e''
sub_env e'' (dfss v e'')

goal (1 subgoal):
 1. sub_env e (dfss v e'')
[PROOF STEP]
by (metis sub_env_trans)
[PROOF STATE]
proof (state)
this:
sub_env e (dfss v e'')

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

goal (2 subgoals):
 1. \<lbrakk>w \<notin> explored e; w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
 2. \<lbrakk>w \<notin> explored e; \<not> w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sub_env e (dfss v e'')

goal (2 subgoals):
 1. \<lbrakk>w \<notin> explored e; w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
 2. \<lbrakk>w \<notin> explored e; \<not> w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
from postdfsw post''
[PROOF STATE]
proof (chain)
picking this:
post_dfs w e e'
post_dfss v e'' (dfss v e'')
[PROOF STEP]
have "\<exists>ns. stack e = ns @ (stack (dfss v e''))"
[PROOF STATE]
proof (prove)
using this:
post_dfs w e e'
post_dfss v e'' (dfss v e'')

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

goal (2 subgoals):
 1. \<lbrakk>w \<notin> explored e; w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
 2. \<lbrakk>w \<notin> explored e; \<not> w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<exists>ns. stack e = ns @ stack (dfss v e'')

goal (2 subgoals):
 1. \<lbrakk>w \<notin> explored e; w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
 2. \<lbrakk>w \<notin> explored e; \<not> w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<exists>ns. stack e = ns @ stack (dfss v e'')

goal (2 subgoals):
 1. \<lbrakk>w \<notin> explored e; w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
 2. \<lbrakk>w \<notin> explored e; \<not> w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>w \<notin> explored e; w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
 2. \<lbrakk>w \<notin> explored e; \<not> w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
assume n: "n \<in> set (tl (stack (dfss v e'')))"
[PROOF STATE]
proof (state)
this:
n \<in> set (tl (stack (dfss v e'')))

goal (2 subgoals):
 1. \<lbrakk>w \<notin> explored e; w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
 2. \<lbrakk>w \<notin> explored e; \<not> w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
with post''
[PROOF STATE]
proof (chain)
picking this:
post_dfss v e'' (dfss v e'')
n \<in> set (tl (stack (dfss v e'')))
[PROOF STEP]
have "\<S> (dfss v e'') n = \<S> e' n"
[PROOF STATE]
proof (prove)
using this:
post_dfss v e'' (dfss v e'')
n \<in> set (tl (stack (dfss v e'')))

goal (1 subgoal):
 1. \<S> (dfss v e'') n = \<S> e' n
[PROOF STEP]
by (simp add: post_dfss_def e''_def)
[PROOF STATE]
proof (state)
this:
\<S> (dfss v e'') n = \<S> e' n

goal (2 subgoals):
 1. \<lbrakk>w \<notin> explored e; w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
 2. \<lbrakk>w \<notin> explored e; \<not> w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<S> (dfss v e'') n = \<S> e' n

goal (2 subgoals):
 1. \<lbrakk>w \<notin> explored e; w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
 2. \<lbrakk>w \<notin> explored e; \<not> w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
from \<open>pre_dfss v e''\<close> n post''
[PROOF STATE]
proof (chain)
picking this:
pre_dfss v e''
n \<in> set (tl (stack (dfss v e'')))
post_dfss v e'' (dfss v e'')
[PROOF STEP]
have "stack e' \<noteq> [] \<and> n \<in> set (tl (stack e''))"
[PROOF STATE]
proof (prove)
using this:
pre_dfss v e''
n \<in> set (tl (stack (dfss v e'')))
post_dfss v e'' (dfss v e'')

goal (1 subgoal):
 1. stack e' \<noteq> [] \<and> n \<in> set (tl (stack e''))
[PROOF STEP]
apply (simp add: pre_dfss_def post_dfss_def e''_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wf_env (e'\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e' v \<union> {w} else vsuccs e' x\<rparr>) \<and> v \<in> visited e' \<and> stack e' \<noteq> [] \<and> v \<in> \<S> e' (hd (stack e')) \<and> (w \<in> explored e' \<or> w \<in> \<S> e' (hd (stack e'))) \<and> (\<forall>w\<in>vsuccs e' v. w \<in> explored e' \<or> w \<in> \<S> e' (hd (stack e'))) \<and> (\<forall>n\<in>set (stack e'). reachable n v) \<and> (\<exists>ns. cstack e' = v # ns); n \<in> set (tl (stack (dfss v (e'\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e' v \<union> {w} else vsuccs e' x\<rparr>)))); wf_env (dfss v (e'\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e' v \<union> {w} else vsuccs e' x\<rparr>)) \<and> vsuccs (dfss v (e'\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e' v \<union> {w} else vsuccs e' x\<rparr>)) v = successors v \<and> (\<forall>wa\<in>visited e' - {v}. vsuccs (dfss v (e'\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e' v \<union> {w} else vsuccs e' x\<rparr>)) wa = vsuccs e' wa) \<and> sub_env (e'\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e' v \<union> {w} else vsuccs e' x\<rparr>) (dfss v (e'\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e' v \<union> {w} else vsuccs e' x\<rparr>)) \<and> (\<forall>wa\<in>successors v. wa \<in> explored (dfss v (e'\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e' v \<union> {w} else vsuccs e' x\<rparr>)) \<or> wa \<in> \<S> (dfss v (e'\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e' v \<union> {w} else vsuccs e' x\<rparr>)) (hd (stack (dfss v (e'\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e' v \<union> {w} else vsuccs e' x\<rparr>))))) \<and> (\<forall>n\<in>set (stack (dfss v (e'\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e' v \<union> {w} else vsuccs e' x\<rparr>))). reachable n v) \<and> stack (dfss v (e'\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e' v \<union> {w} else vsuccs e' x\<rparr>)) \<noteq> [] \<and> (\<exists>ns. stack e' = ns @ stack (dfss v (e'\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e' v \<union> {w} else vsuccs e' x\<rparr>))) \<and> v \<in> \<S> (dfss v (e'\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e' v \<union> {w} else vsuccs e' x\<rparr>)) (hd (stack (dfss v (e'\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e' v \<union> {w} else vsuccs e' x\<rparr>)))) \<and> (\<forall>n\<in>set (tl (stack (dfss v (e'\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e' v \<union> {w} else vsuccs e' x\<rparr>)))). \<S> (dfss v (e'\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e' v \<union> {w} else vsuccs e' x\<rparr>)) n = \<S> e' n) \<and> (hd (stack (dfss v (e'\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e' v \<union> {w} else vsuccs e' x\<rparr>))) = v \<longrightarrow> (\<forall>n\<in>set (tl (stack (dfss v (e'\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e' v \<union> {w} else vsuccs e' x\<rparr>)))). \<not> reachable v n)) \<and> cstack (dfss v (e'\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e' v \<union> {w} else vsuccs e' x\<rparr>)) = cstack e'\<rbrakk> \<Longrightarrow> n \<in> set (tl (stack e'))
[PROOF STEP]
by (metis (no_types, lifting) Un_iff list.set_sel(2) self_append_conv2 set_append tl_append2)
[PROOF STATE]
proof (state)
this:
stack e' \<noteq> [] \<and> n \<in> set (tl (stack e''))

goal (2 subgoals):
 1. \<lbrakk>w \<notin> explored e; w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
 2. \<lbrakk>w \<notin> explored e; \<not> w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
with postdfsw
[PROOF STATE]
proof (chain)
picking this:
post_dfs w e e'
stack e' \<noteq> [] \<and> n \<in> set (tl (stack e''))
[PROOF STEP]
have "\<S> e' n = \<S> e n"
[PROOF STATE]
proof (prove)
using this:
post_dfs w e e'
stack e' \<noteq> [] \<and> n \<in> set (tl (stack e''))

goal (1 subgoal):
 1. \<S> e' n = \<S> e n
[PROOF STEP]
apply (simp add: post_dfs_def e''_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>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> 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> [] \<and> n \<in> set (tl (stack e'))\<rbrakk> \<Longrightarrow> \<S> e' n = \<S> e n
[PROOF STEP]
by (metis list.set_sel(2))
[PROOF STATE]
proof (state)
this:
\<S> e' n = \<S> e n

goal (2 subgoals):
 1. \<lbrakk>w \<notin> explored e; w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
 2. \<lbrakk>w \<notin> explored e; \<not> w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<S> (dfss v e'') n = \<S> e' n
\<S> e' n = \<S> e n
[PROOF STEP]
have "\<S> (dfss v e'') n = \<S> e n"
[PROOF STATE]
proof (prove)
using this:
\<S> (dfss v e'') n = \<S> e' n
\<S> e' n = \<S> e n

goal (1 subgoal):
 1. \<S> (dfss v e'') n = \<S> e n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<S> (dfss v e'') n = \<S> e n

goal (2 subgoals):
 1. \<lbrakk>w \<notin> explored e; w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
 2. \<lbrakk>w \<notin> explored e; \<not> w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?n8 \<in> set (tl (stack (dfss v e''))) \<Longrightarrow> \<S> (dfss v e'') ?n8 = \<S> e ?n8

goal (2 subgoals):
 1. \<lbrakk>w \<notin> explored e; w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
 2. \<lbrakk>w \<notin> explored e; \<not> w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?n8 \<in> set (tl (stack (dfss v e''))) \<Longrightarrow> \<S> (dfss v e'') ?n8 = \<S> e ?n8

goal (2 subgoals):
 1. \<lbrakk>w \<notin> explored e; w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
 2. \<lbrakk>w \<notin> explored e; \<not> w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
from postdfsw
[PROOF STATE]
proof (chain)
picking this:
post_dfs w e e'
[PROOF STEP]
have "cstack e'' = cstack e"
[PROOF STATE]
proof (prove)
using this:
post_dfs w e e'

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

goal (2 subgoals):
 1. \<lbrakk>w \<notin> explored e; w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
 2. \<lbrakk>w \<notin> explored e; \<not> w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
post_dfss v e'' (dfss v e'')
\<forall>u\<in>visited e - {v}. vsuccs (dfss v e'') u = vsuccs e u
sub_env e (dfss v e'')
\<exists>ns. stack e = ns @ stack (dfss v e'')
?n8 \<in> set (tl (stack (dfss v e''))) \<Longrightarrow> \<S> (dfss v e'') ?n8 = \<S> e ?n8
cstack e'' = cstack e
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
post_dfss v e'' (dfss v e'')
\<forall>u\<in>visited e - {v}. vsuccs (dfss v e'') u = vsuccs e u
sub_env e (dfss v e'')
\<exists>ns. stack e = ns @ stack (dfss v e'')
?n8 \<in> set (tl (stack (dfss v e''))) \<Longrightarrow> \<S> (dfss v e'') ?n8 = \<S> e ?n8
cstack e'' = cstack e

goal (1 subgoal):
 1. post_dfss v e (dfss v e)
[PROOF STEP]
by (auto simp: dfss post_dfss_def)
[PROOF STATE]
proof (state)
this:
post_dfss v e (dfss v e)

goal (1 subgoal):
 1. \<lbrakk>w \<notin> explored e; \<not> w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>w \<notin> explored e; \<not> w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> w \<notin> visited e

goal (1 subgoal):
 1. \<lbrakk>w \<notin> explored e; \<not> w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
hence e': "e' = unite v w e"
[PROOF STATE]
proof (prove)
using this:
\<not> w \<notin> visited e

goal (1 subgoal):
 1. e' = unite v w e
[PROOF STEP]
using notexplored
[PROOF STATE]
proof (prove)
using this:
\<not> w \<notin> visited e
w \<notin> explored e

goal (1 subgoal):
 1. e' = unite v w e
[PROOF STEP]
using e'_def
[PROOF STATE]
proof (prove)
using this:
\<not> w \<notin> visited e
w \<notin> explored e
e' = (if w \<in> explored e then e else if w \<notin> visited e then dfs w e else unite v w e)

goal (1 subgoal):
 1. e' = unite v w e
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
e' = unite v w e

goal (1 subgoal):
 1. \<lbrakk>w \<notin> explored e; \<not> w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
from False
[PROOF STATE]
proof (chain)
picking this:
\<not> w \<notin> visited e
[PROOF STEP]
have "w \<in> visited e"
[PROOF STATE]
proof (prove)
using this:
\<not> w \<notin> visited e

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

goal (1 subgoal):
 1. \<lbrakk>w \<notin> explored e; \<not> w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
from wf wvs notexplored False
[PROOF STATE]
proof (chain)
picking this:
wf_env e
w \<in> successors v - vsuccs e v
w \<notin> explored e
\<not> w \<notin> visited e
[PROOF STEP]
obtain pfx where
            pfx: "stack e = pfx @ (stack e')" "stack e' \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
wf_env e
w \<in> successors v - vsuccs e v
w \<notin> explored e
\<not> w \<notin> visited e

goal (1 subgoal):
 1. (\<And>pfx. \<lbrakk>stack e = pfx @ stack e'; stack e' \<noteq> []\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding e'
[PROOF STATE]
proof (prove)
using this:
wf_env e
w \<in> successors v - vsuccs e v
w \<notin> explored e
\<not> w \<notin> visited e

goal (1 subgoal):
 1. (\<And>pfx. \<lbrakk>stack e = pfx @ stack (unite v w e); stack (unite v w e) \<noteq> []\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (blast dest: unite_stack)
[PROOF STATE]
proof (state)
this:
stack e = pfx @ stack e'
stack e' \<noteq> []

goal (1 subgoal):
 1. \<lbrakk>w \<notin> explored e; \<not> w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
from predfss wvs notexplored False \<open>e' = unite v w e\<close>
[PROOF STATE]
proof (chain)
picking this:
pre_dfss v e
w \<in> successors v - vsuccs e v
w \<notin> explored e
\<not> w \<notin> visited e
e' = unite v w e
[PROOF STEP]
have "pre_dfss v e''"
[PROOF STATE]
proof (prove)
using this:
pre_dfss v e
w \<in> successors v - vsuccs e v
w \<notin> explored e
\<not> w \<notin> visited e
e' = unite v w e

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

goal (1 subgoal):
 1. \<lbrakk>w \<notin> explored e; \<not> w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
with prepostdfss vs_case \<open>e' = unite v w e\<close>  \<open>w \<notin> explored e\<close> \<open>w \<in> visited e\<close>
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?vs6 = successors v - vsuccs e v; ?vs6 \<noteq> {}; ?w6 = (SOME x. x \<in> ?vs6); ?e'6 = (if ?w6 \<in> explored e then e else if ?w6 \<notin> visited e then dfs ?w6 e else unite v ?w6 e); ?e''6 = ?e'6\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs ?e'6 v \<union> {?w6} else vsuccs ?e'6 x\<rparr>; pre_dfss v ?e''6\<rbrakk> \<Longrightarrow> post_dfss v ?e''6 (dfss v ?e''6)
successors v - vsuccs e v \<noteq> {}
e' = unite v w e
w \<notin> explored e
w \<in> visited e
pre_dfss v e''
[PROOF STEP]
have post'': "post_dfss v e'' (dfss v e'')"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?vs6 = successors v - vsuccs e v; ?vs6 \<noteq> {}; ?w6 = (SOME x. x \<in> ?vs6); ?e'6 = (if ?w6 \<in> explored e then e else if ?w6 \<notin> visited e then dfs ?w6 e else unite v ?w6 e); ?e''6 = ?e'6\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs ?e'6 v \<union> {?w6} else vsuccs ?e'6 x\<rparr>; pre_dfss v ?e''6\<rbrakk> \<Longrightarrow> post_dfss v ?e''6 (dfss v ?e''6)
successors v - vsuccs e v \<noteq> {}
e' = unite v w e
w \<notin> explored e
w \<in> visited e
pre_dfss v e''

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

goal (1 subgoal):
 1. \<lbrakk>w \<notin> explored e; \<not> w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
post_dfss v e'' (dfss v e'')

goal (1 subgoal):
 1. \<lbrakk>w \<notin> explored e; \<not> w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
from post''
[PROOF STATE]
proof (chain)
picking this:
post_dfss v e'' (dfss v e'')
[PROOF STEP]
have "\<forall>u \<in> visited e - {v}. vsuccs (dfss v e'') u = vsuccs e u"
[PROOF STATE]
proof (prove)
using this:
post_dfss v e'' (dfss v e'')

goal (1 subgoal):
 1. \<forall>u\<in>visited e - {v}. vsuccs (dfss v e'') u = vsuccs e u
[PROOF STEP]
by (auto simp: post_dfss_def e''_def e' unite_def)
[PROOF STATE]
proof (state)
this:
\<forall>u\<in>visited e - {v}. vsuccs (dfss v e'') u = vsuccs e u

goal (1 subgoal):
 1. \<lbrakk>w \<notin> explored e; \<not> w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>u\<in>visited e - {v}. vsuccs (dfss v e'') u = vsuccs e u

goal (1 subgoal):
 1. \<lbrakk>w \<notin> explored e; \<not> w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
have "sub_env e (dfss v e'')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sub_env e (dfss v e'')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sub_env e (dfss v e'')
[PROOF STEP]
from predfss wvs \<open>w \<in> visited e\<close> notexplored
[PROOF STATE]
proof (chain)
picking this:
pre_dfss v e
w \<in> successors v - vsuccs e v
w \<in> visited e
w \<notin> explored e
[PROOF STEP]
have "sub_env e e'"
[PROOF STATE]
proof (prove)
using this:
pre_dfss v e
w \<in> successors v - vsuccs e v
w \<in> visited e
w \<notin> explored e

goal (1 subgoal):
 1. sub_env e e'
[PROOF STEP]
unfolding e'
[PROOF STATE]
proof (prove)
using this:
pre_dfss v e
w \<in> successors v - vsuccs e v
w \<in> visited e
w \<notin> explored e

goal (1 subgoal):
 1. sub_env e (unite v w e)
[PROOF STEP]
by (blast dest: unite_sub_env)
[PROOF STATE]
proof (state)
this:
sub_env e e'

goal (1 subgoal):
 1. sub_env e (dfss v e'')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sub_env e e'

goal (1 subgoal):
 1. sub_env e (dfss v e'')
[PROOF STEP]
have "sub_env e' e''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sub_env e' e''
[PROOF STEP]
by (auto simp: sub_env_def e''_def)
[PROOF STATE]
proof (state)
this:
sub_env e' e''

goal (1 subgoal):
 1. sub_env e (dfss v e'')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sub_env e' e''

goal (1 subgoal):
 1. sub_env e (dfss v e'')
[PROOF STEP]
from post''
[PROOF STATE]
proof (chain)
picking this:
post_dfss v e'' (dfss v e'')
[PROOF STEP]
have "sub_env e'' (dfss v e'')"
[PROOF STATE]
proof (prove)
using this:
post_dfss v e'' (dfss v e'')

goal (1 subgoal):
 1. sub_env e'' (dfss v e'')
[PROOF STEP]
by (simp add: post_dfss_def)
[PROOF STATE]
proof (state)
this:
sub_env e'' (dfss v e'')

goal (1 subgoal):
 1. sub_env e (dfss v e'')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
sub_env e e'
sub_env e' e''
sub_env e'' (dfss v e'')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sub_env e e'
sub_env e' e''
sub_env e'' (dfss v e'')

goal (1 subgoal):
 1. sub_env e (dfss v e'')
[PROOF STEP]
by (metis sub_env_trans)
[PROOF STATE]
proof (state)
this:
sub_env e (dfss v e'')

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

goal (1 subgoal):
 1. \<lbrakk>w \<notin> explored e; \<not> w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sub_env e (dfss v e'')

goal (1 subgoal):
 1. \<lbrakk>w \<notin> explored e; \<not> w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
from post'' \<open>stack e = pfx @ stack e'\<close>
[PROOF STATE]
proof (chain)
picking this:
post_dfss v e'' (dfss v e'')
stack e = pfx @ stack e'
[PROOF STEP]
have "\<exists>ns. stack e = ns @ (stack (dfss v e''))"
[PROOF STATE]
proof (prove)
using this:
post_dfss v e'' (dfss v e'')
stack e = pfx @ stack e'

goal (1 subgoal):
 1. \<exists>ns. stack e = ns @ stack (dfss v e'')
[PROOF STEP]
by (auto simp: post_dfss_def e''_def)
[PROOF STATE]
proof (state)
this:
\<exists>ns. stack e = ns @ stack (dfss v e'')

goal (1 subgoal):
 1. \<lbrakk>w \<notin> explored e; \<not> w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<exists>ns. stack e = ns @ stack (dfss v e'')

goal (1 subgoal):
 1. \<lbrakk>w \<notin> explored e; \<not> w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<exists>ns. stack e = ns @ stack (dfss v e'')

goal (1 subgoal):
 1. \<lbrakk>w \<notin> explored e; \<not> w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>w \<notin> explored e; \<not> w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
assume n: "n \<in> set (tl (stack (dfss v e'')))"
[PROOF STATE]
proof (state)
this:
n \<in> set (tl (stack (dfss v e'')))

goal (1 subgoal):
 1. \<lbrakk>w \<notin> explored e; \<not> w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
with post''
[PROOF STATE]
proof (chain)
picking this:
post_dfss v e'' (dfss v e'')
n \<in> set (tl (stack (dfss v e'')))
[PROOF STEP]
have "\<S> (dfss v e'') n = \<S> e'' n"
[PROOF STATE]
proof (prove)
using this:
post_dfss v e'' (dfss v e'')
n \<in> set (tl (stack (dfss v e'')))

goal (1 subgoal):
 1. \<S> (dfss v e'') n = \<S> e'' n
[PROOF STEP]
by (simp add: post_dfss_def)
[PROOF STATE]
proof (state)
this:
\<S> (dfss v e'') n = \<S> e'' n

goal (1 subgoal):
 1. \<lbrakk>w \<notin> explored e; \<not> w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<S> (dfss v e'') n = \<S> e'' n

goal (1 subgoal):
 1. \<lbrakk>w \<notin> explored e; \<not> w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
from n post'' \<open>stack e' \<noteq> []\<close>
[PROOF STATE]
proof (chain)
picking this:
n \<in> set (tl (stack (dfss v e'')))
post_dfss v e'' (dfss v e'')
stack e' \<noteq> []
[PROOF STEP]
have "n \<in> set (tl (stack e''))"
[PROOF STATE]
proof (prove)
using this:
n \<in> set (tl (stack (dfss v e'')))
post_dfss v e'' (dfss v e'')
stack e' \<noteq> []

goal (1 subgoal):
 1. n \<in> set (tl (stack e''))
[PROOF STEP]
apply (simp add: post_dfss_def e''_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<in> set (tl (stack (dfss v (e'\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e' v \<union> {w} else vsuccs e' x\<rparr>)))); wf_env (dfss v (e'\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e' v \<union> {w} else vsuccs e' x\<rparr>)) \<and> vsuccs (dfss v (e'\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e' v \<union> {w} else vsuccs e' x\<rparr>)) v = successors v \<and> (\<forall>wa\<in>visited e' - {v}. vsuccs (dfss v (e'\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e' v \<union> {w} else vsuccs e' x\<rparr>)) wa = vsuccs e' wa) \<and> sub_env (e'\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e' v \<union> {w} else vsuccs e' x\<rparr>) (dfss v (e'\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e' v \<union> {w} else vsuccs e' x\<rparr>)) \<and> (\<forall>wa\<in>successors v. wa \<in> explored (dfss v (e'\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e' v \<union> {w} else vsuccs e' x\<rparr>)) \<or> wa \<in> \<S> (dfss v (e'\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e' v \<union> {w} else vsuccs e' x\<rparr>)) (hd (stack (dfss v (e'\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e' v \<union> {w} else vsuccs e' x\<rparr>))))) \<and> (\<forall>n\<in>set (stack (dfss v (e'\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e' v \<union> {w} else vsuccs e' x\<rparr>))). reachable n v) \<and> stack (dfss v (e'\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e' v \<union> {w} else vsuccs e' x\<rparr>)) \<noteq> [] \<and> (\<exists>ns. stack e' = ns @ stack (dfss v (e'\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e' v \<union> {w} else vsuccs e' x\<rparr>))) \<and> v \<in> \<S> (dfss v (e'\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e' v \<union> {w} else vsuccs e' x\<rparr>)) (hd (stack (dfss v (e'\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e' v \<union> {w} else vsuccs e' x\<rparr>)))) \<and> (\<forall>n\<in>set (tl (stack (dfss v (e'\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e' v \<union> {w} else vsuccs e' x\<rparr>)))). \<S> (dfss v (e'\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e' v \<union> {w} else vsuccs e' x\<rparr>)) n = \<S> e' n) \<and> (hd (stack (dfss v (e'\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e' v \<union> {w} else vsuccs e' x\<rparr>))) = v \<longrightarrow> (\<forall>n\<in>set (tl (stack (dfss v (e'\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e' v \<union> {w} else vsuccs e' x\<rparr>)))). \<not> reachable v n)) \<and> cstack (dfss v (e'\<lparr>vsuccs := \<lambda>x. if x = v then vsuccs e' v \<union> {w} else vsuccs e' x\<rparr>)) = cstack e'; stack e' \<noteq> []\<rbrakk> \<Longrightarrow> n \<in> set (tl (stack e'))
[PROOF STEP]
by (metis (no_types, lifting) Un_iff list.set_sel(2) self_append_conv2 set_append tl_append2)
[PROOF STATE]
proof (state)
this:
n \<in> set (tl (stack e''))

goal (1 subgoal):
 1. \<lbrakk>w \<notin> explored e; \<not> w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
with wf wvs \<open>w \<in> visited e\<close> notexplored
[PROOF STATE]
proof (chain)
picking this:
wf_env e
w \<in> successors v - vsuccs e v
w \<in> visited e
w \<notin> explored e
n \<in> set (tl (stack e''))
[PROOF STEP]
have "\<S> e'' n = \<S> e n"
[PROOF STATE]
proof (prove)
using this:
wf_env e
w \<in> successors v - vsuccs e v
w \<in> visited e
w \<notin> explored e
n \<in> set (tl (stack e''))

goal (1 subgoal):
 1. \<S> e'' n = \<S> e n
[PROOF STEP]
by (auto simp: e''_def e' dest: unite_S_tl)
[PROOF STATE]
proof (state)
this:
\<S> e'' n = \<S> e n

goal (1 subgoal):
 1. \<lbrakk>w \<notin> explored e; \<not> w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<S> (dfss v e'') n = \<S> e'' n
\<S> e'' n = \<S> e n
[PROOF STEP]
have "\<S> (dfss v e'') n = \<S> e n"
[PROOF STATE]
proof (prove)
using this:
\<S> (dfss v e'') n = \<S> e'' n
\<S> e'' n = \<S> e n

goal (1 subgoal):
 1. \<S> (dfss v e'') n = \<S> e n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<S> (dfss v e'') n = \<S> e n

goal (1 subgoal):
 1. \<lbrakk>w \<notin> explored e; \<not> w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?n8 \<in> set (tl (stack (dfss v e''))) \<Longrightarrow> \<S> (dfss v e'') ?n8 = \<S> e ?n8

goal (1 subgoal):
 1. \<lbrakk>w \<notin> explored e; \<not> w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?n8 \<in> set (tl (stack (dfss v e''))) \<Longrightarrow> \<S> (dfss v e'') ?n8 = \<S> e ?n8

goal (1 subgoal):
 1. \<lbrakk>w \<notin> explored e; \<not> w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
from post''
[PROOF STATE]
proof (chain)
picking this:
post_dfss v e'' (dfss v e'')
[PROOF STEP]
have "cstack (dfss v e'') = cstack e"
[PROOF STATE]
proof (prove)
using this:
post_dfss v e'' (dfss v e'')

goal (1 subgoal):
 1. cstack (dfss v e'') = cstack e
[PROOF STEP]
by (simp add: post_dfss_def e''_def e' unite_def)
[PROOF STATE]
proof (state)
this:
cstack (dfss v e'') = cstack e

goal (1 subgoal):
 1. \<lbrakk>w \<notin> explored e; \<not> w \<notin> visited e\<rbrakk> \<Longrightarrow> post_dfss v e (dfss v e)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
post_dfss v e'' (dfss v e'')
\<forall>u\<in>visited e - {v}. vsuccs (dfss v e'') u = vsuccs e u
sub_env e (dfss v e'')
\<exists>ns. stack e = ns @ stack (dfss v e'')
?n8 \<in> set (tl (stack (dfss v e''))) \<Longrightarrow> \<S> (dfss v e'') ?n8 = \<S> e ?n8
cstack (dfss v e'') = cstack e
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
post_dfss v e'' (dfss v e'')
\<forall>u\<in>visited e - {v}. vsuccs (dfss v e'') u = vsuccs e u
sub_env e (dfss v e'')
\<exists>ns. stack e = ns @ stack (dfss v e'')
?n8 \<in> set (tl (stack (dfss v e''))) \<Longrightarrow> \<S> (dfss v e'') ?n8 = \<S> e ?n8
cstack (dfss v e'') = cstack e

goal (1 subgoal):
 1. post_dfss v e (dfss v e)
[PROOF STEP]
by (simp add: dfss post_dfss_def)
[PROOF STATE]
proof (state)
this:
post_dfss v e (dfss v e)

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed