---

Step * 2 of Lemma unzip-as-accum


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:
                  <[], []>))
BY
{ ((ParallelLast THEN (InstHyp [⌜[]⌝;⌜[]⌝] (-1)⋅ THENA Auto))
   THEN RevHypSubst (-1) 0
   THEN RepUR ``unzip`` 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  \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>))
\mvdash{}  \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:
((ParallelLast  THEN  (InstHyp  [\mkleeneopen{}[]\mkleeneclose{};\mkleeneopen{}[]\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto))
  THEN  RevHypSubst  (-1)  0
  THEN  RepUR  ``unzip``  0
  THEN  Auto)

---

Home Index