---

Step * of Lemma callbyvalueall-single-bag-combine2

No Annotations
∀[F,G,a:Top].  (let x ⟵ [a] in let y ⟵ ⋃z∈x.G[z] in F[y] ~ let x ⟵ a in let y ⟵ G[x] @ [] in F[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:Top].
    (let  x  \mleftarrow{}{}  [a]
      in  let  y  \mleftarrow{}{}  \mcup{}z\mmember{}x.G[z]
            in  F[y]  \msim{}  let  x  \mleftarrow{}{}  a
                                in  let  y  \mleftarrow{}{}  G[x]  @  []
                                      in  F[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