## CSTRS Format

The format for context-sensitive term rewrite systems is an extension of the basic TRS format, according to the following grammar:

The restrictions oncsrs::=[(VARidlist)](REPLACEMENT-MAPcslist) (RULESrulelist)[(COMMENTstring)]idlist::=ε|ididlistrulelist::=ε|rulerulelistrule::=term->termterm::=id|id()|id(termlist)termlist::=term|term,termlist

`id`

and
`string`

are the same as in the
TRS format and `cslist`

specifies the replacement map:
Herecslist::=fun|funcslistfun::=(idintlist)intlist::=ε|int,intlist

`int`

is a nonempty sequence of digits, denoting
an argument position. Function symbols declared in
`cslist`

must appear as function symbols in
`(RULES ``rulelist`)

and may not appear as variables in
`(VAR ``idlist`)

.
The `intlist`

declaration is a list of strictly
increasing positive integers corresponding to the active (replacing)
argument positions of function symbol `id`

. Function
symbols may appear only once in
`(REPLACEMENT-MAP ``cslist`)

. If a function symbol in
`(RULES ``rulelist`)

is not listed in the
`(REPLACEMENT-MAP ``cslist`)

, all its argument
positions are considered active.
### Example

(VAR L X) (REPLACEMENT-MAP (cons 1) ) (RULES incr(nil) -> nil incr(cons(X,L)) -> cons(s(X),incr(L)) adx(nil) -> nil adx(cons(X,L)) -> incr(cons(X,adx(L))) nats -> adx(zeros) zeros -> cons(0,zeros) head(cons(X,L)) -> X tail(cons(X,L)) -> L )