---

Step * of Lemma cbva_seq-combine

∀[F,L1,L2:Top]. ∀[m1,m2:ℕ].
  (cbva_seq(L1; λg.cbva_seq(L2[g]; F; 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_gen(g;m1 + m2;m1;m2)); m1 + m2))
BY
{ ((UnivCD THENA Auto) THEN RepUR ``cbva_seq`` 0 THEN BLemma `callbyvalueall_seq-combine2-0` THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[F,L1,L2:Top].  \mforall{}[m1,m2:\mBbbN{}].
    (cbva\_seq(L1;  \mlambda{}g.cbva\_seq(L2[g];  F;  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\_gen(g;m1
                                                                                                                                            +  m2;m1;m2));  m1  +  m2))


By

---

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

---

Home Index