User:Alemagno12/Translation maps for SSS

Here are some translation maps between SSS and BM2.3, alongside their proofs.

For a BM2.3 or SSS expression X, o_BM2.3(X) or o_SSS(X) is the order type of all possible standard expressions below it under expansion; for BM2.3, this is guaranteed to be an ordinal by [Yto2023]. ES is the empty string/matrix, + is string/matrix concatenation, X*k = X+X+X+...+X k times for some natural number k, and > is ordering by expansion.

TODO: Prove that lexicographic ordering is equivalent to expansion for SSS. This is already proven for BM2.3 in [Yto2023]

Up to \(\varepsilon_0\)

Lemma 1. Assume that o_SSS(X) = o_BM2.3(X') and o_SSS(Y) = o_BM2.3(Y') for some standard X,X',Y,Y'. Then, o_SSS(X+(0)+Y) = o_BM2.3(X'+Y').

Proof. By induction on Y. Zero and successor cases are trivial. For the limit case, let Z < Y and o_SSS(Z) = o_BM2.3(Z').

• BM2.3 does not have any "stop at the leftmost element if you can't find the bad root" condition, so the bad root of X'+Z' is the bad root of Z', and o_BM2.3(X'+Z') = sup_n<ω(o_BM2.3(X'+exp(Z',n))).

• For SSS, if the second bad root check finds a bad root in Z, the bad root of X+(0)+Z is the bad root of Z. If it does not find a bad root, then since the first bad root must be at least (0,1) and every standard expression starts with 0, (0)+Z = (0,0)+W for some W < (0,1) <= bad root;

WIP