Add an ensures to memmove()

The first n bytes of the source and destination objects being disjoint
is a necessary and sufficient condition to conclude that the source was
not changed as a result of the copy operation.