[STATEMENT]
theorem partial_correctness:
  fixes v
  defines "e \<equiv> dfs v (init_env v)"
  assumes "dfs_dfss_dom (Inl (v, init_env v))"
  shows "sccs e = {S . is_scc S \<and> (\<forall>n\<in>S. reachable v n)}"
    (is "_ = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sccs e = {S. is_scc S \<and> (\<forall>n\<in>S. reachable v n)}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sccs e = {S. is_scc S \<and> (\<forall>n\<in>S. reachable v n)}
[PROOF STEP]
from assms init_env_pre_dfs[of v]
[PROOF STATE]
proof (chain)
picking this:
e \<equiv> dfs v (init_env v)
dfs_dfss_dom (Inl (v, init_env v))
pre_dfs v (init_env v)
[PROOF STEP]
have post: "post_dfs v (init_env v) e"
[PROOF STATE]
proof (prove)
using this:
e \<equiv> dfs v (init_env v)
dfs_dfss_dom (Inl (v, init_env v))
pre_dfs v (init_env v)

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

goal (1 subgoal):
 1. sccs e = {S. is_scc S \<and> (\<forall>n\<in>S. reachable v n)}
[PROOF STEP]
hence wf: "wf_env e"
[PROOF STATE]
proof (prove)
using this:
post_dfs v (init_env v) e

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

goal (1 subgoal):
 1. sccs e = {S. is_scc S \<and> (\<forall>n\<in>S. reachable v n)}
[PROOF STEP]
from post
[PROOF STATE]
proof (chain)
picking this:
post_dfs v (init_env v) e
[PROOF STEP]
have "cstack e = []"
[PROOF STATE]
proof (prove)
using this:
post_dfs v (init_env v) e

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

goal (1 subgoal):
 1. sccs e = {S. is_scc S \<and> (\<forall>n\<in>S. reachable v n)}
[PROOF STEP]
have "stack e = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stack e = []
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. stack e \<noteq> [] \<Longrightarrow> False
[PROOF STEP]
assume "stack e \<noteq> []"
[PROOF STATE]
proof (state)
this:
stack e \<noteq> []

goal (1 subgoal):
 1. stack e \<noteq> [] \<Longrightarrow> False
[PROOF STEP]
hence "hd (stack e) \<preceq> hd (stack e) in stack e"
[PROOF STATE]
proof (prove)
using this:
stack e \<noteq> []

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

goal (1 subgoal):
 1. stack e \<noteq> [] \<Longrightarrow> False
[PROOF STEP]
with wf \<open>cstack e = []\<close>
[PROOF STATE]
proof (chain)
picking this:
wf_env e
cstack e = []
hd (stack e) \<preceq> hd (stack e) in stack e
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
wf_env e
cstack e = []
hd (stack e) \<preceq> hd (stack e) in stack e

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

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

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

goal (1 subgoal):
 1. sccs e = {S. is_scc S \<and> (\<forall>n\<in>S. reachable v n)}
[PROOF STEP]
with post
[PROOF STATE]
proof (chain)
picking this:
post_dfs v (init_env v) e
stack e = []
[PROOF STEP]
have vexp: "v \<in> explored e"
[PROOF STATE]
proof (prove)
using this:
post_dfs v (init_env v) e
stack e = []

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

goal (1 subgoal):
 1. sccs e = {S. is_scc S \<and> (\<forall>n\<in>S. reachable v n)}
[PROOF STEP]
from wf \<open>stack e = []\<close>
[PROOF STATE]
proof (chain)
picking this:
wf_env e
stack e = []
[PROOF STEP]
have "explored e = visited e"
[PROOF STATE]
proof (prove)
using this:
wf_env e
stack e = []

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

goal (1 subgoal):
 1. sccs e = {S. is_scc S \<and> (\<forall>n\<in>S. reachable v n)}
[PROOF STEP]
have "sccs e \<subseteq> ?rhs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sccs e \<subseteq> {S. is_scc S \<and> (\<forall>n\<in>S. reachable v n)}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> sccs e \<Longrightarrow> x \<in> {S. is_scc S \<and> (\<forall>n\<in>S. reachable v n)}
[PROOF STEP]
fix S
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> sccs e \<Longrightarrow> x \<in> {S. is_scc S \<and> (\<forall>n\<in>S. reachable v n)}
[PROOF STEP]
assume S: "S \<in> sccs e"
[PROOF STATE]
proof (state)
this:
S \<in> sccs e

goal (1 subgoal):
 1. \<And>x. x \<in> sccs e \<Longrightarrow> x \<in> {S. is_scc S \<and> (\<forall>n\<in>S. reachable v n)}
[PROOF STEP]
with wf
[PROOF STATE]
proof (chain)
picking this:
wf_env e
S \<in> sccs e
[PROOF STEP]
have "is_scc S"
[PROOF STATE]
proof (prove)
using this:
wf_env e
S \<in> sccs e

goal (1 subgoal):
 1. is_scc S
[PROOF STEP]
by (simp add: wf_env_def)
[PROOF STATE]
proof (state)
this:
is_scc S

goal (1 subgoal):
 1. \<And>x. x \<in> sccs e \<Longrightarrow> x \<in> {S. is_scc S \<and> (\<forall>n\<in>S. reachable v n)}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
is_scc S

goal (1 subgoal):
 1. \<And>x. x \<in> sccs e \<Longrightarrow> x \<in> {S. is_scc S \<and> (\<forall>n\<in>S. reachable v n)}
[PROOF STEP]
from S wf
[PROOF STATE]
proof (chain)
picking this:
S \<in> sccs e
wf_env e
[PROOF STEP]
have "S \<subseteq> explored e"
[PROOF STATE]
proof (prove)
using this:
S \<in> sccs e
wf_env e

goal (1 subgoal):
 1. S \<subseteq> explored e
[PROOF STEP]
unfolding wf_env_def
[PROOF STATE]
proof (prove)
using this:
S \<in> sccs 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. S \<subseteq> explored e
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
S \<subseteq> explored e

goal (1 subgoal):
 1. \<And>x. x \<in> sccs e \<Longrightarrow> x \<in> {S. is_scc S \<and> (\<forall>n\<in>S. reachable v n)}
[PROOF STEP]
with post \<open>explored e = visited e\<close>
[PROOF STATE]
proof (chain)
picking this:
post_dfs v (init_env v) e
explored e = visited e
S \<subseteq> explored e
[PROOF STEP]
have "\<forall>n\<in>S. reachable v n"
[PROOF STATE]
proof (prove)
using this:
post_dfs v (init_env v) e
explored e = visited e
S \<subseteq> explored e

goal (1 subgoal):
 1. \<forall>n\<in>S. reachable v n
[PROOF STEP]
by (auto simp: post_dfs_def wf_env_def sub_env_def init_env_def)
[PROOF STATE]
proof (state)
this:
\<forall>n\<in>S. reachable v n

goal (1 subgoal):
 1. \<And>x. x \<in> sccs e \<Longrightarrow> x \<in> {S. is_scc S \<and> (\<forall>n\<in>S. reachable v n)}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
is_scc S
\<forall>n\<in>S. reachable v n
[PROOF STEP]
show "S \<in> ?rhs"
[PROOF STATE]
proof (prove)
using this:
is_scc S
\<forall>n\<in>S. reachable v n

goal (1 subgoal):
 1. S \<in> {S. is_scc S \<and> (\<forall>n\<in>S. reachable v n)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
S \<in> {S. is_scc S \<and> (\<forall>n\<in>S. reachable v n)}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sccs e \<subseteq> {S. is_scc S \<and> (\<forall>n\<in>S. reachable v n)}

goal (1 subgoal):
 1. sccs e = {S. is_scc S \<and> (\<forall>n\<in>S. reachable v n)}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sccs e \<subseteq> {S. is_scc S \<and> (\<forall>n\<in>S. reachable v n)}

goal (1 subgoal):
 1. sccs e = {S. is_scc S \<and> (\<forall>n\<in>S. reachable v n)}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
sccs e \<subseteq> {S. is_scc S \<and> (\<forall>n\<in>S. reachable v n)}

goal (1 subgoal):
 1. sccs e = {S. is_scc S \<and> (\<forall>n\<in>S. reachable v n)}
[PROOF STEP]
fix S
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sccs e = {S. is_scc S \<and> (\<forall>n\<in>S. reachable v n)}
[PROOF STEP]
assume "is_scc S" "\<forall>n\<in>S. reachable v n"
[PROOF STATE]
proof (state)
this:
is_scc S
\<forall>n\<in>S. reachable v n

goal (1 subgoal):
 1. sccs e = {S. is_scc S \<and> (\<forall>n\<in>S. reachable v n)}
[PROOF STEP]
from \<open>\<forall>n\<in>S. reachable v n\<close> vexp wf
[PROOF STATE]
proof (chain)
picking this:
\<forall>n\<in>S. reachable v n
v \<in> explored e
wf_env e
[PROOF STEP]
have "S \<subseteq> \<Union> (sccs e)"
[PROOF STATE]
proof (prove)
using this:
\<forall>n\<in>S. reachable v n
v \<in> explored e
wf_env e

goal (1 subgoal):
 1. S \<subseteq> \<Union> (sccs e)
[PROOF STEP]
unfolding wf_env_def
[PROOF STATE]
proof (prove)
using this:
\<forall>n\<in>S. reachable v n
v \<in> explored 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. S \<subseteq> \<Union> (sccs e)
[PROOF STEP]
by (metis subset_eq)
[PROOF STATE]
proof (state)
this:
S \<subseteq> \<Union> (sccs e)

goal (1 subgoal):
 1. sccs e = {S. is_scc S \<and> (\<forall>n\<in>S. reachable v n)}
[PROOF STEP]
with \<open>is_scc S\<close>
[PROOF STATE]
proof (chain)
picking this:
is_scc S
S \<subseteq> \<Union> (sccs e)
[PROOF STEP]
obtain S' where S': "S' \<in> sccs e \<and> S \<inter> S' \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
is_scc S
S \<subseteq> \<Union> (sccs e)

goal (1 subgoal):
 1. (\<And>S'. S' \<in> sccs e \<and> S \<inter> S' \<noteq> {} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding is_scc_def
[PROOF STATE]
proof (prove)
using this:
S \<noteq> {} \<and> is_subscc S \<and> (\<forall>S'. S \<subseteq> S' \<and> is_subscc S' \<longrightarrow> S' = S)
S \<subseteq> \<Union> (sccs e)

goal (1 subgoal):
 1. (\<And>S'. S' \<in> sccs e \<and> S \<inter> S' \<noteq> {} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis Union_disjoint inf.absorb_iff2 inf_commute)
[PROOF STATE]
proof (state)
this:
S' \<in> sccs e \<and> S \<inter> S' \<noteq> {}

goal (1 subgoal):
 1. sccs e = {S. is_scc S \<and> (\<forall>n\<in>S. reachable v n)}
[PROOF STEP]
with wf
[PROOF STATE]
proof (chain)
picking this:
wf_env e
S' \<in> sccs e \<and> S \<inter> S' \<noteq> {}
[PROOF STEP]
have "is_scc S'"
[PROOF STATE]
proof (prove)
using this:
wf_env e
S' \<in> sccs e \<and> S \<inter> S' \<noteq> {}

goal (1 subgoal):
 1. is_scc S'
[PROOF STEP]
by (simp add: wf_env_def)
[PROOF STATE]
proof (state)
this:
is_scc S'

goal (1 subgoal):
 1. sccs e = {S. is_scc S \<and> (\<forall>n\<in>S. reachable v n)}
[PROOF STEP]
with S' \<open>is_scc S\<close>
[PROOF STATE]
proof (chain)
picking this:
S' \<in> sccs e \<and> S \<inter> S' \<noteq> {}
is_scc S
is_scc S'
[PROOF STEP]
have "S \<in> sccs e"
[PROOF STATE]
proof (prove)
using this:
S' \<in> sccs e \<and> S \<inter> S' \<noteq> {}
is_scc S
is_scc S'

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

goal (1 subgoal):
 1. sccs e = {S. is_scc S \<and> (\<forall>n\<in>S. reachable v n)}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>is_scc ?S8; \<forall>n\<in>?S8. reachable v n\<rbrakk> \<Longrightarrow> ?S8 \<in> sccs e

goal (1 subgoal):
 1. sccs e = {S. is_scc S \<and> (\<forall>n\<in>S. reachable v n)}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
sccs e \<subseteq> {S. is_scc S \<and> (\<forall>n\<in>S. reachable v n)}
\<lbrakk>is_scc ?S8; \<forall>n\<in>?S8. reachable v n\<rbrakk> \<Longrightarrow> ?S8 \<in> sccs e
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sccs e \<subseteq> {S. is_scc S \<and> (\<forall>n\<in>S. reachable v n)}
\<lbrakk>is_scc ?S8; \<forall>n\<in>?S8. reachable v n\<rbrakk> \<Longrightarrow> ?S8 \<in> sccs e

goal (1 subgoal):
 1. sccs e = {S. is_scc S \<and> (\<forall>n\<in>S. reachable v n)}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
sccs e = {S. is_scc S \<and> (\<forall>n\<in>S. reachable v n)}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wf_term: "wf dfs_dfss_term"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf dfs_dfss_term
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wf dfs_dfss_term
[PROOF STEP]
let ?r = "(finite_psubset :: ('v set \<times> 'v set) set)
            <*lex*> (finite_psubset :: ((('v \<times> 'v) set) \<times> ('v \<times> 'v) set) set)
            <*lex*> pred_nat"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wf dfs_dfss_term
[PROOF STEP]
have "wf (finite_psubset :: ('v set \<times> 'v set) set)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf finite_psubset
[PROOF STEP]
by (rule wf_finite_psubset)
[PROOF STATE]
proof (state)
this:
wf finite_psubset

goal (1 subgoal):
 1. wf dfs_dfss_term
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
wf finite_psubset

goal (1 subgoal):
 1. wf dfs_dfss_term
[PROOF STEP]
have "wf (finite_psubset :: ((('v \<times> 'v) set) \<times> ('v \<times> 'v) set) set)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf finite_psubset
[PROOF STEP]
by (rule wf_finite_psubset)
[PROOF STATE]
proof (state)
this:
wf finite_psubset

goal (1 subgoal):
 1. wf dfs_dfss_term
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
wf finite_psubset
wf finite_psubset
[PROOF STEP]
have "wf ?r"
[PROOF STATE]
proof (prove)
using this:
wf finite_psubset
wf finite_psubset

goal (1 subgoal):
 1. wf (finite_psubset <*lex*> finite_psubset <*lex*> pred_nat)
[PROOF STEP]
using wf_pred_nat
[PROOF STATE]
proof (prove)
using this:
wf finite_psubset
wf finite_psubset
wf pred_nat

goal (1 subgoal):
 1. wf (finite_psubset <*lex*> finite_psubset <*lex*> pred_nat)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
wf (finite_psubset <*lex*> finite_psubset <*lex*> pred_nat)

goal (1 subgoal):
 1. wf dfs_dfss_term
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
wf (finite_psubset <*lex*> finite_psubset <*lex*> pred_nat)

goal (1 subgoal):
 1. wf dfs_dfss_term
[PROOF STEP]
have "dfs_dfss_term \<subseteq> inv_image ?r dfs_dfss_to_tuple"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dfs_dfss_term \<subseteq> inv_image (finite_psubset <*lex*> finite_psubset <*lex*> pred_nat) dfs_dfss_to_tuple
[PROOF STEP]
proof (clarify)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> dfs_dfss_term \<Longrightarrow> (a, b) \<in> inv_image (finite_psubset <*lex*> finite_psubset <*lex*> pred_nat) dfs_dfss_to_tuple
[PROOF STEP]
fix a b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> dfs_dfss_term \<Longrightarrow> (a, b) \<in> inv_image (finite_psubset <*lex*> finite_psubset <*lex*> pred_nat) dfs_dfss_to_tuple
[PROOF STEP]
assume "(a,b) \<in> dfs_dfss_term"
[PROOF STATE]
proof (state)
this:
(a, b) \<in> dfs_dfss_term

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> dfs_dfss_term \<Longrightarrow> (a, b) \<in> inv_image (finite_psubset <*lex*> finite_psubset <*lex*> pred_nat) dfs_dfss_to_tuple
[PROOF STEP]
hence "(\<exists>v w e e''. a = Inr(v,e'') \<and> b = Inr(v,e) \<and> v \<in> vertices \<and> sub_env e e''
                      \<and> w \<in> vertices \<and> w \<notin> vsuccs e v \<and> w \<in> vsuccs e'' v)
         \<or> (\<exists>v e e1. a = Inr(v,e1) \<and> b = Inl(v,e) \<and> v \<in> vertices - visited e
                   \<and> visited e1 = visited e \<union> {v})
         \<or> (\<exists>v w e. a = Inl(w,e) \<and> b = Inr(v,e))"
         (is "?c1 \<or> ?c2 \<or> ?c3")
[PROOF STATE]
proof (prove)
using this:
(a, b) \<in> dfs_dfss_term

goal (1 subgoal):
 1. (\<exists>v w e e''. a = Inr (v, e'') \<and> b = Inr (v, e) \<and> v \<in> vertices \<and> sub_env e e'' \<and> w \<in> vertices \<and> w \<notin> vsuccs e v \<and> w \<in> vsuccs e'' v) \<or> (\<exists>v e e1. a = Inr (v, e1) \<and> b = Inl (v, e) \<and> v \<in> vertices - visited e \<and> visited e1 = visited e \<union> {v}) \<or> (\<exists>v w e. a = Inl (w, e) \<and> b = Inr (v, e))
[PROOF STEP]
by (auto simp: dfs_dfss_term_def)
[PROOF STATE]
proof (state)
this:
(\<exists>v w e e''. a = Inr (v, e'') \<and> b = Inr (v, e) \<and> v \<in> vertices \<and> sub_env e e'' \<and> w \<in> vertices \<and> w \<notin> vsuccs e v \<and> w \<in> vsuccs e'' v) \<or> (\<exists>v e e1. a = Inr (v, e1) \<and> b = Inl (v, e) \<and> v \<in> vertices - visited e \<and> visited e1 = visited e \<union> {v}) \<or> (\<exists>v w e. a = Inl (w, e) \<and> b = Inr (v, e))

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> dfs_dfss_term \<Longrightarrow> (a, b) \<in> inv_image (finite_psubset <*lex*> finite_psubset <*lex*> pred_nat) dfs_dfss_to_tuple
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<exists>v w e e''. a = Inr (v, e'') \<and> b = Inr (v, e) \<and> v \<in> vertices \<and> sub_env e e'' \<and> w \<in> vertices \<and> w \<notin> vsuccs e v \<and> w \<in> vsuccs e'' v) \<or> (\<exists>v e e1. a = Inr (v, e1) \<and> b = Inl (v, e) \<and> v \<in> vertices - visited e \<and> visited e1 = visited e \<union> {v}) \<or> (\<exists>v w e. a = Inl (w, e) \<and> b = Inr (v, e))
[PROOF STEP]
show "(a,b) \<in> inv_image ?r dfs_dfss_to_tuple"
[PROOF STATE]
proof (prove)
using this:
(\<exists>v w e e''. a = Inr (v, e'') \<and> b = Inr (v, e) \<and> v \<in> vertices \<and> sub_env e e'' \<and> w \<in> vertices \<and> w \<notin> vsuccs e v \<and> w \<in> vsuccs e'' v) \<or> (\<exists>v e e1. a = Inr (v, e1) \<and> b = Inl (v, e) \<and> v \<in> vertices - visited e \<and> visited e1 = visited e \<union> {v}) \<or> (\<exists>v w e. a = Inl (w, e) \<and> b = Inr (v, e))

goal (1 subgoal):
 1. (a, b) \<in> inv_image (finite_psubset <*lex*> finite_psubset <*lex*> pred_nat) dfs_dfss_to_tuple
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>v w e e''. a = Inr (v, e'') \<and> b = Inr (v, e) \<and> v \<in> vertices \<and> sub_env e e'' \<and> w \<in> vertices \<and> w \<notin> vsuccs e v \<and> w \<in> vsuccs e'' v \<Longrightarrow> (a, b) \<in> inv_image (finite_psubset <*lex*> finite_psubset <*lex*> pred_nat) dfs_dfss_to_tuple
 2. (\<exists>v e e1. a = Inr (v, e1) \<and> b = Inl (v, e) \<and> v \<in> vertices - visited e \<and> visited e1 = visited e \<union> {v}) \<or> (\<exists>v w e. a = Inl (w, e) \<and> b = Inr (v, e)) \<Longrightarrow> (a, b) \<in> inv_image (finite_psubset <*lex*> finite_psubset <*lex*> pred_nat) dfs_dfss_to_tuple
[PROOF STEP]
assume "?c1"
[PROOF STATE]
proof (state)
this:
\<exists>v w e e''. a = Inr (v, e'') \<and> b = Inr (v, e) \<and> v \<in> vertices \<and> sub_env e e'' \<and> w \<in> vertices \<and> w \<notin> vsuccs e v \<and> w \<in> vsuccs e'' v

goal (2 subgoals):
 1. \<exists>v w e e''. a = Inr (v, e'') \<and> b = Inr (v, e) \<and> v \<in> vertices \<and> sub_env e e'' \<and> w \<in> vertices \<and> w \<notin> vsuccs e v \<and> w \<in> vsuccs e'' v \<Longrightarrow> (a, b) \<in> inv_image (finite_psubset <*lex*> finite_psubset <*lex*> pred_nat) dfs_dfss_to_tuple
 2. (\<exists>v e e1. a = Inr (v, e1) \<and> b = Inl (v, e) \<and> v \<in> vertices - visited e \<and> visited e1 = visited e \<union> {v}) \<or> (\<exists>v w e. a = Inl (w, e) \<and> b = Inr (v, e)) \<Longrightarrow> (a, b) \<in> inv_image (finite_psubset <*lex*> finite_psubset <*lex*> pred_nat) dfs_dfss_to_tuple
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>v w e e''. a = Inr (v, e'') \<and> b = Inr (v, e) \<and> v \<in> vertices \<and> sub_env e e'' \<and> w \<in> vertices \<and> w \<notin> vsuccs e v \<and> w \<in> vsuccs e'' v
[PROOF STEP]
obtain v w e e'' where
        ab: "a = Inr(v, e'')" "b = Inr(v,e)" and
        vw: "v \<in> vertices" "w \<in> vertices" "w \<in> vsuccs e'' v" "w \<notin> vsuccs e v" and
        sub: "sub_env e e''"
[PROOF STATE]
proof (prove)
using this:
\<exists>v w e e''. a = Inr (v, e'') \<and> b = Inr (v, e) \<and> v \<in> vertices \<and> sub_env e e'' \<and> w \<in> vertices \<and> w \<notin> vsuccs e v \<and> w \<in> vsuccs e'' v

goal (1 subgoal):
 1. (\<And>v e'' e w. \<lbrakk>a = Inr (v, e''); b = Inr (v, e); v \<in> vertices; w \<in> vertices; w \<in> vsuccs e'' v; w \<notin> vsuccs e v; sub_env e e''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
a = Inr (v, e'')
b = Inr (v, e)
v \<in> vertices
w \<in> vertices
w \<in> vsuccs e'' v
w \<notin> vsuccs e v
sub_env e e''

goal (2 subgoals):
 1. \<exists>v w e e''. a = Inr (v, e'') \<and> b = Inr (v, e) \<and> v \<in> vertices \<and> sub_env e e'' \<and> w \<in> vertices \<and> w \<notin> vsuccs e v \<and> w \<in> vsuccs e'' v \<Longrightarrow> (a, b) \<in> inv_image (finite_psubset <*lex*> finite_psubset <*lex*> pred_nat) dfs_dfss_to_tuple
 2. (\<exists>v e e1. a = Inr (v, e1) \<and> b = Inl (v, e) \<and> v \<in> vertices - visited e \<and> visited e1 = visited e \<union> {v}) \<or> (\<exists>v w e. a = Inl (w, e) \<and> b = Inr (v, e)) \<Longrightarrow> (a, b) \<in> inv_image (finite_psubset <*lex*> finite_psubset <*lex*> pred_nat) dfs_dfss_to_tuple
[PROOF STEP]
from sub
[PROOF STATE]
proof (chain)
picking this:
sub_env e e''
[PROOF STEP]
have "vertices - visited e'' \<subseteq> vertices - visited e"
[PROOF STATE]
proof (prove)
using this:
sub_env e e''

goal (1 subgoal):
 1. vertices - visited e'' \<subseteq> vertices - visited e
[PROOF STEP]
by (auto simp: sub_env_def)
[PROOF STATE]
proof (state)
this:
vertices - visited e'' \<subseteq> vertices - visited e

goal (2 subgoals):
 1. \<exists>v w e e''. a = Inr (v, e'') \<and> b = Inr (v, e) \<and> v \<in> vertices \<and> sub_env e e'' \<and> w \<in> vertices \<and> w \<notin> vsuccs e v \<and> w \<in> vsuccs e'' v \<Longrightarrow> (a, b) \<in> inv_image (finite_psubset <*lex*> finite_psubset <*lex*> pred_nat) dfs_dfss_to_tuple
 2. (\<exists>v e e1. a = Inr (v, e1) \<and> b = Inl (v, e) \<and> v \<in> vertices - visited e \<and> visited e1 = visited e \<union> {v}) \<or> (\<exists>v w e. a = Inl (w, e) \<and> b = Inr (v, e)) \<Longrightarrow> (a, b) \<in> inv_image (finite_psubset <*lex*> finite_psubset <*lex*> pred_nat) dfs_dfss_to_tuple
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
vertices - visited e'' \<subseteq> vertices - visited e

goal (2 subgoals):
 1. \<exists>v w e e''. a = Inr (v, e'') \<and> b = Inr (v, e) \<and> v \<in> vertices \<and> sub_env e e'' \<and> w \<in> vertices \<and> w \<notin> vsuccs e v \<and> w \<in> vsuccs e'' v \<Longrightarrow> (a, b) \<in> inv_image (finite_psubset <*lex*> finite_psubset <*lex*> pred_nat) dfs_dfss_to_tuple
 2. (\<exists>v e e1. a = Inr (v, e1) \<and> b = Inl (v, e) \<and> v \<in> vertices - visited e \<and> visited e1 = visited e \<union> {v}) \<or> (\<exists>v w e. a = Inl (w, e) \<and> b = Inr (v, e)) \<Longrightarrow> (a, b) \<in> inv_image (finite_psubset <*lex*> finite_psubset <*lex*> pred_nat) dfs_dfss_to_tuple
[PROOF STEP]
from sub vw
[PROOF STATE]
proof (chain)
picking this:
sub_env e e''
v \<in> vertices
w \<in> vertices
w \<in> vsuccs e'' v
w \<notin> vsuccs e v
[PROOF STEP]
have "(vertices \<times> vertices - {(u,u') | u u'. u' \<in> vsuccs e'' u})
          \<subset> (vertices \<times> vertices - {(u,u') | u u'. u' \<in> vsuccs e u})"
[PROOF STATE]
proof (prove)
using this:
sub_env e e''
v \<in> vertices
w \<in> vertices
w \<in> vsuccs e'' v
w \<notin> vsuccs e v

goal (1 subgoal):
 1. vertices \<times> vertices - {(u, u') |u u'. u' \<in> vsuccs e'' u} \<subset> vertices \<times> vertices - {(u, u') |u u'. u' \<in> vsuccs e u}
[PROOF STEP]
by (auto simp: sub_env_def)
[PROOF STATE]
proof (state)
this:
vertices \<times> vertices - {(u, u') |u u'. u' \<in> vsuccs e'' u} \<subset> vertices \<times> vertices - {(u, u') |u u'. u' \<in> vsuccs e u}

goal (2 subgoals):
 1. \<exists>v w e e''. a = Inr (v, e'') \<and> b = Inr (v, e) \<and> v \<in> vertices \<and> sub_env e e'' \<and> w \<in> vertices \<and> w \<notin> vsuccs e v \<and> w \<in> vsuccs e'' v \<Longrightarrow> (a, b) \<in> inv_image (finite_psubset <*lex*> finite_psubset <*lex*> pred_nat) dfs_dfss_to_tuple
 2. (\<exists>v e e1. a = Inr (v, e1) \<and> b = Inl (v, e) \<and> v \<in> vertices - visited e \<and> visited e1 = visited e \<union> {v}) \<or> (\<exists>v w e. a = Inl (w, e) \<and> b = Inr (v, e)) \<Longrightarrow> (a, b) \<in> inv_image (finite_psubset <*lex*> finite_psubset <*lex*> pred_nat) dfs_dfss_to_tuple
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
vertices - visited e'' \<subseteq> vertices - visited e
vertices \<times> vertices - {(u, u') |u u'. u' \<in> vsuccs e'' u} \<subset> vertices \<times> vertices - {(u, u') |u u'. u' \<in> vsuccs e u}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
vertices - visited e'' \<subseteq> vertices - visited e
vertices \<times> vertices - {(u, u') |u u'. u' \<in> vsuccs e'' u} \<subset> vertices \<times> vertices - {(u, u') |u u'. u' \<in> vsuccs e u}

goal (1 subgoal):
 1. (a, b) \<in> inv_image (finite_psubset <*lex*> finite_psubset <*lex*> pred_nat) dfs_dfss_to_tuple
[PROOF STEP]
using vfin ab
[PROOF STATE]
proof (prove)
using this:
vertices - visited e'' \<subseteq> vertices - visited e
vertices \<times> vertices - {(u, u') |u u'. u' \<in> vsuccs e'' u} \<subset> vertices \<times> vertices - {(u, u') |u u'. u' \<in> vsuccs e u}
finite vertices
a = Inr (v, e'')
b = Inr (v, e)

goal (1 subgoal):
 1. (a, b) \<in> inv_image (finite_psubset <*lex*> finite_psubset <*lex*> pred_nat) dfs_dfss_to_tuple
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(a, b) \<in> inv_image (finite_psubset <*lex*> finite_psubset <*lex*> pred_nat) dfs_dfss_to_tuple

goal (1 subgoal):
 1. (\<exists>v e e1. a = Inr (v, e1) \<and> b = Inl (v, e) \<and> v \<in> vertices - visited e \<and> visited e1 = visited e \<union> {v}) \<or> (\<exists>v w e. a = Inl (w, e) \<and> b = Inr (v, e)) \<Longrightarrow> (a, b) \<in> inv_image (finite_psubset <*lex*> finite_psubset <*lex*> pred_nat) dfs_dfss_to_tuple
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<exists>v e e1. a = Inr (v, e1) \<and> b = Inl (v, e) \<and> v \<in> vertices - visited e \<and> visited e1 = visited e \<union> {v}) \<or> (\<exists>v w e. a = Inl (w, e) \<and> b = Inr (v, e)) \<Longrightarrow> (a, b) \<in> inv_image (finite_psubset <*lex*> finite_psubset <*lex*> pred_nat) dfs_dfss_to_tuple
[PROOF STEP]
assume "?c2 \<or> ?c3"
[PROOF STATE]
proof (state)
this:
(\<exists>v e e1. a = Inr (v, e1) \<and> b = Inl (v, e) \<and> v \<in> vertices - visited e \<and> visited e1 = visited e \<union> {v}) \<or> (\<exists>v w e. a = Inl (w, e) \<and> b = Inr (v, e))

goal (1 subgoal):
 1. (\<exists>v e e1. a = Inr (v, e1) \<and> b = Inl (v, e) \<and> v \<in> vertices - visited e \<and> visited e1 = visited e \<union> {v}) \<or> (\<exists>v w e. a = Inl (w, e) \<and> b = Inr (v, e)) \<Longrightarrow> (a, b) \<in> inv_image (finite_psubset <*lex*> finite_psubset <*lex*> pred_nat) dfs_dfss_to_tuple
[PROOF STEP]
with vfin
[PROOF STATE]
proof (chain)
picking this:
finite vertices
(\<exists>v e e1. a = Inr (v, e1) \<and> b = Inl (v, e) \<and> v \<in> vertices - visited e \<and> visited e1 = visited e \<union> {v}) \<or> (\<exists>v w e. a = Inl (w, e) \<and> b = Inr (v, e))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite vertices
(\<exists>v e e1. a = Inr (v, e1) \<and> b = Inl (v, e) \<and> v \<in> vertices - visited e \<and> visited e1 = visited e \<union> {v}) \<or> (\<exists>v w e. a = Inl (w, e) \<and> b = Inr (v, e))

goal (1 subgoal):
 1. (a, b) \<in> inv_image (finite_psubset <*lex*> finite_psubset <*lex*> pred_nat) dfs_dfss_to_tuple
[PROOF STEP]
by (auto simp: pred_nat_def)
[PROOF STATE]
proof (state)
this:
(a, b) \<in> inv_image (finite_psubset <*lex*> finite_psubset <*lex*> pred_nat) dfs_dfss_to_tuple

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(a, b) \<in> inv_image (finite_psubset <*lex*> finite_psubset <*lex*> pred_nat) dfs_dfss_to_tuple

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
dfs_dfss_term \<subseteq> inv_image (finite_psubset <*lex*> finite_psubset <*lex*> pred_nat) dfs_dfss_to_tuple

goal (1 subgoal):
 1. wf dfs_dfss_term
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
wf (finite_psubset <*lex*> finite_psubset <*lex*> pred_nat)
dfs_dfss_term \<subseteq> inv_image (finite_psubset <*lex*> finite_psubset <*lex*> pred_nat) dfs_dfss_to_tuple
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
wf (finite_psubset <*lex*> finite_psubset <*lex*> pred_nat)
dfs_dfss_term \<subseteq> inv_image (finite_psubset <*lex*> finite_psubset <*lex*> pred_nat) dfs_dfss_to_tuple

goal (1 subgoal):
 1. wf dfs_dfss_term
[PROOF STEP]
using wf_inv_image wf_subset
[PROOF STATE]
proof (prove)
using this:
wf (finite_psubset <*lex*> finite_psubset <*lex*> pred_nat)
dfs_dfss_term \<subseteq> inv_image (finite_psubset <*lex*> finite_psubset <*lex*> pred_nat) dfs_dfss_to_tuple
wf ?r \<Longrightarrow> wf (inv_image ?r ?f)
\<lbrakk>wf ?r; ?p \<subseteq> ?r\<rbrakk> \<Longrightarrow> wf ?p

goal (1 subgoal):
 1. wf dfs_dfss_term
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
wf dfs_dfss_term

goal:
No subgoals!
[PROOF STEP]
qed