---

Step * 1 1 2 2 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. v@0 : 𝔹
⊢ (v@0 ∧b (eq u1 u)) ∧b (list-deq(eq) v1 v) = v@0 ∧b (list-deq(eq) [u1 / v1] [u / v])
BY
{ (RenameVar `b' (-1)⋅ THEN BoolCase ⌜b⌝⋅ THEN Auto) }

1
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
⊢ (eq u1 u) ∧b (list-deq(eq) v1 v) = list-deq(eq) [u1 / v1] [u / v]

---

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.  v@0  :  \mBbbB{}
\mvdash{}  (v@0  \mwedge{}\msubb{}  (eq  u1  u))  \mwedge{}\msubb{}  (list-deq(eq)  v1  v)  =  v@0  \mwedge{}\msubb{}  (list-deq(eq)  [u1  /  v1]  [u  /  v])


By

---

Latex:
(RenameVar  `b'  (-1)\mcdot{}  THEN  BoolCase  \mkleeneopen{}b\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index