---

Step * 1 1 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)
7. 0 < gcd(v1;v2)
8. v1 = ((v1 * gcd(v1;v2)) + (v1 rem gcd(v1;v2))) ∈ ℤ
9. 0 ≤ (v1 rem gcd(v1;v2))
10. v1 rem gcd(v1;v2) < gcd(v1;v2)
⊢ gcd(v1;v2) = 1 ∈ ℤ
BY
{ xxx((Assert ((v1 * gcd(v1;v2)) + (v1 rem gcd(v1;v2))) ≤ v1 BY Auto) THEN  Decide ⌜2 ≤ gcd(v1;v2)⌝⋅ THEN 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)) + (v1 rem gcd(v1;v2))) ∈ ℤ
9. 0 ≤ (v1 rem gcd(v1;v2))
10. v1 rem gcd(v1;v2) < gcd(v1;v2)
11. ((v1 * gcd(v1;v2)) + (v1 rem gcd(v1;v2))) ≤ v1
12. 2 ≤ 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)
7.  0  <  gcd(v1;v2)
8.  v1  =  ((v1  *  gcd(v1;v2))  +  (v1  rem  gcd(v1;v2)))
9.  0  \mleq{}  (v1  rem  gcd(v1;v2))
10.  v1  rem  gcd(v1;v2)  <  gcd(v1;v2)
\mvdash{}  gcd(v1;v2)  =  1


By

---

Latex:
xxx((Assert  ((v1  *  gcd(v1;v2))  +  (v1  rem  gcd(v1;v2)))  \mleq{}  v1  BY
                      Auto)
        THEN    Decide  \mkleeneopen{}2  \mleq{}  gcd(v1;v2)\mkleeneclose{}\mcdot{}
        THEN  Auto)xxx

---

Home Index