Certificate for #3040 ⟨a, b | aabaababbba=1⟩

Completion settings:

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

Axiom: aabaababbba=1.

Referenced by [4].

Axiom: bbb=c.

Defines rule #5.

Referenced by [4], [5], [19], [21], [25], [30], [36], [42].

Axiom: aaabaaba=d.

Defines rule #18.

Referenced by [6], [7], [8], [9], [13], [15], [16], [17], [18], [20], [24].

Overlap of [1] aabaababbba=1 with [2] bbb=c:

Critical pair: aabaabaca=1.

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

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

Critical pair: bc=cb.

Defines rule #3.

Referenced by [22], [32], [35].

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

Critical pair: aaabaabd=daabaaba.

Flip LHS and RHS.

Referenced by [17], [24], [26], [33].

Overlap of [3] aaabaaba=d with [4] aabaabaca=1:

Critical pair: a=dca.

Flip LHS and RHS.

Referenced by [11].

Overlap of [3] aaabaaba=d with [4] aabaabaca=1:

Critical pair: aaab=dabaca.

Flip LHS and RHS.

Defines rule #7.

Referenced by [14], [15], [18], [22], [27], [28].

Overlap of [4] aabaabaca=1 with [3] aaabaaba=d:

Critical pair: aabaabacd=aabaaba.

Referenced by [12].

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

Critical pair: aabaabac=abaabaca.

Flip LHS and RHS.

Referenced by [15], [16], [17], [18], [20], [24].

Overlap of [7] dca=a with [4] aabaabaca=1:

Critical pair: dc=aabaabaca.

Reduce RHS:

Defines rule #2.

Referenced by [15], [17], [18], [19], [20], [23], [24], [25], [41], [42].

Overlap of [4] aabaabaca=1 with [9] aabaabacd=aabaaba:

Critical pair: aabaabacaabaaba=abaabacd.

Reduce LHS:

Flip LHS and RHS.

Referenced by [13], [14].

Overlap of [3] aaabaaba=d with [12] abaabacd=abaaba:

Critical pair: aaabaababaaba=dbaabacd.

Reduce LHS:

Flip LHS and RHS.

Referenced by [15].

Overlap of [8] dabaca=aaab with [12] abaabacd=abaaba:

Critical pair: dabacabaaba=aaabbaabacd.

Reduce LHS:

Flip LHS and RHS.

Referenced by [17], [19].

Overlap of [13] dbaabacd=dbaaba with [8] dabaca=aaab:

Critical pair: dbaabacaaab=dbaabaabaca.

Reduce RHS:

Referenced by [17].

Overlap of [3] aaabaaba=d with [10] abaabaca=aabaabac:

Critical pair: aaabaabaabaabac=dbaabaca.

Reduce LHS:

Flip LHS and RHS.

Referenced by [17], [24], [29].

Overlap of [15] dbaabacaaab=db with [14] aaabbaabacd=aaabbaaba:

Critical pair: dbaabacaaabbaaba=dbbaabacd.

Reduce LHS:

Flip LHS and RHS.

Referenced by [18].

Overlap of [17] dbbaabacd=dbbaaba with [8] dabaca=aaab:

Critical pair: dbbaabacaaab=dbbaabaabaca.

Reduce RHS:

Referenced by [19].

Overlap of [18] dbbaabacaaab=dbb with [14] aaabbaabacd=aaabbaaba:

Critical pair: dbbaabacaaabbaaba=dbbbaabacd.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [20].

Overlap of [10] abaabaca=aabaabac with [19] aabacd=aaba:

Critical pair: abaabacaaba=aabaabacabacd.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [21].

Overlap of [2] bbb=c with [20] bacd=ba:

Critical pair: bbba=cacd.

Reduce LHS:

Flip LHS and RHS.

Referenced by [22], [23].

Overlap of [8] dabaca=aaab with [21] cacd=ca:

Critical pair: dabaca=aaabcd.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [24].

Overlap of [11] dc=1 with [21] cacd=ca:

Critical pair: dca=acd.

Reduce LHS:

Flip LHS and RHS.

Referenced by [31].

Overlap of [16] dbaabaca=dabaabac with [22] aaacbd=aaab:

Critical pair: dbaabacaaab=dabaabacaacbd.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #4.

Referenced by [25], [26], [27], [31], [33], [34], [39].

Overlap of [2] bbb=c with [24] bd=db:

Critical pair: bbdb=cd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #1.

Referenced by [28], [29], [37], [40].

Overlap of [24] bd=db with [6] daabaaba=aaabaabd:

Critical pair: baaabaabd=dbaabaaba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #15.

Referenced by [39].

Overlap of [24] bd=db with [8] dabaca=aaab:

Critical pair: baaab=dbabaca.

Flip LHS and RHS.

Defines rule #9.

Referenced by [34].

Overlap of [25] cd=1 with [8] dabaca=aaab:

Critical pair: caaab=abaca.

Referenced by [30].

Overlap of [25] cd=1 with [16] dbaabaca=dabaabac:

Critical pair: cdabaabac=baabaca.

Reduce LHS:

Flip LHS and RHS.

Defines rule #12.

Referenced by [36], [38].

Overlap of [28] caaab=abaca with [2] bbb=c:

Critical pair: caaac=abacabb.

Referenced by [31].

Overlap of [30] caaac=abacabb with [23] acd=a:

Critical pair: caaa=abacabbd.

Reduce RHS:

Defines rule #6.

Referenced by [32].

Overlap of [5] bc=cb with [31] caaa=abacadbb:

Critical pair: babacadbb=cbaaa.

Flip LHS and RHS.

Defines rule #8.

Referenced by [35].

Simplify [6] daabaaba=aaabaabd.

Reduce RHS:

Defines rule #14.

Overlap of [24] bd=db with [27] dbabaca=baaab:

Critical pair: bbaaab=dbbabaca.

Flip LHS and RHS.

Defines rule #11.

Overlap of [5] bc=cb with [32] cbaaa=babacadbb:

Critical pair: bbabacadbb=cbbaaa.

Flip LHS and RHS.

Defines rule #10.

Overlap of [2] bbb=c with [29] baabaca=abaabac:

Critical pair: bbabaabac=caabaca.

Referenced by [37], [38].

Overlap of [36] bbabaabac=caabaca with [25] cd=1:

Critical pair: bbabaaba=caabacad.

Defines rule #13.

Overlap of [36] bbabaabac=caabaca with [29] baabaca=abaabac:

Critical pair: bbaabaabac=caabacaa.

Referenced by [40].

Overlap of [24] bd=db with [26] dbaabaaba=baaabaadb:

Critical pair: bbaaabaadb=dbbaabaaba.

Flip LHS and RHS.

Referenced by [41].

Overlap of [38] bbaabaabac=caabacaa with [25] cd=1:

Critical pair: bbaabaaba=caabacaad.

Defines rule #17.

Referenced by [41].

Overlap of [39] dbbaabaaba=bbaaabaadb with [40] bbaabaaba=caabacaad:

Critical pair: dcaabacaad=bbaaabaadb.

Reduce LHS:

Flip LHS and RHS.

Referenced by [42].

Overlap of [41] bbaaabaadb=aabacaad with [2] bbb=c:

Critical pair: bbaaabaadc=aabacaadbb.

Reduce LHS:

Defines rule #16.