A single TRS is inputted by typing the rules into the upper left text area or by uploading a file via the browse button. The size of the TRS may not exceed 10K. In the latter case, the file name must match the pattern [a-zA-Z0-9][.a-zA-Z0-9_]*.trs.
A TRS is presented as a sequence of rewrite rules, separated by semi-colons. Rewrite rules are pairs of terms, separated by "->".
Terms are built from variables and function symbols, using commas and parentheses (and spaces). Variables and function symbols must start with a lowercase letter and may contain uppercase letters, digits, underscores, and the sharp "#" and single quote "'" characters. To distinguish variables from constants, the latter must be followed by "()". Alternatively, a list of variables (like [m,n,x,y]) may be given before the sequence of rewrite rules. In addition, numbers as well as the string "" (both without "()") are treated as constants. We also allow binary infix operators that consist of one or more of the characters "+", "-", "*", ":", ".", "/", "\", "=", "|", "@", "<" and ">".
TRSs may also be inputted in the official format of the Termination Problems Data Base.
The following rules for computing disjunctive normal forms adhere to
the above syntax:
not(not(x)) -> x;
not(x \/ y) -> not(x) /\ not(y);
not(x /\ y) -> not(x) \/ not(y);
x /\ (y \/ z) -> (x /\ y) \/ (x /\ z);
(y \/ z) /\ x -> (x /\ y) \/ (x /\ z)
Here is another example:
 @ y -> y ;
(n:x) @ y -> n:(x @ y) ;
0 <= y -> true() ;
s(x) <= 0 -> false() ;
s(x) <= s(y) -> x <= y ;
low(n,) ->  ;
low(n,m:x) -> ifLow(m<=n,n,m:x) ;
high(n,) ->  ;
high(n,m:x) -> ifHigh(m<=n,n,m:x) ;
ifLow(true(),n,m:x) -> m:low(n,x) ;
ifLow(false(),n,m:x) -> low(n,x) ;
ifHigh(true(),n,m:x) -> high(n,x) ;
ifHigh(false(),n,m:x) -> m:high(n,x) ;
quicksort() ->  ;
quicksort(n:x) -> quicksort(low(n,x)) @ (n:quicksort(high(n,x)))
TYPES 0 : N ; s : N => N ; id : N => N ; add : N => N => N ; map : (N => N) => L => L ; nil : L ; cons : N => L => L RULES id x -> x ; add 0 -> id ; add (s x) y -> s (add x y) ; map f nil -> nil ; map f (cons x xs) -> cons (f x) (map f xs)