---

Step * of Lemma callbyvalueall_seq-combine

∀[F,L1,L2,K:Top]. ∀[m1:ℕ+]. ∀[m2:ℕ]. ∀[n:ℕm1].
  (callbyvalueall_seq(L1;λf.mk_applies(f;K;n);λg.(g 
                                                  mk_lambdas(λout.callbyvalueall_seq(L2[out];λx.x;λg.(g F[m2]);0;m2);m1 
                                                  - 1));n;m1) 
  ~ callbyvalueall_seq(λi.if i <z m1 then L1 i else mk_lambdas(λout.(L2[out] (i - m1));m1 - 1) fi ;λf.mk_applies(f;K;n)
                      ;λg.(g mk_lambdas(F[m2];m1));n;m1 + m2))
BY
{ ((UnivCD THENA Auto)
   THEN RepeatFor 2 ((D (-1) THENA Auto))
   THEN (Assert ⌜∃k:ℕ. (m1 = (n + k) ∈ ℤ)⌝⋅ THENA (InstConcl [⌜m1 - n⌝]⋅ THEN Auto'))
   THEN D (-1)
   THEN (Assert ⌜0 < k⌝⋅ THENA Auto')
   THEN (HypSubst' (-2) 0 THENA Auto)
   THEN ThinVar `m1'
   THEN RepeatFor 2 (MoveToConcl (-4))
   THEN NatInd (-2)
   THEN (UnivCD THENA Auto)
   THEN Try (Complete (Auto))
   THEN (Decide ⌜k = 1 ∈ ℤ⌝⋅ THENA Auto)) }

1
1. F : Top
2. L1 : Top
3. L2 : Top
4. m2 : ℕ
5. k : ℤ
6. 0 < k
7. 0 < k - 1
⇒ (∀K:Top. ∀n:ℤ.
      ((0 ≤ n)
      ⇒ (callbyvalueall_seq(L1;λf.mk_applies(f;K;n);λg.(g 
                                                         mk_lambdas(λout.callbyvalueall_seq(L2[out];λx.x;λg.(g F[m2]);0
                                                                                           ;m2);(n + (k - 1)) - 1));n;n
                            + (k - 1)) ~ callbyvalueall_seq(λi.if i <z n + (k - 1)
                                                               then L1 i
                                                               else mk_lambdas(λout.(L2[out] (i - n + (k - 1)));(n
                                                                    + (k - 1)) - 1)
                                                               fi ;λf.mk_applies(f;K;n);λg.(g 
                                                                                            mk_lambdas(F[m2];n
                                                                                            + (k - 1)));n;(n + (k - 1))
                                                           + m2))))
8. 0 < k
9. K : Top
10. n : ℤ
11. 0 ≤ n
12. k = 1 ∈ ℤ
⊢ callbyvalueall_seq(L1;λf.mk_applies(f;K;n);λg.(g 
                                                 mk_lambdas(λout.callbyvalueall_seq(L2[out];λx.x;λg.(g F[m2]);0;m2);(n
                                                 + k) - 1));n;n + k) 
~ callbyvalueall_seq(λi.if i <z n + k then L1 i else mk_lambdas(λout.(L2[out] (i - n + k));(n + k) - 1) fi 
                    ;λf.mk_applies(f;K;n);λg.(g mk_lambdas(F[m2];n + k));n;(n + k) + m2)

2
1. F : Top
2. L1 : Top
3. L2 : Top
4. m2 : ℕ
5. k : ℤ
6. 0 < k
7. 0 < k - 1
⇒ (∀K:Top. ∀n:ℤ.
      ((0 ≤ n)
      ⇒ (callbyvalueall_seq(L1;λf.mk_applies(f;K;n);λg.(g 
                                                         mk_lambdas(λout.callbyvalueall_seq(L2[out];λx.x;λg.(g F[m2]);0
                                                                                           ;m2);(n + (k - 1)) - 1));n;n
                            + (k - 1)) ~ callbyvalueall_seq(λi.if i <z n + (k - 1)
                                                               then L1 i
                                                               else mk_lambdas(λout.(L2[out] (i - n + (k - 1)));(n
                                                                    + (k - 1)) - 1)
                                                               fi ;λf.mk_applies(f;K;n);λg.(g 
                                                                                            mk_lambdas(F[m2];n
                                                                                            + (k - 1)));n;(n + (k - 1))
                                                           + m2))))
8. 0 < k
9. K : Top
10. n : ℤ
11. 0 ≤ n
12. ¬(k = 1 ∈ ℤ)
⊢ callbyvalueall_seq(L1;λf.mk_applies(f;K;n);λg.(g 
                                                 mk_lambdas(λout.callbyvalueall_seq(L2[out];λx.x;λg.(g F[m2]);0;m2);(n
                                                 + k) - 1));n;n + k) 
~ callbyvalueall_seq(λi.if i <z n + k then L1 i else mk_lambdas(λout.(L2[out] (i - n + k));(n + k) - 1) fi 
                    ;λf.mk_applies(f;K;n);λg.(g mk_lambdas(F[m2];n + k));n;(n + k) + m2)

---

Latex:

---

Latex:
\mforall{}[F,L1,L2,K:Top].  \mforall{}[m1:\mBbbN{}\msupplus{}].  \mforall{}[m2:\mBbbN{}].  \mforall{}[n:\mBbbN{}m1].
    (callbyvalueall\_seq(L1;\mlambda{}f.mk\_applies(f;K;n);\mlambda{}g.(g 
                                                                                                    mk\_lambdas(\mlambda{}out.callbyvalueall\_seq(L2[out];\mlambda{}x.x
                                                                                                                                                                        ;\mlambda{}g.(g  F[m2]);0
                                                                                                                                                                        ;m2);m1  -  1));n
                                          ;m1)  \msim{}  callbyvalueall\_seq(\mlambda{}i.if  i  <z  m1
                                                                                                    then  L1  i
                                                                                                    else  mk\_lambdas(\mlambda{}out.(L2[out]  (i  -  m1));m1  -  1)
                                                                                                    fi  ;\mlambda{}f.mk\_applies(f;K;n);\mlambda{}g.(g 
                                                                                                                                                              mk\_lambdas(F[m2];m1))
                                                                                            ;n;m1  +  m2))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RepeatFor  2  ((D  (-1)  THENA  Auto))
  THEN  (Assert  \mkleeneopen{}\mexists{}k:\mBbbN{}.  (m1  =  (n  +  k))\mkleeneclose{}\mcdot{}  THENA  (InstConcl  [\mkleeneopen{}m1  -  n\mkleeneclose{}]\mcdot{}  THEN  Auto'))
  THEN  D  (-1)
  THEN  (Assert  \mkleeneopen{}0  <  k\mkleeneclose{}\mcdot{}  THENA  Auto')
  THEN  (HypSubst'  (-2)  0  THENA  Auto)
  THEN  ThinVar  `m1'
  THEN  RepeatFor  2  (MoveToConcl  (-4))
  THEN  NatInd  (-2)
  THEN  (UnivCD  THENA  Auto)
  THEN  Try  (Complete  (Auto))
  THEN  (Decide  \mkleeneopen{}k  =  1\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index