{ PRE: n >= 0 and x != 0 } { P5: n>=0 and x^n=1*x^n and x!=0 and x!=0 } k, y, z := n, 1, x { INV: k>=0 and x^n=y*z^k and x!=0 and z!=0 } while k != 0 do { P3: INV and k!=0 } if odd(k) { P2: (k-1)>=0 and x^n=(y*z)*z^(k-1) and x!=0 and z!=0 } then k, y := k-1, y * z { P1: (k/2)>=0 and x^n=y*(z*z)^(k/2) and x!=0 and (z*z)!=0 } else k, z := k/2, z * z endif { INV: k>=0 and x^n=y*z^k and x!=0 and z!=0 } endwhile { P4: INV and ~(k!=0) } { POST: y = x^n }