type Head = {
  data first:Node; 
  pointer last:Node[this.first<next*.[pos.next=null]>last];
}
type Node = {
  bool value; data next:Node; 
  pointer prev:Node[this^Node.next={prev}];
}

data garbage:Node;

proc delete(data list:Head, pointer p:Node):void
  set S:Node;  
  pointer L:Head;
  pointer P:Node;
[list.first<next*>p & list.last<prev*>p & p<next*>list.last & p<prev*>list.first &
 list.first<next*>S & L=list & P=p & p!=null]
{
  if (p=list.first) {
    list.first = p.next;
  }
  if (p=list.last) {
    list.last = p.prev;
  }
  if (p.prev!=null) {
    p.prev.next = p.next;
  }
  if (p.next!=null) {
    p.next.prev = p.prev;
  }
  if (garbage!=null) {
    garbage.prev = p;
  }
  p.next = garbage;
  p.prev = null;
  garbage = p;
}
[!L.first<next*>P & allpos q of Node: q in S <=> (L.first<next*>q | q=P)]

proc search(data list:Head, bool value):Node
  bool V;
  pointer L:Head;
[list!=null & V=value & L=list]
{
  pointer t:Node;
  t = list.first;
  while [list!=null & V=value & L=list & (t=null | list.first<next*>t) &
         (t=null => allpos p of Node: list.first<next*>p => p.value!=value) &
         allpos p of Node: p<next.next*>t => p.value!=value]
        (t!=null & t.value!=value) {
    t = t.next;
  }
  return t;
}
[L!=null & 
 (existpos p of Node: L.first<next*.[pos.value=V]>p) => 
  L.first<next*.[pos.value=V]>return]

proc insert(data list:Head, data node:Node):void
[list!=null & node!=null & node.next=null & node.prev=null]
{
  if (list.first=null) {
    list.last = node;
  }
  else {
    list.first.prev = node;
  }
  node.next = list.first;
  list.first = node;
  node = null; 
}
[true]

proc concat(data list1,list2:Head):Head
[list1!=null & list2!=null]
{
  if (list1.last!=null) {
    list1.last.next = list2.first;
  }
  else {
    list1.first = list2.first;
  }
  if (list2.first!=null) {
    list2.first.prev = list1.last;
    list1.last = list2.last;
  }
  list2.first = null;
  list2.last = null;
  return list1;
}
[true]