An Autowrite specification file starts with the definition of a signature, eventually followed by the definition of a set of variables. Next we may have in any order definitions of TRSs, automata, termsets, each one of them associated with a distinct name.

Example: `WRS.txt`

Ops 0:0 s:1 +:2 *:2 Vars x y TRS R ; addition +(0,x) -> x +(s(x),y) -> s(+(x,y)) ; product *(0,x) -> 0 *(s(x),y) -> +(*(x,y),y) Automaton EVEN States odd even Final States even Transitions 0 -> even s(even) -> odd s(odd) -> even Termset RS 0 s(x) Termset "T(F)" x Term *(*(0,s(0)),+(0,s(0))) Term *(o,+(0,s(0))) Term *(*(0,s(0)),o) Term s(s(s(0)))

2005-02-01