flatmap14

Syntax:
Exp u ::= x         variable
          λx.u      λ-abstraction
          u1 u2     application

Computation rule:
(λx.u2) u1
[u1/x]u2

0 := λf.λx.x
1 := λf.λx.f x
2 := λf.λx.f (f x)

(λf.λx.f (f x)) foo bar
(λx.foo (foo x)) bar
foo (foo bar)

s := λn.λf.λx.f (n f x)

s 2
1

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

+ := λa.λb.a s b

* := λa.λb.a (+ b) 0

* 2 (+ 2 2)

2
λf.λx.f x

solution from last time:
replace x with (0, 0)
replace f with something that maps (a, b) to (a + 1, a)
(0, 0)
(1, 0)
(2, 1)
(3, 2)
then pick the second part of the pair to get previous number

keeping track of two numbers is maybe meh
 - dependencies on bleeding-edge technologies like pairs
   - dependencies!
     - mvn

s (s (s (s (s 0))))

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

1
(λf.λx.f x) zero 

2 
identity (identity zero)


----
Tony Morris: Explain List Folds to Yourself
http://functionaltalks.org/2013/06/19/tony-morris-explain-list-folds-to-yourself/

cons
nil

fold foo bar (cons 1 (cons 3 (cons 5 nil)))
             (foo 1 (foo 3 (foo 5 bar)))



   fold + 0 (cons 1 (cons 2 (cons 3 nil)))
=>          (+    1 (+    2 (+    3 0)))

appendy:
a = (cons 1 (cons 2 nil))
b = (cons 3 (cons 4 nil))
   fold cons b a
=> fold cons b (cons 1 (cons 2 nil))
=>             (cons 1 (cons 2 b))
=>             (cons 1 (cons 2 (cons 3 (cons 4 nil))))

cons
nil

s
0


list:
(cons 1 (cons 2 (cons 3 nil)))
number:
(s (s (s 0)))

so numbers are basically lists, but without junk in them:
list:
             junk
       _______|_______
      |       |       |
      v       v       v
(cons 1 (cons 2 (cons 3 nil)))

number:
           no junk
       _______|_______
      |       |       |
      v       v       v
(s      (s      (s      0)))


   fold foo bar (cons 1 (cons 2 (cons 3 nil)))
=>              (foo  1 (foo  2 (foo  3 bar)))

and so
   fold foo bar (s   (s   (s   0)))
=>              (foo (foo (foo bar)))


(s (s (s 0))) foo bar
(λn.λf.λx.f (n f x)) ((λn.λf.λx.f (n f x)) ((λn.λf.λx.f (n f x)) (λf.λx.x))) foo bar
(λf.λx.f ((λn.λf.λx.f (n f x)) ((λn.λf.λx.f (n f x)) (λf.λx.x)) f x)) foo bar
(λx.foo ((λn.λf.λx.f (n f x)) ((λn.λf.λx.f (n f x)) (λf.λx.x)) foo x)) bar
foo ((λn.λf.λx.f (n f x)) ((λn.λf.λx.f (n f x)) (λf.λx.x)) foo bar)
foo ((λf.λx.f ((λn.λf.λx.f (n f x)) (λf.λx.x) f x)) foo bar)
foo ((λx.foo ((λn.λf.λx.f (n f x)) (λf.λx.x) foo x)) bar)
foo (foo ((λn.λf.λx.f (n f x)) (λf.λx.x) foo bar))
foo (foo ((λf.λx.f ((λf.λx.x) f x)) foo bar))
foo (foo ((λx.foo ((λf.λx.x) foo x)) bar))
foo (foo (foo ((λf.λx.x) foo bar)))
foo (foo (foo ((λx.x) bar)))
foo (foo (foo bar))

(s (s (s 0)))
(λn.λf.λx.f (n f x)) ((λn.λf.λx.f (n f x)) ((λn.λf.λx.f (n f x)) (λf.λx.x)))
λf.λx.f ((λn.λf.λx.f (n f x)) ((λn.λf.λx.f (n f x)) (λf.λx.x)) f x)
λf.λx.f ((λf.λx.f ((λn.λf.λx.f (n f x)) (λf.λx.x) f x)) f x)
λf.λx.f ((λx.f ((λn.λf.λx.f (n f x)) (λf.λx.x) f x)) x)
λf.λx.f (f ((λn.λf.λx.f (n f x)) (λf.λx.x) f x))
λf.λx.f (f ((λf.λx.f ((λf.λx.x) f x)) f x))
λf.λx.f (f ((λx.f ((λf.λx.x) f x)) x))
λf.λx.f (f (f ((λf.λx.x) f x)))
λf.λx.f (f (f ((λx.x) x)))
λf.λx.f (f (f x))


----
In fact, a data structure can be faithfully represented by -- is isomorphic to -- its right fold. For example, the entire list processing library, from head and tail to drop and take and even zipWith can be written entirely in terms of foldr.
http://okmij.org/ftp/Haskell/AlgorithmsH1.html#foldl
----
constructors and that then:
0 : nat
0 := λf.λx.x
s : nat -> nat
s := λn.λf.λx.f (n f x)

and then
fold thing : (a -> a) -> a -> a
e.g. if we pass in a nat to replace 0, we must pass in a nat -> nat to replace s
     if we pass in a (nat -> nat) -> nat for 0, we must do ((nat -> nat) -> nat) -> ((nat -> nat) -> nat) for s
     etc

id := λx.x
(s (s (s 0))) id 0
(λn.λf.λx.f (n f x)) ((λn.λf.λx.f (n f x)) ((λn.λf.λx.f (n f x)) (λf.λx.x))) (λx.x) (λf.λx.x)
(λf.λx.f ((λn.λf.λx.f (n f x)) ((λn.λf.λx.f (n f x)) (λf.λx.x)) f x)) (λx.x) (λf.λx.x)
(λx.(λx.x) ((λn.λf.λx.f (n f x)) ((λn.λf.λx.f (n f x)) (λf.λx.x)) (λx.x) x)) (λf.λx.x)
(λx.x) ((λn.λf.λx.f (n f x)) ((λn.λf.λx.f (n f x)) (λf.λx.x)) (λx.x) (λf.λx.x))
(λn.λf.λx.f (n f x)) ((λn.λf.λx.f (n f x)) (λf.λx.x)) (λx.x) (λf.λx.x)
(λf.λx.f ((λn.λf.λx.f (n f x)) (λf.λx.x) f x)) (λx.x) (λf.λx.x)
(λx.(λx.x) ((λn.λf.λx.f (n f x)) (λf.λx.x) (λx.x) x)) (λf.λx.x)
(λx.x) ((λn.λf.λx.f (n f x)) (λf.λx.x) (λx.x) (λf.λx.x))
(λn.λf.λx.f (n f x)) (λf.λx.x) (λx.x) (λf.λx.x)
(λf.λx.f ((λf.λx.x) f x)) (λx.x) (λf.λx.x)
(λx.(λx.x) ((λf.λx.x) (λx.x) x)) (λf.λx.x)
(λx.x) ((λf.λx.x) (λx.x) (λf.λx.x))
(λf.λx.x) (λx.x) (λf.λx.x)
(λx.x) (λf.λx.x)
λf.λx.x

s (s (s 0)) s -1

Peano axiom 7: For every natural number n, S(n) = 0 is false. That is, there is no natural number whose successor is 0.
----
s foo
foo s

z_repl : (nat -> nat) -> nat
z_repl := λ_.0

s_repl : ((nat -> nat) -> nat) -> ((nat -> nat) -> nat)
s_repl := λg.λh.h (g s)

s_repl (s_repl (s_repl z_repl))


pred := λn.(n s_repl z_repl) id

pred (s (s (s (s 0))))
(λn.n (λg.λh.h (g (λn.λf.λx.f (n f x)))) (λ_.λf.λx.x) (λx.x)) ((λn.λf.λx.f (n f x)) ((λn.λf.λx.f (n f x)) ((λn.λf.λx.f (n f x)) ((λn.λf.λx.f (n f x)) (λf.λx.x)))))
(λn.λf.λx.f (n f x)) ((λn.λf.λx.f (n f x)) ((λn.λf.λx.f (n f x)) ((λn.λf.λx.f (n f x)) (λf.λx.x)))) (λg.λh.h (g (λn.λf.λx.f (n f x)))) (λ_.λf.λx.x) (λx.x)
(λf.λx.f ((λn.λf.λx.f (n f x)) ((λn.λf.λx.f (n f x)) ((λn.λf.λx.f (n f x)) (λf.λx.x))) f x)) (λg.λh.h (g (λn.λf.λx.f (n f x)))) (λ_.λf.λx.x) (λx.x)
(λx.(λg.λh.h (g (λn.λf.λx.f (n f x)))) ((λn.λf.λx.f (n f x)) ((λn.λf.λx.f (n f x)) ((λn.λf.λx.f (n f x)) (λf.λx.x))) (λg.λh.h (g (λn.λf.λx.f (n f x)))) x)) (λ_.λf.λx.x) (λx.x)
(λg.λh.h (g (λn.λf.λx.f (n f x)))) ((λn.λf.λx.f (n f x)) ((λn.λf.λx.f (n f x)) ((λn.λf.λx.f (n f x)) (λf.λx.x))) (λg.λh.h (g (λn.λf.λx.f (n f x)))) (λ_.λf.λx.x)) (λx.x)
(λh.h ((λn.λf.λx.f (n f x)) ((λn.λf.λx.f (n f x)) ((λn.λf.λx.f (n f x)) (λf.λx.x))) (λg.λh.h (g (λn.λf.λx.f (n f x)))) (λ_.λf.λx.x) (λn.λf.λx.f (n f x)))) (λx.x)
(λx.x) ((λn.λf.λx.f (n f x)) ((λn.λf.λx.f (n f x)) ((λn.λf.λx.f (n f x)) (λf.λx.x))) (λg.λh.h (g (λn.λf.λx.f (n f x)))) (λ_.λf.λx.x) (λn.λf.λx.f (n f x)))
(λn.λf.λx.f (n f x)) ((λn.λf.λx.f (n f x)) ((λn.λf.λx.f (n f x)) (λf.λx.x))) (λg.λh.h (g (λn.λf.λx.f (n f x)))) (λ_.λf.λx.x) (λn.λf.λx.f (n f x))
(λf.λx.f ((λn.λf.λx.f (n f x)) ((λn.λf.λx.f (n f x)) (λf.λx.x)) f x)) (λg.λh.h (g (λn.λf.λx.f (n f x)))) (λ_.λf.λx.x) (λn.λf.λx.f (n f x))
(λx.(λg.λh.h (g (λn.λf.λx.f (n f x)))) ((λn.λf.λx.f (n f x)) ((λn.λf.λx.f (n f x)) (λf.λx.x)) (λg.λh.h (g (λn.λf.λx.f (n f x)))) x)) (λ_.λf.λx.x) (λn.λf.λx.f (n f x))
(λg.λh.h (g (λn.λf.λx.f (n f x)))) ((λn.λf.λx.f (n f x)) ((λn.λf.λx.f (n f x)) (λf.λx.x)) (λg.λh.h (g (λn.λf.λx.f (n f x)))) (λ_.λf.λx.x)) (λn.λf.λx.f (n f x))
(λh.h ((λn.λf.λx.f (n f x)) ((λn.λf.λx.f (n f x)) (λf.λx.x)) (λg.λh.h (g (λn.λf.λx.f (n f x)))) (λ_.λf.λx.x) (λn.λf.λx.f (n f x)))) (λn.λf.λx.f (n f x))
(λn.λf.λx.f (n f x)) ((λn.λf.λx.f (n f x)) ((λn.λf.λx.f (n f x)) (λf.λx.x)) (λg.λh.h (g (λn.λf.λx.f (n f x)))) (λ_.λf.λx.x) (λn.λf.λx.f (n f x)))
λf.λx.f ((λn.λf.λx.f (n f x)) ((λn.λf.λx.f (n f x)) (λf.λx.x)) (λg.λh.h (g (λn.λf.λx.f (n f x)))) (λ_.λf.λx.x) (λn.λf.λx.f (n f x)) f x)
λf.λx.f ((λf.λx.f ((λn.λf.λx.f (n f x)) (λf.λx.x) f x)) (λg.λh.h (g (λn.λf.λx.f (n f x)))) (λ_.λf.λx.x) (λn.λf.λx.f (n f x)) f x)
λf.λx.f ((λx.(λg.λh.h (g (λn.λf.λx.f (n f x)))) ((λn.λf.λx.f (n f x)) (λf.λx.x) (λg.λh.h (g (λn.λf.λx.f (n f x)))) x)) (λ_.λf.λx.x) (λn.λf.λx.f (n f x)) f x)
λf.λx.f ((λg.λh.h (g (λn.λf.λx.f (n f x)))) ((λn.λf.λx.f (n f x)) (λf.λx.x) (λg.λh.h (g (λn.λf.λx.f (n f x)))) (λ_.λf.λx.x)) (λn.λf.λx.f (n f x)) f x)
λf.λx.f ((λh.h ((λn.λf.λx.f (n f x)) (λf.λx.x) (λg.λh.h (g (λn.λf.λx.f (n f x)))) (λ_.λf.λx.x) (λn.λf.λx.f (n f x)))) (λn.λf.λx.f (n f x)) f x)
λf.λx.f ((λn.λf.λx.f (n f x)) ((λn.λf.λx.f (n f x)) (λf.λx.x) (λg.λh.h (g (λn.λf.λx.f (n f x)))) (λ_.λf.λx.x) (λn.λf.λx.f (n f x))) f x)
λf.λx.f ((λf.λx.f ((λn.λf.λx.f (n f x)) (λf.λx.x) (λg.λh.h (g (λn.λf.λx.f (n f x)))) (λ_.λf.λx.x) (λn.λf.λx.f (n f x)) f x)) f x)
λf.λx.f ((λx.f ((λn.λf.λx.f (n f x)) (λf.λx.x) (λg.λh.h (g (λn.λf.λx.f (n f x)))) (λ_.λf.λx.x) (λn.λf.λx.f (n f x)) f x)) x)
λf.λx.f (f ((λn.λf.λx.f (n f x)) (λf.λx.x) (λg.λh.h (g (λn.λf.λx.f (n f x)))) (λ_.λf.λx.x) (λn.λf.λx.f (n f x)) f x))
λf.λx.f (f ((λf.λx.f ((λf.λx.x) f x)) (λg.λh.h (g (λn.λf.λx.f (n f x)))) (λ_.λf.λx.x) (λn.λf.λx.f (n f x)) f x))
λf.λx.f (f ((λx.(λg.λh.h (g (λn.λf.λx.f (n f x)))) ((λf.λx.x) (λg.λh.h (g (λn.λf.λx.f (n f x)))) x)) (λ_.λf.λx.x) (λn.λf.λx.f (n f x)) f x))
λf.λx.f (f ((λg.λh.h (g (λn.λf.λx.f (n f x)))) ((λf.λx.x) (λg.λh.h (g (λn.λf.λx.f (n f x)))) (λ_.λf.λx.x)) (λn.λf.λx.f (n f x)) f x))
λf.λx.f (f ((λh.h ((λf.λx.x) (λg.λh.h (g (λn.λf.λx.f (n f x)))) (λ_.λf.λx.x) (λn.λf.λx.f (n f x)))) (λn.λf.λx.f (n f x)) f x))
λf.λx.f (f ((λn.λf.λx.f (n f x)) ((λf.λx.x) (λg.λh.h (g (λn.λf.λx.f (n f x)))) (λ_.λf.λx.x) (λn.λf.λx.f (n f x))) f x))
λf.λx.f (f ((λf.λx.f ((λf.λx.x) (λg.λh.h (g (λn.λf.λx.f (n f x)))) (λ_.λf.λx.x) (λn.λf.λx.f (n f x)) f x)) f x))
λf.λx.f (f ((λx.f ((λf.λx.x) (λg.λh.h (g (λn.λf.λx.f (n f x)))) (λ_.λf.λx.x) (λn.λf.λx.f (n f x)) f x)) x))
λf.λx.f (f (f ((λf.λx.x) (λg.λh.h (g (λn.λf.λx.f (n f x)))) (λ_.λf.λx.x) (λn.λf.λx.f (n f x)) f x)))
λf.λx.f (f (f ((λx.x) (λ_.λf.λx.x) (λn.λf.λx.f (n f x)) f x)))
λf.λx.f (f (f ((λ_.λf.λx.x) (λn.λf.λx.f (n f x)) f x)))
λf.λx.f (f (f ((λf.λx.x) f x)))
λf.λx.f (f (f ((λx.x) x)))
λf.λx.f (f (f x))

nil foo bar => bar

(cons 1 (cons 2 nil)) foo bar => foo 1 (foo 2 bar)

nil := λc.λn.n

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

cons := λh.λt.λc.λn.c h (t c n)

(cons t1 (cons t2 (cons t3 nil))) foo bar
foo t1 (foo t2 (foo t3 bar))

append := λa.λb.a cons b

alist := cons t1 (cons t2 nil)

append alist alist
(λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) ((λh.λt.λc.λn.c h (t c n)) t1 ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n))) ((λh.λt.λc.λn.c h (t c n)) t1 ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n)))
(λb.(λh.λt.λc.λn.c h (t c n)) t1 ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n)) (λh.λt.λc.λn.c h (t c n)) b) ((λh.λt.λc.λn.c h (t c n)) t1 ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n)))
(λh.λt.λc.λn.c h (t c n)) t1 ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n)) (λh.λt.λc.λn.c h (t c n)) ((λh.λt.λc.λn.c h (t c n)) t1 ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n)))
(λt.λc.λn.c t1 (t c n)) ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n)) (λh.λt.λc.λn.c h (t c n)) ((λh.λt.λc.λn.c h (t c n)) t1 ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n)))
(λc.λn.c t1 ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n) c n)) (λh.λt.λc.λn.c h (t c n)) ((λh.λt.λc.λn.c h (t c n)) t1 ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n)))
(λn.(λh.λt.λc.λn.c h (t c n)) t1 ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n) (λh.λt.λc.λn.c h (t c n)) n)) ((λh.λt.λc.λn.c h (t c n)) t1 ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n)))
(λh.λt.λc.λn.c h (t c n)) t1 ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n) (λh.λt.λc.λn.c h (t c n)) ((λh.λt.λc.λn.c h (t c n)) t1 ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n))))
(λt.λc.λn.c t1 (t c n)) ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n) (λh.λt.λc.λn.c h (t c n)) ((λh.λt.λc.λn.c h (t c n)) t1 ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n))))
λc.λn.c t1 ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n) (λh.λt.λc.λn.c h (t c n)) ((λh.λt.λc.λn.c h (t c n)) t1 ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n))) c n)
λc.λn.c t1 ((λt.λc.λn.c t2 (t c n)) (λc.λn.n) (λh.λt.λc.λn.c h (t c n)) ((λh.λt.λc.λn.c h (t c n)) t1 ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n))) c n)
λc.λn.c t1 ((λc.λn.c t2 ((λc.λn.n) c n)) (λh.λt.λc.λn.c h (t c n)) ((λh.λt.λc.λn.c h (t c n)) t1 ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n))) c n)
λc.λn.c t1 ((λn.(λh.λt.λc.λn.c h (t c n)) t2 ((λc.λn.n) (λh.λt.λc.λn.c h (t c n)) n)) ((λh.λt.λc.λn.c h (t c n)) t1 ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n))) c n)
λc.λn.c t1 ((λh.λt.λc.λn.c h (t c n)) t2 ((λc.λn.n) (λh.λt.λc.λn.c h (t c n)) ((λh.λt.λc.λn.c h (t c n)) t1 ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n)))) c n)
λc.λn.c t1 ((λt.λc.λn.c t2 (t c n)) ((λc.λn.n) (λh.λt.λc.λn.c h (t c n)) ((λh.λt.λc.λn.c h (t c n)) t1 ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n)))) c n)
λc.λn.c t1 ((λc.λn.c t2 ((λc.λn.n) (λh.λt.λc.λn.c h (t c n)) ((λh.λt.λc.λn.c h (t c n)) t1 ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n))) c n)) c n)
λc.λn.c t1 ((λn.c t2 ((λc.λn.n) (λh.λt.λc.λn.c h (t c n)) ((λh.λt.λc.λn.c h (t c n)) t1 ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n))) c n)) n)
λc.λn.c t1 (c t2 ((λc.λn.n) (λh.λt.λc.λn.c h (t c n)) ((λh.λt.λc.λn.c h (t c n)) t1 ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n))) c n))
λc.λn.c t1 (c t2 ((λn.n) ((λh.λt.λc.λn.c h (t c n)) t1 ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n))) c n))
λc.λn.c t1 (c t2 ((λh.λt.λc.λn.c h (t c n)) t1 ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n)) c n))
λc.λn.c t1 (c t2 ((λt.λc.λn.c t1 (t c n)) ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n)) c n))
λc.λn.c t1 (c t2 ((λc.λn.c t1 ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n) c n)) c n))
λc.λn.c t1 (c t2 ((λn.c t1 ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n) c n)) n))
λc.λn.c t1 (c t2 (c t1 ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n) c n)))
λc.λn.c t1 (c t2 (c t1 ((λt.λc.λn.c t2 (t c n)) (λc.λn.n) c n)))
λc.λn.c t1 (c t2 (c t1 ((λc.λn.c t2 ((λc.λn.n) c n)) c n)))
λc.λn.c t1 (c t2 (c t1 ((λn.c t2 ((λc.λn.n) c n)) n)))
λc.λn.c t1 (c t2 (c t1 (c t2 ((λc.λn.n) c n))))
λc.λn.c t1 (c t2 (c t1 (c t2 ((λn.n) n))))
λc.λn.c t1 (c t2 (c t1 (c t2 n)))

map := λf.λl.l (λh.λt.cons (f h) t) nil

useful := λx.cons x (cons x nil)

map useful alist
(λf.λl.l (λh.λt.(λh.λt.λc.λn.c h (t c n)) (f h) t) (λc.λn.n)) (λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) ((λh.λt.λc.λn.c h (t c n)) t1 ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n)))
(λl.l (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n)) ((λh.λt.λc.λn.c h (t c n)) t1 ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n)))
(λh.λt.λc.λn.c h (t c n)) t1 ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n)) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n)
(λt.λc.λn.c t1 (t c n)) ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n)) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n)
(λc.λn.c t1 ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n) c n)) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n)
(λn.(λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) t1 ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) n)) (λc.λn.n)
(λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) t1 ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n))
(λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) t1) t) ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n))
(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) t1) ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n))
(λt.λc.λn.c ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) t1) (t c n)) ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n))
λc.λn.c ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) t1) ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) c n)
λc.λn.c ((λh.λt.λc.λn.c h (t c n)) t1 ((λh.λt.λc.λn.c h (t c n)) t1 (λc.λn.n))) ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) c n)
λc.λn.c ((λt.λc.λn.c t1 (t c n)) ((λh.λt.λc.λn.c h (t c n)) t1 (λc.λn.n))) ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) c n)
λc.λn.c (λc.λn.c t1 ((λh.λt.λc.λn.c h (t c n)) t1 (λc.λn.n) c n)) ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) c n)
λc.λn.c (λc.λn.c t1 ((λt.λc.λn.c t1 (t c n)) (λc.λn.n) c n)) ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) c n)
λc.λn.c (λc.λn.c t1 ((λc.λn.c t1 ((λc.λn.n) c n)) c n)) ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) c n)
λc.λn.c (λc.λn.c t1 ((λn.c t1 ((λc.λn.n) c n)) n)) ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) c n)
λc.λn.c (λc.λn.c t1 (c t1 ((λc.λn.n) c n))) ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) c n)
λc.λn.c (λc.λn.c t1 (c t1 ((λn.n) n))) ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) c n)
λc.λn.c (λc.λn.c t1 (c t1 n)) ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) c n)
λc.λn.c (λc.λn.c t1 (c t1 n)) ((λt.λc.λn.c t2 (t c n)) (λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) c n)
λc.λn.c (λc.λn.c t1 (c t1 n)) ((λc.λn.c t2 ((λc.λn.n) c n)) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) c n)
λc.λn.c (λc.λn.c t1 (c t1 n)) ((λn.(λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) t2 ((λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) n)) (λc.λn.n) c n)
λc.λn.c (λc.λn.c t1 (c t1 n)) ((λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) t2 ((λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n)) c n)
λc.λn.c (λc.λn.c t1 (c t1 n)) ((λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) t2) t) ((λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n)) c n)
λc.λn.c (λc.λn.c t1 (c t1 n)) ((λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) t2) ((λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n)) c n)
λc.λn.c (λc.λn.c t1 (c t1 n)) ((λt.λc.λn.c ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) t2) (t c n)) ((λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n)) c n)
λc.λn.c (λc.λn.c t1 (c t1 n)) ((λc.λn.c ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) t2) ((λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) c n)) c n)
λc.λn.c (λc.λn.c t1 (c t1 n)) ((λn.c ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) t2) ((λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) c n)) n)
λc.λn.c (λc.λn.c t1 (c t1 n)) (c ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) t2) ((λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) c n))
λc.λn.c (λc.λn.c t1 (c t1 n)) (c ((λh.λt.λc.λn.c h (t c n)) t2 ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n))) ((λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) c n))
λc.λn.c (λc.λn.c t1 (c t1 n)) (c ((λt.λc.λn.c t2 (t c n)) ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n))) ((λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) c n))
λc.λn.c (λc.λn.c t1 (c t1 n)) (c (λc.λn.c t2 ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n) c n)) ((λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) c n))
λc.λn.c (λc.λn.c t1 (c t1 n)) (c (λc.λn.c t2 ((λt.λc.λn.c t2 (t c n)) (λc.λn.n) c n)) ((λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) c n))
λc.λn.c (λc.λn.c t1 (c t1 n)) (c (λc.λn.c t2 ((λc.λn.c t2 ((λc.λn.n) c n)) c n)) ((λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) c n))
λc.λn.c (λc.λn.c t1 (c t1 n)) (c (λc.λn.c t2 ((λn.c t2 ((λc.λn.n) c n)) n)) ((λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) c n))
λc.λn.c (λc.λn.c t1 (c t1 n)) (c (λc.λn.c t2 (c t2 ((λc.λn.n) c n))) ((λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) c n))
λc.λn.c (λc.λn.c t1 (c t1 n)) (c (λc.λn.c t2 (c t2 ((λn.n) n))) ((λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) c n))
λc.λn.c (λc.λn.c t1 (c t1 n)) (c (λc.λn.c t2 (c t2 n)) ((λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) c n))
λc.λn.c (λc.λn.c t1 (c t1 n)) (c (λc.λn.c t2 (c t2 n)) ((λn.n) (λc.λn.n) c n))
λc.λn.c (λc.λn.c t1 (c t1 n)) (c (λc.λn.c t2 (c t2 n)) ((λc.λn.n) c n))
λc.λn.c (λc.λn.c t1 (c t1 n)) (c (λc.λn.c t2 (c t2 n)) ((λn.n) n))


flat := λl.l append nil

flat (λc.λn.c (λc.λn.c t1 (c t1 n)) (c (λc.λn.c t2 (c t2 n)) n))
(λl.l (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n)) (λc.λn.c (λc.λn.c t1 (c t1 n)) (c (λc.λn.c t2 (c t2 n)) n))
(λc.λn.c (λc.λn.c t1 (c t1 n)) (c (λc.λn.c t2 (c t2 n)) n)) (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n)
(λn.(λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.c t1 (c t1 n)) ((λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.c t2 (c t2 n)) n)) (λc.λn.n)
(λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.c t1 (c t1 n)) ((λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.c t2 (c t2 n)) (λc.λn.n))
(λb.(λc.λn.c t1 (c t1 n)) (λh.λt.λc.λn.c h (t c n)) b) ((λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.c t2 (c t2 n)) (λc.λn.n))
(λc.λn.c t1 (c t1 n)) (λh.λt.λc.λn.c h (t c n)) ((λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.c t2 (c t2 n)) (λc.λn.n))
(λn.(λh.λt.λc.λn.c h (t c n)) t1 ((λh.λt.λc.λn.c h (t c n)) t1 n)) ((λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.c t2 (c t2 n)) (λc.λn.n))
(λh.λt.λc.λn.c h (t c n)) t1 ((λh.λt.λc.λn.c h (t c n)) t1 ((λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.c t2 (c t2 n)) (λc.λn.n)))
(λt.λc.λn.c t1 (t c n)) ((λh.λt.λc.λn.c h (t c n)) t1 ((λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.c t2 (c t2 n)) (λc.λn.n)))
λc.λn.c t1 ((λh.λt.λc.λn.c h (t c n)) t1 ((λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.c t2 (c t2 n)) (λc.λn.n)) c n)
λc.λn.c t1 ((λt.λc.λn.c t1 (t c n)) ((λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.c t2 (c t2 n)) (λc.λn.n)) c n)
λc.λn.c t1 ((λc.λn.c t1 ((λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.c t2 (c t2 n)) (λc.λn.n) c n)) c n)
λc.λn.c t1 ((λn.c t1 ((λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.c t2 (c t2 n)) (λc.λn.n) c n)) n)
λc.λn.c t1 (c t1 ((λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.c t2 (c t2 n)) (λc.λn.n) c n))
λc.λn.c t1 (c t1 ((λb.(λc.λn.c t2 (c t2 n)) (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n) c n))
λc.λn.c t1 (c t1 ((λc.λn.c t2 (c t2 n)) (λh.λt.λc.λn.c h (t c n)) (λc.λn.n) c n))
λc.λn.c t1 (c t1 ((λn.(λh.λt.λc.λn.c h (t c n)) t2 ((λh.λt.λc.λn.c h (t c n)) t2 n)) (λc.λn.n) c n))
λc.λn.c t1 (c t1 ((λh.λt.λc.λn.c h (t c n)) t2 ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n)) c n))
λc.λn.c t1 (c t1 ((λt.λc.λn.c t2 (t c n)) ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n)) c n))
λc.λn.c t1 (c t1 ((λc.λn.c t2 ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n) c n)) c n))
λc.λn.c t1 (c t1 ((λn.c t2 ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n) c n)) n))
λc.λn.c t1 (c t1 (c t2 ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n) c n)))
λc.λn.c t1 (c t1 (c t2 ((λt.λc.λn.c t2 (t c n)) (λc.λn.n) c n)))
λc.λn.c t1 (c t1 (c t2 ((λc.λn.c t2 ((λc.λn.n) c n)) c n)))
λc.λn.c t1 (c t1 (c t2 ((λn.c t2 ((λc.λn.n) c n)) n)))
λc.λn.c t1 (c t1 (c t2 (c t2 ((λc.λn.n) c n))))
λc.λn.c t1 (c t1 (c t2 (c t2 ((λn.n) n))))
λc.λn.c t1 (c t1 (c t2 (c t2 n)))

flatmap := λf.λl.flat (map f l)

flatmap useful alist
(λf.λl.(λl.l (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n)) ((λf.λl.l (λh.λt.(λh.λt.λc.λn.c h (t c n)) (f h) t) (λc.λn.n)) f l)) (λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) ((λh.λt.λc.λn.c h (t c n)) t1 ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n)))
(λl.(λl.l (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n)) ((λf.λl.l (λh.λt.(λh.λt.λc.λn.c h (t c n)) (f h) t) (λc.λn.n)) (λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) l)) ((λh.λt.λc.λn.c h (t c n)) t1 ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n)))
(λl.l (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n)) ((λf.λl.l (λh.λt.(λh.λt.λc.λn.c h (t c n)) (f h) t) (λc.λn.n)) (λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) ((λh.λt.λc.λn.c h (t c n)) t1 ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n))))
(λf.λl.l (λh.λt.(λh.λt.λc.λn.c h (t c n)) (f h) t) (λc.λn.n)) (λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) ((λh.λt.λc.λn.c h (t c n)) t1 ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n))) (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n)
(λl.l (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n)) ((λh.λt.λc.λn.c h (t c n)) t1 ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n))) (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n)
(λh.λt.λc.λn.c h (t c n)) t1 ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n)) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n)
(λt.λc.λn.c t1 (t c n)) ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n)) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n)
(λc.λn.c t1 ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n) c n)) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n)
(λn.(λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) t1 ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) n)) (λc.λn.n) (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n)
(λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) t1 ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n)) (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n)
(λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) t1) t) ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n)) (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n)
(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) t1) ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n)) (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n)
(λt.λc.λn.c ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) t1) (t c n)) ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n)) (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n)
(λc.λn.c ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) t1) ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) c n)) (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n)
(λn.(λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) t1) ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) n)) (λc.λn.n)
(λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) t1) ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n))
(λb.(λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) t1 (λh.λt.λc.λn.c h (t c n)) b) ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n))
(λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) t1 (λh.λt.λc.λn.c h (t c n)) ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n))
(λh.λt.λc.λn.c h (t c n)) t1 ((λh.λt.λc.λn.c h (t c n)) t1 (λc.λn.n)) (λh.λt.λc.λn.c h (t c n)) ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n))
(λt.λc.λn.c t1 (t c n)) ((λh.λt.λc.λn.c h (t c n)) t1 (λc.λn.n)) (λh.λt.λc.λn.c h (t c n)) ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n))
(λc.λn.c t1 ((λh.λt.λc.λn.c h (t c n)) t1 (λc.λn.n) c n)) (λh.λt.λc.λn.c h (t c n)) ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n))
(λn.(λh.λt.λc.λn.c h (t c n)) t1 ((λh.λt.λc.λn.c h (t c n)) t1 (λc.λn.n) (λh.λt.λc.λn.c h (t c n)) n)) ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n))
(λh.λt.λc.λn.c h (t c n)) t1 ((λh.λt.λc.λn.c h (t c n)) t1 (λc.λn.n) (λh.λt.λc.λn.c h (t c n)) ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n)))
(λt.λc.λn.c t1 (t c n)) ((λh.λt.λc.λn.c h (t c n)) t1 (λc.λn.n) (λh.λt.λc.λn.c h (t c n)) ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n)))
λc.λn.c t1 ((λh.λt.λc.λn.c h (t c n)) t1 (λc.λn.n) (λh.λt.λc.λn.c h (t c n)) ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n)) c n)
λc.λn.c t1 ((λt.λc.λn.c t1 (t c n)) (λc.λn.n) (λh.λt.λc.λn.c h (t c n)) ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n)) c n)
λc.λn.c t1 ((λc.λn.c t1 ((λc.λn.n) c n)) (λh.λt.λc.λn.c h (t c n)) ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n)) c n)
λc.λn.c t1 ((λn.(λh.λt.λc.λn.c h (t c n)) t1 ((λc.λn.n) (λh.λt.λc.λn.c h (t c n)) n)) ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n)) c n)
λc.λn.c t1 ((λh.λt.λc.λn.c h (t c n)) t1 ((λc.λn.n) (λh.λt.λc.λn.c h (t c n)) ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n))) c n)
λc.λn.c t1 ((λt.λc.λn.c t1 (t c n)) ((λc.λn.n) (λh.λt.λc.λn.c h (t c n)) ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n))) c n)
λc.λn.c t1 ((λc.λn.c t1 ((λc.λn.n) (λh.λt.λc.λn.c h (t c n)) ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n)) c n)) c n)
λc.λn.c t1 ((λn.c t1 ((λc.λn.n) (λh.λt.λc.λn.c h (t c n)) ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n)) c n)) n)
λc.λn.c t1 (c t1 ((λc.λn.n) (λh.λt.λc.λn.c h (t c n)) ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n)) c n))
λc.λn.c t1 (c t1 ((λn.n) ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n)) c n))
λc.λn.c t1 (c t1 ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n) c n))
λc.λn.c t1 (c t1 ((λt.λc.λn.c t2 (t c n)) (λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n) c n))
λc.λn.c t1 (c t1 ((λc.λn.c t2 ((λc.λn.n) c n)) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n) c n))
λc.λn.c t1 (c t1 ((λn.(λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) t2 ((λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) n)) (λc.λn.n) (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n) c n))
λc.λn.c t1 (c t1 ((λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) t2 ((λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n)) (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n) c n))
λc.λn.c t1 (c t1 ((λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) t2) t) ((λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n)) (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n) c n))
λc.λn.c t1 (c t1 ((λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) t2) ((λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n)) (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n) c n))
λc.λn.c t1 (c t1 ((λt.λc.λn.c ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) t2) (t c n)) ((λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n)) (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n) c n))
λc.λn.c t1 (c t1 ((λc.λn.c ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) t2) ((λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) c n)) (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n) c n))
λc.λn.c t1 (c t1 ((λn.(λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) t2) ((λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) n)) (λc.λn.n) c n))
λc.λn.c t1 (c t1 ((λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) t2) ((λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n)) c n))
λc.λn.c t1 (c t1 ((λb.(λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) t2 (λh.λt.λc.λn.c h (t c n)) b) ((λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n)) c n))
λc.λn.c t1 (c t1 ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) t2 (λh.λt.λc.λn.c h (t c n)) ((λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n)) c n))
λc.λn.c t1 (c t1 ((λh.λt.λc.λn.c h (t c n)) t2 ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n)) (λh.λt.λc.λn.c h (t c n)) ((λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n)) c n))
λc.λn.c t1 (c t1 ((λt.λc.λn.c t2 (t c n)) ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n)) (λh.λt.λc.λn.c h (t c n)) ((λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n)) c n))
λc.λn.c t1 (c t1 ((λc.λn.c t2 ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n) c n)) (λh.λt.λc.λn.c h (t c n)) ((λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n)) c n))
λc.λn.c t1 (c t1 ((λn.(λh.λt.λc.λn.c h (t c n)) t2 ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n) (λh.λt.λc.λn.c h (t c n)) n)) ((λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n)) c n))
λc.λn.c t1 (c t1 ((λh.λt.λc.λn.c h (t c n)) t2 ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n) (λh.λt.λc.λn.c h (t c n)) ((λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n))) c n))
λc.λn.c t1 (c t1 ((λt.λc.λn.c t2 (t c n)) ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n) (λh.λt.λc.λn.c h (t c n)) ((λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n))) c n))
λc.λn.c t1 (c t1 ((λc.λn.c t2 ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n) (λh.λt.λc.λn.c h (t c n)) ((λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n)) c n)) c n))
λc.λn.c t1 (c t1 ((λn.c t2 ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n) (λh.λt.λc.λn.c h (t c n)) ((λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n)) c n)) n))
λc.λn.c t1 (c t1 (c t2 ((λh.λt.λc.λn.c h (t c n)) t2 (λc.λn.n) (λh.λt.λc.λn.c h (t c n)) ((λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n)) c n)))
λc.λn.c t1 (c t1 (c t2 ((λt.λc.λn.c t2 (t c n)) (λc.λn.n) (λh.λt.λc.λn.c h (t c n)) ((λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n)) c n)))
λc.λn.c t1 (c t1 (c t2 ((λc.λn.c t2 ((λc.λn.n) c n)) (λh.λt.λc.λn.c h (t c n)) ((λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n)) c n)))
λc.λn.c t1 (c t1 (c t2 ((λn.(λh.λt.λc.λn.c h (t c n)) t2 ((λc.λn.n) (λh.λt.λc.λn.c h (t c n)) n)) ((λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n)) c n)))
λc.λn.c t1 (c t1 (c t2 ((λh.λt.λc.λn.c h (t c n)) t2 ((λc.λn.n) (λh.λt.λc.λn.c h (t c n)) ((λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n))) c n)))
λc.λn.c t1 (c t1 (c t2 ((λt.λc.λn.c t2 (t c n)) ((λc.λn.n) (λh.λt.λc.λn.c h (t c n)) ((λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n))) c n)))
λc.λn.c t1 (c t1 (c t2 ((λc.λn.c t2 ((λc.λn.n) (λh.λt.λc.λn.c h (t c n)) ((λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n)) c n)) c n)))
λc.λn.c t1 (c t1 (c t2 ((λn.c t2 ((λc.λn.n) (λh.λt.λc.λn.c h (t c n)) ((λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n)) c n)) n)))
λc.λn.c t1 (c t1 (c t2 (c t2 ((λc.λn.n) (λh.λt.λc.λn.c h (t c n)) ((λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n)) c n))))
λc.λn.c t1 (c t1 (c t2 (c t2 ((λn.n) ((λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n)) c n))))
λc.λn.c t1 (c t1 (c t2 (c t2 ((λc.λn.n) (λh.λt.(λh.λt.λc.λn.c h (t c n)) ((λx.(λh.λt.λc.λn.c h (t c n)) x ((λh.λt.λc.λn.c h (t c n)) x (λc.λn.n))) h) t) (λc.λn.n) (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n) c n))))
λc.λn.c t1 (c t1 (c t2 (c t2 ((λn.n) (λc.λn.n) (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n) c n))))
λc.λn.c t1 (c t1 (c t2 (c t2 ((λc.λn.n) (λa.λb.a (λh.λt.λc.λn.c h (t c n)) b) (λc.λn.n) c n))))
λc.λn.c t1 (c t1 (c t2 (c t2 ((λn.n) (λc.λn.n) c n))))
λc.λn.c t1 (c t1 (c t2 (c t2 ((λc.λn.n) c n))))
λc.λn.c t1 (c t1 (c t2 (c t2 ((λn.n) n))))
λc.λn.c t1 (c t1 (c t2 (c t2 n)))

tail-implementation can be done like the first predecessor
i.e. "count" in pairs to drop this one
       __________________________|
      |                               
      v
   (cons 1 (cons 2 (cons 3 nil)))
=>         (cons 2 (cons 3 nil))

can keep the *first* length-1 elements by doing like second predecessor
i.e. replace nil with something that eats this one
                       ______________________|
                      |
                      v
   (cons 1 (cons 2 (cons 3 nil)))
=> (cons 1 (cons 2         nil))

----
http://llama-the-ultimate.org/lambdum/