THEORY exercise IS

  aa~ + (bb + cc) = aa~ + bb + cc

TAC

  rulesX~

END

&

THEORY rulesX IS

  x~ + y == (x + y)~;

  aa + (bb + cc) == (aa + bb + cc)


END
