---

Step * 1 of Lemma m-regularize-mcauchy

.....assertion..... 
1. X : Type
2. d : metric(X)
3. s : ℕ ⟶ X
4. k : ℕ+
⊢ ∀n:ℕ. ∀m:ℕn.  (((6 * k) ≤ n) ⇒ ((6 * k) ≤ m) ⇒ (mdist(d;m-regularize(d;s) n;m-regularize(d;s) m) ≤ (r1/r(k))))
BY
{ (Auto
   THEN Unfold `m-regularize` 0
   THEN Reduce 0
   THEN (InstLemma `first-m-not-reg-property` [⌜X⌝;⌜d⌝;⌜n + 1⌝;⌜s⌝]⋅ THENA Auto)
   THEN MoveToConcl (-1)
   THEN GenConclAtAddr [1;1;1;2]
   THEN Thin (-1)
   THEN (InstLemma `first-m-not-reg-property` [⌜X⌝;⌜d⌝;⌜m + 1⌝;⌜s⌝]⋅ THENA Auto)
   THEN MoveToConcl (-1)
   THEN GenConclAtAddr [1;1;1;2]
   THEN Thin (-1)
   THEN (CallByValueReduce 0 THENA Auto)
   THEN RepUR ``let`` 0
   THEN RepeatFor 2 ((D 0 THENA Auto))
   THEN ExRepD
   THEN (Decide ⌜0 < v1⌝⋅ THENA Auto)) }

1
1. X : Type
2. d : metric(X)
3. s : ℕ ⟶ X
4. k : ℕ+
5. n : ℕ
6. m : ℕn
7. (6 * k) ≤ n
8. (6 * k) ≤ m
9. v : ℕ(n + 1) + 1
10. v1 : ℕ(m + 1) + 1
11. v1 = 0 ∈ ℤ ⇐⇒ ∀n:ℕm + 1. m-not-reg(d;s;n) = ff
12. (∀n:ℕv1 - 1. m-not-reg(d;s;n) = ff) ∧ m-not-reg(d;s;v1 - 1) = tt supposing 0 < v1
13. v = 0 ∈ ℤ ⇐⇒ ∀n:ℕn + 1. m-not-reg(d;s;n) = ff
14. (∀n:ℕv - 1. m-not-reg(d;s;n) = ff) ∧ m-not-reg(d;s;v - 1) = tt supposing 0 < v
15. 0 < v1
⊢ mdist(d;if 0 <z v then s (v - 2) else s n fi ;if 0 <z v1 then s (v1 - 2) else s m fi ) ≤ (r1/r(k))

2
1. X : Type
2. d : metric(X)
3. s : ℕ ⟶ X
4. k : ℕ+
5. n : ℕ
6. m : ℕn
7. (6 * k) ≤ n
8. (6 * k) ≤ m
9. v : ℕ(n + 1) + 1
10. v1 : ℕ(m + 1) + 1
11. v1 = 0 ∈ ℤ ⇐⇒ ∀n:ℕm + 1. m-not-reg(d;s;n) = ff
12. (∀n:ℕv1 - 1. m-not-reg(d;s;n) = ff) ∧ m-not-reg(d;s;v1 - 1) = tt supposing 0 < v1
13. v = 0 ∈ ℤ ⇐⇒ ∀n:ℕn + 1. m-not-reg(d;s;n) = ff
14. (∀n:ℕv - 1. m-not-reg(d;s;n) = ff) ∧ m-not-reg(d;s;v - 1) = tt supposing 0 < v
15. ¬0 < v1
⊢ mdist(d;if 0 <z v then s (v - 2) else s n fi ;if 0 <z v1 then s (v1 - 2) else s m fi ) ≤ (r1/r(k))

---

Latex:

---

Latex:
.....assertion..... 
1.  X  :  Type
2.  d  :  metric(X)
3.  s  :  \mBbbN{}  {}\mrightarrow{}  X
4.  k  :  \mBbbN{}\msupplus{}
\mvdash{}  \mforall{}n:\mBbbN{}.  \mforall{}m:\mBbbN{}n.
        (((6  *  k)  \mleq{}  n)
        {}\mRightarrow{}  ((6  *  k)  \mleq{}  m)
        {}\mRightarrow{}  (mdist(d;m-regularize(d;s)  n;m-regularize(d;s)  m)  \mleq{}  (r1/r(k))))


By

---

Latex:
(Auto
  THEN  Unfold  `m-regularize`  0
  THEN  Reduce  0
  THEN  (InstLemma  `first-m-not-reg-property`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}n  +  1\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  GenConclAtAddr  [1;1;1;2]
  THEN  Thin  (-1)
  THEN  (InstLemma  `first-m-not-reg-property`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}m  +  1\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  GenConclAtAddr  [1;1;1;2]
  THEN  Thin  (-1)
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  RepUR  ``let``  0
  THEN  RepeatFor  2  ((D  0  THENA  Auto))
  THEN  ExRepD
  THEN  (Decide  \mkleeneopen{}0  <  v1\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index