Definition s16Max : Z := (2 ^ 15) - 1.
