YCombinator= Lambda[{f}, Lambda[{x}, f[x[x]] ] [ Lambda[{x}, f[x[x]] ] ] ];
In[]:=
FunctionToApplication[s[s[k[s]][s[k[k]][s[k][k]]]][s[s[k[s]][s[k[k]][s[k][k]]]][s[s[k[s]][s[k[k]][s[k][k]]]][s[s[k[s]][s[k[k]][s[k][k]]]][s[s[k[s]][s[k[k]][s[k][k]]]][s[s[k[s]][s[k[k]][s[k][k]]]][s[s[k[s]][k[k]]][k[k]]]]]]]]]
Out[]=
s(s(ks)(s(kk)(skk)))(s(s(ks)(s(kk)(skk)))(s(s(ks)(s(kk)(skk)))(s(s(ks)(s(kk)(skk)))(s(s(ks)(s(kk)(skk)))(s(s(ks)(s(kk)(skk)))(s(s(ks)(kk))(kk)))))))
[ CR implies no critical pairs are needed ]
[ Substitution lemmas implement cached subexpression transformations ]
In[]:=
SKOuterEvolveList2[s[s[s[s]]][s][s],10]
Out[]=
{s[s[s[s]]][s][s],s[s[s]][s][s[s]],s[s][s[s]][s[s[s]]],s[s[s[s]]][s[s][s[s[s]]]],s[s[s[s]]][s[s][s[s[s]]]],s[s[s[s]]][s[s][s[s[s]]]],s[s[s[s]]][s[s][s[s[s]]]],s[s[s[s]]][s[s][s[s[s]]]],s[s[s[s]]][s[s][s[s[s]]]],s[s[s[s]]][s[s][s[s[s]]]],s[s[s[s]]][s[s][s[s[s]]]]}
In[]:=
SKOuterEvolveList2[s[s[s[s]]][s][s][s][k],10]
Out[]=
{s[s[s[s]]][s][s][s][k],s[s[s]][s][s[s]][s][k],s[s][s[s]][s[s[s]]][s][k],s[s[s[s]]][s[s][s[s[s]]]][s][k],s[s[s]][s][s[s][s[s[s]]][s]][k],s[s[s]][s][s[s][s[s[s]][s]]][k],s[s][s[s][s[s[s]][s]]][s[s[s][s[s[s]][s]]]][k],s[s[s[s][s[s[s]][s]]]][s[s][s[s[s]][s]][s[s[s][s[s[s]][s]]]]][k],s[s[s][s[s[s]][s]]][k][s[s][s[s[s]][s]][s[s[s][s[s[s]][s]]]][k]],s[s][s[s[s]][s]][s[s][s[s[s]][s]][s[s[s][s[s[s]][s]]]][k]][k[s[s][s[s[s]][s]][s[s[s][s[s[s]][s]]]][k]]],s[s][s[s[s]][s]][s[s[s[s][s[s[s]][s]]]][s[s[s]][s][s[s[s][s[s[s]][s]]]]][k]][k[s[s][s[s[s]][s]][s[s[s][s[s[s]][s]]]][k]]]}
Like adding a lemma
s[s[s[s]]][s][s][s][k]->s[s][s[s[s]][s]][s[s[s[s][s[s[s]][s]]]][s[s[s]][s][s[s[s][s[s[s]][s]]]]][k]][k[s[s][s[s[s]][s]][s[s[s][s[s[s]][s]]]][k]]]
Causal edge density heuristic for picking lemmas ....
As a thing to cache, pick the expression where there are the most possible matches......