---

Step * of Lemma bag-map-map

∀[as,f,g:Top].  (bag-map(f;bag-map(g;as)) ~ bag-map(f o g;as))
BY
{ skip{((UnivCD THENA Auto)
        THEN (GenConcl ⌜as = L ∈ (Top List)⌝⋅ THENA (DoSubsume THEN Auto THEN BLemma `bag-subtype-list` THEN Auto))
        THEN Try (Complete (Auto))
        THEN (Thin (-1) THEN RepUR ``bag-append bag-map`` 0)
        THEN ListInd (-1)
        THEN Reduce 0
        THEN Auto)} }

1
∀[as,f,g:Top].  (bag-map(f;bag-map(g;as)) ~ bag-map(f o g;as))

---

Latex:

---

Latex:
\mforall{}[as,f,g:Top].    (bag-map(f;bag-map(g;as))  \msim{}  bag-map(f  o  g;as))


By

---

Latex:
skip\{((UnivCD  THENA  Auto)
            THEN  (GenConcl  \mkleeneopen{}as  =  L\mkleeneclose{}\mcdot{}  THENA  (DoSubsume  THEN  Auto  THEN  BLemma  `bag-subtype-list`  THEN  Auto))
            THEN  Try  (Complete  (Auto))
            THEN  (Thin  (-1)  THEN  RepUR  ``bag-append  bag-map``  0)
            THEN  ListInd  (-1)
            THEN  Reduce  0
            THEN  Auto)\}

---

Home Index