---

Step * of Lemma sbdecode-code

∀[m,n:ℕ+].  (sbdecode(sbcode(m;n)) ~ <m ÷ gcd(m;n), n ÷ gcd(m;n)>)
BY
{ ((Assert ∀[m,n:ℕ].  (0 < m ⇒ 0 < n ⇒ (sbdecode(sbcode(m;n)) ~ <m ÷ gcd(m;n), n ÷ gcd(m;n)>)) BY
          RepeatFor 2 (CompleteInductionOnNat))
   THEN Try ((RepeatFor 2 (ParallelLast') THEN Auto))
   THEN RepeatFor 2 ((D 0 THENA Auto))
   THEN RecUnfold `sbcode` 0
   THEN Repeat (AutoSplit)
   THEN Unfold `sbdecode` 0
   THEN Reduce 0
   THEN Try (Fold `sbdecode` 0)) }

1
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:ℕn. (0 < m ⇒ 0 < n ⇒ (sbdecode(sbcode(m;n)) ~ <m ÷ gcd(m;n), n ÷ gcd(m;n)>))
5. 0 < m
6. 0 < n
7. m < n
⊢ let m,n = sbdecode(sbcode(m;n - m)) 
  in <m, m + n> ~ <m ÷ 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
⊢ let m,n = sbdecode(sbcode(m - n;n)) 
  in <m + n, n> ~ <m ÷ gcd(m;n), n ÷ gcd(m;n)>

3
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)>

---

Latex:

---

Latex:
\mforall{}[m,n:\mBbbN{}\msupplus{}].    (sbdecode(sbcode(m;n))  \msim{}  <m  \mdiv{}  gcd(m;n),  n  \mdiv{}  gcd(m;n)>)


By

---

Latex:
((Assert  \mforall{}[m,n:\mBbbN{}].    (0  <  m  {}\mRightarrow{}  0  <  n  {}\mRightarrow{}  (sbdecode(sbcode(m;n))  \msim{}  <m  \mdiv{}  gcd(m;n),  n  \mdiv{}  gcd(m;n)>))  BY
                RepeatFor  2  (CompleteInductionOnNat))
  THEN  Try  ((RepeatFor  2  (ParallelLast')  THEN  Auto))
  THEN  RepeatFor  2  ((D  0  THENA  Auto))
  THEN  RecUnfold  `sbcode`  0
  THEN  Repeat  (AutoSplit)
  THEN  Unfold  `sbdecode`  0
  THEN  Reduce  0
  THEN  Try  (Fold  `sbdecode`  0))

---

Home Index