---

Step * 1 of Lemma sbdecode_wf_gcd


1. L : ℕ2 List
2. v1 : ℕ+
3. v2 : ℕ+
4. sbdecode(L) = <v1, v2> ∈ (ℕ+ × ℕ+)
5. L = sbcode(v1;v2) ∈ (ℕ2 List)
⊢ gcd(v1;v2) = 1 ∈ ℤ
BY
{ xxx(HypSubst' (-1) (-2) THEN (RWO "sbdecode-code" (-2) THENA Auto) THEN EqHD (-2) THEN Auto THEN All Reduce)xxx }

1
1. L : ℕ2 List
2. v1 : ℕ+
3. v2 : ℕ+
4. (v1 ÷ gcd(v1;v2)) = v1 ∈ ℕ+
5. (v2 ÷ gcd(v1;v2)) = v2 ∈ ℕ+
6. L = sbcode(v1;v2) ∈ (ℕ2 List)
⊢ gcd(v1;v2) = 1 ∈ ℤ

---

Latex:

---

Latex:

1.  L  :  \mBbbN{}2  List
2.  v1  :  \mBbbN{}\msupplus{}
3.  v2  :  \mBbbN{}\msupplus{}
4.  sbdecode(L)  =  <v1,  v2>
5.  L  =  sbcode(v1;v2)
\mvdash{}  gcd(v1;v2)  =  1


By

---

Latex:
xxx(HypSubst'  (-1)  (-2)
        THEN  (RWO  "sbdecode-code"  (-2)  THENA  Auto)
        THEN  EqHD  (-2)
        THEN  Auto
        THEN  All  Reduce)xxx

---

Home Index