Certificate for #3256 ⟨a, b | ababbababba=1⟩

Completion settings:

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

Axiom: ababbababba=1.

Referenced by [3].

Axiom: babba=c.

Referenced by [3], [4], [5], [6].

Overlap of [1] ababbababba=1 with [2] babba=c:

Critical pair: acbabba=1.

Reduce LHS:

Defines rule #2.

Referenced by [4], [7], [8], [11], [12], [15], [16], [17], [18], [19], [20], [22], [23], [24], [25], [26].

Overlap of [2] babba=c with [3] acc=1:

Critical pair: babb=ccc.

Referenced by [5], [6], [12], [13].

Overlap of [2] babba=c with [4] babb=ccc:

Critical pair: ccca=c.

Referenced by [7], [9].

Overlap of [2] babba=c with [4] babb=ccc:

Critical pair: babccc=cbb.

Flip LHS and RHS.

Defines rule #4.

Referenced by [8], [14], [25].

Overlap of [3] acc=1 with [5] ccca=c:

Critical pair: ac=ca.

Flip LHS and RHS.

Defines rule #1.

Referenced by [10], [16], [17], [18], [20], [21], [22], [24], [25], [26].

Overlap of [3] acc=1 with [6] cbb=babccc:

Critical pair: acbabccc=bb.

Referenced by [9].

Overlap of [8] acbabccc=bb with [5] ccca=c:

Critical pair: acbabc=bba.

Referenced by [10].

Overlap of [9] acbabc=bba with [7] ca=ac:

Critical pair: acbabac=bbaa.

Referenced by [11].

Overlap of [10] acbabac=bbaa with [3] acc=1:

Critical pair: acbab=bbaac.

Defines rule #6.

Referenced by [12], [16], [24].

Overlap of [11] acbab=bbaac with [4] babb=ccc:

Critical pair: acccc=bbaacb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #7.

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

Overlap of [4] babb=ccc with [12] bbaacb=cc:

Critical pair: babcc=cccbaacb.

Flip LHS and RHS.

Referenced by [15].

Overlap of [12] bbaacb=cc with [6] cbb=babccc:

Critical pair: bbaababccc=ccb.

Referenced by [20].

Overlap of [3] acc=1 with [13] cccbaacb=babcc:

Critical pair: ababcc=cbaacb.

Flip LHS and RHS.

Defines rule #5.

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

Overlap of [3] acc=1 with [15] cbaacb=ababcc:

Critical pair: acababcc=baacb.

Reduce LHS:

Referenced by [19].

Overlap of [12] bbaacb=cc with [15] cbaacb=ababcc:

Critical pair: bbaaababcc=ccaacb.

Reduce RHS:

Referenced by [22].

Overlap of [15] cbaacb=ababcc with [15] cbaacb=ababcc:

Critical pair: cbaaababcc=ababccaacb.

Reduce RHS:

Referenced by [26].

Overlap of [16] abbac=baacb with [3] acc=1:

Critical pair: abb=baacbc.

Defines rule #3.

Overlap of [14] bbaababccc=ccb with [7] ca=ac:

Critical pair: bbaababccac=ccba.

Reduce LHS:

Referenced by [21].

Overlap of [20] bbaababc=ccba with [7] ca=ac:

Critical pair: bbaababac=ccbaa.

Referenced by [23], [24].

Overlap of [17] bbaaababcc=acb with [7] ca=ac:

Critical pair: bbaaababcac=acba.

Reduce LHS:

Defines rule #11.

Overlap of [21] bbaababac=ccbaa with [3] acc=1:

Critical pair: bbaabab=ccbaac.

Defines rule #10.

Referenced by [24].

Overlap of [21] bbaababac=ccbaa with [11] acbab=bbaac:

Critical pair: bbaababbbaac=ccbaabab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [25].

Overlap of [3] acc=1 with [24] ccbaabab=bbacbaac:

Critical pair: acbbacbaac=cbaabab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #8.

Overlap of [18] cbaaababcc=ababacb with [7] ca=ac:

Critical pair: cbaaababcac=ababacba.

Reduce LHS:

Defines rule #9.