AProVE Help: Term Rewrite Systems

Syntax of TES input files (*.tes)

      Program    = [VarDecl] [AcDecl] [CDecl] [ADecl] Rule {Rule}.
      VarDecl    = "[" IdList "]".
      AcDecl     = "AC" "[" IdList "]".
      CDecl      = "C" "[" IdList "]".
      ADecl      = "A" "[" IdList "]".
      IdList     = Id { "," Id }.
      Id         = Name | InfixName {InfixName}.
      InfixName  = "@" | "&" | "%" | "/" | "\" | ":" | "-" | "+" | "*" | "." | "<" | ">" | "=" | "!" | "$" | "?" | "^".
      SimpleRule = Term  "->"  Term.
      CondRule   = SimpleRule {"," SimpleRule } "|" SimpleRule.
      Equation   = Term "==" Term.
      Rule       = SimpleRule | CondRule | Equation.
      PrefixTerm = Name | Name "(" Term {"," Term } ")" | "(" Term ")".
      InfixTerm  = PrefixTerm InfixName PefixTerm
      Term       = InfixTerm | PrefixTerm

Name are non-empty sequences of characters except space, '(', ')', '"' and ',' and excluding special sequences '->', '==', '|' and combinations of InfixNames

Examples

Simple Example


      [x,y]
      times(x,plus(y,1)) -> plus(times(x,plus(y,times(1,0))),x)
      times(x,1) -> x
      plus(x,0) -> x
      times(x,0) -> 0

Infix Example


      [x, y, u, v, w]

      (x + y) - y -> x
      0 / (y + 1) -> 0
      (x + 1) / (y + 1) -> ((x - y) / (y + 1)) + 1

      0 + 0 == 0
      1 + 0 == 1
      0 + 1 == 1
      u + (v + w) == (u + v) + w

Conditional Example


      [x, y, x', y', z]
      x -> 0, y -> y' | plus(x, y) -> y'
      x -> s(x'), y -> y' | plus(x, y) -> s(plus(x', y'))
      fibi(0) -> pair(0, s(0))
      fibi(x) -> pair(y, z) | fibi(s(x)) -> pair(z, plus(y, z))
      fib(x) -> sel(fibi(x))
      sel(pair(x, y)) -> x