Certificate for #7848 ⟨a, b, c | ab=1, cba=bcc⟩

Completion settings:

[1] ab=1

Axiom: ab=1.

Defines rule #1.

Referenced by [3], [4].

[2] bcc=cba

Axiom: cba=bcc.

Flip LHS and RHS.

Defines rule #4.

Referenced by [3], [6], [7].

[3] acba=cc

Overlap of [1] ab=1 with [2] bcc=cba:

a b bcc

Critical pair: acba=cc.

Referenced by [4], [5].

[4] acb=ccb

Overlap of [3] acba=cc with [1] ab=1:

acb a ab

Critical pair: acb=ccb.

Defines rule #3.

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

[5] ccba=cc

Overlap of [3] acba=cc with [4] acb=ccb:

acba acb

Critical pair: ccba=cc.

Defines rule #5.

Referenced by [6], [7].

[6] acc=ccc

Overlap of [4] acb=ccb with [2] bcc=cba:

ac b bcc

Critical pair: accba=ccbcc.

Reduce LHS:

[5]a(ccba)
⇒ acc

Reduce RHS:

[2]cc(bcc)
[5]⇒ c(ccba)
⇒ ccc

Defines rule #2.

[7] cbac=cc

Overlap of [2] bcc=cba with [5] ccba=cc:

bc c ccba

Critical pair: bccc=cbacba.

Reduce LHS:

[2](bcc)c
⇒ cbac

Reduce RHS:

[4]cb(acb)a
[2]⇒ c(bcc)ba
[5]⇒ (ccba)ba
[5]⇒ (ccba)
⇒ cc

Defines rule #6.