Input Format of NaTT

sym ::=

• • <sym>
    • text
    </sym>

term ::=

• • sym constant or variable
• • <app>
    • sym function
    • term⁺ arguments
    </app>

cond ::=

• • <cond>
    • term
    • term
    </cond>

rule ::=

• • <rule>
    • term left hand side
    • term right hand side
    • cond* conditions
    </rule>

sym-decl ::=

• declares a variable symbol
  • <var>
    • text
    </var>
• declares a function symbol
  • <fun
    • theory="AC?|C"
    >
    • text
    </fun>

Content

• <trs>
  • sym-decl*
  • rule⁺
  • (<infeasibility>
    • sym-decl*
    • cond⁺
    </infeasibility>)^?
  </trs>