Confluence Competition

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 ≤ in 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 { af(b), f(a)b } as the first and { af(b), h(a,a)b, f(b)b } as the second TRS over the common signature { a:0, b:0, f:1, h:2 }.