[STATEMENT]
lemma adjacent_singleton: "t \<noteq> Leaf \<Longrightarrow> adjacent (l t, r t) [t]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<noteq> Leaf \<Longrightarrow> adjacent (l t, r t) [t]
[PROOF STEP]
unfolding adjacent_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<noteq> Leaf \<Longrightarrow> Leaf \<notin> set [t] \<and> list_all2 (\<lambda>t u. l t = Suc (r u)) (butlast [t]) (tl [t]) \<and> ([t] = [] \<or> l (last [t]) = fst (l t, r t) \<and> r (hd [t]) = snd (l t, r t))
[PROOF STEP]
by simp