```// **************************************************************************
//
//    eses                   eses
//   eses                     eses
//  eses    eseses  esesese    eses   Embedded Systems Group
//  ese    ese  ese ese         ese
//  ese    eseseses eseseses    ese   Department of Computer Science
//  eses   eses          ese   eses
//   eses   eseses  eseseses  eses    University of Kaiserslautern
//    eses                   eses
//
// **************************************************************************

module Presburger(
int x, y, z
)  {
nothing;
} satisfies {

// --- " <= " is a total order
ord01 : assert x <= x;
ord02 : assert x<=y & y<=x -> x==y;
ord03 : assert (x <= y) & (y <= z) -> (x <= z);
ord04 : assert (x <= y) | (y <= x);

// --- "<" is a strict total order
ord05 : assert !(x < x);
ord06 : assert (x < y) -> !(y < x);
ord07 : assert (x < y) & (y < z) -> (x<z);
ord08 : assert (x < y) | (x==y) | (y<x);

// --- defining numeric relations by "<"
ord09 : assert (x <= y) <-> (x<y) | (x==y);
ord10 : assert (x>y) <-> (y<x);
ord11 : assert (x>=y) <-> !(x<y);
ord12 : assert (x==y) <-> !(x<y) & !(y<x);

// --- defining numeric relations by " <= "
ord13 : assert (x<y) <-> (x <= y) & !(y <= x);
ord14 : assert (x>y) <-> !(x <= y);
ord15 : assert (x>=y) <-> (y <= x);
ord16 : assert (x==y) <-> (x <= y) & (y <= x);

// --- ring axioms ---------------------
r01 : assert x+0==x;
r02 : assert x+y==y+x;
r03 : assert (x+y)+z == x+(y+z);
r04 : assert x+(0-x)==0;

// --- arithmetic laws ---------------------
arith00 : assert x*0==0;
arith01 : assert (x+y)-x==y;
arith03 : assert x-(y+z) == x-y-z;
arith04 : assert 1*x == x;
arith05 : assert 2*x == x+x;
arith06 : assert 3*x == x+x+x;

// --- monotonicity ------------------------
mono00 : assert (x==y) <-> (x+z==y+z);
mono01 : assert (x <= y) <-> (x+z <= y+z);
mono02 : assert (x<y) <-> (x+z<y+z);
mono03 : assert (x+y==0) & (0 <= x) & (0 <= y) -> (x==0) & (y==0);
mono04 : assert (x+y==x) -> (y==0);
mono05 : assert (x<y) & (0 <= z) -> (x<y+z);
mono06 : assert (x<y) & (y <= z) -> (x<z);

// --- other stuff ------------------------
div2 : assert exists y:int. ((x == y+y) | (x == y+y+1));
div3 : assert exists y:int. ((x == y+y+y) | (x == y+y+y+1) | (x == y+y+y+2));
div4 : assert exists y:int. ((x == y+y+y+y) | (x == y+y+y+y+1) | (x == y+y+y+y+2) | (x == y+y+y+y+3));
div5 : assert exists y:int. ((x == y+y+y+y+y) | (x == y+y+y+y+y+1) | (x == y+y+y+y+y+2) | (x == y+y+y+y+y+3) | (x == y+y+y+y+y+4));
unbounded : assert exists y:int. (x<y);
}

```