---

Step * of Lemma rv-disjoint-shift

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

---

Latex:

---

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


By

---

Latex:
xxx(Auto
        THEN  ParallelLast
        THEN  Auto
        THEN  ((InstHyp  [\mkleeneopen{}i  +  1\mkleeneclose{}]  (-2))\mcdot{}  THENA  Auto)
        THEN  ParallelLast
        THEN  Try  ((Fold  `random-variable`  0  THEN  Auto))
        THEN  Try  ((Fold  `p-outcome`  0  THEN  Auto))
        THEN  Auto
        THEN  RepUR  ``rv-shift``  0
        THEN  BackThruSomeHyp
        THEN  Auto
        THEN  RepUR  ``cons-seq``  0
        THEN  SplitOnConclITE
        THEN  Auto
        THEN  BackThruSomeHyp
        THEN  Auto')xxx

---

Home Index