---

Step * 1 of Lemma taba-property

.....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))))
BY
{ (InductionOnList⋅⋅ THEN Reduce 0) }

1
1. A : Type
2. B : Type
3. init : B
4. F : A ⟶ A ⟶ B ⟶ B
5. xs : A List
⊢ ∀ys:A List. ((0 ≤ ||ys||) ⇒ (<init, ys> = <init, ys> ∈ (B × (A List))))

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

---

Latex:

---

Latex:
.....assertion..... 
1.  A  :  Type
2.  B  :  Type
3.  init  :  B
4.  F  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  B  {}\mrightarrow{}  B
5.  xs  :  A  List
\mvdash{}  \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)
                  >))


By

---

Latex:
(InductionOnList\mcdot{}\mcdot{}  THEN  Reduce  0)

---

Home Index