---

Step * 2 1 of Lemma eval-mklist-sq


1. T : Type
2. value-type(T)
3. n : ℤ
4. 0 < n
5. ∀[offset:ℕ]. ∀[f:{offset..(n - 1) + offset-} ⟶ T].
     (eval-mklist(n - 1;f;offset) ~ primrec(n - 1;[];λi,l. (l @ [(λi.(f (i + offset))) i])))
6. offset : ℕ
7. f : {offset..n + offset-} ⟶ T
8. ¬(n = 0 ∈ ℤ)
⊢ [f offset / primrec(n - 1;[];λi,l. (l @ [f (i + offset + 1)]))] ~ primrec(n - 1;[];λi,l. (l @ [f (i + offset)]))
@ [f ((n - 1) + offset)]
BY
{ ((MoveToConcl (-2) THEN (Subst' n + offset ~ (n - 1) + offset + 1 0 THENA Auto))
   THEN (GenConcl ⌜(n - 1) = m ∈ ℕ⌝⋅ THENA Auto)
   ) }

1
1. T : Type
2. value-type(T)
3. n : ℤ
4. 0 < n
5. ∀[offset:ℕ]. ∀[f:{offset..(n - 1) + offset-} ⟶ T].
     (eval-mklist(n - 1;f;offset) ~ primrec(n - 1;[];λi,l. (l @ [(λi.(f (i + offset))) i])))
6. offset : ℕ
7. ¬(n = 0 ∈ ℤ)
8. m : ℕ
9. (n - 1) = m ∈ ℕ
⊢ ∀f:{offset..m + offset + 1-} ⟶ T
    ([f offset / primrec(m;[];λi,l. (l @ [f (i + offset + 1)]))] ~ primrec(m;[];λi,l. (l @ [f (i + offset)]))
    @ [f (m + offset)])

---

Latex:

---

Latex:

1.  T  :  Type
2.  value-type(T)
3.  n  :  \mBbbZ{}
4.  0  <  n
5.  \mforall{}[offset:\mBbbN{}].  \mforall{}[f:\{offset..(n  -  1)  +  offset\msupminus{}\}  {}\mrightarrow{}  T].
          (eval-mklist(n  -  1;f;offset)  \msim{}  primrec(n  -  1;[];\mlambda{}i,l.  (l  @  [(\mlambda{}i.(f  (i  +  offset)))  i])))
6.  offset  :  \mBbbN{}
7.  f  :  \{offset..n  +  offset\msupminus{}\}  {}\mrightarrow{}  T
8.  \mneg{}(n  =  0)
\mvdash{}  [f  offset  /  primrec(n  -  1;[];\mlambda{}i,l.  (l  @  [f  (i  +  offset  +  1)]))]  \msim{}  primrec(n  -  1;[];\mlambda{}i,l.  (l
                                                                                                                                                                            @  [f 
                                                                                                                                                                                  (i
                                                                                                                                                                                  +  offset)])\000C)
@  [f  ((n  -  1)  +  offset)]


By

---

Latex:
((MoveToConcl  (-2)  THEN  (Subst'  n  +  offset  \msim{}  (n  -  1)  +  offset  +  1  0  THENA  Auto))
  THEN  (GenConcl  \mkleeneopen{}(n  -  1)  =  m\mkleeneclose{}\mcdot{}  THENA  Auto)
  )

---

Home Index