---

Step * 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 : ℕ
⊢ m-not-reg(d;s;n) = ff
BY
{ (Unfold `m-not-reg` 0 THEN GenConclAtAddr [2;1] THEN D -2 THEN Reduce 0 THEN Auto THEN ExRepD) }

1
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

---

Latex:

---

Latex:

1.  X  :  Type
2.  d  :  metric(X)
3.  s  :  \mBbbN{}  {}\mrightarrow{}  X
4.  m-k-regular(d;2;s)
5.  n  :  \mBbbN{}
\mvdash{}  m-not-reg(d;s;n)  =  ff


By

---

Latex:
(Unfold  `m-not-reg`  0  THEN  GenConclAtAddr  [2;1]  THEN  D  -2  THEN  Reduce  0  THEN  Auto  THEN  ExRepD)

---

Home Index