use pneq/2

This commit is contained in:
Markus Triska
2023-08-15 21:50:15 +02:00
parent 67c1b171c7
commit 7f024f3b8d

View File

@@ -2819,7 +2819,7 @@ matches([
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
m(var(X) #\= integer(Y)) => [g(neq_num(X, Y))],
m(var(X) #\= var(Y)) => [g(neq(X,Y))],
m(var(X) #\= var(Y)) => [p(pneq(X,Y))],
m(var(X) #\= var(Y) + var(Z)) => [p(x_neq_y_plus_z(X, Y, Z))],
m(var(X) #\= var(Y) - var(Z)) => [p(x_neq_y_plus_z(Y, X, Z))],
m(var(X) #\= var(Y)*var(Z)) => [p(ptimes(Y,Z,P)), g(neq(X,P))],