Certificate for #5893 ⟨a, b, c | ab=a, bcb=bc⟩

Back:⟨a, b, c | ab=a, bcb=bc⟩

Completion settings:

[1] ab=a

Axiom: ab=a.

Defines rule #1.

Referenced by [5].

[2] bcb=bc

Axiom: bcb=bc.

Referenced by [4].

[3] cb=d

Axiom: cb=d.

Defines rule #5.

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

[4] bc=bd

Overlap of [2] bcb=bc with [3] cb=d:

b cb cb

Critical pair: bd=bc.

Flip LHS and RHS.

Defines rule #3.

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

[5] ac=ad

Overlap of [1] ab=a with [4] bc=bd:

a b bc

Critical pair: abd=ac.

Reduce LHS:

[1](ab)d
⇒ ad

Flip LHS and RHS.

Defines rule #2.

Referenced by [8].

[6] dc=dd

Overlap of [3] cb=d with [4] bc=bd:

c b bc

Critical pair: cbd=dc.

Reduce LHS:

[3](cb)d
⇒ dd

Flip LHS and RHS.

Defines rule #4.

Referenced by [9].

[7] bdb=bd

Overlap of [4] bc=bd with [3] cb=d:

b c cb

Critical pair: bd=bdb.

Flip LHS and RHS.

Defines rule #7.

[8] adb=ad

Overlap of [5] ac=ad with [3] cb=d:

a c cb

Critical pair: ad=adb.

Flip LHS and RHS.

Defines rule #6.

[9] ddb=dd

Overlap of [6] dc=dd with [3] cb=d:

d c cb

Critical pair: dd=ddb.

Flip LHS and RHS.

Defines rule #8.