Definition s8Max  : Z := (2 ^ 7) - 1.
