---

Step * of Lemma parallel-class-disjoint-classrel

∀[Info,A,B:Type]. ∀[es:EO+(Info)]. ∀[X,Y:EClass(A)]. ∀[Z:EClass(B)].
  (disjoint-classrel(es;A;X;B;Z) ⇒ disjoint-classrel(es;A;Y;B;Z) ⇒ disjoint-classrel(es;A;X || Y;B;Z))
BY
{ ((UnivCD THENA MaAuto)
   THEN All (Unfold `disjoint-classrel`)
   THEN Auto
   THEN RepeatFor 2 ((InstHyp [⌜e⌝] (-3)⋅ THENA Auto))
   THEN D (-2)
   THEN D (-1)
   THEN Try (Complete ((OrRight THEN Auto)))
   THEN (OrLeft THENA Auto)
   THEN Auto
   THEN RepeatFor 2 ((InstHyp [⌜a⌝] (-3)⋅ THENA Auto))
   THEN (D 0 THENA Auto)
   THEN UseClassRel (-1)
   THEN D (-1)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Info,A,B:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X,Y:EClass(A)].  \mforall{}[Z:EClass(B)].
    (disjoint-classrel(es;A;X;B;Z)
    {}\mRightarrow{}  disjoint-classrel(es;A;Y;B;Z)
    {}\mRightarrow{}  disjoint-classrel(es;A;X  ||  Y;B;Z))


By

---

Latex:
((UnivCD  THENA  MaAuto)
  THEN  All  (Unfold  `disjoint-classrel`)
  THEN  Auto
  THEN  RepeatFor  2  ((InstHyp  [\mkleeneopen{}e\mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto))
  THEN  D  (-2)
  THEN  D  (-1)
  THEN  Try  (Complete  ((OrRight  THEN  Auto)))
  THEN  (OrLeft  THENA  Auto)
  THEN  Auto
  THEN  RepeatFor  2  ((InstHyp  [\mkleeneopen{}a\mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto))
  THEN  (D  0  THENA  Auto)
  THEN  UseClassRel  (-1)
  THEN  D  (-1)
  THEN  Auto)

---

Home Index