[STATEMENT]
lemma scc_root_exists:
    assumes "is_scc E scc"
    and scc: "scc \<inter> dom (discovered s) \<noteq> {}"
    shows "\<exists>r. scc_root s r scc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>r. scc_root s r scc
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>r. scc_root s r scc
[PROOF STEP]
let ?S = "scc \<inter> dom (discovered s)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>r. scc_root s r scc
[PROOF STEP]
from discovered_finite
[PROOF STATE]
proof (chain)
picking this:
finite (dom (discovered s))
[PROOF STEP]
have "finite (\<delta> s`?S)"
[PROOF STATE]
proof (prove)
using this:
finite (dom (discovered s))

goal (1 subgoal):
 1. finite (\<delta> s ` (scc \<inter> dom (discovered s)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (\<delta> s ` (scc \<inter> dom (discovered s)))

goal (1 subgoal):
 1. \<exists>r. scc_root s r scc
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite (\<delta> s ` (scc \<inter> dom (discovered s)))

goal (1 subgoal):
 1. \<exists>r. scc_root s r scc
[PROOF STEP]
from scc
[PROOF STATE]
proof (chain)
picking this:
scc \<inter> dom (discovered s) \<noteq> {}
[PROOF STEP]
have "\<delta> s ` ?S \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
scc \<inter> dom (discovered s) \<noteq> {}

goal (1 subgoal):
 1. \<delta> s ` (scc \<inter> dom (discovered s)) \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<delta> s ` (scc \<inter> dom (discovered s)) \<noteq> {}

goal (1 subgoal):
 1. \<exists>r. scc_root s r scc
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<delta> s ` (scc \<inter> dom (discovered s)) \<noteq> {}

goal (1 subgoal):
 1. \<exists>r. scc_root s r scc
[PROOF STEP]
have "\<And>(x::nat) f A. x \<notin> f ` A \<or> (\<exists>y. x = f y \<and> y \<in> A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x f A. x \<notin> f ` A \<or> (\<exists>y. x = f y \<and> y \<in> A)
[PROOF STEP]
by blast 
      \<comment> \<open>autogenerated by sledgehammer\<close>
[PROOF STATE]
proof (state)
this:
?x7 \<notin> ?f7 ` ?A7 \<or> (\<exists>y. ?x7 = ?f7 y \<and> y \<in> ?A7)

goal (1 subgoal):
 1. \<exists>r. scc_root s r scc
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
finite (\<delta> s ` (scc \<inter> dom (discovered s)))
\<delta> s ` (scc \<inter> dom (discovered s)) \<noteq> {}
?x7 \<notin> ?f7 ` ?A7 \<or> (\<exists>y. ?x7 = ?f7 y \<and> y \<in> ?A7)
[PROOF STEP]
have "\<exists>x \<in> ?S. \<delta> s x = Min (\<delta> s ` ?S)"
[PROOF STATE]
proof (prove)
using this:
finite (\<delta> s ` (scc \<inter> dom (discovered s)))
\<delta> s ` (scc \<inter> dom (discovered s)) \<noteq> {}
?x7 \<notin> ?f7 ` ?A7 \<or> (\<exists>y. ?x7 = ?f7 y \<and> y \<in> ?A7)

goal (1 subgoal):
 1. \<exists>x\<in>scc \<inter> dom (discovered s). \<delta> s x = Min (\<delta> s ` (scc \<inter> dom (discovered s)))
[PROOF STEP]
by (metis Min_in)
[PROOF STATE]
proof (state)
this:
\<exists>x\<in>scc \<inter> dom (discovered s). \<delta> s x = Min (\<delta> s ` (scc \<inter> dom (discovered s)))

goal (1 subgoal):
 1. \<exists>r. scc_root s r scc
[PROOF STEP]
with Min_disc_is_scc_root \<open>is_scc E scc\<close>
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?v \<in> ?scc; ?v \<in> dom (discovered s); is_scc E ?scc; \<delta> s ?v = Min (\<delta> s ` (?scc \<inter> dom (discovered s)))\<rbrakk> \<Longrightarrow> scc_root s ?v ?scc
is_scc E scc
\<exists>x\<in>scc \<inter> dom (discovered s). \<delta> s x = Min (\<delta> s ` (scc \<inter> dom (discovered s)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?v \<in> ?scc; ?v \<in> dom (discovered s); is_scc E ?scc; \<delta> s ?v = Min (\<delta> s ` (?scc \<inter> dom (discovered s)))\<rbrakk> \<Longrightarrow> scc_root s ?v ?scc
is_scc E scc
\<exists>x\<in>scc \<inter> dom (discovered s). \<delta> s x = Min (\<delta> s ` (scc \<inter> dom (discovered s)))

goal (1 subgoal):
 1. \<exists>r. scc_root s r scc
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>r. scc_root s r scc

goal:
No subgoals!
[PROOF STEP]
qed