Certificate for #4854 ⟨a, b, c | ab=a, baccb=1⟩

Back:⟨a, b, c | ab=a, baccb=1⟩

Completion settings:

[1] ab=a

Axiom: ab=a.

Defines rule #1.

Referenced by [3].

[2] baccb=1

Axiom: baccb=1.

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

[3] aaccb=a

Overlap of [1] ab=a with [2] baccb=1:

a b baccb

Critical pair: a=aaccb.

Flip LHS and RHS.

Referenced by [5].

[4] bacc=accb

Overlap of [2] baccb=1 with [2] baccb=1:

bacc b baccb

Critical pair: bacc=accb.

Defines rule #3.

Referenced by [6].

[5] aacc=a

Overlap of [3] aaccb=a with [2] baccb=1:

aacc b baccb

Critical pair: aacc=aaccb.

Reduce RHS:

[3](aaccb)
⇒ a

Defines rule #2.

[6] accbb=1

Overlap of [2] baccb=1 with [4] bacc=accb:

baccb bacc

Critical pair: accbb=1.

Defines rule #4.