Step
*
1
of Lemma
sbcode-decode
sbcode(1;1) ~ []
BY
{ xxx(RecUnfold `sbcode` 0 THEN Reduce 0 THEN Auto)xxx }
Latex:
Latex:
sbcode(1;1)  \msim{}  []
By
Latex:
xxx(RecUnfold  `sbcode`  0  THEN  Reduce  0  THEN  Auto)xxx
Home
Index