---

Step * of Lemma callbyvalueall_seq-spread0

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

---

Latex:

---

Latex:
\mforall{}[F,G,H,L:Top].  \mforall{}[m:\mBbbN{}].
    (let  x,y  =  callbyvalueall\_seq(L;\mlambda{}x.x;\mlambda{}g.<F[g],  G[g]>0;m) 
      in  H[x;y]  \msim{}  callbyvalueall\_seq(L;\mlambda{}x.x;\mlambda{}g.H[F[g];G[g]];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{}  THENA  Auto)
  THEN  RepUR  ``mk\_applies``  (-1)
  THEN  Auto)

---

Home Index