Certificate for #1729 ⟨a, b | aabbbaaab=a⟩

Completion settings:

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

Axiom: aabbbaaab=a.

Referenced by [3].

Axiom: aaa=c.

Referenced by [3], [4], [5], [6], [8].

Overlap of [1] aabbbaaab=a with [2] aaa=c:

Critical pair: aabbbcb=a.

Referenced by [5], [6], [7], [9].

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

Critical pair: ac=ca.

Flip LHS and RHS.

Referenced by [6], [7].

Overlap of [2] aaa=c with [3] aabbbcb=a:

Critical pair: aa=cbbbcb.

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

Overlap of [2] aaa=c with [3] aabbbcb=a:

Critical pair: aaa=cabbbcb.

Reduce LHS:

Reduce RHS:

Referenced by [8].

Overlap of [4] ca=ac with [3] aabbbcb=a:

Critical pair: ca=acabbbcb.

Reduce LHS:

Reduce RHS:

Referenced by [8], [10].

Overlap of [2] aaa=c with [5] aa=cbbbcb:

Critical pair: cbbbcba=c.

Reduce LHS:

Referenced by [11].

Overlap of [3] aabbbcb=a with [5] aa=cbbbcb:

Critical pair: cbbbcbbbbcb=a.

Flip LHS and RHS.

Defines rule #10.

Referenced by [10].

Simplify [7] ac=cbbbcbcbbbcb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #5.

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

Simplify [8] cbbbcbcbbbcbbbbcb=c.

Reduce LHS:

Defines rule #9.

Referenced by [12], [13], [14], [15], [16], [17], [18].

Overlap of [10] cbbbcbcbbbcb=cbbbcbbbbcbc with [11] cbbbcbbbbcbcbbbcb=c:

Critical pair: cbbbcbc=cbbbcbbbbcbcbbbcbcbbbcb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #1.

Overlap of [11] cbbbcbbbbcbcbbbcb=c with [10] cbbbcbcbbbcb=cbbbcbbbbcbc:

Critical pair: cbbbcbbbbcbcbbbcbbbcbbbbcbc=cbbcbcbbbcb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #4.

Referenced by [15].

Overlap of [11] cbbbcbbbbcbcbbbcb=c with [11] cbbbcbbbbcbcbbbcb=c:

Critical pair: cbbbcbbbbcbcbbbc=cbbcbbbbcbcbbbcb.

Flip LHS and RHS.

Defines rule #8.

Referenced by [17], [18].

Overlap of [11] cbbbcbbbbcbcbbbcb=c with [13] cbbcbcbbbcb=cbbcbbbbcbc:

Critical pair: cbbbcbbbbcbcbbbcbbcbbbbcbc=cbcbcbbbcb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #3.

Referenced by [16].

Overlap of [11] cbbbcbbbbcbcbbbcb=c with [15] cbcbcbbbcb=cbcbbbbcbc:

Critical pair: cbbbcbbbbcbcbbbcbcbbbbcbc=ccbcbbbcb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #2.

Overlap of [11] cbbbcbbbbcbcbbbcb=c with [14] cbbcbbbbcbcbbbcb=cbbbcbbbbcbcbbbc:

Critical pair: cbbbcbbbbcbcbbbcbbbcbbbbcbcbbbc=cbcbbbbcbcbbbcb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #7.

Overlap of [14] cbbcbbbbcbcbbbcb=cbbbcbbbbcbcbbbc with [14] cbbcbbbbcbcbbbcb=cbbbcbbbbcbcbbbc:

Critical pair: cbbcbbbbcbcbbbcbbbcbbbbcbcbbbc=cbbbcbbbbcbcbbbcbcbbbbcbcbbbcb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #6.