---

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
{ xxx(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)xxx }

---

Latex:

---

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

---

Latex:
xxx(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)xxx

---

Home Index