1 2 3 4 5 6 7 8 9 10 11 12
(datatype KAT (par KAT KAT) ) (constructor AConst () KAT) (let $A (AConst)) (rewrite (par p p) p) (rule ((= r (par q r)) (= q (par q r))) ((union r q))) ; tests (let $q (par $A $A)) (run 10)