1. Find a fixed point `X` for the succ function: H := \f.succ(ff) X := HH == (\f.succ(ff)) H ~~> succ(HH) So `succ(HH) <~~> succ(succ(HH))`. 2. Prove that `add 1 X <~~> X`: add 1 X == (\mn.m succ n) 1 X ~~> 1 succ X == (\fz.fz) succ X ~~> succ X What about `add 2 X`? add 2 X == (\mn.m succ n) 2 X ~~> 2 succ X == (\fz.f(fz)) succ X ~~> succ (succ X) So `add n X <~~> X` for all (finite) natural numbers `n`.