---

Step * of Lemma sb-equipollent

ℕ2 List ~ {p:ℕ+ × ℕ+| let m,n = p in gcd(m;n) = 1 ∈ ℤ} 
BY
{ xxxxxx(With ⌜λL.sbdecode(L)⌝ (D 0)⋅ THEN Auto THEN RepeatFor 2 (D 0) THEN Reduce 0 THEN Auto)xxxxxx }

1
1. a1 : ℕ2 List
2. a2 : ℕ2 List
3. sbdecode(a1) = sbdecode(a2) ∈ {p:ℕ+ × ℕ+| let m,n = p in gcd(m;n) = 1 ∈ ℤ} 
⊢ a1 = a2 ∈ (ℕ2 List)

2
1. b : {p:ℕ+ × ℕ+| let m,n = p in gcd(m;n) = 1 ∈ ℤ} 
⊢ ∃a:ℕ2 List. (sbdecode(a) = b ∈ {p:ℕ+ × ℕ+| let m,n = p in gcd(m;n) = 1 ∈ ℤ} )

---

Latex:

---

Latex:
\mBbbN{}2  List  \msim{}  \{p:\mBbbN{}\msupplus{}  \mtimes{}  \mBbbN{}\msupplus{}|  let  m,n  =  p  in  gcd(m;n)  =  1\} 


By

---

Latex:
xxxxxx(With  \mkleeneopen{}\mlambda{}L.sbdecode(L)\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto  THEN  RepeatFor  2  (D  0)  THEN  Reduce  0  THEN  Auto)xxxxxx

---

Home Index