-operator RR_REWRITE 2:3 "actual rewrite rule"
-operator RR_REDUCTION 2:3 "actual reduction rule"
-operator RR_DEDUCTION 2:3 "actual deduction rule"
+operator RR_REWRITE 2:3 "actual rewrite rule (for rewrite-rules theory)"
+operator RR_REDUCTION 2:3 "actual reduction rule (for rewrite-rules theory)"
+operator RR_DEDUCTION 2:3 "actual deduction rule (for rewrite-rules theory)"