Redexer

Click a reducible expression to step through the reduction of an untyped lambda calculus term.


(λx.λy.λs.λz.(x s) (y s z)) (λs.λz.s z) (λs.λz.s (s z))