---

Step * of Lemma find-random_wf

∀[p:FinProbSpace]. ∀[a,b:Atom2]. ∀[C:p-open(p)].
  (find-random{2}(C;p;a;b) ∈ {n:ℕ| (C <n, random(p;a;b)>) = 1 ∈ ℤ} ) supposing ((a#C:p-open(p) ∨ b#C:p-open(p)) and meas\000Cure(C) = 1)
BY
{ ((At ⌈Type⌉ UnivCD⋅ THENA Auto) THEN Try (Complete ((DoSubsume THEN Auto)))) }

1
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 ∈ ℤ} 

---

Latex:


\mforall{}[p:FinProbSpace].  \mforall{}[a,b:Atom2].  \mforall{}[C:p-open(p)].
    (find-random\{2\}(C;p;a;b)  \mmember{}  \{n:\mBbbN{}|  (C  <n,  random(p;a;b)>)  =  1\}  )  supposing  ((a\#C:p-open(p)  \mvee{}  b\#C:p-o\000Cpen(p))  and  measure(C)  =  1)


By

((At  \mkleeneopen{}Type\mkleeneclose{}  UnivCD\mcdot{}  THENA  Auto)  THEN  Try  (Complete  ((DoSubsume  THEN  Auto))))

---

Home Index