---

Step * 2 1 1 of Lemma simple-cbva-seq-sqequal-n


1. L : Base
2. F1 : Base
3. F2 : Base
4. v : Base
5. k : ℕ
6. j : ℕ
7. 0 < j
⊢ ∀n:ℕ
    ((((k + j) ≤ (n + 2)) ⇒ (F1 ~(n - k + j) + 2 F2))
    ⇒ (callbyvalueall-seq(L;v;mk_lambdas(F1;(k + j) - 1);k;k + j) ~(n + 1) - 1 callbyvalueall-seq(L;v;mk_lambdas(F2;(k
                                                                                                   + j) - 1);k;k + j)))
BY
{ (RepeatFor 2 (MoveToConcl (-3)) THEN NatInd (-2) THEN Auto') }

1
1. L : Base
2. F1 : Base
3. F2 : Base
4. j : ℤ
5. [%1] : 0 < j
6. 0 < j - 1
⇒ (∀v:Base. ∀k,n:ℕ.
      ((((k + (j - 1)) ≤ (n + 2)) ⇒ (F1 ~(n - k + (j - 1)) + 2 F2))
      ⇒ (callbyvalueall-seq(L;v;mk_lambdas(F1;(k + (j - 1)) - 1);k;k + (j - 1)) ~(n + 1) 
         - 1 callbyvalueall-seq(L;v;mk_lambdas(F2;(k + (j - 1)) - 1);k;k + (j - 1)))))
7. 0 < j
8. v : Base
9. k : ℕ
10. n : ℕ
11. ((k + j) ≤ (n + 2)) ⇒ (F1 ~(n - k + j) + 2 F2)
⊢ callbyvalueall-seq(L;v;mk_lambdas(F1;(k + j) - 1);k;k + j) ~(n + 1) 
- 1 callbyvalueall-seq(L;v;mk_lambdas(F2;(k + j) - 1);k;k + j)

---

Latex:

---

Latex:

1.  L  :  Base
2.  F1  :  Base
3.  F2  :  Base
4.  v  :  Base
5.  k  :  \mBbbN{}
6.  j  :  \mBbbN{}
7.  0  <  j
\mvdash{}  \mforall{}n:\mBbbN{}
        ((((k  +  j)  \mleq{}  (n  +  2))  {}\mRightarrow{}  (F1  \msim{}(n  -  k  +  j)  +  2  F2))
        {}\mRightarrow{}  (callbyvalueall-seq(L;v;mk\_lambdas(F1;(k  +  j)  -  1);k;k  +  j)  \msim{}(n  +  1) 
              -  1  callbyvalueall-seq(L;v;mk\_lambdas(F2;(k  +  j)  -  1);k;k  +  j)))


By

---

Latex:
(RepeatFor  2  (MoveToConcl  (-3))  THEN  NatInd  (-2)  THEN  Auto')

---

Home Index