Certificate for #2742 ⟨a, b | baaab=aaaba⟩

Back:⟨a, b | baaab=aaaba⟩

Completion settings:

[1] aaaba=baaab

Axiom: baaab=aaaba.

Flip LHS and RHS.

Defines rule #1.

Referenced by [2].

[2] bbbaaabba=aaabbaaab

Overlap of [1] aaaba=baaab with [1] aaaba=baaab:

aaab a aaaba

Critical pair: aaabbaaab=baaabaaba.

Reduce RHS:

[1]b(aaaba)aba
[1]⇒ bb(aaaba)ba
⇒ bbbaaabba

Flip LHS and RHS.

Defines rule #2.