---

Step * 2 of Lemma sbdecode-code


1. m : ℕ
2. ∀m:ℕm. ∀[n:ℕ]. (0 < m ⇒ 0 < n ⇒ (sbdecode(sbcode(m;n)) ~ <m ÷ gcd(m;n), n ÷ gcd(m;n)>))
3. n : ℕ
4. ¬m < n
5. ∀n:ℕn. (0 < m ⇒ 0 < n ⇒ (sbdecode(sbcode(m;n)) ~ <m ÷ gcd(m;n), n ÷ gcd(m;n)>))
6. 0 < m
7. 0 < n
8. n < m
⊢ let m,n = sbdecode(sbcode(m - n;n)) 
  in <m + n, n> ~ <m ÷ gcd(m;n), n ÷ gcd(m;n)>
BY
{ xxx(RWO "2" 0
      THEN Reduce 0
      THEN Try (Complete (Auto))
      THEN (InstLemma `gcd-positive` [⌜n⌝;⌜m⌝]⋅ THENA Auto)
      THEN Subst ⌜gcd(m - n;n) ~ gcd(m;n)⌝ 0⋅)xxx }

1
.....equality..... 
1. m : ℕ
2. ∀m:ℕm. ∀[n:ℕ]. (0 < m ⇒ 0 < n ⇒ (sbdecode(sbcode(m;n)) ~ <m ÷ gcd(m;n), n ÷ gcd(m;n)>))
3. n : ℕ
4. ¬m < n
5. ∀n:ℕn. (0 < m ⇒ 0 < n ⇒ (sbdecode(sbcode(m;n)) ~ <m ÷ gcd(m;n), n ÷ gcd(m;n)>))
6. 0 < m
7. 0 < n
8. n < m
9. 0 < gcd(m;n)
⊢ gcd(m - n;n) ~ gcd(m;n)

2
1. m : ℕ
2. ∀m:ℕm. ∀[n:ℕ]. (0 < m ⇒ 0 < n ⇒ (sbdecode(sbcode(m;n)) ~ <m ÷ gcd(m;n), n ÷ gcd(m;n)>))
3. n : ℕ
4. ¬m < n
5. ∀n:ℕn. (0 < m ⇒ 0 < n ⇒ (sbdecode(sbcode(m;n)) ~ <m ÷ gcd(m;n), n ÷ gcd(m;n)>))
6. 0 < m
7. 0 < n
8. n < m
9. 0 < gcd(m;n)
⊢ <((m - n) ÷ gcd(m;n)) + (n ÷ gcd(m;n)), n ÷ gcd(m;n)> ~ <m ÷ gcd(m;n), n ÷ gcd(m;n)>

---

Latex:

---

Latex:

1.  m  :  \mBbbN{}
2.  \mforall{}m:\mBbbN{}m.  \mforall{}[n:\mBbbN{}].  (0  <  m  {}\mRightarrow{}  0  <  n  {}\mRightarrow{}  (sbdecode(sbcode(m;n))  \msim{}  <m  \mdiv{}  gcd(m;n),  n  \mdiv{}  gcd(m;n)>))
3.  n  :  \mBbbN{}
4.  \mneg{}m  <  n
5.  \mforall{}n:\mBbbN{}n.  (0  <  m  {}\mRightarrow{}  0  <  n  {}\mRightarrow{}  (sbdecode(sbcode(m;n))  \msim{}  <m  \mdiv{}  gcd(m;n),  n  \mdiv{}  gcd(m;n)>))
6.  0  <  m
7.  0  <  n
8.  n  <  m
\mvdash{}  let  m,n  =  sbdecode(sbcode(m  -  n;n)) 
    in  <m  +  n,  n>  \msim{}  <m  \mdiv{}  gcd(m;n),  n  \mdiv{}  gcd(m;n)>


By

---

Latex:
xxx(RWO  "2"  0
        THEN  Reduce  0
        THEN  Try  (Complete  (Auto))
        THEN  (InstLemma  `gcd-positive`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{}  THENA  Auto)
        THEN  Subst  \mkleeneopen{}gcd(m  -  n;n)  \msim{}  gcd(m;n)\mkleeneclose{}  0\mcdot{})xxx

---

Home Index