Certificate for #2084 ⟨a, b, c | aaab=1, bccc=1⟩

Back:⟨a, b, c | aaab=1, bccc=1⟩

Completion settings:

[1] aaab=1

Axiom: aaab=1.

Referenced by [3], [7], [8], [12].

[2] bccc=1

Axiom: bccc=1.

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

[3] ccc=aaa

Overlap of [1] aaab=1 with [2] bccc=1:

aaa b bccc

Critical pair: aaa=ccc.

Flip LHS and RHS.

Defines rule #3.

Referenced by [4], [5].

[4] bcaaa=c

Overlap of [2] bccc=1 with [3] ccc=aaa:

bc cc ccc

Critical pair: bcaaa=c.

Referenced by [6].

[5] caaa=aaac

Overlap of [3] ccc=aaa with [3] ccc=aaa:

c cc ccc

Critical pair: caaa=aaac.

Defines rule #5.

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

[6] baaac=c

Simplify [4] bcaaa=c.

Reduce LHS:

[5]b(caaa)
⇒ baaac

Referenced by [9], [10].

[7] aaacb=c

Overlap of [5] caaa=aaac with [1] aaab=1:

c aaa aaab

Critical pair: c=aaacb.

Flip LHS and RHS.

Referenced by [9].

[8] aaacab=ca

Overlap of [5] caaa=aaac with [1] aaab=1:

ca aa aaab

Critical pair: ca=aaacab.

Flip LHS and RHS.

Referenced by [10].

[9] cb=bc

Overlap of [6] baaac=c with [7] aaacb=c:

b aaac aaacb

Critical pair: bc=cb.

Flip LHS and RHS.

Defines rule #2.

Referenced by [11].

[10] cab=bca

Overlap of [6] baaac=c with [8] aaacab=ca:

b aaac aaacab

Critical pair: bca=cab.

Flip LHS and RHS.

Referenced by [11].

[11] ab=ba

Overlap of [2] bccc=1 with [10] cab=bca:

bcc c cab

Critical pair: bccbca=ab.

Reduce LHS:

[9]bc(cb)ca
[9]⇒ b(cb)cca
[2]⇒ b(bccc)a
⇒ ba

Flip LHS and RHS.

Defines rule #1.

Referenced by [12].

[12] baaa=1

Overlap of [1] aaab=1 with [11] ab=ba:

aa ab ab

Critical pair: aaba=1.

Reduce LHS:

[11]a(ab)a
[11]⇒ (ab)aa
⇒ baaa

Defines rule #4.