---

Step * of Lemma callbyvalueall_seq-combine3

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

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

2
1. F : Top
2. L1 : Top
3. L2 : Top
4. m2 : ℕ
5. k : ℤ
6. 0 < k
7. ∀K:Top. ∀n:ℤ.
     ((0 ≤ n)
     ⇒ (callbyvalueall_seq(L1;λf.mk_applies(f;K;n);λg.callbyvalueall_seq(L2[g];λx.x;F[g];0;m2);n;n + (k - 1)) 
        ~ callbyvalueall_seq(λi.if i <z n + (k - 1)
                                then L1 i
                                else mk_lambdas_fun(λg.(L2[g] (i - n + (k - 1)));n + (k - 1))
                                fi ;λf.mk_applies(f;K;n);λg.(F[partial_ap(g;(n + (k - 1)) + m2;n + (k - 1))] 
                                                             partial_ap_gen(g;(n + (k - 1)) + m2;n + (k - 1);m2));n;(n
                            + (k - 1))
                            + m2)))
8. K : Top
9. n : ℤ
10. 0 ≤ n
⊢ callbyvalueall_seq(L1;λf.mk_applies(f;K;n);λg.callbyvalueall_seq(L2[g];λx.x;F[g];0;m2);n;n + k) 
~ callbyvalueall_seq(λi.if i <z n + k then L1 i else mk_lambdas_fun(λg.(L2[g] (i - n + k));n + k) fi 
                    ;λf.mk_applies(f;K;n);λg.(F[partial_ap(g;(n + k) + m2;n + k)] 
                                              partial_ap_gen(g;(n + k) + m2;n + k;m2));n;(n + k) + m2)

---

Latex:

---

Latex:
\mforall{}[F,L1,L2,K:Top].  \mforall{}[m1,m2:\mBbbN{}].  \mforall{}[n:\mBbbN{}m1  +  1].
    (callbyvalueall\_seq(L1;\mlambda{}f.mk\_applies(f;K;n);\mlambda{}g.callbyvalueall\_seq(L2[g];\mlambda{}x.x;F[g];0;m2);n;m1) 
    \msim{}  callbyvalueall\_seq(\mlambda{}i.if  i  <z  m1  then  L1  i  else  mk\_lambdas\_fun(\mlambda{}g.(L2[g]  (i  -  m1));m1)  fi 
                                            ;\mlambda{}f.mk\_applies(f;K;n);\mlambda{}g.(F[partial\_ap(g;m1  +  m2;m1)] 
                                                                                                partial\_ap\_gen(g;m1  +  m2;m1;m2));n;m1  +  m2))


By

---

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

---

Home Index