Combinator equivalent to eta conversion

In lambda calculus, one can prove that two expressions compute the same function if they are equivalent under both beta reduction and eta conversion, where eta conversion consists of eta reduction,
$$
(\lambda x.A x) \to A \qquad\text{if $x$ is not free in $A$}
$$
and eta expansion,
$$
A \to (\lambda x.Ax) \qquad\text{where $x$ is not free in $A$.}
$$
Thus, while one cannot computationally check whether two expressions compute the same function, one can computationally verify a proof that they do, if someone produces a sequence of beta reductions and eta conversions that takes one expression to the other. The reason that determining equality between expressions is undecidable has to do with the need to use eta expansions as well as contractions, so you have to backtrack to search for a proof.

My first question is: is the above characterisation correct? It seems to be from what I've read, but I haven't seen it explained in exactly that way and I might have misunderstood.

My second question is, does eta conversion exist in the combinator calculus, or is there an equivalent? In other words, is there a set of formal manipulations on combinator expressions that can be used to show that two are equivalent to one another?

As a simple example, the expressions $S\,K\,K$ and $S\,K\,S$ are equivalent. (They are both the identity function.) I can show this by explicitly evaluating both of them:
$$
(S\,K\,K)\,x = (K\,x)\,(K\,x) = x,
$$
whereas
$$
(S\,K\,S)\,x = (K\,x)\,(S\,x) = x.
$$
But this involves introducing variables (i.e. moving away from "pure" SK combinator expressions), and it doesn't proceed by starting from one expression and manipulating it to convert it into the other. Is there a set of syntactic moves that can be used to show this equivalence, analogously to eta conversions in lambda calculus?

From the Barendregt lambda calculus book, we can find theory $CL$ (combinatory logic) defined as follows

$$
K P Q = P \qquad
S P Q R = P R (Q R)
$$

where $K,S$ are constant symbols (for the well known combinators), while $P,Q,R$ range over all the possible $CL$ terms (built from $K,S$, variables and application). The relation $=$ is postulated to be a congruence.

The $CL$ theory can be extended with the following $A_\beta$ axioms:

$$
\begin{array}{ll}
A.1 & K = S(S(KS)(S(KK)K))(K(SKK)) \\
A.2 & S = S(S(KS)(S(K(S(KS)))(S(K(S(KK)))S)))(K(K(SKK))) \\
A.3 & S(S(KS)(S(KK)(S(KS)K)))(KK)=S(KK) \\
A.4 & S(KS)(S(KK)) = \\
& \qquad S(KK)(S(S(KS)(S(KK)(SKK)))(K(SKK))) \\
A.5 & S(K(S(KS)))(S(KS)(S(KS))) = \\
& \qquad S(S(KS)(S(KK)(S(KS)(S(K(S(KS)))S))))(KS)
\end{array}
$$

(I have double checked these, but I can't swear I got them right.)

Corollary 7.3.15 states that $CL\ +\ A_\beta$ is equivalent to $\lambda$ (the theory of the $\lambda$ calculus with $\beta$ conversion, but no $\eta$ or extensionality).

Hence, in principle one can use "only" the above laws to prove $SKK=SKS$.

The convenience of the above laws is self-evident, I think.

A similar set of axioms is found in the same book for $\lambda\eta = \lambda + \bf ext$. These are $A.3,A.4,A.5$ (hence no $A.1,A.2$) and

$$
\begin{array}{ll}
A.6 & S(S(KS)K)(K(SKK)) = SKK
\end{array}
$$

StackExchange Computer Science Q#57361, answer score: 5