Step
*
1
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. ¬(((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)
BY
{ ((Subst ⌜n + 1 ~ 0 + n + 1⌝ 0⋅ THENA Auto)
THEN (Subst ⌜(0 + n + 1) + m2 ~ m2 + n + 1⌝ 0⋅ THENA Auto)
THEN (RWO "callbyvalueall_seq-shift<" 0 THENA Auto)
THEN (Subst ⌜0 + n + 1 ~ n + 1⌝ 0⋅ THENA Auto)
THEN Reduce 0
THEN (Subst ⌜λf.(mk_applies(f;K;n) v) ~ λf.mk_applies(f;λi.if (i =z n) then v else K i fi ;n + 1)⌝ 0⋅
THENA ((RW (AddrC [2;1] (LemmaC `mk_applies_unroll`)) 0 THENA Auto)
THEN Reduce 0
THEN AutoSplit
THEN (Subst ⌜(n + 1) - 1 ~ n⌝ 0⋅ THENA Auto)
THEN RWO "mk_applies_fun" 0
THEN Auto)
)
THEN (RWO "callbyvalueall_seq-shift-init0" 0 THENA Auto)
THEN Reduce 0
THEN (RWO "mk_applies_lambdas2" 0 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. ¬(((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.mk_applies(if i + n + 1 <z n + 1
then L1 (i + n + 1)
else mk_lambdas(λout.(L2[out]
((i + n + 1) - n
+ 1));n)
fi ;λi.if (i =z n) then v else K i fi ;n + 1)
;λx.x;λg.(g F[m2]);0;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. \mneg{}(((n + 1) + m2) \mleq{} n)
12. \mneg{}((n + 1) \mleq{} n)
13. 0 \mleq{} n
14. k = 1
15. (n + 1) \mleq{} (n + 1)
16. v : Base
\mvdash{} callbyvalueall\_seq(L2[v];\mlambda{}x.x;\mlambda{}g.(g F[m2]);0;m2)
\msim{} callbyvalueall\_seq(\mlambda{}i.if i <z n + 1 then L1 i else mk\_lambdas(\mlambda{}out.(L2[out] (i - n + 1));n) fi
;\mlambda{}f.(mk\_applies(f;K;n) v);\mlambda{}g.(g mk\_lambdas(F[m2];n + 1));n + 1;(n + 1) + m2)
By
Latex:
((Subst \mkleeneopen{}n + 1 \msim{} 0 + n + 1\mkleeneclose{} 0\mcdot{} THENA Auto)
THEN (Subst \mkleeneopen{}(0 + n + 1) + m2 \msim{} m2 + n + 1\mkleeneclose{} 0\mcdot{} THENA Auto)
THEN (RWO "callbyvalueall\_seq-shift<" 0 THENA Auto)
THEN (Subst \mkleeneopen{}0 + n + 1 \msim{} n + 1\mkleeneclose{} 0\mcdot{} THENA Auto)
THEN Reduce 0
THEN (Subst \mkleeneopen{}\mlambda{}f.(mk\_applies(f;K;n) v) \msim{} \mlambda{}f.mk\_applies(f;\mlambda{}i.if (i =\msubz{} n) then v else K i fi ;n + 1)\mkleeneclose{}
0\mcdot{}
THENA ((RW (AddrC [2;1] (LemmaC `mk\_applies\_unroll`)) 0 THENA Auto)
THEN Reduce 0
THEN AutoSplit
THEN (Subst \mkleeneopen{}(n + 1) - 1 \msim{} n\mkleeneclose{} 0\mcdot{} THENA Auto)
THEN RWO "mk\_applies\_fun" 0
THEN Auto)
)
THEN (RWO "callbyvalueall\_seq-shift-init0" 0 THENA Auto)
THEN Reduce 0
THEN (RWO "mk\_applies\_lambdas2" 0 THENA Auto))
Home
Index