Certificate for #2918 ⟨a, b | aaabaababba=1⟩

Completion settings:

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

Axiom: aaabaababba=1.

Referenced by [4].

Axiom: baabab=c.

Defines rule #10.

Referenced by [4], [8], [9], [13], [15], [19], [36].

Axiom: aacb=d.

Referenced by [4], [7].

Overlap of [1] aaabaababba=1 with [2] baabab=c:

Critical pair: aaacba=1.

Reduce LHS:

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

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

Critical pair: ad=da.

Defines rule #1.

Referenced by [6], [11], [24], [25], [26], [27], [28], [34], [35], [39], [40], [42].

Overlap of [4] ada=1 with [5] ad=da:

Critical pair: daa=1.

Defines rule #2.

Referenced by [7], [9], [15], [17], [18], [22], [23], [24], [25], [26], [28], [33], [34], [38], [39], [41], [42], [44], [45], [46], [47], [48], [49].

Overlap of [6] daa=1 with [3] aacb=d:

Critical pair: dd=cb.

Flip LHS and RHS.

Defines rule #3.

Referenced by [9], [10], [13], [14], [25], [29], [34].

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

Critical pair: baabac=caabab.

Defines rule #14.

Overlap of [7] cb=dd with [2] baabab=c:

Critical pair: cc=ddaabab.

Reduce RHS:

Defines rule #5.

Referenced by [10].

Overlap of [9] cc=dbab with [7] cb=dd:

Critical pair: cdd=dbabb.

Flip LHS and RHS.

Referenced by [11].

Overlap of [5] ad=da with [10] dbabb=cdd:

Critical pair: acdd=dababb.

Flip LHS and RHS.

Referenced by [12].

Overlap of [4] ada=1 with [11] dababb=acdd:

Critical pair: aacdd=babb.

Flip LHS and RHS.

Defines rule #9.

Referenced by [13], [14], [15], [16], [30], [31].

Overlap of [2] baabab=c with [12] babb=aacdd:

Critical pair: baaaacdd=cb.

Reduce RHS:

Referenced by [17].

Overlap of [7] cb=dd with [12] babb=aacdd:

Critical pair: caacdd=ddabb.

Referenced by [22].

Overlap of [12] babb=aacdd with [2] baabab=c:

Critical pair: babc=aacddaabab.

Reduce RHS:

Defines rule #13.

Overlap of [12] babb=aacdd with [12] babb=aacdd:

Critical pair: babaacdd=aacddabb.

Referenced by [41].

Overlap of [13] baaaacdd=dd with [6] daa=1:

Critical pair: baaaacd=ddaa.

Reduce RHS:

Referenced by [18].

Overlap of [17] baaaacd=d with [6] daa=1:

Critical pair: baaaac=daa.

Reduce RHS:

Defines rule #4.

Referenced by [19], [20].

Overlap of [2] baabab=c with [18] baaaac=1:

Critical pair: baaba=caaaac.

Flip LHS and RHS.

Defines rule #8.

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

Overlap of [18] baaaac=1 with [19] caaaac=baaba:

Critical pair: baaaabaaba=aaaac.

Referenced by [36], [37], [38].

Overlap of [19] caaaac=baaba with [19] caaaac=baaba:

Critical pair: caaaabaaba=baabaaaaac.

Flip LHS and RHS.

Defines rule #19.

Overlap of [14] caacdd=ddabb with [6] daa=1:

Critical pair: caacd=ddabbaa.

Referenced by [23].

Overlap of [22] caacd=ddabbaa with [6] daa=1:

Critical pair: caac=ddabbaaaa.

Defines rule #6.

Referenced by [24], [25].

Overlap of [19] caaaac=baaba with [23] caac=ddabbaaaa:

Critical pair: caaaaddabbaaaa=baabaaac.

Reduce LHS:

Flip LHS and RHS.

Defines rule #18.

Overlap of [23] caac=ddabbaaaa with [7] cb=dd:

Critical pair: caadd=ddabbaaaab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [26].

Overlap of [5] ad=da with [25] ddabbaaaab=cd:

Critical pair: acd=dadabbaaaab.

Reduce RHS:

Flip LHS and RHS.

Referenced by [27].

Overlap of [5] ad=da with [26] dbbaaaab=acd:

Critical pair: aacd=dabbaaaab.

Flip LHS and RHS.

Referenced by [28].

Overlap of [5] ad=da with [27] dabbaaaab=aacd:

Critical pair: aaacd=daabbaaaab.

Reduce RHS:

Flip LHS and RHS.

Defines rule #12.

Referenced by [29], [30], [31], [32], [38], [43].

Overlap of [7] cb=dd with [28] bbaaaab=aaacd:

Critical pair: caaacd=ddbaaaab.

Referenced by [33].

Overlap of [12] babb=aacdd with [28] bbaaaab=aaacd:

Critical pair: babaaacd=aacddbaaaab.

Referenced by [45].

Overlap of [28] bbaaaab=aaacd with [12] babb=aacdd:

Critical pair: bbaaaaaacdd=aaacdabb.

Referenced by [46].

Overlap of [28] bbaaaab=aaacd with [28] bbaaaab=aaacd:

Critical pair: bbaaaaaaacd=aaacdbaaaab.

Referenced by [48].

Overlap of [29] caaacd=ddbaaaab with [6] daa=1:

Critical pair: caaac=ddbaaaabaa.

Defines rule #7.

Referenced by [34].

Overlap of [33] caaac=ddbaaaabaa with [7] cb=dd:

Critical pair: caaadd=ddbaaaabaab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [35].

Overlap of [5] ad=da with [34] ddbaaaabaab=cda:

Critical pair: acda=dadbaaaabaab.

Reduce RHS:

Flip LHS and RHS.

Referenced by [39].

Overlap of [20] baaaabaaba=aaaac with [2] baabab=c:

Critical pair: baaaabaac=aaaacabab.

Defines rule #16.

Overlap of [20] baaaabaaba=aaaac with [20] baaaabaaba=aaaac:

Critical pair: baaaabaaaaaac=aaaacaaabaaba.

Defines rule #22.

Overlap of [28] bbaaaab=aaacd with [20] baaaabaaba=aaaac:

Critical pair: bbaaaaaaaac=aaacdaaaabaaba.

Reduce RHS:

Defines rule #24.

Overlap of [5] ad=da with [35] ddabaaaabaab=acda:

Critical pair: aacda=dadabaaaabaab.

Reduce RHS:

Flip LHS and RHS.

Referenced by [40].

Overlap of [5] ad=da with [39] dbaaaabaab=aacda:

Critical pair: aaacda=dabaaaabaab.

Flip LHS and RHS.

Referenced by [42].

Overlap of [16] babaacdd=aacddabb with [6] daa=1:

Critical pair: babaacd=aacddabbaa.

Referenced by [44].

Overlap of [5] ad=da with [40] dabaaaabaab=aaacda:

Critical pair: aaaacda=daabaaaabaab.

Reduce RHS:

Flip LHS and RHS.

Defines rule #11.

Referenced by [43].

Overlap of [42] baaaabaab=aaaacda with [28] bbaaaab=aaacd:

Critical pair: baaaabaaaaacd=aaaacdabaaaab.

Referenced by [49].

Overlap of [41] babaacd=aacddabbaa with [6] daa=1:

Critical pair: babaac=aacddabbaaaa.

Defines rule #15.

Overlap of [30] babaaacd=aacddbaaaab with [6] daa=1:

Critical pair: babaaac=aacddbaaaabaa.

Defines rule #17.

Overlap of [31] bbaaaaaacdd=aaacdabb with [6] daa=1:

Critical pair: bbaaaaaacd=aaacdabbaa.

Referenced by [47].

Overlap of [46] bbaaaaaacd=aaacdabbaa with [6] daa=1:

Critical pair: bbaaaaaac=aaacdabbaaaa.

Defines rule #21.

Overlap of [32] bbaaaaaaacd=aaacdbaaaab with [6] daa=1:

Critical pair: bbaaaaaaac=aaacdbaaaabaa.

Defines rule #23.

Overlap of [43] baaaabaaaaacd=aaaacdabaaaab with [6] daa=1:

Critical pair: baaaabaaaaac=aaaacdabaaaabaa.

Defines rule #20.