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

Completion settings:

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

Axiom: abaabbaba=ab.

Referenced by [3].

Axiom: abb=c.

Defines rule #4.

Referenced by [3], [4], [7], [10], [14], [15], [17], [21].

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

Critical pair: abacaba=ab.

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

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.

Defines rule #7.

Referenced by [6], [7], [13], [14], [15], [16], [17], [19], [22].

Simplify [4] abacabc=cb.

Reduce LHS:

Defines rule #6.

Referenced by [7], [8], [9], [12], [16], [18], [20], [22], [23], [25].

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

Critical pair: abacabcb=abbcabac.

Reduce LHS:

Reduce RHS:

Defines rule #9.

Referenced by [9], [20], [24], [26], [27].

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

Critical pair: abcab=cbaba.

Flip LHS and RHS.

Defines rule #10.

Referenced by [10], [11], [12], [16].

Overlap of [6] abcabac=cb with [7] cbb=ccabac:

Critical pair: abcabaccabac=cbbb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #17.

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

Critical pair: cbabc=abcabbb.

Reduce RHS:

Defines rule #11.

Referenced by [12].

Overlap of [8] cbaba=abcab with [3] abacaba=ab:

Critical pair: cbab=abcabcaba.

Flip LHS and RHS.

Defines rule #20.

Overlap of [10] cbabc=abccb with [6] abcabac=cb:

Critical pair: cbcb=abccbabac.

Reduce RHS:

Flip LHS and RHS.

Defines rule #21.

Overlap of [3] abacaba=ab with [5] abacab=abcaba:

Critical pair: abcabaa=ab.

Defines rule #5.

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

Overlap of [3] abacaba=ab with [5] abacab=abcaba:

Critical pair: abacababcaba=abbacab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #2.

Referenced by [21], [22].

Overlap of [5] abacab=abcaba with [2] abb=c:

Critical pair: abacc=abcabab.

Flip LHS and RHS.

Defines rule #18.

Overlap of [5] abacab=abcaba with [6] abcabac=cb:

Critical pair: abaccb=abcabacabac.

Reduce RHS:

Defines rule #8.

Referenced by [26].

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

Critical pair: abacabab=abbcabaa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #1.

Referenced by [18], [19].

Overlap of [6] abcabac=cb with [17] ccabaa=c:

Critical pair: abcabac=cbcabaa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #12.

Referenced by [20].

Overlap of [17] ccabaa=c with [5] abacab=abcaba:

Critical pair: ccabaabcaba=cbacab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #13.

Overlap of [18] cbcabaa=cb with [6] abcabac=cb:

Critical pair: cbcabacb=cbbcabac.

Reduce RHS:

Defines rule #24.

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

Critical pair: cacc=ccabab.

Flip LHS and RHS.

Defines rule #15.

Referenced by [25].

Overlap of [14] cacab=ccaba with [6] abcabac=cb:

Critical pair: caccb=ccabacabac.

Reduce RHS:

Defines rule #3.

Referenced by [23], [24].

Overlap of [6] abcabac=cb with [22] caccb=ccabc:

Critical pair: abcabaccabc=cbaccb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #14.

Referenced by [27].

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

Critical pair: cacccabac=ccabcb.

Flip LHS and RHS.

Defines rule #16.

Overlap of [6] abcabac=cb with [21] ccabab=cacc:

Critical pair: abcabacacc=cbcabab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #22.

Overlap of [16] abaccb=abcabc with [7] cbb=ccabac:

Critical pair: abacccabac=abcabcb.

Flip LHS and RHS.

Defines rule #19.

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

Critical pair: cbacccabac=cbcabcb.

Flip LHS and RHS.

Defines rule #23.