theorem

https://www.cambridge.org/core/journals/journal-of-symbolic-logic/article/abs/basis-result-in-combinatory-logic/306DF60857C5A842C9793FBBAA4A2970

A basis result in combinatory logic,
Remi Legrand, J. Symb. Logic 53.4 (1988), pp. 1224-1226.

Define an n-form as a lambda calculus term containing (at least) n free variables.
Define an n-bind as a term containing an n-form as well as its n binding lambdas.

Example 3-binds are combinators S, B, C, and V, which contain 3-forms
3 1 (2 1), 3 (2 1), 3 1 2, and 1 3 2 respectively in de-Bruijn notation.
Note that a closed term containing an n-form is necessarily an n-bind,
but an n-bind is not necessarily closed.

Define a 2-2-form as a 2-form containing a 2-bind and a disjoint subterm containing the 2-form variables.

An example 2-2-form is T (x y) where T is the transpose combinator \x\y.y x.
A non-example is x T y, as it has no xy subterm disjoint from T.

Call a term T deprived if contains neither a 3-form nor a 2-2-form.

For example, S,B,C, and V are not deprived, as they contain a 3-form.
All the following combinators in de-Bruijn notation are deprived:
K = \\2, W = \\2 1 1, C2 = \\2(2 1),
O = \\1(2 1), T = \\1 2, D = \1 1,
as is any composition of these.

Lemma: deprived terms only reduce to deprived terms.

Proof:
Suppose T0 is a deprived term that 1-step reduces to T1,
with redex A = (\x.M) N and reduct M[x:=N].

First suppose that T1 has a 3-form. Since the reduct has no new variables,
this 3-form must appear within the reduct. Since M and N both lack a 3-form,
this 3-form must have some variables in M and some in a substituted N.
There cannot be two of the former, or they plus x would make M contain a 3-form.
Hence there is only one 3-form variable y in M,
and two 3-form variables z1,z2 in a substituted N.
Since all 3 binding lambdas must ancestor the 3-form containing y,
and lambdas in M cannot bind variables in N, \z1 and \z2 must ancestor A.
Since A is not a 3-form, \y must be in M.
That makes \x.M a 2-bind and A a 2-form with N as disjoint subterm, a contradiction.
Thus T1 has no 3-form.

Finally, suppose that T1 has a 2-2-form T_2_2 containing 2-bind T and free variables y and z.
Since T0 contains no 2-2-form, T must be in the redex.
Variables y and z can't both be outside A, since A either contains T or a 2-bind with x.
By disjointness, neither y nor z can be outside A.
Since A has no 2-2-form, y and z can't both be in N.
They cannot both be in M either, as that implies a 3-form in M with variables x,y,z.
If y is in M and z in N, then M has a 2-2-form with T and free variables x and y.
Thus M[x:=N] has no 2-2-form either.
QED

The Lemma proves the following

Theorem: A basis for CL must contain a non-deprived  combinator.
So {K,W,C2,O,T,D} is not a basis.

Theorem: {K,W,Q} is a basis, where Q = \\\2(3 1).

Proof: {K, W, B, C} is a well-known basis, and
       B = Q(Q(Q K Q)(Q Q)) W
       C = Q Q(Q(Q(Q K Q) W)).