Certificate for #7549 ⟨a, b, c | ab=1, bcac=cc⟩

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

Completion settings:

[1] ab=1

Axiom: ab=1.

Defines rule #2.

Referenced by [5].

[2] bcac=cc

Axiom: bcac=cc.

Referenced by [4].

[3] cac=d

Axiom: cac=d.

Defines rule #5.

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

[4] bd=cc

Overlap of [2] bcac=cc with [3] cac=d:

b cac cac

Critical pair: bd=cc.

Defines rule #3.

Referenced by [5].

[5] acc=d

Overlap of [1] ab=1 with [4] bd=cc:

a b bd

Critical pair: acc=d.

Defines rule #8.

Referenced by [7], [8].

[6] cad=dac

Overlap of [3] cac=d with [3] cac=d:

ca c cac

Critical pair: cad=dac.

Defines rule #4.

[7] cd=dc

Overlap of [3] cac=d with [5] acc=d:

c ac acc

Critical pair: cd=dc.

Defines rule #1.

Referenced by [8].

[8] adc=dac

Overlap of [5] acc=d with [3] cac=d:

ac c cac

Critical pair: acd=dac.

Reduce LHS:

[7]a(cd)
⇒ adc

Defines rule #7.

Referenced by [9].

[9] add=dad

Overlap of [8] adc=dac with [3] cac=d:

ad c cac

Critical pair: add=dacac.

Reduce RHS:

[3]da(cac)
⇒ dad

Defines rule #6.