---

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


1. L : Base
2. F1 : Base
3. F2 : Base
4. m : {1...}
5. n : ℕ
6. (m ≤ (n + 2)) ⇒ (F1 ~(n - m) + 2 F2)
7. v : Base
8. k : ℕ
9. 0 = k ∈ ℕ
⊢ callbyvalueall-seq(L;v;mk_lambdas(F1;m - 1);k;m) ~(n + 1) - 1 callbyvalueall-seq(L;v;mk_lambdas(F2;m - 1);k;m)
BY
{ ((Assert ⌜∃j:ℕ. (m = (k + j) ∈ ℤ)⌝⋅ THENA (InstConcl [⌜m - k⌝]⋅ THEN Auto'))
   THEN MoveToConcl (-6)
   THEN D (-1)
   THEN HypSubst' (-1) 0
   THEN (Assert ⌜0 < j⌝⋅ THENA Auto')
   THEN ThinVar `m'
   THEN Thin (-3)) }

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

---

Latex:

---

Latex:

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


By

---

Latex:
((Assert  \mkleeneopen{}\mexists{}j:\mBbbN{}.  (m  =  (k  +  j))\mkleeneclose{}\mcdot{}  THENA  (InstConcl  [\mkleeneopen{}m  -  k\mkleeneclose{}]\mcdot{}  THEN  Auto'))
  THEN  MoveToConcl  (-6)
  THEN  D  (-1)
  THEN  HypSubst'  (-1)  0
  THEN  (Assert  \mkleeneopen{}0  <  j\mkleeneclose{}\mcdot{}  THENA  Auto')
  THEN  ThinVar  `m'
  THEN  Thin  (-3))

---

Home Index