---

Step * of Lemma rv-disjoint-rv-add

∀p:FinProbSpace. ∀n:ℕ. ∀X,Y,Z:RandomVariable(p;n).
  (rv-disjoint(p;n;X;Y) ⇒ rv-disjoint(p;n;X;Z) ⇒ rv-disjoint(p;n;X;Y + Z))
BY
{ (Auto
   THEN (All (Unfold `rv-disjoint`))
   THEN ParallelLast
   THEN (InstHyp [⌈i⌉] 6⋅ THENA Auto)
   THEN SplitOrHyps
   THEN Try (((OrLeft THENM Trivial)
              THENA (Auto THEN Try ((Fold `random-variable` 0 THEN Auto)) THEN Try ((Fold `p-outcome` 0 THEN Auto)))
              ))
   THEN (OrRight THENA (Auto THEN Try ((Fold `random-variable` 0 THEN Auto)) THEN Try ((Fold `p-outcome` 0 THEN Auto))))
   THEN RepUR ``rv-add`` 0
   THEN Auto
   THEN EqCD
   THEN Auto
   THEN BackThruSomeHyp
   THEN Trivial) }

---

Latex:


\mforall{}p:FinProbSpace.  \mforall{}n:\mBbbN{}.  \mforall{}X,Y,Z:RandomVariable(p;n).
    (rv-disjoint(p;n;X;Y)  {}\mRightarrow{}  rv-disjoint(p;n;X;Z)  {}\mRightarrow{}  rv-disjoint(p;n;X;Y  +  Z))


By

(Auto
  THEN  (All  (Unfold  `rv-disjoint`))
  THEN  ParallelLast
  THEN  (InstHyp  [\mkleeneopen{}i\mkleeneclose{}]  6\mcdot{}  THENA  Auto)
  THEN  SplitOrHyps
  THEN  Try  (((OrLeft  THENM  Trivial)
                        THENA  (Auto
                                      THEN  Try  ((Fold  `random-variable`  0  THEN  Auto))
                                      THEN  Try  ((Fold  `p-outcome`  0  THEN  Auto)))
                        ))
  THEN  (OrRight
              THENA  (Auto
                            THEN  Try  ((Fold  `random-variable`  0  THEN  Auto))
                            THEN  Try  ((Fold  `p-outcome`  0  THEN  Auto)))
              )
  THEN  RepUR  ``rv-add``  0
  THEN  Auto
  THEN  EqCD
  THEN  Auto
  THEN  BackThruSomeHyp
  THEN  Trivial)

---

Home Index