---

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


1. T : Type
2. eq : EqDecider(T)
3. L : T List
4. R : T List
5. rev(L) = R ∈ (T List)
6. ||R|| = ||L|| ∈ ℤ
⊢ 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;L)
  with starting value:
   tt) ~ tt ∧b (list-deq(eq) R L)
BY
{ ((GenConclTerm ⌜tt⌝⋅ THENA Auto)
   THEN Thin (-1)
   THEN RepeatFor 2 (MoveToConcl (-1))
   THEN Thin (-1)
   THEN MoveToConcl (-1)
   THEN ListInd (-1)
   THEN Reduce 0
   THEN InductionOnList
   THEN Reduce  0
   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. 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;v)
  with starting value:
   eval b = v@0 ∧b (eq u1 u) in
   b) 
= v@0 ∧b (list-deq(eq) [u1 / v1] [u / v])

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  L  :  T  List
4.  R  :  T  List
5.  rev(L)  =  R
6.  ||R||  =  ||L||
\mvdash{}  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;L)
    with  starting  value:
      tt)  \msim{}  tt  \mwedge{}\msubb{}  (list-deq(eq)  R  L)


By

---

Latex:
((GenConclTerm  \mkleeneopen{}tt\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Thin  (-1)
  THEN  RepeatFor  2  (MoveToConcl  (-1))
  THEN  Thin  (-1)
  THEN  MoveToConcl  (-1)
  THEN  ListInd  (-1)
  THEN  Reduce  0
  THEN  InductionOnList
  THEN  Reduce    0
  THEN  Auto')

---

Home Index