Certificate for #10016 ⟨a, b | aa=1, abbabb=bb⟩

Completion settings:

• Auxiliary generators:
  1. c = bab
• Reduction order:
  • Left-to-right recursive path with deg(b) = deg(c) = 0, b < c; deg(a) = 1

Axiom: aa=1.

Defines rule #15.

Referenced by [6], [16].

Axiom: abbabb=bb.

Referenced by [4].

Axiom: bab=c.

Defines rule #13.

Referenced by [4], [5], [7], [8], [11], [12], [14].

Overlap of [2] abbabb=bb with [3] bab=c:

Critical pair: abcb=bb.

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

Overlap of [3] bab=c with [3] bab=c:

Critical pair: bac=cab.

Flip LHS and RHS.

Defines rule #14.

Overlap of [1] aa=1 with [4] abcb=bb:

Critical pair: abb=bcb.

Defines rule #9.

Referenced by [11], [12], [13], [15].

Overlap of [3] bab=c with [4] abcb=bb:

Critical pair: bbb=ccb.

Flip LHS and RHS.

Defines rule #1.

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

Overlap of [7] ccb=bbb with [3] bab=c:

Critical pair: ccc=bbbab.

Reduce RHS:

Defines rule #2.

Referenced by [9], [10], [16].

Overlap of [8] ccc=bbc with [7] ccb=bbb:

Critical pair: cbbb=bbcb.

Referenced by [18].

Overlap of [8] ccc=bbc with [8] ccc=bbc:

Critical pair: cbbc=bbcc.

Referenced by [19].

Overlap of [3] bab=c with [6] abb=bcb:

Critical pair: bbcb=cb.

Defines rule #5.

Referenced by [13], [14], [18].

Overlap of [6] abb=bcb with [3] bab=c:

Critical pair: abc=bcbab.

Reduce RHS:

Defines rule #10.

Referenced by [16], [17].

Overlap of [6] abb=bcb with [11] bbcb=cb:

Critical pair: acb=bcbcb.

Defines rule #11.

Overlap of [11] bbcb=cb with [3] bab=c:

Critical pair: bbcc=cbab.

Reduce RHS:

Defines rule #6.

Referenced by [15], [19].

Overlap of [6] abb=bcb with [14] bbcc=cc:

Critical pair: acc=bcbcc.

Defines rule #12.

Overlap of [1] aa=1 with [12] abc=bcc:

Critical pair: abcc=bc.

Reduce LHS:

Defines rule #4.

Overlap of [4] abcb=bb with [12] abc=bcc:

Critical pair: bccb=bb.

Reduce LHS:

Defines rule #3.

Simplify [9] cbbb=bbcb.

Reduce RHS:

Defines rule #7.

Simplify [10] cbbc=bbcc.

Reduce RHS:

Defines rule #8.