Certificate for #16133 ⟨a, b | aab=aa, bbab=aa⟩

Back:⟨a, b | aab=aa, bbab=aa⟩

Completion settings:

[1] aab=aa

Axiom: aab=aa.

Referenced by [3].

[2] aa=bbab

Axiom: bbab=aa.

Flip LHS and RHS.

Defines rule #2.

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

[3] aab=bbab

Simplify [1] aab=aa.

Reduce RHS:

[2](aa)
⇒ bbab

Referenced by [4].

[4] bbabb=bbab

Overlap of [3] aab=bbab with [2] aa=bbab:

aab aa

Critical pair: bbabb=bbab.

Defines rule #1.

[5] bbaba=abbab

Overlap of [2] aa=bbab with [2] aa=bbab:

a a aa

Critical pair: abbab=bbaba.

Flip LHS and RHS.

Defines rule #3.