## CSCTRS Format

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

The restrictions oncscrs::=(CONDITIONTYPEctype)[(VARidlist)](REPLACEMENT-MAPcslist) (RULESrulelist)[(COMMENTstring)]ctype::=SEMI-EQUATIONAL|JOIN|ORIENTEDidlist::=ε|ididlistrulelist::=ε|rulerulelistrule::=term->term|term->term|condlistcondlist::=cond|cond,condlistcond::=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

(CONDITIONTYPE ORIENTED) (VAR l x y) (REPLACEMENT-MAP (cons 2) (le 1) ) (RULES le(0,s(x)) -> true le(x,0) -> false le(s(x),s(y)) -> le(x,y) min(cons(x,nil)) -> x min(cons(x,l)) -> x | le(x,min(l)) == true min(cons(x,l)) -> min(l) | le(x,min(l)) == false min(cons(x,l)) -> min(l) | min(l) == x )