Certificate for #486 ⟨a, b | aabb=1, baba=1⟩

Back:⟨a, b | aabb=1, baba=1⟩

Completion settings:

[1] aabb=1

Axiom: aabb=1.

Defines rule #2.

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

[2] baba=1

Axiom: baba=1.

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

[3] aba=aab

Overlap of [1] aabb=1 with [2] baba=1:

aab b baba

Critical pair: aab=aba.

Flip LHS and RHS.

Referenced by [6].

[4] bab=abb

Overlap of [2] baba=1 with [1] aabb=1:

bab a aabb

Critical pair: bab=abb.

Referenced by [5].

[5] abba=1

Overlap of [2] baba=1 with [4] bab=abb:

baba bab

Critical pair: abba=1.

Referenced by [6].

[6] ba=ab

Overlap of [3] aba=aab with [5] abba=1:

ab a abba

Critical pair: ab=aabbba.

Reduce RHS:

[1](aabb)ba
⇒ ba

Flip LHS and RHS.

Defines rule #1.