---

Step * 1 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
{ (At ⌈𝕌'⌉Intros⋅
   THEN Auto
   THEN UnfoldTopAb 0
   THEN Auto
   THEN 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) }

---

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

(At  \mkleeneopen{}\mBbbU{}'\mkleeneclose{}Intros\mcdot{}
  THEN  Auto
  THEN  UnfoldTopAb  0
  THEN  Auto
  THEN  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