---

Step * 1 of Lemma callbyvalueall_seq-extend


1. F : Top
2. G : Top
3. L : Top
4. i : ℤ
5. K : Top
6. n : ℤ
7. 0 ≤ n
⊢ callbyvalueall_seq(L;λf.mk_applies(f;K;n);λg.let x ⟵ F[g]
                                               in G[g;x];n;n + 0) 
~ callbyvalueall_seq(λn@0.if (n@0 =z n + 0) then mk_lambdas_fun(λg.F[g];n + 0) else L n@0 fi ;λf.mk_applies(f;K;n)
                    ;λg.G[partial_ap(g;(n + 0) + 1;n + 0);select_fun_ap(g;(n + 0) + 1;n + 0)];n;(n + 0) + 1)
BY
{ ((Subst ⌜n + 0 ~ n⌝ 0⋅ THENA Auto)
   THEN RepeatFor 2 ((RecUnfold `callbyvalueall_seq` 0 THEN Repeat (AutoSplit)))
   THEN (RWO "mk_applies_lambdas_fun0" 0 THENA Auto)
   THEN Reduce 0
   THEN MemCD
   THEN Try (Complete (Auto))
   THEN (RWO "mk_applies_roll" 0 THENA Auto)
   THEN RepUR ``partial_ap mk_lambdas`` 0
   THEN (Subst ⌜(n + 1) - n ~ 1⌝ 0⋅ THENA Auto)
   THEN Reduce 0
   THEN (RWO "mk_applies_lambdas_fun1" 0 THENA Auto)
   THEN Reduce 0
   THEN (Subst ⌜(n + 1) - n ~ 1⌝ 0⋅ THENA Auto)
   THEN RW (AddrC [2;2;1] (UnfoldTopC `mk_applies`)) 0
   THEN (RWO "primrec-unroll" 0 THENA Auto)
   THEN Reduce 0
   THEN (RW (AddrC [2;2;1] (LemmaC `mk_applies_fun`)) 0 THENA Auto)
   THEN RepUR ``select_fun_ap`` 0
   THEN (Subst ⌜(n + 1) - n - 1 ~ 0⌝ 0⋅ THENA Auto)
   THEN RepUR ``mk_lambdas`` 0
   THEN Fold `mk_lambdas` 0
   THEN (RWO "mk_applies_lambdas1" 0 THENA Auto)
   THEN Reduce 0
   THEN (Subst ⌜(n + 1) - n ~ 1⌝ 0⋅ THENA Auto)
   THEN RW (AddrC [2;3] (UnfoldC `mk_applies`)) 0
   THEN Reduce 0
   THEN AutoSplit) }

---

Latex:

---

Latex:

1.  F  :  Top
2.  G  :  Top
3.  L  :  Top
4.  i  :  \mBbbZ{}
5.  K  :  Top
6.  n  :  \mBbbZ{}
7.  0  \mleq{}  n
\mvdash{}  callbyvalueall\_seq(L;\mlambda{}f.mk\_applies(f;K;n);\mlambda{}g.let  x  \mleftarrow{}{}  F[g]
                                                                                              in  G[g;x];n;n  +  0) 
\msim{}  callbyvalueall\_seq(\mlambda{}n@0.if  (n@0  =\msubz{}  n  +  0)  then  mk\_lambdas\_fun(\mlambda{}g.F[g];n  +  0)  else  L  n@0  fi 
                                        ;\mlambda{}f.mk\_applies(f;K;n);\mlambda{}g.G[partial\_ap(g;(n  +  0)  +  1;n  +  0);select\_fun\_ap(g;(n
                                                                                          +  0)
                                                                                          +  1;n  +  0)];n;(n  +  0)  +  1)


By

---

Latex:
((Subst  \mkleeneopen{}n  +  0  \msim{}  n\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  ((RecUnfold  `callbyvalueall\_seq`  0  THEN  Repeat  (AutoSplit)))
  THEN  (RWO  "mk\_applies\_lambdas\_fun0"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  MemCD
  THEN  Try  (Complete  (Auto))
  THEN  (RWO  "mk\_applies\_roll"  0  THENA  Auto)
  THEN  RepUR  ``partial\_ap  mk\_lambdas``  0
  THEN  (Subst  \mkleeneopen{}(n  +  1)  -  n  \msim{}  1\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  Reduce  0
  THEN  (RWO  "mk\_applies\_lambdas\_fun1"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  (Subst  \mkleeneopen{}(n  +  1)  -  n  \msim{}  1\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  RW  (AddrC  [2;2;1]  (UnfoldTopC  `mk\_applies`))  0
  THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  (RW  (AddrC  [2;2;1]  (LemmaC  `mk\_applies\_fun`))  0  THENA  Auto)
  THEN  RepUR  ``select\_fun\_ap``  0
  THEN  (Subst  \mkleeneopen{}(n  +  1)  -  n  -  1  \msim{}  0\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  RepUR  ``mk\_lambdas``  0
  THEN  Fold  `mk\_lambdas`  0
  THEN  (RWO  "mk\_applies\_lambdas1"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  (Subst  \mkleeneopen{}(n  +  1)  -  n  \msim{}  1\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  RW  (AddrC  [2;3]  (UnfoldC  `mk\_applies`))  0
  THEN  Reduce  0
  THEN  AutoSplit)

---

Home Index