Certificate for #49 ⟨a, b, c | bb=ac, bc=1⟩

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

Completion settings:

[1] bb=ac

Axiom: bb=ac.

Referenced by [3], [4].

[2] bc=1

Axiom: bc=1.

Referenced by [4], [5].

[3] acb=bac

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

b b bb

Critical pair: bac=acb.

Flip LHS and RHS.

Referenced by [6].

[4] b=acc

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

b b bc

Critical pair: b=acc.

Defines rule #3.

Referenced by [5], [6].

[5] accc=1

Overlap of [2] bc=1 with [4] b=acc:

bc b

Critical pair: accc=1.

Defines rule #1.

[6] accac=acacc

Simplify [3] acb=bac.

Reduce LHS:

[4]ac(b)
⇒ acacc

Reduce RHS:

[4](b)ac
⇒ accac

Flip LHS and RHS.

Defines rule #2.