[STATEMENT]
lemma G_edge_succ_a'_no_loop:
    assumes no_loop_a: "head G a \<noteq> tail G a" shows G_edge_succ_a': "edge_succ M a' = a'" (is ?t2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. edge_succ M a' = a'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. edge_succ M a' = a'
[PROOF STEP]
have *: "out_arcs G (tail G a') = {a'}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. out_arcs G (tail G a') = {a'}
[PROOF STEP]
using a_in isolated_head no_loop_a
[PROOF STATE]
proof (prove)
using this:
a \<in> arcs G
head G a \<in> H.isolated_verts
head G a \<noteq> tail G a

goal (1 subgoal):
 1. out_arcs G (tail G a') = {a'}
[PROOF STEP]
by (auto simp: H.isolated_verts_def verts_H out_arcs_def arcs_H tail_H)
[PROOF STATE]
proof (state)
this:
out_arcs G (tail G a') = {a'}

goal (1 subgoal):
 1. edge_succ M a' = a'
[PROOF STEP]
obtain "edge_succ M a' \<in> {a'}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (edge_succ M a' \<in> {a'} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using G.edge_succ_cyclic[of "tail G a'"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>tail G a' \<in> verts G; out_arcs G (tail G a') \<noteq> {}\<rbrakk> \<Longrightarrow> cyclic_on (edge_succ M) (out_arcs G (tail G a'))

goal (1 subgoal):
 1. (edge_succ M a' \<in> {a'} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply (rule eq_on_cyclic_on_iff1[where x="a'"])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. (edge_succ M a' \<in> {a'} \<Longrightarrow> thesis) \<Longrightarrow> tail G a' \<in> verts G
 2. (edge_succ M a' \<in> {a'} \<Longrightarrow> thesis) \<Longrightarrow> out_arcs G (tail G a') \<noteq> {}
 3. (edge_succ M a' \<in> {a'} \<Longrightarrow> thesis) \<Longrightarrow> a' \<in> out_arcs G (tail G a')
 4. \<lbrakk>edge_succ M a' \<in> {a'} \<Longrightarrow> thesis; edge_succ M a' \<in> out_arcs G (tail G a'); (edge_succ M a' = a') = (card (out_arcs G (tail G a')) = 1)\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using * a_in a_neq_a' no_loop_a
[PROOF STATE]
proof (prove)
using this:
out_arcs G (tail G a') = {a'}
a \<in> arcs G
a \<noteq> a'
head G a \<noteq> tail G a

goal (4 subgoals):
 1. (edge_succ M a' \<in> {a'} \<Longrightarrow> thesis) \<Longrightarrow> tail G a' \<in> verts G
 2. (edge_succ M a' \<in> {a'} \<Longrightarrow> thesis) \<Longrightarrow> out_arcs G (tail G a') \<noteq> {}
 3. (edge_succ M a' \<in> {a'} \<Longrightarrow> thesis) \<Longrightarrow> a' \<in> out_arcs G (tail G a')
 4. \<lbrakk>edge_succ M a' \<in> {a'} \<Longrightarrow> thesis; edge_succ M a' \<in> out_arcs G (tail G a'); (edge_succ M a' = a') = (card (out_arcs G (tail G a')) = 1)\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
edge_succ M a' \<in> {a'}

goal (1 subgoal):
 1. edge_succ M a' = a'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
edge_succ M a' \<in> {a'}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
edge_succ M a' \<in> {a'}

goal (1 subgoal):
 1. edge_succ M a' = a'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
edge_succ M a' = a'

goal:
No subgoals!
[PROOF STEP]
qed