understanding loop invariants
The reverse of X[:i], the prefix of X up to the $i$-th position is equal to Y[n-i+1:], the suffix of Y from the $(n-i+1)$-th position onward.
Before the loop starts, which we could consider as $i=0$, we have that the reverse of the prefix of X of length zero is equal to suffix of Y of length zero.
Each step of the loop preserves the property for the previous value of i and makes the property true for the current value of i.
At the end of the loop the property is satisfied for i=n, which implies that the reverse of X is equal to Y.