---

Step * 1 2 1 1 1 1 of Lemma metric-weak-Markov

.....basecase..... 
1. [X] : Type
2. d : metric(X)
3. mcomplete(X with d)
4. x : X
5. y : X
6. ∀z:X. ((¬z ≡ x) ∨ (¬z ≡ y))
7. r : ℝ
8. ∀n:ℕ+. ((mdist(d;x;y) < (r1/r(n))) ∨ (r < mdist(d;x;y)) ∨ (r0 < r))
9. c : ℕ+ ⟶ ℕ3
10. ∀n:ℕ+
      ((((c n) = 0 ∈ ℤ) ⇒ (mdist(d;x;y) < (r1/r(n))))
      ∧ (((c n) = 1 ∈ ℤ) ⇒ (r < mdist(d;x;y)))
      ∧ (((c n) = 2 ∈ ℤ) ⇒ (r0 < r)))
11. ∀v:ℕ List. ∀s:ℕ3.
      (accumulate (with value u and list item k):
        if 0 <z u then u else c (k + 1) fi 
       over list:
         v
       with starting value:
        s) ∈ ℕ3)
12. n : ℕ+
⊢ (((accumulate (with value u and list item k):
      if 0 <z u then u else c (k + 1) fi 
     over list:
       upto(1)
     with starting value:
      0)
   = 0
   ∈ ℤ)
   ⇒ (mdist(d;x;y) < (r1/r1)))
  ∧ ((accumulate (with value u and list item k):
       if 0 <z u then u else c (k + 1) fi 
      over list:
        upto(1)
      with starting value:
       0)
    = 1
    ∈ ℤ)
    ⇒ (r < mdist(d;x;y)))
  ∧ ((accumulate (with value u and list item k):
       if 0 <z u then u else c (k + 1) fi 
      over list:
        upto(1)
      with starting value:
       0)
    = 2
    ∈ ℤ)
    ⇒ (r0 < r)))
∧ ((accumulate (with value u and list item k):
     if 0 <z u then u else c (k + 1) fi 
    over list:
      upto(1)
    with starting value:
     0)
  = 1
  ∈ ℤ)
  ⇒ (accumulate (with value u and list item k):
       if 0 <z u then u else c (k + 1) fi 
      over list:
        upto(1 + 1)
      with starting value:
       0)
     = 1
     ∈ ℤ))
∧ ((accumulate (with value u and list item k):
     if 0 <z u then u else c (k + 1) fi 
    over list:
      upto(1)
    with starting value:
     0)
  = 2
  ∈ ℤ)
  ⇒ (accumulate (with value u and list item k):
       if 0 <z u then u else c (k + 1) fi 
      over list:
        upto(1 + 1)
      with starting value:
       0)
     = 2
     ∈ ℤ))
BY
{ (RepUR ``upto`` 0 THEN RepeatFor 3 ((RecUnfold `from-upto` 0 THEN Reduce 0)) THEN Auto) }

---

Latex:

---

Latex:
.....basecase..... 
1.  [X]  :  Type
2.  d  :  metric(X)
3.  mcomplete(X  with  d)
4.  x  :  X
5.  y  :  X
6.  \mforall{}z:X.  ((\mneg{}z  \mequiv{}  x)  \mvee{}  (\mneg{}z  \mequiv{}  y))
7.  r  :  \mBbbR{}
8.  \mforall{}n:\mBbbN{}\msupplus{}.  ((mdist(d;x;y)  <  (r1/r(n)))  \mvee{}  (r  <  mdist(d;x;y))  \mvee{}  (r0  <  r))
9.  c  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbN{}3
10.  \mforall{}n:\mBbbN{}\msupplus{}
            ((((c  n)  =  0)  {}\mRightarrow{}  (mdist(d;x;y)  <  (r1/r(n))))
            \mwedge{}  (((c  n)  =  1)  {}\mRightarrow{}  (r  <  mdist(d;x;y)))
            \mwedge{}  (((c  n)  =  2)  {}\mRightarrow{}  (r0  <  r)))
11.  \mforall{}v:\mBbbN{}  List.  \mforall{}s:\mBbbN{}3.
            (accumulate  (with  value  u  and  list  item  k):
                if  0  <z  u  then  u  else  c  (k  +  1)  fi 
              over  list:
                  v
              with  starting  value:
                s)  \mmember{}  \mBbbN{}3)
12.  n  :  \mBbbN{}\msupplus{}
\mvdash{}  (((accumulate  (with  value  u  and  list  item  k):
            if  0  <z  u  then  u  else  c  (k  +  1)  fi 
          over  list:
              upto(1)
          with  starting  value:
            0)
      =  0)
      {}\mRightarrow{}  (mdist(d;x;y)  <  (r1/r1)))
    \mwedge{}  ((accumulate  (with  value  u  and  list  item  k):
              if  0  <z  u  then  u  else  c  (k  +  1)  fi 
            over  list:
                upto(1)
            with  starting  value:
              0)
        =  1)
        {}\mRightarrow{}  (r  <  mdist(d;x;y)))
    \mwedge{}  ((accumulate  (with  value  u  and  list  item  k):
              if  0  <z  u  then  u  else  c  (k  +  1)  fi 
            over  list:
                upto(1)
            with  starting  value:
              0)
        =  2)
        {}\mRightarrow{}  (r0  <  r)))
\mwedge{}  ((accumulate  (with  value  u  and  list  item  k):
          if  0  <z  u  then  u  else  c  (k  +  1)  fi 
        over  list:
            upto(1)
        with  starting  value:
          0)
    =  1)
    {}\mRightarrow{}  (accumulate  (with  value  u  and  list  item  k):
              if  0  <z  u  then  u  else  c  (k  +  1)  fi 
            over  list:
                upto(1  +  1)
            with  starting  value:
              0)
          =  1))
\mwedge{}  ((accumulate  (with  value  u  and  list  item  k):
          if  0  <z  u  then  u  else  c  (k  +  1)  fi 
        over  list:
            upto(1)
        with  starting  value:
          0)
    =  2)
    {}\mRightarrow{}  (accumulate  (with  value  u  and  list  item  k):
              if  0  <z  u  then  u  else  c  (k  +  1)  fi 
            over  list:
                upto(1  +  1)
            with  starting  value:
              0)
          =  2))


By

---

Latex:
(RepUR  ``upto``  0  THEN  RepeatFor  3  ((RecUnfold  `from-upto`  0  THEN  Reduce  0))  THEN  Auto)

---

Home Index