Format

The syntax of the TRS format is specified as follows:

 TRS ::= ( format TRS ) fun* rule*
 fun ::= ( fun identifier number )
rule ::= ( rule term term )

Function symbols and their arities are declared by (fun f n). Function symbols must be declared once. Undeclared identifiers are regarded as variables. In terms, function symbols must be used with the same number of arguments as specified in their arities. So with (fun f 1) and (fun a 0) the rules (rule (f a) (f a a)) and (rule a f) are ill-formed. Moreover, rules should respect the usual variable conditions: left-hand sides cannot be variables and variables occurring in right-hand sides must occur in the corresponding left-hand sides. So (rule x (f a)) and (rule (f x) y) are ill-formed rules.

Examples

; @author Christina Kohl
; @cops 1655
; secret problem 2022
(format TRS)
(fun f 2)
(fun g 1)
(fun a 0)
(fun b 0)
(rule (f x1 (g x2)) (f x1 (g x1)))
(rule (f (g y1) y2) (f (g y1) (g y1)))
(rule (g a) (g b))
(rule b a)

Here x1, x2, y1 and y2 are variables.

; @author Franziska Rapp
; @cops 557
(format TRS)
(fun f 2)
(fun a 0)
(fun b 0)
(fun c 0)
(rule a b)
(rule (f x a) (f b b))
(rule (f b x) (f b b))
(rule (f (f x y) z) (f b b))

Note that the contant c does not appear in the rewrite rules.