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/nZ). At the moment, termination analysis is only supported over Z. "@z" is the default and may be omitted.