!def true = \x y. x true !def TRUE = \x y. x TRUE !def FALSE = \x y. y !def IF = \x y z. x y z IF TRUE t e !trace IF TRUE t e !leftmost_innermost !help !quit !def add = \m n f x. m f (n f x) !def 2 = \f x. f (f x) !def add 2 2 add 2 2 !trace add 2 2 !def 4 = \f x.f (f (f (f x))) add 4 4 def 8 = \f x.f (f (f (f (f (f (f (f x))))))) !def 8 = \f x.f (f (f (f (f (f (f (f x))))))) add 8 8 IF T t e !def NOT = \z x y. z y x NOT T NOT F