---

Step * of Lemma unzip-as-accum

∀[as:(Top × Top) List]
  (unzip(as) ~ accumulate (with value p and list item a):
                let p1,p2 = p 
                in let a1,a2 = a 
                   in <p1 @ [a1], p2 @ [a2]>
               over list:
                 as
               with starting value:
                <[], []>))
BY
{ xxxAssert ⌜∀as:(Top × Top) List. ∀b1,b2:Top List.
               (let as1,as2 = unzip(as) 
                in <b1 @ as1, b2 @ as2> ~ accumulate (with value p and list item a):
                                           let p1,p2 = p 
                                           in let a1,a2 = a 
                                              in <p1 @ [a1], p2 @ [a2]>
                                          over list:
                                            as
                                          with starting value:
                                           <b1, b2>))⌝⋅xxx }

1
.....assertion..... 
∀as:(Top × Top) List. ∀b1,b2:Top List.
  (let as1,as2 = unzip(as) 
   in <b1 @ as1, b2 @ as2> ~ accumulate (with value p and list item a):
                              let p1,p2 = p 
                              in let a1,a2 = a 
                                 in <p1 @ [a1], p2 @ [a2]>
                             over list:
                               as
                             with starting value:
                              <b1, b2>))

2
1. ∀as:(Top × Top) List. ∀b1,b2:Top List.
     (let as1,as2 = unzip(as) 
      in <b1 @ as1, b2 @ as2> ~ accumulate (with value p and list item a):
                                 let p1,p2 = p 
                                 in let a1,a2 = a 
                                    in <p1 @ [a1], p2 @ [a2]>
                                over list:
                                  as
                                with starting value:
                                 <b1, b2>))
⊢ ∀[as:(Top × Top) List]
    (unzip(as) ~ accumulate (with value p and list item a):
                  let p1,p2 = p 
                  in let a1,a2 = a 
                     in <p1 @ [a1], p2 @ [a2]>
                 over list:
                   as
                 with starting value:
                  <[], []>))

---

Latex:

---

Latex:
\mforall{}[as:(Top  \mtimes{}  Top)  List]
    (unzip(as)  \msim{}  accumulate  (with  value  p  and  list  item  a):
                                let  p1,p2  =  p 
                                in  let  a1,a2  =  a 
                                      in  <p1  @  [a1],  p2  @  [a2]>
                              over  list:
                                  as
                              with  starting  value:
                                <[],  []>))


By

---

Latex:
xxxAssert  \mkleeneopen{}\mforall{}as:(Top  \mtimes{}  Top)  List.  \mforall{}b1,b2:Top  List.
                          (let  as1,as2  =  unzip(as) 
                            in  <b1  @  as1,  b2  @  as2>  \msim{}  accumulate  (with  value  p  and  list  item  a):
                                                                                  let  p1,p2  =  p 
                                                                                  in  let  a1,a2  =  a 
                                                                                        in  <p1  @  [a1],  p2  @  [a2]>
                                                                                over  list:
                                                                                    as
                                                                                with  starting  value:
                                                                                  <b1,  b2>))\mkleeneclose{}\mcdot{}xxx

---

Home Index