---

Step * 1 of Lemma find-random_wf


1. p : FinProbSpace
2. a : Atom2
3. b : Atom2
4. C : p-open(p)
5. measure(C) = 1
6. a#C:p-open(p) ∨ b#C:p-open(p)
⊢ find-random{2}(C;p;a;b) ∈ {n:ℕ| (C <n, random(p;a;b)>) = 1 ∈ ℤ} 
BY
{ ((Unfold `member` 0 THEN Refine `findRandomEquality` []) THEN Auto) }

---

Latex:



1.  p  :  FinProbSpace
2.  a  :  Atom2
3.  b  :  Atom2
4.  C  :  p-open(p)
5.  measure(C)  =  1
6.  a\#C:p-open(p)  \mvee{}  b\#C:p-open(p)
\mvdash{}  find-random\{2\}(C;p;a;b)  \mmember{}  \{n:\mBbbN{}|  (C  <n,  random(p;a;b)>)  =  1\} 


By

((Unfold  `member`  0  THEN  Refine  `findRandomEquality`  [])  THEN  Auto)

---

Home Index