Certificate for #13121 ⟨a, b | aab=aaa, aba=ab⟩

Back:⟨a, b | aab=aaa, aba=ab⟩

Completion settings:

[1] aaa=aab

Axiom: aab=aaa.

Flip LHS and RHS.

Defines rule #3.

Referenced by [3].

[2] aba=ab

Axiom: aba=ab.

Defines rule #2.

Referenced by [3].

[3] abb=ab

Overlap of [2] aba=ab with [1] aaa=aab:

ab a aaa

Critical pair: abaab=abaa.

Reduce LHS:

[2](aba)ab
[2]⇒ (aba)b
⇒ abb

Reduce RHS:

[2](aba)a
[2]⇒ (aba)
⇒ ab

Defines rule #1.