Skip to content

Instantly share code, notes, and snippets.

@Glorp

Glorp/flatmap14

Created May 13, 2014 19:54
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save Glorp/6ccb40722f18b19a1843 to your computer and use it in GitHub Desktop.
Save Glorp/6ccb40722f18b19a1843 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
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/
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment