[STATEMENT]
lemma unite_wf_env:
  fixes e v w
  defines "e' \<equiv> unite v w e"
  assumes pre: "pre_dfss v e"
      and w: "w \<in> successors v" "w \<notin> vsuccs e v" "w \<in> visited e" "w \<notin> explored e"
  shows "wf_env e'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_env e'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wf_env e'
[PROOF STEP]
from pre
[PROOF STATE]
proof (chain)
picking this:
pre_dfss v e
[PROOF STEP]
have wf: "wf_env e"
[PROOF STATE]
proof (prove)
using this:
pre_dfss v e

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

goal (1 subgoal):
 1. wf_env e'
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
e' \<equiv> unite v w e
pre_dfss v e
edge v w
w \<notin> vsuccs e v
w \<in> visited e
w \<notin> explored e
[PROOF STEP]
obtain pfx where
    pfx: "stack e = pfx @ (stack e')" "stack e' \<noteq> []"
         "let cc = \<Union> {\<S> e n |n. n \<in> set pfx \<union> {hd (stack e')}}
          in \<S> e' = (\<lambda>x. if x \<in> cc then cc else \<S> e x)"
[PROOF STATE]
proof (prove)
using this:
e' \<equiv> unite v w e
pre_dfss v e
edge v w
w \<notin> vsuccs e v
w \<in> visited e
w \<notin> explored e

goal (1 subgoal):
 1. (\<And>pfx. \<lbrakk>stack e = pfx @ stack e'; stack e' \<noteq> []; let cc = \<Union> {\<S> e n |n. n \<in> set pfx \<union> {hd (stack e')}} in \<S> e' = (\<lambda>x. if x \<in> cc then cc else \<S> e x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (blast dest: unite_stack[OF wf])
[PROOF STATE]
proof (state)
this:
stack e = pfx @ stack e'
stack e' \<noteq> []
let cc = \<Union> {\<S> e n |n. n \<in> set pfx \<union> {hd (stack e')}} in \<S> e' = (\<lambda>x. if x \<in> cc then cc else \<S> e x)

goal (1 subgoal):
 1. wf_env e'
[PROOF STEP]
define cc where "cc \<equiv> \<Union> {\<S> e n |n. n \<in> set pfx \<union> {hd (stack e')}}"
[PROOF STATE]
proof (state)
this:
cc \<equiv> \<Union> {\<S> e n |n. n \<in> set pfx \<union> {hd (stack e')}}

goal (1 subgoal):
 1. wf_env e'
[PROOF STEP]
from pfx
[PROOF STATE]
proof (chain)
picking this:
stack e = pfx @ stack e'
stack e' \<noteq> []
let cc = \<Union> {\<S> e n |n. n \<in> set pfx \<union> {hd (stack e')}} in \<S> e' = (\<lambda>x. if x \<in> cc then cc else \<S> e x)
[PROOF STEP]
have Se': "\<forall>x. \<S> e' x = (if x \<in> cc then cc else \<S> e x)"
[PROOF STATE]
proof (prove)
using this:
stack e = pfx @ stack e'
stack e' \<noteq> []
let cc = \<Union> {\<S> e n |n. n \<in> set pfx \<union> {hd (stack e')}} in \<S> e' = (\<lambda>x. if x \<in> cc then cc else \<S> e x)

goal (1 subgoal):
 1. \<forall>x. \<S> e' x = (if x \<in> cc then cc else \<S> e x)
[PROOF STEP]
by (auto simp add: cc_def)
[PROOF STATE]
proof (state)
this:
\<forall>x. \<S> e' x = (if x \<in> cc then cc else \<S> e x)

goal (1 subgoal):
 1. wf_env e'
[PROOF STEP]
have cc_Un: "cc = \<Union> {\<S> e x | x. x \<in> cc}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cc = \<Union> {\<S> e x |x. x \<in> cc}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. cc \<subseteq> \<Union> {\<S> e x |x. x \<in> cc}
 2. \<Union> {\<S> e x |x. x \<in> cc} \<subseteq> cc
[PROOF STEP]
from S_reflexive[OF wf]
[PROOF STATE]
proof (chain)
picking this:
?n \<in> \<S> e ?n
[PROOF STEP]
show "cc \<subseteq> \<Union> {\<S> e x | x. x \<in> cc}"
[PROOF STATE]
proof (prove)
using this:
?n \<in> \<S> e ?n

goal (1 subgoal):
 1. cc \<subseteq> \<Union> {\<S> e x |x. x \<in> cc}
[PROOF STEP]
by (auto simp: cc_def)
[PROOF STATE]
proof (state)
this:
cc \<subseteq> \<Union> {\<S> e x |x. x \<in> cc}

goal (1 subgoal):
 1. \<Union> {\<S> e x |x. x \<in> cc} \<subseteq> cc
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Union> {\<S> e x |x. x \<in> cc} \<subseteq> cc
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Union> {\<S> e x |x. x \<in> cc} \<subseteq> cc
[PROOF STEP]
fix n x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Union> {\<S> e x |x. x \<in> cc} \<subseteq> cc
[PROOF STEP]
assume "x \<in> cc" "n \<in> \<S> e x"
[PROOF STATE]
proof (state)
this:
x \<in> cc
n \<in> \<S> e x

goal (1 subgoal):
 1. \<Union> {\<S> e x |x. x \<in> cc} \<subseteq> cc
[PROOF STEP]
with wf
[PROOF STATE]
proof (chain)
picking this:
wf_env e
x \<in> cc
n \<in> \<S> e x
[PROOF STEP]
have "n \<in> cc"
[PROOF STATE]
proof (prove)
using this:
wf_env e
x \<in> cc
n \<in> \<S> e x

goal (1 subgoal):
 1. n \<in> cc
[PROOF STEP]
unfolding wf_env_def cc_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
x \<in> \<Union> {\<S> e n |n. n \<in> set pfx \<union> {hd (stack e')}}
n \<in> \<S> e x

goal (1 subgoal):
 1. n \<in> \<Union> {\<S> e n |n. n \<in> set pfx \<union> {hd (stack e')}}
[PROOF STEP]
by (smt (verit) Union_iff mem_Collect_eq)
[PROOF STATE]
proof (state)
this:
n \<in> cc

goal (1 subgoal):
 1. \<Union> {\<S> e x |x. x \<in> cc} \<subseteq> cc
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x8 \<in> cc; ?n8 \<in> \<S> e ?x8\<rbrakk> \<Longrightarrow> ?n8 \<in> cc

goal (1 subgoal):
 1. \<Union> {\<S> e x |x. x \<in> cc} \<subseteq> cc
[PROOF STEP]
thus "(\<Union> {\<S> e x | x. x \<in> cc}) \<subseteq> cc"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x8 \<in> cc; ?n8 \<in> \<S> e ?x8\<rbrakk> \<Longrightarrow> ?n8 \<in> cc

goal (1 subgoal):
 1. \<Union> {\<S> e x |x. x \<in> cc} \<subseteq> cc
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<Union> {\<S> e x |x. x \<in> cc} \<subseteq> cc

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
cc = \<Union> {\<S> e x |x. x \<in> cc}

goal (1 subgoal):
 1. wf_env e'
[PROOF STEP]
from S_reflexive[OF wf, of "hd (stack e')"]
[PROOF STATE]
proof (chain)
picking this:
hd (stack e') \<in> \<S> e (hd (stack e'))
[PROOF STEP]
have hd_cc: "\<S> e' (hd (stack e')) = cc"
[PROOF STATE]
proof (prove)
using this:
hd (stack e') \<in> \<S> e (hd (stack e'))

goal (1 subgoal):
 1. \<S> e' (hd (stack e')) = cc
[PROOF STEP]
by (auto simp: cc_def Se')
[PROOF STATE]
proof (state)
this:
\<S> e' (hd (stack e')) = cc

goal (1 subgoal):
 1. wf_env e'
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<S> e' (hd (stack e')) = cc

goal (1 subgoal):
 1. wf_env e'
[PROOF STEP]
fix n m
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wf_env e'
[PROOF STEP]
assume n: "n \<in> set (tl (stack e'))"
       and m: "m \<in> \<S> e n \<inter> cc"
[PROOF STATE]
proof (state)
this:
n \<in> set (tl (stack e'))
m \<in> \<S> e n \<inter> cc

goal (1 subgoal):
 1. wf_env e'
[PROOF STEP]
from m
[PROOF STATE]
proof (chain)
picking this:
m \<in> \<S> e n \<inter> cc
[PROOF STEP]
obtain l where
      "l \<in> set pfx \<union> {hd (stack e')}" "m \<in> \<S> e l"
[PROOF STATE]
proof (prove)
using this:
m \<in> \<S> e n \<inter> cc

goal (1 subgoal):
 1. (\<And>l. \<lbrakk>l \<in> set pfx \<union> {hd (stack e')}; m \<in> \<S> e l\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: cc_def)
[PROOF STATE]
proof (state)
this:
l \<in> set pfx \<union> {hd (stack e')}
m \<in> \<S> e l

goal (1 subgoal):
 1. wf_env e'
[PROOF STEP]
with n m wf \<open>stack e = pfx @ stack e'\<close> \<open>stack e' \<noteq> []\<close>
[PROOF STATE]
proof (chain)
picking this:
n \<in> set (tl (stack e'))
m \<in> \<S> e n \<inter> cc
wf_env e
stack e = pfx @ stack e'
stack e' \<noteq> []
l \<in> set pfx \<union> {hd (stack e')}
m \<in> \<S> e l
[PROOF STEP]
have "False"
[PROOF STATE]
proof (prove)
using this:
n \<in> set (tl (stack e'))
m \<in> \<S> e n \<inter> cc
wf_env e
stack e = pfx @ stack e'
stack e' \<noteq> []
l \<in> set pfx \<union> {hd (stack e')}
m \<in> \<S> e l

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding wf_env_def
[PROOF STATE]
proof (prove)
using this:
n \<in> set (tl (stack e'))
m \<in> \<S> e n \<inter> cc
(\<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 = pfx @ stack e'
stack e' \<noteq> []
l \<in> set pfx \<union> {hd (stack e')}
m \<in> \<S> e l

goal (1 subgoal):
 1. False
[PROOF STEP]
by (metis (no_types, lifting) Int_iff UnCI UnE disjoint_insert(1) distinct.simps(2)
                distinct_append emptyE hd_Cons_tl insert_iff list.set_sel(1) list.set_sel(2)
                mk_disjoint_insert set_append)
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. wf_env e'
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?n8 \<in> set (tl (stack e')); ?m8 \<in> \<S> e ?n8 \<inter> cc\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. wf_env e'
[PROOF STEP]
hence tl_cc: "\<forall>n \<in> set (tl (stack e')). \<S> e n \<inter> cc = {}"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?n8 \<in> set (tl (stack e')); ?m8 \<in> \<S> e ?n8 \<inter> cc\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. \<forall>n\<in>set (tl (stack e')). \<S> e n \<inter> cc = {}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>n\<in>set (tl (stack e')). \<S> e n \<inter> cc = {}

goal (1 subgoal):
 1. wf_env e'
[PROOF STEP]
from wf
[PROOF STATE]
proof (chain)
picking this:
wf_env e
[PROOF STEP]
have "\<forall>n \<in> visited e'. reachable (root e') n"
       "distinct (cstack e')"
       "explored e' \<subseteq> visited e'"
       "set (cstack e') \<subseteq> visited e'"
       "\<forall>n \<in> explored e'. \<forall>m. reachable n m \<longrightarrow> m \<in> explored e'"
       "\<forall>n. vsuccs e' n \<subseteq> successors n \<inter> visited e'"
       "\<forall>n. n \<notin> visited e' \<longrightarrow> vsuccs e' n = {}"
       "\<forall>n \<in> explored e'. vsuccs e' n = successors n"
       "\<forall>n \<in> visited e' - set (cstack e'). vsuccs e' n = successors n"
       "\<forall>S \<in> sccs e'. is_scc S"
       "\<Union> (sccs e') = explored e'"
[PROOF STATE]
proof (prove)
using this:
wf_env e

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

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

goal (1 subgoal):
 1. wf_env e'
[PROOF STEP]
from wf \<open>stack e = pfx @ stack e'\<close>
[PROOF STATE]
proof (chain)
picking this:
wf_env e
stack e = pfx @ stack e'
[PROOF STEP]
have "distinct (stack e')"
[PROOF STATE]
proof (prove)
using this:
wf_env e
stack e = pfx @ stack e'

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

goal (1 subgoal):
 1. wf_env e'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
distinct (stack e')

goal (1 subgoal):
 1. wf_env e'
[PROOF STEP]
have "\<forall>n m. n \<preceq> m in stack e' \<longrightarrow> n \<preceq> m in cstack e'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n m. n \<preceq> m in stack e' \<longrightarrow> n \<preceq> m in cstack e'
[PROOF STEP]
proof (clarify)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n m. n \<preceq> m in stack e' \<Longrightarrow> n \<preceq> m in cstack e'
[PROOF STEP]
fix n m
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n m. n \<preceq> m in stack e' \<Longrightarrow> n \<preceq> m in cstack e'
[PROOF STEP]
assume "n \<preceq> m in stack e'"
[PROOF STATE]
proof (state)
this:
n \<preceq> m in stack e'

goal (1 subgoal):
 1. \<And>n m. n \<preceq> m in stack e' \<Longrightarrow> n \<preceq> m in cstack e'
[PROOF STEP]
with \<open>stack e = pfx @ stack e'\<close> wf
[PROOF STATE]
proof (chain)
picking this:
stack e = pfx @ stack e'
wf_env e
n \<preceq> m in stack e'
[PROOF STEP]
have "n \<preceq> m in cstack e"
[PROOF STATE]
proof (prove)
using this:
stack e = pfx @ stack e'
wf_env e
n \<preceq> m in stack e'

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

goal (1 subgoal):
 1. n \<preceq> m in cstack e
[PROOF STEP]
by (metis precedes_append_left)
[PROOF STATE]
proof (state)
this:
n \<preceq> m in cstack e

goal (1 subgoal):
 1. \<And>n m. n \<preceq> m in stack e' \<Longrightarrow> n \<preceq> m in cstack e'
[PROOF STEP]
thus "n \<preceq> m in cstack e'"
[PROOF STATE]
proof (prove)
using this:
n \<preceq> m in cstack e

goal (1 subgoal):
 1. n \<preceq> m in cstack e'
[PROOF STEP]
by (simp add: e'_def unite_def)
[PROOF STATE]
proof (state)
this:
n \<preceq> m in cstack e'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>n m. n \<preceq> m in stack e' \<longrightarrow> n \<preceq> m in cstack e'

goal (1 subgoal):
 1. wf_env e'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>n m. n \<preceq> m in stack e' \<longrightarrow> n \<preceq> m in cstack e'

goal (1 subgoal):
 1. wf_env e'
[PROOF STEP]
from wf \<open>stack e = pfx @ stack e'\<close>
[PROOF STATE]
proof (chain)
picking this:
wf_env e
stack e = pfx @ stack e'
[PROOF STEP]
have "\<forall>n m. n \<preceq> m in stack e' \<longrightarrow> reachable m n"
[PROOF STATE]
proof (prove)
using this:
wf_env e
stack e = pfx @ stack e'

goal (1 subgoal):
 1. \<forall>n m. n \<preceq> m in stack e' \<longrightarrow> reachable m 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 = pfx @ stack e'

goal (1 subgoal):
 1. \<forall>n m. n \<preceq> m in stack e' \<longrightarrow> reachable m n
[PROOF STEP]
by (metis precedes_append_left)
[PROOF STATE]
proof (state)
this:
\<forall>n m. n \<preceq> m in stack e' \<longrightarrow> reachable m n

goal (1 subgoal):
 1. wf_env e'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>n m. n \<preceq> m in stack e' \<longrightarrow> reachable m n

goal (1 subgoal):
 1. wf_env e'
[PROOF STEP]
have "\<forall>n m. m \<in> \<S> e' n \<longleftrightarrow> (\<S> e' n = \<S> e' m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n m. (m \<in> \<S> e' n) = (\<S> e' n = \<S> e' m)
[PROOF STEP]
proof (clarify)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n m. (m \<in> \<S> e' n) = (\<S> e' n = \<S> e' m)
[PROOF STEP]
fix n m
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n m. (m \<in> \<S> e' n) = (\<S> e' n = \<S> e' m)
[PROOF STEP]
show "m \<in> \<S> e' n \<longleftrightarrow> (\<S> e' n = \<S> e' m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (m \<in> \<S> e' n) = (\<S> e' n = \<S> e' m)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. m \<in> \<S> e' n \<Longrightarrow> \<S> e' n = \<S> e' m
 2. \<S> e' n = \<S> e' m \<Longrightarrow> m \<in> \<S> e' n
[PROOF STEP]
assume l: "m \<in> \<S> e' n"
[PROOF STATE]
proof (state)
this:
m \<in> \<S> e' n

goal (2 subgoals):
 1. m \<in> \<S> e' n \<Longrightarrow> \<S> e' n = \<S> e' m
 2. \<S> e' n = \<S> e' m \<Longrightarrow> m \<in> \<S> e' n
[PROOF STEP]
show "\<S> e' n = \<S> e' m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<S> e' n = \<S> e' m
[PROOF STEP]
proof (cases "n \<in> cc")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n \<in> cc \<Longrightarrow> \<S> e' n = \<S> e' m
 2. n \<notin> cc \<Longrightarrow> \<S> e' n = \<S> e' m
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
n \<in> cc

goal (2 subgoals):
 1. n \<in> cc \<Longrightarrow> \<S> e' n = \<S> e' m
 2. n \<notin> cc \<Longrightarrow> \<S> e' n = \<S> e' m
[PROOF STEP]
with l
[PROOF STATE]
proof (chain)
picking this:
m \<in> \<S> e' n
n \<in> cc
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
m \<in> \<S> e' n
n \<in> cc

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

goal (1 subgoal):
 1. n \<notin> cc \<Longrightarrow> \<S> e' n = \<S> e' m
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n \<notin> cc \<Longrightarrow> \<S> e' n = \<S> e' m
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
n \<notin> cc

goal (1 subgoal):
 1. n \<notin> cc \<Longrightarrow> \<S> e' n = \<S> e' m
[PROOF STEP]
with l wf
[PROOF STATE]
proof (chain)
picking this:
m \<in> \<S> e' n
wf_env e
n \<notin> cc
[PROOF STEP]
have "\<S> e n = \<S> e m"
[PROOF STATE]
proof (prove)
using this:
m \<in> \<S> e' n
wf_env e
n \<notin> cc

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

goal (1 subgoal):
 1. n \<notin> cc \<Longrightarrow> \<S> e' n = \<S> e' m
[PROOF STEP]
with False cc_Un wf
[PROOF STATE]
proof (chain)
picking this:
n \<notin> cc
cc = \<Union> {\<S> e x |x. x \<in> cc}
wf_env e
\<S> e n = \<S> e m
[PROOF STEP]
have "m \<notin> cc"
[PROOF STATE]
proof (prove)
using this:
n \<notin> cc
cc = \<Union> {\<S> e x |x. x \<in> cc}
wf_env e
\<S> e n = \<S> e m

goal (1 subgoal):
 1. m \<notin> cc
[PROOF STEP]
unfolding wf_env_def e'_def
[PROOF STATE]
proof (prove)
using this:
n \<notin> cc
cc = \<Union> {\<S> e x |x. x \<in> cc}
(\<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
\<S> e n = \<S> e m

goal (1 subgoal):
 1. m \<notin> cc
[PROOF STEP]
by (smt (verit, best) Union_iff mem_Collect_eq)
[PROOF STATE]
proof (state)
this:
m \<notin> cc

goal (1 subgoal):
 1. n \<notin> cc \<Longrightarrow> \<S> e' n = \<S> e' m
[PROOF STEP]
with \<open>\<S> e n = \<S> e m\<close> False
[PROOF STATE]
proof (chain)
picking this:
\<S> e n = \<S> e m
n \<notin> cc
m \<notin> cc
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<S> e n = \<S> e m
n \<notin> cc
m \<notin> cc

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<S> e' n = \<S> e' m

goal (1 subgoal):
 1. \<S> e' n = \<S> e' m \<Longrightarrow> m \<in> \<S> e' n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<S> e' n = \<S> e' m \<Longrightarrow> m \<in> \<S> e' n
[PROOF STEP]
assume r: "\<S> e' n = \<S> e' m"
[PROOF STATE]
proof (state)
this:
\<S> e' n = \<S> e' m

goal (1 subgoal):
 1. \<S> e' n = \<S> e' m \<Longrightarrow> m \<in> \<S> e' n
[PROOF STEP]
show "m \<in> \<S> e' n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m \<in> \<S> e' n
[PROOF STEP]
proof (cases "n \<in> cc")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n \<in> cc \<Longrightarrow> m \<in> \<S> e' n
 2. n \<notin> cc \<Longrightarrow> m \<in> \<S> e' n
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
n \<in> cc

goal (2 subgoals):
 1. n \<in> cc \<Longrightarrow> m \<in> \<S> e' n
 2. n \<notin> cc \<Longrightarrow> m \<in> \<S> e' n
[PROOF STEP]
with r pfx
[PROOF STATE]
proof (chain)
picking this:
\<S> e' n = \<S> e' m
stack e = pfx @ stack e'
stack e' \<noteq> []
let cc = \<Union> {\<S> e n |n. n \<in> set pfx \<union> {hd (stack e')}} in \<S> e' = (\<lambda>x. if x \<in> cc then cc else \<S> e x)
n \<in> cc
[PROOF STEP]
have "\<S> e' m = cc"
[PROOF STATE]
proof (prove)
using this:
\<S> e' n = \<S> e' m
stack e = pfx @ stack e'
stack e' \<noteq> []
let cc = \<Union> {\<S> e n |n. n \<in> set pfx \<union> {hd (stack e')}} in \<S> e' = (\<lambda>x. if x \<in> cc then cc else \<S> e x)
n \<in> cc

goal (1 subgoal):
 1. \<S> e' m = cc
[PROOF STEP]
by (auto simp: cc_def)
[PROOF STATE]
proof (state)
this:
\<S> e' m = cc

goal (2 subgoals):
 1. n \<in> cc \<Longrightarrow> m \<in> \<S> e' n
 2. n \<notin> cc \<Longrightarrow> m \<in> \<S> e' n
[PROOF STEP]
have "m \<in> cc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m \<in> cc
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. m \<notin> cc \<Longrightarrow> False
[PROOF STEP]
assume "m \<notin> cc"
[PROOF STATE]
proof (state)
this:
m \<notin> cc

goal (1 subgoal):
 1. m \<notin> cc \<Longrightarrow> False
[PROOF STEP]
with pfx
[PROOF STATE]
proof (chain)
picking this:
stack e = pfx @ stack e'
stack e' \<noteq> []
let cc = \<Union> {\<S> e n |n. n \<in> set pfx \<union> {hd (stack e')}} in \<S> e' = (\<lambda>x. if x \<in> cc then cc else \<S> e x)
m \<notin> cc
[PROOF STEP]
have "\<S> e' m = \<S> e m"
[PROOF STATE]
proof (prove)
using this:
stack e = pfx @ stack e'
stack e' \<noteq> []
let cc = \<Union> {\<S> e n |n. n \<in> set pfx \<union> {hd (stack e')}} in \<S> e' = (\<lambda>x. if x \<in> cc then cc else \<S> e x)
m \<notin> cc

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

goal (1 subgoal):
 1. m \<notin> cc \<Longrightarrow> False
[PROOF STEP]
with S_reflexive[OF wf, of m] \<open>\<S> e' m = cc\<close> \<open>m \<notin> cc\<close>
[PROOF STATE]
proof (chain)
picking this:
m \<in> \<S> e m
\<S> e' m = cc
m \<notin> cc
\<S> e' m = \<S> e m
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
m \<in> \<S> e m
\<S> e' m = cc
m \<notin> cc
\<S> e' m = \<S> e m

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:
m \<in> cc

goal (2 subgoals):
 1. n \<in> cc \<Longrightarrow> m \<in> \<S> e' n
 2. n \<notin> cc \<Longrightarrow> m \<in> \<S> e' n
[PROOF STEP]
with pfx True
[PROOF STATE]
proof (chain)
picking this:
stack e = pfx @ stack e'
stack e' \<noteq> []
let cc = \<Union> {\<S> e n |n. n \<in> set pfx \<union> {hd (stack e')}} in \<S> e' = (\<lambda>x. if x \<in> cc then cc else \<S> e x)
n \<in> cc
m \<in> cc
[PROOF STEP]
show "m \<in> \<S> e' n"
[PROOF STATE]
proof (prove)
using this:
stack e = pfx @ stack e'
stack e' \<noteq> []
let cc = \<Union> {\<S> e n |n. n \<in> set pfx \<union> {hd (stack e')}} in \<S> e' = (\<lambda>x. if x \<in> cc then cc else \<S> e x)
n \<in> cc
m \<in> cc

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

goal (1 subgoal):
 1. n \<notin> cc \<Longrightarrow> m \<in> \<S> e' n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n \<notin> cc \<Longrightarrow> m \<in> \<S> e' n
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
n \<notin> cc

goal (1 subgoal):
 1. n \<notin> cc \<Longrightarrow> m \<in> \<S> e' n
[PROOF STEP]
hence "\<S> e' n = \<S> e n"
[PROOF STATE]
proof (prove)
using this:
n \<notin> cc

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

goal (1 subgoal):
 1. n \<notin> cc \<Longrightarrow> m \<in> \<S> e' n
[PROOF STEP]
have "m \<notin> cc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m \<notin> cc
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. m \<in> cc \<Longrightarrow> False
[PROOF STEP]
assume m: "m \<in> cc"
[PROOF STATE]
proof (state)
this:
m \<in> cc

goal (1 subgoal):
 1. m \<in> cc \<Longrightarrow> False
[PROOF STEP]
with \<open>\<S> e' n = \<S> e n\<close> r
[PROOF STATE]
proof (chain)
picking this:
\<S> e' n = \<S> e n
\<S> e' n = \<S> e' m
m \<in> cc
[PROOF STEP]
have "\<S> e n = cc"
[PROOF STATE]
proof (prove)
using this:
\<S> e' n = \<S> e n
\<S> e' n = \<S> e' m
m \<in> cc

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

goal (1 subgoal):
 1. m \<in> cc \<Longrightarrow> False
[PROOF STEP]
with S_reflexive[OF wf, of n]
[PROOF STATE]
proof (chain)
picking this:
n \<in> \<S> e n
\<S> e n = cc
[PROOF STEP]
have "n \<in> cc"
[PROOF STATE]
proof (prove)
using this:
n \<in> \<S> e n
\<S> e n = cc

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

goal (1 subgoal):
 1. m \<in> cc \<Longrightarrow> False
[PROOF STEP]
with \<open>n \<notin> cc\<close>
[PROOF STATE]
proof (chain)
picking this:
n \<notin> cc
n \<in> cc
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
n \<notin> cc
n \<in> cc

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
m \<notin> cc

goal (1 subgoal):
 1. n \<notin> cc \<Longrightarrow> m \<in> \<S> e' n
[PROOF STEP]
with r \<open>\<S> e' n = \<S> e n\<close>
[PROOF STATE]
proof (chain)
picking this:
\<S> e' n = \<S> e' m
\<S> e' n = \<S> e n
m \<notin> cc
[PROOF STEP]
have "\<S> e m = \<S> e n"
[PROOF STATE]
proof (prove)
using this:
\<S> e' n = \<S> e' m
\<S> e' n = \<S> e n
m \<notin> cc

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

goal (1 subgoal):
 1. n \<notin> cc \<Longrightarrow> m \<in> \<S> e' n
[PROOF STEP]
with S_reflexive[OF wf, of m]
[PROOF STATE]
proof (chain)
picking this:
m \<in> \<S> e m
\<S> e m = \<S> e n
[PROOF STEP]
have "m \<in> \<S> e n"
[PROOF STATE]
proof (prove)
using this:
m \<in> \<S> e m
\<S> e m = \<S> e n

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

goal (1 subgoal):
 1. n \<notin> cc \<Longrightarrow> m \<in> \<S> e' n
[PROOF STEP]
with \<open>\<S> e' n = \<S> e n\<close>
[PROOF STATE]
proof (chain)
picking this:
\<S> e' n = \<S> e n
m \<in> \<S> e n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<S> e' n = \<S> e n
m \<in> \<S> e n

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
m \<in> \<S> e' n

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(m \<in> \<S> e' n) = (\<S> e' n = \<S> e' m)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>n m. (m \<in> \<S> e' n) = (\<S> e' n = \<S> e' m)

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

goal (1 subgoal):
 1. wf_env e'
[PROOF STEP]
have "\<forall>n. n \<notin> visited e' \<longrightarrow> \<S> e' n = {n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. n \<notin> visited e' \<longrightarrow> \<S> e' n = {n}
[PROOF STEP]
proof (clarify)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. n \<notin> visited e' \<Longrightarrow> \<S> e' n = {n}
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. n \<notin> visited e' \<Longrightarrow> \<S> e' n = {n}
[PROOF STEP]
assume "n \<notin> visited e'"
[PROOF STATE]
proof (state)
this:
n \<notin> visited e'

goal (1 subgoal):
 1. \<And>n. n \<notin> visited e' \<Longrightarrow> \<S> e' n = {n}
[PROOF STEP]
hence "n \<notin> visited e"
[PROOF STATE]
proof (prove)
using this:
n \<notin> visited e'

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

goal (1 subgoal):
 1. \<And>n. n \<notin> visited e' \<Longrightarrow> \<S> e' n = {n}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
n \<notin> visited e

goal (1 subgoal):
 1. \<And>n. n \<notin> visited e' \<Longrightarrow> \<S> e' n = {n}
[PROOF STEP]
have "n \<notin> cc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<notin> cc
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n \<in> cc \<Longrightarrow> False
[PROOF STEP]
assume "n \<in> cc"
[PROOF STATE]
proof (state)
this:
n \<in> cc

goal (1 subgoal):
 1. n \<in> cc \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n \<in> cc
[PROOF STEP]
obtain m where "m \<in> set pfx \<union> {hd (stack e')}" "n \<in> \<S> e m"
[PROOF STATE]
proof (prove)
using this:
n \<in> cc

goal (1 subgoal):
 1. (\<And>m. \<lbrakk>m \<in> set pfx \<union> {hd (stack e')}; n \<in> \<S> e m\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: cc_def)
[PROOF STATE]
proof (state)
this:
m \<in> set pfx \<union> {hd (stack e')}
n \<in> \<S> e m

goal (1 subgoal):
 1. n \<in> cc \<Longrightarrow> False
[PROOF STEP]
with \<open>stack e = pfx @ stack e'\<close> \<open>stack e' \<noteq> []\<close>
[PROOF STATE]
proof (chain)
picking this:
stack e = pfx @ stack e'
stack e' \<noteq> []
m \<in> set pfx \<union> {hd (stack e')}
n \<in> \<S> e m
[PROOF STEP]
have "m \<in> set (stack e)"
[PROOF STATE]
proof (prove)
using this:
stack e = pfx @ stack e'
stack e' \<noteq> []
m \<in> set pfx \<union> {hd (stack e')}
n \<in> \<S> e m

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

goal (1 subgoal):
 1. n \<in> cc \<Longrightarrow> False
[PROOF STEP]
with stack_class[OF wf this \<open>n \<in> \<S> e m\<close>] \<open>n \<notin> visited e\<close>
[PROOF STATE]
proof (chain)
picking this:
n \<in> visited e - explored e
n \<notin> visited e
m \<in> set (stack e)
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
n \<in> visited e - explored e
n \<notin> visited e
m \<in> set (stack e)

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:
n \<notin> cc

goal (1 subgoal):
 1. \<And>n. n \<notin> visited e' \<Longrightarrow> \<S> e' n = {n}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
n \<notin> visited e
n \<notin> cc
[PROOF STEP]
show "\<S> e' n = {n}"
[PROOF STATE]
proof (prove)
using this:
n \<notin> visited e
n \<notin> cc

goal (1 subgoal):
 1. \<S> e' n = {n}
[PROOF STEP]
using wf
[PROOF STATE]
proof (prove)
using this:
n \<notin> visited e
n \<notin> cc
wf_env e

goal (1 subgoal):
 1. \<S> e' n = {n}
[PROOF STEP]
by (auto simp: wf_env_def Se')
[PROOF STATE]
proof (state)
this:
\<S> e' n = {n}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>n. n \<notin> visited e' \<longrightarrow> \<S> e' n = {n}

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

goal (1 subgoal):
 1. wf_env e'
[PROOF STEP]
have "\<forall>n \<in> set (stack e'). \<forall>m \<in> set (stack e'). n \<noteq> m \<longrightarrow> \<S> e' n \<inter> \<S> e' m = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n\<in>set (stack e'). \<forall>m\<in>set (stack e'). n \<noteq> m \<longrightarrow> \<S> e' n \<inter> \<S> e' m = {}
[PROOF STEP]
proof (clarify)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n m. \<lbrakk>n \<in> set (stack e'); m \<in> set (stack e'); n \<noteq> m\<rbrakk> \<Longrightarrow> \<S> e' n \<inter> \<S> e' m = {}
[PROOF STEP]
fix n m
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n m. \<lbrakk>n \<in> set (stack e'); m \<in> set (stack e'); n \<noteq> m\<rbrakk> \<Longrightarrow> \<S> e' n \<inter> \<S> e' m = {}
[PROOF STEP]
assume "n \<in> set (stack e')" "m \<in> set (stack e')" "n \<noteq> m"
[PROOF STATE]
proof (state)
this:
n \<in> set (stack e')
m \<in> set (stack e')
n \<noteq> m

goal (1 subgoal):
 1. \<And>n m. \<lbrakk>n \<in> set (stack e'); m \<in> set (stack e'); n \<noteq> m\<rbrakk> \<Longrightarrow> \<S> e' n \<inter> \<S> e' m = {}
[PROOF STEP]
show "\<S> e' n \<inter> \<S> e' m = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<S> e' n \<inter> \<S> e' m = {}
[PROOF STEP]
proof (cases "n = hd (stack e')")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n = hd (stack e') \<Longrightarrow> \<S> e' n \<inter> \<S> e' m = {}
 2. n \<noteq> hd (stack e') \<Longrightarrow> \<S> e' n \<inter> \<S> e' m = {}
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
n = hd (stack e')

goal (2 subgoals):
 1. n = hd (stack e') \<Longrightarrow> \<S> e' n \<inter> \<S> e' m = {}
 2. n \<noteq> hd (stack e') \<Longrightarrow> \<S> e' n \<inter> \<S> e' m = {}
[PROOF STEP]
with \<open>m \<in> set (stack e')\<close> \<open>n \<noteq> m\<close> \<open>stack e' \<noteq> []\<close>
[PROOF STATE]
proof (chain)
picking this:
m \<in> set (stack e')
n \<noteq> m
stack e' \<noteq> []
n = hd (stack e')
[PROOF STEP]
have "m \<in> set (tl (stack e'))"
[PROOF STATE]
proof (prove)
using this:
m \<in> set (stack e')
n \<noteq> m
stack e' \<noteq> []
n = hd (stack e')

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

goal (2 subgoals):
 1. n = hd (stack e') \<Longrightarrow> \<S> e' n \<inter> \<S> e' m = {}
 2. n \<noteq> hd (stack e') \<Longrightarrow> \<S> e' n \<inter> \<S> e' m = {}
[PROOF STEP]
with True hd_cc tl_cc unite_S_tl[OF wf w]
[PROOF STATE]
proof (chain)
picking this:
n = hd (stack e')
\<S> e' (hd (stack e')) = cc
\<forall>n\<in>set (tl (stack e')). \<S> e n \<inter> cc = {}
?n \<in> set (tl (stack (unite v w e))) \<Longrightarrow> \<S> (unite v w e) ?n = \<S> e ?n
m \<in> set (tl (stack e'))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n = hd (stack e')
\<S> e' (hd (stack e')) = cc
\<forall>n\<in>set (tl (stack e')). \<S> e n \<inter> cc = {}
?n \<in> set (tl (stack (unite v w e))) \<Longrightarrow> \<S> (unite v w e) ?n = \<S> e ?n
m \<in> set (tl (stack e'))

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

goal (1 subgoal):
 1. n \<noteq> hd (stack e') \<Longrightarrow> \<S> e' n \<inter> \<S> e' m = {}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n \<noteq> hd (stack e') \<Longrightarrow> \<S> e' n \<inter> \<S> e' m = {}
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
n \<noteq> hd (stack e')

goal (1 subgoal):
 1. n \<noteq> hd (stack e') \<Longrightarrow> \<S> e' n \<inter> \<S> e' m = {}
[PROOF STEP]
with \<open>n \<in> set (stack e')\<close> \<open>stack e' \<noteq> []\<close>
[PROOF STATE]
proof (chain)
picking this:
n \<in> set (stack e')
stack e' \<noteq> []
n \<noteq> hd (stack e')
[PROOF STEP]
have "n \<in> set (tl (stack e'))"
[PROOF STATE]
proof (prove)
using this:
n \<in> set (stack e')
stack e' \<noteq> []
n \<noteq> hd (stack e')

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

goal (1 subgoal):
 1. n \<noteq> hd (stack e') \<Longrightarrow> \<S> e' n \<inter> \<S> e' m = {}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<S> e' n \<inter> \<S> e' m = {}
[PROOF STEP]
proof (cases "m = hd (stack e')")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. m = hd (stack e') \<Longrightarrow> \<S> e' n \<inter> \<S> e' m = {}
 2. m \<noteq> hd (stack e') \<Longrightarrow> \<S> e' n \<inter> \<S> e' m = {}
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
m = hd (stack e')

goal (2 subgoals):
 1. m = hd (stack e') \<Longrightarrow> \<S> e' n \<inter> \<S> e' m = {}
 2. m \<noteq> hd (stack e') \<Longrightarrow> \<S> e' n \<inter> \<S> e' m = {}
[PROOF STEP]
with \<open>n \<in> set (tl (stack e'))\<close> hd_cc tl_cc unite_S_tl[OF wf w]
[PROOF STATE]
proof (chain)
picking this:
n \<in> set (tl (stack e'))
\<S> e' (hd (stack e')) = cc
\<forall>n\<in>set (tl (stack e')). \<S> e n \<inter> cc = {}
?n \<in> set (tl (stack (unite v w e))) \<Longrightarrow> \<S> (unite v w e) ?n = \<S> e ?n
m = hd (stack e')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n \<in> set (tl (stack e'))
\<S> e' (hd (stack e')) = cc
\<forall>n\<in>set (tl (stack e')). \<S> e n \<inter> cc = {}
?n \<in> set (tl (stack (unite v w e))) \<Longrightarrow> \<S> (unite v w e) ?n = \<S> e ?n
m = hd (stack e')

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

goal (1 subgoal):
 1. m \<noteq> hd (stack e') \<Longrightarrow> \<S> e' n \<inter> \<S> e' m = {}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. m \<noteq> hd (stack e') \<Longrightarrow> \<S> e' n \<inter> \<S> e' m = {}
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
m \<noteq> hd (stack e')

goal (1 subgoal):
 1. m \<noteq> hd (stack e') \<Longrightarrow> \<S> e' n \<inter> \<S> e' m = {}
[PROOF STEP]
with \<open>m \<in> set (stack e')\<close> \<open>stack e' \<noteq> []\<close>
[PROOF STATE]
proof (chain)
picking this:
m \<in> set (stack e')
stack e' \<noteq> []
m \<noteq> hd (stack e')
[PROOF STEP]
have "m \<in> set (tl (stack e'))"
[PROOF STATE]
proof (prove)
using this:
m \<in> set (stack e')
stack e' \<noteq> []
m \<noteq> hd (stack e')

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

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

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

goal (1 subgoal):
 1. m \<noteq> hd (stack e') \<Longrightarrow> \<S> e' n \<inter> \<S> e' m = {}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<S> e' m = \<S> e m \<and> \<S> e' n = \<S> e n

goal (1 subgoal):
 1. m \<noteq> hd (stack e') \<Longrightarrow> \<S> e' n \<inter> \<S> e' m = {}
[PROOF STEP]
from \<open>m \<in> set (stack e')\<close> \<open>n \<in> set (stack e')\<close> \<open>stack e = pfx @ stack e'\<close>
[PROOF STATE]
proof (chain)
picking this:
m \<in> set (stack e')
n \<in> set (stack e')
stack e = pfx @ stack e'
[PROOF STEP]
have "m \<in> set (stack e) \<and> n \<in> set (stack e)"
[PROOF STATE]
proof (prove)
using this:
m \<in> set (stack e')
n \<in> set (stack e')
stack e = pfx @ stack e'

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

goal (1 subgoal):
 1. m \<noteq> hd (stack e') \<Longrightarrow> \<S> e' n \<inter> \<S> e' m = {}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<S> e' m = \<S> e m \<and> \<S> e' n = \<S> e n
m \<in> set (stack e) \<and> n \<in> set (stack e)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<S> e' m = \<S> e m \<and> \<S> e' n = \<S> e n
m \<in> set (stack e) \<and> n \<in> set (stack e)

goal (1 subgoal):
 1. \<S> e' n \<inter> \<S> e' m = {}
[PROOF STEP]
using wf \<open>n \<noteq> m\<close>
[PROOF STATE]
proof (prove)
using this:
\<S> e' m = \<S> e m \<and> \<S> e' n = \<S> e n
m \<in> set (stack e) \<and> n \<in> set (stack e)
wf_env e
n \<noteq> m

goal (1 subgoal):
 1. \<S> e' n \<inter> \<S> e' m = {}
[PROOF STEP]
by (auto simp: wf_env_def)
[PROOF STATE]
proof (state)
this:
\<S> e' n \<inter> \<S> e' m = {}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<S> e' n \<inter> \<S> e' m = {}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<S> e' n \<inter> \<S> e' m = {}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>n\<in>set (stack e'). \<forall>m\<in>set (stack e'). n \<noteq> m \<longrightarrow> \<S> e' n \<inter> \<S> e' m = {}

goal (1 subgoal):
 1. wf_env e'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>n\<in>set (stack e'). \<forall>m\<in>set (stack e'). n \<noteq> m \<longrightarrow> \<S> e' n \<inter> \<S> e' m = {}

goal (1 subgoal):
 1. wf_env e'
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<forall>n\<in>set (stack e'). \<forall>m\<in>set (stack e'). n \<noteq> m \<longrightarrow> \<S> e' n \<inter> \<S> e' m = {}

goal (1 subgoal):
 1. wf_env e'
[PROOF STEP]
from unite_S_equal[OF wf w]
[PROOF STATE]
proof (chain)
picking this:
\<Union> {\<S> (unite v w e) n |n. n \<in> set (stack (unite v w e))} = \<Union> {\<S> e n |n. n \<in> set (stack e)}
[PROOF STEP]
have "\<Union> {\<S> e' n | n. n \<in> set (stack e')} = \<Union> {\<S> e n | n. n \<in> set (stack e)}"
[PROOF STATE]
proof (prove)
using this:
\<Union> {\<S> (unite v w e) n |n. n \<in> set (stack (unite v w e))} = \<Union> {\<S> e n |n. n \<in> set (stack e)}

goal (1 subgoal):
 1. \<Union> {\<S> e' n |n. n \<in> set (stack e')} = \<Union> {\<S> e n |n. n \<in> set (stack e)}
[PROOF STEP]
by (simp add: e'_def)
[PROOF STATE]
proof (state)
this:
\<Union> {\<S> e' n |n. n \<in> set (stack e')} = \<Union> {\<S> e n |n. n \<in> set (stack e)}

goal (1 subgoal):
 1. wf_env e'
[PROOF STEP]
with wf
[PROOF STATE]
proof (chain)
picking this:
wf_env e
\<Union> {\<S> e' n |n. n \<in> set (stack e')} = \<Union> {\<S> e n |n. n \<in> set (stack e)}
[PROOF STEP]
have "\<Union> {\<S> e' n | n. n \<in> set (stack e')} = visited e - explored e"
[PROOF STATE]
proof (prove)
using this:
wf_env e
\<Union> {\<S> e' n |n. n \<in> set (stack e')} = \<Union> {\<S> e n |n. n \<in> set (stack e)}

goal (1 subgoal):
 1. \<Union> {\<S> e' n |n. n \<in> set (stack e')} = visited e - explored e
[PROOF STEP]
by (simp add: wf_env_def)
[PROOF STATE]
proof (state)
this:
\<Union> {\<S> e' n |n. n \<in> set (stack e')} = visited e - explored e

goal (1 subgoal):
 1. wf_env e'
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<Union> {\<S> e' n |n. n \<in> set (stack e')} = visited e - explored e

goal (1 subgoal):
 1. wf_env e'
[PROOF STEP]
hence "\<Union> {\<S> e' n | n. n \<in> set (stack e')} = visited e' - explored e'"
[PROOF STATE]
proof (prove)
using this:
\<Union> {\<S> e' n |n. n \<in> set (stack e')} = visited e - explored e

goal (1 subgoal):
 1. \<Union> {\<S> e' n |n. n \<in> set (stack e')} = visited e' - explored e'
[PROOF STEP]
by (simp add: e'_def unite_def)
[PROOF STATE]
proof (state)
this:
\<Union> {\<S> e' n |n. n \<in> set (stack e')} = visited e' - explored e'

goal (1 subgoal):
 1. wf_env e'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Union> {\<S> e' n |n. n \<in> set (stack e')} = visited e' - explored e'

goal (1 subgoal):
 1. wf_env e'
[PROOF STEP]
have "\<forall>n \<in> set (stack e'). \<forall>m \<in> \<S> e' n.
           m \<in> set (cstack e') \<longrightarrow> m \<preceq> n in cstack e'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n\<in>set (stack e'). \<forall>m\<in>\<S> e' n. m \<in> set (cstack e') \<longrightarrow> m \<preceq> n in cstack e'
[PROOF STEP]
proof (clarify)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n m. \<lbrakk>n \<in> set (stack e'); m \<in> \<S> e' n; m \<in> set (cstack e')\<rbrakk> \<Longrightarrow> m \<preceq> n in cstack e'
[PROOF STEP]
fix n m
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n m. \<lbrakk>n \<in> set (stack e'); m \<in> \<S> e' n; m \<in> set (cstack e')\<rbrakk> \<Longrightarrow> m \<preceq> n in cstack e'
[PROOF STEP]
assume "n \<in> set (stack e')" "m \<in> \<S> e' n" "m \<in> set (cstack e')"
[PROOF STATE]
proof (state)
this:
n \<in> set (stack e')
m \<in> \<S> e' n
m \<in> set (cstack e')

goal (1 subgoal):
 1. \<And>n m. \<lbrakk>n \<in> set (stack e'); m \<in> \<S> e' n; m \<in> set (cstack e')\<rbrakk> \<Longrightarrow> m \<preceq> n in cstack e'
[PROOF STEP]
from \<open>m \<in> set (cstack e')\<close>
[PROOF STATE]
proof (chain)
picking this:
m \<in> set (cstack e')
[PROOF STEP]
have "m \<in> set (cstack e)"
[PROOF STATE]
proof (prove)
using this:
m \<in> set (cstack e')

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

goal (1 subgoal):
 1. \<And>n m. \<lbrakk>n \<in> set (stack e'); m \<in> \<S> e' n; m \<in> set (cstack e')\<rbrakk> \<Longrightarrow> m \<preceq> n in cstack e'
[PROOF STEP]
have "m \<preceq> n in cstack e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m \<preceq> n in cstack e
[PROOF STEP]
proof (cases "n = hd (stack e')")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n = hd (stack e') \<Longrightarrow> m \<preceq> n in cstack e
 2. n \<noteq> hd (stack e') \<Longrightarrow> m \<preceq> n in cstack e
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
n = hd (stack e')

goal (2 subgoals):
 1. n = hd (stack e') \<Longrightarrow> m \<preceq> n in cstack e
 2. n \<noteq> hd (stack e') \<Longrightarrow> m \<preceq> n in cstack e
[PROOF STEP]
with \<open>m \<in> \<S> e' n\<close>
[PROOF STATE]
proof (chain)
picking this:
m \<in> \<S> e' n
n = hd (stack e')
[PROOF STEP]
have "m \<in> cc"
[PROOF STATE]
proof (prove)
using this:
m \<in> \<S> e' n
n = hd (stack e')

goal (1 subgoal):
 1. m \<in> cc
[PROOF STEP]
by (simp add: hd_cc)
[PROOF STATE]
proof (state)
this:
m \<in> cc

goal (2 subgoals):
 1. n = hd (stack e') \<Longrightarrow> m \<preceq> n in cstack e
 2. n \<noteq> hd (stack e') \<Longrightarrow> m \<preceq> n in cstack e
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
m \<in> cc
[PROOF STEP]
obtain l where
        "l \<in> set pfx \<union> {hd (stack e')}" "m \<in> \<S> e l"
[PROOF STATE]
proof (prove)
using this:
m \<in> cc

goal (1 subgoal):
 1. (\<And>l. \<lbrakk>l \<in> set pfx \<union> {hd (stack e')}; m \<in> \<S> e l\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: cc_def)
[PROOF STATE]
proof (state)
this:
l \<in> set pfx \<union> {hd (stack e')}
m \<in> \<S> e l

goal (2 subgoals):
 1. n = hd (stack e') \<Longrightarrow> m \<preceq> n in cstack e
 2. n \<noteq> hd (stack e') \<Longrightarrow> m \<preceq> n in cstack e
[PROOF STEP]
with \<open>stack e = pfx @ stack e'\<close> \<open>stack e' \<noteq> []\<close>
[PROOF STATE]
proof (chain)
picking this:
stack e = pfx @ stack e'
stack e' \<noteq> []
l \<in> set pfx \<union> {hd (stack e')}
m \<in> \<S> e l
[PROOF STEP]
have "l \<in> set (stack e)"
[PROOF STATE]
proof (prove)
using this:
stack e = pfx @ stack e'
stack e' \<noteq> []
l \<in> set pfx \<union> {hd (stack e')}
m \<in> \<S> e l

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

goal (2 subgoals):
 1. n = hd (stack e') \<Longrightarrow> m \<preceq> n in cstack e
 2. n \<noteq> hd (stack e') \<Longrightarrow> m \<preceq> n in cstack e
[PROOF STEP]
with \<open>m \<in> \<S> e l\<close> \<open>m \<in> set (cstack e)\<close> wf
[PROOF STATE]
proof (chain)
picking this:
m \<in> \<S> e l
m \<in> set (cstack e)
wf_env e
l \<in> set (stack e)
[PROOF STEP]
have "m \<preceq> l in cstack e"
[PROOF STATE]
proof (prove)
using this:
m \<in> \<S> e l
m \<in> set (cstack e)
wf_env e
l \<in> set (stack e)

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

goal (2 subgoals):
 1. n = hd (stack e') \<Longrightarrow> m \<preceq> n in cstack e
 2. n \<noteq> hd (stack e') \<Longrightarrow> m \<preceq> n in cstack e
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
m \<preceq> l in cstack e

goal (2 subgoals):
 1. n = hd (stack e') \<Longrightarrow> m \<preceq> n in cstack e
 2. n \<noteq> hd (stack e') \<Longrightarrow> m \<preceq> n in cstack e
[PROOF STEP]
from \<open>l \<in> set pfx \<union> {hd (stack e')}\<close> True
           \<open>stack e = pfx @ stack e'\<close> \<open>stack e' \<noteq> []\<close>
[PROOF STATE]
proof (chain)
picking this:
l \<in> set pfx \<union> {hd (stack e')}
n = hd (stack e')
stack e = pfx @ stack e'
stack e' \<noteq> []
[PROOF STEP]
have "l \<preceq> n in stack e"
[PROOF STATE]
proof (prove)
using this:
l \<in> set pfx \<union> {hd (stack e')}
n = hd (stack e')
stack e = pfx @ stack e'
stack e' \<noteq> []

goal (1 subgoal):
 1. l \<preceq> n in stack e
[PROOF STEP]
by (metis List.set_insert empty_set hd_Cons_tl insert_Nil set_append split_list_precedes)
[PROOF STATE]
proof (state)
this:
l \<preceq> n in stack e

goal (2 subgoals):
 1. n = hd (stack e') \<Longrightarrow> m \<preceq> n in cstack e
 2. n \<noteq> hd (stack e') \<Longrightarrow> m \<preceq> n in cstack e
[PROOF STEP]
with wf
[PROOF STATE]
proof (chain)
picking this:
wf_env e
l \<preceq> n in stack e
[PROOF STEP]
have "l \<preceq> n in cstack e"
[PROOF STATE]
proof (prove)
using this:
wf_env e
l \<preceq> n in stack e

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

goal (2 subgoals):
 1. n = hd (stack e') \<Longrightarrow> m \<preceq> n in cstack e
 2. n \<noteq> hd (stack e') \<Longrightarrow> m \<preceq> n in cstack e
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
m \<preceq> l in cstack e
l \<preceq> n in cstack e
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
m \<preceq> l in cstack e
l \<preceq> n in cstack e

goal (1 subgoal):
 1. m \<preceq> n in cstack e
[PROOF STEP]
using wf
[PROOF STATE]
proof (prove)
using this:
m \<preceq> l in cstack e
l \<preceq> n in cstack e
wf_env e

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

goal (1 subgoal):
 1. m \<preceq> n in cstack e
[PROOF STEP]
by (meson precedes_trans)
[PROOF STATE]
proof (state)
this:
m \<preceq> n in cstack e

goal (1 subgoal):
 1. n \<noteq> hd (stack e') \<Longrightarrow> m \<preceq> n in cstack e
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n \<noteq> hd (stack e') \<Longrightarrow> m \<preceq> n in cstack e
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
n \<noteq> hd (stack e')

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

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

goal (1 subgoal):
 1. n \<noteq> hd (stack e') \<Longrightarrow> m \<preceq> n in cstack e
[PROOF STEP]
with unite_S_tl[OF wf w] \<open>m \<in> \<S> e' n\<close>
[PROOF STATE]
proof (chain)
picking this:
?n \<in> set (tl (stack (unite v w e))) \<Longrightarrow> \<S> (unite v w e) ?n = \<S> e ?n
m \<in> \<S> e' n
n \<in> set (tl (stack e'))
[PROOF STEP]
have "m \<in> \<S> e n"
[PROOF STATE]
proof (prove)
using this:
?n \<in> set (tl (stack (unite v w e))) \<Longrightarrow> \<S> (unite v w e) ?n = \<S> e ?n
m \<in> \<S> e' n
n \<in> set (tl (stack e'))

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

goal (1 subgoal):
 1. n \<noteq> hd (stack e') \<Longrightarrow> m \<preceq> n in cstack e
[PROOF STEP]
with \<open>n \<in> set (stack e')\<close> \<open>stack e = pfx @ stack e'\<close>
           \<open>m \<in> set (cstack e)\<close> wf
[PROOF STATE]
proof (chain)
picking this:
n \<in> set (stack e')
stack e = pfx @ stack e'
m \<in> set (cstack e)
wf_env e
m \<in> \<S> e n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n \<in> set (stack e')
stack e = pfx @ stack e'
m \<in> set (cstack e)
wf_env e
m \<in> \<S> e n

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
m \<preceq> n in cstack e

goal (1 subgoal):
 1. \<And>n m. \<lbrakk>n \<in> set (stack e'); m \<in> \<S> e' n; m \<in> set (cstack e')\<rbrakk> \<Longrightarrow> m \<preceq> n in cstack e'
[PROOF STEP]
thus "m \<preceq> n in cstack e'"
[PROOF STATE]
proof (prove)
using this:
m \<preceq> n in cstack e

goal (1 subgoal):
 1. m \<preceq> n in cstack e'
[PROOF STEP]
by (simp add: e'_def unite_def)
[PROOF STATE]
proof (state)
this:
m \<preceq> n in cstack e'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>n\<in>set (stack e'). \<forall>m\<in>\<S> e' n. m \<in> set (cstack e') \<longrightarrow> m \<preceq> n in cstack e'

goal (1 subgoal):
 1. wf_env e'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>n\<in>set (stack e'). \<forall>m\<in>\<S> e' n. m \<in> set (cstack e') \<longrightarrow> m \<preceq> n in cstack e'

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

goal (1 subgoal):
 1. \<And>n m u. \<lbrakk>u \<in> \<S> e' n; n \<preceq> m in stack e'; n \<noteq> m; reachable_avoiding u m (unvisited e' n)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
proof (cases "x = hd (stack e')")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = hd (stack e') \<Longrightarrow> False
 2. x \<noteq> hd (stack e') \<Longrightarrow> False
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x = hd (stack e')

goal (2 subgoals):
 1. x = hd (stack e') \<Longrightarrow> False
 2. x \<noteq> hd (stack e') \<Longrightarrow> False
[PROOF STEP]
hence "\<S> e' x = cc"
[PROOF STATE]
proof (prove)
using this:
x = hd (stack e')

goal (1 subgoal):
 1. \<S> e' x = cc
[PROOF STEP]
by (simp add: hd_cc)
[PROOF STATE]
proof (state)
this:
\<S> e' x = cc

goal (2 subgoals):
 1. x = hd (stack e') \<Longrightarrow> False
 2. x \<noteq> hd (stack e') \<Longrightarrow> False
[PROOF STEP]
with \<open>u \<in> \<S> e' x\<close>
[PROOF STATE]
proof (chain)
picking this:
u \<in> \<S> e' x
\<S> e' x = cc
[PROOF STEP]
obtain x' where
        x': "x' \<in> set pfx \<union> {hd (stack e')}" "u \<in> \<S> e x'"
[PROOF STATE]
proof (prove)
using this:
u \<in> \<S> e' x
\<S> e' x = cc

goal (1 subgoal):
 1. (\<And>x'. \<lbrakk>x' \<in> set pfx \<union> {hd (stack e')}; u \<in> \<S> e x'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: cc_def)
[PROOF STATE]
proof (state)
this:
x' \<in> set pfx \<union> {hd (stack e')}
u \<in> \<S> e x'

goal (2 subgoals):
 1. x = hd (stack e') \<Longrightarrow> False
 2. x \<noteq> hd (stack e') \<Longrightarrow> False
[PROOF STEP]
from \<open>stack e = pfx @ stack e'\<close> \<open>stack e' \<noteq> []\<close>
[PROOF STATE]
proof (chain)
picking this:
stack e = pfx @ stack e'
stack e' \<noteq> []
[PROOF STEP]
have "stack e = pfx @ (hd (stack e') # tl (stack e'))"
[PROOF STATE]
proof (prove)
using this:
stack e = pfx @ stack e'
stack e' \<noteq> []

goal (1 subgoal):
 1. stack e = pfx @ hd (stack e') # tl (stack e')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
stack e = pfx @ hd (stack e') # tl (stack e')

goal (2 subgoals):
 1. x = hd (stack e') \<Longrightarrow> False
 2. x \<noteq> hd (stack e') \<Longrightarrow> False
[PROOF STEP]
with x' True
[PROOF STATE]
proof (chain)
picking this:
x' \<in> set pfx \<union> {hd (stack e')}
u \<in> \<S> e x'
x = hd (stack e')
stack e = pfx @ hd (stack e') # tl (stack e')
[PROOF STEP]
have "x' \<preceq> x in stack e"
[PROOF STATE]
proof (prove)
using this:
x' \<in> set pfx \<union> {hd (stack e')}
u \<in> \<S> e x'
x = hd (stack e')
stack e = pfx @ hd (stack e') # tl (stack e')

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

goal (2 subgoals):
 1. x = hd (stack e') \<Longrightarrow> False
 2. x \<noteq> hd (stack e') \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x' \<preceq> x in stack e

goal (2 subgoals):
 1. x = hd (stack e') \<Longrightarrow> False
 2. x \<noteq> hd (stack e') \<Longrightarrow> False
[PROOF STEP]
from xy \<open>stack e = pfx @ stack e'\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<preceq> y in stack e'
x \<noteq> y
stack e = pfx @ stack e'
[PROOF STEP]
have "x \<preceq> y in stack e"
[PROOF STATE]
proof (prove)
using this:
x \<preceq> y in stack e'
x \<noteq> y
stack e = pfx @ stack e'

goal (1 subgoal):
 1. x \<preceq> y in stack e
[PROOF STEP]
by (simp add: precedes_append_left)
[PROOF STATE]
proof (state)
this:
x \<preceq> y in stack e

goal (2 subgoals):
 1. x = hd (stack e') \<Longrightarrow> False
 2. x \<noteq> hd (stack e') \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x' \<preceq> x in stack e
x \<preceq> y in stack e
[PROOF STEP]
have "x' \<preceq> y in stack e"
[PROOF STATE]
proof (prove)
using this:
x' \<preceq> x in stack e
x \<preceq> y in stack e

goal (1 subgoal):
 1. x' \<preceq> y in stack e
[PROOF STEP]
using wf
[PROOF STATE]
proof (prove)
using this:
x' \<preceq> x in stack e
x \<preceq> y in stack e
wf_env e

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

goal (2 subgoals):
 1. x = hd (stack e') \<Longrightarrow> False
 2. x \<noteq> hd (stack e') \<Longrightarrow> False
[PROOF STEP]
from \<open>x' \<preceq> x in stack e\<close> \<open>x \<preceq> y in stack e\<close> wf \<open>x \<noteq> y\<close>
[PROOF STATE]
proof (chain)
picking this:
x' \<preceq> x in stack e
x \<preceq> y in stack e
wf_env e
x \<noteq> y
[PROOF STEP]
have "x' \<noteq> y"
[PROOF STATE]
proof (prove)
using this:
x' \<preceq> x in stack e
x \<preceq> y in stack e
wf_env e
x \<noteq> y

goal (1 subgoal):
 1. x' \<noteq> y
[PROOF STEP]
by (auto simp: wf_env_def dest: precedes_antisym)
[PROOF STATE]
proof (state)
this:
x' \<noteq> y

goal (2 subgoals):
 1. x = hd (stack e') \<Longrightarrow> False
 2. x \<noteq> hd (stack e') \<Longrightarrow> False
[PROOF STEP]
let ?unv = "\<Union> {unvisited e y | y. y \<in> set pfx \<union> {hd (stack e')}}"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = hd (stack e') \<Longrightarrow> False
 2. x \<noteq> hd (stack e') \<Longrightarrow> False
[PROOF STEP]
from \<open>\<S> e' x = cc\<close>
[PROOF STATE]
proof (chain)
picking this:
\<S> e' x = cc
[PROOF STEP]
have "?unv = unvisited e' x"
[PROOF STATE]
proof (prove)
using this:
\<S> e' x = cc

goal (1 subgoal):
 1. \<Union> {unvisited e y |y. y \<in> set pfx \<union> {hd (stack e')}} = unvisited e' x
[PROOF STEP]
by (auto simp: unvisited_def cc_def e'_def unite_def)
[PROOF STATE]
proof (state)
this:
\<Union> {unvisited e y |y. y \<in> set pfx \<union> {hd (stack e')}} = unvisited e' x

goal (2 subgoals):
 1. x = hd (stack e') \<Longrightarrow> False
 2. x \<noteq> hd (stack e') \<Longrightarrow> False
[PROOF STEP]
with \<open>reachable_avoiding u y (unvisited e' x)\<close>
[PROOF STATE]
proof (chain)
picking this:
reachable_avoiding u y (unvisited e' x)
\<Union> {unvisited e y |y. y \<in> set pfx \<union> {hd (stack e')}} = unvisited e' x
[PROOF STEP]
have "reachable_avoiding u y ?unv"
[PROOF STATE]
proof (prove)
using this:
reachable_avoiding u y (unvisited e' x)
\<Union> {unvisited e y |y. y \<in> set pfx \<union> {hd (stack e')}} = unvisited e' x

goal (1 subgoal):
 1. reachable_avoiding u y (\<Union> {unvisited e y |y. y \<in> set pfx \<union> {hd (stack e')}})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
reachable_avoiding u y (\<Union> {unvisited e y |y. y \<in> set pfx \<union> {hd (stack e')}})

goal (2 subgoals):
 1. x = hd (stack e') \<Longrightarrow> False
 2. x \<noteq> hd (stack e') \<Longrightarrow> False
[PROOF STEP]
with x'
[PROOF STATE]
proof (chain)
picking this:
x' \<in> set pfx \<union> {hd (stack e')}
u \<in> \<S> e x'
reachable_avoiding u y (\<Union> {unvisited e y |y. y \<in> set pfx \<union> {hd (stack e')}})
[PROOF STEP]
have "reachable_avoiding u y (unvisited e x')"
[PROOF STATE]
proof (prove)
using this:
x' \<in> set pfx \<union> {hd (stack e')}
u \<in> \<S> e x'
reachable_avoiding u y (\<Union> {unvisited e y |y. y \<in> set pfx \<union> {hd (stack e')}})

goal (1 subgoal):
 1. reachable_avoiding u y (unvisited e x')
[PROOF STEP]
by (blast intro: ra_mono)
[PROOF STATE]
proof (state)
this:
reachable_avoiding u y (unvisited e x')

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

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

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

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

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

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

goal (1 subgoal):
 1. u \<in> \<S> e x
[PROOF STEP]
by (auto simp add: unite_S_tl[OF wf w] e'_def)
[PROOF STATE]
proof (state)
this:
u \<in> \<S> e x

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

goal (1 subgoal):
 1. x \<noteq> hd (stack e') \<Longrightarrow> False
[PROOF STEP]
from \<open>x \<preceq> y in stack e'\<close> \<open>stack e = pfx @ stack e'\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<preceq> y in stack e'
stack e = pfx @ stack e'
[PROOF STEP]
have "x \<preceq> y in stack e"
[PROOF STATE]
proof (prove)
using this:
x \<preceq> y in stack e'
stack e = pfx @ stack e'

goal (1 subgoal):
 1. x \<preceq> y in stack e
[PROOF STEP]
by (simp add: precedes_append_left)
[PROOF STATE]
proof (state)
this:
x \<preceq> y in stack e

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

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

goal (1 subgoal):
 1. unvisited e' x = unvisited e x
[PROOF STEP]
by (auto simp: unvisited_def e'_def unite_def)
[PROOF STATE]
proof (state)
this:
unvisited e' x = unvisited e x

goal (1 subgoal):
 1. x \<noteq> hd (stack e') \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
u \<in> \<S> e x
x \<preceq> y in stack e
unvisited e' x = unvisited e x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
u \<in> \<S> e x
x \<preceq> y in stack e
unvisited e' x = unvisited e x

goal (1 subgoal):
 1. False
[PROOF STEP]
using \<open>x \<noteq> y\<close> \<open>reachable_avoiding u y (unvisited e' x)\<close> wf
[PROOF STATE]
proof (prove)
using this:
u \<in> \<S> e x
x \<preceq> y in stack e
unvisited e' x = unvisited e x
x \<noteq> y
reachable_avoiding u y (unvisited e' x)
wf_env e

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

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

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

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

goal (1 subgoal):
 1. wf_env e'
[PROOF STEP]
have "\<forall>n. is_subscc (\<S> e' n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. is_subscc (\<S> e' n)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. is_subscc (\<S> e' n)
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. is_subscc (\<S> e' n)
[PROOF STEP]
show "is_subscc (\<S> e' n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_subscc (\<S> e' n)
[PROOF STEP]
proof (cases "n \<in> cc")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n \<in> cc \<Longrightarrow> is_subscc (\<S> e' n)
 2. n \<notin> cc \<Longrightarrow> is_subscc (\<S> e' n)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
n \<in> cc

goal (2 subgoals):
 1. n \<in> cc \<Longrightarrow> is_subscc (\<S> e' n)
 2. n \<notin> cc \<Longrightarrow> is_subscc (\<S> e' n)
[PROOF STEP]
hence "\<S> e' n = cc"
[PROOF STATE]
proof (prove)
using this:
n \<in> cc

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

goal (2 subgoals):
 1. n \<in> cc \<Longrightarrow> is_subscc (\<S> e' n)
 2. n \<notin> cc \<Longrightarrow> is_subscc (\<S> e' n)
[PROOF STEP]
with unite_subscc[OF pre w] hd_cc
[PROOF STATE]
proof (chain)
picking this:
is_subscc (\<S> (unite v w e) (hd (stack (unite v w e))))
\<S> e' (hd (stack e')) = cc
\<S> e' n = cc
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
is_subscc (\<S> (unite v w e) (hd (stack (unite v w e))))
\<S> e' (hd (stack e')) = cc
\<S> e' n = cc

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

goal (1 subgoal):
 1. n \<notin> cc \<Longrightarrow> is_subscc (\<S> e' n)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n \<notin> cc \<Longrightarrow> is_subscc (\<S> e' n)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
n \<notin> cc

goal (1 subgoal):
 1. n \<notin> cc \<Longrightarrow> is_subscc (\<S> e' n)
[PROOF STEP]
with wf
[PROOF STATE]
proof (chain)
picking this:
wf_env e
n \<notin> cc
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
wf_env e
n \<notin> cc

goal (1 subgoal):
 1. is_subscc (\<S> e' n)
[PROOF STEP]
by (simp add: Se' wf_env_def)
[PROOF STATE]
proof (state)
this:
is_subscc (\<S> e' n)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
is_subscc (\<S> e' n)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>n. is_subscc (\<S> e' n)

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed