---

Step * of Lemma free-word-inv-append

∀[x:Top List]. ∀[y:Top].  (free-word-inv(x @ y) ~ free-word-inv(y) @ free-word-inv(x))
BY
{ (Auto
   THEN RepUR ``free-word-inv`` 0
   THEN (RWO  "map_append_sq<" 0 THENA Auto)
   THEN RWO "reverse_append_sq" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[x:Top  List].  \mforall{}[y:Top].    (free-word-inv(x  @  y)  \msim{}  free-word-inv(y)  @  free-word-inv(x))


By

---

Latex:
(Auto
  THEN  RepUR  ``free-word-inv``  0
  THEN  (RWO    "map\_append\_sq<"  0  THENA  Auto)
  THEN  RWO  "reverse\_append\_sq"  0
  THEN  Auto)

---

Home Index