This page explains the format for many-sorted TRSs. Any many-sorted TRS with a unique sort is identified with the TRS in the obvious way.
In the MSTRS format, sorted function symbols and rules are specified. Formally, decl of the grammar of the old TPDB format is replaced as follows:
........... decl ::= RULES listofrules | SIG funlist | id anylist funlist ::= | fun funlist fun ::= ( id sort ) sort ::= idlist -> id idlist ::= e | id idlist ...........
An example of the format is as follows:
(SIG (app List List -> List) (cons Nat List -> List) (nil -> List) (s Nat -> Nat) (0 -> Nat) ) (RULES app(nil,ys) -> ys app(cons(x,xs),ys) -> cons(x,app(xs,ys)) )
Here is a converter between the TRS format and the MSTRS format.