Certificate for #3682 ⟨a, b | aabbbbaaba=b⟩

Completion settings:

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

Axiom: aabbbbaaba=b.

Defines rule #1.

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

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

Critical pair: aabbbbaabb=babbbbaaba.

Defines rule #2.

Referenced by [3], [4].

Overlap of [2] aabbbbaabb=babbbbaaba with [1] aabbbbaaba=b:

Critical pair: aabbbbb=babbbbaababbaaba.

Flip LHS and RHS.

Defines rule #4.

Referenced by [5], [6].

Overlap of [2] aabbbbaabb=babbbbaaba with [2] aabbbbaabb=babbbbaaba:

Critical pair: aabbbbbabbbbaaba=babbbbaababbaabb.

Flip LHS and RHS.

Defines rule #5.

Overlap of [1] aabbbbaaba=b with [3] babbbbaababbaaba=aabbbbb:

Critical pair: aabbbbaaaabbbbb=bbbbbaababbaaba.

Defines rule #3.

Overlap of [3] babbbbaababbaaba=aabbbbb with [3] babbbbaababbaaba=aabbbbb:

Critical pair: babbbbaababbaaaabbbbb=aabbbbbbbbbaababbaaba.

Defines rule #6.