Il faut "remarquer" que $x^y \times r$ est un invariant de boucle. Il est en effet évident que sa valeur ne change pas entre les lignes 2 & 3.

Donc sa valeur ne change pas entre les lignes 1 & 4.
À la ligne 1, sa valeur est $A^B$.
À la ligne 4, comme $y=0$ (on est sorti de la boucle), sa valeur est $r$.