Certificate for #3077 ⟨a, b | aababbaabab=1⟩

Completion settings:

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

Axiom: aababbaabab=1.

Referenced by [3].

Axiom: aabab=c.

Referenced by [3], [6].

Overlap of [1] aababbaabab=1 with [2] aabab=c:

Critical pair: cbaabab=1.

Reduce LHS:

Referenced by [4], [5], [9].

Overlap of [3] cbc=1 with [3] cbc=1:

Critical pair: cb=bc.

Defines rule #1.

Referenced by [5], [9], [10], [12], [13], [17], [19], [20], [21], [23], [26].

Overlap of [3] cbc=1 with [4] cb=bc:

Critical pair: bcc=1.

Defines rule #2.

Referenced by [6], [7], [8], [11], [12], [13], [15], [18], [21], [22], [23], [24], [25], [27].

Overlap of [2] aabab=c with [5] bcc=1:

Critical pair: aaba=ccc.

Defines rule #7.

Referenced by [7], [12], [13], [23].

Overlap of [6] aaba=ccc with [6] aaba=ccc:

Critical pair: aabccc=cccaba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [8].

Overlap of [5] bcc=1 with [7] cccaba=aac:

Critical pair: baac=caba.

Flip LHS and RHS.

Defines rule #4.

Referenced by [9], [14], [20].

Overlap of [3] cbc=1 with [8] caba=baac:

Critical pair: cbbaac=aba.

Reduce LHS:

Referenced by [10].

Overlap of [9] bbcaac=aba with [4] cb=bc:

Critical pair: bbcaabc=abab.

Referenced by [11].

Overlap of [10] bbcaabc=abab with [5] bcc=1:

Critical pair: bbcaa=ababc.

Referenced by [12], [17].

Overlap of [11] bbcaa=ababc with [6] aaba=ccc:

Critical pair: bbcccc=ababcba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [13], [14].

Overlap of [6] aaba=ccc with [12] ababbca=1:

Critical pair: aab=cccbabbca.

Reduce RHS:

Flip LHS and RHS.

Defines rule #5.

Referenced by [15], [16], [21].

Overlap of [12] ababbca=1 with [8] caba=baac:

Critical pair: ababbbaac=ba.

Referenced by [19].

Overlap of [5] bcc=1 with [13] cabbca=aab:

Critical pair: bcaab=abbca.

Referenced by [17], [18].

Overlap of [13] cabbca=aab with [13] cabbca=aab:

Critical pair: cabbaab=aabbbca.

Referenced by [25].

Overlap of [11] bbcaa=ababc with [15] bcaab=abbca:

Critical pair: babbca=ababcb.

Reduce RHS:

Defines rule #3.

Referenced by [20], [21].

Overlap of [15] bcaab=abbca with [5] bcc=1:

Critical pair: bcaa=abbcacc.

Defines rule #6.

Overlap of [14] ababbbaac=ba with [4] cb=bc:

Critical pair: ababbbaabc=bab.

Referenced by [22].

Overlap of [17] babbca=ababbc with [8] caba=baac:

Critical pair: babbbaac=ababbcba.

Reduce RHS:

Referenced by [26].

Overlap of [17] babbca=ababbc with [13] cabbca=aab:

Critical pair: babbaab=ababbcbbca.

Reduce RHS:

Referenced by [24].

Overlap of [19] ababbbaabc=bab with [5] bcc=1:

Critical pair: ababbbaa=babc.

Referenced by [23].

Overlap of [6] aaba=ccc with [22] ababbbaa=babc:

Critical pair: aabbabc=cccbabbbaa.

Reduce RHS:

Flip LHS and RHS.

Defines rule #11.

Overlap of [21] babbaab=ababbba with [5] bcc=1:

Critical pair: babbaa=ababbbacc.

Defines rule #8.

Overlap of [16] cabbaab=aabbbca with [5] bcc=1:

Critical pair: cabbaa=aabbbcacc.

Defines rule #10.

Overlap of [20] babbbaac=ababbbca with [4] cb=bc:

Critical pair: babbbaabc=ababbbcab.

Referenced by [27].

Overlap of [26] babbbaabc=ababbbcab with [5] bcc=1:

Critical pair: babbbaa=ababbbcabc.

Defines rule #9.