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 >
Wrap
Text File
|
2000-01-24
|
1KB
|
55 lines
% EQUALITY MODULE
max(A,C) = C ->> A <= C.
max(B,C) = B ->> C <= B.
X <=Y and not Y <= X ->> X < Y.
X <= Y and not X = Y ->> X < Y.
X <= Y and not Y = X ->> X < Y.
X <= Y or Y < X ->> true.
X = Y and X <= Y ->> X = Y.
X = Y and Y <= X ->> X = Y.
X and Y = Z and Y <= Z ->> X and Y = Z.
X < Y < Z ->> X < Y and Y < Z.
X < Y <= Z ->> X < Y and Y <= Z.
X <= Y < Z ->> X <= Y and Y < Z.
X=X ->> true.
X < X ->> false.
X < Y and Y < Z and not X < Z ->> false.
% X <= Y ->> X=Y or X < Y.
X = Y ->> false :- number(X), number(Y), X =\= Y.
X < Y ->> true :- number(X), number(Y), X < Y.
X <> Y ->> true :- number(X), number(Y), X \== Y.
X <> Y ->> not(X=Y).
X + Y = Z ->> X = D :- D assigned Z - Y.
X - Y = Z ->> X = D :- D assigned Z + Y.
X + Y = X ->> Y = 0.
X - Y = X ->> Y = 0.
X < X + Y ->> 0 < Y.
X < Y ->> true :- D assigned (Y-X), 0 < D.
X < Y ->> false :- D assigned (X-Y), 0 =< D.
X + Y < 0 ->> X < D :- D assigned -Y.
X + Y + Z = X + U + V ->> Y + Z = U + V.
X + Y + Z = U + X + V ->> Y + Z = U + V.
X + Y + Z = U + V + X ->> Y + Z = U + V.
X + Y + Z = U + V + Y ->> X + Z = U + V.
X * Y * Z = U * X * V ->> Y * Z = U * V.
X * Y * Z = U * V * X ->> Y * Z = U * V.
X * Y * Z = X * U * V ->> Y * Z = U * V.