Certificate for #3670 ⟨a, b | aabbbaabba=b⟩

Completion settings:

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

Axiom: aabbbaabba=b.

Defines rule #1.

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

Overlap of [1] aabbbaabba=b with [1] aabbbaabba=b:

Critical pair: aabbbaabbb=babbbaabba.

Defines rule #2.

Referenced by [3], [4].

Overlap of [2] aabbbaabbb=babbbaabba with [1] aabbbaabba=b:

Critical pair: aabbbb=babbbaabbaaabba.

Flip LHS and RHS.

Defines rule #4.

Referenced by [5], [6].

Overlap of [2] aabbbaabbb=babbbaabba with [2] aabbbaabbb=babbbaabba:

Critical pair: aabbbbabbbaabba=babbbaabbaaabbb.

Flip LHS and RHS.

Defines rule #5.

Overlap of [1] aabbbaabba=b with [3] babbbaabbaaabba=aabbbb:

Critical pair: aabbbaabaabbbb=bbbbaabbaaabba.

Defines rule #3.

Overlap of [3] babbbaabbaaabba=aabbbb with [3] babbbaabbaaabba=aabbbb:

Critical pair: babbbaabbaaabaabbbb=aabbbbbbbaabbaaabba.

Defines rule #6.