% benchmark parameters -N8 -p % Find a noncommutative ring. To make it more difficult, assume % the ring has a unit. op(450, xfx, +). % sum op(400, xfx, *). % product op(350, fy, ~). % minus list(usable). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % RING AXIOMS % <+,~,0> is an Abelian group: 0+x=x. x+0=x. ~x+x=0. x+ ~x=0. (x+y)+z=x+ (y+z). x+y=y+x. % Product is associative: (x*y)*z=x* (y*z). % Left and right distributivity: x* (y+z)=x*y+x*z. (y+z)*x=y*x+z*x. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Ring lemmas ~ ~x=x. ~0=0. 0*x=0. x*0=0. % Assume the ring has a unit. 1*x=x. x*1=x. % There are 2 noncommuting elements. a*b!=b*a. % Using constants a and b as the noncommuting elements allows % the possibility that they can be 0 or 1. % Since 0 and 1 commute with everything, we could fix the % noncommuting elements by using 2*3!=3*2 instead. % In general it's a good idea to do this, but it doesn't make % much difference in this case. % % 2*3!=3*2. end_of_list.