Certificate for #1593 ⟨a, b, c | aaa=bc, cbb=1⟩

Completion settings:

• Reduction order:
  • Left-to-right shortlex with a < b < c

Axiom: aaa=bc.

Defines rule #1.

Referenced by [3], [10], [12], [13].

Axiom: cbb=1.

Defines rule #3.

Referenced by [4], [5], [10], [11], [12], [13].

Overlap of [1] aaa=bc with [1] aaa=bc:

Critical pair: abc=bca.

Flip LHS and RHS.

Defines rule #2.

Referenced by [4], [6], [9], [13].

Overlap of [2] cbb=1 with [3] bca=abc:

Critical pair: cbabc=ca.

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

Overlap of [4] cbabc=ca with [2] cbb=1:

Critical pair: cbab=cabb.

Defines rule #4.

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

Overlap of [4] cbabc=ca with [3] bca=abc:

Critical pair: cbaabc=caa.

Referenced by [11].

Overlap of [4] cbabc=ca with [5] cbab=cabb:

Critical pair: cabbc=ca.

Defines rule #6.

Referenced by [8], [9], [12].

Overlap of [4] cbabc=ca with [5] cbab=cabb:

Critical pair: cbabcabb=cabab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #5.

Referenced by [9].

Overlap of [7] cabbc=ca with [3] bca=abc:

Critical pair: cababc=caa.

Reduce LHS:

Defines rule #9.

Referenced by [10], [13].

Overlap of [9] caabbc=caa with [5] cbab=cabb:

Critical pair: caabbcabb=caabab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #8.

Overlap of [6] cbaabc=caa with [2] cbb=1:

Critical pair: cbaab=caabb.

Defines rule #7.

Referenced by [12], [13].

Overlap of [7] cabbc=ca with [11] cbaab=caabb:

Critical pair: cabbcaabb=cabaab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #10.

Overlap of [9] caabbc=caa with [11] cbaab=caabb:

Critical pair: caabbcaabb=caabaab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #11.