---

Step * of Lemma cbva_seq-combine2

∀[F,L1,L2:Top]. ∀[m1,m2:ℕ].
  (cbva_seq(L1; λg.cbva_seq(L2[g]; F[g]; m2); m1) ~ cbva_seq(λn.if n <z m1
                                                                then L1 n
                                                                else mk_lambdas_fun(λg.(L2[g] (n - m1));m1)
                                                                fi ; λg.(F[partial_ap(g;m1 + m2;m1)] 
                                                                         partial_ap_gen(g;m1 + m2;m1;m2)); m1 + m2))
BY
{ ((UnivCD THENA Auto) THEN RepUR ``cbva_seq`` 0 THEN BLemma `callbyvalueall_seq-combine3-0` THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[F,L1,L2:Top].  \mforall{}[m1,m2:\mBbbN{}].
    (cbva\_seq(L1;  \mlambda{}g.cbva\_seq(L2[g];  F[g];  m2);  m1)  \msim{}  cbva\_seq(\mlambda{}n.if  n  <z  m1
                                                                                                                                then  L1  n
                                                                                                                                else  mk\_lambdas\_fun(\mlambda{}g.(L2[g] 
                                                                                                                                                                                (n 
                                                                                                                                                                                -  m1));m1)
                                                                                                                                fi  ;  \mlambda{}g.(F[partial\_ap(g;m1
                                                                                                                                                  +  m2;m1)] 
                                                                                                                                                  partial\_ap\_gen(g;m1
                                                                                                                                                  +  m2;m1;m2));  m1  +  m2))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RepUR  ``cbva\_seq``  0
  THEN  BLemma  `callbyvalueall\_seq-combine3-0`
  THEN  Auto)

---

Home Index