Step
*
1
1
of Lemma
random_wf
1. p : FinProbSpace
2. a : Atom2
3. b : 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