---

Step * of Lemma ml-revappend-sq

∀[T:Type]. ∀[as,bs:T List].  (ml-revappend(as;bs) ~ rev(as) + bs) supposing valueall-type(T)
BY
{ (InductionOnList
   THEN Intro
   THEN All (RepUR ``ml-revappend spreadcons ml_apply let``)
   THEN RW (AddrC [1] (SweepUpC UnrollRecursionC)) 0
   THEN Reduce 0
   THEN (CallByValueReduceOn ⌜bs⌝ 0⋅ THENA Auto)
   THEN (Trivial ORELSE ((CallByValueReduce 0⋅ THENA Auto) THEN Reduce 0 THEN RWO "-2" 0 THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[as,bs:T  List].    (ml-revappend(as;bs)  \msim{}  rev(as)  +  bs)  supposing  valueall-type(T)


By

---

Latex:
(InductionOnList
  THEN  Intro
  THEN  All  (RepUR  ``ml-revappend  spreadcons  ml\_apply  let``)
  THEN  RW  (AddrC  [1]  (SweepUpC  UnrollRecursionC))  0
  THEN  Reduce  0
  THEN  (CallByValueReduceOn  \mkleeneopen{}bs\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  (Trivial  ORELSE  ((CallByValueReduce  0\mcdot{}  THENA  Auto)  THEN  Reduce  0  THEN  RWO  "-2"  0  THEN  Auto)))

---

Home Index