(* Verification Conditions for Alt-Ergo *)

logic fact : int -> int
axiom A1: fact(0)=1
axiom A2: forall n: int. n>0 -> fact(n)=n*fact(n-1)

logic i, f, n: int

goal intra_loop:
(i<=n and 
f=fact(i-1) and 
(i>0) and 
i<=(n+1)  ->
     (f*i)=fact(i) and 
     ((i+1)>0) and 
     i<=n)


goal exit:
((i>=(n+1)) and 
f=fact(i-1) and 
(i>0) and 
i<=(n+1)  ->
     f=fact(n))


goal start:
((n>=0)  ->
     1=fact(0) and 
     (1>0) and 
     0<=n)