---

Step * of Lemma cbva_seq-spread

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

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  RepUR  ``cbva\_seq``  0
  THEN  InstLemma  `callbyvalueall\_seq-spread0`  [\mkleeneopen{}F\mkleeneclose{};\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}H\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index