---

Step * of Lemma callbyvalueall-seq-spread0

∀[F,G,H,L:Top]. ∀[m:ℕ+].
  (let x,y = callbyvalueall-seq(L;λx.x;mk_lambdas(λa.<F[a], G[a]>;m - 1);0;m) 
   in H[x;y] ~ callbyvalueall-seq(L;λx.x;mk_lambdas(λa.H[F[a];G[a]];m - 1);0;m))
BY
{ (Auto
   THEN InstLemma `callbyvalueall-seq-spread` [⌜F⌝;⌜G⌝;⌜H⌝;⌜L⌝;⌜λx.x⌝;⌜m⌝;⌜0⌝]⋅
   THEN Auto
   THEN RepUR ``mk_applies`` (-1)
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  InstLemma  `callbyvalueall-seq-spread`  [\mkleeneopen{}F\mkleeneclose{};\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}H\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{};\mkleeneopen{}\mlambda{}x.x\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  RepUR  ``mk\_applies``  (-1)
  THEN  Auto)

---

Home Index