Definition u8Max  : Z := (2 ^ 8) - 1.
