Adapting the ARI format for Equational Rewriting

[ffrohn]

Since we want to use the ARI format in the future, we have to extend it for equational rewriting. Here's a first proposal:

  ETRS ::= ( format ETRS ) fun* rule*
   fun ::= ( fun identifier number theory? )
theory ::= ( :theory [A | AC | C] )
  rule ::= ( rule term term )

What do you think?

[ffrohn]

Everybody seems to be happy with the proposal.