Certificate for #6739 ⟨a, b | aba=a, aabb=ba⟩

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

Completion settings:

[1] aba=a

Axiom: aba=a.

Defines rule #3.

Referenced by [3], [4].

[2] aabb=ba

Axiom: aabb=ba.

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

[3] abba=ba

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

ab a aabb

Critical pair: abba=aabb.

Reduce RHS:

[2](aabb)
⇒ ba

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

[4] baa=a

Overlap of [2] aabb=ba with [3] abba=ba:

a abb abba

Critical pair: aba=baa.

Reduce LHS:

[1](aba)
⇒ a

Flip LHS and RHS.

Defines rule #1.

Referenced by [5].

[5] abbba=abb

Overlap of [3] abba=ba with [2] aabb=ba:

abb a aabb

Critical pair: abbba=baabb.

Reduce RHS:

[4](baa)bb
⇒ abb

Referenced by [6].

[6] abb=bba

Overlap of [3] abba=ba with [3] abba=ba:

abb a abba

Critical pair: abbba=babba.

Reduce LHS:

[5](abbba)
⇒ abb

Reduce RHS:

[3]b(abba)
⇒ bba

Defines rule #2.