23 Jul
2021
23 Jul
'21
09:44
Hello. When a symbol is declared AC in the TRS format, which relation is (dis)proved terminating? Is it rewriting with matching modulo AC or rewriting modulo AC, i.e. rewriting on AC-classes?