Certificate for #2827 ⟨a, b | aaaaabbaaba=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. bbaab=d

Axiom: aaaaabbaaba=1.

Referenced by [4].

Axiom: aaaaaa=c.

Defines rule #5.

Referenced by [6], [7], [8], [11], [15], [17], [23], [25], [27], [33].

Axiom: bbaab=d.

Defines rule #17.

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

Overlap of [1] aaaaabbaaba=1 with [3] bbaab=d:

Critical pair: aaaaada=1.

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

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

Critical pair: bbaad=dbaab.

Flip LHS and RHS.

Referenced by [19].

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

Critical pair: ac=ca.

Defines rule #3.

Referenced by [24], [28], [31].

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], [12].

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

Critical pair: cd=aaaaada.

Reduce RHS:

Flip LHS and RHS.

Referenced by [12], [13].

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

Critical pair: cad=aaaaaada.

Reduce RHS:

Referenced by [18].

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

Critical pair: aaaadaa=1.

Reduce LHS:

Defines rule #1.

Referenced by [13], [15], [17], [20], [25], [29].

Simplify [10] aaaadaa=cd.

Reduce RHS:

Referenced by [14], [16].

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

Critical pair: aaaad=aadaa.

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

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

Critical pair: aaaadaa=cd.

Reduce LHS:

Reduce RHS:

Referenced by [16].

Overlap of [13] aaaadaa=1 with [14] aaaad=aadaa:

Critical pair: aaaadaadaa=aad.

Reduce LHS:

Flip LHS and RHS.

Referenced by [17], [19], [21].

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

Critical pair: aaaadaa=cd.

Reduce LHS:

Reduce RHS:

Defines rule #2.

Referenced by [18], [23], [32], [33].

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

Critical pair: da=ad.

Flip LHS and RHS.

Defines rule #4.

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

Simplify [5] dbaab=bbaad.

Reduce RHS:

Defines rule #7.

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

Overlap of [12] cd=1 with [19] dbaab=bbdaa:

Critical pair: cbbdaa=baab.

Referenced by [23].

Overlap of [16] aad=daa with [19] dbaab=bbdaa:

Critical pair: aabbdaa=daabaab.

Flip LHS and RHS.

Defines rule #12.

Referenced by [30].

Overlap of [18] ad=da with [19] dbaab=bbdaa:

Critical pair: abbdaa=dabaab.

Flip LHS and RHS.

Defines rule #9.

Overlap of [20] cbbdaa=baab with [2] aaaaaa=c:

Critical pair: cbbdc=baabaaaa.

Reduce LHS:

Defines rule #6.

Referenced by [24], [25].

Overlap of [6] ac=ca with [23] cbb=baabaaaa:

Critical pair: abaabaaaa=cabb.

Flip LHS and RHS.

Defines rule #8.

Referenced by [28].

Overlap of [23] cbb=baabaaaa with [3] bbaab=d:

Critical pair: cd=baabaaaaaab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [26].

Overlap of [25] baabcb=1 with [25] baabcb=1:

Critical pair: baabc=aabcb.

Flip LHS and RHS.

Defines rule #10.

Referenced by [27].

Overlap of [2] aaaaaa=c with [26] aabcb=baabc:

Critical pair: aaaabaabc=cbcb.

Referenced by [29].

Overlap of [6] ac=ca with [24] cabb=abaabaaaa:

Critical pair: aabaabaaaa=caabb.

Flip LHS and RHS.

Defines rule #11.

Referenced by [31].

Overlap of [27] aaaabaabc=cbcb with [12] cd=1:

Critical pair: aaaabaab=cbcbd.

Defines rule #16.

Referenced by [32].

Overlap of [18] ad=da with [21] daabaab=aabbdaa:

Critical pair: aaabbdaa=daaabaab.

Flip LHS and RHS.

Defines rule #14.

Referenced by [32].

Overlap of [6] ac=ca with [28] caabb=aabaabaaaa:

Critical pair: aaabaabaaaa=caaabb.

Flip LHS and RHS.

Defines rule #13.

Overlap of [18] ad=da with [30] daaabaab=aaabbdaa:

Critical pair: aaaabbdaa=daaaabaab.

Reduce RHS:

Referenced by [33].

Overlap of [32] aaaabbdaa=bcbd with [2] aaaaaa=c:

Critical pair: aaaabbdc=bcbdaaaa.

Reduce LHS:

Defines rule #15.