Certificate for #21725 ⟨a, b | aaa=1, abababb=b⟩

Back:⟨a, b | aaa=1, abababb=b⟩

Completion settings:

[1] aaa=1

Axiom: aaa=1.

Defines rule #1.

Referenced by [3], [6].

[2] abababb=b

Axiom: abababb=b.

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

[3] bababb=aab

Overlap of [1] aaa=1 with [2] abababb=b:

aa a abababb

Critical pair: aab=bababb.

Flip LHS and RHS.

Defines rule #2.

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

[4] abababaab=aab

Overlap of [2] abababb=b with [3] bababb=aab:

ababab b bababb

Critical pair: abababaab=bababb.

Reduce RHS:

[3](bababb)
⇒ aab

Referenced by [6].

[5] bababaab=ab

Overlap of [3] bababb=aab with [3] bababb=aab:

babab b bababb

Critical pair: bababaab=aabababb.

Reduce RHS:

[2]a(abababb)
⇒ ab

Defines rule #4.

Referenced by [6].

[6] bababab=b

Overlap of [3] bababb=aab with [5] bababaab=ab:

babab b bababaab

Critical pair: bababab=aabababaab.

Reduce RHS:

[4]a(abababaab)
[1]⇒ (aaa)b
⇒ b

Defines rule #3.