Certificate for #489 ⟨a, b, c | bb=ac, aab=1⟩

Back:⟨a, b, c | bb=ac, aab=1⟩

Completion settings:

[1] bb=ac

Axiom: bb=ac.

Referenced by [3], [4].

[2] aab=1

Axiom: aab=1.

Referenced by [4], [6].

[3] bac=acb

Overlap of [1] bb=ac with [1] bb=ac:

b b bb

Critical pair: bac=acb.

Referenced by [5].

[4] b=aaac

Overlap of [2] aab=1 with [1] bb=ac:

aa b bb

Critical pair: aaac=b.

Flip LHS and RHS.

Defines rule #3.

Referenced by [5], [6].

[5] acaaac=aaacac

Simplify [3] bac=acb.

Reduce LHS:

[4](b)ac
⇒ aaacac

Reduce RHS:

[4]ac(b)
⇒ acaaac

Flip LHS and RHS.

Defines rule #1.

[6] aaaaac=1

Overlap of [2] aab=1 with [4] b=aaac:

aa b b

Critical pair: aaaaac=1.

Defines rule #2.