Certificate for #1882 ⟨a, b, c | aba=bc, ccb=1⟩

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

Completion settings:

[1] aba=bc

Axiom: aba=bc.

Defines rule #4.

Referenced by [3].

[2] ccb=1

Axiom: ccb=1.

Defines rule #1.

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

[3] abbc=bcba

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

ab a aba

Critical pair: abbc=bcba.

Referenced by [4], [5].

[4] abb=bcbacb

Overlap of [3] abbc=bcba with [2] ccb=1:

abb c ccb

Critical pair: abb=bcbacb.

Defines rule #2.

Referenced by [5].

[5] bcbacbc=bcba

Overlap of [3] abbc=bcba with [4] abb=bcbacb:

abbc abb

Critical pair: bcbacbc=bcba.

Referenced by [6].

[6] cbacbc=cba

Overlap of [2] ccb=1 with [5] bcbacbc=bcba:

cc b bcbacbc

Critical pair: ccbcba=cbacbc.

Reduce LHS:

[2](ccb)cba
⇒ cba

Flip LHS and RHS.

Referenced by [7].

[7] acbc=a

Overlap of [2] ccb=1 with [6] cbacbc=cba:

c cb cbacbc

Critical pair: ccba=acbc.

Reduce LHS:

[2](ccb)a
⇒ a

Flip LHS and RHS.

Defines rule #3.