---

Step * 2 1 of Lemma sb-equipollent


1. b1 : ℕ+
2. b2 : ℕ+
3. [%1] : gcd(b1;b2) = 1 ∈ ℤ
⊢ ∃a:ℕ2 List. (sbdecode(a) = <b1, b2> ∈ {p:ℕ+ × ℕ+| let m,n = p in gcd(m;n) = 1 ∈ ℤ} )
BY
{ xxx((With ⌜sbcode(b1;b2)⌝ (D 0)⋅ THEN Auto) THEN RWO "sbdecode-code" 0 THEN Auto THEN HypSubst' (-1) 0 THEN Auto)xxx }

---

Latex:

---

Latex:

1.  b1  :  \mBbbN{}\msupplus{}
2.  b2  :  \mBbbN{}\msupplus{}
3.  [\%1]  :  gcd(b1;b2)  =  1
\mvdash{}  \mexists{}a:\mBbbN{}2  List.  (sbdecode(a)  =  <b1,  b2>)


By

---

Latex:
xxx((With  \mkleeneopen{}sbcode(b1;b2)\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)
        THEN  RWO  "sbdecode-code"  0
        THEN  Auto
        THEN  HypSubst'  (-1)  0
        THEN  Auto)xxx

---

Home Index