logic gcd : int, int -> int
axiom A1: forall x: int. forall y: int. x=y -> gcd(x,y)=x
axiom A2: forall x: int. forall y: int. x>y -> gcd(x,y)=gcd(x-y,y)
axiom A3: forall x: int. forall y: int. x<y -> gcd(x,y)=gcd(x,y-x)

logic x, y, m, n: int

goal intra_loop:
(not((x=y)) and 
gcd(x,y)=gcd(m,n) and 
(x>=1) and 
(y>=1)  ->
     ((x>y)  ->
          gcd(x-y,y)=gcd(m,n) and 
          ((x-y)>=1) and 
          (y>=1))
 and 
     (not((x>y))  ->
          gcd(x,y-x)=gcd(m,n) and 
          (x>=1) and 
          ((y-x)>=1))
)


goal exit:
(x=y and 
gcd(x,y)=gcd(m,n) and 
(x>=1) and 
(y>=1)  ->
     x=gcd(m,n))


goal start:
(x=m and 
y=n and 
(m>0) and 
(n>0)  ->
     gcd(x,y)=gcd(m,n) and 
     (x>=1) and 
     (y>=1))