[STATEMENT]
lemma reachable_visited:
  assumes e: "wf_env e"
      and v: "v \<in> visited e"
      and w: "reachable v w"
      and s: "\<forall>n \<in> visited e. \<forall>m \<in> successors n - vsuccs e n.
                 reachable v n \<longrightarrow> \<not> reachable m w"
  shows "w \<in> visited e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w \<in> visited e
[PROOF STEP]
using w v s
[PROOF STATE]
proof (prove)
using this:
reachable v w
v \<in> visited e
\<forall>n\<in>visited e. \<forall>m\<in>successors n - vsuccs e n. reachable v n \<longrightarrow> \<not> reachable m w

goal (1 subgoal):
 1. w \<in> visited e
[PROOF STEP]
proof (induction)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>x \<in> visited e; \<forall>n\<in>visited e. \<forall>m\<in>successors n - vsuccs e n. reachable x n \<longrightarrow> \<not> reachable m x\<rbrakk> \<Longrightarrow> x \<in> visited e
 2. \<And>x y z. \<lbrakk>edge x y; reachable y z; \<lbrakk>y \<in> visited e; \<forall>n\<in>visited e. \<forall>m\<in>successors n - vsuccs e n. reachable y n \<longrightarrow> \<not> reachable m z\<rbrakk> \<Longrightarrow> z \<in> visited e; x \<in> visited e; \<forall>n\<in>visited e. \<forall>m\<in>successors n - vsuccs e n. reachable x n \<longrightarrow> \<not> reachable m z\<rbrakk> \<Longrightarrow> z \<in> visited e
[PROOF STEP]
case (reachable_refl x)
[PROOF STATE]
proof (state)
this:
x \<in> visited e
\<forall>n\<in>visited e. \<forall>m\<in>successors n - vsuccs e n. reachable x n \<longrightarrow> \<not> reachable m x

goal (2 subgoals):
 1. \<And>x. \<lbrakk>x \<in> visited e; \<forall>n\<in>visited e. \<forall>m\<in>successors n - vsuccs e n. reachable x n \<longrightarrow> \<not> reachable m x\<rbrakk> \<Longrightarrow> x \<in> visited e
 2. \<And>x y z. \<lbrakk>edge x y; reachable y z; \<lbrakk>y \<in> visited e; \<forall>n\<in>visited e. \<forall>m\<in>successors n - vsuccs e n. reachable y n \<longrightarrow> \<not> reachable m z\<rbrakk> \<Longrightarrow> z \<in> visited e; x \<in> visited e; \<forall>n\<in>visited e. \<forall>m\<in>successors n - vsuccs e n. reachable x n \<longrightarrow> \<not> reachable m z\<rbrakk> \<Longrightarrow> z \<in> visited e
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> visited e
\<forall>n\<in>visited e. \<forall>m\<in>successors n - vsuccs e n. reachable x n \<longrightarrow> \<not> reachable m x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
x \<in> visited e
\<forall>n\<in>visited e. \<forall>m\<in>successors n - vsuccs e n. reachable x n \<longrightarrow> \<not> reachable m x

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

goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>edge x y; reachable y z; \<lbrakk>y \<in> visited e; \<forall>n\<in>visited e. \<forall>m\<in>successors n - vsuccs e n. reachable y n \<longrightarrow> \<not> reachable m z\<rbrakk> \<Longrightarrow> z \<in> visited e; x \<in> visited e; \<forall>n\<in>visited e. \<forall>m\<in>successors n - vsuccs e n. reachable x n \<longrightarrow> \<not> reachable m z\<rbrakk> \<Longrightarrow> z \<in> visited e
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>edge x y; reachable y z; \<lbrakk>y \<in> visited e; \<forall>n\<in>visited e. \<forall>m\<in>successors n - vsuccs e n. reachable y n \<longrightarrow> \<not> reachable m z\<rbrakk> \<Longrightarrow> z \<in> visited e; x \<in> visited e; \<forall>n\<in>visited e. \<forall>m\<in>successors n - vsuccs e n. reachable x n \<longrightarrow> \<not> reachable m z\<rbrakk> \<Longrightarrow> z \<in> visited e
[PROOF STEP]
case (reachable_succ x y z)
[PROOF STATE]
proof (state)
this:
edge x y
reachable y z
\<lbrakk>y \<in> visited e; \<forall>n\<in>visited e. \<forall>m\<in>successors n - vsuccs e n. reachable y n \<longrightarrow> \<not> reachable m z\<rbrakk> \<Longrightarrow> z \<in> visited e
x \<in> visited e
\<forall>n\<in>visited e. \<forall>m\<in>successors n - vsuccs e n. reachable x n \<longrightarrow> \<not> reachable m z

goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>edge x y; reachable y z; \<lbrakk>y \<in> visited e; \<forall>n\<in>visited e. \<forall>m\<in>successors n - vsuccs e n. reachable y n \<longrightarrow> \<not> reachable m z\<rbrakk> \<Longrightarrow> z \<in> visited e; x \<in> visited e; \<forall>n\<in>visited e. \<forall>m\<in>successors n - vsuccs e n. reachable x n \<longrightarrow> \<not> reachable m z\<rbrakk> \<Longrightarrow> z \<in> visited e
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
edge x y
reachable y z
\<lbrakk>y \<in> visited e; \<forall>n\<in>visited e. \<forall>m\<in>successors n - vsuccs e n. reachable y n \<longrightarrow> \<not> reachable m z\<rbrakk> \<Longrightarrow> z \<in> visited e
x \<in> visited e
\<forall>n\<in>visited e. \<forall>m\<in>successors n - vsuccs e n. reachable x n \<longrightarrow> \<not> reachable m z
[PROOF STEP]
have "y \<in> vsuccs e x"
[PROOF STATE]
proof (prove)
using this:
edge x y
reachable y z
\<lbrakk>y \<in> visited e; \<forall>n\<in>visited e. \<forall>m\<in>successors n - vsuccs e n. reachable y n \<longrightarrow> \<not> reachable m z\<rbrakk> \<Longrightarrow> z \<in> visited e
x \<in> visited e
\<forall>n\<in>visited e. \<forall>m\<in>successors n - vsuccs e n. reachable x n \<longrightarrow> \<not> reachable m z

goal (1 subgoal):
 1. y \<in> vsuccs e x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
y \<in> vsuccs e x

goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>edge x y; reachable y z; \<lbrakk>y \<in> visited e; \<forall>n\<in>visited e. \<forall>m\<in>successors n - vsuccs e n. reachable y n \<longrightarrow> \<not> reachable m z\<rbrakk> \<Longrightarrow> z \<in> visited e; x \<in> visited e; \<forall>n\<in>visited e. \<forall>m\<in>successors n - vsuccs e n. reachable x n \<longrightarrow> \<not> reachable m z\<rbrakk> \<Longrightarrow> z \<in> visited e
[PROOF STEP]
with e
[PROOF STATE]
proof (chain)
picking this:
wf_env e
y \<in> vsuccs e x
[PROOF STEP]
have "y \<in> visited e"
[PROOF STATE]
proof (prove)
using this:
wf_env e
y \<in> vsuccs e x

goal (1 subgoal):
 1. y \<in> visited e
[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
y \<in> vsuccs e x

goal (1 subgoal):
 1. y \<in> visited e
[PROOF STEP]
by (meson le_infE subset_eq)
[PROOF STATE]
proof (state)
this:
y \<in> visited e

goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>edge x y; reachable y z; \<lbrakk>y \<in> visited e; \<forall>n\<in>visited e. \<forall>m\<in>successors n - vsuccs e n. reachable y n \<longrightarrow> \<not> reachable m z\<rbrakk> \<Longrightarrow> z \<in> visited e; x \<in> visited e; \<forall>n\<in>visited e. \<forall>m\<in>successors n - vsuccs e n. reachable x n \<longrightarrow> \<not> reachable m z\<rbrakk> \<Longrightarrow> z \<in> visited e
[PROOF STEP]
with reachable_succ reachable.reachable_succ
[PROOF STATE]
proof (chain)
picking this:
edge x y
reachable y z
\<lbrakk>y \<in> visited e; \<forall>n\<in>visited e. \<forall>m\<in>successors n - vsuccs e n. reachable y n \<longrightarrow> \<not> reachable m z\<rbrakk> \<Longrightarrow> z \<in> visited e
x \<in> visited e
\<forall>n\<in>visited e. \<forall>m\<in>successors n - vsuccs e n. reachable x n \<longrightarrow> \<not> reachable m z
\<lbrakk>edge ?x ?y; reachable ?y ?z\<rbrakk> \<Longrightarrow> reachable ?x ?z
y \<in> visited e
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
edge x y
reachable y z
\<lbrakk>y \<in> visited e; \<forall>n\<in>visited e. \<forall>m\<in>successors n - vsuccs e n. reachable y n \<longrightarrow> \<not> reachable m z\<rbrakk> \<Longrightarrow> z \<in> visited e
x \<in> visited e
\<forall>n\<in>visited e. \<forall>m\<in>successors n - vsuccs e n. reachable x n \<longrightarrow> \<not> reachable m z
\<lbrakk>edge ?x ?y; reachable ?y ?z\<rbrakk> \<Longrightarrow> reachable ?x ?z
y \<in> visited e

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma avoiding_explored:
  assumes e: "wf_env e"
      and xy: "reachable_avoiding x y E"
      and y: "y \<notin> explored e"
      and w: "w \<in> explored e"
    shows "reachable_avoiding x y (E \<union> {(v,w)})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reachable_avoiding x y (E \<union> {(v, w)})
[PROOF STEP]
using xy y
[PROOF STATE]
proof (prove)
using this:
reachable_avoiding x y E
y \<notin> explored e

goal (1 subgoal):
 1. reachable_avoiding x y (E \<union> {(v, w)})
[PROOF STEP]
proof (induction)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x E. x \<notin> explored e \<Longrightarrow> reachable_avoiding x x (E \<union> {(v, w)})
 2. \<And>x y E z. \<lbrakk>reachable_avoiding x y E; y \<notin> explored e \<Longrightarrow> reachable_avoiding x y (E \<union> {(v, w)}); edge y z; (y, z) \<notin> E; z \<notin> explored e\<rbrakk> \<Longrightarrow> reachable_avoiding x z (E \<union> {(v, w)})
[PROOF STEP]
case (ra_refl x E)
[PROOF STATE]
proof (state)
this:
x \<notin> explored e

goal (2 subgoals):
 1. \<And>x E. x \<notin> explored e \<Longrightarrow> reachable_avoiding x x (E \<union> {(v, w)})
 2. \<And>x y E z. \<lbrakk>reachable_avoiding x y E; y \<notin> explored e \<Longrightarrow> reachable_avoiding x y (E \<union> {(v, w)}); edge y z; (y, z) \<notin> E; z \<notin> explored e\<rbrakk> \<Longrightarrow> reachable_avoiding x z (E \<union> {(v, w)})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<notin> explored e
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
x \<notin> explored e

goal (1 subgoal):
 1. reachable_avoiding x x (E \<union> {(v, w)})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
reachable_avoiding x x (E \<union> {(v, w)})

goal (1 subgoal):
 1. \<And>x y E z. \<lbrakk>reachable_avoiding x y E; y \<notin> explored e \<Longrightarrow> reachable_avoiding x y (E \<union> {(v, w)}); edge y z; (y, z) \<notin> E; z \<notin> explored e\<rbrakk> \<Longrightarrow> reachable_avoiding x z (E \<union> {(v, w)})
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y E z. \<lbrakk>reachable_avoiding x y E; y \<notin> explored e \<Longrightarrow> reachable_avoiding x y (E \<union> {(v, w)}); edge y z; (y, z) \<notin> E; z \<notin> explored e\<rbrakk> \<Longrightarrow> reachable_avoiding x z (E \<union> {(v, w)})
[PROOF STEP]
case (ra_succ x y E z)
[PROOF STATE]
proof (state)
this:
reachable_avoiding x y E
edge y z
(y, z) \<notin> E
y \<notin> explored e \<Longrightarrow> reachable_avoiding x y (E \<union> {(v, w)})
z \<notin> explored e

goal (1 subgoal):
 1. \<And>x y E z. \<lbrakk>reachable_avoiding x y E; y \<notin> explored e \<Longrightarrow> reachable_avoiding x y (E \<union> {(v, w)}); edge y z; (y, z) \<notin> E; z \<notin> explored e\<rbrakk> \<Longrightarrow> reachable_avoiding x z (E \<union> {(v, w)})
[PROOF STEP]
from e \<open>z \<in> successors y\<close> \<open>z \<notin> explored e\<close>
[PROOF STATE]
proof (chain)
picking this:
wf_env e
edge y z
z \<notin> explored e
[PROOF STEP]
have "y \<notin> explored e"
[PROOF STATE]
proof (prove)
using this:
wf_env e
edge y z
z \<notin> explored e

goal (1 subgoal):
 1. y \<notin> explored e
[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
edge y z
z \<notin> explored e

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

goal (1 subgoal):
 1. \<And>x y E z. \<lbrakk>reachable_avoiding x y E; y \<notin> explored e \<Longrightarrow> reachable_avoiding x y (E \<union> {(v, w)}); edge y z; (y, z) \<notin> E; z \<notin> explored e\<rbrakk> \<Longrightarrow> reachable_avoiding x z (E \<union> {(v, w)})
[PROOF STEP]
with ra_succ.IH
[PROOF STATE]
proof (chain)
picking this:
y \<notin> explored e \<Longrightarrow> reachable_avoiding x y (E \<union> {(v, w)})
y \<notin> explored e
[PROOF STEP]
have "reachable_avoiding x y (E \<union> {(v,w)})"
[PROOF STATE]
proof (prove)
using this:
y \<notin> explored e \<Longrightarrow> reachable_avoiding x y (E \<union> {(v, w)})
y \<notin> explored e

goal (1 subgoal):
 1. reachable_avoiding x y (E \<union> {(v, w)})
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
reachable_avoiding x y (E \<union> {(v, w)})

goal (1 subgoal):
 1. \<And>x y E z. \<lbrakk>reachable_avoiding x y E; y \<notin> explored e \<Longrightarrow> reachable_avoiding x y (E \<union> {(v, w)}); edge y z; (y, z) \<notin> E; z \<notin> explored e\<rbrakk> \<Longrightarrow> reachable_avoiding x z (E \<union> {(v, w)})
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
reachable_avoiding x y (E \<union> {(v, w)})

goal (1 subgoal):
 1. \<And>x y E z. \<lbrakk>reachable_avoiding x y E; y \<notin> explored e \<Longrightarrow> reachable_avoiding x y (E \<union> {(v, w)}); edge y z; (y, z) \<notin> E; z \<notin> explored e\<rbrakk> \<Longrightarrow> reachable_avoiding x z (E \<union> {(v, w)})
[PROOF STEP]
from w \<open>(y,z) \<notin> E\<close> \<open>z \<notin> explored e\<close>
[PROOF STATE]
proof (chain)
picking this:
w \<in> explored e
(y, z) \<notin> E
z \<notin> explored e
[PROOF STEP]
have "(y,z) \<notin> E \<union> {(v,w)}"
[PROOF STATE]
proof (prove)
using this:
w \<in> explored e
(y, z) \<notin> E
z \<notin> explored e

goal (1 subgoal):
 1. (y, z) \<notin> E \<union> {(v, w)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(y, z) \<notin> E \<union> {(v, w)}

goal (1 subgoal):
 1. \<And>x y E z. \<lbrakk>reachable_avoiding x y E; y \<notin> explored e \<Longrightarrow> reachable_avoiding x y (E \<union> {(v, w)}); edge y z; (y, z) \<notin> E; z \<notin> explored e\<rbrakk> \<Longrightarrow> reachable_avoiding x z (E \<union> {(v, w)})
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
reachable_avoiding x y (E \<union> {(v, w)})
(y, z) \<notin> E \<union> {(v, w)}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
reachable_avoiding x y (E \<union> {(v, w)})
(y, z) \<notin> E \<union> {(v, w)}

goal (1 subgoal):
 1. reachable_avoiding x z (E \<union> {(v, w)})
[PROOF STEP]
using  \<open>z \<in> successors y\<close>
[PROOF STATE]
proof (prove)
using this:
reachable_avoiding x y (E \<union> {(v, w)})
(y, z) \<notin> E \<union> {(v, w)}
edge y z

goal (1 subgoal):
 1. reachable_avoiding x z (E \<union> {(v, w)})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
reachable_avoiding x z (E \<union> {(v, w)})

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma init_env_pre_dfs: "pre_dfs v (init_env v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pre_dfs v (init_env v)
[PROOF STEP]
by (auto simp: pre_dfs_def wf_env_def init_env_def is_subscc_def
           dest: precedes_mem)


[STATEMENT]
lemma dfs_S_hd_stack:
  assumes wf: "wf_env e"
      and post: "post_dfs v e e'"
      and n: "stack e \<noteq> []" "n \<in> \<S> e (hd (stack e))"
    shows "stack e' \<noteq> []" "n \<in> \<S> e' (hd (stack e'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stack e' \<noteq> [] &&& n \<in> \<S> e' (hd (stack e'))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. stack e' \<noteq> []
 2. n \<in> \<S> e' (hd (stack e'))
[PROOF STEP]
have 1: "stack e' \<noteq> [] \<and> n \<in> \<S> e' (hd (stack e'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stack e' \<noteq> [] \<and> n \<in> \<S> e' (hd (stack e'))
[PROOF STEP]
proof (cases "stack e' = stack e \<and> (\<forall>n \<in> set (stack e'). \<S> e' n = \<S> e n)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. stack e' = stack e \<and> (\<forall>n\<in>set (stack e'). \<S> e' n = \<S> e n) \<Longrightarrow> stack e' \<noteq> [] \<and> n \<in> \<S> e' (hd (stack e'))
 2. \<not> (stack e' = stack e \<and> (\<forall>n\<in>set (stack e'). \<S> e' n = \<S> e n)) \<Longrightarrow> stack e' \<noteq> [] \<and> n \<in> \<S> e' (hd (stack e'))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
stack e' = stack e \<and> (\<forall>n\<in>set (stack e'). \<S> e' n = \<S> e n)

goal (2 subgoals):
 1. stack e' = stack e \<and> (\<forall>n\<in>set (stack e'). \<S> e' n = \<S> e n) \<Longrightarrow> stack e' \<noteq> [] \<and> n \<in> \<S> e' (hd (stack e'))
 2. \<not> (stack e' = stack e \<and> (\<forall>n\<in>set (stack e'). \<S> e' n = \<S> e n)) \<Longrightarrow> stack e' \<noteq> [] \<and> n \<in> \<S> e' (hd (stack e'))
[PROOF STEP]
with n
[PROOF STATE]
proof (chain)
picking this:
stack e \<noteq> []
n \<in> \<S> e (hd (stack e))
stack e' = stack e \<and> (\<forall>n\<in>set (stack e'). \<S> e' n = \<S> e n)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
stack e \<noteq> []
n \<in> \<S> e (hd (stack e))
stack e' = stack e \<and> (\<forall>n\<in>set (stack e'). \<S> e' n = \<S> e n)

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

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

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

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

goal (1 subgoal):
 1. \<not> (stack e' = stack e \<and> (\<forall>n\<in>set (stack e'). \<S> e' n = \<S> e n)) \<Longrightarrow> stack e' \<noteq> [] \<and> n \<in> \<S> e' (hd (stack e'))
[PROOF STEP]
from n
[PROOF STATE]
proof (chain)
picking this:
stack e \<noteq> []
n \<in> \<S> e (hd (stack e))
[PROOF STEP]
have "hd (stack e) \<in> set (stack e)"
[PROOF STATE]
proof (prove)
using this:
stack e \<noteq> []
n \<in> \<S> e (hd (stack e))

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

goal (1 subgoal):
 1. \<not> (stack e' = stack e \<and> (\<forall>n\<in>set (stack e'). \<S> e' n = \<S> e n)) \<Longrightarrow> stack e' \<noteq> [] \<and> n \<in> \<S> e' (hd (stack e'))
[PROOF STEP]
with 2 n post
[PROOF STATE]
proof (chain)
picking this:
\<not> (stack e' = stack e \<and> (\<forall>n\<in>set (stack e'). \<S> e' n = \<S> e n))
stack e \<noteq> []
n \<in> \<S> e (hd (stack e))
post_dfs v e e'
hd (stack e) \<in> set (stack e)
[PROOF STEP]
obtain u where
      u: "u \<in> set (stack e')" "n \<in> \<S> e' u"
[PROOF STATE]
proof (prove)
using this:
\<not> (stack e' = stack e \<and> (\<forall>n\<in>set (stack e'). \<S> e' n = \<S> e n))
stack e \<noteq> []
n \<in> \<S> e (hd (stack e))
post_dfs v e e'
hd (stack e) \<in> set (stack e)

goal (1 subgoal):
 1. (\<And>u. \<lbrakk>u \<in> set (stack e'); n \<in> \<S> e' u\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding post_dfs_def sub_env_def
[PROOF STATE]
proof (prove)
using this:
\<not> (stack e' = stack e \<and> (\<forall>n\<in>set (stack e'). \<S> e' n = \<S> e n))
stack e \<noteq> []
n \<in> \<S> e (hd (stack e))
wf_env e' \<and> v \<in> visited e' \<and> (root e' = root e \<and> visited e \<subseteq> visited e' \<and> explored e \<subseteq> explored e' \<and> (\<forall>v. vsuccs e v \<subseteq> vsuccs e' v) \<and> (\<forall>v. \<S> e v \<subseteq> \<S> e' v) \<and> \<Union> {\<S> e v |v. v \<in> set (stack e)} \<subseteq> \<Union> {\<S> e' v |v. v \<in> set (stack e')}) \<and> vsuccs e' v = successors v \<and> (\<forall>w\<in>visited e. vsuccs e' w = vsuccs e w) \<and> (\<forall>n\<in>set (stack e'). reachable n v) \<and> (\<exists>ns. stack e = ns @ stack e') \<and> (v \<in> explored e' \<and> stack e' = stack e \<and> (\<forall>n\<in>set (stack e'). \<S> e' n = \<S> e n) \<or> stack e' \<noteq> [] \<and> v \<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
hd (stack e) \<in> set (stack e)

goal (1 subgoal):
 1. (\<And>u. \<lbrakk>u \<in> set (stack e'); n \<in> \<S> e' u\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
u \<in> set (stack e')
n \<in> \<S> e' u

goal (1 subgoal):
 1. \<not> (stack e' = stack e \<and> (\<forall>n\<in>set (stack e'). \<S> e' n = \<S> e n)) \<Longrightarrow> stack e' \<noteq> [] \<and> n \<in> \<S> e' (hd (stack e'))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stack e' \<noteq> [] \<and> n \<in> \<S> e' (hd (stack e'))
[PROOF STEP]
proof (cases "u = hd (stack e')")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. u = hd (stack e') \<Longrightarrow> stack e' \<noteq> [] \<and> n \<in> \<S> e' (hd (stack e'))
 2. u \<noteq> hd (stack e') \<Longrightarrow> stack e' \<noteq> [] \<and> n \<in> \<S> e' (hd (stack e'))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
u = hd (stack e')

goal (2 subgoals):
 1. u = hd (stack e') \<Longrightarrow> stack e' \<noteq> [] \<and> n \<in> \<S> e' (hd (stack e'))
 2. u \<noteq> hd (stack e') \<Longrightarrow> stack e' \<noteq> [] \<and> n \<in> \<S> e' (hd (stack e'))
[PROOF STEP]
with u \<open>stack e' \<noteq> []\<close>
[PROOF STATE]
proof (chain)
picking this:
u \<in> set (stack e')
n \<in> \<S> e' u
stack e' \<noteq> []
u = hd (stack e')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
u \<in> set (stack e')
n \<in> \<S> e' u
stack e' \<noteq> []
u = hd (stack e')

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

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

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

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

goal (1 subgoal):
 1. u \<noteq> hd (stack e') \<Longrightarrow> stack e' \<noteq> [] \<and> n \<in> \<S> e' (hd (stack e'))
[PROOF STEP]
with u 2 post
[PROOF STATE]
proof (chain)
picking this:
u \<in> set (stack e')
n \<in> \<S> e' u
\<not> (stack e' = stack e \<and> (\<forall>n\<in>set (stack e'). \<S> e' n = \<S> e n))
post_dfs v e e'
u \<in> set (tl (stack e'))
[PROOF STEP]
have "u \<in> set (tl (stack e)) \<and> n \<in> \<S> e u"
[PROOF STATE]
proof (prove)
using this:
u \<in> set (stack e')
n \<in> \<S> e' u
\<not> (stack e' = stack e \<and> (\<forall>n\<in>set (stack e'). \<S> e' n = \<S> e n))
post_dfs v e e'
u \<in> set (tl (stack e'))

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

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

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

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

goal (1 subgoal):
 1. stack e' \<noteq> [] \<and> n \<in> \<S> e' (hd (stack e'))
[PROOF STEP]
by (metis (no_types, opaque_lifting) disjoint_iff_not_equal distinct.simps(2) list.collapse list.set_sel(2))
[PROOF STATE]
proof (state)
this:
stack e' \<noteq> [] \<and> n \<in> \<S> e' (hd (stack e'))

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

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

goal (2 subgoals):
 1. stack e' \<noteq> []
 2. n \<in> \<S> e' (hd (stack e'))
[PROOF STEP]
from 1
[PROOF STATE]
proof (chain)
picking this:
stack e' \<noteq> [] \<and> n \<in> \<S> e' (hd (stack e'))
[PROOF STEP]
show "stack e' \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
stack e' \<noteq> [] \<and> n \<in> \<S> e' (hd (stack e'))

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

goal (1 subgoal):
 1. n \<in> \<S> e' (hd (stack e'))
[PROOF STEP]
from 1
[PROOF STATE]
proof (chain)
picking this:
stack e' \<noteq> [] \<and> n \<in> \<S> e' (hd (stack e'))
[PROOF STEP]
show "n \<in> \<S> e' (hd (stack e'))"
[PROOF STATE]
proof (prove)
using this:
stack e' \<noteq> [] \<and> n \<in> \<S> e' (hd (stack e'))

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dfs_S_tl_stack:
  assumes post: "post_dfs v e e'"
    and nempty: "stack e \<noteq> []"
  shows "stack e' \<noteq> []" "\<forall>n \<in> set (tl (stack e')). \<S> e' n = \<S> e n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stack e' \<noteq> [] &&& \<forall>n\<in>set (tl (stack e')). \<S> e' n = \<S> e n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. stack e' \<noteq> []
 2. \<forall>n\<in>set (tl (stack e')). \<S> e' n = \<S> e n
[PROOF STEP]
have 1: "stack e' \<noteq> [] \<and> (\<forall>n \<in> set (tl (stack e')). \<S> e' n = \<S> e n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stack e' \<noteq> [] \<and> (\<forall>n\<in>set (tl (stack e')). \<S> e' n = \<S> e n)
[PROOF STEP]
proof (cases "stack e' = stack e \<and> (\<forall>n \<in> set (stack e'). \<S> e' n = \<S> e n)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. stack e' = stack e \<and> (\<forall>n\<in>set (stack e'). \<S> e' n = \<S> e n) \<Longrightarrow> stack e' \<noteq> [] \<and> (\<forall>n\<in>set (tl (stack e')). \<S> e' n = \<S> e n)
 2. \<not> (stack e' = stack e \<and> (\<forall>n\<in>set (stack e'). \<S> e' n = \<S> e n)) \<Longrightarrow> stack e' \<noteq> [] \<and> (\<forall>n\<in>set (tl (stack e')). \<S> e' n = \<S> e n)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
stack e' = stack e \<and> (\<forall>n\<in>set (stack e'). \<S> e' n = \<S> e n)

goal (2 subgoals):
 1. stack e' = stack e \<and> (\<forall>n\<in>set (stack e'). \<S> e' n = \<S> e n) \<Longrightarrow> stack e' \<noteq> [] \<and> (\<forall>n\<in>set (tl (stack e')). \<S> e' n = \<S> e n)
 2. \<not> (stack e' = stack e \<and> (\<forall>n\<in>set (stack e'). \<S> e' n = \<S> e n)) \<Longrightarrow> stack e' \<noteq> [] \<and> (\<forall>n\<in>set (tl (stack e')). \<S> e' n = \<S> e n)
[PROOF STEP]
with nempty
[PROOF STATE]
proof (chain)
picking this:
stack e \<noteq> []
stack e' = stack e \<and> (\<forall>n\<in>set (stack e'). \<S> e' n = \<S> e n)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
stack e \<noteq> []
stack e' = stack e \<and> (\<forall>n\<in>set (stack e'). \<S> e' n = \<S> e n)

goal (1 subgoal):
 1. stack e' \<noteq> [] \<and> (\<forall>n\<in>set (tl (stack e')). \<S> e' n = \<S> e n)
[PROOF STEP]
by (simp add: list.set_sel(2))
[PROOF STATE]
proof (state)
this:
stack e' \<noteq> [] \<and> (\<forall>n\<in>set (tl (stack e')). \<S> e' n = \<S> e n)

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

goal (1 subgoal):
 1. \<not> (stack e' = stack e \<and> (\<forall>n\<in>set (stack e'). \<S> e' n = \<S> e n)) \<Longrightarrow> stack e' \<noteq> [] \<and> (\<forall>n\<in>set (tl (stack e')). \<S> e' n = \<S> e n)
[PROOF STEP]
with post
[PROOF STATE]
proof (chain)
picking this:
post_dfs v e e'
\<not> (stack e' = stack e \<and> (\<forall>n\<in>set (stack e'). \<S> e' n = \<S> e n))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
post_dfs v e e'
\<not> (stack e' = stack e \<and> (\<forall>n\<in>set (stack e'). \<S> e' n = \<S> e n))

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

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

goal (2 subgoals):
 1. stack e' \<noteq> []
 2. \<forall>n\<in>set (tl (stack e')). \<S> e' n = \<S> e n
[PROOF STEP]
from 1
[PROOF STATE]
proof (chain)
picking this:
stack e' \<noteq> [] \<and> (\<forall>n\<in>set (tl (stack e')). \<S> e' n = \<S> e n)
[PROOF STEP]
show "stack e' \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
stack e' \<noteq> [] \<and> (\<forall>n\<in>set (tl (stack e')). \<S> e' n = \<S> e n)

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

goal (1 subgoal):
 1. \<forall>n\<in>set (tl (stack e')). \<S> e' n = \<S> e n
[PROOF STEP]
from 1
[PROOF STATE]
proof (chain)
picking this:
stack e' \<noteq> [] \<and> (\<forall>n\<in>set (tl (stack e')). \<S> e' n = \<S> e n)
[PROOF STEP]
show "\<forall>n \<in> set (tl (stack e')). \<S> e' n = \<S> e n"
[PROOF STATE]
proof (prove)
using this:
stack e' \<noteq> [] \<and> (\<forall>n\<in>set (tl (stack e')). \<S> e' n = \<S> e n)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma unite_stack:
  fixes e v w
  defines "e' \<equiv> unite v w e"
  assumes wf: "wf_env e"
      and w: "w \<in> successors v" "w \<notin> vsuccs e v" "w \<in> visited e" "w \<notin> explored e"
  obtains pfx where "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)"
                    "w \<in> \<S> e' (hd (stack e'))"
[PROOF STATE]
proof (prove)
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); w \<in> \<S> e' (hd (stack e'))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
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); w \<in> \<S> e' (hd (stack e'))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
define pfx where "pfx = takeWhile (\<lambda>x. w \<notin> \<S> e x) (stack e)"
[PROOF STATE]
proof (state)
this:
pfx = takeWhile (\<lambda>x. w \<notin> \<S> e x) (stack 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); w \<in> \<S> e' (hd (stack e'))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
define sfx where "sfx = dropWhile (\<lambda>x. w \<notin> \<S> e x) (stack e)"
[PROOF STATE]
proof (state)
this:
sfx = dropWhile (\<lambda>x. w \<notin> \<S> e x) (stack 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); w \<in> \<S> e' (hd (stack e'))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
define cc where "cc = \<Union> {\<S> e x |x. x \<in> set pfx \<union> {hd sfx}}"
[PROOF STATE]
proof (state)
this:
cc = \<Union> {\<S> e x |x. x \<in> set pfx \<union> {hd sfx}}

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); w \<in> \<S> e' (hd (stack e'))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "stack e = pfx @ sfx"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stack e = pfx @ sfx
[PROOF STEP]
by (simp add: pfx_def sfx_def)
[PROOF STATE]
proof (state)
this:
stack e = pfx @ sfx

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); w \<in> \<S> e' (hd (stack e'))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
stack e = pfx @ sfx

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); w \<in> \<S> e' (hd (stack e'))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "stack e' = sfx"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stack e' = sfx
[PROOF STEP]
by (simp add: e'_def unite_def sfx_def)
[PROOF STATE]
proof (state)
this:
stack e' = sfx

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); w \<in> \<S> e' (hd (stack e'))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
stack e' = sfx

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); w \<in> \<S> e' (hd (stack e'))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from wf w
[PROOF STATE]
proof (chain)
picking this:
wf_env e
edge v w
w \<notin> vsuccs e v
w \<in> visited e
w \<notin> explored e
[PROOF STEP]
have "w \<in> \<Union> {\<S> e n | n. n \<in> set (stack e)}"
[PROOF STATE]
proof (prove)
using this:
wf_env e
edge v w
w \<notin> vsuccs e v
w \<in> visited e
w \<notin> explored e

goal (1 subgoal):
 1. w \<in> \<Union> {\<S> e n |n. n \<in> set (stack e)}
[PROOF STEP]
by (simp add: wf_env_def)
[PROOF STATE]
proof (state)
this:
w \<in> \<Union> {\<S> e n |n. n \<in> set (stack 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); w \<in> \<S> e' (hd (stack e'))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
w \<in> \<Union> {\<S> e n |n. n \<in> set (stack e)}
[PROOF STEP]
obtain n where "n \<in> set (stack e)" "w \<in> \<S> e n"
[PROOF STATE]
proof (prove)
using this:
w \<in> \<Union> {\<S> e n |n. n \<in> set (stack e)}

goal (1 subgoal):
 1. (\<And>n. \<lbrakk>n \<in> set (stack e); w \<in> \<S> e n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n \<in> set (stack e)
w \<in> \<S> e n

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); w \<in> \<S> e' (hd (stack e'))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
hence sfx: "sfx \<noteq> [] \<and> w \<in> \<S> e (hd sfx)"
[PROOF STATE]
proof (prove)
using this:
n \<in> set (stack e)
w \<in> \<S> e n

goal (1 subgoal):
 1. sfx \<noteq> [] \<and> w \<in> \<S> e (hd sfx)
[PROOF STEP]
unfolding sfx_def
[PROOF STATE]
proof (prove)
using this:
n \<in> set (stack e)
w \<in> \<S> e n

goal (1 subgoal):
 1. dropWhile (\<lambda>x. w \<notin> \<S> e x) (stack e) \<noteq> [] \<and> w \<in> \<S> e (hd (dropWhile (\<lambda>x. w \<notin> \<S> e x) (stack e)))
[PROOF STEP]
by (metis dropWhile_eq_Nil_conv hd_dropWhile)
[PROOF STATE]
proof (state)
this:
sfx \<noteq> [] \<and> w \<in> \<S> e (hd sfx)

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); w \<in> \<S> e' (hd (stack e'))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sfx \<noteq> [] \<and> w \<in> \<S> e (hd sfx)

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); w \<in> \<S> e' (hd (stack e'))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "\<S> e' = (\<lambda>x. if x \<in> cc then cc else \<S> e x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<S> e' = (\<lambda>x. if x \<in> cc then cc else \<S> e x)
[PROOF STEP]
by (rule,
        auto simp add: e'_def unite_def pfx_def sfx_def cc_def)
[PROOF STATE]
proof (state)
this:
\<S> e' = (\<lambda>x. if x \<in> cc then cc else \<S> e x)

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); w \<in> \<S> e' (hd (stack e'))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<S> e' = (\<lambda>x. if x \<in> cc then cc else \<S> e x)

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); w \<in> \<S> e' (hd (stack e'))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from sfx
[PROOF STATE]
proof (chain)
picking this:
sfx \<noteq> [] \<and> w \<in> \<S> e (hd sfx)
[PROOF STEP]
have "w \<in> cc"
[PROOF STATE]
proof (prove)
using this:
sfx \<noteq> [] \<and> w \<in> \<S> e (hd sfx)

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

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); w \<in> \<S> e' (hd (stack e'))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from S_reflexive[OF wf, of "hd sfx"]
[PROOF STATE]
proof (chain)
picking this:
hd sfx \<in> \<S> e (hd sfx)
[PROOF STEP]
have "hd sfx \<in> cc"
[PROOF STATE]
proof (prove)
using this:
hd sfx \<in> \<S> e (hd sfx)

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

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); w \<in> \<S> e' (hd (stack e'))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with \<open>w \<in> cc\<close> \<open>\<S> e' = (\<lambda>x. if x \<in> cc then cc else \<S> e x)\<close>
[PROOF STATE]
proof (chain)
picking this:
w \<in> cc
\<S> e' = (\<lambda>x. if x \<in> cc then cc else \<S> e x)
hd sfx \<in> cc
[PROOF STEP]
have "w \<in> \<S> e' (hd sfx)"
[PROOF STATE]
proof (prove)
using this:
w \<in> cc
\<S> e' = (\<lambda>x. if x \<in> cc then cc else \<S> e x)
hd sfx \<in> cc

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

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); w \<in> \<S> e' (hd (stack e'))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
stack e = pfx @ sfx
stack e' = sfx
sfx \<noteq> [] \<and> w \<in> \<S> e (hd sfx)
\<S> e' = (\<lambda>x. if x \<in> cc then cc else \<S> e x)
w \<in> \<S> e' (hd sfx)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
stack e = pfx @ sfx
stack e' = sfx
sfx \<noteq> [] \<and> w \<in> \<S> e (hd sfx)
\<S> e' = (\<lambda>x. if x \<in> cc then cc else \<S> e x)
w \<in> \<S> e' (hd sfx)

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that e'_def unite_def pfx_def sfx_def cc_def
[PROOF STATE]
proof (prove)
using this:
stack e = pfx @ sfx
stack e' = sfx
sfx \<noteq> [] \<and> w \<in> \<S> e (hd sfx)
\<S> e' = (\<lambda>x. if x \<in> cc then cc else \<S> e x)
w \<in> \<S> e' (hd sfx)
\<lbrakk>stack e = ?pfx6 @ stack e'; stack e' \<noteq> []; let cc = \<Union> {\<S> e n |n. n \<in> set ?pfx6 \<union> {hd (stack e')}} in \<S> e' = (\<lambda>x. if x \<in> cc then cc else \<S> e x); w \<in> \<S> e' (hd (stack e'))\<rbrakk> \<Longrightarrow> thesis
e' \<equiv> unite v w e
unite ?v ?w ?e \<equiv> let pfx = takeWhile (\<lambda>x. ?w \<notin> \<S> ?e x) (stack ?e); sfx = dropWhile (\<lambda>x. ?w \<notin> \<S> ?e x) (stack ?e); cc = \<Union> {\<S> ?e x |x. x \<in> set pfx \<union> {hd sfx}} in ?e\<lparr>\<S> := \<lambda>x. if x \<in> cc then cc else \<S> ?e x, stack := sfx\<rparr>
pfx = takeWhile (\<lambda>x. w \<notin> \<S> e x) (stack e)
sfx = dropWhile (\<lambda>x. w \<notin> \<S> e x) (stack e)
cc = \<Union> {\<S> e x |x. x \<in> set pfx \<union> {hd sfx}}

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma unite_S_tl:
  fixes e v w
  defines "e' \<equiv> unite v w e"
  assumes wf: "wf_env e"
      and w: "w \<in> successors v" "w \<notin> vsuccs e v" "w \<in> visited e" "w \<notin> explored e"
      and n: "n \<in> set (tl (stack e'))"
  shows "\<S> e' n = \<S> e n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<S> e' n = \<S> e n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<S> e' n = \<S> e n
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
e' \<equiv> unite v w e
wf_env e
edge v w
w \<notin> vsuccs e v
w \<in> visited e
w \<notin> explored e
n \<in> set (tl (stack 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
wf_env e
edge v w
w \<notin> vsuccs e v
w \<in> visited e
w \<notin> explored e
n \<in> set (tl (stack 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)
[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. \<S> e' n = \<S> e n
[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. \<S> e' n = \<S> e 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 S_reflexive[OF wf, of n] n wf \<open>stack e = pfx @ stack e'\<close> \<open>stack e' \<noteq> []\<close>
[PROOF STATE]
proof (chain)
picking this:
n \<in> \<S> e n
n \<in> set (tl (stack e'))
wf_env e
stack e = pfx @ stack e'
stack e' \<noteq> []
m \<in> set pfx \<union> {hd (stack e')}
n \<in> \<S> e m
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
n \<in> \<S> e n
n \<in> set (tl (stack e'))
wf_env e
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. False
[PROOF STEP]
unfolding wf_env_def
[PROOF STATE]
proof (prove)
using this:
n \<in> \<S> e n
n \<in> set (tl (stack e'))
(\<forall>n\<in>visited e. reachable (root e) n) \<and> distinct (stack e) \<and> distinct (cstack e) \<and> (\<forall>n m. n \<preceq> m in stack e \<longrightarrow> n \<preceq> m in cstack e) \<and> (\<forall>n m. n \<preceq> m in stack e \<longrightarrow> reachable m n) \<and> explored e \<subseteq> visited e \<and> set (cstack e) \<subseteq> visited e \<and> (\<forall>n\<in>explored e. \<forall>m. reachable n m \<longrightarrow> m \<in> explored e) \<and> (\<forall>n. vsuccs e n \<subseteq> successors n \<inter> visited e) \<and> (\<forall>n. n \<notin> visited e \<longrightarrow> vsuccs e n = {}) \<and> (\<forall>n\<in>explored e. vsuccs e n = successors n) \<and> (\<forall>n\<in>visited e - set (cstack e). vsuccs e n = successors n) \<and> (\<forall>n m. (m \<in> \<S> e n) = (\<S> e n = \<S> e m)) \<and> (\<forall>n. n \<notin> visited e \<longrightarrow> \<S> e n = {n}) \<and> (\<forall>n\<in>set (stack e). \<forall>m\<in>set (stack e). n \<noteq> m \<longrightarrow> \<S> e n \<inter> \<S> e m = {}) \<and> \<Union> {\<S> e n |n. n \<in> set (stack e)} = visited e - explored e \<and> (\<forall>n\<in>set (stack e). \<forall>m\<in>\<S> e n. m \<in> set (cstack e) \<longrightarrow> m \<preceq> n in cstack e) \<and> (\<forall>n m. n \<preceq> m in stack e \<and> n \<noteq> m \<longrightarrow> (\<forall>u\<in>\<S> e n. \<not> reachable_avoiding u m (unvisited e n))) \<and> (\<forall>n. is_subscc (\<S> e n)) \<and> Ball (sccs e) is_scc \<and> \<Union> (sccs e) = explored e
stack e = pfx @ stack e'
stack e' \<noteq> []
m \<in> set pfx \<union> {hd (stack e')}
n \<in> \<S> e m

goal (1 subgoal):
 1. False
[PROOF STEP]
by (smt (z3) Diff_triv Un_iff Un_insert_right append.right_neutral disjoint_insert(1)
                   distinct.simps(2) distinct_append empty_set insertE insert_Diff list.exhaust_sel
                   list.simps(15) set_append)
[PROOF STATE]
proof (state)
this:
False

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

goal (1 subgoal):
 1. \<S> e' n = \<S> e n
[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)
n \<notin> cc
[PROOF STEP]
show "\<S> e' n = \<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 \<notin> cc

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma unite_S_equal:
  fixes e v w
  defines "e' \<equiv> unite v w e"
  assumes wf: "wf_env e"
      and w: "w \<in> successors v" "w \<notin> vsuccs e v" "w \<in> visited e" "w \<notin> explored e"
  shows "(\<Union> {\<S> e' n | n. n \<in> set (stack e')}) = (\<Union> {\<S> e n | n. n \<in> set (stack e)})"
[PROOF STATE]
proof (prove)
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]
proof -
[PROOF STATE]
proof (state)
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]
from assms
[PROOF STATE]
proof (chain)
picking this:
e' \<equiv> unite v w e
wf_env 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
wf_env 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)
[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. \<Union> {\<S> e' n |n. n \<in> set (stack e')} = \<Union> {\<S> e n |n. n \<in> set (stack 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. \<Union> {\<S> e' n |n. n \<in> set (stack e')} = \<Union> {\<S> e n |n. n \<in> set (stack 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: 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. \<Union> {\<S> e' n |n. n \<in> set (stack e')} = \<Union> {\<S> e n |n. n \<in> set (stack 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 S_hd: "\<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: Se' cc_def)
[PROOF STATE]
proof (state)
this:
\<S> e' (hd (stack e')) = cc

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]
from \<open>stack e' \<noteq> []\<close>
[PROOF STATE]
proof (chain)
picking this:
stack e' \<noteq> []
[PROOF STEP]
have ste': "set (stack e') = {hd (stack e')} \<union> set (tl (stack e'))"
[PROOF STATE]
proof (prove)
using this:
stack e' \<noteq> []

goal (1 subgoal):
 1. set (stack e') = {hd (stack e')} \<union> set (tl (stack e'))
[PROOF STEP]
by (metis insert_is_Un list.exhaust_sel list.simps(15))
[PROOF STATE]
proof (state)
this:
set (stack e') = {hd (stack e')} \<union> set (tl (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]
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 (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]
hence "\<Union> {\<S> e n | n. n \<in> set (stack e)}
        = cc \<union> (\<Union> {\<S> e n | n. n \<in> set (tl (stack e'))})"
[PROOF STATE]
proof (prove)
using this:
stack e = pfx @ hd (stack e') # tl (stack e')

goal (1 subgoal):
 1. \<Union> {\<S> e n |n. n \<in> set (stack e)} = cc \<union> \<Union> {\<S> e n |n. n \<in> set (tl (stack e'))}
[PROOF STEP]
by (auto simp add: cc_def)
[PROOF STATE]
proof (state)
this:
\<Union> {\<S> e n |n. n \<in> set (stack e)} = cc \<union> \<Union> {\<S> e n |n. n \<in> set (tl (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]
also
[PROOF STATE]
proof (state)
this:
\<Union> {\<S> e n |n. n \<in> set (stack e)} = cc \<union> \<Union> {\<S> e n |n. n \<in> set (tl (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]
from S_hd unite_S_tl[OF wf w]
[PROOF STATE]
proof (chain)
picking this:
\<S> e' (hd (stack e')) = cc
?n \<in> set (tl (stack (unite v w e))) \<Longrightarrow> \<S> (unite v w e) ?n = \<S> e ?n
[PROOF STEP]
have "\<dots> = \<S> e' (hd (stack e')) \<union> (\<Union> {\<S> e' n | n. n \<in> set (tl (stack e'))})"
[PROOF STATE]
proof (prove)
using this:
\<S> e' (hd (stack e')) = cc
?n \<in> set (tl (stack (unite v w e))) \<Longrightarrow> \<S> (unite v w e) ?n = \<S> e ?n

goal (1 subgoal):
 1. cc \<union> \<Union> {\<S> e n |n. n \<in> set (tl (stack e'))} = \<S> e' (hd (stack e')) \<union> \<Union> {\<S> e' n |n. n \<in> set (tl (stack e'))}
[PROOF STEP]
by (auto simp: e'_def)
[PROOF STATE]
proof (state)
this:
cc \<union> \<Union> {\<S> e n |n. n \<in> set (tl (stack e'))} = \<S> e' (hd (stack e')) \<union> \<Union> {\<S> e' n |n. n \<in> set (tl (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]
also
[PROOF STATE]
proof (state)
this:
cc \<union> \<Union> {\<S> e n |n. n \<in> set (tl (stack e'))} = \<S> e' (hd (stack e')) \<union> \<Union> {\<S> e' n |n. n \<in> set (tl (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]
from ste'
[PROOF STATE]
proof (chain)
picking this:
set (stack e') = {hd (stack e')} \<union> set (tl (stack e'))
[PROOF STEP]
have "\<dots> = \<Union> {\<S> e' n | n. n \<in> set (stack e')}"
[PROOF STATE]
proof (prove)
using this:
set (stack e') = {hd (stack e')} \<union> set (tl (stack e'))

goal (1 subgoal):
 1. \<S> e' (hd (stack e')) \<union> \<Union> {\<S> e' n |n. n \<in> set (tl (stack e'))} = \<Union> {\<S> e' n |n. n \<in> set (stack e')}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<S> e' (hd (stack e')) \<union> \<Union> {\<S> e' n |n. n \<in> set (tl (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')} = \<Union> {\<S> e n |n. n \<in> set (stack e)}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<Union> {\<S> e n |n. n \<in> set (stack e)} = \<Union> {\<S> e' n |n. n \<in> set (stack e')}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using 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. \<Union> {\<S> e' n |n. n \<in> set (stack e')} = \<Union> {\<S> e n |n. n \<in> set (stack e)}
[PROOF STEP]
by simp
[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:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma unite_subscc:
  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 "is_subscc (\<S> e' (hd (stack e')))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_subscc (\<S> e' (hd (stack e')))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_subscc (\<S> e' (hd (stack 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. is_subscc (\<S> e' (hd (stack 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. is_subscc (\<S> e' (hd (stack 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. is_subscc (\<S> e' (hd (stack e')))
[PROOF STEP]
from wf w
[PROOF STATE]
proof (chain)
picking this:
wf_env e
edge v w
w \<notin> vsuccs e v
w \<in> visited e
w \<notin> explored e
[PROOF STEP]
have "w \<in> \<Union> {\<S> e n | n. n \<in> set (stack e)}"
[PROOF STATE]
proof (prove)
using this:
wf_env e
edge v w
w \<notin> vsuccs e v
w \<in> visited e
w \<notin> explored e

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

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

goal (1 subgoal):
 1. w \<in> \<S> e (hd (stack e'))
[PROOF STEP]
apply (simp add: e'_def unite_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. (\<exists>n. x = \<S> e n \<and> n \<in> set (stack e)) \<and> w \<in> x \<Longrightarrow> w \<in> \<S> e (hd (dropWhile (\<lambda>x. w \<notin> \<S> e x) (stack e)))
[PROOF STEP]
by (metis dropWhile_eq_Nil_conv hd_dropWhile)
[PROOF STATE]
proof (state)
this:
w \<in> \<S> e (hd (stack e'))

goal (1 subgoal):
 1. is_subscc (\<S> e' (hd (stack e')))
[PROOF STEP]
have "is_subscc cc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_subscc cc
[PROOF STEP]
proof (clarsimp simp: is_subscc_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> cc; y \<in> cc\<rbrakk> \<Longrightarrow> reachable x y
[PROOF STEP]
fix x y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> cc; y \<in> cc\<rbrakk> \<Longrightarrow> reachable x y
[PROOF STEP]
assume "x \<in> cc" "y \<in> cc"
[PROOF STATE]
proof (state)
this:
x \<in> cc
y \<in> cc

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> cc; y \<in> cc\<rbrakk> \<Longrightarrow> reachable x y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> cc
y \<in> cc
[PROOF STEP]
obtain nx ny where
      nx: "nx \<in> set pfx \<union> {hd (stack e')}" "x \<in> \<S> e nx" and
      ny: "ny \<in> set pfx \<union> {hd (stack e')}" "y \<in> \<S> e ny"
[PROOF STATE]
proof (prove)
using this:
x \<in> cc
y \<in> cc

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

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> cc; y \<in> cc\<rbrakk> \<Longrightarrow> reachable x y
[PROOF STEP]
with wf
[PROOF STATE]
proof (chain)
picking this:
wf_env e
nx \<in> set pfx \<union> {hd (stack e')}
x \<in> \<S> e nx
ny \<in> set pfx \<union> {hd (stack e')}
y \<in> \<S> e ny
[PROOF STEP]
have "reachable x nx" "reachable ny y"
[PROOF STATE]
proof (prove)
using this:
wf_env e
nx \<in> set pfx \<union> {hd (stack e')}
x \<in> \<S> e nx
ny \<in> set pfx \<union> {hd (stack e')}
y \<in> \<S> e ny

goal (1 subgoal):
 1. reachable x nx &&& reachable ny y
[PROOF STEP]
by (auto simp: wf_env_def is_subscc_def)
[PROOF STATE]
proof (state)
this:
reachable x nx
reachable ny y

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> cc; y \<in> cc\<rbrakk> \<Longrightarrow> reachable x y
[PROOF STEP]
from w pre
[PROOF STATE]
proof (chain)
picking this:
edge v w
w \<notin> vsuccs e v
w \<in> visited e
w \<notin> explored e
pre_dfss v e
[PROOF STEP]
have "reachable v w"
[PROOF STATE]
proof (prove)
using this:
edge v w
w \<notin> vsuccs e v
w \<in> visited e
w \<notin> explored e
pre_dfss v e

goal (1 subgoal):
 1. reachable v w
[PROOF STEP]
by (auto simp: pre_dfss_def)
[PROOF STATE]
proof (state)
this:
reachable v w

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> cc; y \<in> cc\<rbrakk> \<Longrightarrow> reachable x y
[PROOF STEP]
from pre
[PROOF STATE]
proof (chain)
picking this:
pre_dfss v e
[PROOF STEP]
have "reachable (hd (stack e)) v"
[PROOF STATE]
proof (prove)
using this:
pre_dfss v e

goal (1 subgoal):
 1. reachable (hd (stack e)) v
[PROOF STEP]
by (auto simp: pre_dfss_def wf_env_def is_subscc_def)
[PROOF STATE]
proof (state)
this:
reachable (hd (stack e)) v

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> cc; y \<in> cc\<rbrakk> \<Longrightarrow> reachable x y
[PROOF STEP]
from pre
[PROOF STATE]
proof (chain)
picking this:
pre_dfss v e
[PROOF STEP]
have "stack e = hd (stack e) # tl (stack e)"
[PROOF STATE]
proof (prove)
using this:
pre_dfss v e

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

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> cc; y \<in> cc\<rbrakk> \<Longrightarrow> reachable x y
[PROOF STEP]
with nx \<open>stack e = pfx @ (stack e')\<close> \<open>stack e' \<noteq> []\<close>
[PROOF STATE]
proof (chain)
picking this:
nx \<in> set pfx \<union> {hd (stack e')}
x \<in> \<S> e nx
stack e = pfx @ stack e'
stack e' \<noteq> []
stack e = hd (stack e) # tl (stack e)
[PROOF STEP]
have "hd (stack e) \<preceq> nx in stack e"
[PROOF STATE]
proof (prove)
using this:
nx \<in> set pfx \<union> {hd (stack e')}
x \<in> \<S> e nx
stack e = pfx @ stack e'
stack e' \<noteq> []
stack e = hd (stack e) # tl (stack e)

goal (1 subgoal):
 1. hd (stack e) \<preceq> nx in stack e
[PROOF STEP]
by (metis Un_iff Un_insert_right head_precedes list.exhaust_sel list.simps(15)
                set_append sup_bot.right_neutral)
[PROOF STATE]
proof (state)
this:
hd (stack e) \<preceq> nx in stack e

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> cc; y \<in> cc\<rbrakk> \<Longrightarrow> reachable x y
[PROOF STEP]
with wf
[PROOF STATE]
proof (chain)
picking this:
wf_env e
hd (stack e) \<preceq> nx in stack e
[PROOF STEP]
have "reachable nx (hd (stack e))"
[PROOF STATE]
proof (prove)
using this:
wf_env e
hd (stack e) \<preceq> nx in stack e

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

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> cc; y \<in> cc\<rbrakk> \<Longrightarrow> reachable x y
[PROOF STEP]
from \<open>stack e = pfx @ (stack e')\<close> \<open>stack e' \<noteq> []\<close> ny
[PROOF STATE]
proof (chain)
picking this:
stack e = pfx @ stack e'
stack e' \<noteq> []
ny \<in> set pfx \<union> {hd (stack e')}
y \<in> \<S> e ny
[PROOF STEP]
have "ny \<preceq> hd (stack e') in stack e"
[PROOF STATE]
proof (prove)
using this:
stack e = pfx @ stack e'
stack e' \<noteq> []
ny \<in> set pfx \<union> {hd (stack e')}
y \<in> \<S> e ny

goal (1 subgoal):
 1. ny \<preceq> hd (stack e') in stack e
[PROOF STEP]
by (metis List.set_insert empty_set insert_Nil list.exhaust_sel set_append split_list_precedes)
[PROOF STATE]
proof (state)
this:
ny \<preceq> hd (stack e') in stack e

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> cc; y \<in> cc\<rbrakk> \<Longrightarrow> reachable x y
[PROOF STEP]
with wf
[PROOF STATE]
proof (chain)
picking this:
wf_env e
ny \<preceq> hd (stack e') in stack e
[PROOF STEP]
have "reachable (hd (stack e')) ny"
[PROOF STATE]
proof (prove)
using this:
wf_env e
ny \<preceq> hd (stack e') in stack e

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

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> cc; y \<in> cc\<rbrakk> \<Longrightarrow> reachable x y
[PROOF STEP]
from wf \<open>stack e' \<noteq> []\<close> \<open>w \<in> \<S> e (hd (stack e'))\<close>
[PROOF STATE]
proof (chain)
picking this:
wf_env e
stack e' \<noteq> []
w \<in> \<S> e (hd (stack e'))
[PROOF STEP]
have "reachable w (hd (stack e'))"
[PROOF STATE]
proof (prove)
using this:
wf_env e
stack e' \<noteq> []
w \<in> \<S> e (hd (stack e'))

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

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> cc; y \<in> cc\<rbrakk> \<Longrightarrow> reachable x y
[PROOF STEP]
from \<open>reachable x nx\<close> \<open>reachable nx (hd (stack e))\<close>
         \<open>reachable (hd (stack e)) v\<close> \<open>reachable v w\<close>
         \<open>reachable w (hd (stack e'))\<close>
         \<open>reachable (hd (stack e')) ny\<close> \<open>reachable ny y\<close>
[PROOF STATE]
proof (chain)
picking this:
reachable x nx
reachable nx (hd (stack e))
reachable (hd (stack e)) v
reachable v w
reachable w (hd (stack e'))
reachable (hd (stack e')) ny
reachable ny y
[PROOF STEP]
show "reachable x y"
[PROOF STATE]
proof (prove)
using this:
reachable x nx
reachable nx (hd (stack e))
reachable (hd (stack e)) v
reachable v w
reachable w (hd (stack e'))
reachable (hd (stack e')) ny
reachable ny y

goal (1 subgoal):
 1. reachable x y
[PROOF STEP]
using reachable_trans
[PROOF STATE]
proof (prove)
using this:
reachable x nx
reachable nx (hd (stack e))
reachable (hd (stack e)) v
reachable v w
reachable w (hd (stack e'))
reachable (hd (stack e')) ny
reachable ny y
\<lbrakk>reachable ?x ?y; reachable ?y ?z\<rbrakk> \<Longrightarrow> reachable ?x ?z

goal (1 subgoal):
 1. reachable x y
[PROOF STEP]
by meson
[PROOF STATE]
proof (state)
this:
reachable x y

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

goal (1 subgoal):
 1. is_subscc (\<S> e' (hd (stack e')))
[PROOF STEP]
with S_reflexive[OF wf, of "hd (stack e')"] pfx
[PROOF STATE]
proof (chain)
picking this:
hd (stack e') \<in> \<S> e (hd (stack e'))
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)
is_subscc cc
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
hd (stack e') \<in> \<S> e (hd (stack e'))
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)
is_subscc cc

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma unite_sub_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 "sub_env e e'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sub_env e e'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sub_env e 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. sub_env e 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. sub_env e 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. sub_env e e'
[PROOF STEP]
have "\<forall>n. \<S> e n \<subseteq> \<S> e' n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. \<S> e n \<subseteq> \<S> e' n
[PROOF STEP]
proof (clarify)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n x. x \<in> \<S> e n \<Longrightarrow> x \<in> \<S> e' n
[PROOF STEP]
fix n u
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n x. x \<in> \<S> e n \<Longrightarrow> x \<in> \<S> e' n
[PROOF STEP]
assume u: "u \<in> \<S> e n"
[PROOF STATE]
proof (state)
this:
u \<in> \<S> e n

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

goal (2 subgoals):
 1. n \<in> cc \<Longrightarrow> u \<in> \<S> e' n
 2. n \<notin> cc \<Longrightarrow> u \<in> \<S> e' n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n \<in> cc
[PROOF STEP]
obtain m where
        m: "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 (2 subgoals):
 1. n \<in> cc \<Longrightarrow> u \<in> \<S> e' n
 2. n \<notin> cc \<Longrightarrow> u \<in> \<S> e' n
[PROOF STEP]
with wf S_reflexive[OF wf, of n] u
[PROOF STATE]
proof (chain)
picking this:
wf_env e
n \<in> \<S> e n
u \<in> \<S> e n
m \<in> set pfx \<union> {hd (stack e')}
n \<in> \<S> e m
[PROOF STEP]
have "u \<in> \<S> e m"
[PROOF STATE]
proof (prove)
using this:
wf_env e
n \<in> \<S> e n
u \<in> \<S> e n
m \<in> set pfx \<union> {hd (stack e')}
n \<in> \<S> e m

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

goal (2 subgoals):
 1. n \<in> cc \<Longrightarrow> u \<in> \<S> e' n
 2. n \<notin> cc \<Longrightarrow> u \<in> \<S> e' n
[PROOF STEP]
with m pfx
[PROOF STATE]
proof (chain)
picking this:
m \<in> set pfx \<union> {hd (stack e')}
n \<in> \<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)
u \<in> \<S> e m
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
m \<in> set pfx \<union> {hd (stack e')}
n \<in> \<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)
u \<in> \<S> e m

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

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

goal (1 subgoal):
 1. n \<notin> cc \<Longrightarrow> u \<in> \<S> e' n
[PROOF STEP]
with pfx u
[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)
u \<in> \<S> e n
n \<notin> cc
[PROOF STEP]
show ?thesis
[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)
u \<in> \<S> e n
n \<notin> cc

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

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

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

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

goal (1 subgoal):
 1. sub_env e e'
[PROOF STEP]
have "root e' = root e \<and> visited e' = visited e
      \<and> explored e' = explored e \<and> vsuccs e' = vsuccs e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. root e' = root e \<and> visited e' = visited e \<and> explored e' = explored e \<and> vsuccs e' = vsuccs e
[PROOF STEP]
by (simp add: e'_def unite_def)
[PROOF STATE]
proof (state)
this:
root e' = root e \<and> visited e' = visited e \<and> explored e' = explored e \<and> vsuccs e' = vsuccs e

goal (1 subgoal):
 1. sub_env e e'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>n. \<S> e n \<subseteq> \<S> e' n
root e' = root e \<and> visited e' = visited e \<and> explored e' = explored e \<and> vsuccs e' = vsuccs e
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>n. \<S> e n \<subseteq> \<S> e' n
root e' = root e \<and> visited e' = visited e \<and> explored e' = explored e \<and> vsuccs e' = vsuccs e

goal (1 subgoal):
 1. sub_env e e'
[PROOF STEP]
using unite_S_equal[OF wf w]
[PROOF STATE]
proof (prove)
using this:
\<forall>n. \<S> e n \<subseteq> \<S> e' n
root e' = root e \<and> visited e' = visited e \<and> explored e' = explored e \<and> vsuccs e' = vsuccs e
\<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. sub_env e e'
[PROOF STEP]
by (simp add: e'_def sub_env_def)
[PROOF STATE]
proof (state)
this:
sub_env e e'

goal:
No subgoals!
[PROOF STEP]
qed