type List = {data next:List;}

pred roots(pointer p1,p2,p3:List) = 
  allpos p of List: p1<next*>p | p2<next*>p | p3<next*>p;
  /* exploit that we know all data variables */

proc zip(data list1,list2:List):List
[roots(list1,list2,null)]
{
  data res:List;
  pointer p,t:List;
  if (list1=null) {
    t = list1;
    list1 = list2;
    list2 = t;
  }
  res = null;
  p = null;
  while [(list1=null => list2=null) & 
         (res=null <=> p=null) & 
         (res!=null => p.next=null & res<next*>p) & 
         roots(list1,list2,res)]
    (list1!=null) 
  {
    if (res=null) {
      res = list1;
      p = list1;
    }
    else {
      p.next = list1;
      p = p.next;
    }
    list1 = list1.next;
    p.next = null;
    if (list2!=null) {
      t = list1;
      list1 = list2;
      list2 = t;
    }
  }
  return res;
}
[roots(return,null,null)]