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

proc search(data x:List):List
  pointer X:List;
[X=x]
{
  pointer p:List;
  p = x;
  while [X=x & (x<next*>p | p=null) &
         (p=null => allpos q of List: x<next*>q => q.value=false) &
         allpos q of List: q<next.next*>p => q.value=false]
        (p!=null & p.value!=true) {
    p = p.next;
  }
  return p;
}
[(existpos q of List: X<next*.[pos.value]>q) => 
 X<([!pos.value].next)*.[pos.value]>return]