---

Step * 1 1 2 2 1 1 1 1 1 of Lemma assert-palindrome-test


1. T : Type
2. eq : EqDecider(T)
3. u : T
4. v : T List
5. ∀R:T List
     ((||R|| = ||v|| ∈ ℤ)
     ⇒ (∀v@0:𝔹
           (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(R;v)
            with starting value:
             v@0) ~ v@0 ∧b (list-deq(eq) R v))))
6. u1 : T
7. v1 : T List
8. (||v1|| = (||v|| + 1) ∈ ℤ)
⇒ (∀v@0:𝔹
      (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(v1;[u / v])
       with starting value:
        v@0) ~ v@0 ∧b (list-deq(eq) v1 [u / v])))
9. (||v1|| + 1) = (||v|| + 1) ∈ ℤ
10. b : 𝔹
11. ↑b
⊢ (u1 = u ∈ T) ∧ (↑(list-deq(eq) v1 v)) ⇐⇒ ↑(list-deq(eq) [u1 / v1] [u / v])
BY
{ (RWO "deq_property<" 0⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  u  :  T
4.  v  :  T  List
5.  \mforall{}R:T  List
          ((||R||  =  ||v||)
          {}\mRightarrow{}  (\mforall{}v@0:\mBbbB{}
                      (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(R;v)
                        with  starting  value:
                          v@0)  \msim{}  v@0  \mwedge{}\msubb{}  (list-deq(eq)  R  v))))
6.  u1  :  T
7.  v1  :  T  List
8.  (||v1||  =  (||v||  +  1))
{}\mRightarrow{}  (\mforall{}v@0:\mBbbB{}
            (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(v1;[u  /  v])
              with  starting  value:
                v@0)  \msim{}  v@0  \mwedge{}\msubb{}  (list-deq(eq)  v1  [u  /  v])))
9.  (||v1||  +  1)  =  (||v||  +  1)
10.  b  :  \mBbbB{}
11.  \muparrow{}b
\mvdash{}  (u1  =  u)  \mwedge{}  (\muparrow{}(list-deq(eq)  v1  v))  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}(list-deq(eq)  [u1  /  v1]  [u  /  v])


By

---

Latex:
(RWO  "deq\_property<"  0\mcdot{}  THEN  Auto)

---

Home Index