Certificate for #3485 ⟨a, b | aaabbaaaba=b⟩

Completion settings:

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

Axiom: aaabbaaaba=b.

Defines rule #1.

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

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

Critical pair: aaabbaaabb=baabbaaaba.

Defines rule #2.

Referenced by [3], [4].

Overlap of [2] aaabbaaabb=baabbaaaba with [1] aaabbaaaba=b:

Critical pair: aaabbb=baabbaaabaaaaba.

Flip LHS and RHS.

Defines rule #4.

Referenced by [5], [6].

Overlap of [2] aaabbaaabb=baabbaaaba with [2] aaabbaaabb=baabbaaaba:

Critical pair: aaabbbaabbaaaba=baabbaaabaaaabb.

Flip LHS and RHS.

Defines rule #5.

Overlap of [1] aaabbaaaba=b with [3] baabbaaabaaaaba=aaabbb:

Critical pair: aaabbaaaaaabbb=babbaaabaaaaba.

Defines rule #3.

Overlap of [3] baabbaaabaaaaba=aaabbb with [3] baabbaaabaaaaba=aaabbb:

Critical pair: baabbaaabaaaaaaabbb=aaabbbabbaaabaaaaba.

Defines rule #6.