Certificate for #1301 ⟨a, b | aaaaabbaba=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. aaaaaa=c
  2. bbab=d

Axiom: aaaaabbaba=1.

Referenced by [4].

Axiom: aaaaaa=c.

Defines rule #5.

Referenced by [6], [7], [8], [11], [20], [23], [38], [39], [41], [43], [48], [52], [53].

Axiom: bbab=d.

Defines rule #19.

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

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

Critical pair: aaaaada=1.

Referenced by [7], [8], [9], [10], [11], [14].

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

Critical pair: bbad=dbab.

Flip LHS and RHS.

Referenced by [17], [18], [19], [22], [24], [27], [31].

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

Critical pair: ac=ca.

Defines rule #3.

Referenced by [12], [13], [28], [37], [40], [42], [46], [47], [49].

Overlap of [2] aaaaaa=c with [4] aaaaada=1:

Critical pair: a=cda.

Flip LHS and RHS.

Referenced by [10], [11].

Overlap of [2] aaaaaa=c with [4] aaaaada=1:

Critical pair: aa=cada.

Flip LHS and RHS.

Referenced by [11].

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

Critical pair: aaaaad=aaaada.

Referenced by [10], [14].

Overlap of [7] cda=a with [4] aaaaada=1:

Critical pair: cd=aaaaada.

Reduce RHS:

Flip LHS and RHS.

Referenced by [14], [15].

Overlap of [8] cada=aa with [4] aaaaada=1:

Critical pair: cad=aaaaaada.

Reduce RHS:

Referenced by [12], [26].

Overlap of [6] ac=ca with [11] cad=a:

Critical pair: aa=caad.

Flip LHS and RHS.

Referenced by [13], [17].

Overlap of [6] ac=ca with [12] caad=aa:

Critical pair: aaa=caaad.

Flip LHS and RHS.

Referenced by [18].

Overlap of [4] aaaaada=1 with [9] aaaaad=aaaada:

Critical pair: aaaadaa=1.

Reduce LHS:

Defines rule #1.

Referenced by [15], [19], [20], [23], [29], [30], [45].

Simplify [10] aaaadaa=cd.

Reduce RHS:

Referenced by [16], [21].

Overlap of [15] aaaadaa=1 with [15] aaaadaa=1:

Critical pair: aaaad=aadaa.

Referenced by [20], [21], [22], [23].

Overlap of [12] caad=aa with [5] dbab=bbad:

Critical pair: caabbad=aabab.

Referenced by [32].

Overlap of [13] caaad=aaa with [5] dbab=bbad:

Critical pair: caaabbad=aaabab.

Referenced by [33].

Overlap of [14] cd=1 with [5] dbab=bbad:

Critical pair: cbbad=bab.

Referenced by [25].

Overlap of [2] aaaaaa=c with [16] aaaad=aadaa:

Critical pair: aaaadaa=cd.

Reduce LHS:

Reduce RHS:

Referenced by [21].

Overlap of [15] aaaadaa=1 with [16] aaaad=aadaa:

Critical pair: aaaadaadaa=aad.

Reduce LHS:

Flip LHS and RHS.

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

Overlap of [16] aaaad=aadaa with [5] dbab=bbad:

Critical pair: aaaabbad=aadaabab.

Reduce RHS:

Flip LHS and RHS.

Referenced by [34].

Overlap of [2] aaaaaa=c with [21] aad=daa:

Critical pair: aaaadaa=cd.

Reduce LHS:

Reduce RHS:

Defines rule #2.

Referenced by [25], [26], [38], [41], [43], [48], [49], [50], [52], [53].

Overlap of [21] aad=daa with [5] dbab=bbad:

Critical pair: aabbad=daabab.

Flip LHS and RHS.

Referenced by [35].

Overlap of [19] cbbad=bab with [23] dc=1:

Critical pair: cbba=babc.

Referenced by [28], [29], [30].

Overlap of [23] dc=1 with [11] cad=a:

Critical pair: da=ad.

Flip LHS and RHS.

Defines rule #4.

Referenced by [27], [30], [31], [32], [33], [34], [35], [44], [51].

Overlap of [26] ad=da with [5] dbab=bbad:

Critical pair: abbad=dabab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #10.

Overlap of [6] ac=ca with [25] cbba=babc:

Critical pair: ababc=cabba.

Flip LHS and RHS.

Referenced by [40].

Overlap of [25] cbba=babc with [3] bbab=d:

Critical pair: cd=babcb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [36].

Overlap of [25] cbba=babc with [26] ad=da:

Critical pair: cbbda=babcd.

Reduce RHS:

Referenced by [37], [38].

Simplify [5] dbab=bbad.

Reduce RHS:

Defines rule #7.

Overlap of [17] caabbad=aabab with [26] ad=da:

Critical pair: caabbda=aabab.

Referenced by [43].

Overlap of [18] caaabbad=aaabab with [26] ad=da:

Critical pair: caaabbda=aaabab.

Referenced by [47], [48].

Simplify [22] daaaabab=aaaabbad.

Reduce RHS:

Defines rule #16.

Simplify [24] daabab=aabbad.

Reduce RHS:

Defines rule #12.

Referenced by [44].

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

Critical pair: babc=abcb.

Flip LHS and RHS.

Defines rule #8.

Referenced by [39].

Overlap of [6] ac=ca with [30] cbbda=bab:

Critical pair: abab=cabbda.

Flip LHS and RHS.

Referenced by [41].

Overlap of [30] cbbda=bab with [2] aaaaaa=c:

Critical pair: cbbdc=babaaaaa.

Reduce LHS:

Defines rule #6.

Overlap of [2] aaaaaa=c with [36] abcb=babc:

Critical pair: aaaaababc=cbcb.

Referenced by [45].

Overlap of [6] ac=ca with [28] cabba=ababc:

Critical pair: aababc=caabba.

Flip LHS and RHS.

Referenced by [42].

Overlap of [37] cabbda=abab with [2] aaaaaa=c:

Critical pair: cabbdc=ababaaaaa.

Reduce LHS:

Defines rule #9.

Overlap of [6] ac=ca with [40] caabba=aababc:

Critical pair: aaababc=caaabba.

Flip LHS and RHS.

Referenced by [46].

Overlap of [32] caabbda=aabab with [2] aaaaaa=c:

Critical pair: caabbdc=aababaaaaa.

Reduce LHS:

Defines rule #11.

Overlap of [26] ad=da with [35] daabab=aabbda:

Critical pair: aaabbda=daaabab.

Flip LHS and RHS.

Defines rule #14.

Overlap of [39] aaaaababc=cbcb with [14] cd=1:

Critical pair: aaaaabab=cbcbd.

Defines rule #18.

Referenced by [49].

Overlap of [6] ac=ca with [42] caaabba=aaababc:

Critical pair: aaaababc=caaaabba.

Flip LHS and RHS.

Referenced by [49].

Overlap of [6] ac=ca with [33] caaabbda=aaabab:

Critical pair: aaaabab=caaaabbda.

Flip LHS and RHS.

Referenced by [53].

Overlap of [33] caaabbda=aaabab with [2] aaaaaa=c:

Critical pair: caaabbdc=aaababaaaaa.

Reduce LHS:

Defines rule #13.

Overlap of [6] ac=ca with [46] caaaabba=aaaababc:

Critical pair: aaaaababc=caaaaabba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [50].

Overlap of [23] dc=1 with [49] caaaaabba=cbcb:

Critical pair: dcbcb=aaaaabba.

Reduce LHS:

Flip LHS and RHS.

Referenced by [51].

Overlap of [50] aaaaabba=bcb with [26] ad=da:

Critical pair: aaaaabbda=bcbd.

Referenced by [52].

Overlap of [51] aaaaabbda=bcbd with [2] aaaaaa=c:

Critical pair: aaaaabbdc=bcbdaaaaa.

Reduce LHS:

Defines rule #17.

Overlap of [47] caaaabbda=aaaabab with [2] aaaaaa=c:

Critical pair: caaaabbdc=aaaababaaaaa.

Reduce LHS:

Defines rule #15.