---

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 : ℕ
6. n ≤ m
7. C : p-open(p)
8. ¬(n = 0 ∈ ℤ)
9. ¬(m = 0 ∈ ℤ)
10. x : ℕ||p||
⊢ λp.(C <(fst(p)) + 1, cons-seq(x;snd(p))>) ∈ p-open(p)
BY
{ xxx((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)))xxx }

---

Latex:

---

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{}
6.  n  \mleq{}  m
7.  C  :  p-open(p)
8.  \mneg{}(n  =  0)
9.  \mneg{}(m  =  0)
10.  x  :  \mBbbN{}||p||
\mvdash{}  \mlambda{}p.(C  <(fst(p))  +  1,  cons-seq(x;snd(p))>)  \mmember{}  p-open(p)


By

---

Latex:
xxx((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)))xxx

---

Home Index