---

Step * of Lemma mklist_defn2

∀[f:Top]. ∀[n:ℕ].  (mklist(n;f) ~ mklist-general(n;λl.(f ||l||)))
BY
{ ((UnivCD THENA Auto)
   THEN NatInd (-1)
   THEN RepUR ``mklist mklist-general`` 0
   THEN Try (Trivial)
   THEN (RWO "primrec-unroll" 0 THENA Auto)
   THEN (Fold `mklist` 0
         THEN (Subst ⌜λm,rl. (rl @ [f ||rl||]) ~ λm,rl. (rl @ [(λl.(f ||l||)) rl])⌝ 0⋅ THENA (Reduce 0 THEN Auto))
         THEN Fold `mklist-general` 0)
   THEN Reduce 0
   THEN AutoSplit
   THEN Auto
   THEN RWO "mklist-general-length" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[f:Top].  \mforall{}[n:\mBbbN{}].    (mklist(n;f)  \msim{}  mklist-general(n;\mlambda{}l.(f  ||l||)))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  NatInd  (-1)
  THEN  RepUR  ``mklist  mklist-general``  0
  THEN  Try  (Trivial)
  THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
  THEN  (Fold  `mklist`  0
              THEN  (Subst  \mkleeneopen{}\mlambda{}m,rl.  (rl  @  [f  ||rl||])  \msim{}  \mlambda{}m,rl.  (rl  @  [(\mlambda{}l.(f  ||l||))  rl])\mkleeneclose{}  0\mcdot{}
                          THENA  (Reduce  0  THEN  Auto)
                          )
              THEN  Fold  `mklist-general`  0)
  THEN  Reduce  0
  THEN  AutoSplit
  THEN  Auto
  THEN  RWO  "mklist-general-length"  0
  THEN  Auto)

---

Home Index