---

Step * 2 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
⊢ eval-mklist(n;f;offset) ~ primrec(n;[];λi,l. (l @ [(λi.(f (i + offset))) i]))
BY
{ ((Assert ¬(n = 0 ∈ ℤ) BY
          Auto)
   THEN (RWO "primrec-unroll" 0 THENA Auto)
   THEN (OReduce 0 THENA Auto)
   THEN Unfolds ``eval-mklist`` 0
   THEN Reduce 0
   THEN RepeatFor 3 ((CallByValueReduce 0 THENA Auto))
   THEN ((RWO "5" 0 THENA Auto) THEN (CallByValueReduce 0 THENA Auto))
   THEN Reduce 0) }

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. 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)]

---

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
\mvdash{}  eval-mklist(n;f;offset)  \msim{}  primrec(n;[];\mlambda{}i,l.  (l  @  [(\mlambda{}i.(f  (i  +  offset)))  i]))


By

---

Latex:
((Assert  \mneg{}(n  =  0)  BY
                Auto)
  THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
  THEN  (OReduce  0  THENA  Auto)
  THEN  Unfolds  ``eval-mklist``  0
  THEN  Reduce  0
  THEN  RepeatFor  3  ((CallByValueReduce  0  THENA  Auto))
  THEN  ((RWO  "5"  0  THENA  Auto)  THEN  (CallByValueReduce  0  THENA  Auto))
  THEN  Reduce  0)

---

Home Index