---

Step * 1 of Lemma callbyvalueall_seq-partial-ap-all


1. L : Top
2. F : Top
3. k : ℤ
4. K : Top
5. n : ℤ
6. 0 ≤ n
⊢ callbyvalueall_seq(L;λf.mk_applies(f;K;n);F;n;n + 0) ~ callbyvalueall_seq(L;λf.mk_applies(f;K;n);λg.(F 
                                                                                                       partial_ap(g;n
                                                                                                       + 0;n + 0));n;n
                                                                           + 0)
BY
{ ((Subst ⌜n + 0 ~ n⌝ 0⋅ THENA Auto)
   THEN RecUnfold `callbyvalueall_seq` 0
   THEN AutoSplit
   THEN RepUR ``partial_ap`` 0
   THEN (Subst ⌜n - n ~ 0⌝ 0⋅ THENA Auto)
   THEN RepUR ``mk_lambdas`` 0
   THEN (RWO "mk_applies_lambdas_fun" 0 THENA Auto)
   THEN Reduce 0
   THEN (Subst ⌜n - n ~ 0⌝ 0⋅ THENA Auto)
   THEN RepUR ``mk_lambdas_fun`` 0
   THEN RecUnfold `mk_lambdas-fun` 0
   THEN AutoSplit) }

---

Latex:

---

Latex:

1.  L  :  Top
2.  F  :  Top
3.  k  :  \mBbbZ{}
4.  K  :  Top
5.  n  :  \mBbbZ{}
6.  0  \mleq{}  n
\mvdash{}  callbyvalueall\_seq(L;\mlambda{}f.mk\_applies(f;K;n);F;n;n  +  0) 
\msim{}  callbyvalueall\_seq(L;\mlambda{}f.mk\_applies(f;K;n);\mlambda{}g.(F  partial\_ap(g;n  +  0;n  +  0));n;n  +  0)


By

---

Latex:
((Subst  \mkleeneopen{}n  +  0  \msim{}  n\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  RecUnfold  `callbyvalueall\_seq`  0
  THEN  AutoSplit
  THEN  RepUR  ``partial\_ap``  0
  THEN  (Subst  \mkleeneopen{}n  -  n  \msim{}  0\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  RepUR  ``mk\_lambdas``  0
  THEN  (RWO  "mk\_applies\_lambdas\_fun"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  (Subst  \mkleeneopen{}n  -  n  \msim{}  0\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  RepUR  ``mk\_lambdas\_fun``  0
  THEN  RecUnfold  `mk\_lambdas-fun`  0
  THEN  AutoSplit)

---

Home Index