---

Step * 1 of Lemma unzip-as-accum

.....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>))
BY
{ (Unfold `unzip` 0
   THEN InductionOnList
   THEN All Reduce
   THEN Try (Complete ((RepeatFor 2 ((D 0 THENA Auto)) THEN RWO "append_nil_sq" 0 THEN Auto)))
   THEN DVar `u'
   THEN Reduce 0
   THEN RepeatFor 2 ((D 0 THENA Auto))
   THEN (RWO  "-3<" 0 THENA Auto)
   THEN Thin (-3)) }

1
1. u1 : Top
2. u2 : Top
3. v : (Top × Top) List
4. b1 : Top List
5. b2 : Top List
⊢ <b1 @ [u1 / map(λp.(fst(p));v)], b2 @ [u2 / map(λp.(snd(p));v)]> ~ <(b1 @ [u1]) @ map(λp.(fst(p));v)
                                                                   , (b2 @ [u2]) @ map(λp.(snd(p));v)
                                                                   >

---

Latex:

---

Latex:
.....assertion..... 
\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>))


By

---

Latex:
(Unfold  `unzip`  0
  THEN  InductionOnList
  THEN  All  Reduce
  THEN  Try  (Complete  ((RepeatFor  2  ((D  0  THENA  Auto))  THEN  RWO  "append\_nil\_sq"  0  THEN  Auto)))
  THEN  DVar  `u'
  THEN  Reduce  0
  THEN  RepeatFor  2  ((D  0  THENA  Auto))
  THEN  (RWO    "-3<"  0  THENA  Auto)
  THEN  Thin  (-3))

---

Home Index