
#ifndef HASEQUALNEIGHBORS_H_INCLUDED
#define HASEQUALNEIGHBORS_H_INCLUDED

#include "typedefs.h"

/*@
  predicate
    HasEqualNeighbors{L}(value_type* a, integer n) =
      \exists integer i; 0 <= i < n-1 && a[i] == a[i+1];
*/

#endif /* HASEQUALNEIGHBORS_H_INCLUDED */

