---

Step * of Lemma word-rel-length

∀[X:Type]. ∀[w1,w2:(X + X) List].  ||w2|| < ||w1|| supposing word-rel(X;w1;w2)
BY
{ (Auto THEN D -1 THEN ExRepD THEN RWO "-2 -1" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[X:Type].  \mforall{}[w1,w2:(X  +  X)  List].    ||w2||  <  ||w1||  supposing  word-rel(X;w1;w2)


By

---

Latex:
(Auto  THEN  D  -1  THEN  ExRepD  THEN  RWO  "-2  -1"  0  THEN  Auto)

---

Home Index