Certificate for #19245 ⟨a, b | aaa=a, aaabb=ba⟩

Back:⟨a, b | aaa=a, aaabb=ba⟩

Completion settings:

[1] aaa=a

Axiom: aaa=a.

Defines rule #3.

Referenced by [2], [3].

[2] ba=abb

Axiom: aaabb=ba.

Reduce LHS:

[1](aaa)bb
⇒ abb

Flip LHS and RHS.

Defines rule #2.

Referenced by [3].

[3] abbbbbbbb=abb

Overlap of [2] ba=abb with [1] aaa=a:

b a aaa

Critical pair: ba=abbaa.

Reduce LHS:

[2](ba)
⇒ abb

Reduce RHS:

[2]ab(ba)a
[2]⇒ a(ba)bba
[2]⇒ aabbb(ba)
[2]⇒ aabb(ba)bb
[2]⇒ aab(ba)bbbb
[2]⇒ aa(ba)bbbbbb
[1]⇒ (aaa)bbbbbbbb
⇒ abbbbbbbb

Flip LHS and RHS.

Defines rule #1.