Certificate for #3085 ⟨a, b | aababbbaaba=1⟩

Completion settings:

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

Axiom: aababbbaaba=1.

Referenced by [4].

Axiom: bbb=c.

Defines rule #2.

Referenced by [4], [5], [18], [24], [26], [31], [33].

Axiom: aabaaaba=d.

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

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

Critical pair: aabacaaba=1.

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

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

Critical pair: bc=cb.

Defines rule #1.

Referenced by [11], [12], [21].

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

Critical pair: aabad=daaba.

Flip LHS and RHS.

Defines rule #9.

Referenced by [16].

Overlap of [4] aabacaaba=1 with [3] aabaaaba=d:

Critical pair: aabacd=aaba.

Referenced by [10].

Overlap of [4] aabacaaba=1 with [3] aabaaaba=d:

Critical pair: aabacaabd=abaaaba.

Flip LHS and RHS.

Referenced by [13], [14].

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

Critical pair: aabac=caaba.

Flip LHS and RHS.

Defines rule #6.

Referenced by [12], [14].

Overlap of [4] aabacaaba=1 with [7] aabacd=aaba:

Critical pair: aabacaaba=cd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #4.

Referenced by [11], [19], [23], [27].

Overlap of [5] bc=cb with [10] cd=1:

Critical pair: b=cbd.

Flip LHS and RHS.

Referenced by [15].

Overlap of [5] bc=cb with [9] caaba=aabac:

Critical pair: baabac=cbaaba.

Flip LHS and RHS.

Defines rule #7.

Referenced by [21].

Overlap of [3] aabaaaba=d with [8] abaaaba=aabacaabd:

Critical pair: aaabacaabd=d.

Referenced by [14], [17].

Overlap of [4] aabacaaba=1 with [9] caaba=aabac:

Critical pair: aabaaabac=1.

Reduce LHS:

Defines rule #3.

Referenced by [15], [18], [24], [25], [31], [33].

Overlap of [14] dc=1 with [11] cbd=b:

Critical pair: db=bd.

Flip LHS and RHS.

Defines rule #5.

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

Overlap of [15] bd=db with [6] daaba=aabad:

Critical pair: baabad=dbaaba.

Flip LHS and RHS.

Defines rule #10.

Referenced by [22].

Simplify [13] aaabacaabd=d.

Reduce LHS:

Referenced by [18].

Overlap of [17] aaabacaadb=d with [2] bbb=c:

Critical pair: aaabacaadc=dbb.

Reduce LHS:

Defines rule #19.

Referenced by [19], [20].

Overlap of [18] aaabacaa=dbb with [18] aaabacaa=dbb:

Critical pair: aaabacdbb=dbbabacaa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [23], [24].

Overlap of [18] aaabacaa=dbb with [18] aaabacaa=dbb:

Critical pair: aaabacadbb=dbbaabacaa.

Flip LHS and RHS.

Referenced by [25].

Overlap of [5] bc=cb with [12] cbaaba=baabac:

Critical pair: bbaabac=cbbaaba.

Flip LHS and RHS.

Defines rule #8.

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

Overlap of [15] bd=db with [16] dbaaba=baabad:

Critical pair: bbaabad=dbbaaba.

Flip LHS and RHS.

Defines rule #11.

Referenced by [25], [29].

Overlap of [10] cd=1 with [19] dbbabacaa=aaababb:

Critical pair: caaababb=bbabacaa.

Flip LHS and RHS.

Defines rule #13.

Overlap of [15] bd=db with [19] dbbabacaa=aaababb:

Critical pair: baaababb=dbbbabacaa.

Reduce RHS:

Referenced by [26].

Overlap of [20] dbbaabacaa=aaabacadbb with [22] dbbaaba=bbaabad:

Critical pair: bbaabadcaa=aaabacadbb.

Reduce LHS:

Defines rule #14.

Referenced by [28], [29].

Overlap of [24] baaababb=abacaa with [2] bbb=c:

Critical pair: baaabac=abacaab.

Referenced by [27].

Overlap of [26] baaabac=abacaab with [10] cd=1:

Critical pair: baaaba=abacaabd.

Reduce RHS:

Defines rule #12.

Overlap of [21] cbbaaba=bbaabac with [25] bbaabaaa=aaabacadbb:

Critical pair: caaabacadbb=bbaabacaa.

Flip LHS and RHS.

Defines rule #15.

Referenced by [30].

Overlap of [22] dbbaaba=bbaabad with [25] bbaabaaa=aaabacadbb:

Critical pair: daaabacadbb=bbaabadaa.

Referenced by [31].

Overlap of [21] cbbaaba=bbaabac with [28] bbaabacaa=caaabacadbb:

Critical pair: ccaaabacadbb=bbaabaccaa.

Flip LHS and RHS.

Defines rule #16.

Referenced by [32].

Overlap of [29] daaabacadbb=bbaabadaa with [2] bbb=c:

Critical pair: daaabacadc=bbaabadaab.

Reduce LHS:

Defines rule #18.

Overlap of [21] cbbaaba=bbaabac with [30] bbaabaccaa=ccaaabacadbb:

Critical pair: cccaaabacadbb=bbaabacccaa.

Referenced by [33].

Overlap of [32] cccaaabacadbb=bbaabacccaa with [2] bbb=c:

Critical pair: cccaaabacadc=bbaabacccaab.

Reduce LHS:

Defines rule #17.