Certificate for #3798 ⟨a, b | abbaaaaaab=b⟩

Completion settings:

• Reduction order:
  • Left-to-right shortlex with b < a

Axiom: abbaaaaaab=b.

Defines rule #7.

Referenced by [2], [3], [4], [5], [6], [7].

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

Critical pair: abbaaaaab=bbaaaaaab.

Defines rule #6.

Referenced by [3].

Overlap of [2] abbaaaaab=bbaaaaaab with [1] abbaaaaaab=b:

Critical pair: abbaaaab=bbaaaaaabbaaaaaab.

Reduce RHS:

Defines rule #5.

Referenced by [4].

Overlap of [3] abbaaaab=bbaaaaab with [1] abbaaaaaab=b:

Critical pair: abbaaab=bbaaaaabbaaaaaab.

Reduce RHS:

Defines rule #4.

Referenced by [5].

Overlap of [4] abbaaab=bbaaaab with [1] abbaaaaaab=b:

Critical pair: abbaab=bbaaaabbaaaaaab.

Reduce RHS:

Defines rule #3.

Referenced by [6].

Overlap of [5] abbaab=bbaaab with [1] abbaaaaaab=b:

Critical pair: abbab=bbaaabbaaaaaab.

Reduce RHS:

Defines rule #2.

Referenced by [7].

Overlap of [6] abbab=bbaab with [1] abbaaaaaab=b:

Critical pair: abbb=bbaabbaaaaaab.

Reduce RHS:

Defines rule #1.