User:Alemagno12/Translation maps for SSS

Here are some (conjectured) translation maps between SSS and BM2.3.

Term(PrSS), Term(PSS), Term(TSS), Term(SSS) are the sets of all PrSS, PSS, TSS and SSS expressions respectively. ES is the empty string/matrix, + is string/matrix concatenation, and > is lexicographic comaparison.

Up to \(\varepsilon_0\)

Define a function Prune : Term(SSS) -> Term(SSS) inductively as follows:

• Prune(ES) = ES
• Prune((A,0)) = (Prune(A),0)
• Prune((A,0,B,1)) = (Prune(A),0,B), where B >= 1
• Otherwise, Prune(A) doesn't exist.

Define a function Shift : Term(PrSS) -> Term(PrSS) inductively as follows:

• Shift(ES) = ES
• Shift((A,k)) = (Shift(A),k+1)

i.e. Shift(A) is the result of adding 1 to all the elements in A.

Define a function Map : Term(SSS) -> Term(PrSS) inductively as follows:

• Map(ES) = ES
• Map((A,0)) = (Map(A),0)
• Map((0,A)) = I'll finish this later, also maybe a more algorithmic approach would be better? E.g first turn all (0,1^k)s into (k)s, then add inbetween elements