Certificate for #4125 ⟨a, b | aab=aaa, baa=b⟩

Back:⟨a, b | aab=aaa, baa=b⟩

Completion settings:

[1] aaa=aab

Axiom: aab=aaa.

Flip LHS and RHS.

Defines rule #3.

Referenced by [3].

[2] baa=b

Axiom: baa=b.

Referenced by [3], [4].

[3] ba=bb

Overlap of [2] baa=b with [1] aaa=aab:

b aa aaa

Critical pair: baab=ba.

Reduce LHS:

[2](baa)b
⇒ bb

Flip LHS and RHS.

Defines rule #1.

Referenced by [4].

[4] bbb=b

Overlap of [2] baa=b with [3] ba=bb:

baa ba

Critical pair: bba=b.

Reduce LHS:

[3]b(ba)
⇒ bbb

Defines rule #2.