---

Step * of Lemma rv-disjoint-rv-shift

∀p:FinProbSpace. ∀n:ℕ. ∀X,Y:RandomVariable(p;n).
  (rv-disjoint(p;n;X;Y)
  ⇒ (∀x,y:Outcome.  (rv-shift(x;X) = rv-shift(y;X) ∈ RandomVariable(p;n - 1)))
     ∨ (∀x,y:Outcome.  (rv-shift(x;Y) = rv-shift(y;Y) ∈ RandomVariable(p;n - 1))) 
     supposing 0 < n)
BY
{ xxx(Auto
      THEN Unfold `rv-disjoint` -2
      THEN ((InstHyp [⌜0⌝] (-2))⋅ THENA Auto)
      THEN ParallelLast
      THEN xxxAutoxxx
      THEN RepUR ``rv-shift random-variable`` 0
      THEN Try (Fold `p-outcome` 0)
      THEN Ext
      THEN Reduce 0
      THEN Auto
      THEN Try ((Fold `random-variable` 0 THEN Auto))
      THEN Try ((Fold `p-outcome` 0 THEN Auto))
      THEN BackThruSomeHyp
      THEN RepUR ``cons-seq`` 0
      THEN Auto
      THEN SplitOnConclITE
      THEN Auto)xxx }

---

Latex:

---

Latex:
\mforall{}p:FinProbSpace.  \mforall{}n:\mBbbN{}.  \mforall{}X,Y:RandomVariable(p;n).
    (rv-disjoint(p;n;X;Y)
    {}\mRightarrow{}  (\mforall{}x,y:Outcome.    (rv-shift(x;X)  =  rv-shift(y;X)))
          \mvee{}  (\mforall{}x,y:Outcome.    (rv-shift(x;Y)  =  rv-shift(y;Y))) 
          supposing  0  <  n)


By

---

Latex:
xxx(Auto
        THEN  Unfold  `rv-disjoint`  -2
        THEN  ((InstHyp  [\mkleeneopen{}0\mkleeneclose{}]  (-2))\mcdot{}  THENA  Auto)
        THEN  ParallelLast
        THEN  xxxAutoxxx
        THEN  RepUR  ``rv-shift  random-variable``  0
        THEN  Try  (Fold  `p-outcome`  0)
        THEN  Ext
        THEN  Reduce  0
        THEN  Auto
        THEN  Try  ((Fold  `random-variable`  0  THEN  Auto))
        THEN  Try  ((Fold  `p-outcome`  0  THEN  Auto))
        THEN  BackThruSomeHyp
        THEN  RepUR  ``cons-seq``  0
        THEN  Auto
        THEN  SplitOnConclITE
        THEN  Auto)xxx

---

Home Index