---

Step * 1 1 1 of Lemma not-nullset


1. p : FinProbSpace
2. ∀tree:(n:ℕ × (ℕn ⟶ Outcome)) ⟶ 𝔹
     ((∀i,j:ℕ.  ((i ≤ j) ⇒ (∀x:ℕj ⟶ Outcome. ((↑(tree <j, x>)) ⇒ (↑(tree <i, x>))))))
     ⇒ (¬(∃b:ℕ. ∀x:ℕb ⟶ Outcome. (¬↑(tree <b, x>))))
     ⇒ (∃s:ℕ ⟶ Outcome. ∀n:ℕ. (↑(tree <n, s>))))
3. nullset(p;λs.True)
4. C : p-open(p)
5. ∀s:ℕ ⟶ Outcome. s ∈ C
6. measure(C) ≤ (1/2)
7. i : ℕ
8. j : ℕ
9. i ≤ j
10. x : ℕj ⟶ Outcome
11. ↑(C <j, x> =z 0)
⊢ (C <i, x>) = 0 ∈ ℤ
BY
{ (((RW assert_pushdownC (-1)) THENA Auto)
   THEN ((RW assert_pushdownC (0)) THENA Auto)
   THEN DVar `C'
   THEN Assert ⌜(C <i, x>) ≤ (C <j, x>)⌝⋅
   THEN Auto') }

1
.....assertion..... 
1. p : FinProbSpace
2. ∀tree:(n:ℕ × (ℕn ⟶ Outcome)) ⟶ 𝔹
     ((∀i,j:ℕ.  ((i ≤ j) ⇒ (∀x:ℕj ⟶ Outcome. ((↑(tree <j, x>)) ⇒ (↑(tree <i, x>))))))
     ⇒ (¬(∃b:ℕ. ∀x:ℕb ⟶ Outcome. (¬↑(tree <b, x>))))
     ⇒ (∃s:ℕ ⟶ Outcome. ∀n:ℕ. (↑(tree <n, s>))))
3. nullset(p;λs.True)
4. C : (n:ℕ × (ℕn ⟶ Outcome)) ⟶ ℕ2
5. ∀s:ℕ ⟶ Outcome. ∀j:ℕ. ∀i:ℕj.  ((C <i, s>) ≤ (C <j, s>))
6. ∀s:ℕ ⟶ Outcome. s ∈ C
7. measure(C) ≤ (1/2)
8. i : ℕ
9. j : ℕ
10. i ≤ j
11. x : ℕj ⟶ Outcome
12. (C <j, x>) = 0 ∈ ℤ
⊢ (C <i, x>) ≤ (C <j, x>)

---

Latex:

---

Latex:

1.  p  :  FinProbSpace
2.  \mforall{}tree:(n:\mBbbN{}  \mtimes{}  (\mBbbN{}n  {}\mrightarrow{}  Outcome))  {}\mrightarrow{}  \mBbbB{}
          ((\mforall{}i,j:\mBbbN{}.    ((i  \mleq{}  j)  {}\mRightarrow{}  (\mforall{}x:\mBbbN{}j  {}\mrightarrow{}  Outcome.  ((\muparrow{}(tree  <j,  x>))  {}\mRightarrow{}  (\muparrow{}(tree  <i,  x>))))))
          {}\mRightarrow{}  (\mneg{}(\mexists{}b:\mBbbN{}.  \mforall{}x:\mBbbN{}b  {}\mrightarrow{}  Outcome.  (\mneg{}\muparrow{}(tree  <b,  x>))))
          {}\mRightarrow{}  (\mexists{}s:\mBbbN{}  {}\mrightarrow{}  Outcome.  \mforall{}n:\mBbbN{}.  (\muparrow{}(tree  <n,  s>))))
3.  nullset(p;\mlambda{}s.True)
4.  C  :  p-open(p)
5.  \mforall{}s:\mBbbN{}  {}\mrightarrow{}  Outcome.  s  \mmember{}  C
6.  measure(C)  \mleq{}  (1/2)
7.  i  :  \mBbbN{}
8.  j  :  \mBbbN{}
9.  i  \mleq{}  j
10.  x  :  \mBbbN{}j  {}\mrightarrow{}  Outcome
11.  \muparrow{}(C  <j,  x>  =\msubz{}  0)
\mvdash{}  (C  <i,  x>)  =  0


By

---

Latex:
(((RW  assert\_pushdownC  (-1))  THENA  Auto)
  THEN  ((RW  assert\_pushdownC  (0))  THENA  Auto)
  THEN  DVar  `C'
  THEN  Assert  \mkleeneopen{}(C  <i,  x>)  \mleq{}  (C  <j,  x>)\mkleeneclose{}\mcdot{}
  THEN  Auto')

---

Home Index