---

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

∀L:Top. ∀F1,F2:Base. ∀m,n:ℕ.
  (((m ≤ (n + 2)) ⇒ (F1 ~(n - m) + 2 F2)) ⇒ (simple-cbva-seq(L;F1;m) ~n simple-cbva-seq(L;F2;m)))
BY
{ (Auto' THEN SqEqualNTopToBase THEN PromoteHyp (-1) 1 THEN RepUR ``simple-cbva-seq cbva-seq`` 0 THEN AutoSplit) }

1
1. L : Base
2. F1 : Base
3. F2 : Base
4. m : ℕ
5. n : ℕ
6. (m ≤ (n + 2)) ⇒ (F1 ~(n - m) + 2 F2)
7. 0 < n + 1
8. m = 0 ∈ ℤ
⊢ callbyvalueall-seq(L;λx.x;F1;0;m) ~(n + 1) - 1 callbyvalueall-seq(L;λx.x;F2;0;m)

2
1. L : Base
2. F1 : Base
3. F2 : Base
4. m : {1...}
5. n : ℕ
6. (m ≤ (n + 2)) ⇒ (F1 ~(n - m) + 2 F2)
7. 0 < n + 1
⊢ callbyvalueall-seq(L;λx.x;mk_lambdas(F1;m - 1);0;m) ~(n + 1) - 1 callbyvalueall-seq(L;λx.x;mk_lambdas(F2;m - 1);0;m)

---

Latex:

---

Latex:
\mforall{}L:Top.  \mforall{}F1,F2:Base.  \mforall{}m,n:\mBbbN{}.
    (((m  \mleq{}  (n  +  2))  {}\mRightarrow{}  (F1  \msim{}(n  -  m)  +  2  F2))  {}\mRightarrow{}  (simple-cbva-seq(L;F1;m)  \msim{}n  simple-cbva-seq(L;F2;m)))


By

---

Latex:
(Auto'
  THEN  SqEqualNTopToBase
  THEN  PromoteHyp  (-1)  1
  THEN  RepUR  ``simple-cbva-seq  cbva-seq``  0
  THEN  AutoSplit)

---

Home Index