% code for CiME tool specifing the TRS of the AMAST paper of 2008
% authors: C. Prisacariu and G. Schneider
% some versions of CiME have problems with comments. If this is the case just load the comments free file amast_CA_alg_TRS_nocoments.cim
% the signature specification
% the axioms of associativity and commutativity of + and & are given directly by defining the operators to be AC
% CiME does rewriting modulo AC as otherwise termination is not the case
let F = signature "a,b,0,1 : constant;
+ : AC;
. : infix binary;
& : AC;
";
% the variables declaration
let X = vars "x y z";
% the definition of the term rewriting system
% because CiME does not support subsorting we had to use "brute force" and encode all possible pairs for the last axiom
% We can do this because we have a finite number of basic actions
% note that we have here that & is idempotent but only over basic actions
let R = TRS F X "
x + 0 -> x;
x + x -> x;
x . 1 -> x;
1 . x -> x;
x . 0 -> 0;
0 . x -> 0;
(x . y) . z -> x . (y . z);
x . (y + z) -> (x . y) + (x . z);
(x + y) . z -> (x . z) + (y . z);
x & 1 -> x;
x & 0 -> 0;
a & a -> a;
b & b -> b;
x & (y + z) -> (x & y) + (x & z);
(x + y) & z -> (x & z) + (y & z);
(a . x) & (a . y) -> (a & a) . (x & y);
(a . x) & (b . y) -> (a & b) . (x & y);
(a . x) & (a & b . y) -> (a & a & b) . (x & y);
(b . x) & (b . y) -> (b & b) . (x & y);
(b . x) & (a & b . y) -> (b & a & b) . (x & y);
(a & b . x) & (a & b . y) -> (a & b & a & b) . (x & y);
a & (a . x) -> (a & a) . x;
a & (b . x) -> (a & b) . x;
a & (a & b . x) -> (a & a & b) . x;
b & (a . x) -> (b & a) . x;
b & (b . x) -> (b & b) . x;
b & (a & b . x) -> (b & a & b) . x;
a & b & (a & b . x) -> (a & b & a & b) . x;
a & b & (a . x) -> (a & b & a) . x;
a & b & (b . x) -> (a & b & b) . x;
";