proof3.txt

count t
(count) = aux t 0
To prove nodes t = count t, one can first prove acc + node t = aux t acc.

Generalized statement (*): acc + node t = aux t acc

Base Case: t = Empty
Statement being proven in base case: acc + node Empty = aux Empty acc
Proof of base case:
acc + node Empty
(node) = acc + match Empty with Empty -> 0 | Node (l,r) -> 1 + (nodes l) + (nodes r)
(match) = acc + 0
(arith) = acc
(match) = match Empty with Empty -> acc | Node (l,r) -> aux r (aux l (acc+1))
(aux) = aux Empty acc
---
Inductive Step: 
Induction hypothesis (or hypotheses):
For trees a and b holds:
acc + node x = aux x acc (I.H. 1)
and
acc + node y = aux y acc (I.H. 2)
Statement being proved in inductive step: acc + node (Node (x, y)) = aux (Node (x, y)) acc
Proof of inductive step:
acc + node (Node (x, y))
(node) = acc + (match t with Empty -> 0 | Node (l,r) -> 1 + (nodes l) + (nodes r))
(match) = acc + (1 + (nodes x) + (nodes y))
(arith) = acc + 1 + nodes x + nodes y
(arith) = ((acc+1) + node x) + node y
(I.H. 2) = aux y ((acc+1) + node x)
(I.H. 1) = aux y (aux x (acc+1))
(match) = match (Node (x, y)) with Empty -> acc | Node (l,r) -> aux r (aux l (acc+1))
(aux) = aux (Node (x, y)) acc
---
Instantiation of generalization:
count t
(count) = aux t 0
(*) = 0 + node t
(arith) = node t
---
QED