Certificate for #1868 ⟨a, b, c | aba=bc, bac=1⟩

Back:⟨a, b, c | aba=bc, bac=1⟩

Completion settings:

[1] aba=bc

Axiom: aba=bc.

Referenced by [3], [4].

[2] bac=1

Axiom: bac=1.

Referenced by [4], [6].

[3] bcba=abbc

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

ab a aba

Critical pair: abbc=bcba.

Flip LHS and RHS.

Referenced by [5].

[4] a=bcc

Overlap of [1] aba=bc with [2] bac=1:

a ba bac

Critical pair: a=bcc.

Defines rule #3.

Referenced by [5], [6].

[5] bccbbc=bcbbcc

Simplify [3] bcba=abbc.

Reduce LHS:

[4]bcb(a)
⇒ bcbbcc

Reduce RHS:

[4](a)bbc
⇒ bccbbc

Flip LHS and RHS.

Defines rule #2.

[6] bbccc=1

Overlap of [2] bac=1 with [4] a=bcc:

b ac a

Critical pair: bbccc=1.

Defines rule #1.