Current state

Tromp diagram

0 beta step 0 redexes 0 marks
Ready Enter a term or choose an example to begin.
β0 (λm.λn.λf.m (n f)) ((λm.λn.λf.m (n f)) (λf.λx.f (f (f x))) (λf.λx.f (f x))) (λf.λx.f x)
Ready · β0/24
λ

Loading the computation engine…

Binder family Application Active structure