Proof of Nuprl Lemma : callbyvalueall

Step * 2 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
{ ((D (-6) THENA Auto)
   THEN RW (AddrC [1] (RecUnfoldTopC `callbyvalueall_seq`)) 0
   THEN RW (AddrC [2] (RecUnfoldTopC `callbyvalueall_seq`)) 0
   THEN Reduce 0
   THEN (RWO "mk_applies_lambdas" 0 THENA Auto')
   THEN Repeat ((AutoSplit THEN Try (Complete (Auto'))))
   THEN MemCD
   THEN Try (Complete (Auto))) }

1
1. F : Top
2. L1 : Top
3. L2 : Top
4. m2 : ℕ
5. k : ℤ
6. 0 < k
7. 0 < k
8. K : Top
9. n : ℤ
10. ¬((n + k) ≤ n)
11. 0 ≤ n
12. ¬(k = 1 ∈ ℤ)
13. ∀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)))

14. v : Base
⊢ callbyvalueall_seq(L1;λf.(mk_applies(f;K;n) v);λg.(g

                                                     mk_lambdas(λout.callbyvalueall_seq(L2[out];λx.x;λg.(g F[m2]);0

                                                                                       ;m2);(n + k) - 1));n + 1;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) v);λg.(g mk_lambdas(F[m2];n + k));n + 1;(n + k) + 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. \mneg{}(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: ((D (-6) THENA Auto) THEN RW (AddrC [1] (RecUnfoldTopC `callbyvalueall\_seq`)) 0 THEN RW (AddrC [2] (RecUnfoldTopC `callbyvalueall\_seq`)) 0 THEN Reduce 0 THEN (RWO "mk\_applies\_lambdas" 0 THENA Auto') THEN Repeat ((AutoSplit THEN Try (Complete (Auto')))) THEN MemCD THEN Try (Complete (Auto))) Home Index