---

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


1. X : Type
2. d : metric(X)
3. s : ℕ ⟶ X
4. m-k-regular(d;2;s)
5. n : ℕ
6. n1 : ℕn
7. x1 : ((r(2)/r(n1 + 1)) + (r(2)/r(n + 1))) < mdist(d;s n1;s n)
8. m-reg-test(d;n;s;s n)
= (inl <n1, x1>)
∈ ((∃n1:ℕn. (((r(2)/r(n1 + 1)) + (r(2)/r(n + 1))) < mdist(d;s n1;s n)))
  ∨ (∀n1:ℕn. (mdist(d;s n1;s n) < ((r(3)/r(n1 + 1)) + (r(3)/r(n + 1))))))
⊢ tt = ff
BY
{ ((D 4 With ⌜n1⌝  THENA Auto) THEN D -1 With ⌜n⌝  THEN Auto) }

---

Latex:

---

Latex:

1.  X  :  Type
2.  d  :  metric(X)
3.  s  :  \mBbbN{}  {}\mrightarrow{}  X
4.  m-k-regular(d;2;s)
5.  n  :  \mBbbN{}
6.  n1  :  \mBbbN{}n
7.  x1  :  ((r(2)/r(n1  +  1))  +  (r(2)/r(n  +  1)))  <  mdist(d;s  n1;s  n)
8.  m-reg-test(d;n;s;s  n)  =  (inl  <n1,  x1>)
\mvdash{}  tt  =  ff


By

---

Latex:
((D  4  With  \mkleeneopen{}n1\mkleeneclose{}    THENA  Auto)  THEN  D  -1  With  \mkleeneopen{}n\mkleeneclose{}    THEN  Auto)

---

Home Index