Step
*
1
2
1
1
1
of Lemma
metric-weak-Markov
.....assertion.....
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)))
⊢ ∃a:ℕ+ ⟶ ℕ3
∀n:ℕ+
(((((a n) = 0 ∈ ℤ) ⇒ (mdist(d;x;y) < (r1/r(n))))
∧ (((a n) = 1 ∈ ℤ) ⇒ (r < mdist(d;x;y)))
∧ (((a n) = 2 ∈ ℤ) ⇒ (r0 < r)))
∧ (((a n) = 1 ∈ ℤ) ⇒ ((a (n + 1)) = 1 ∈ ℤ))
∧ (((a n) = 2 ∈ ℤ) ⇒ ((a (n + 1)) = 2 ∈ ℤ)))
BY
{ ((Assert ∀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) BY
(InductionOnList THEN Reduce 0 THEN Auto))
THEN (D 0 With ⌜λ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)⌝
THENW Auto
)
THEN Reduce 0
THEN InductionOnNat) }
1
.....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
∈ ℤ))
2
.....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
∈ ℤ))
Latex:
Latex:
.....assertion.....
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)))
\mvdash{} \mexists{}a:\mBbbN{}\msupplus{} {}\mrightarrow{} \mBbbN{}3
\mforall{}n:\mBbbN{}\msupplus{}
(((((a n) = 0) {}\mRightarrow{} (mdist(d;x;y) < (r1/r(n))))
\mwedge{} (((a n) = 1) {}\mRightarrow{} (r < mdist(d;x;y)))
\mwedge{} (((a n) = 2) {}\mRightarrow{} (r0 < r)))
\mwedge{} (((a n) = 1) {}\mRightarrow{} ((a (n + 1)) = 1))
\mwedge{} (((a n) = 2) {}\mRightarrow{} ((a (n + 1)) = 2)))
By
Latex:
((Assert \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) BY
(InductionOnList THEN Reduce 0 THEN Auto))
THEN (D 0 With \mkleeneopen{}\mlambda{}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)\mkleeneclose{}
THENW Auto
)
THEN Reduce 0
THEN InductionOnNat)
Home
Index