---

Step * of Lemma simple-cbva-seq-combine

∀[F,L1,L2:Top]. ∀[m1,m2:ℕ+].
  (simple-cbva-seq(L1;λout.simple-cbva-seq(L2[out];F;m2);m1) ~ simple-cbva-seq(λn.if n <z m1
                                                                                  then L1 n
                                                                                  else mk_lambdas(λout.(L2[out] 
                                                                                                        (n - m1));m1 
                                                                                       - 1)
                                                                                  fi ;F;m1 + m2))
BY
{ xxx((UnivCD THENA Auto)
      THEN RepUR ``simple-cbva-seq cbva-seq`` 0
      THEN RepeatFor 2 (AutoSplit)
      THEN RepeatFor 2 ((RWO "callbyvalueall_seq-seq" 0 THENA Auto'))
      THEN (InstLemma `callbyvalueall_seq-combine0` [⌜λ2m2.mk_lambdas(F;m2 - 1)⌝;⌜L1⌝;⌜L2⌝;⌜m1⌝;⌜m2⌝]⋅ THENA Auto)
      THEN RWO "-1" 0
      THEN (RWO "mk_lambdas_compose" 0⋅ THENA Auto)
      THEN Subst ⌜(m2 - 1) + m1 ~ (m1 + m2) - 1⌝ 0⋅
      THEN Auto)xxx }

---

Latex:

---

Latex:
\mforall{}[F,L1,L2:Top].  \mforall{}[m1,m2:\mBbbN{}\msupplus{}].
    (simple-cbva-seq(L1;\mlambda{}out.simple-cbva-seq(L2[out];F;m2);m1) 
    \msim{}  simple-cbva-seq(\mlambda{}n.if  n  <z  m1  then  L1  n  else  mk\_lambdas(\mlambda{}out.(L2[out]  (n  -  m1));m1  -  1)  fi  ;F;m1
    +  m2))


By

---

Latex:
xxx((UnivCD  THENA  Auto)
        THEN  RepUR  ``simple-cbva-seq  cbva-seq``  0
        THEN  RepeatFor  2  (AutoSplit)
        THEN  RepeatFor  2  ((RWO  "callbyvalueall\_seq-seq"  0  THENA  Auto'))
        THEN  (InstLemma  `callbyvalueall\_seq-combine0`  [\mkleeneopen{}\mlambda{}\msubtwo{}m2.mk\_lambdas(F;m2  -  1)\mkleeneclose{};\mkleeneopen{}L1\mkleeneclose{};\mkleeneopen{}L2\mkleeneclose{};\mkleeneopen{}m1\mkleeneclose{};\mkleeneopen{}m2\mkleeneclose{}]\mcdot{}
                    THENA  Auto
                    )
        THEN  RWO  "-1"  0
        THEN  (RWO  "mk\_lambdas\_compose"  0\mcdot{}  THENA  Auto)
        THEN  Subst  \mkleeneopen{}(m2  -  1)  +  m1  \msim{}  (m1  +  m2)  -  1\mkleeneclose{}  0\mcdot{}
        THEN  Auto)xxx

---

Home Index