```// **************************************************************************
//
//    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 UnsignedBitArithmetic(
nat{range} x,y,z
)  {
nothing;
} satisfies {
// --- "<=" is a total order
ord00 : assert (0 <= 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)) % range == 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: 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 [DisProveA]: 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);

// --- modulo  ------------------------
mod1: assert !(y == 0) -> (0 <= x % y);
mod2: assert (0 < y) -> (x % y < y);
mod3: assert (y < 0) -> (y < x % y);
mod4: assert (x == (x / y) * y + (x % y));

}

```