% 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; ";