---

Step * 2 1 1 1 of Lemma eval-mklist-sq


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)])
BY
{ (NatInd (-1)
   THEN Reduce 0
   THEN Auto
   THEN (RWO "primrec-unroll" 0 THENA Auto)
   THEN (OReduce 0 THENA Auto)
   THEN (RWO  "5<" 0 THENA Auto)
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  offset  :  \mBbbN{}
3.  m  :  \mBbbN{}
\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:
(NatInd  (-1)
  THEN  Reduce  0
  THEN  Auto
  THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
  THEN  (OReduce  0  THENA  Auto)
  THEN  (RWO    "5<"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  Auto)

---

Home Index