Format

To represent multiple rewrite systems, we use :number n in the format specification, where n > 1 specifies the number of rewrite systems. Rewrite rules have an optional argument :index i where 1 ≤ i ≤ n specifies that the rule belongs to the i-th rewrite system. If the argument is not given, the rule belongs to all n rewrite systems

multiple-TRS ::= ( format TRS :number number ) fun* rule*
        rule ::= ( rule term term (:index number)? )

By setting n = 2 in the format declaration, we obtain the format that is used to specify commutation problems.

Example

(format TRS :number 2)
(fun f 1)
(fun h 2)
(fun a 0)
(fun b 0)
(rule a (f b))
(rule (f a) b :index 1)
(rule (h a a) b :index 2)
(rule (f b) b :index 2)

This example specifies { a → f(b), f(a) → b } as the first and { a → f(b), h(a,a) → b, f(b) → b } as the second TRS over the common signature { a:0, b:0, f:1, h:2 }.