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 }
.