Certificate for #485 ⟨a, b | aabb=1, abba=1⟩

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

Completion settings:

[1] aabb=1

Axiom: aabb=1.

Referenced by [4].

[2] abba=1

Axiom: abba=1.

Referenced by [5].

[3] bb=c

Axiom: bb=c.

Defines rule #3.

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

[4] aac=1

Overlap of [1] aabb=1 with [3] bb=c:

aa bb bb

Critical pair: aac=1.

Referenced by [8].

[5] aca=1

Overlap of [2] abba=1 with [3] bb=c:

a bba bb

Critical pair: aca=1.

Referenced by [7], [11].

[6] bc=cb

Overlap of [3] bb=c with [3] bb=c:

b b bb

Critical pair: bc=cb.

Defines rule #2.

Referenced by [9].

[7] ac=ca

Overlap of [5] aca=1 with [5] aca=1:

ac a aca

Critical pair: ac=ca.

Defines rule #1.

Referenced by [8], [10].

[8] caa=1

Simplify [4] aac=1.

Reduce LHS:

[7]a(ac)
[7]⇒ (ac)a
⇒ caa

Defines rule #4.

Referenced by [9].

[9] cbaa=b

Overlap of [6] bc=cb with [8] caa=1:

b c caa

Critical pair: b=cbaa.

Flip LHS and RHS.

Referenced by [10].

[10] cabaa=ab

Overlap of [7] ac=ca with [9] cbaa=b:

a c cbaa

Critical pair: ab=cabaa.

Flip LHS and RHS.

Referenced by [11].

[11] baa=aab

Overlap of [5] aca=1 with [10] cabaa=ab:

a ca cabaa

Critical pair: aab=baa.

Flip LHS and RHS.

Defines rule #5.