Definition s32Max : Z := (2 ^ 31) - 1.
