 Combinatorial completeness is usually proved via defining a “pseudo” \(\lambda\)-abstraction (or bracket abstraction) in CL. There are various algorithms to define a bracket abstraction operator in CL, that behaves as the \(\lambda\) operator does in a \(\lambda\)-calculus. This operator is usually denoted by \([\,]\) or by \(\lambda^*\). The algorithms differ from each other in various aspects: (i) the set of combinators they presuppose, (ii) the length of the resulting terms, (iii) whether they compose into (syntactic) identity with the algorithm that translates a combinatory term into a \(\lambda\)-term, and (iv) whether they commute with either of the reductions or equalities.