Definition x := nat.