(* Verification Conditions for Alt-Ergo *)

logic power : int, int -> int
axiom A1: forall x, y: int. (y=0  ->
     power(x,y)=1)

axiom A2: forall x, y: int. ((y>0)  ->
     power(x,y)=(x*power(x,y-1)))


logic x, y, i, n: int

goal intra_loop:
((i<n) and 
y=power(x,i) and 
(i>0) and 
i<=n  ->
     (y*x)=power(x,i+1) and 
     ((i+1)>0) and 
     (i+1)<=n)


goal exit:
((i>=n) and 
y=power(x,i) and 
(i>0) and 
i<=n  ->
     y=power(x,n))


goal start:
((x>0) and 
(n>0)  ->
     x=power(x,1) and 
     (1>0) and 
     1<=n)