lambda_calculus_fib_5

(λy.y (λp.λt.t (p (λf.λg.g)) (λs.λx.p (λf.λg.f) s (p (λf.λg.g) s x))) (λt.t (λf.λx.f x) (λf.λx.f x)) (λf.λg.g)) (λf.λx.f (f (f x)))

(λf.λx.f (f (f x))) (λp.λt.t (p (λf.λg.g)) (λs.λx.p (λf.λg.f) s (p (λf.λg.g) s x))) (λt.t (λf.λx.f x) (λf.λx.f x)) (λf.λg.g)

(λx.(λp.λt.t (p (λf.λg.g)) (λs.λx.p (λf.λg.f) s (p (λf.λg.g) s x))) ((λp.λt.t (p (λf.λg.g)) (λs.λx.p (λf.λg.f) s (p (λf.λg.g) s x))) ((λp.λt.t (p (λf.λg.g)) (λs.λx.p (λf.λg.f) s (p (λf.λg.g) s x))) x))) (λt.t (λf.λx.f x) (λf.λx.f x)) (λf.λg.g)

(λp.λt.t (p (λf.λg.g)) (λs.λx.p (λf.λg.f) s (p (λf.λg.g) s x))) ((λp.λt.t (p (λf.λg.g)) (λs.λx.p (λf.λg.f) s (p (λf.λg.g) s x))) ((λp.λt.t (p (λf.λg.g)) (λs.λx.p (λf.λg.f) s (p (λf.λg.g) s x))) (λt.t (λf.λx.f x) (λf.λx.f x)))) (λf.λg.g)

(λt.t (((λp.λt.t (p (λf.λg.g)) (λs.λx.p (λf.λg.f) s (p (λf.λg.g) s x))) ((λp.λt.t (p (λf.λg.g)) (λs.λx.p (λf.λg.f) s (p (λf.λg.g) s x))) (λt.t (λf.λx.f x) (λf.λx.f x)))) (λf.λg.g)) (λs.λx.((λp.λt.t (p (λf.λg.g)) (λs.λx.p (λf.λg.f) s (p (λf.λg.g) s x))) ((λp.λt.t (p (λf.λg.g)) (λs.λx.p (λf.λg.f) s (p (λf.λg.g) s x))) (λt.t (λf.λx.f x) (λf.λx.f x)))) (λf.λg.f) s (((λp.λt.t (p (λf.λg.g)) (λs.λx.p (λf.λg.f) s (p (λf.λg.g) s x))) ((λp.λt.t (p (λf.λg.g)) (λs.λx.p (λf.λg.f) s (p (λf.λg.g) s x))) (λt.t (λf.λx.f x) (λf.λx.f x)))) (λf.λg.g) s x))) (λf.λg.g)

(λf.λg.g) (((λp.λt.t (p (λf.λg.g)) (λs.λx.p (λf.λg.f) s (p (λf.λg.g) s x))) ((λp.λt.t (p (λf.λg.g)) (λs.λx.p (λf.λg.f) s (p (λf.λg.g) s x))) (λt.t (λf.λx.f x) (λf.λx.f x)))) (λf.λg.g)) (λs.λx.((λp.λt.t (p (λf.λg.g)) (λs.λx.p (λf.λg.f) s (p (λf.λg.g) s x))) ((λp.λt.t (p (λf.λg.g)) (λs.λx.p (λf.λg.f) s (p (λf.λg.g) s x))) (λt.t (λf.λx.f x) (λf.λx.f x)))) (λf.λg.f) s (((λp.λt.t (p (λf.λg.g)) (λs.λx.p (λf.λg.f) s (p (λf.λg.g) s x))) ((λp.λt.t (p (λf.λg.g)) (λs.λx.p (λf.λg.f) s (p (λf.λg.g) s x))) (λt.t (λf.λx.f x) (λf.λx.f x)))) (λf.λg.g) s x))

(λs.λx.(λt.t ((λp.λt.t (p (λf.λg.g)) (λs.λx.p (λf.λg.f) s (p (λf.λg.g) s x))) (λt.t (λf.λx.f x) (λf.λx.f x)) (λf.λg.g)) (λs.λx.(λp.λt.t (p (λf.λg.g)) (λs.λx.p (λf.λg.f) s (p (λf.λg.g) s x))) (λt.t (λf.λx.f x) (λf.λx.f x)) (λf.λg.f) s ((λp.λt.t (p (λf.λg.g)) (λs.λx.p (λf.λg.f) s (p (λf.λg.g) s x))) (λt.t (λf.λx.f x) (λf.λx.f x)) (λf.λg.g) s x))) (λf.λg.f) s ((λt.t ((λp.λt.t (p (λf.λg.g)) (λs.λx.p (λf.λg.f) s (p (λf.λg.g) s x))) (λt.t (λf.λx.f x) (λf.λx.f x)) (λf.λg.g)) (λs.λx.(λp.λt.t (p (λf.λg.g)) (λs.λx.p (λf.λg.f) s (p (λf.λg.g) s x))) (λt.t (λf.λx.f x) (λf.λx.f x)) (λf.λg.f) s ((λp.λt.t (p (λf.λg.g)) (λs.λx.p (λf.λg.f) s (p (λf.λg.g) s x))) (λt.t (λf.λx.f x) (λf.λx.f x)) (λf.λg.g) s x))) (λf.λg.g) s x))

(λs.λx.((λf.λg.f) ((λt.λp.t (p (λf.λg.g)) (λs.λx.p (λf.λg.f) s (p (λf.λg.g) s x))) (λt.t (λf.λx.f x) (λf.λx.f x)) (λf.λg.g)) (λs.λx.(λp.λt.t (p (λf.λg.g)) (λs.λx.p (λf.λg.f) s (p (λf.λg.g) s x))) (λt.t (λf.λx.f x) (λf.λx.f x)) (λf.λg.f) s ((λp.λt.t (p (λf.λg.g)) (λs.λx.p (λf.λg.f) s (p (λf.λg.g) s x))) (λt.t (λf.λx.f x) (λf.λx.f x)) (λf.λg.g) s x))) s (((λf.λg.g) ((λp.λt.t (p (λf.λg.g)) (λs.λx.p (λf.λg.f) s (p (λf.λg.g) s x))) (λt.t (λf.λx.f x) (λf.λx.f x)) (λf.λg.g)) (λs.λx.(λp.λt.t (p (λf.λg.g)) (λs.λx.p (λf.λg.f) s (p (λf.λg.g) s x))) (λt.t (λf.λx.f x) (λf.λx.f x)) (λf.λg.f) s ((λp.λt.t (p (λf.λg.g)) (λs.λx.p (λf.λg.f) s (p (λf.λg.g) s x))) (λt.t (λf.λx.f x) (λf.λx.f x)) (λf.λg.g) s x))) s x))

(λs.λx.((λg.(λt.λp.t (p (λf.λg.g)) (λs.λx.p (λf.λg.f) s (p (λf.λg.g) s x))) (λt.t (λf.λx.f x) (λf.λx.f x)) (λf.λg.g)) (λs.λx.(λt.t (λt.t (λf.λx.f x) (λf.λx.f x)) (λf.λg.g) (λs.λx.(λt.t (λf.λx.f x) (λf.λx.f x)) (λf.λg.f) s ((λt.t (λf.λx.f x) (λf.λx.f x)) (λf.λg.g) s x))) (λf.λg.f) s ((λt.t (λt.t (λf.λx.f x) (λf.λx.f x)) (λf.λg.g)) (λs.λx.(λt.t (λf.λx.f x) (λf.λx.f x)) (λf.λg.f) s ((λt.t (λf.λx.f x) (λf.λx.f x)) (λf.λg.g) s x))) (λf.λg.g) s x)) s (((λs.λx.(λt.t ((λt.t (λf.λx.f x) (λf.λx.f x)) (λf.λg.g)) (λs.λx.(λt.t (λf.λx.f x) (λf.λx.f x)) (λf.λg.f) s ((λt.t (λf.λx.f x) (λf.λx.f x)) (λf.λg.g) s x))) (λf.λg.f) s ((λt.t ((λt.t (λf.λx.f x) (λf.λx.f x)) (λf.λg.g)) (λs.λx.(λt.t (λf.λx.f x) (λf.λx.f x)) (λf.λg.f) s ((λt.t (λf.λx.f x) (λf.λx.f x)) (λf.λg.g) s x))) (λf.λg.g) s x))) s x))

(λs.λx.(λt.λp.t (p (λf.λg.g)) (λs.λx.p (λf.λg.f) s (p (λf.λg.g) s x))) (λt.t (λf.λx.f x) (λf.λx.f x)) (λf.λg.g) s ((λx.(λt.t ((λt.t (λf.λx.f x) (λf.λx.f x)) (λf.λg.g)) (λs.λx.(λt.t (λf.λx.f x) (λf.λx.f x)) (λf.λg.f) s ((λt.t (λf.λx.f x) (λf.λx.f x)) (λf.λg.g) s x))) (λf.λg.f) s ((λt.t ((λt.t (λf.λx.f x) (λf.λx.f x)) (λf.λg.g)) (λs.λx.(λt.t (λf.λx.f x) (λf.λx.f x)) (λf.λg.f) s ((λt.t (λf.λx.f x) (λf.λx.f x)) (λf.λg.g) s x))) (λf.λg.g) s x)) x))

(λs.λx.(λp.(λt.t (λf.λx.f x) (λf.λx.f x)) (p (λf.λg.g)) (λs.λx.p (λf.λg.f) s (p (λf.λg.g) s x))) (λf.λg.g) s ((λt.t ((λt.t (λf.λx.f x) (λf.λx.f x)) (λf.λg.g)) (λs.λx.(λt.t (λf.λx.f x) (λf.λx.f x)) (λf.λg.f) s ((λt.t (λf.λx.f x) (λf.λx.f x)) (λf.λg.g) s x))) (λf.λg.f) s ((λt.t ((λt.t (λf.λx.f x) (λf.λx.f x)) (λf.λg.g)) (λs.λx.(λt.t (λf.λx.f x) (λf.λx.f x)) (λf.λg.f) s ((λt.t (λf.λx.f x) (λf.λx.f x)) (λf.λg.g) s x))) (λf.λg.g) s x))))

(λs.λx.(λt.t (λf.λx.f x) (λf.λx.f x)) ((λf.λg.g) (λf.λg.g)) (λs.λx.(λf.λg.g) (λf.λg.f) s ((λf.λg.g) (λf.λg.g) s x)) s ((λf.λg.f) ((λt.t (λf.λx.f x) (λf.λx.f x)) (λf.λg.g)) (λs.λx.(λt.t (λf.λx.f x) (λf.λx.f x)) (λf.λg.f) s ((λt.t (λf.λx.f x) (λf.λx.f x)) (λf.λg.g) s x)) s ((λf.λg.g) ((λt.t (λf.λx.f x) (λf.λx.f x)) (λf.λg.g)) (λs.λx.(λt.t (λf.λx.f x) (λf.λx.f x)) (λf.λg.f) s ((λt.t (λf.λx.f x) (λf.λx.f x)) (λf.λg.g) s x)) s x)))

(λs.λx.(λf.λg.g) (λf.λg.g) (λf.λx.f x) (λf.λx.f x) (λs.λx.(λg.g) s ((λg.g) s x)) s ((λg.((λt.t (λf.λx.f x) (λf.λx.f x)) (λf.λg.g))) (λs.λx.(λf.λg.f) (λf.λx.f x) (λf.λx.f x) s ((λf.λg.g) (λf.λx.f x) (λf.λx.f x) s x)) s ((λs.λx.(λf.λg.f) (λf.λx.f x) (λf.λx.f x) s ((λf.λg.g) (λf.λx.f x) (λf.λx.f x) s x)) s x)))

(λs.λx.(λf.λx.f x) (λf.λx.f x) (λs.λx.s (s x)) s ((λt.t (λf.λx.f x) (λf.λx.f x)) (λf.λg.g) s ((λx.(λf.λg.f) (λf.λx.f x) (λf.λx.f x) s ((λf.λg.g) (λf.λx.f x) (λf.λx.f x) s x)) x)))

(λs.λx.(λf.λx.f x) (λs.λx.s (s x)) s ((λf.λx.f x) s ((λg.(λf.λx.f x)) (λf.λx.f x) s ((λf.λx.f x) s x))))

(λs.λx.(λx.(λs.λx.s (s x)) x) s ((λx.s x) ((λf.λx.f x) s ((λf.λx.f x) s x))))

(λs.λx.(λx.s (s x)) (s ((λx.s x) ((λx.s x) x))))

(λs.λx.s (s (s ((λx.s x) ((λx.s x) x)))))

(λs.λx.s (s (s (s ((λx.s x) x))))))

(λs.λx.s (s (s (s (s x))))))