solution for 3a

[ar1516.git] / a2 / src / 3a.prvr9

diff --git a/a2/src/3a.prvr9 b/a2/src/3a.prvr9
index 812fdd4..a12d73d 100644 (file)
--- a/a2/src/3a.prvr9
+++ b/a2/src/3a.prvr9
@@ -1,11 +1,11 @@
 formulas(assumptions).
 all x all y all z (x*(y*z)=(x*y)*z).
-all x (x*I=x).
-all x (x*inv(x)=I).
+all x (x*a=x).
+all x (x*inv(x)=a).
 end_of_list.
 formulas(goals).
-%I*x=x.
+%a*x=x.
 %inv(inv(x))=x.
-%inv(x)*x=I.
+%inv(x)*x=a.
 all x all y (x*y=y*x).
 end_of_list.