Originally Posted by

**gomdohri** 3. (Extension work) Prove count(revT t) = count (t)

Base Case P (Nil)

count (rev T Nil) = count (Nil)

= count (rev T Nil) (LH)

= count (Nil) -- T1

Step Case Step Case ∀t1, ∀t2, P(t1) ^ P (t2) => (P (Node x t1 t2))

Assume P (u1) ^ P (u2)

count (rev T u1) = count (u1) -- IH1

count (rev T u2) = count (u2) -- IH2

Prove P (Node a u1 u2), that is

count (revT (Node a u1 u2)) = count (Node a u1 u2)

= count (Node a (revT u2) (revT u1)) -- T2

= Node (count a) (count(revT u2) (count (rev u1)) -

= Node (count a) (count u2) (count u1) -- IH1, IH2

= count (Node a u2 u1) (LH)