Certificate for #7607 ⟨a, b, c | ab=1, cbcc=ba⟩

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

Completion settings:

[1] ab=1

Axiom: ab=1.

Defines rule #1.

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

[2] cbcc=ba

Axiom: cbcc=ba.

Defines rule #5.

Referenced by [3], [4], [9].

[3] cbcba=bcc

Overlap of [2] cbcc=ba with [2] cbcc=ba:

cbc c cbcc

Critical pair: cbcba=babcc.

Reduce RHS:

[1]b(ab)cc
⇒ bcc

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

[4] cbba=bcba

Overlap of [2] cbcc=ba with [3] cbcba=bcc:

cbc c cbcba

Critical pair: cbcbcc=babcba.

Reduce LHS:

[2]cb(cbcc)
⇒ cbba

Reduce RHS:

[1]b(ab)cba
⇒ bcba

Referenced by [6].

[5] cbcb=bccb

Overlap of [3] cbcba=bcc with [1] ab=1:

cbcb a ab

Critical pair: cbcb=bccb.

Defines rule #4.

Referenced by [7].

[6] cbb=bcb

Overlap of [4] cbba=bcba with [1] ab=1:

cbb a ab

Critical pair: cbb=bcbab.

Reduce RHS:

[1]bcb(ab)
⇒ bcb

Defines rule #2.

[7] bccba=bcc

Overlap of [3] cbcba=bcc with [5] cbcb=bccb:

cbcba cbcb

Critical pair: bccba=bcc.

Referenced by [8].

[8] ccba=cc

Overlap of [1] ab=1 with [7] bccba=bcc:

a b bccba

Critical pair: abcc=ccba.

Reduce LHS:

[1](ab)cc
⇒ cc

Flip LHS and RHS.

Defines rule #6.

Referenced by [9].

[9] bacba=bac

Overlap of [2] cbcc=ba with [8] ccba=cc:

cbc c ccba

Critical pair: cbccc=bacba.

Reduce LHS:

[2](cbcc)c
⇒ bac

Flip LHS and RHS.

Referenced by [10].

[10] acba=ac

Overlap of [1] ab=1 with [9] bacba=bac:

a b bacba

Critical pair: abac=acba.

Reduce LHS:

[1](ab)ac
⇒ ac

Flip LHS and RHS.

Defines rule #3.