Certificate for #6539 ⟨a, b | aaa=a, aabb=ba⟩

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

Completion settings:

[1] aaa=a

Axiom: aaa=a.

Defines rule #1.

Referenced by [3], [4], [6].

[2] aabb=ba

Axiom: aabb=ba.

Referenced by [3], [4], [5], [6].

[3] abb=aba

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

a aa aabb

Critical pair: aba=abb.

Flip LHS and RHS.

Defines rule #2.

[4] aaba=ba

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

aa a aabb

Critical pair: aaba=aabb.

Reduce RHS:

[2](aabb)
⇒ ba

Defines rule #4.

Referenced by [5].

[5] bba=baa

Overlap of [4] aaba=ba with [2] aabb=ba:

aab a aabb

Critical pair: aabba=baabb.

Reduce LHS:

[2](aabb)a
⇒ baa

Reduce RHS:

[2]b(aabb)
⇒ bba

Flip LHS and RHS.

Defines rule #3.

Referenced by [6].

[6] baba=ba

Overlap of [2] aabb=ba with [5] bba=baa:

aab b bba

Critical pair: aabbaa=baba.

Reduce LHS:

[2](aabb)aa
[1]⇒ b(aaa)
⇒ ba

Flip LHS and RHS.

Defines rule #5.