---

Step * of Lemma not-nullset

∀[p:FinProbSpace]. ¬nullset(p;λs.True) supposing ¬¬Konig(||p||)
BY
{ (Auto
   THEN Try ((DVar `p' THEN Complete (Auto)))
   THEN D 0
   THEN Auto
   THEN (Assert ∃C:p-open(p). ((∀s:ℕ ─→ Outcome. s ∈ C) ∧ measure(C) ≤ (1/2)) BY
               (Unfold `nullset` -1
                THEN ((InstHyp [⌈(1/2)⌉] (-1))⋅ THENA Auto)
                THEN (Reduce (-1))
                THEN RepeatFor 3 (ParallelLast)
                THEN Auto))
   THEN ExRepD
   THEN D 2
   THEN (D 0 THENA (Auto THEN DVar `p' THEN Auto))) }

1
1. p : FinProbSpace
2. nullset(p;λs.True)@i
3. C : p-open(p)
4. ∀s:ℕ ─→ Outcome. s ∈ C
5. measure(C) ≤ (1/2)
6. Konig(||p||)@i
⊢ False

---

Latex:


\mforall{}[p:FinProbSpace].  \mneg{}nullset(p;\mlambda{}s.True)  supposing  \mneg{}\mneg{}Konig(||p||)


By

(Auto
  THEN  Try  ((DVar  `p'  THEN  Complete  (Auto)))
  THEN  D  0
  THEN  Auto
  THEN  (Assert  \mexists{}C:p-open(p).  ((\mforall{}s:\mBbbN{}  {}\mrightarrow{}  Outcome.  s  \mmember{}  C)  \mwedge{}  measure(C)  \mleq{}  (1/2))  BY
                          (Unfold  `nullset`  -1
                            THEN  ((InstHyp  [\mkleeneopen{}(1/2)\mkleeneclose{}]  (-1))\mcdot{}  THENA  Auto)
                            THEN  (Reduce  (-1))
                            THEN  RepeatFor  3  (ParallelLast)
                            THEN  Auto))
  THEN  ExRepD
  THEN  D  2
  THEN  (D  0  THENA  (Auto  THEN  DVar  `p'  THEN  Auto)))

---

Home Index