---

Step * of Lemma assert-int-palindrome-test

∀[L:ℤ List]. uiff(↑int-palindrome-test(L);rev(L) = L ∈ (ℤ List))
BY
{ ((UnivCD⋅ THENA Auto) THEN RWW "int-palindrome-test-sq assert-palindrome-test" 0 THEN Auto)⋅ }

---

Latex:

---

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


By

---

Latex:
((UnivCD\mcdot{}  THENA  Auto)  THEN  RWW  "int-palindrome-test-sq  assert-palindrome-test"  0  THEN  Auto)\mcdot{}

---

Home Index