---

Step * of Lemma rv-disjoint-compose

∀F,G:ℚ ─→ ℚ. ∀p:FinProbSpace. ∀n:ℕ. ∀X,Y:RandomVariable(p;n).
  (rv-disjoint(p;n;X;Y) ⇒ rv-disjoint(p;n;(X.F[X]) o X;(Y.G[Y]) o Y))
BY
{ (Auto
   THEN RepeatFor 3 (ParallelLast)
   THEN Try ((Fold `random-variable` 0 THEN Auto))
   THEN (Try ((Fold `p-outcome` 0 THEN Auto)) THEN RepeatFor 3 (ParallelLast))
   THEN Try ((RepUR ``rv-compose`` 0 THEN EqCD THEN Auto))) }

---

Latex:


\mforall{}F,G:\mBbbQ{}  {}\mrightarrow{}  \mBbbQ{}.  \mforall{}p:FinProbSpace.  \mforall{}n:\mBbbN{}.  \mforall{}X,Y:RandomVariable(p;n).
    (rv-disjoint(p;n;X;Y)  {}\mRightarrow{}  rv-disjoint(p;n;(X.F[X])  o  X;(Y.G[Y])  o  Y))


By

(Auto
  THEN  RepeatFor  3  (ParallelLast)
  THEN  Try  ((Fold  `random-variable`  0  THEN  Auto))
  THEN  (Try  ((Fold  `p-outcome`  0  THEN  Auto))  THEN  RepeatFor  3  (ParallelLast))
  THEN  Try  ((RepUR  ``rv-compose``  0  THEN  EqCD  THEN  Auto)))

---

Home Index