(subst
	(subst
		(subst
			(subst
				((if (zero? 0) + -) 3 4)
				[
					(= (\m (\n (& (<= m n) (<= n m)))))])
			[
				(<= (\m (\n (zero? (- m n)))))])
		[
			(2 (succ 1))
			(3 (succ (succ 1)))
			(4 (succ (succ (succ 1))))
			(+ (\m(\n (m succ n))))
			(* (\m(\n(\f (m (n f))))))
			(** (\b(\e (e b))))
			(- (\m(\n (n pred m))))
			(zero? (\n ((n (\x #f)) #t)))])
	[(succ  (\n(\f(\x (f (n f x))))))
	 (pred  (\n(\f(\x(((n (\g(\h(h (g f))))) (\u x)) (\u u))))))
	 (1     (\ff(\xx (ff xx))))
	 (0     (\ff(\xx xx)))
	 (#t    (\x(\y x)))
	 (#f    (\x(\y y)))
	 (&     (\p(\q (p q p))))
	 (|     (\p(\q (p p q))))
	 (if    (\p(\a(\b (p a b)))))
	 (I     (\x x))
	 (K     (\x (\y x)))
	 (S     (\x (\y (\z ((x z) (y z))))))
	 (Y     (\f ((\x (f (x x))) (\x (f (x x))))))
	 (AY    (\f ((\x (f (\arg ((x x) arg)))) (\x (f (\arg ((x x) arg)))))))])