---

Step * of Lemma callbyvalueall_seq-extend

∀[F,G,L,K:Top]. ∀[m:ℕ]. ∀[n:ℕm + 1].
  (callbyvalueall_seq(L;λf.mk_applies(f;K;n);λg.let x ⟵ F[g]
                                                in G[g;x];n;m) ~ callbyvalueall_seq(λn.if (n =z m)
                                                                                       then mk_lambdas_fun(λg.F[g];m)
                                                                                       else L n
                                                                                       fi ;λf.mk_applies(f;K;n)
                                                                                   ;λg.G[partial_ap(g;m
                                                                                       + 1;m);select_fun_ap(g;m + 1;m)]
                                                                                   ;n;m + 1))
BY
{ ((UnivCD THENA Auto)
   THEN (Assert ⌜∃i:ℕ. (m = (n + i) ∈ ℤ)⌝⋅ THENA (InstConcl [⌜m - n⌝]⋅ THEN Auto'))
   THEN D (-1)
   THEN RepeatFor 2 ((D (-3) THENA Auto))
   THEN HypSubst' (-1) 0⋅
   THEN ThinVar `m'
   THEN MoveToConcl (-3)
   THEN MoveToConcl (-2)
   THEN NatInd (-1)
   THEN (UnivCD THENA Auto)) }

1
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)

2
1. F : Top
2. G : Top
3. L : Top
4. i : ℤ
5. 0 < i
6. ∀K:Top. ∀n:ℤ.
     ((0 ≤ n)
     ⇒ (callbyvalueall_seq(L;λf.mk_applies(f;K;n);λg.let x ⟵ F[g]
                                                      in G[g;x];n;n + (i - 1)) 
        ~ callbyvalueall_seq(λn@0.if (n@0 =z n + (i - 1)) then mk_lambdas_fun(λg.F[g];n + (i - 1)) else L n@0 fi 
                            ;λf.mk_applies(f;K;n);λg.G[partial_ap(g;(n + (i - 1)) + 1;n + (i - 1));select_fun_ap(g;(n
                                                     + (i - 1))
                                                     + 1;n + (i - 1))];n;(n + (i - 1)) + 1)))
7. K : Top
8. n : ℤ
9. 0 ≤ n
⊢ callbyvalueall_seq(L;λf.mk_applies(f;K;n);λg.let x ⟵ F[g]
                                               in G[g;x];n;n + i) 
~ callbyvalueall_seq(λn@0.if (n@0 =z n + i) then mk_lambdas_fun(λg.F[g];n + i) else L n@0 fi ;λf.mk_applies(f;K;n)
                    ;λg.G[partial_ap(g;(n + i) + 1;n + i);select_fun_ap(g;(n + i) + 1;n + i)];n;(n + i) + 1)

---

Latex:

---

Latex:
\mforall{}[F,G,L,K:Top].  \mforall{}[m:\mBbbN{}].  \mforall{}[n:\mBbbN{}m  +  1].
    (callbyvalueall\_seq(L;\mlambda{}f.mk\_applies(f;K;n);\mlambda{}g.let  x  \mleftarrow{}{}  F[g]
                                                                                                in  G[g;x];n;m) 
    \msim{}  callbyvalueall\_seq(\mlambda{}n.if  (n  =\msubz{}  m)  then  mk\_lambdas\_fun(\mlambda{}g.F[g];m)  else  L  n  fi 
                                            ;\mlambda{}f.mk\_applies(f;K;n);\mlambda{}g.G[partial\_ap(g;m  +  1;m);select\_fun\_ap(g;m  +  1;m)];n;m
                                            +  1))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}\mexists{}i:\mBbbN{}.  (m  =  (n  +  i))\mkleeneclose{}\mcdot{}  THENA  (InstConcl  [\mkleeneopen{}m  -  n\mkleeneclose{}]\mcdot{}  THEN  Auto'))
  THEN  D  (-1)
  THEN  RepeatFor  2  ((D  (-3)  THENA  Auto))
  THEN  HypSubst'  (-1)  0\mcdot{}
  THEN  ThinVar  `m'
  THEN  MoveToConcl  (-3)
  THEN  MoveToConcl  (-2)
  THEN  NatInd  (-1)
  THEN  (UnivCD  THENA  Auto))

---

Home Index