---

Step * of Lemma callbyvalueall-single-bag-combine1

∀[F,a,as:Top].  (let x ⟵ [a] in let y ⟵ ⋃z∈x.map(z;as) in F[y] ~ let x ⟵ a in let y ⟵ map(x;as) in F[y])
BY
{ ((RWO "callbyvalueall-single" 0 THENA Auto)
   THEN (RWO  "bag-combine-unit-left-top" 0 THENA Auto)
   THEN RepUR ``bag-append empty-bag`` 0
   THEN (RWO "map-append-empty" 0 THENA Auto)
   THEN (UnivCD THENA Auto)) }

1
1. F : Top
2. a : Top
3. as : Top
⊢ let x ⟵ a
  in let y ⟵ map(a;as)
     in F[y] ~ let x ⟵ a
               in let y ⟵ map(x;as)
                  in F[y]

---

Latex:

---

Latex:
\mforall{}[F,a,as:Top].
    (let  x  \mleftarrow{}{}  [a]
      in  let  y  \mleftarrow{}{}  \mcup{}z\mmember{}x.map(z;as)
            in  F[y]  \msim{}  let  x  \mleftarrow{}{}  a
                                in  let  y  \mleftarrow{}{}  map(x;as)
                                      in  F[y])


By

---

Latex:
((RWO  "callbyvalueall-single"  0  THENA  Auto)
  THEN  (RWO    "bag-combine-unit-left-top"  0  THENA  Auto)
  THEN  RepUR  ``bag-append  empty-bag``  0
  THEN  (RWO  "map-append-empty"  0  THENA  Auto)
  THEN  (UnivCD  THENA  Auto))

---

Home Index