---

Step * 1 of Lemma callbyvalueall_seq-combine


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)
BY
{ (HypSubst' (-1) 0
   THEN (Subst ⌜(n + 1) - 1 ~ n⌝ 0⋅ THENA Auto)
   THEN RW (AddrC [1] (RecUnfoldTopC `callbyvalueall_seq`)) 0
   THEN AutoSplit
   THEN RW (AddrC [1;2] (RecUnfoldTopC `callbyvalueall_seq`)) 0
   THEN AutoSplit
   THEN (RWO "mk_applies_lambdas2" 0 THENA Auto)
   THEN Reduce 0
   THEN RW (AddrC [2] (RecUnfoldTopC `callbyvalueall_seq`)) 0
   THEN AutoSplit
   THEN EqCD
   THEN Try (Trivial)) }

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. ¬(((n + 1) + m2) ≤ n)
12. ¬((n + 1) ≤ n)
13. 0 ≤ n
14. k = 1 ∈ ℤ
15. (n + 1) ≤ (n + 1)
16. v : Base
⊢ callbyvalueall_seq(L2[v];λx.x;λg.(g F[m2]);0;m2) 
~ callbyvalueall_seq(λi.if i <z n + 1 then L1 i else mk_lambdas(λout.(L2[out] (i - n + 1));n) fi ;λf.(mk_applies(f;K;n) 
                                                                                                      v)
                    ;λg.(g mk_lambdas(F[m2];n + 1));n + 1;(n + 1) + m2)

---

Latex:

---

Latex:

1.  F  :  Top
2.  L1  :  Top
3.  L2  :  Top
4.  m2  :  \mBbbN{}
5.  k  :  \mBbbZ{}
6.  0  <  k
7.  0  <  k  -  1
{}\mRightarrow{}  (\mforall{}K:Top.  \mforall{}n:\mBbbZ{}.
            ((0  \mleq{}  n)
            {}\mRightarrow{}  (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);(n  +  (k  -  1))  -  1));n;n
                                                        +  (k  -  1)) 
                  \msim{}  callbyvalueall\_seq(\mlambda{}i.if  i  <z  n  +  (k  -  1)
                                                                  then  L1  i
                                                                  else  mk\_lambdas(\mlambda{}out.(L2[out]  (i  -  n  +  (k  -  1)));(n  +  (k  -  1))  -  1)
                                                                  fi  ;\mlambda{}f.mk\_applies(f;K;n);\mlambda{}g.(g  mk\_lambdas(F[m2];n  +  (k  -  1)));n;(n
                                                          +  (k  -  1))
                                                          +  m2))))
8.  0  <  k
9.  K  :  Top
10.  n  :  \mBbbZ{}
11.  0  \mleq{}  n
12.  k  =  1
\mvdash{}  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);(n  +  k) 
                                                                                                  -  1));n;n  +  k) 
\msim{}  callbyvalueall\_seq(\mlambda{}i.if  i  <z  n  +  k
                                                then  L1  i
                                                else  mk\_lambdas(\mlambda{}out.(L2[out]  (i  -  n  +  k));(n  +  k)  -  1)
                                                fi  ;\mlambda{}f.mk\_applies(f;K;n);\mlambda{}g.(g  mk\_lambdas(F[m2];n  +  k));n;(n  +  k)  +  m2)


By

---

Latex:
(HypSubst'  (-1)  0
  THEN  (Subst  \mkleeneopen{}(n  +  1)  -  1  \msim{}  n\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  RW  (AddrC  [1]  (RecUnfoldTopC  `callbyvalueall\_seq`))  0
  THEN  AutoSplit
  THEN  RW  (AddrC  [1;2]  (RecUnfoldTopC  `callbyvalueall\_seq`))  0
  THEN  AutoSplit
  THEN  (RWO  "mk\_applies\_lambdas2"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  RW  (AddrC  [2]  (RecUnfoldTopC  `callbyvalueall\_seq`))  0
  THEN  AutoSplit
  THEN  EqCD
  THEN  Try  (Trivial))

---

Home Index