Certificate for #6186 ⟨a, b, c | aa=1, abccab=1⟩

Back:⟨a, b, c | aa=1, abccab=1⟩

Completion settings:

[1] aa=1

Axiom: aa=1.

Defines rule #1.

Referenced by [6].

[2] abccab=1

Axiom: abccab=1.

Referenced by [4].

[3] cc=d

Axiom: cc=d.

Defines rule #6.

Referenced by [4], [5].

[4] abdab=1

Overlap of [2] abccab=1 with [3] cc=d:

ab ccab cc

Critical pair: abdab=1.

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

[5] dc=cd

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

c c cc

Critical pair: cd=dc.

Flip LHS and RHS.

Defines rule #4.

Referenced by [9].

[6] bdab=a

Overlap of [1] aa=1 with [4] abdab=1:

a a abdab

Critical pair: a=bdab.

Flip LHS and RHS.

Referenced by [8].

[7] dab=abd

Overlap of [4] abdab=1 with [4] abdab=1:

abd ab abdab

Critical pair: abd=dab.

Flip LHS and RHS.

Defines rule #2.

Referenced by [8], [10].

[8] babd=a

Simplify [6] bdab=a.

Reduce LHS:

[7]b(dab)
⇒ babd

Defines rule #3.

Referenced by [9].

[9] babcd=ac

Overlap of [8] babd=a with [5] dc=cd:

bab d dc

Critical pair: babcd=ac.

Referenced by [10].

[10] babcabd=acab

Overlap of [9] babcd=ac with [7] dab=abd:

babc d dab

Critical pair: babcabd=acab.

Referenced by [11].

[11] babc=acabab

Overlap of [10] babcabd=acab with [4] abdab=1:

babc abd abdab

Critical pair: babc=acabab.

Defines rule #5.