---

Step * of Lemma cbva_seq_extend

∀[F,G,L:Top]. ∀[m:ℕ].
  (cbva_seq(L; λg.let x ⟵ F[g]
                  in G[g;x]; m) ~ cbva_seq(λn.if (n =z m) then mk_lambdas_fun(λg.F[g];m) else L n fi ;
                                           λg.G[partial_ap(g;m + 1;m);select_fun_ap(g;m + 1;m)]; m + 1))
BY
{ ((UnivCD THENA Auto)
   THEN (InstLemma `callbyvalueall_seq-extend` [⌜F⌝;⌜G⌝;⌜L⌝;⌜λx.x⌝;⌜m⌝;⌜0⌝]⋅ THENA Auto)
   THEN RepUR ``mk_applies`` (-1)
   THEN Fold `cbva_seq` (-1)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[F,G,L:Top].  \mforall{}[m:\mBbbN{}].
    (cbva\_seq(L;  \mlambda{}g.let  x  \mleftarrow{}{}  F[g]
                                    in  G[g;x];  m) 
    \msim{}  cbva\_seq(\mlambda{}n.if  (n  =\msubz{}  m)  then  mk\_lambdas\_fun(\mlambda{}g.F[g];m)  else  L  n  fi  ;
                          \mlambda{}g.G[partial\_ap(g;m  +  1;m);select\_fun\_ap(g;m  +  1;m)];  m  +  1))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (InstLemma  `callbyvalueall\_seq-extend`  [\mkleeneopen{}F\mkleeneclose{};\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{};\mkleeneopen{}\mlambda{}x.x\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepUR  ``mk\_applies``  (-1)
  THEN  Fold  `cbva\_seq`  (-1)
  THEN  Auto)

---

Home Index