A more readable form of the program is given at [1]. The tree contains all combinators built up from the single point basis A = λxλyλz. x z (y (λ_.z)), which is

A more readable form of the program is given at [1]. The tree contains all combinators built up from the single point basis A = λxλyλz. x z (y (λ_.z)), which is encoded as bit 0 (left branch), while bit 1 (right branch) encodes prefix application. [1] https://github.com/tromp/AIT/blob/master/ait/allA.lam https://github.com/tromp/AIT/blob/master/ait/allA.lam