Certificate for #2675 ⟨a, b | abaab=aabba⟩

Completion settings:

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

Axiom: abaab=aabba.

Referenced by [4].

Axiom: babba=c.

Defines rule #24.

Referenced by [5], [6], [9], [11], [13], [15], [19], [21], [24], [29].

Axiom: baa=d.

Defines rule #23.

Referenced by [4], [6], [7], [8], [10], [12], [14], [16], [23], [25].

Overlap of [1] abaab=aabba with [3] baa=d:

Critical pair: adb=aabba.

Flip LHS and RHS.

Defines rule #27.

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

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

Critical pair: babc=cbba.

Flip LHS and RHS.

Defines rule #8.

Overlap of [2] babba=c with [3] baa=d:

Critical pair: babd=ca.

Flip LHS and RHS.

Defines rule #7.

Referenced by [11], [19], [21], [29].

Overlap of [3] baa=d with [4] aabba=adb:

Critical pair: badb=dbba.

Flip LHS and RHS.

Defines rule #9.

Referenced by [13], [18], [19], [20], [21], [22], [26], [27], [28].

Overlap of [3] baa=d with [4] aabba=adb:

Critical pair: baadb=dabba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #25.

Referenced by [21], [24].

Overlap of [4] aabba=adb with [2] babba=c:

Critical pair: aabc=adbbba.

Flip LHS and RHS.

Defines rule #20.

Referenced by [29].

Overlap of [4] aabba=adb with [3] baa=d:

Critical pair: aabd=adba.

Flip LHS and RHS.

Defines rule #19.

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

Overlap of [2] babba=c with [10] adba=aabd:

Critical pair: babbaabd=cdba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #10.

Referenced by [19].

Overlap of [3] baa=d with [10] adba=aabd:

Critical pair: baaabd=ddba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #12.

Referenced by [21], [23].

Overlap of [10] adba=aabd with [2] babba=c:

Critical pair: adc=aabdbba.

Reduce RHS:

Flip LHS and RHS.

Defines rule #5.

Referenced by [15], [16], [17], [18], [20], [22], [26].

Overlap of [10] adba=aabd with [3] baa=d:

Critical pair: add=aabda.

Flip LHS and RHS.

Defines rule #28.

Referenced by [25].

Overlap of [2] babba=c with [13] adbdb=adc:

Critical pair: babbadc=cdbdb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #1.

Referenced by [19], [20], [27].

Overlap of [3] baa=d with [13] adbdb=adc:

Critical pair: baadc=ddbdb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #2.

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

Overlap of [4] aabba=adb with [13] adbdb=adc:

Critical pair: aabbadc=adbdbdb.

Reduce LHS:

Reduce RHS:

Defines rule #6.

Overlap of [13] adbdb=adc with [7] dbba=badb:

Critical pair: adbbadb=adcba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #21.

Overlap of [15] cdbdb=cdc with [2] babba=c:

Critical pair: cdbdc=cdcabba.

Reduce RHS:

Defines rule #3.

Overlap of [15] cdbdb=cdc with [7] dbba=badb:

Critical pair: cdbbadb=cdcba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #15.

Overlap of [16] ddbdb=ddc with [2] babba=c:

Critical pair: ddbdc=ddcabba.

Reduce RHS:

Defines rule #4.

Overlap of [16] ddbdb=ddc with [7] dbba=badb:

Critical pair: ddbbadb=ddcba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #16.

Overlap of [12] ddba=dabd with [3] baa=d:

Critical pair: ddd=dabda.

Flip LHS and RHS.

Defines rule #26.

Overlap of [8] dabba=ddb with [2] babba=c:

Critical pair: dabc=ddbbba.

Flip LHS and RHS.

Defines rule #13.

Overlap of [3] baa=d with [14] aabda=add:

Critical pair: badd=dbda.

Flip LHS and RHS.

Defines rule #14.

Referenced by [26], [27], [28].

Overlap of [13] adbdb=adc with [25] dbda=badd:

Critical pair: adbbadd=adcda.

Reduce LHS:

Flip LHS and RHS.

Defines rule #22.

Overlap of [15] cdbdb=cdc with [25] dbda=badd:

Critical pair: cdbbadd=cdcda.

Reduce LHS:

Flip LHS and RHS.

Defines rule #17.

Overlap of [16] ddbdb=ddc with [25] dbda=badd:

Critical pair: ddbbadd=ddcda.

Reduce LHS:

Flip LHS and RHS.

Defines rule #18.

Overlap of [2] babba=c with [9] adbbba=aabc:

Critical pair: babbaabc=cdbbba.

Reduce LHS:

Flip LHS and RHS.

Defines rule #11.