Step
*
2
1
1
1
of Lemma
open-expectation-monotone
.....wf.....
1. p : FinProbSpace
2. n : ℤ
3. 0 < n
4. ∀m:ℕ. (((n - 1) ≤ m)
⇒ (∀C:p-open(p). (E(n - 1;λs.(C <n - 1, s>)) ≤ E(m;λs.(C <m, s>)))))
5. m : ℕ@i
6. n ≤ m@i
7. C : p-open(p)@i
8. ¬(n = 0 ∈ ℤ)
9. ¬(m = 0 ∈ ℤ)
10. x : ℕ||p||@i
⊢ λp.(C <(fst(p)) + 1, cons-seq(x;snd(p))>) ∈ p-open(p)
BY
{ ((All (Unfold `p-open`))
THEN MemTypeCD
THEN Reduce 0
THEN Auto
THEN Try ((D -1 THEN Reduce 0 THEN Auto'))
THEN Try ((DVar `C' THEN Unhide THEN Auto))
THEN Try ((Unfold `p-outcome` 0 THEN Auto))
THEN Try ((BackThruSomeHyp THEN Unfold `cons-seq` 0 THEN Auto))
THEN Try ((Unfold `p-outcome` 0 THEN Auto))) }
Latex:
.....wf.....
1. p : FinProbSpace
2. n : \mBbbZ{}
3. 0 < n
4. \mforall{}m:\mBbbN{}. (((n - 1) \mleq{} m) {}\mRightarrow{} (\mforall{}C:p-open(p). (E(n - 1;\mlambda{}s.(C <n - 1, s>)) \mleq{} E(m;\mlambda{}s.(C <m, s>)))))
5. m : \mBbbN{}@i
6. n \mleq{} m@i
7. C : p-open(p)@i
8. \mneg{}(n = 0)
9. \mneg{}(m = 0)
10. x : \mBbbN{}||p||@i
\mvdash{} \mlambda{}p.(C <(fst(p)) + 1, cons-seq(x;snd(p))>) \mmember{} p-open(p)
By
((All (Unfold `p-open`))
THEN MemTypeCD
THEN Reduce 0
THEN Auto
THEN Try ((D -1 THEN Reduce 0 THEN Auto'))
THEN Try ((DVar `C' THEN Unhide THEN Auto))
THEN Try ((Unfold `p-outcome` 0 THEN Auto))
THEN Try ((BackThruSomeHyp THEN Unfold `cons-seq` 0 THEN Auto))
THEN Try ((Unfold `p-outcome` 0 THEN Auto)))
Home
Index