[STATEMENT]
lemma leaf_not_mem_awalk:
  "\<lbrakk> leaf x; awalk u p v; v \<noteq> x \<rbrakk> \<Longrightarrow> x \<notin> set (awalk_verts u p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>leaf x; awalk u p v; v \<noteq> x\<rbrakk> \<Longrightarrow> x \<notin> set (awalk_verts u p)
[PROOF STEP]
proof(induction p arbitrary: u)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>u. \<lbrakk>leaf x; awalk u [] v; v \<noteq> x\<rbrakk> \<Longrightarrow> x \<notin> set (awalk_verts u [])
 2. \<And>a p u. \<lbrakk>\<And>u. \<lbrakk>leaf x; awalk u p v; v \<noteq> x\<rbrakk> \<Longrightarrow> x \<notin> set (awalk_verts u p); leaf x; awalk u (a # p) v; v \<noteq> x\<rbrakk> \<Longrightarrow> x \<notin> set (awalk_verts u (a # p))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
leaf x
awalk u [] v
v \<noteq> x

goal (2 subgoals):
 1. \<And>u. \<lbrakk>leaf x; awalk u [] v; v \<noteq> x\<rbrakk> \<Longrightarrow> x \<notin> set (awalk_verts u [])
 2. \<And>a p u. \<lbrakk>\<And>u. \<lbrakk>leaf x; awalk u p v; v \<noteq> x\<rbrakk> \<Longrightarrow> x \<notin> set (awalk_verts u p); leaf x; awalk u (a # p) v; v \<noteq> x\<rbrakk> \<Longrightarrow> x \<notin> set (awalk_verts u (a # p))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
leaf x
awalk u [] v
v \<noteq> x
[PROOF STEP]
have "u = v"
[PROOF STATE]
proof (prove)
using this:
leaf x
awalk u [] v
v \<noteq> x

goal (1 subgoal):
 1. u = v
[PROOF STEP]
unfolding awalk_conv
[PROOF STATE]
proof (prove)
using this:
leaf x
set (awalk_verts u []) \<subseteq> verts T \<and> set [] \<subseteq> arcs T \<and> awhd u [] = u \<and> awlast u [] = v \<and> cas u [] v
v \<noteq> x

goal (1 subgoal):
 1. u = v
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
u = v

goal (2 subgoals):
 1. \<And>u. \<lbrakk>leaf x; awalk u [] v; v \<noteq> x\<rbrakk> \<Longrightarrow> x \<notin> set (awalk_verts u [])
 2. \<And>a p u. \<lbrakk>\<And>u. \<lbrakk>leaf x; awalk u p v; v \<noteq> x\<rbrakk> \<Longrightarrow> x \<notin> set (awalk_verts u p); leaf x; awalk u (a # p) v; v \<noteq> x\<rbrakk> \<Longrightarrow> x \<notin> set (awalk_verts u (a # p))
[PROOF STEP]
with Nil
[PROOF STATE]
proof (chain)
picking this:
leaf x
awalk u [] v
v \<noteq> x
u = v
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
leaf x
awalk u [] v
v \<noteq> x
u = v

goal (1 subgoal):
 1. x \<notin> set (awalk_verts u [])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<notin> set (awalk_verts u [])

goal (1 subgoal):
 1. \<And>a p u. \<lbrakk>\<And>u. \<lbrakk>leaf x; awalk u p v; v \<noteq> x\<rbrakk> \<Longrightarrow> x \<notin> set (awalk_verts u p); leaf x; awalk u (a # p) v; v \<noteq> x\<rbrakk> \<Longrightarrow> x \<notin> set (awalk_verts u (a # p))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a p u. \<lbrakk>\<And>u. \<lbrakk>leaf x; awalk u p v; v \<noteq> x\<rbrakk> \<Longrightarrow> x \<notin> set (awalk_verts u p); leaf x; awalk u (a # p) v; v \<noteq> x\<rbrakk> \<Longrightarrow> x \<notin> set (awalk_verts u (a # p))
[PROOF STEP]
case (Cons a p)
[PROOF STATE]
proof (state)
this:
\<lbrakk>leaf x; awalk ?u2 p v; v \<noteq> x\<rbrakk> \<Longrightarrow> x \<notin> set (awalk_verts ?u2 p)
leaf x
awalk u (a # p) v
v \<noteq> x

goal (1 subgoal):
 1. \<And>a p u. \<lbrakk>\<And>u. \<lbrakk>leaf x; awalk u p v; v \<noteq> x\<rbrakk> \<Longrightarrow> x \<notin> set (awalk_verts u p); leaf x; awalk u (a # p) v; v \<noteq> x\<rbrakk> \<Longrightarrow> x \<notin> set (awalk_verts u (a # p))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>leaf x; awalk ?u2 p v; v \<noteq> x\<rbrakk> \<Longrightarrow> x \<notin> set (awalk_verts ?u2 p)
leaf x
awalk u (a # p) v
v \<noteq> x
[PROOF STEP]
have "x \<notin> set (awalk_verts (head T a) p)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>leaf x; awalk ?u2 p v; v \<noteq> x\<rbrakk> \<Longrightarrow> x \<notin> set (awalk_verts ?u2 p)
leaf x
awalk u (a # p) v
v \<noteq> x

goal (1 subgoal):
 1. x \<notin> set (awalk_verts (head T a) p)
[PROOF STEP]
by (simp add: awalk_Cons_iff)
[PROOF STATE]
proof (state)
this:
x \<notin> set (awalk_verts (head T a) p)

goal (1 subgoal):
 1. \<And>a p u. \<lbrakk>\<And>u. \<lbrakk>leaf x; awalk u p v; v \<noteq> x\<rbrakk> \<Longrightarrow> x \<notin> set (awalk_verts u p); leaf x; awalk u (a # p) v; v \<noteq> x\<rbrakk> \<Longrightarrow> x \<notin> set (awalk_verts u (a # p))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<notin> set (awalk_verts (head T a) p)

goal (1 subgoal):
 1. \<And>a p u. \<lbrakk>\<And>u. \<lbrakk>leaf x; awalk u p v; v \<noteq> x\<rbrakk> \<Longrightarrow> x \<notin> set (awalk_verts u p); leaf x; awalk u (a # p) v; v \<noteq> x\<rbrakk> \<Longrightarrow> x \<notin> set (awalk_verts u (a # p))
[PROOF STEP]
from Cons.prems
[PROOF STATE]
proof (chain)
picking this:
leaf x
awalk u (a # p) v
v \<noteq> x
[PROOF STEP]
have "tail T a \<noteq> x"
[PROOF STATE]
proof (prove)
using this:
leaf x
awalk u (a # p) v
v \<noteq> x

goal (1 subgoal):
 1. tail T a \<noteq> x
[PROOF STEP]
unfolding leaf_def out_arcs_def
[PROOF STATE]
proof (prove)
using this:
x \<in> verts T \<and> {e \<in> arcs T. tail T e = x} = {}
awalk u (a # p) v
v \<noteq> x

goal (1 subgoal):
 1. tail T a \<noteq> x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
tail T a \<noteq> x

goal (1 subgoal):
 1. \<And>a p u. \<lbrakk>\<And>u. \<lbrakk>leaf x; awalk u p v; v \<noteq> x\<rbrakk> \<Longrightarrow> x \<notin> set (awalk_verts u p); leaf x; awalk u (a # p) v; v \<noteq> x\<rbrakk> \<Longrightarrow> x \<notin> set (awalk_verts u (a # p))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x \<notin> set (awalk_verts (head T a) p)
tail T a \<noteq> x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
x \<notin> set (awalk_verts (head T a) p)
tail T a \<noteq> x

goal (1 subgoal):
 1. x \<notin> set (awalk_verts u (a # p))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<notin> set (awalk_verts u (a # p))

goal:
No subgoals!
[PROOF STEP]
qed