 The theorem is stated in a rather general way without specifying exactly which combinatory base or which modification of TA\(_\textrm{CL}\) is assumed, because the theorem holds for any combinatory base. Indeed, there is an algorithm that given a combinator decides if the combinator is typable, and for a typable combinator produces a type too. Of course, in the combinatorially complete base \(\{\textsf{S},\textsf{K}\}\) all the combinators are expressible as terms consisting of these two combinators only. However, this assumption is not needed for a solution of typability, though it might provide an explanation for the existence of a general algorithm.