---

Step * 1 of Lemma randomness

.....set predicate..... 
1. p : FinProbSpace@i
2. a : Atom2@i
3. b : Atom2@i
4. C : p-open(p)@i
5. measure(C) = 1@i
6. a#C:p-open(p) ∨ b#C:p-open(p)@i
⊢ 0 ≤ find-random{2}(C;p;a;b)
BY
{ (GenConclTerm ⌈find-random{2}(C;p;a;b)⌉⋅ THEN Auto) }

---

Latex:


.....set  predicate..... 
1.  p  :  FinProbSpace@i
2.  a  :  Atom2@i
3.  b  :  Atom2@i
4.  C  :  p-open(p)@i
5.  measure(C)  =  1@i
6.  a\#C:p-open(p)  \mvee{}  b\#C:p-open(p)@i
\mvdash{}  0  \mleq{}  find-random\{2\}(C;p;a;b)


By

(GenConclTerm  \mkleeneopen{}find-random\{2\}(C;p;a;b)\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index