---

Step * 1 of Lemma callbyvalueall_seq-combine3


1. F : Top
2. L1 : Top
3. L2 : Top
4. m2 : ℕ
5. k : ℤ
6. K : Top
7. n : ℤ
8. 0 ≤ n
⊢ callbyvalueall_seq(L1;λf.mk_applies(f;K;n);λg.callbyvalueall_seq(L2[g];λx.x;F[g];0;m2);n;n + 0) 
~ callbyvalueall_seq(λi.if i <z n + 0 then L1 i else mk_lambdas_fun(λg.(L2[g] (i - n + 0));n + 0) fi 
                    ;λf.mk_applies(f;K;n);λg.(F[partial_ap(g;(n + 0) + m2;n + 0)] 
                                              partial_ap_gen(g;(n + 0) + m2;n + 0;m2));n;(n + 0) + m2)
BY
{ ((Subst ⌜n + 0 ~ n⌝ 0⋅ THENA Auto)
   THEN RW (AddrC [1] (RecUnfoldTopC `callbyvalueall_seq`)) 0
   THEN AutoSplit
   THEN (Subst ⌜n ~ 0 + n⌝ 0⋅ THENA Auto)
   THEN (Subst ⌜(0 + n) + m2 ~ m2 + n⌝ 0⋅ THENA Auto)
   THEN (RWO "callbyvalueall_seq-shift<" 0 THENA Auto)
   THEN (Subst ⌜0 + n ~ n⌝ 0⋅ THENA Auto)
   THEN Reduce 0
   THEN (RWO "callbyvalueall_seq-shift-init0" 0 THENA Auto)
   THEN Reduce 0
   THEN (RWO "mk_applies_ite" 0 THENA Auto)
   THEN (RWO "callbyvalueall_seq-fun1" 0 THENA Auto)
   THEN Try (Complete (Auto))
   THEN (RWO "mk_applies_lambdas_fun0" 0 THENA Auto)
   THEN Reduce 0
   THEN (RWO "callbyvalueall_seq-eta" 0 THENA Auto)
   THEN Try (Complete (Auto'))
   THEN RepUR ``partial_ap_gen partial_ap`` 0
   THEN (Subst ⌜(m2 + n) - m2 - n ~ 0⌝ 0⋅ THENA Auto)
   THEN (Subst ⌜(m2 + n) - n ~ m2⌝ 0⋅ THENA Auto)
   THEN (RWO "mk_applies_lambdas" 0 THENA Auto)
   THEN (RWO "mk_applies_lambdas_fun0" 0 THENA Auto)
   THEN Reduce 0
   THEN (Subst ⌜n - n ~ 0⌝ 0⋅ THENA Auto)
   THEN RepUR ``mk_lambdas`` 0
   THEN Try (Fold `mk_lambdas` 0)
   THEN (Subst ⌜λg.(F[λf.(g mk_lambdas(mk_applies(f;K;n);m2))] (λf.(g mk_lambdas_fun(λh.(h f);m2)))) 
                ~ λg.(F[λf.(g mk_lambdas(mk_applies(f;K;n);m2))] partial_ap(g;m2;m2))⌝ 0⋅
         THENA (RepUR ``partial_ap`` 0 THEN (Subst ⌜m2 - m2 ~ 0⌝ 0⋅ THENA Auto) THEN RepUR ``mk_lambdas`` 0 THEN Auto)
         )
   THEN (InstLemma `callbyvalueall_seq-lambdas-all0` [⌜L2[λx.mk_applies(x;K;n)]⌝;⌜λ2f.mk_applies(f;K;n)⌝;
         ⌜λ2g.partial_ap(g;m2;m2)⌝;⌜λ2p.F[p]⌝;⌜m2⌝]⋅
         THENA Auto
         )
   THEN RWO "-1<" 0
   THEN RWO "callbyvalueall_seq-partial-ap-all0<" 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  F  :  Top
2.  L1  :  Top
3.  L2  :  Top
4.  m2  :  \mBbbN{}
5.  k  :  \mBbbZ{}
6.  K  :  Top
7.  n  :  \mBbbZ{}
8.  0  \mleq{}  n
\mvdash{}  callbyvalueall\_seq(L1;\mlambda{}f.mk\_applies(f;K;n);\mlambda{}g.callbyvalueall\_seq(L2[g];\mlambda{}x.x;F[g];0;m2);n;n  +  0) 
\msim{}  callbyvalueall\_seq(\mlambda{}i.if  i  <z  n  +  0
                                                then  L1  i
                                                else  mk\_lambdas\_fun(\mlambda{}g.(L2[g]  (i  -  n  +  0));n  +  0)
                                                fi  ;\mlambda{}f.mk\_applies(f;K;n);\mlambda{}g.(F[partial\_ap(g;(n  +  0)  +  m2;n  +  0)] 
                                                                                                          partial\_ap\_gen(g;(n  +  0)  +  m2;n  +  0;m2));n;(n
                                        +  0)
                                        +  m2)


By

---

Latex:
((Subst  \mkleeneopen{}n  +  0  \msim{}  n\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  RW  (AddrC  [1]  (RecUnfoldTopC  `callbyvalueall\_seq`))  0
  THEN  AutoSplit
  THEN  (Subst  \mkleeneopen{}n  \msim{}  0  +  n\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  (Subst  \mkleeneopen{}(0  +  n)  +  m2  \msim{}  m2  +  n\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  (RWO  "callbyvalueall\_seq-shift<"  0  THENA  Auto)
  THEN  (Subst  \mkleeneopen{}0  +  n  \msim{}  n\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  Reduce  0
  THEN  (RWO  "callbyvalueall\_seq-shift-init0"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  (RWO  "mk\_applies\_ite"  0  THENA  Auto)
  THEN  (RWO  "callbyvalueall\_seq-fun1"  0  THENA  Auto)
  THEN  Try  (Complete  (Auto))
  THEN  (RWO  "mk\_applies\_lambdas\_fun0"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  (RWO  "callbyvalueall\_seq-eta"  0  THENA  Auto)
  THEN  Try  (Complete  (Auto'))
  THEN  RepUR  ``partial\_ap\_gen  partial\_ap``  0
  THEN  (Subst  \mkleeneopen{}(m2  +  n)  -  m2  -  n  \msim{}  0\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  (Subst  \mkleeneopen{}(m2  +  n)  -  n  \msim{}  m2\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  (RWO  "mk\_applies\_lambdas"  0  THENA  Auto)
  THEN  (RWO  "mk\_applies\_lambdas\_fun0"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  (Subst  \mkleeneopen{}n  -  n  \msim{}  0\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  RepUR  ``mk\_lambdas``  0
  THEN  Try  (Fold  `mk\_lambdas`  0)
  THEN  (Subst  \mkleeneopen{}\mlambda{}g.(F[\mlambda{}f.(g  mk\_lambdas(mk\_applies(f;K;n);m2))]  (\mlambda{}f.(g  mk\_lambdas\_fun(\mlambda{}h.(h  f);m2)))) 
                            \msim{}  \mlambda{}g.(F[\mlambda{}f.(g  mk\_lambdas(mk\_applies(f;K;n);m2))]  partial\_ap(g;m2;m2))\mkleeneclose{}  0\mcdot{}
              THENA  (RepUR  ``partial\_ap``  0
                            THEN  (Subst  \mkleeneopen{}m2  -  m2  \msim{}  0\mkleeneclose{}  0\mcdot{}  THENA  Auto)
                            THEN  RepUR  ``mk\_lambdas``  0
                            THEN  Auto)
              )
  THEN  (InstLemma  `callbyvalueall\_seq-lambdas-all0`  [\mkleeneopen{}L2[\mlambda{}x.mk\_applies(x;K;n)]\mkleeneclose{};
              \mkleeneopen{}\mlambda{}\msubtwo{}f.mk\_applies(f;K;n)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}g.partial\_ap(g;m2;m2)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}p.F[p]\mkleeneclose{};\mkleeneopen{}m2\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  RWO  "-1<"  0
  THEN  RWO  "callbyvalueall\_seq-partial-ap-all0<"  0
  THEN  Auto)

---

Home Index