---

Step * of Lemma parallel-class-single-val

∀[Info,A:Type]. ∀[es:EO+(Info)]. ∀[X,Y:EClass(A)].
  (single-valued-classrel(es;X || Y;A)) supposing 
     (single-valued-classrel(es;X;A) and 
     single-valued-classrel(es;Y;A) and 
     disjoint-classrel(es;A;X;A;Y))
BY
{ ((UnivCD THENA Auto)
   THEN RepUR ``single-valued-classrel`` 0
   THEN Auto
   THEN UseClassRel (-2)
   THEN UseClassRel (-1)
   THEN SplitOrHyps
   THEN Try (UseSingleVal (-1) (-2))
   THEN UseDisjointClassRel (-1) (-2)) }

---

Latex:

---

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


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RepUR  ``single-valued-classrel``  0
  THEN  Auto
  THEN  UseClassRel  (-2)
  THEN  UseClassRel  (-1)
  THEN  SplitOrHyps
  THEN  Try  (UseSingleVal  (-1)  (-2))
  THEN  UseDisjointClassRel  (-1)  (-2))

---

Home Index