Definition u16Min : Z := 0.
