---

Step * 1 of Lemma assert-palindrome-test


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))
BY
{ Subst ⌜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) ~ list-deq(eq) rev(L) L⌝ 0⋅ }

1
.....equality..... 
1. T : Type
2. eq : EqDecider(T)
3. L : T List
⊢ 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) ~ list-deq(eq) rev(L) L

2
1. T : Type
2. eq : EqDecider(T)
3. L : T List
⊢ uiff(↑(list-deq(eq) rev(L) L);rev(L) = L ∈ (T List))

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  L  :  T  List
\mvdash{}  uiff(\muparrow{}accumulate  (with  value  a  and  list  item  p):
                  let  x,x'  =  p 
                  in  eval  b  =  a  \mwedge{}\msubb{}  (eq  x  x')  in
                        b
                over  list:
                    zip(rev(L);L)
                with  starting  value:
                  tt);rev(L)  =  L)


By

---

Latex:
Subst  \mkleeneopen{}accumulate  (with  value  a  and  list  item  p):
                let  x,x'  =  p 
                in  eval  b  =  a  \mwedge{}\msubb{}  (eq  x  x')  in
                      b
              over  list:
                  zip(rev(L);L)
              with  starting  value:
                tt)  \msim{}  list-deq(eq)  rev(L)  L\mkleeneclose{}  0\mcdot{}

---

Home Index