---

Step * of Lemma parallel-class-es-sv

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[A:Type]. ∀[X,Y:EClass(A)].
  (es-sv-class(es;X || Y)) supposing (es-sv-class(es;X) and es-sv-class(es;Y) and disjoint-classrel(es;A;X;A;Y))
BY
{ ((UnivCD THENA MaAuto)
   THEN RepUR ``es-sv-class parallel-class eclass-compose2`` 0
   THEN Auto
   THEN All (Unfold `es-sv-class`)
   THEN (RWO "bag-size-append" 0 THENA Auto)
   THEN RepeatFor 2 ((InstHyp [⌜e⌝] (-3)⋅ THENA Auto))
   THEN (Assert ⌜(#(X es e) = 0 ∈ ℤ) ∨ (#(X es e) = 1 ∈ ℤ)⌝⋅ THENA Auto')
   THEN (Assert ⌜(#(Y es e) = 0 ∈ ℤ) ∨ (#(Y es e) = 1 ∈ ℤ)⌝⋅ THENA Auto')
   THEN D (-2)
   THEN D (-1)
   THEN Auto'
   THEN Assert ⌜False⌝⋅
   THEN Auto
   THEN RepeatFor 2 ((FLemma `bag-size-one` [-2] THENA Auto))
   THEN (Assert ⌜single-valued-bag(X es e;A)⌝⋅ THENA (BLemma `single-valued-bag-if-le1` THEN Auto))
   THEN (Assert ⌜single-valued-bag(Y es e;A)⌝⋅ THENA (BLemma `single-valued-bag-if-le1` THEN Auto))
   THEN (Assert ⌜only(X es e) ↓∈ {only(X es e)}⌝⋅ THENA (BagMemberD 0 THEN Auto))
   THEN (Assert ⌜only(Y es e) ↓∈ {only(Y es e)}⌝⋅ THENA (BagMemberD 0 THEN Auto))
   THEN RevHypSubst' (-6) (-2)
   THEN RevHypSubst' (-5) (-1)⋅
   THEN Try (Fold `classrel` (-1))
   THEN Try (Fold `classrel` (-2))
   THEN UseDisjointClassRel (-1) (-2)) }

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[A:Type].  \mforall{}[X,Y:EClass(A)].
    (es-sv-class(es;X  ||  Y))  supposing 
          (es-sv-class(es;X)  and 
          es-sv-class(es;Y)  and 
          disjoint-classrel(es;A;X;A;Y))


By

---

Latex:
((UnivCD  THENA  MaAuto)
  THEN  RepUR  ``es-sv-class  parallel-class  eclass-compose2``  0
  THEN  Auto
  THEN  All  (Unfold  `es-sv-class`)
  THEN  (RWO  "bag-size-append"  0  THENA  Auto)
  THEN  RepeatFor  2  ((InstHyp  [\mkleeneopen{}e\mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto))
  THEN  (Assert  \mkleeneopen{}(\#(X  es  e)  =  0)  \mvee{}  (\#(X  es  e)  =  1)\mkleeneclose{}\mcdot{}  THENA  Auto')
  THEN  (Assert  \mkleeneopen{}(\#(Y  es  e)  =  0)  \mvee{}  (\#(Y  es  e)  =  1)\mkleeneclose{}\mcdot{}  THENA  Auto')
  THEN  D  (-2)
  THEN  D  (-1)
  THEN  Auto'
  THEN  Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  RepeatFor  2  ((FLemma  `bag-size-one`  [-2]  THENA  Auto))
  THEN  (Assert  \mkleeneopen{}single-valued-bag(X  es  e;A)\mkleeneclose{}\mcdot{}  THENA  (BLemma  `single-valued-bag-if-le1`  THEN  Auto))
  THEN  (Assert  \mkleeneopen{}single-valued-bag(Y  es  e;A)\mkleeneclose{}\mcdot{}  THENA  (BLemma  `single-valued-bag-if-le1`  THEN  Auto))
  THEN  (Assert  \mkleeneopen{}only(X  es  e)  \mdownarrow{}\mmember{}  \{only(X  es  e)\}\mkleeneclose{}\mcdot{}  THENA  (BagMemberD  0  THEN  Auto))
  THEN  (Assert  \mkleeneopen{}only(Y  es  e)  \mdownarrow{}\mmember{}  \{only(Y  es  e)\}\mkleeneclose{}\mcdot{}  THENA  (BagMemberD  0  THEN  Auto))
  THEN  RevHypSubst'  (-6)  (-2)
  THEN  RevHypSubst'  (-5)  (-1)\mcdot{}
  THEN  Try  (Fold  `classrel`  (-1))
  THEN  Try  (Fold  `classrel`  (-2))
  THEN  UseDisjointClassRel  (-1)  (-2))

---

Home Index