Lambda calculus predecessor function reduction steps
11:00 09 Jan 2012

I am getting stuck with the Wikipedia description of the predecessor function in lambda calculus.

What Wikipedia says is the following:

PRED := λn.λf.λx. n (λg.λh. h (g f)) (λu.x) (λu.u)

Can someone explain reduction processes step-by-step?

Thanks.

lambda-calculus reduction