---

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


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 : ℤ
13. 0 < n
14. zz : ℕ3
15. ¬0 < zz
16. accumulate (with value u and list item k):
     if 0 <z u then u else c (k + 1) fi 
    over list:
      upto(n)
    with starting value:
     0)
= zz
∈ ℕ3
17. yy : ℕ3
18. accumulate (with value u and list item k):
     if 0 <z u then u else c (k + 1) fi 
    over list:
      upto(n + 1)
    with starting value:
     0)
= yy
∈ ℕ3
19. (((zz = 0 ∈ ℤ) ⇒ (mdist(d;x;y) < (r1/r(n)))) ∧ ((zz = 1 ∈ ℤ) ⇒ (r < mdist(d;x;y))) ∧ ((zz = 2 ∈ ℤ) ⇒ (r0 < r)))
∧ ((zz = 1 ∈ ℤ) ⇒ (yy = 1 ∈ ℤ))
∧ ((zz = 2 ∈ ℤ) ⇒ (yy = 2 ∈ ℤ))
⊢ ((((c (n + 1)) = 0 ∈ ℤ) ⇒ (mdist(d;x;y) < (r1/r(n + 1))))
  ∧ (((c (n + 1)) = 1 ∈ ℤ) ⇒ (r < mdist(d;x;y)))
  ∧ (((c (n + 1)) = 2 ∈ ℤ) ⇒ (r0 < r)))
∧ (((c (n + 1)) = 1 ∈ ℤ) ⇒ (if 0 <z yy then yy else c ((n + 1) + 1) fi  = 1 ∈ ℤ))
∧ (((c (n + 1)) = 2 ∈ ℤ) ⇒ (if 0 <z yy then yy else c ((n + 1) + 1) fi  = 2 ∈ ℤ))
BY
{ ((RWO "upto_add_1" (-2) THENA Auto) THEN (RWO "list_accum_append" (-2) THENA Auto) THEN Reduce -2) }

1
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 : ℤ
13. 0 < n
14. zz : ℕ3
15. ¬0 < zz
16. accumulate (with value u and list item k):
     if 0 <z u then u else c (k + 1) fi 
    over list:
      upto(n)
    with starting value:
     0)
= zz
∈ ℕ3
17. yy : ℕ3
18. if 0 <z accumulate (with value u and list item k):
             if 0 <z u then u else c (k + 1) fi 
            over list:
              upto(n)
            with starting value:
             0)
then accumulate (with value u and list item k):
      if 0 <z u then u else c (k + 1) fi 
     over list:
       upto(n)
     with starting value:
      0)
else c (n + 1)
fi 
= yy
∈ ℕ3
19. (((zz = 0 ∈ ℤ) ⇒ (mdist(d;x;y) < (r1/r(n)))) ∧ ((zz = 1 ∈ ℤ) ⇒ (r < mdist(d;x;y))) ∧ ((zz = 2 ∈ ℤ) ⇒ (r0 < r)))
∧ ((zz = 1 ∈ ℤ) ⇒ (yy = 1 ∈ ℤ))
∧ ((zz = 2 ∈ ℤ) ⇒ (yy = 2 ∈ ℤ))
⊢ ((((c (n + 1)) = 0 ∈ ℤ) ⇒ (mdist(d;x;y) < (r1/r(n + 1))))
  ∧ (((c (n + 1)) = 1 ∈ ℤ) ⇒ (r < mdist(d;x;y)))
  ∧ (((c (n + 1)) = 2 ∈ ℤ) ⇒ (r0 < r)))
∧ (((c (n + 1)) = 1 ∈ ℤ) ⇒ (if 0 <z yy then yy else c ((n + 1) + 1) fi  = 1 ∈ ℤ))
∧ (((c (n + 1)) = 2 ∈ ℤ) ⇒ (if 0 <z yy then yy else c ((n + 1) + 1) fi  = 2 ∈ ℤ))

---

Latex:

---

Latex:

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  :  \mBbbZ{}
13.  0  <  n
14.  zz  :  \mBbbN{}3
15.  \mneg{}0  <  zz
16.  accumulate  (with  value  u  and  list  item  k):
          if  0  <z  u  then  u  else  c  (k  +  1)  fi 
        over  list:
            upto(n)
        with  starting  value:
          0)
=  zz
17.  yy  :  \mBbbN{}3
18.  accumulate  (with  value  u  and  list  item  k):
          if  0  <z  u  then  u  else  c  (k  +  1)  fi 
        over  list:
            upto(n  +  1)
        with  starting  value:
          0)
=  yy
19.  (((zz  =  0)  {}\mRightarrow{}  (mdist(d;x;y)  <  (r1/r(n))))
        \mwedge{}  ((zz  =  1)  {}\mRightarrow{}  (r  <  mdist(d;x;y)))
        \mwedge{}  ((zz  =  2)  {}\mRightarrow{}  (r0  <  r)))
\mwedge{}  ((zz  =  1)  {}\mRightarrow{}  (yy  =  1))
\mwedge{}  ((zz  =  2)  {}\mRightarrow{}  (yy  =  2))
\mvdash{}  ((((c  (n  +  1))  =  0)  {}\mRightarrow{}  (mdist(d;x;y)  <  (r1/r(n  +  1))))
    \mwedge{}  (((c  (n  +  1))  =  1)  {}\mRightarrow{}  (r  <  mdist(d;x;y)))
    \mwedge{}  (((c  (n  +  1))  =  2)  {}\mRightarrow{}  (r0  <  r)))
\mwedge{}  (((c  (n  +  1))  =  1)  {}\mRightarrow{}  (if  0  <z  yy  then  yy  else  c  ((n  +  1)  +  1)  fi    =  1))
\mwedge{}  (((c  (n  +  1))  =  2)  {}\mRightarrow{}  (if  0  <z  yy  then  yy  else  c  ((n  +  1)  +  1)  fi    =  2))


By

---

Latex:
((RWO  "upto\_add\_1"  (-2)  THENA  Auto)  THEN  (RWO  "list\_accum\_append"  (-2)  THENA  Auto)  THEN  Reduce  -2)

---

Home Index