---

Step * 1 1 of Lemma sbdecode_wf_gcd


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 ∈ ℤ
BY
{ xxx((InstLemma `gcd-positive` [⌜v2⌝;⌜v1⌝]⋅ THENA Auto)
      THEN (InstLemma `div_rem_sum` [⌜v1⌝;⌜gcd(v1;v2)⌝]⋅ THENA Auto)
      )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)
7. 0 < gcd(v1;v2)
8. v1 = (((v1 ÷ gcd(v1;v2)) * gcd(v1;v2)) + (v1 rem gcd(v1;v2))) ∈ ℤ
⊢ gcd(v1;v2) = 1 ∈ ℤ

---

Latex:

---

Latex:

1.  L  :  \mBbbN{}2  List
2.  v1  :  \mBbbN{}\msupplus{}
3.  v2  :  \mBbbN{}\msupplus{}
4.  (v1  \mdiv{}  gcd(v1;v2))  =  v1
5.  (v2  \mdiv{}  gcd(v1;v2))  =  v2
6.  L  =  sbcode(v1;v2)
\mvdash{}  gcd(v1;v2)  =  1


By

---

Latex:
xxx((InstLemma  `gcd-positive`  [\mkleeneopen{}v2\mkleeneclose{};\mkleeneopen{}v1\mkleeneclose{}]\mcdot{}  THENA  Auto)
        THEN  (InstLemma  `div\_rem\_sum`  [\mkleeneopen{}v1\mkleeneclose{};\mkleeneopen{}gcd(v1;v2)\mkleeneclose{}]\mcdot{}  THENA  Auto)
        )xxx

---

Home Index