-- haskell

data Tree = Leaf | Node Tree Tree

N :: Tree -> Int
N (Leaf) = 0
N (Node T1 T2) = (N T1) + (N T2) + 1

H :: Tree -> Int
H (Leaf) = 0
H (Node T1 T2) = 1 + (max (H T1) (H T2))

-- Prove by induction that (N t) < 2^(H t)

P(t) := (N t) < 2^(H t)

We'll prove that forall t: Tree . P(t) by induction on t

Base Case (P(Leaf))

N Leaf = 0
       < 1
       = 2^0
       = 2^(H Leaf)

Step Case: Assume forall l,r:Tree . P(l),P(r). We show that P (Node l r) holds

N (Node l r) = N l + N r + 1
             < 2^(H l) + 2^(H r) + 1 (I.H)
             < 2^(1 + (max (H l) (H r)))
             = 2^(H (Node l r))