0 := \f x.x (inc n) := \f x.(f (n f x)) (add n m) := (m inc n) (mult n m) := (m (n f)) (exp m n) := (m n) # This is the final output. 5 := (inc (inc (inc (inc (inc 0))))) (exp 5 5)