Certificate for #25203 ⟨a, b | aa=a, abbab=bab⟩

Back:⟨a, b | aa=a, abbab=bab⟩

Completion settings:

[1] aa=a

Axiom: aa=a.

Defines rule #1.

Referenced by [3].

[2] abbab=bab

Axiom: abbab=bab.

Referenced by [3], [4].

[3] abab=bab

Overlap of [1] aa=a with [2] abbab=bab:

a a abbab

Critical pair: abab=abbab.

Reduce RHS:

[2](abbab)
⇒ bab

Defines rule #2.

Referenced by [4].

[4] bbab=bab

Overlap of [3] abab=bab with [2] abbab=bab:

ab ab abbab

Critical pair: abbab=babbab.

Reduce LHS:

[2](abbab)
⇒ bab

Reduce RHS:

[2]b(abbab)
⇒ bbab

Flip LHS and RHS.

Defines rule #3.