---

Step * of Lemma simple-cbva-seq-spread

∀[F,G,H,L:Top]. ∀[m:ℕ+].
  (let x,y = simple-cbva-seq(L;λa.<F[a], G[a]>;m) 
   in H[x;y] ~ simple-cbva-seq(L;λa.H[F[a];G[a]];m))
BY
{ (Auto
   THEN RepUR ``simple-cbva-seq cbva-seq`` 0
   THEN D (-1)
   THEN AutoSplit
   THEN BLemma `callbyvalueall-seq-spread0`
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[F,G,H,L:Top].  \mforall{}[m:\mBbbN{}\msupplus{}].
    (let  x,y  =  simple-cbva-seq(L;\mlambda{}a.<F[a],  G[a]>m) 
      in  H[x;y]  \msim{}  simple-cbva-seq(L;\mlambda{}a.H[F[a];G[a]];m))


By

---

Latex:
(Auto
  THEN  RepUR  ``simple-cbva-seq  cbva-seq``  0
  THEN  D  (-1)
  THEN  AutoSplit
  THEN  BLemma  `callbyvalueall-seq-spread0`
  THEN  Auto)

---

Home Index