User:Alemagno12/Translation maps for SSS: Difference between revisions
Jump to navigation
Jump to search
m
Formatting
Alemagno12 (talk | contribs) (Created page with "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), whe...") |
Alemagno12 (talk | contribs) m (Formatting) |
||
Line 6:
Define a function Prune : Term(SSS) -> Term(SSS) inductively as follows:
Define a function Shift : Term(PrSS) -> Term(PrSS) inductively as follows:
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:
| |||