---

Step * 2 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. 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)
BY
{ (Thin (-1)
   THEN (GenConclAtAddrType ⌜Base⌝ [2;2]⋅ THENA Auto)
   THEN Thin (-1)
   THEN (GenConclAtAddrType ⌜ℕ⌝ [2;4]⋅ THENA Auto)
   THEN RenameVar `k' (-2)) }

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

---

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.  0  <  n  +  1
\mvdash{}  callbyvalueall-seq(L;\mlambda{}x.x;mk\_lambdas(F1;m  -  1);0;m)  \msim{}(n  +  1) 
-  1  callbyvalueall-seq(L;\mlambda{}x.x;mk\_lambdas(F2;m  -  1);0;m)


By

---

Latex:
(Thin  (-1)
  THEN  (GenConclAtAddrType  \mkleeneopen{}Base\mkleeneclose{}  [2;2]\mcdot{}  THENA  Auto)
  THEN  Thin  (-1)
  THEN  (GenConclAtAddrType  \mkleeneopen{}\mBbbN{}\mkleeneclose{}  [2;4]\mcdot{}  THENA  Auto)
  THEN  RenameVar  `k'  (-2))

---

Home Index