Certificate for #294 ⟨a, b | aaabbaba=1⟩

Completion settings:

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

Axiom: aaabbaba=1.

Referenced by [4].

Axiom: aaaa=c.

Defines rule #5.

Referenced by [5], [6], [13], [14], [19], [21], [23], [27].

Axiom: bbab=d.

Defines rule #15.

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

Overlap of [1] aaabbaba=1 with [3] bbab=d:

Critical pair: aaada=1.

Referenced by [6], [7], [8], [10].

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

Critical pair: ac=ca.

Defines rule #3.

Referenced by [20], [24].

Overlap of [2] aaaa=c with [4] aaada=1:

Critical pair: a=cda.

Flip LHS and RHS.

Referenced by [8].

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

Critical pair: aaad=aada.

Referenced by [8], [10], [14].

Overlap of [6] cda=a with [4] aaada=1:

Critical pair: cd=aaada.

Reduce RHS:

Flip LHS and RHS.

Referenced by [10], [11].

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

Critical pair: bbad=dbab.

Flip LHS and RHS.

Referenced by [15].

Overlap of [4] aaada=1 with [7] aaad=aada:

Critical pair: aadaa=1.

Reduce LHS:

Defines rule #1.

Referenced by [11], [13], [16], [21], [25].

Simplify [8] aadaa=cd.

Reduce RHS:

Referenced by [12], [14].

Overlap of [11] aadaa=1 with [11] aadaa=1:

Critical pair: aad=daa.

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

Overlap of [2] aaaa=c with [12] aad=daa:

Critical pair: aadaa=cd.

Reduce LHS:

Reduce RHS:

Defines rule #2.

Referenced by [14], [19], [26], [27].

Overlap of [11] aadaa=1 with [12] aad=daa:

Critical pair: aadadaa=ad.

Reduce LHS:

Flip LHS and RHS.

Defines rule #4.

Referenced by [15], [18], [26].

Simplify [9] dbab=bbad.

Reduce RHS:

Defines rule #7.

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

Overlap of [10] cd=1 with [15] dbab=bbda:

Critical pair: cbbda=bab.

Referenced by [19].

Overlap of [12] aad=daa with [15] dbab=bbda:

Critical pair: aabbda=daabab.

Flip LHS and RHS.

Defines rule #12.

Referenced by [26].

Overlap of [14] ad=da with [15] dbab=bbda:

Critical pair: abbda=dabab.

Flip LHS and RHS.

Defines rule #10.

Overlap of [16] cbbda=bab with [2] aaaa=c:

Critical pair: cbbdc=babaaa.

Reduce LHS:

Defines rule #6.

Referenced by [20], [21].

Overlap of [5] ac=ca with [19] cbb=babaaa:

Critical pair: ababaaa=cabb.

Flip LHS and RHS.

Defines rule #9.

Referenced by [24].

Overlap of [19] cbb=babaaa with [3] bbab=d:

Critical pair: cd=babaaaab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [22].

Overlap of [21] babcb=1 with [21] babcb=1:

Critical pair: babc=abcb.

Flip LHS and RHS.

Defines rule #8.

Referenced by [23].

Overlap of [2] aaaa=c with [22] abcb=babc:

Critical pair: aaababc=cbcb.

Referenced by [25].

Overlap of [5] ac=ca with [20] cabb=ababaaa:

Critical pair: aababaaa=caabb.

Flip LHS and RHS.

Defines rule #11.

Overlap of [23] aaababc=cbcb with [10] cd=1:

Critical pair: aaabab=cbcbd.

Defines rule #14.

Referenced by [26].

Overlap of [14] ad=da with [17] daabab=aabbda:

Critical pair: aaabbda=daaabab.

Reduce RHS:

Referenced by [27].

Overlap of [26] aaabbda=bcbd with [2] aaaa=c:

Critical pair: aaabbdc=bcbdaaa.

Reduce LHS:

Defines rule #13.