---

Step * 3 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. ¬n < m
5. ¬m < n
6. ∀n:ℕn. (0 < m ⇒ 0 < n ⇒ (sbdecode(sbcode(m;n)) ~ <m ÷ gcd(m;n), n ÷ gcd(m;n)>))
7. 0 < m
8. 0 < n
⊢ <1, 1> ~ <m ÷ gcd(m;n), n ÷ gcd(m;n)>
BY
{ xxx((Subst' m ~ n 0 THENA Auto')
      THEN Subst' gcd(n;n) ~ n 0
      THEN Try (EqCD)
      THEN RWW "div-self gcd_eq_args" 0
      THEN Auto)xxx }

---

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{}n  <  m
5.  \mneg{}m  <  n
6.  \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)>))
7.  0  <  m
8.  0  <  n
\mvdash{}  ə,  1>  \msim{}  <m  \mdiv{}  gcd(m;n),  n  \mdiv{}  gcd(m;n)>


By

---

Latex:
xxx((Subst'  m  \msim{}  n  0  THENA  Auto')
        THEN  Subst'  gcd(n;n)  \msim{}  n  0
        THEN  Try  (EqCD)
        THEN  RWW  "div-self  gcd\_eq\_args"  0
        THEN  Auto)xxx

---

Home Index