Specification Files

The user may specify a set of Autowrite objects (Trss, automata, termsets) related to a common signature and set of variable, in a specification file whose name should have the extension .txt.

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)))