[STATEMENT]
lemma dtail_root_in_set:
  assumes "e \<in> darcs t" and "t = Node r xs" and "dtail t dt e = r"
  shows "e \<in> snd ` fset xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e \<in> snd ` fset xs
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. e \<notin> snd ` fset xs \<Longrightarrow> False
[PROOF STEP]
assume "e \<notin> snd ` fset xs"
[PROOF STATE]
proof (state)
this:
e \<notin> snd ` fset xs

goal (1 subgoal):
 1. e \<notin> snd ` fset xs \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
e \<notin> snd ` fset xs
[PROOF STEP]
obtain x e1 where x_def: "(x,e1) \<in> fset xs \<and> e \<in> darcs x"
[PROOF STATE]
proof (prove)
using this:
e \<notin> snd ` fset xs

goal (1 subgoal):
 1. (\<And>x e1. (x, e1) \<in> fset xs \<and> e \<in> darcs x \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms(1,2)
[PROOF STATE]
proof (prove)
using this:
e \<notin> snd ` fset xs
e \<in> darcs t
t = Node r xs

goal (1 subgoal):
 1. (\<And>x e1. (x, e1) \<in> fset xs \<and> e \<in> darcs x \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(x, e1) \<in> fset xs \<and> e \<in> darcs x

goal (1 subgoal):
 1. e \<notin> snd ` fset xs \<Longrightarrow> False
[PROOF STEP]
interpret X: wf_dtree x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_dtree x
[PROOF STEP]
using assms(2) x_def wf_dtree_rec
[PROOF STATE]
proof (prove)
using this:
t = Node r xs
(x, e1) \<in> fset xs \<and> e \<in> darcs x
\<lbrakk>Node ?r ?xs = t; (?x, ?e) \<in> fset ?xs\<rbrakk> \<Longrightarrow> wf_dtree ?x

goal (1 subgoal):
 1. wf_dtree x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. e \<notin> snd ` fset xs \<Longrightarrow> False
[PROOF STEP]
have "dtail t dt e = dtail x dt e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dtail t dt e = dtail x dt e
[PROOF STEP]
using dtail_in_child_eq_child[of x] wf_arcs assms(2) x_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(x, ?e1.0) \<in> fset ?xs; ?e \<in> darcs x; wf_darcs (Node ?r ?xs)\<rbrakk> \<Longrightarrow> dtail (Node ?r ?xs) ?def ?e = dtail x ?def ?e
wf_darcs t
t = Node r xs
(x, e1) \<in> fset xs \<and> e \<in> darcs x

goal (1 subgoal):
 1. dtail t dt e = dtail x dt e
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
dtail t dt e = dtail x dt e

goal (1 subgoal):
 1. e \<notin> snd ` fset xs \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dtail t dt e = dtail x dt e
[PROOF STEP]
have "dtail t dt e \<in> dverts x"
[PROOF STATE]
proof (prove)
using this:
dtail t dt e = dtail x dt e

goal (1 subgoal):
 1. dtail t dt e \<in> dverts x
[PROOF STEP]
using X.dtail_in_dverts x_def
[PROOF STATE]
proof (prove)
using this:
dtail t dt e = dtail x dt e
?e \<in> darcs x \<Longrightarrow> dtail x ?def ?e \<in> dverts x
(x, e1) \<in> fset xs \<and> e \<in> darcs x

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

goal (1 subgoal):
 1. e \<notin> snd ` fset xs \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dtail t dt e \<in> dverts x
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
dtail t dt e \<in> dverts x

goal (1 subgoal):
 1. False
[PROOF STEP]
using assms(2,3) wf_verts x_def
[PROOF STATE]
proof (prove)
using this:
dtail t dt e \<in> dverts x
t = Node r xs
dtail t dt e = r
wf_dverts t
(x, e1) \<in> fset xs \<and> e \<in> darcs x

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding wf_dverts_iff_dverts'
[PROOF STATE]
proof (prove)
using this:
dtail t dt e \<in> dverts x
t = Node r xs
dtail t dt e = r
wf_dverts' t
(x, e1) \<in> fset xs \<and> e \<in> darcs x

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

goal:
No subgoals!
[PROOF STEP]
qed