Certificate for #1360 ⟨a, b | aaababbaba=1⟩

Completion settings:

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

Axiom: aaababbaba=1.

Referenced by [4].

Axiom: aaaa=c.

Defines rule #2.

Referenced by [5], [6], [8], [13], [14], [15], [16], [22], [23], [36], [42].

Axiom: babbab=d.

Referenced by [4], [25], [26], [34].

Overlap of [1] aaababbaba=1 with [3] babbab=d:

Critical pair: aaada=1.

Referenced by [6], [7], [9], [10], [11], [14], [17], [22].

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

Critical pair: ac=ca.

Flip LHS and RHS.

Defines rule #1.

Referenced by [13], [18], [19], [21], [33], [39], [40], [41].

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

Critical pair: a=cda.

Flip LHS and RHS.

Referenced by [8], [9], [12], [18], [20].

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

Critical pair: aaad=aada.

Referenced by [9], [11], [15], [17], [22].

Overlap of [6] cda=a with [2] aaaa=c:

Critical pair: cdc=aaaa.

Reduce RHS:

Referenced by [12].

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

Critical pair: cd=aaada.

Reduce RHS:

Flip LHS and RHS.

Referenced by [10], [11], [12], [13], [14], [15].

Overlap of [4] aaada=1 with [9] aadaa=cd:

Critical pair: acd=a.

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

Overlap of [4] aaada=1 with [9] aadaa=cd:

Critical pair: aaadcd=adaa.

Reduce LHS:

Referenced by [12], [15].

Overlap of [6] cda=a with [9] aadaa=cd:

Critical pair: cdcd=aadaa.

Reduce LHS:

Reduce RHS:

Referenced by [13], [14], [15], [16], [18], [23].

Overlap of [9] aadaa=cd with [2] aaaa=c:

Critical pair: aadc=cdaa.

Reduce RHS:

Referenced by [15].

Overlap of [9] aadaa=cd with [4] aaada=1:

Critical pair: aad=cdada.

Reduce RHS:

Flip LHS and RHS.

Referenced by [15].

Overlap of [9] aadaa=cd with [9] aadaa=cd:

Critical pair: aadcd=cddaa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

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

Simplify [10] acd=a.

Reduce LHS:

Referenced by [17], [18].

Overlap of [4] aaada=1 with [16] adc=a:

Critical pair: aaada=dc.

Reduce LHS:

Referenced by [18].

Overlap of [6] cda=a with [16] adc=a:

Critical pair: cda=adc.

Reduce LHS:

Reduce RHS:

Defines rule #4.

Referenced by [19], [20], [24].

Overlap of [18] dac=a with [5] ca=ac:

Critical pair: daac=aa.

Defines rule #5.

Referenced by [21], [29].

Overlap of [18] dac=a with [6] cda=a:

Critical pair: daa=ada.

Flip LHS and RHS.

Referenced by [22], [23].

Overlap of [19] daac=aa with [5] ca=ac:

Critical pair: daaac=aaa.

Defines rule #6.

Referenced by [30].

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

Critical pair: aadaa=1.

Reduce LHS:

Defines rule #3.

Referenced by [23], [31], [34], [35], [36], [38].

Simplify [12] cd=adaaa.

Reduce RHS:

Defines rule #8.

Referenced by [24], [27], [32], [38].

Overlap of [18] dac=a with [23] cd=1:

Critical pair: da=ad.

Flip LHS and RHS.

Defines rule #7.

Referenced by [26], [28].

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

Critical pair: babd=dbab.

Flip LHS and RHS.

Defines rule #10.

Referenced by [27], [28].

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

Critical pair: babbad=dabbab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [32], [37].

Overlap of [23] cd=1 with [25] dbab=babd:

Critical pair: cbabd=bab.

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

Overlap of [24] ad=da with [25] dbab=babd:

Critical pair: ababd=dabab.

Flip LHS and RHS.

Defines rule #11.

Overlap of [19] daac=aa with [27] cbabd=bab:

Critical pair: daabab=aababd.

Defines rule #12.

Overlap of [21] daaac=aaa with [27] cbabd=bab:

Critical pair: daaabab=aaababd.

Defines rule #13.

Referenced by [37], [38].

Overlap of [27] cbabd=bab with [22] dc=1:

Critical pair: cbab=babc.

Defines rule #9.

Referenced by [32], [33], [34], [39], [40], [41].

Overlap of [23] cd=1 with [26] dabbab=babbda:

Critical pair: cbabbda=abbab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #14.

Referenced by [33], [34].

Overlap of [5] ca=ac with [32] abbab=babcbda:

Critical pair: cbabcbda=acbbab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #15.

Referenced by [39].

Overlap of [31] cbab=babc with [32] abbab=babcbda:

Critical pair: cbbabcbda=babcbab.

Reduce RHS:

Referenced by [35].

Overlap of [22] dc=1 with [34] cbbabcbda=1:

Critical pair: d=bbabcbda.

Flip LHS and RHS.

Referenced by [36], [37].

Overlap of [35] bbabcbda=d with [2] aaaa=c:

Critical pair: bbabcbdc=daaa.

Reduce LHS:

Defines rule #22.

Referenced by [37], [38].

Overlap of [35] bbabcbda=d with [26] dabbab=babbda:

Critical pair: bbabcbbabbda=dbbab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #21.

Overlap of [36] bbabcb=daaa with [36] bbabcb=daaa:

Critical pair: bbabcdaaa=daaababcb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #16.

Referenced by [40].

Overlap of [5] ca=ac with [33] acbbab=babccbda:

Critical pair: cbabccbda=accbbab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #19.

Referenced by [42].

Overlap of [5] ca=ac with [38] aaababb=bbabaaa:

Critical pair: cbbabaaa=acaababb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #17.

Referenced by [41].

Overlap of [5] ca=ac with [40] aaababcb=cbbabaaa:

Critical pair: ccbbabaaa=acaababcb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #18.

Overlap of [2] aaaa=c with [39] accbbab=babcccbda:

Critical pair: aaababcccbda=cccbbab.

Flip LHS and RHS.

Defines rule #20.