Certificate for #10279 ⟨a, b | aa=1, ababb=bab⟩

Completion settings:

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

Axiom: aa=1.

Defines rule #1.

Referenced by [3], [6], [7].

Axiom: ababb=bab.

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

Overlap of [1] aa=1 with [2] ababb=bab:

Critical pair: abab=babb.

Flip LHS and RHS.

Defines rule #2.

Referenced by [4], [5], [8].

Overlap of [2] ababb=bab with [3] babb=abab:

Critical pair: abababab=bababb.

Reduce RHS:

Referenced by [8].

Overlap of [3] babb=abab with [3] babb=abab:

Critical pair: bababab=abababb.

Reduce RHS:

Defines rule #5.

Referenced by [6].

Overlap of [5] bababab=abbab with [5] bababab=abbab:

Critical pair: baabbab=abbabab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [7], [8].

Overlap of [1] aa=1 with [6] abbabab=bbbab:

Critical pair: abbbab=bbabab.

Flip LHS and RHS.

Defines rule #3.

Overlap of [3] babb=abab with [6] abbabab=bbbab:

Critical pair: bbbbab=abababab.

Reduce RHS:

Defines rule #4.