Certificate for #27144 ⟨a, b | aa=1, abbabba=bb⟩

Completion settings:

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

Axiom: aa=1.

Defines rule #15.

Referenced by [6], [7], [9], [15], [16], [23].

Axiom: abbabba=bb.

Referenced by [4].

Axiom: bab=c.

Defines rule #6.

Referenced by [4], [5], [8], [10], [11], [13], [14], [17], [24], [25].

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

Critical pair: abcba=bb.

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

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

Critical pair: bac=cab.

Defines rule #14.

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

Critical pair: abb=bcba.

Flip LHS and RHS.

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

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

Critical pair: abcb=bba.

Referenced by [11], [15], [19].

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

Critical pair: abcc=bbb.

Referenced by [20].

Overlap of [6] bcba=abb with [1] aa=1:

Critical pair: bcb=abba.

Flip LHS and RHS.

Referenced by [13], [14].

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

Critical pair: bcc=abbb.

Referenced by [12].

Overlap of [3] bab=c with [7] abcb=bba:

Critical pair: bbba=ccb.

Flip LHS and RHS.

Referenced by [12], [16].

Overlap of [10] bcc=abbb with [11] ccb=bbba:

Critical pair: bcbbba=abbbcb.

Flip LHS and RHS.

Referenced by [15], [21].

Overlap of [3] bab=c with [9] abba=bcb:

Critical pair: bbcb=cba.

Flip LHS and RHS.

Defines rule #10.

Referenced by [15], [16], [17], [18].

Overlap of [9] abba=bcb with [3] bab=c:

Critical pair: abc=bcbb.

Defines rule #13.

Referenced by [19], [20], [23].

Overlap of [7] abcb=bba with [13] cba=bbcb:

Critical pair: abbbcb=bbaa.

Reduce LHS:

Reduce RHS:

Referenced by [21].

Overlap of [11] ccb=bbba with [13] cba=bbcb:

Critical pair: cbbcb=bbbaa.

Reduce RHS:

Referenced by [29].

Overlap of [13] cba=bbcb with [3] bab=c:

Critical pair: cc=bbcbb.

Defines rule #8.

Overlap of [6] bcba=abb with [13] cba=bbcb:

Critical pair: bbbcb=abb.

Flip LHS and RHS.

Defines rule #5.

Referenced by [22], [25], [26].

Overlap of [7] abcb=bba with [14] abc=bcbb:

Critical pair: bcbbb=bba.

Flip LHS and RHS.

Defines rule #7.

Referenced by [28].

Overlap of [8] abcc=bbb with [14] abc=bcbb:

Critical pair: bcbbc=bbb.

Referenced by [22].

Simplify [12] abbbcb=bcbbba.

Reduce RHS:

Referenced by [22].

Overlap of [21] abbbcb=bb with [18] abb=bbbcb:

Critical pair: bbbcbbcb=bb.

Reduce LHS:

Defines rule #1.

Referenced by [24], [29].

Overlap of [1] aa=1 with [14] abc=bcbb:

Critical pair: abcbb=bc.

Reduce LHS:

Defines rule #3.

Referenced by [27], [28], [29].

Overlap of [3] bab=c with [22] bbbbbb=bb:

Critical pair: babb=cbbbbb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #2.

Overlap of [3] bab=c with [18] abb=bbbcb:

Critical pair: bbbbcb=cb.

Referenced by [26], [27].

Overlap of [18] abb=bbbcb with [25] bbbbcb=cb:

Critical pair: acb=bbbcbbbcb.

Defines rule #12.

Overlap of [25] bbbbcb=cb with [23] bcbbbb=bc:

Critical pair: bbbbc=cbbbb.

Defines rule #4.

Overlap of [23] bcbbbb=bc with [19] bba=bcbbb:

Critical pair: bcbbbcbbb=bca.

Flip LHS and RHS.

Defines rule #11.

Overlap of [16] cbbcb=bbb with [23] bcbbbb=bc:

Critical pair: cbbc=bbbbbb.

Reduce RHS:

Defines rule #9.