AProVE Help: Term Rewrite Systems

Syntax of SRS input files (*.srs)

      Program      = { "(" Decl ")" }.
      Decl         = "VAR" {Id} | "THEORY" { "(" ThDecl ")" } | "RULES" {Rule} | "STRATEGY" StrategyDecl | Id [AnyList].
      AnyList      = Any {"," Anylist}.
      Any          = Id | String | "(" AnyList ")".
      ThDecl       = {Id} | "A" {Id} | "C" {Id} | "AC" {Id} | "EQUATIONS" {Equation}.
      Equation     = Term   "=="   Term.
      Rule         = Term  "->"   Term | Term  "->"  Term   | CondList.
      CondList     = Cond { "," Cond }.
      Cond         = Term   "->"   Term | Term   "-><-"   Term.
      Term         = Id | Id "(" ")" | Id "(" Termlist ")".
      Termlist     = Term {"," Term}.
      StrategyDecl = INNERMOST | CONTEXTSENSITIVE {Replacements}.
      Replacements = "(" Id  {int} ")".

Id are non-empty sequences of characters except space, '(', ')', '"' and ',' and excluding special sequences '->', '==', '-><-', '|' and keywords CONTEXTSENSITIVE, EQUATIONS, INNERMOST, RULES, STRATEGY, THEORY and VAR.

string are sequences of any characters between double quotes

int are non-empty sequences of digits

Semantical conditions

a symbol declared in a VAR section must not have been used in previous declarations, and is assumed to denote a variable in remaining declarations (in particular must not be applied to arguments)
a symbol occuring in a RULES section which has not been used before is assumed to denote a function symbol, and must be used afterwards always with the same arity.