OBJ> obj PROJECTIE is
  protecting BOOL .
  sorts element of Bool .
  op o : -> element .
  op _ * _ : element element -> element .
  op _ / _ : element element -> element .
  var x : element .
  var y : element .
  var z : element .
  [e1] eq x * o = x .
  [e2] eq o * x = x .
  [e3] eq x / o = x .
  [e4] eq o / x = o .
  [e5] eq x / x = o .
  [e6] eq (x * y) / z = (x / z) * (y / (z / x)) .
  [e7] eq z / (x * y) = (z / x) / y .	
endo

Te controleren kritische paren:

< o * o ,  o * o > 		(1,2)
< (x * o) / z , (x * o) / z > 	(1,6)
< z / (x * o) , z / (x * o) > 	(1,7)

< (o * x) / z , (o * x) / z > 	(2,6)
< z / (o * x) , z / (o * x) > 	(2,7)

< o / o ,  o / o > 		(3,4)
< o / o , o / o > 	(3,5)
< (x * y) / o , (x * y) / o > 	(3,6)

< o / o , o / o > 	(4,5)
< o / (x * y) , o / (x * y) > (4,7)

< (x * y) / (x * y) , (x * y) / (x * y) > 	(5,6)
< (x * y) / (x * y) , (x * y) / (x * y) > 	(5,7)

< (x * y) / (z * u) , (x * y) / (z * u) > 	(6,7)

Instantiering geeft ons :

o * o 			(1,2)
o / o 			(3,4);(3,5);(4,5)
(o * o) / o 		(1,6);(2,6);(3,6)
o / (o * o) 		(1,7);(2,7);(4,7)
(o * o) / (o * o) 	(5,6);(5,7);(6,7)

Al deze paren herschrijfregels lossen op voor de respectieve instanties.