---

Step * of Lemma sbdecode_wf_gcd

∀[L:ℕ2 List]. (sbdecode(L) ∈ {p:ℕ+ × ℕ+| let m,n = p in gcd(m;n) = 1 ∈ ℤ} )
BY
{ xxx(Auto
      THEN MemTypeCD
      THEN Auto
      THEN GenConclAtAddr [1]
      THEN D -2
      THEN Reduce 0
      THEN (ApFunToHypEquands `Z' ⌜let m,n = Z in sbcode(m;n)⌝ ⌜ℕ2 List⌝ (-1)⋅ THENA Auto)
      THEN ((RWO "sbcode-decode" (-1) THENM Reduce (-1)) THENA Auto))xxx }

1
1. L : ℕ2 List
2. v1 : ℕ+
3. v2 : ℕ+
4. sbdecode(L) = <v1, v2> ∈ (ℕ+ × ℕ+)
5. L = sbcode(v1;v2) ∈ (ℕ2 List)
⊢ gcd(v1;v2) = 1 ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[L:\mBbbN{}2  List].  (sbdecode(L)  \mmember{}  \{p:\mBbbN{}\msupplus{}  \mtimes{}  \mBbbN{}\msupplus{}|  let  m,n  =  p  in  gcd(m;n)  =  1\}  )


By

---

Latex:
xxx(Auto
        THEN  MemTypeCD
        THEN  Auto
        THEN  GenConclAtAddr  [1]
        THEN  D  -2
        THEN  Reduce  0
        THEN  (ApFunToHypEquands  `Z'  \mkleeneopen{}let  m,n  =  Z  in  sbcode(m;n)\mkleeneclose{}  \mkleeneopen{}\mBbbN{}2  List\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)
        THEN  ((RWO  "sbcode-decode"  (-1)  THENM  Reduce  (-1))  THENA  Auto))xxx

---

Home Index