Certificate for #4682 ⟨a, b | aabbaaab=abb⟩

Completion settings:

• Reduction order:
  • Right-to-left shortlex with a < b

Axiom: aabbaaab=abb.

Defines rule #1.

Referenced by [2], [3], [5].

Overlap of [1] aabbaaab=abb with [1] aabbaaab=abb:

Critical pair: aabbaabb=abbbaaab.

Defines rule #2.

Referenced by [3], [4].

Overlap of [2] aabbaabb=abbbaaab with [1] aabbaaab=abb:

Critical pair: aabbabb=abbbaaabaaab.

Flip LHS and RHS.

Defines rule #3.

Referenced by [5], [6].

Overlap of [2] aabbaabb=abbbaaab with [2] aabbaabb=abbbaaab:

Critical pair: aabbabbbaaab=abbbaaabaabb.

Flip LHS and RHS.

Defines rule #4.

Overlap of [1] aabbaaab=abb with [3] abbbaaabaaab=aabbabb:

Critical pair: aabbaaaabbabb=abbbbaaabaaab.

Defines rule #5.

Overlap of [3] abbbaaabaaab=aabbabb with [3] abbbaaabaaab=aabbabb:

Critical pair: abbbaaabaaaabbabb=aabbabbbbaaabaaab.

Defines rule #6.