Certificate for #3109 ⟨a, b | aabbaababba=1⟩

Completion settings:

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

Axiom: aabbaababba=1.

Referenced by [3].

Axiom: abbaa=c.

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

Overlap of [1] aabbaababba=1 with [2] abbaa=c:

Critical pair: acbabba=1.

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

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

Critical pair: abbac=cbbaa.

Flip LHS and RHS.

Referenced by [10].

Overlap of [3] acbabba=1 with [2] abbaa=c:

Critical pair: acbc=a.

Referenced by [7].

Overlap of [3] acbabba=1 with [2] abbaa=c:

Critical pair: acbabbc=bbaa.

Flip LHS and RHS.

Referenced by [15], [16].

Overlap of [3] acbabba=1 with [5] acbc=a:

Critical pair: acbabba=cbc.

Reduce LHS:

Flip LHS and RHS.

Referenced by [8], [9].

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

Critical pair: cb=bc.

Defines rule #1.

Referenced by [9], [10], [11], [12], [15], [16], [20], [22], [24], [25], [26].

Overlap of [7] cbc=1 with [8] cb=bc:

Critical pair: bcc=1.

Defines rule #2.

Referenced by [11], [13], [17], [18], [19], [20], [22], [23], [24], [25], [26].

Simplify [4] cbbaa=abbac.

Reduce LHS:

Defines rule #6.

Referenced by [11], [20], [26].

Overlap of [8] cb=bc with [10] bbcaa=abbac:

Critical pair: cabbac=bcbcaa.

Reduce RHS:

Referenced by [12].

Overlap of [11] cabbac=baa with [8] cb=bc:

Critical pair: cabbabc=baab.

Referenced by [13].

Overlap of [12] cabbabc=baab with [9] bcc=1:

Critical pair: cabba=baabc.

Defines rule #3.

Referenced by [14].

Overlap of [13] cabba=baabc with [2] abbaa=c:

Critical pair: cc=baabca.

Flip LHS and RHS.

Referenced by [19], [23].

Overlap of [2] abbaa=c with [6] bbaa=acbabbc:

Critical pair: aacbabbc=c.

Reduce LHS:

Referenced by [17].

Simplify [6] bbaa=acbabbc.

Reduce RHS:

Defines rule #5.

Overlap of [15] aabcabbc=c with [9] bcc=1:

Critical pair: aabcab=cc.

Referenced by [18], [21].

Overlap of [17] aabcab=cc with [9] bcc=1:

Critical pair: aabca=cccc.

Defines rule #7.

Referenced by [19].

Overlap of [14] baabca=cc with [18] aabca=cccc:

Critical pair: baabccccc=ccabca.

Reduce LHS:

Flip LHS and RHS.

Referenced by [20].

Overlap of [9] bcc=1 with [19] ccabca=baaccc:

Critical pair: bcbaaccc=cabca.

Reduce LHS:

Flip LHS and RHS.

Defines rule #4.

Referenced by [21].

Overlap of [17] aabcab=cc with [20] cabca=abbacccc:

Critical pair: aababbacccc=ccca.

Referenced by [22].

Overlap of [21] aababbacccc=ccca with [8] cb=bc:

Critical pair: aababbacccbc=cccab.

Reduce LHS:

Referenced by [23], [24].

Overlap of [14] baabca=cc with [22] aababbacc=cccab:

Critical pair: baabccccab=ccababbacc.

Reduce LHS:

Flip LHS and RHS.

Referenced by [25].

Overlap of [22] aababbacc=cccab with [8] cb=bc:

Critical pair: aababbacbc=cccabb.

Reduce LHS:

Defines rule #9.

Overlap of [23] ccababbacc=baaccab with [8] cb=bc:

Critical pair: ccababbacbc=baaccabb.

Reduce LHS:

Referenced by [26].

Overlap of [9] bcc=1 with [25] ccababba=baaccabb:

Critical pair: bcbaaccabb=cababba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #8.