## Single Rewrite Systems

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.

### Examples

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

## Multiple Rewrite Systems

A collection of TRSs can be given as input to TTT by uploading
a zip archive. The name of the archive must match
`[a-zA-Z0-9][a-zA-Z0-9_]*.zip`
and its size may not exceed 100K. All files matching
`[a-zA-Z0-9][.a-zA-Z0-9_]*.trs`
are extracted from the archive and the termination prover runs on each
of these files in turn.

## Simply-Typed Applicative Rewrite Systems

In addition to ordinary first-order rewrite systems as described above,
TTT can handle simply-typed applicative rewrite systems introduced by
Aoto and Yamada. A typical example is
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)