Certificate for #5393 ⟨a, b, c | ab=a, bcbc=b⟩

Back:⟨a, b, c | ab=a, bcbc=b⟩

Completion settings:

[1] ab=a

Axiom: ab=a.

Defines rule #1.

Referenced by [3], [5].

[2] bcbc=b

Axiom: bcbc=b.

Referenced by [3], [4], [5], [7].

[3] acbc=a

Overlap of [1] ab=a with [2] bcbc=b:

a b bcbc

Critical pair: ab=acbc.

Reduce LHS:

[1](ab)
⇒ a

Flip LHS and RHS.

Referenced by [5], [6].

[4] bcb=bbc

Overlap of [2] bcbc=b with [2] bcbc=b:

bc bc bcbc

Critical pair: bcb=bbc.

Defines rule #4.

Referenced by [7].

[5] acb=ac

Overlap of [3] acbc=a with [2] bcbc=b:

ac bc bcbc

Critical pair: acb=abc.

Reduce RHS:

[1](ab)c
⇒ ac

Defines rule #2.

Referenced by [6].

[6] acc=a

Overlap of [3] acbc=a with [5] acb=ac:

acbc acb

Critical pair: acc=a.

Defines rule #3.

[7] bbcc=b

Overlap of [2] bcbc=b with [4] bcb=bbc:

bcbc bcb

Critical pair: bbcc=b.

Defines rule #5.