Step
*
1
2
1
1
1
2
of Lemma
metric-weak-Markov
.....upcase.....
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. (((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)
= 0
∈ ℤ)
⇒ (mdist(d;x;y) < (r1/r(n))))
∧ ((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)
= 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(n)
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(n)
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(n + 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(n)
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(n + 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(n + 1)
with starting value:
0)
= 0
∈ ℤ)
⇒ (mdist(d;x;y) < (r1/r(n + 1))))
∧ ((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)
= 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(n + 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(n + 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((n + 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(n + 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((n + 1) + 1)
with starting value:
0)
= 2
∈ ℤ))
BY
{ (((RWO "upto_add_1" 0 THENA Auto) THEN (RWO "list_accum_append" 0 THENA Auto) THEN Reduce 0)
THEN MoveToConcl (-1)
THEN (GenConcl ⌜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⌝⋅
THENA Auto
)
THEN (GenConcl ⌜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⌝⋅
THENA Auto
)) }
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. 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
16. yy : ℕ3
17. 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
⊢ ((((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 ∈ ℤ)))
⇒ ((((if 0 <z zz then zz else c (n + 1) fi = 0 ∈ ℤ) ⇒ (mdist(d;x;y) < (r1/r(n + 1))))
∧ ((if 0 <z zz then zz else c (n + 1) fi = 1 ∈ ℤ) ⇒ (r < mdist(d;x;y)))
∧ ((if 0 <z zz then zz else c (n + 1) fi = 2 ∈ ℤ) ⇒ (r0 < r)))
∧ ((if 0 <z zz then zz else c (n + 1) fi = 1 ∈ ℤ) ⇒ (if 0 <z yy then yy else c ((n + 1) + 1) fi = 1 ∈ ℤ))
∧ ((if 0 <z zz then zz else c (n + 1) fi = 2 ∈ ℤ) ⇒ (if 0 <z yy then yy else c ((n + 1) + 1) fi = 2 ∈ ℤ)))
Latex:
Latex:
.....upcase.....
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. (((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)
= 0)
{}\mRightarrow{} (mdist(d;x;y) < (r1/r(n))))
\mwedge{} ((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)
= 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(n)
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(n)
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(n + 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(n)
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(n + 1)
with starting value:
0)
= 2))
\mvdash{} (((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)
= 0)
{}\mRightarrow{} (mdist(d;x;y) < (r1/r(n + 1))))
\mwedge{} ((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)
= 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(n + 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(n + 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((n + 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(n + 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((n + 1) + 1)
with starting value:
0)
= 2))
By
Latex:
(((RWO "upto\_add\_1" 0 THENA Auto) THEN (RWO "list\_accum\_append" 0 THENA Auto) THEN Reduce 0)
THEN MoveToConcl (-1)
THEN (GenConcl \mkleeneopen{}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\mkleeneclose{}\mcdot{}
THENA Auto
)
THEN (GenConcl \mkleeneopen{}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\mkleeneclose{}\mcdot{}
THENA Auto
))
Home
Index