Certificate for #1297 ⟨a, b | aaaaababba=1⟩

Completion settings:

• Auxiliary generators:
  1. c = aaaaaa
  2. d = babb
• Reduction order:
  • Right-to-left recursive path with deg(c) = deg(d) = deg(a) = 0, c < d < a; deg(b) = 1

Axiom: aaaaababba=1.

Referenced by [4].

Axiom: aaaaaa=c.

Defines rule #5.

Referenced by [6], [7], [15], [18], [20], [23], [25], [26], [30], [33], [36].

Axiom: babb=d.

Defines rule #19.

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

Overlap of [1] aaaaababba=1 with [3] babb=d:

Critical pair: aaaaada=1.

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

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

Critical pair: babd=dabb.

Referenced by [14], [16].

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

Critical pair: ac=ca.

Flip LHS and RHS.

Defines rule #3.

Referenced by [19], [21], [27], [31], [34].

Overlap of [2] aaaaaa=c with [4] aaaaada=1:

Critical pair: a=cda.

Flip LHS and RHS.

Referenced by [9].

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

Critical pair: aaaaad=aaaada.

Flip LHS and RHS.

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

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

Critical pair: cd=aaaaada.

Reduce RHS:

Defines rule #2.

Referenced by [18], [20], [26], [30], [33], [35], [36].

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

Critical pair: aaaaadaaaaad=aaada.

Reduce LHS:

Flip LHS and RHS.

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

Overlap of [8] aaaada=aaaaad with [8] aaaada=aaaaad:

Critical pair: aaaadaaaaad=aaaaadaaada.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

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

Overlap of [11] aada=aaad with [4] aaaaada=1:

Critical pair: aad=aaadaaaada.

Reduce RHS:

Flip LHS and RHS.

Referenced by [15].

Overlap of [11] aada=aaad with [8] aaaada=aaaaad:

Critical pair: aadaaaaad=aaadaaada.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #4.

Referenced by [14], [15], [16], [22], [28], [32].

Overlap of [5] babd=dabb with [13] da=ad:

Critical pair: babad=dabba.

Reduce RHS:

Defines rule #10.

Referenced by [22].

Overlap of [13] da=ad with [2] aaaaaa=c:

Critical pair: dc=adaaaaa.

Reduce RHS:

Defines rule #1.

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

Simplify [5] babd=dabb.

Reduce RHS:

Defines rule #7.

Referenced by [17].

Overlap of [16] babd=adbb with [15] dc=1:

Critical pair: bab=adbbc.

Flip LHS and RHS.

Referenced by [18], [19].

Overlap of [2] aaaaaa=c with [17] adbbc=bab:

Critical pair: aaaaabab=cdbbc.

Reduce RHS:

Flip LHS and RHS.

Defines rule #6.

Referenced by [23].

Overlap of [17] adbbc=bab with [6] ca=ac:

Critical pair: adbbac=baba.

Referenced by [20], [21].

Overlap of [2] aaaaaa=c with [19] adbbac=baba:

Critical pair: aaaaababa=cdbbac.

Reduce RHS:

Flip LHS and RHS.

Defines rule #9.

Overlap of [19] adbbac=baba with [6] ca=ac:

Critical pair: adbbaac=babaa.

Referenced by [26], [27].

Overlap of [14] babad=adbba with [13] da=ad:

Critical pair: babaad=adbbaa.

Defines rule #12.

Referenced by [28].

Overlap of [3] babb=d with [18] bbc=aaaaabab:

Critical pair: baaaaaabab=dc.

Reduce LHS:

Reduce RHS:

Referenced by [24].

Overlap of [23] bcbab=1 with [23] bcbab=1:

Critical pair: bcba=cbab.

Defines rule #8.

Referenced by [25].

Overlap of [24] bcba=cbab with [2] aaaaaa=c:

Critical pair: bcbc=cbabaaaaa.

Flip LHS and RHS.

Referenced by [29].

Overlap of [2] aaaaaa=c with [21] adbbaac=babaa:

Critical pair: aaaaababaa=cdbbaac.

Reduce RHS:

Flip LHS and RHS.

Defines rule #11.

Overlap of [21] adbbaac=babaa with [6] ca=ac:

Critical pair: adbbaaac=babaaa.

Referenced by [30], [31].

Overlap of [22] babaad=adbbaa with [13] da=ad:

Critical pair: babaaad=adbbaaa.

Defines rule #14.

Referenced by [32].

Overlap of [15] dc=1 with [25] cbabaaaaa=bcbc:

Critical pair: dbcbc=babaaaaa.

Flip LHS and RHS.

Defines rule #18.

Referenced by [34].

Overlap of [2] aaaaaa=c with [27] adbbaaac=babaaa:

Critical pair: aaaaababaaa=cdbbaaac.

Reduce RHS:

Flip LHS and RHS.

Defines rule #13.

Overlap of [27] adbbaaac=babaaa with [6] ca=ac:

Critical pair: adbbaaaac=babaaaa.

Referenced by [33], [34].

Overlap of [28] babaaad=adbbaaa with [13] da=ad:

Critical pair: babaaaad=adbbaaaa.

Defines rule #16.

Overlap of [2] aaaaaa=c with [31] adbbaaaac=babaaaa:

Critical pair: aaaaababaaaa=cdbbaaaac.

Reduce RHS:

Flip LHS and RHS.

Defines rule #15.

Overlap of [31] adbbaaaac=babaaaa with [6] ca=ac:

Critical pair: adbbaaaaac=babaaaaa.

Reduce RHS:

Referenced by [35].

Overlap of [34] adbbaaaaac=dbcbc with [9] cd=1:

Critical pair: adbbaaaaa=dbcbcd.

Reduce RHS:

Referenced by [36].

Overlap of [2] aaaaaa=c with [35] adbbaaaaa=dbcb:

Critical pair: aaaaadbcb=cdbbaaaaa.

Reduce RHS:

Flip LHS and RHS.

Defines rule #17.