This MR adds:
- The symmetric and reflexive/transitive/symmetric closure of a relation
- Different notions of confluence: diamond property, confluence, local confluence (following the naming conventions in https://www21.in.tum.de/~nipkow/TRaAT/)
- Standard properties such as diamond ⊢ confluence ⊢ local confluence, the Church-Rosser property, Newman's lemma
As part of this MR, I removed the hint database
ars. The name made no sense and it was not used anywhere to my knowledge. If it was used anywhere, it would be very unreliable as it contained hints like
rtc_trans that would generally lead to loops.