Certificate for #2865 ⟨a, b | aaaababbaba=1⟩

Completion settings:

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

Axiom: aaaababbaba=1.

Referenced by [4].

Axiom: aaaaa=c.

Defines rule #2.

Referenced by [5], [6], [7], [10], [16], [18], [19], [34], [36], [39], [46].

Axiom: babbab=d.

Referenced by [4], [11], [12], [32].

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

Critical pair: aaaada=1.

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

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

Critical pair: ac=ca.

Defines rule #1.

Referenced by [26], [27], [29], [37].

Overlap of [2] aaaaa=c with [4] aaaada=1:

Critical pair: a=cda.

Flip LHS and RHS.

Referenced by [9], [10].

Overlap of [2] aaaaa=c with [4] aaaada=1:

Critical pair: aa=cada.

Flip LHS and RHS.

Referenced by [10].

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

Critical pair: aaaad=aaada.

Referenced by [9], [13].

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

Critical pair: cd=aaaada.

Reduce RHS:

Flip LHS and RHS.

Referenced by [13], [14].

Overlap of [7] cada=aa with [4] aaaada=1:

Critical pair: cad=aaaaada.

Reduce RHS:

Referenced by [21].

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

Critical pair: babd=dbab.

Flip LHS and RHS.

Defines rule #11.

Referenced by [22], [23].

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

Critical pair: babbad=dabbab.

Flip LHS and RHS.

Referenced by [24].

Overlap of [4] aaaada=1 with [8] aaaad=aaada:

Critical pair: aaadaa=1.

Reduce LHS:

Defines rule #4.

Referenced by [14], [16], [20], [22], [31], [47].

Simplify [9] aaadaa=cd.

Reduce RHS:

Referenced by [15], [17].

Overlap of [14] aaadaa=1 with [14] aaadaa=1:

Critical pair: aaad=adaa.

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

Overlap of [2] aaaaa=c with [15] aaad=adaa:

Critical pair: aaadaa=cd.

Reduce LHS:

Reduce RHS:

Referenced by [17], [18].

Overlap of [14] aaadaa=1 with [16] adaaaa=1:

Critical pair: aaada=daaaa.

Reduce LHS:

Referenced by [18].

Overlap of [15] aaad=adaa with [16] adaaaa=1:

Critical pair: aa=adaaaaaa.

Reduce RHS:

Flip LHS and RHS.

Referenced by [19].

Overlap of [18] dcaa=aa with [2] aaaaa=c:

Critical pair: dcc=aaaaa.

Reduce RHS:

Referenced by [20].

Overlap of [19] dcc=c with [13] cd=1:

Critical pair: dc=cd.

Reduce RHS:

Defines rule #3.

Referenced by [21], [25], [32], [33], [34], [36], [39].

Overlap of [20] dc=1 with [10] cad=a:

Critical pair: da=ad.

Flip LHS and RHS.

Defines rule #5.

Referenced by [23], [24], [28], [30], [38], [47].

Overlap of [13] cd=1 with [11] dbab=babd:

Critical pair: cbabd=bab.

Referenced by [25].

Overlap of [21] ad=da with [11] dbab=babd:

Critical pair: ababd=dabab.

Flip LHS and RHS.

Defines rule #12.

Referenced by [28].

Simplify [12] dabbab=babbad.

Reduce RHS:

Referenced by [31], [35].

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

Critical pair: cbab=babc.

Defines rule #6.

Referenced by [26], [31], [32].

Overlap of [5] ac=ca with [25] cbab=babc:

Critical pair: ababc=cabab.

Flip LHS and RHS.

Defines rule #7.

Referenced by [27].

Overlap of [5] ac=ca with [26] cabab=ababc:

Critical pair: aababc=caabab.

Flip LHS and RHS.

Defines rule #8.

Referenced by [29].

Overlap of [21] ad=da with [23] dabab=ababd:

Critical pair: aababd=daabab.

Flip LHS and RHS.

Defines rule #13.

Referenced by [30].

Overlap of [5] ac=ca with [27] caabab=aababc:

Critical pair: aaababc=caaabab.

Flip LHS and RHS.

Defines rule #9.

Referenced by [37].

Overlap of [21] ad=da with [28] daabab=aababd:

Critical pair: aaababd=daaabab.

Flip LHS and RHS.

Defines rule #14.

Referenced by [38].

Overlap of [13] cd=1 with [24] dabbab=babbda:

Critical pair: cbabbda=abbab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #16.

Referenced by [32].

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

Critical pair: cbbabcbda=babcbab.

Reduce RHS:

Referenced by [33], [34], [35].

Overlap of [20] dc=1 with [32] cbbabcbda=1:

Critical pair: d=bbabcbda.

Flip LHS and RHS.

Referenced by [36].

Overlap of [32] cbbabcbda=1 with [2] aaaaa=c:

Critical pair: cbbabcbdc=aaaa.

Reduce LHS:

Referenced by [35].

Overlap of [32] cbbabcbda=1 with [24] dabbab=babbda:

Critical pair: cbbabcbbabbda=bbab.

Reduce LHS:

Referenced by [39], [40].

Overlap of [33] bbabcbda=d with [2] aaaaa=c:

Critical pair: bbabcbdc=daaaa.

Reduce LHS:

Defines rule #24.

Overlap of [5] ac=ca with [29] caaabab=aaababc:

Critical pair: aaaababc=caaaabab.

Flip LHS and RHS.

Defines rule #10.

Referenced by [41], [42], [43], [44], [45].

Overlap of [21] ad=da with [30] daaabab=aaababd:

Critical pair: aaaababd=daaaabab.

Flip LHS and RHS.

Defines rule #15.

Referenced by [40].

Overlap of [35] aaaababbda=bbab with [2] aaaaa=c:

Critical pair: aaaababbdc=bbabaaaa.

Reduce LHS:

Defines rule #17.

Referenced by [41].

Overlap of [38] daaaabab=aaaababd with [35] aaaababbda=bbab:

Critical pair: dbbab=aaaababdbda.

Defines rule #23.

Overlap of [37] caaaabab=aaaababc with [39] aaaababb=bbabaaaa:

Critical pair: cbbabaaaa=aaaababcb.

Flip LHS and RHS.

Defines rule #18.

Referenced by [42].

Overlap of [37] caaaabab=aaaababc with [41] aaaababcb=cbbabaaaa:

Critical pair: ccbbabaaaa=aaaababccb.

Flip LHS and RHS.

Defines rule #19.

Referenced by [43].

Overlap of [37] caaaabab=aaaababc with [42] aaaababccb=ccbbabaaaa:

Critical pair: cccbbabaaaa=aaaababcccb.

Flip LHS and RHS.

Defines rule #20.

Referenced by [44].

Overlap of [37] caaaabab=aaaababc with [43] aaaababcccb=cccbbabaaaa:

Critical pair: ccccbbabaaaa=aaaababccccb.

Flip LHS and RHS.

Defines rule #21.

Referenced by [45].

Overlap of [37] caaaabab=aaaababc with [44] aaaababccccb=ccccbbabaaaa:

Critical pair: cccccbbabaaaa=aaaababcccccb.

Referenced by [46].

Overlap of [45] cccccbbabaaaa=aaaababcccccb with [2] aaaaa=c:

Critical pair: cccccbbabc=aaaababcccccba.

Referenced by [47].

Overlap of [46] cccccbbabc=aaaababcccccba with [13] cd=1:

Critical pair: cccccbbab=aaaababcccccbad.

Reduce RHS:

Defines rule #22.