---

Step * of Lemma no_repeats_reverse

∀[T:Type]. ∀[L:T List].  uiff(no_repeats(T;rev(L));no_repeats(T;L))
BY
{ (Auto
   THEN ParallelLast
   THEN Auto
   THEN (Assert ||rev(L)|| = ||L|| ∈ ℤ BY
               (RWO "length-reverse" 0 THEN Auto))
   THEN InstHyp [⌜||L|| - 1 - i⌝;⌜||L|| - 1 - j⌝] 3⋅
   THEN (Auto' THEN Try ((RWO "select-reverse" (-1) THEN Auto)))
   THEN RWO "select-reverse" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L:T  List].    uiff(no\_repeats(T;rev(L));no\_repeats(T;L))


By

---

Latex:
(Auto
  THEN  ParallelLast
  THEN  Auto
  THEN  (Assert  ||rev(L)||  =  ||L||  BY
                          (RWO  "length-reverse"  0  THEN  Auto))
  THEN  InstHyp  [\mkleeneopen{}||L||  -  1  -  i\mkleeneclose{};\mkleeneopen{}||L||  -  1  -  j\mkleeneclose{}]  3\mcdot{}
  THEN  (Auto'  THEN  Try  ((RWO  "select-reverse"  (-1)  THEN  Auto)))
  THEN  RWO  "select-reverse"  0
  THEN  Auto)

---

Home Index