---

Step * of Lemma callbyvalueall-single-bag-combine3

No Annotations
∀[F,G,a,b:Top].
  (let x ⟵ [a]
   in let z ⟵ b
      in let y ⟵ ⋃v∈x.G[z;v]
         in F[z;y] ~ let x ⟵ a
                     in let z ⟵ b
                        in let y ⟵ G[z;x] @ []
                           in F[z;y])
BY
{ ((UnivCD THENA Auto)
   THEN RW (BasicSymbolicComputeC ``reduce map append``) 0
   THEN Repeat (Folds ``it nil cons`` 0)
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[F,G,a,b:Top].
    (let  x  \mleftarrow{}{}  [a]
      in  let  z  \mleftarrow{}{}  b
            in  let  y  \mleftarrow{}{}  \mcup{}v\mmember{}x.G[z;v]
                  in  F[z;y]  \msim{}  let  x  \mleftarrow{}{}  a
                                          in  let  z  \mleftarrow{}{}  b
                                                in  let  y  \mleftarrow{}{}  G[z;x]  @  []
                                                      in  F[z;y])


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RW  (BasicSymbolicComputeC  ``reduce  map  append``)  0
  THEN  Repeat  (Folds  ``it  nil  cons``  0)
  THEN  Reduce  0
  THEN  Auto)

---

Home Index