---

Step * of Lemma eclass2-single-val

∀[Info,B,C:Type]. ∀[X:EClass(B ─→ bag(C))]. ∀[Y:EClass(B)]. ∀[es:EO+(Info)].
  (single-valued-classrel(es;(X o Y);C)) supposing 
     (single-valued-classrel(es;X;B ─→ bag(C)) and 
     single-valued-classrel(es;Y;B) and 
     (∀b:B. ∀cs:bag(C). ∀es:EO+(Info). ∀e:E.  (cs ∈ X(b)(e) ⇒ single-valued-bag(cs;C))))
BY
{ skip{((UnivCD THENA Auto)
        THEN skip{(UnfoldTopAb 0
                   THEN Auto
                   THEN skip{(All(\h.MaUseClassRel h)
                              THEN Repeat (SingleVal `e')
                              THEN (Eliminate ⌈b1⌉⋅ THENA Auto)
                              THEN ThinVar `b1'
                              THEN (Eliminate ⌈f1⌉⋅ THENA Auto)
                              THEN ThinVar `f1'
                              THEN (InstHyp [⌈b⌉;⌈f b⌉;⌈es⌉;⌈e⌉] 9⋅ THENA Auto)
                              THEN Try (Complete (UseSingleVal (-7) (-4)))
                              THEN MaUseClassRel 0
                              THEN D 0
                              THEN InstConcl [⌈f⌉]⋅
                              THEN Auto)})}
        )} }

1
∀[Info,B,C:Type]. ∀[X:EClass(B ─→ bag(C))]. ∀[Y:EClass(B)]. ∀[es:EO+(Info)].
  (single-valued-classrel(es;(X o Y);C)) supposing 
     (single-valued-classrel(es;X;B ─→ bag(C)) and 
     single-valued-classrel(es;Y;B) and 
     (∀b:B. ∀cs:bag(C). ∀es:EO+(Info). ∀e:E.  (cs ∈ X(b)(e) ⇒ single-valued-bag(cs;C))))

---

Latex:


\mforall{}[Info,B,C:Type].  \mforall{}[X:EClass(B  {}\mrightarrow{}  bag(C))].  \mforall{}[Y:EClass(B)].  \mforall{}[es:EO+(Info)].
    (single-valued-classrel(es;(X  o  Y);C))  supposing 
          (single-valued-classrel(es;X;B  {}\mrightarrow{}  bag(C))  and 
          single-valued-classrel(es;Y;B)  and 
          (\mforall{}b:B.  \mforall{}cs:bag(C).  \mforall{}es:EO+(Info).  \mforall{}e:E.    (cs  \mmember{}  X(b)(e)  {}\mRightarrow{}  single-valued-bag(cs;C))))


By

skip\{((UnivCD  THENA  Auto)
            THEN  skip\{(UnfoldTopAb  0
                                  THEN  Auto
                                  THEN  skip\{(All(\mbackslash{}h.MaUseClassRel  h)
                                                        THEN  Repeat  (SingleVal  `e')
                                                        THEN  (Eliminate  \mkleeneopen{}b1\mkleeneclose{}\mcdot{}  THENA  Auto)
                                                        THEN  ThinVar  `b1'
                                                        THEN  (Eliminate  \mkleeneopen{}f1\mkleeneclose{}\mcdot{}  THENA  Auto)
                                                        THEN  ThinVar  `f1'
                                                        THEN  (InstHyp  [\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}f  b\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]  9\mcdot{}  THENA  Auto)
                                                        THEN  Try  (Complete  (UseSingleVal  (-7)  (-4)))
                                                        THEN  MaUseClassRel  0
                                                        THEN  D  0
                                                        THEN  InstConcl  [\mkleeneopen{}f\mkleeneclose{}]\mcdot{}
                                                        THEN  Auto)\})\}
            )\}

---

Home Index