---

Step * of Lemma sbcode-decode

∀[L:ℕ2 List]. (let m,n = sbdecode(L) in sbcode(m;n) ~ L)
BY
{ xxx(InductionOnList THEN Unfold `sbdecode` 0 THEN Reduce 0 THEN Try (Fold `sbdecode` 0))xxx }

1
sbcode(1;1) ~ []

2
1. u : ℕ2
2. v : ℕ2 List
3. let m,n = sbdecode(v) 
   in sbcode(m;n) ~ v
⊢ let m,n = let m,n = sbdecode(v) 
            in if u=0 then <m, m + n> else <m + n, n> 
  in sbcode(m;n) ~ [u / v]

---

Latex:

---

Latex:
\mforall{}[L:\mBbbN{}2  List].  (let  m,n  =  sbdecode(L)  in  sbcode(m;n)  \msim{}  L)


By

---

Latex:
xxx(InductionOnList  THEN  Unfold  `sbdecode`  0  THEN  Reduce  0  THEN  Try  (Fold  `sbdecode`  0))xxx

---

Home Index