type List = {bool value; data next:List; bool free;}

data freenodes:List;

proc delete(data x:List, pointer p:List):void
[(x<next*>p | x=null & p=null) & allpos t of List: freenodes<next*>t <=> t.free=true]
{
  pointer q:List;
  if (p!=null) {
    if (p.next=null) {
      q = x.next;
      x.free = true;
      x.next = freenodes;
      freenodes = x;
      x = q;
    }
    else {
      q = p.next.next;
      p.next.free = true;
      p.next.next = freenodes;
      freenodes = p.next;
      p.next = q;
    }    
  }
}
[allpos t of List: freenodes<next*>t <=> t.free=true]