Certificate for #1360 ⟨a, b | aaababbaba=1⟩

Completion settings:

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

Axiom: aaababbaba=1.

Referenced by [4].

Axiom: aaaa=c.

Defines rule #5.

Referenced by [5], [6], [13], [23], [32], [34].

Axiom: babbab=d.

Referenced by [4], [9], [10], [20].

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

Critical pair: aaada=1.

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

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

Critical pair: ac=ca.

Flip LHS and RHS.

Defines rule #1.

Referenced by [17], [19], [25], [26], [27], [30].

Overlap of [2] aaaa=c with [4] aaada=1:

Critical pair: a=cda.

Flip LHS and RHS.

Referenced by [8].

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

Critical pair: aaad=aada.

Flip LHS and RHS.

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

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

Critical pair: cd=aaada.

Reduce RHS:

Defines rule #2.

Referenced by [14], [17], [24], [25], [34].

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

Critical pair: babd=dbab.

Flip LHS and RHS.

Defines rule #7.

Referenced by [14], [18], [25], [28], [29], [31], [33].

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

Critical pair: babbad=dabbab.

Flip LHS and RHS.

Referenced by [15].

Overlap of [4] aaada=1 with [7] aada=aaad:

Critical pair: aaadaaad=ada.

Reduce LHS:

Flip LHS and RHS.

Referenced by [13].

Overlap of [7] aada=aaad with [7] aada=aaad:

Critical pair: aadaaad=aaadada.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #3.

Referenced by [13], [15], [18], [28], [29], [31], [33].

Overlap of [12] da=ad with [2] aaaa=c:

Critical pair: dc=adaaa.

Reduce RHS:

Defines rule #4.

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

Overlap of [8] cd=1 with [9] dbab=babd:

Critical pair: cbabd=bab.

Referenced by [16].

Overlap of [10] dabbab=babbad with [12] da=ad:

Critical pair: adbbab=babbad.

Defines rule #10.

Referenced by [17], [18].

Overlap of [14] cbabd=bab with [13] dc=1:

Critical pair: cbab=babc.

Defines rule #6.

Referenced by [17], [19], [20], [26], [27], [30].

Overlap of [5] ca=ac with [15] adbbab=babbad:

Critical pair: cbabbad=acdbbab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #8.

Referenced by [19], [20].

Overlap of [12] da=ad with [15] adbbab=babbad:

Critical pair: dbabbad=addbbab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #17.

Referenced by [29].

Overlap of [5] ca=ac with [17] abbab=babcbad:

Critical pair: cbabcbad=acbbab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #9.

Referenced by [26].

Overlap of [16] cbab=babc with [17] abbab=babcbad:

Critical pair: cbbabcbad=babcbab.

Reduce RHS:

Referenced by [21].

Overlap of [13] dc=1 with [20] cbbabcbad=1:

Critical pair: d=bbabcbad.

Flip LHS and RHS.

Referenced by [22].

Overlap of [21] bbabcbad=d with [13] dc=1:

Critical pair: bbabcba=dc.

Reduce RHS:

Referenced by [23].

Overlap of [22] bbabcba=1 with [2] aaaa=c:

Critical pair: bbabcbc=aaa.

Referenced by [24].

Overlap of [23] bbabcbc=aaa with [8] cd=1:

Critical pair: bbabcb=aaad.

Defines rule #20.

Referenced by [25].

Overlap of [24] bbabcb=aaad with [24] bbabcb=aaad:

Critical pair: bbabcaaad=aaadbabcb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #11.

Referenced by [27], [28].

Overlap of [5] ca=ac with [19] acbbab=babccbad:

Critical pair: cbabccbad=accbbab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #16.

Referenced by [32].

Overlap of [5] ca=ac with [25] aaababb=bbabaaa:

Critical pair: cbbabaaa=acaababb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #12.

Referenced by [30].

Overlap of [12] da=ad with [25] aaababb=bbabaaa:

Critical pair: dbbabaaa=adaababb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #13.

Referenced by [31].

Overlap of [12] da=ad with [18] addbbab=babdbad:

Critical pair: dbabdbad=adddbbab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [33].

Overlap of [5] ca=ac with [27] aaababcb=cbbabaaa:

Critical pair: ccbbabaaa=acaababcb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #14.

Overlap of [12] da=ad with [28] aaababdb=dbbabaaa:

Critical pair: ddbbabaaa=adaababdb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #15.

Overlap of [2] aaaa=c with [26] accbbab=babcccbad:

Critical pair: aaababcccbad=cccbbab.

Flip LHS and RHS.

Defines rule #18.

Overlap of [12] da=ad with [29] adddbbab=babddbad:

Critical pair: dbabddbad=addddbbab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [34].

Overlap of [2] aaaa=c with [33] addddbbab=babdddbad:

Critical pair: aaababdddbad=cddddbbab.

Reduce RHS:

Flip LHS and RHS.

Defines rule #19.