Definition s64Max : Z := (2 ^ 63) - 1.
