Certificate for #4276 ⟨a, b | abaabbaba=ab⟩

Completion settings:

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

Axiom: abaabbaba=ab.

Referenced by [3].

Axiom: abb=c.

Defines rule #10.

Referenced by [3], [4], [7], [10], [12], [16], [17], [18], [21], [23], [27].

Overlap of [1] abaabbaba=ab with [2] abb=c:

Critical pair: abacaba=ab.

Referenced by [4], [5], [7], [8], [15], [16].

Overlap of [3] abacaba=ab with [2] abb=c:

Critical pair: abacabc=abbb.

Reduce RHS:

Referenced by [6].

Overlap of [3] abacaba=ab with [3] abacaba=ab:

Critical pair: abacab=abcaba.

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

Simplify [4] abacabc=cb.

Reduce LHS:

Referenced by [7], [8], [9], [18].

Overlap of [3] abacaba=ab with [6] abcabac=cb:

Critical pair: abacabcb=abbcabac.

Reduce LHS:

Reduce RHS:

Defines rule #4.

Referenced by [11], [13], [16], [18], [25], [26], [28], [29].

Overlap of [6] abcabac=cb with [3] abacaba=ab:

Critical pair: abcab=cbaba.

Defines rule #12.

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

Overlap of [6] abcabac=cb with [8] abcab=cbaba:

Critical pair: cbabaac=cb.

Defines rule #5.

Referenced by [11], [16], [19], [22], [24], [29].

Overlap of [8] abcab=cbaba with [2] abb=c:

Critical pair: abcc=cbabab.

Flip LHS and RHS.

Defines rule #19.

Referenced by [12].

Overlap of [9] cbabaac=cb with [7] cbb=ccabac:

Critical pair: cbabaaccabac=cbbb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #17.

Referenced by [20], [29].

Overlap of [10] cbabab=abcc with [2] abb=c:

Critical pair: cbabc=abccb.

Flip LHS and RHS.

Defines rule #11.

Referenced by [13].

Overlap of [12] abccb=cbabc with [7] cbb=ccabac:

Critical pair: abcccabac=cbabcb.

Flip LHS and RHS.

Defines rule #18.

Simplify [5] abacab=abcaba.

Reduce RHS:

Defines rule #14.

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

Overlap of [3] abacaba=ab with [14] abacab=cbabaa:

Critical pair: cbabaaa=ab.

Defines rule #6.

Referenced by [16], [18], [20].

Overlap of [3] abacaba=ab with [14] abacab=cbabaa:

Critical pair: abacabcbabaa=abbacab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #3.

Referenced by [21].

Overlap of [14] abacab=cbabaa with [2] abb=c:

Critical pair: abacc=cbabaab.

Flip LHS and RHS.

Defines rule #21.

Referenced by [27].

Overlap of [6] abcabac=cb with [15] cbabaaa=ab:

Critical pair: abcabaab=cbbabaaa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #1.

Referenced by [19], [20].

Overlap of [9] cbabaac=cb with [18] ccabaa=c:

Critical pair: cbabaac=cbcabaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #7.

Overlap of [18] ccabaa=c with [14] abacab=cbabaa:

Critical pair: ccabacbabaa=cbacab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #9.

Overlap of [16] cacab=ccaba with [2] abb=c:

Critical pair: cacc=ccabab.

Flip LHS and RHS.

Defines rule #16.

Referenced by [22], [23].

Overlap of [9] cbabaac=cb with [21] ccabab=cacc:

Critical pair: cbabaacacc=cbcabab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #23.

Overlap of [21] ccabab=cacc with [2] abb=c:

Critical pair: ccabc=caccb.

Flip LHS and RHS.

Defines rule #2.

Referenced by [24], [25].

Overlap of [9] cbabaac=cb with [23] caccb=ccabc:

Critical pair: cbabaaccabc=cbaccb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #8.

Referenced by [26].

Overlap of [23] caccb=ccabc with [7] cbb=ccabac:

Critical pair: cacccabac=ccabcb.

Flip LHS and RHS.

Defines rule #15.

Overlap of [24] cbaccb=cbcabc with [7] cbb=ccabac:

Critical pair: cbacccabac=cbcabcb.

Flip LHS and RHS.

Defines rule #22.

Overlap of [17] cbabaab=abacc with [2] abb=c:

Critical pair: cbabac=abaccb.

Flip LHS and RHS.

Defines rule #13.

Referenced by [28].

Overlap of [27] abaccb=cbabac with [7] cbb=ccabac:

Critical pair: abacccabac=cbabacb.

Flip LHS and RHS.

Defines rule #20.

Overlap of [9] cbabaac=cb with [11] ccabacb=cbcabac:

Critical pair: cbabaacbcabac=cbcabacb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #24.