---

Step * of Lemma not-m-not-reg-3regular

∀[X:Type]. ∀[d:metric(X)]. ∀[s:ℕ ⟶ X]. ∀[b:ℕ].
  ((∀n:ℕb. m-not-reg(d;s;n) = ff) ⇒ (∀n,m:ℕb.  (mdist(d;s n;s m) ≤ ((r(3)/r(n + 1)) + (r(3)/r(m + 1))))))
BY
{ (Auto
   THEN ((Decide ⌜n < m⌝⋅ THENA Auto)
         THENL [(D 5 With ⌜m⌝  THENA Auto)
               ; ((Decide ⌜m < n⌝⋅ THENA Auto)
                  THENL [(D 5 With ⌜n⌝  THENA Auto); ((Subst' n ~ m 0 THENA Auto) THEN RWO "mdist-same" 0 THEN Auto)]
               )]
   )
   THEN MoveToConcl (-1)
   THEN Unfold `m-not-reg` 0
   THEN (GenConclAtAddr [1;2;1] THENA Auto)
   THEN D -2
   THEN Reduce 0
   THEN Auto
   THEN RWO "mdist-symm" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[X:Type].  \mforall{}[d:metric(X)].  \mforall{}[s:\mBbbN{}  {}\mrightarrow{}  X].  \mforall{}[b:\mBbbN{}].
    ((\mforall{}n:\mBbbN{}b.  m-not-reg(d;s;n)  =  ff)
    {}\mRightarrow{}  (\mforall{}n,m:\mBbbN{}b.    (mdist(d;s  n;s  m)  \mleq{}  ((r(3)/r(n  +  1))  +  (r(3)/r(m  +  1))))))


By

---

Latex:
(Auto
  THEN  ((Decide  \mkleeneopen{}n  <  m\mkleeneclose{}\mcdot{}  THENA  Auto)
              THENL  [(D  5  With  \mkleeneopen{}m\mkleeneclose{}    THENA  Auto)
                          ;  ((Decide  \mkleeneopen{}m  <  n\mkleeneclose{}\mcdot{}  THENA  Auto)
                                THENL  [(D  5  With  \mkleeneopen{}n\mkleeneclose{}    THENA  Auto)
                                            ;  ((Subst'  n  \msim{}  m  0  THENA  Auto)  THEN  RWO  "mdist-same"  0  THEN  Auto)]
                          )]
  )
  THEN  MoveToConcl  (-1)
  THEN  Unfold  `m-not-reg`  0
  THEN  (GenConclAtAddr  [1;2;1]  THENA  Auto)
  THEN  D  -2
  THEN  Reduce  0
  THEN  Auto
  THEN  RWO  "mdist-symm"  0
  THEN  Auto)

---

Home Index