```// **************************************************************************
//
//    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
//
// **************************************************************************
//  This file demonstrates the theorem proving facilities of Averest
//  concerning bitvectors.
// **************************************************************************

macro range = 16;

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

// --- " <= " is a total order
ord00 : assert (-range <= x) & (x < range);
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);

// --- field axioms ---------------------
f01 : assert x + +0 == x;
f02 : assert x + y == y + x;
f03 : assert (x + y) + z == x + (y + z);
f04 : assert x + (+0 - x) == +0;
f05 : assert x * +0 == +0;
f06 : assert x == x * +1;
f07 : assert x * y == y * x;
f08 : assert x * (y * z) == (x * y) * z;
f09 : assert x * (y + z) == x * y + x * z;

// --- monotonicity ------------------------
mono00: assert (x == y) <-> (x + z == y + z);
mono01[DisProveA]: assert (x <= y) <-> (x + z <= y + z);
// counterexample for mono01: assert  x == 0000, y=1000, z=1000
mono02[DisProveA]: assert (x < y) <-> (x + z < y + z);
// counterexample for mono02: assert  x == 0000, y=1000, z=1000
mono03: assert (x + y == +0) & (+0 <= x) & (+0 <= y) -> (x == +0) & (y == +0);
mono04: assert (x + y == x) -> (y == +0);
mono05[DisProveA]: assert (x < y) & (+0 <= z) -> (x < y+z);
// counterexample for mono05: assert  x == 0000, y=0100, z=0100
mono06: assert (x < y) & (y <= z) -> (x < z);

// --- division  ------------------------
div1 : assert !(y == +0) -> (+0 <= x % y);
div2 : assert (+0 < y) -> (x % y < y);
div3 : assert (y < +0) -> (y < x % y);
div4 : assert (y!=+0) -> (x == (x / y) * y + (x % y));
}

```