ITRS syntax is similar to TRS syntax. Most notable differences are the existence of predefined operators, which must be used in infix notation.

Predefined symbols may not occur on the LHS, Conditions may not contain non-predefined function symbols.

Line based comments are introduced with a "#" char.

Program = { "(" Decl ")" }. Decl = "VAR" {Id} | "RULES" {Rule}. Id = Alnum { Alnum | "_" } | """ Escape_Sequence """ Rule = Term "->" Term | Term "->" Term ":|:" Term Term = "TRUE" | "FALSE" | Int | Id | Id "(" ")" | Id "(" Termlist ")" | Term Infix Term | Unary Term

*Alnum* is any character from a-z, A-Z, 0-9.

*Escape_Sequence* is a non empty sequency of (unicode) characters, excluding "\", """, newline and carriage return. "\" may be entered as "\\", """ as "\"" and an arbitrary unicode character may be entered as \uXXXX were XXXX is the character code in hex.

*Infix* are the predefined symbols *, /, %, +, -, <, <=, =, >=, >, |, ^, &, ||, &&; *Unary* the predefined symbols - and !. Precedence is java-like, if unsure, use parentheses. Integers and Predefined symbols operating on integers have a suffix "@X" were X is either "z" or a power of two, designating the domain (**Z** or **Z**/n**Z**). At the moment, termination analysis is only supported over **Z**. "@z" is the default and may be omitted.