Certificate for #556 ⟨a, b | aba=b, aabb=1⟩

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

Completion settings:

[1] aba=b

Axiom: aba=b.

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

[2] aabb=1

Axiom: aabb=1.

Referenced by [4].

[3] abb=bba

Overlap of [1] aba=b with [1] aba=b:

ab a aba

Critical pair: abb=bba.

Referenced by [4], [6].

[4] bbaa=1

Simplify [2] aabb=1.

Reduce LHS:

[3]a(abb)
[3]⇒ (abb)a
⇒ bbaa

Referenced by [5], [6], [7], [8].

[5] bbab=ba

Overlap of [4] bbaa=1 with [1] aba=b:

bba a aba

Critical pair: bbab=ba.

Referenced by [6].

[6] ab=baaa

Overlap of [3] abb=bba with [4] bbaa=1:

ab b bbaa

Critical pair: ab=bbabaa.

Reduce RHS:

[5](bbab)aa
⇒ baaa

Defines rule #2.

Referenced by [7].

[7] bb=aa

Overlap of [1] aba=b with [6] ab=baaa:

ab a ab

Critical pair: abbaaa=bb.

Reduce LHS:

[4]a(bbaa)a
⇒ aa

Flip LHS and RHS.

Defines rule #3.

Referenced by [8].

[8] aaaa=1

Overlap of [4] bbaa=1 with [7] bb=aa:

bbaa bb

Critical pair: aaaa=1.

Defines rule #1.