home *** CD-ROM | disk | FTP | other *** search
/ ftp.cs.yorku.ca 2015 / ftp.cs.yorku.ca.tar / ftp.cs.yorku.ca / pub / peter / SVT / equality.simp < prev    next >
Text File  |  2000-01-24  |  1KB  |  55 lines
  1. % EQUALITY MODULE
  2.  
  3. max(A,C) = C ->> A <= C.
  4. max(B,C) = B ->> C <= B.
  5.  
  6.  
  7. X <=Y and not Y <= X ->> X < Y.
  8. X <= Y and not X = Y ->> X < Y.
  9. X <= Y and not Y = X ->> X < Y.
  10. X <= Y or Y < X ->> true. 
  11. X = Y and X <= Y ->> X = Y.
  12. X = Y and Y <= X ->> X = Y.
  13. X and Y = Z and Y <= Z ->> X and Y = Z.
  14. X < Y < Z ->> X < Y and Y < Z.
  15. X < Y <= Z ->> X < Y and Y <= Z.
  16. X <= Y < Z ->> X <= Y and Y < Z.
  17. X=X ->> true.
  18. X < X ->> false.
  19. X < Y and Y < Z and not X < Z ->> false.
  20.  
  21. % X <= Y ->> X=Y or X < Y.
  22.  
  23. X = Y ->> false :- number(X), number(Y), X =\= Y.
  24. X < Y ->> true :- number(X), number(Y), X < Y.
  25.  
  26. X <> Y ->> true :- number(X), number(Y), X \== Y.
  27. X <> Y ->> not(X=Y).
  28.  
  29. X + Y = Z ->> X = D :- D assigned Z - Y.
  30. X - Y = Z ->> X = D :- D assigned Z + Y.
  31.  
  32. X + Y = X ->> Y = 0.
  33. X - Y = X ->> Y = 0.
  34.  
  35. X < X + Y ->> 0 < Y.
  36. X < Y ->> true :- D assigned (Y-X), 0 < D.
  37. X < Y ->> false :- D assigned (X-Y), 0 =< D.
  38.  
  39. X + Y < 0 ->> X < D :- D assigned -Y.
  40.  
  41. X + Y + Z = X + U + V ->> Y + Z = U + V.
  42. X + Y + Z = U + X + V ->> Y + Z = U + V.
  43. X + Y + Z = U + V + X ->> Y + Z = U + V.
  44. X + Y + Z = U + V + Y ->> X + Z = U + V.
  45.  
  46. X * Y * Z = U * X * V ->> Y * Z = U * V.
  47. X * Y * Z = U * V * X ->> Y * Z = U * V.
  48. X * Y * Z = X * U * V ->> Y * Z = U * V.
  49.  
  50.  
  51.  
  52.  
  53.  
  54.  
  55.