---

Step * of Lemma assert-palindrome-test

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:T List].  uiff(↑palindrome-test(eq;L);rev(L) = L ∈ (T List))
BY
{ xxx((UnivCD THENA Auto) THEN Unfold `palindrome-test` 0 THEN (RWO "taba-property" 0 THENA Auto))xxx }

1
1. T : Type
2. eq : EqDecider(T)
3. L : T List
⊢ uiff(↑accumulate (with value a and list item p):
         let x,x' = p 
         in eval b = a ∧b (eq x x') in
            b
        over list:
          zip(rev(L);L)
        with starting value:
         tt);rev(L) = L ∈ (T List))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[L:T  List].    uiff(\muparrow{}palindrome-test(eq;L);rev(L)  =  L)


By

---

Latex:
xxx((UnivCD  THENA  Auto)  THEN  Unfold  `palindrome-test`  0  THEN  (RWO  "taba-property"  0  THENA  Auto))xxx

---

Home Index