Certificate for #26679 ⟨a, b | aa=1, bababbab=b⟩

Back:⟨a, b | aa=1, bababbab=b⟩

Completion settings:

[1] aa=1

Axiom: aa=1.

Defines rule #1.

[2] bababbab=b

Axiom: bababbab=b.

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

[3] babbab=bababb

Overlap of [2] bababbab=b with [2] bababbab=b:

babab bab bababbab

Critical pair: bababb=babbab.

Flip LHS and RHS.

Referenced by [4], [5].

[4] bbab=babb

Overlap of [3] babbab=bababb with [2] bababbab=b:

bab bab bababbab

Critical pair: babb=bababbabbab.

Reduce RHS:

[2](bababbab)bab
⇒ bbab

Flip LHS and RHS.

Defines rule #2.

[5] babababb=b

Overlap of [2] bababbab=b with [3] babbab=bababb:

ba babbab babbab

Critical pair: babababb=b.

Defines rule #3.