
#ifndef ADJACENTDIFFERENCE_H_INCLUDED
#define ADJACENTDIFFERENCE_H_INCLUDED

#include "Difference.h"

/*@
  predicate
    AdjacentDifference{L}(value_type* a, integer n, value_type* b) =
      \forall integer i; 0 <= i < n ==> b[i] == Difference(a, i);
*/

#endif /* ADJACENTDIFFERENCE_H_INCLUDED */

