update, table
[ar1516.git] / a2 / src / 3a.prvr9
index 8ee213c..812fdd4 100644 (file)
@@ -1,11 +1,11 @@
 formulas(assumptions).
-x*(y*z)=(x*y)*z.
-x*I=x.
-x*inv(x)=I.
+all x all y all z (x*(y*z)=(x*y)*z).
+all x (x*I=x).
+all x (x*inv(x)=I).
 end_of_list.
 formulas(goals).
 %I*x=x.
 %inv(inv(x))=x.
 %inv(x)*x=I.
-x*y=y*x.
+all x all y (x*y=y*x).
 end_of_list.