---

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


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)
BY
{ (Thin (-2)
   THEN (HypSubst' (-1) 0
         THEN RecUnfold `callbyvalueall-seq` 0
         THEN AutoSplit
         THEN D (-3)
         THEN Auto
         THEN Subst ⌜n - m ~ n⌝ (-1)⋅
         THEN Auto'
         THEN FLemma `sqequal_n_add` [-1]
         THEN Auto)⋅
   ) }

---

Latex:

---

Latex:

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


By

---

Latex:
(Thin  (-2)
  THEN  (HypSubst'  (-1)  0
              THEN  RecUnfold  `callbyvalueall-seq`  0
              THEN  AutoSplit
              THEN  D  (-3)
              THEN  Auto
              THEN  Subst  \mkleeneopen{}n  -  m  \msim{}  n\mkleeneclose{}  (-1)\mcdot{}
              THEN  Auto'
              THEN  FLemma  `sqequal\_n\_add`  [-1]
              THEN  Auto)\mcdot{}
  )

---

Home Index