---

Step * of Lemma disjoint-union-comb-es-sv

∀[Info,A,B:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(A)]. ∀[Y:EClass(B)].
  (es-sv-class(es;X (+) Y)) supposing (disjoint-classrel(es;A;X;B;Y) and es-sv-class(es;Y) and es-sv-class(es;X))
BY
{ (Intros
   THEN RepUR ``disjoint-union-comb`` 0
   THEN (Using [`A',⌜A + B⌝] (BLemma `parallel-class-es-sv`)⋅ THENA Auto)
   THEN Try (Complete ((Using [`B',⌜A + B⌝] (BLemma `simple-comb-1-es-sv`)⋅ THEN Auto)))
   THEN RepeatFor 2 (((BLemma `simple-comb-1-disjoint-classrel` THENA Auto)
                      THEN (BLemma `disjoint-classrel-symm` THENA Auto)
                      ))
   THEN Trivial) }

---

Latex:

---

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


By

---

Latex:
(Intros
  THEN  RepUR  ``disjoint-union-comb``  0
  THEN  (Using  [`A',\mkleeneopen{}A  +  B\mkleeneclose{}]  (BLemma  `parallel-class-es-sv`)\mcdot{}  THENA  Auto)
  THEN  Try  (Complete  ((Using  [`B',\mkleeneopen{}A  +  B\mkleeneclose{}]  (BLemma  `simple-comb-1-es-sv`)\mcdot{}  THEN  Auto)))
  THEN  RepeatFor  2  (((BLemma  `simple-comb-1-disjoint-classrel`  THENA  Auto)
                                        THEN  (BLemma  `disjoint-classrel-symm`  THENA  Auto)
                                        ))
  THEN  Trivial)

---

Home Index