---

Step * of Lemma assert-slow-int-palindrome-test

∀[L:ℤ List]. uiff(↑slow-int-palindrome-test(L);rev(L) = L ∈ (ℤ List))
BY
{ xxx((UnivCD THENA Auto) THEN Unfold `slow-int-palindrome-test` 0 THEN RWO "deq_property<" 0 THEN Auto)xxx }

---

Latex:

---

Latex:
\mforall{}[L:\mBbbZ{}  List].  uiff(\muparrow{}slow-int-palindrome-test(L);rev(L)  =  L)


By

---

Latex:
xxx((UnivCD  THENA  Auto)
        THEN  Unfold  `slow-int-palindrome-test`  0
        THEN  RWO  "deq\_property<"  0
        THEN  Auto)xxx

---

Home Index