---

Step * 2 of Lemma randomness


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
⊢ (C <find-random{2}(C;p;a;b), random(p;a;b)>) = 1 ∈ ℤ
BY
{ (GenConclAtAddr [2;2;1] THEN D -2 THEN Auto) }

---

Latex:



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{}  (C  <find-random\{2\}(C;p;a;b),  random(p;a;b)>)  =  1


By

(GenConclAtAddr  [2;2;1]  THEN  D  -2  THEN  Auto)

---

Home Index