Step
*
2
1
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. ¬(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)])
BY
{ All Thin }
1
1. T : Type
2. offset : ℕ
3. 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.  \mneg{}(n  =  0)
8.  m  :  \mBbbN{}
9.  (n  -  1)  =  m
\mvdash{}  \mforall{}f:\{offset..m  +  offset  +  1\msupminus{}\}  {}\mrightarrow{}  T
        ([f  offset  /  primrec(m;[];\mlambda{}i,l.  (l  @  [f  (i  +  offset  +  1)]))]  \msim{}  primrec(m;[];\mlambda{}i,l.  (l
                                                                                                                                                                  @  [f  (i  +  offset)])\000C)
        @  [f  (m  +  offset)])
By
Latex:
All  Thin
Home
Index