sum (take (s (s (s (s (s z))))) (cycle (take (s (s (s z))) (filter (leq (s z)) nats)))) where
	id    = \x. x;
	force = \thunk. thunk _;
	fix   = \f. (\x. f (\y. x x y)) (\x. f (\y. x x y));

	true  = \p _. p;
	false = \_ q. q;
	or    = \p q. p p q;
	if    = id;

	z    = \_ z. z;
	s    = \n s z. s (n s z);
	eq0  = \n. n (\_. false) true;
        plus = \m n s z. m s (n s z);
	pred = \n s z. n (\g h. h (g s)) (\_. z) (\x. x);
	sub  = \n m. m pred n;
	leq  = \n m. eq0 (sub n m);

	nil     = \     _ z. z;
	cons    = \x xs f z. f (\_. x) (\f' _. xs f' z);
	consC   = \x xs f z. f  x      (\f' _. xs f' z);
	tail    = \xs f z. xs (\_ r. force (r f)) z;
	foldr   = \f z xs. xs (fix (\rec f x r. f x (r (rec f))) f) z;
	defhead = foldr (\x _. force x);
	head    = defhead _;
	null    = foldr (\_ _. false) true;

	ifNull    = \xs def f. if (null xs) def (\_. force (f xs));
	ifNullNil = \xs. ifNull xs nil;
	append    = fix (\append xs1 xs2. ifNull xs1 xs2
			(\xs1. consC (\_. head xs1) (append (tail xs1) xs2)));
	map       = fix (\map f xs. ifNullNil xs
			(\xs. consC (\_. f (head xs)) (map f (tail xs))));
	take      = fix (\take n xs. if (eq0 n) nil (ifNullNil xs
			(\xs. consC (\_. head xs) (take (pred n) (tail xs)))));
	filter    = fix (\filter p xs. ifNullNil xs
			(\xs. if (p x)
				(cons x (filter p (tail xs)))
				(filter p (tail xs))
			where x = head xs.));
	cycle     = fix (\cycle xs. \_. force (append xs (cycle xs)));

	s1foldr = \f. foldr (\x acc. f  x        (force acc));
	s2foldr = \f. foldr (\x acc. f (force x)  acc       );
	sfoldr  = \f. foldr (\x acc. f (force x) (force acc));

	nats = fix (\rec n. \_. force (cons n (rec (s n)))) z;
	sum  = sfoldr plus z.

result: \s z. s (s (s (s (s (s (s (s (s z))))))))
equals to haskell "sum $ take 5 $ cycle $ take 3 $ filter (1 <=) [0..]" --> 1 + 2 + 3 + 1 + 2 = 9