---

Step * of Lemma taba-property

∀[A,B:Type]. ∀[init:B]. ∀[F:A ⟶ A ⟶ B ⟶ B]. ∀[xs:A List].
  (taba(init;x,x',a.F[x;x';a];xs)
  = accumulate (with value a and list item p):
     let x,x' = p 
     in F[x;x';a]
    over list:
      zip(rev(xs);xs)
    with starting value:
     init)
  ∈ B)
BY
{ (Auto
   THEN Unfold `taba` 0
   THEN (Assert ⌜∀xs,ys:A List.
                   ((||xs|| ≤ ||ys||)
                   ⇒ (rec-case(xs) of
                       [] => <init, ys>
                       x::xs' =>
                        p.let a,ys = p 
                          in let h,t = ys 
                             in <F[x;h;a], t>
                      = <accumulate (with value a and list item p):
                          let x,x' = p 
                          in F[x;x';a]
                         over list:
                           zip(rev(xs);firstn(||xs||;ys))
                         with starting value:
                          init)
                        , nth_tl(||xs||;ys)
                        >
                      ∈ (B × (A List))))⌝⋅
   THENM (RWO "-1" 0 THEN Auto THEN Reduce 0 THEN RWO "firstn_all" 0 THEN Auto)
   )) }

1
.....assertion..... 
1. A : Type
2. B : Type
3. init : B
4. F : A ⟶ A ⟶ B ⟶ B
5. xs : A List
⊢ ∀xs,ys:A List.
    ((||xs|| ≤ ||ys||)
    ⇒ (rec-case(xs) of
        [] => <init, ys>
        x::xs' =>
         p.let a,ys = p 
           in let h,t = ys 
              in <F[x;h;a], t>
       = <accumulate (with value a and list item p):
           let x,x' = p 
           in F[x;x';a]
          over list:
            zip(rev(xs);firstn(||xs||;ys))
          with starting value:
           init)
         , nth_tl(||xs||;ys)
         >
       ∈ (B × (A List))))

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[init:B].  \mforall{}[F:A  {}\mrightarrow{}  A  {}\mrightarrow{}  B  {}\mrightarrow{}  B].  \mforall{}[xs:A  List].
    (taba(init;x,x',a.F[x;x';a];xs)
    =  accumulate  (with  value  a  and  list  item  p):
          let  x,x'  =  p 
          in  F[x;x';a]
        over  list:
            zip(rev(xs);xs)
        with  starting  value:
          init))


By

---

Latex:
(Auto
  THEN  Unfold  `taba`  0
  THEN  (Assert  \mkleeneopen{}\mforall{}xs,ys:A  List.
                                  ((||xs||  \mleq{}  ||ys||)
                                  {}\mRightarrow{}  (rec-case(xs)  of
                                          []  =>  <init,  ys>
                                          x::xs'  =>
                                            p.let  a,ys  =  p 
                                                in  let  h,t  =  ys 
                                                      in  <F[x;h;a],  t>
                                        =  <accumulate  (with  value  a  and  list  item  p):
                                                let  x,x'  =  p 
                                                in  F[x;x';a]
                                              over  list:
                                                  zip(rev(xs);firstn(||xs||;ys))
                                              with  starting  value:
                                                init)
                                            ,  nth\_tl(||xs||;ys)
                                            >))\mkleeneclose{}\mcdot{}
  THENM  (RWO  "-1"  0  THEN  Auto  THEN  Reduce  0  THEN  RWO  "firstn\_all"  0  THEN  Auto)
  ))

---

Home Index