Step
*
1
1
of Lemma
callbyvalueall_seq-shift-init
1. L : Top
2. F : Top
3. k : ℤ
4. 0 < k
5. ∀K:Top. ∀n,p,q:ℕ.
(callbyvalueall_seq(L;λf.mk_applies(f;K;p + q);F;n;n + (k - 1))
~ callbyvalueall_seq(λi.mk_applies(L i;K;p);λf.mk_applies(f;λi.(K (p + i));q);λg.(F (λf.(g mk_applies(f;K;p))));n;n
+ (k - 1)))
6. K : Top
7. n : ℕ
8. ¬((n + k) ≤ n)
9. p : ℕ
10. q : ℕ
11. v : Base
12. callbyvalueall_seq(L;λf.mk_applies(f;λi.if (i =z p + q) then v else K i fi ;p + q + 1);F;n + 1;n + k)
~ callbyvalueall_seq(λi.mk_applies(L i;λi.if (i =z p + q) then v else K i fi ;p);λf.mk_applies(f;λi.if (p + i =z p + q)
then v
else K (p + i)
fi ;q + 1)
;λg.(F (λf.(g mk_applies(f;λi.if (i =z p + q) then v else K i fi ;p))));n + 1;n + k)
⊢ callbyvalueall_seq(L;λf.(mk_applies(f;K;p + q) v);F;n + 1;n + k)
~ callbyvalueall_seq(λi.mk_applies(L i;K;p);λf.(mk_applies(f;λi.(K (p + i));q) v);λg.(F (λf.(g mk_applies(f;K;p))));n
+ 1;n + k)
BY
{ ((RW (AddrC [1;2;1] (LemmaC `mk_applies_unroll`)) (-1) THENA Auto')
THEN Reduce (-1)
THEN SplitOnHypITE (-1)
THEN Try (Complete (Auto))
THEN (RW (AddrC [1;2;1;1] (LemmaC `mk_applies_fun`)) (-2) THENA Auto')
THEN Thin (-1)
THEN (Subst ⌜(p + q + 1) - 1 ~ p + q⌝ (-1)⋅ THENA Auto)
THEN RWO "-1" 0) }
1
1. L : Top
2. F : Top
3. k : ℤ
4. 0 < k
5. ∀K:Top. ∀n,p,q:ℕ.
(callbyvalueall_seq(L;λf.mk_applies(f;K;p + q);F;n;n + (k - 1))
~ callbyvalueall_seq(λi.mk_applies(L i;K;p);λf.mk_applies(f;λi.(K (p + i));q);λg.(F (λf.(g mk_applies(f;K;p))));n;n
+ (k - 1)))
6. K : Top
7. n : ℕ
8. ¬((n + k) ≤ n)
9. p : ℕ
10. q : ℕ
11. v : Base
12. callbyvalueall_seq(L;λf.(mk_applies(f;K;p + q) v);F;n + 1;n + k)
~ callbyvalueall_seq(λi.mk_applies(L i;λi.if (i =z p + q) then v else K i fi ;p);λf.mk_applies(f;λi.if (p + i =z p + q)
then v
else K (p + i)
fi ;q + 1)
;λg.(F (λf.(g mk_applies(f;λi.if (i =z p + q) then v else K i fi ;p))));n + 1;n + k)
⊢ callbyvalueall_seq(λi.mk_applies(L i;λi.if (i =z p + q) then v else K i fi ;p);λf.mk_applies(f;λi.if (p + i =z p + q)
then v
else K (p + i)
fi ;q + 1)
;λg.(F (λf.(g mk_applies(f;λi.if (i =z p + q) then v else K i fi ;p))));n + 1;n + k)
~ callbyvalueall_seq(λi.mk_applies(L i;K;p);λf.(mk_applies(f;λi.(K (p + i));q) v);λg.(F (λf.(g mk_applies(f;K;p))));n
+ 1;n + k)
Latex:
Latex:
1. L : Top
2. F : Top
3. k : \mBbbZ{}
4. 0 < k
5. \mforall{}K:Top. \mforall{}n,p,q:\mBbbN{}.
(callbyvalueall\_seq(L;\mlambda{}f.mk\_applies(f;K;p + q);F;n;n + (k - 1))
\msim{} callbyvalueall\_seq(\mlambda{}i.mk\_applies(L i;K;p);\mlambda{}f.mk\_applies(f;\mlambda{}i.(K (p + i));q)
;\mlambda{}g.(F (\mlambda{}f.(g mk\_applies(f;K;p))));n;n + (k - 1)))
6. K : Top
7. n : \mBbbN{}
8. \mneg{}((n + k) \mleq{} n)
9. p : \mBbbN{}
10. q : \mBbbN{}
11. v : Base
12. callbyvalueall\_seq(L;\mlambda{}f.mk\_applies(f;\mlambda{}i.if (i =\msubz{} p + q) then v else K i fi ;p + q + 1);F;n + 1;n
+ k) \msim{} callbyvalueall\_seq(\mlambda{}i.mk\_applies(L i;\mlambda{}i.if (i =\msubz{} p + q)
then v
else K i
fi ;p)
;\mlambda{}f.mk\_applies(f;\mlambda{}i.if (p + i =\msubz{} p + q)
then v
else K (p + i)
fi ;q + 1)
;\mlambda{}g.(F
(\mlambda{}f.(g
mk\_applies(f;\mlambda{}i.if (i =\msubz{} p + q)
then v
else K i
fi ;p))));n + 1;n + k)
\mvdash{} callbyvalueall\_seq(L;\mlambda{}f.(mk\_applies(f;K;p + q) v);F;n + 1;n + k)
\msim{} callbyvalueall\_seq(\mlambda{}i.mk\_applies(L i;K;p);\mlambda{}f.(mk\_applies(f;\mlambda{}i.(K (p + i));q) v)
;\mlambda{}g.(F (\mlambda{}f.(g mk\_applies(f;K;p))));n + 1;n + k)
By
Latex:
((RW (AddrC [1;2;1] (LemmaC `mk\_applies\_unroll`)) (-1) THENA Auto')
THEN Reduce (-1)
THEN SplitOnHypITE (-1)
THEN Try (Complete (Auto))
THEN (RW (AddrC [1;2;1;1] (LemmaC `mk\_applies\_fun`)) (-2) THENA Auto')
THEN Thin (-1)
THEN (Subst \mkleeneopen{}(p + q + 1) - 1 \msim{} p + q\mkleeneclose{} (-1)\mcdot{} THENA Auto)
THEN RWO "-1" 0)
Home
Index