Certificate for #3188 ⟨a, b | abaaabaabba=1⟩

Completion settings:

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

Axiom: abaaabaabba=1.

Referenced by [4].

Axiom: baab=c.

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

Axiom: aaa=d.

Defines rule #7.

Referenced by [4], [5], [8], [10], [11], [14].

Overlap of [1] abaaabaabba=1 with [3] aaa=d:

Critical pair: abdbaabba=1.

Reduce LHS:

Referenced by [7], [8], [9], [11], [12].

Overlap of [3] aaa=d with [3] aaa=d:

Critical pair: ad=da.

Defines rule #3.

Referenced by [17], [22].

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

Critical pair: baac=caab.

Flip LHS and RHS.

Referenced by [23].

Overlap of [2] baab=c with [4] abdcba=1:

Critical pair: ba=cdcba.

Flip LHS and RHS.

Referenced by [10].

Overlap of [3] aaa=d with [4] abdcba=1:

Critical pair: aa=dbdcba.

Flip LHS and RHS.

Referenced by [11].

Overlap of [4] abdcba=1 with [4] abdcba=1:

Critical pair: abdcb=bdcba.

Referenced by [11], [12].

Overlap of [7] cdcba=ba with [3] aaa=d:

Critical pair: cdcbd=baaa.

Reduce RHS:

Referenced by [13], [21], [22].

Overlap of [8] dbdcba=aa with [4] abdcba=1:

Critical pair: dbdcb=aabdcba.

Reduce RHS:

Flip LHS and RHS.

Referenced by [14].

Overlap of [4] abdcba=1 with [9] abdcb=bdcba:

Critical pair: bdcbaa=1.

Referenced by [13], [14].

Overlap of [10] cdcbd=bd with [12] bdcbaa=1:

Critical pair: cdc=bdcbaa.

Reduce RHS:

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

Overlap of [12] bdcbaa=1 with [3] aaa=d:

Critical pair: bdcbd=a.

Reduce LHS:

Referenced by [19].

Overlap of [13] cdc=1 with [13] cdc=1:

Critical pair: cd=dc.

Defines rule #1.

Referenced by [16], [18], [19], [22].

Overlap of [13] cdc=1 with [15] cd=dc:

Critical pair: dcc=1.

Defines rule #2.

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

Overlap of [5] ad=da with [16] dcc=1:

Critical pair: a=dacc.

Flip LHS and RHS.

Referenced by [18].

Overlap of [15] cd=dc with [17] dacc=a:

Critical pair: ca=dcacc.

Flip LHS and RHS.

Referenced by [20].

Overlap of [15] cd=dc with [14] dbdcb=a:

Critical pair: ca=dcbdcb.

Flip LHS and RHS.

Referenced by [21], [22].

Overlap of [13] cdc=1 with [18] dcacc=ca:

Critical pair: cca=acc.

Flip LHS and RHS.

Defines rule #4.

Overlap of [10] cdcbd=bd with [19] dcbdcb=ca:

Critical pair: cca=bdcb.

Flip LHS and RHS.

Defines rule #6.

Referenced by [22].

Overlap of [10] cdcbd=bd with [19] dcbdcb=ca:

Critical pair: cdcbca=bdcbdcb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #5.

Overlap of [16] dcc=1 with [6] caab=baac:

Critical pair: dcbaac=aab.

Flip LHS and RHS.

Defines rule #8.