Certificate for #544 ⟨a, b, c | ba=ac, cb=b⟩

Completion settings:

[1] ac=ba

Axiom: ba=ac.

Flip LHS and RHS.

Defines rule #4.

Referenced by [4].

[2] cb=b

Axiom: cb=b.

Defines rule #5.

Referenced by [4], [5].

[3] ab=d

Axiom: ab=d.

Defines rule #2.

Referenced by [4], [6].

[4] bd=d

Overlap of [1] ac=ba with [2] cb=b:

a c cb

Critical pair: ab=bab.

Reduce LHS:

[3](ab)
⇒ d

Reduce RHS:

[3]b(ab)
⇒ bd

Flip LHS and RHS.

Defines rule #1.

Referenced by [5], [6].

[5] cd=d

Overlap of [2] cb=b with [4] bd=d:

c b bd

Critical pair: cd=bd.

Reduce RHS:

[4](bd)
⇒ d

Defines rule #6.

[6] ad=dd

Overlap of [3] ab=d with [4] bd=d:

a b bd

Critical pair: ad=dd.

Defines rule #3.