a2/src/3a.prvr9

   1 formulas(assumptions).
   2 x*(y*z)=(x*y)*z.
   3 x*I=x.
   4 x*inv(x)=I.
   5 end_of_list.
   6 formulas(goals).
   7 %I*x=x.
   8 %inv(inv(x))=x.
   9 %inv(x)*x=I.
  10 x*y=y*x.
  11 end_of_list.