---

Step * of Lemma has-value-mklist

∀[n,f:Base].  n ∈ ℤ supposing (mklist(n;f))↓
BY
{ ((UnivCD THENA Auto) THEN (All (RepUR ``mklist``) THEN (All  (RWO "primrec-as-fix") THENA Auto)) THEN Reduce -1) }

1
1. n : Base
2. f : Base
3. (fix((λp,n. if (n) < (1)  then []  else ((p (n - 1)) @ [f (n - 1)]))) n)↓
⊢ n ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[n,f:Base].    n  \mmember{}  \mBbbZ{}  supposing  (mklist(n;f))\mdownarrow{}


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (All  (RepUR  ``mklist``)  THEN  (All    (RWO  "primrec-as-fix")  THENA  Auto))
  THEN  Reduce  -1)

---

Home Index