Certificate for #19256 ⟨a, b | aaa=a, aabba=ba⟩

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

Completion settings:

[1] aaa=a

Axiom: aaa=a.

Defines rule #1.

Referenced by [3].

[2] aabba=ba

Axiom: aabba=ba.

Referenced by [3], [4].

[3] aaba=ba

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

aa a aabba

Critical pair: aaba=aabba.

Reduce RHS:

[2](aabba)
⇒ ba

Defines rule #3.

Referenced by [4].

[4] bba=ba

Overlap of [3] aaba=ba with [2] aabba=ba:

aab a aabba

Critical pair: aabba=baabba.

Reduce LHS:

[2](aabba)
⇒ ba

Reduce RHS:

[2]b(aabba)
⇒ bba

Flip LHS and RHS.

Defines rule #2.