>

λ(λ t.t t (λ h f n.n h f n) t t t) (λ f x.f (f x))

β(λ f x.f (f x)) (λ f x.f (f x)) (λ h f n.n h f n) (λ f x.f (f x)) (λ f x.f (f x)) (λ f x.f (f x))

β(λ x.(λ f x.f (f x)) ((λ f x.f (f x)) x)) (λ h f n.n h f n) (λ f x.f (f x)) (λ f x.f (f x)) (λ f x.f (f x))

β(λ f x.f (f x)) ((λ f x.f (f x)) (λ h f n.n h f n)) (λ f x.f (f x)) (λ f x.f (f x)) (λ f x.f (f x))

β(λ x.(λ f x.f (f x)) (λ h f n.n h f n) ((λ f x.f (f x)) (λ h f n.n h f n) x)) (λ f x.f (f x)) (λ f x.f (f x)) (λ f x.f (f x))

β(λ f x.f (f x)) (λ h f n.n h f n) ((λ f x.f (f x)) (λ h f n.n h f n) (λ f x.f (f x))) (λ f x.f (f x)) (λ f x.f (f x))

β(λ x.(λ h f n.n h f n) ((λ h f n.n h f n) x)) ((λ f x.f (f x)) (λ h f n.n h f n) (λ f x.f (f x))) (λ f x.f (f x)) (λ f x.f (f x))

β(λ h f n.n h f n) ((λ h f n.n h f n) ((λ f x.f (f x)) (λ h f n.n h f n) (λ f x.f (f x)))) (λ f x.f (f x)) (λ f x.f (f x))

β(λ f n.n ((λ h f n.n h f n) ((λ f x.f (f x)) (λ h f n.n h f n) (λ f x.f (f x)))) f n) (λ f x.f (f x)) (λ f x.f (f x))

β(λ n.n ((λ h f n.n h f n) ((λ f x.f (f x)) (λ h f n.n h f n) (λ f x.f (f x)))) (λ f x.f (f x)) n) (λ f x.f (f x))

β(λ f x.f (f x)) ((λ h f n.n h f n) ((λ f x.f (f x)) (λ h f n.n h f n) (λ f x.f (f x)))) (λ f x.f (f x)) (λ f x.f (f x))

β(λ x.(λ h f n.n h f n) ((λ f x.f (f x)) (λ h f n.n h f n) (λ f x.f (f x))) ((λ h f n.n h f n) ((λ f x.f (f x)) (λ h f n.n h f n) (λ f x.f (f x))) x)) (λ f x.f (f x)) (λ f x.f (f x))

β(λ h f n.n h f n) ((λ f x.f (f x)) (λ h f n.n h f n) (λ f x.f (f x))) ((λ h f n.n h f n) ((λ f x.f (f x)) (λ h f n.n h f n) (λ f x.f (f x))) (λ f x.f (f x))) (λ f x.f (f x))

β(λ f n.n ((λ f x.f (f x)) (λ h f n.n h f n) (λ f x.f (f x))) f n) ((λ h f n.n h f n) ((λ f x.f (f x)) (λ h f n.n h f n) (λ f x.f (f x))) (λ f x.f (f x))) (λ f x.f (f x))

β(λ n.n ((λ f x.f (f x)) (λ h f n.n h f n) (λ f x.f (f x))) ((λ h f n.n h f n) ((λ f x.f (f x)) (λ h f n.n h f n) (λ f x.f (f x))) (λ f x.f (f x))) n) (λ f x.f (f x))

β(λ f x.f (f x)) ((λ f x.f (f x)) (λ h f n.n h f n) (λ f x.f (f x))) ((λ h f n.n h f n) ((λ f x.f (f x)) (λ h f n.n h f n) (λ f x.f (f x))) (λ f x.f (f x))) (λ f x.f (f x))

β(λ x.(λ f x.f (f x)) (λ h f n.n h f n) (λ f x.f (f x)) ((λ f x.f (f x)) (λ h f n.n h f n) (λ f x.f (f x)) x)) ((λ h f n.n h f n) ((λ f x.f (f x)) (λ h f n.n h f n) (λ f x.f (f x))) (λ f x.f (f x))) (λ f x.f (f x))

β(λ f x.f (f x)) (λ h f n.n h f n) (λ f x.f (f x)) ((λ f x.f (f x)) (λ h f n.n h f n) (λ f x.f (f x)) ((λ h f n.n h f n) ((λ f x.f (f x)) (λ h f n.n h f n) (λ f x.f (f x))) (λ f x.f (f x)))) (λ f x.f (f x))

β(λ x.(λ h f n.n h f n) ((λ h f n.n h f n) x)) (λ f x.f (f x)) ((λ f x.f (f x)) (λ h f n.n h f n) (λ f x.f (f x)) ((λ h f n.n h f n) ((λ f x.f (f x)) (λ h f n.n h f n) (λ f x.f (f x))) (λ f x.f (f x)))) (λ f x.f (f x))

β(λ h f n.n h f n) ((λ h f n.n h f n) (λ f x.f (f x))) ((λ f x.f (f x)) (λ h f n.n h f n) (λ f x.f (f x)) ((λ h f n.n h f n) ((λ f x.f (f x)) (λ h f n.n h f n) (λ f x.f (f x))) (λ f x.f (f x)))) (λ f x.f (f x))

β(λ f n.n ((λ h f n.n h f n) (λ f x.f (f x))) f n) ((λ f x.f (f x)) (λ h f n.n h f n) (λ f x.f (f x)) ((λ h f n.n h f n) ((λ f x.f (f x)) (λ h f n.n h f n) (λ f x.f (f x))) (λ f x.f (f x)))) (λ f x.f (f x))