---

Step * of Lemma classfun-res-eclass3

∀[Info,B,C:Type]. ∀[X:EClass(B ⟶ C)]. ∀[Y:EClass(B)]. ∀[es:EO+(Info)]. ∀[e:E].
  (eclass3(X;Y)@e = (X@e Y@e) ∈ C) supposing (X is functional at e and Y is functional at e)
BY
{ (Auto
   THEN RepUR ``eclass3 classfun-res classfun class-ap`` 0
   THEN (InstLemma `sv-bag-only-combine` [⌜B ⟶ C⌝;⌜C⌝;⌜X es e⌝;⌜λ2f.bag-map(f;Y es e)⌝]⋅ THENA Auto)
   THEN Try ((HypSubst' (-1) 0 THENA Auto))
   THEN Try ((RWO "sv-bag-only-map2" 0 THEN Auto))
   THEN Try (Complete ((All(Unfold `es-functional-class-at`)
                        THEN Try ((BLemma `single-valued-bag-map` THENA Auto))
                        THEN BLemma `single-valued-classrel-implies-bag`
                        THEN Auto)))
   THEN Try (Complete ((All(Unfold `es-functional-class-at`)
                        THEN Try ((RWO "bag-size-map" 0 THENA Auto))
                        THEN BLemma `member-eclass-iff-size`
                        THEN Auto)))) }

---

Latex:

---

Latex:
\mforall{}[Info,B,C:Type].  \mforall{}[X:EClass(B  {}\mrightarrow{}  C)].  \mforall{}[Y:EClass(B)].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].
    (eclass3(X;Y)@e  =  (X@e  Y@e))  supposing  (X  is  functional  at  e  and  Y  is  functional  at  e)


By

---

Latex:
(Auto
  THEN  RepUR  ``eclass3  classfun-res  classfun  class-ap``  0
  THEN  (InstLemma  `sv-bag-only-combine`  [\mkleeneopen{}B  {}\mrightarrow{}  C\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}X  es  e\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}f.bag-map(f;Y  es  e)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Try  ((HypSubst'  (-1)  0  THENA  Auto))
  THEN  Try  ((RWO  "sv-bag-only-map2"  0  THEN  Auto))
  THEN  Try  (Complete  ((All(Unfold  `es-functional-class-at`)
                                            THEN  Try  ((BLemma  `single-valued-bag-map`  THENA  Auto))
                                            THEN  BLemma  `single-valued-classrel-implies-bag`
                                            THEN  Auto)))
  THEN  Try  (Complete  ((All(Unfold  `es-functional-class-at`)
                                            THEN  Try  ((RWO  "bag-size-map"  0  THENA  Auto))
                                            THEN  BLemma  `member-eclass-iff-size`
                                            THEN  Auto))))

---

Home Index