(* Verification Conditions for Alt-Ergo *)


logic x, y, m, n: int

goal start:
(x=m and 
y=n  ->
     ((x+y)-((x+y)-y))=n and 
     ((x+y)-y)=m
)