Certificate for #3772 ⟨a, b | abababbaab=a⟩

Completion settings:

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

Axiom: abababbaab=a.

Referenced by [3].

Axiom: abba=c.

Defines rule #15.

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

Overlap of [1] abababbaab=a with [2] abba=c:

Critical pair: ababcab=a.

Referenced by [5], [6], [7], [9], [10], [12], [14].

Overlap of [2] abba=c with [2] abba=c:

Critical pair: abbc=cbba.

Defines rule #9.

Overlap of [2] abba=c with [3] ababcab=a:

Critical pair: abba=cbabcab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [8], [9], [11], [13], [15].

Overlap of [3] ababcab=a with [2] abba=c:

Critical pair: ababcc=aba.

Defines rule #24.

Referenced by [10], [11], [18], [31], [35], [36].

Overlap of [3] ababcab=a with [3] ababcab=a:

Critical pair: ababca=aabcab.

Flip LHS and RHS.

Referenced by [16].

Overlap of [5] cbabcab=c with [2] abba=c:

Critical pair: cbabcc=cba.

Defines rule #8.

Referenced by [19], [22], [23], [32].

Overlap of [5] cbabcab=c with [3] ababcab=a:

Critical pair: cbabca=cabcab.

Flip LHS and RHS.

Referenced by [17].

Overlap of [3] ababcab=a with [6] ababcc=aba:

Critical pair: ababcaba=aabcc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #23.

Referenced by [20], [33].

Overlap of [5] cbabcab=c with [6] ababcc=aba:

Critical pair: cbabcaba=cabcc.

Reduce LHS:

Flip LHS and RHS.

Defines rule #7.

Referenced by [12], [13], [21], [34].

Overlap of [3] ababcab=a with [11] cabcc=ca:

Critical pair: ababca=acc.

Defines rule #28.

Referenced by [14], [16], [35], [36].

Overlap of [5] cbabcab=c with [11] cabcc=ca:

Critical pair: cbabca=ccc.

Defines rule #14.

Referenced by [15], [17], [24], [25], [26], [27].

Overlap of [3] ababcab=a with [12] ababca=acc:

Critical pair: accb=a.

Defines rule #10.

Referenced by [36].

Overlap of [5] cbabcab=c with [13] cbabca=ccc:

Critical pair: cccb=c.

Defines rule #1.

Referenced by [18], [19], [20], [21], [24], [25], [26], [30], [37].

Simplify [7] aabcab=ababca.

Reduce RHS:

Referenced by [23].

Simplify [9] cabcab=cbabca.

Reduce RHS:

Referenced by [22].

Overlap of [6] ababcc=aba with [15] cccb=c:

Critical pair: ababc=abacb.

Flip LHS and RHS.

Defines rule #20.

Overlap of [8] cbabcc=cba with [15] cccb=c:

Critical pair: cbabc=cbacb.

Flip LHS and RHS.

Defines rule #4.

Referenced by [26], [27].

Overlap of [10] aabcc=aa with [15] cccb=c:

Critical pair: aabc=aacb.

Flip LHS and RHS.

Defines rule #19.

Referenced by [23], [24], [28].

Overlap of [11] cabcc=ca with [15] cccb=c:

Critical pair: cabc=cacb.

Flip LHS and RHS.

Defines rule #3.

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

Overlap of [21] cacb=cabc with [8] cbabcc=cba:

Critical pair: cacba=cabcabcc.

Reduce LHS:

Reduce RHS:

Defines rule #13.

Referenced by [25], [29], [36].

Overlap of [20] aacb=aabc with [8] cbabcc=cba:

Critical pair: aacba=aabcabcc.

Reduce LHS:

Reduce RHS:

Defines rule #27.

Referenced by [24], [28].

Overlap of [20] aacb=aabc with [13] cbabca=ccc:

Critical pair: aaccc=aabcabca.

Reduce RHS:

Defines rule #21.

Overlap of [21] cacb=cabc with [13] cbabca=ccc:

Critical pair: caccc=cabcabca.

Reduce RHS:

Defines rule #5.

Referenced by [35].

Overlap of [19] cbacb=cbabc with [13] cbabca=ccc:

Critical pair: cbaccc=cbabcabca.

Reduce RHS:

Defines rule #6.

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

Overlap of [19] cbacb=cbabc with [26] cbaccc=cca:

Critical pair: cbacca=cbabcaccc.

Reduce RHS:

Defines rule #12.

Overlap of [20] aacb=aabc with [26] cbaccc=cca:

Critical pair: aacca=aabcaccc.

Reduce RHS:

Defines rule #25.

Overlap of [21] cacb=cabc with [26] cbaccc=cca:

Critical pair: cacca=cabcaccc.

Reduce RHS:

Defines rule #11.

Overlap of [26] cbaccc=cca with [15] cccb=c:

Critical pair: cbac=ccab.

Flip LHS and RHS.

Defines rule #2.

Referenced by [31], [32], [33], [34].

Overlap of [6] ababcc=aba with [30] ccab=cbac:

Critical pair: ababcbac=abaab.

Flip LHS and RHS.

Defines rule #30.

Overlap of [8] cbabcc=cba with [30] ccab=cbac:

Critical pair: cbabcbac=cbaab.

Flip LHS and RHS.

Defines rule #17.

Overlap of [10] aabcc=aa with [30] ccab=cbac:

Critical pair: aabcbac=aaab.

Flip LHS and RHS.

Defines rule #29.

Overlap of [11] cabcc=ca with [30] ccab=cbac:

Critical pair: cabcbac=caab.

Flip LHS and RHS.

Defines rule #16.

Overlap of [12] ababca=acc with [25] caccc=cccca:

Critical pair: ababcccca=accccc.

Reduce LHS:

Defines rule #26.

Overlap of [12] ababca=acc with [22] cabca=ccccc:

Critical pair: ababccccc=accbca.

Reduce LHS:

Reduce RHS:

Defines rule #22.

Referenced by [37].

Overlap of [36] abaccc=aca with [15] cccb=c:

Critical pair: abac=acab.

Flip LHS and RHS.

Defines rule #18.