Certificate for #3020 ⟨a, b | aa=a, abba=ab⟩

Back:⟨a, b | aa=a, abba=ab⟩

Completion settings:

[1] aa=a

Axiom: aa=a.

Defines rule #1.

Referenced by [3].

[2] abba=ab

Axiom: abba=ab.

Referenced by [3], [4].

[3] aba=ab

Overlap of [2] abba=ab with [1] aa=a:

abb a aa

Critical pair: abba=aba.

Reduce LHS:

[2](abba)
⇒ ab

Flip LHS and RHS.

Defines rule #2.

Referenced by [4].

[4] abb=ab

Overlap of [2] abba=ab with [3] aba=ab:

abb a aba

Critical pair: abbab=abba.

Reduce LHS:

[2](abba)b
⇒ abb

Reduce RHS:

[2](abba)
⇒ ab

Defines rule #3.