[Termtools] SRS-certified category?

[Juergen Giesl]

Dear all,

if I understand Rene's proposal correctly, then this would
mean that all SRSs would be copied so that they are contained both in
the SRS-category and in the TRS-category. I am not in favor of this,
because of two reasons:

1. Then the TRS-category would contain extremely many SRSs, i.e.,
   the TRS-collection would be very "biased" towards string rewriting.
   The message of this would be: string rewriting is the most
   interesting part of term rewriting and if you want to be "successful"
   for termination analysis of TRSs, then you should focus on SRSs.
   I disagree with this message.

2. I don't think that the same examples should occur twice in the
   data base. So an example should either be in the SRS- or
   in the TRS-category.

If there is a desire to treat all SRSs equal (and not have some
of them in the SRS-category and some of them in the TRS-category,
as it is the case up to now), then I have a different suggestion:
let's have the two categories "SRS" and "TRSs which are no SRSs".
Then the latter category would only include examples where at least
one function symbol has arity different from 0.

Best Regards
Juergen