Step * 1 1 of Lemma random_wf


1. FinProbSpace
2. Atom2
3. Atom2
⊢ random(p;a;b) random(p;a;b) ∈ (ℕ ─→ Outcome)
BY
(Refine `randomEquality` []  THEN Auto) }


Latex:



1.  p  :  FinProbSpace
2.  a  :  Atom2
3.  b  :  Atom2
\mvdash{}  random(p;a;b)  =  random(p;a;b)


By

(Refine  `randomEquality`  []    THEN  Auto)




Home Index