Certificate for #1131 ⟨a, b | abbaab=aba⟩

Completion settings:

• Auxiliary generators:
  1. c = aabaab
• Reduction order:
  • Left-to-right shortlex with a < b < c

Axiom: abbaab=aba.

Defines rule #18.

Referenced by [4], [5], [6], [7], [9], [19], [20], [25].

Axiom: aabaab=c.

Defines rule #15.

Referenced by [3], [5], [6], [8], [9], [10], [19].

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

Critical pair: aabc=caab.

Flip LHS and RHS.

Defines rule #6.

Referenced by [9], [12], [13], [16], [24].

Overlap of [1] abbaab=aba with [1] abbaab=aba:

Critical pair: abbaaba=ababaab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #20.

Referenced by [19], [21], [23].

Overlap of [1] abbaab=aba with [2] aabaab=c:

Critical pair: abbc=abaaab.

Flip LHS and RHS.

Referenced by [22].

Overlap of [2] aabaab=c with [1] abbaab=aba:

Critical pair: aabaaba=cbaab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #14.

Referenced by [7], [8], [12], [16].

Overlap of [6] cbaab=ca with [1] abbaab=aba:

Critical pair: cbaaba=cabaab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #19.

Referenced by [9], [10], [16].

Overlap of [6] cbaab=ca with [2] aabaab=c:

Critical pair: cbc=caaab.

Flip LHS and RHS.

Referenced by [11].

Overlap of [7] cabaab=caa with [1] abbaab=aba:

Critical pair: cabaaba=caabaab.

Reduce LHS:

Reduce RHS:

Defines rule #5.

Referenced by [10], [11], [14].

Overlap of [7] cabaab=caa with [2] aabaab=c:

Critical pair: cabc=caaaab.

Reduce RHS:

Flip LHS and RHS.

Referenced by [15].

Overlap of [8] caaab=cbc with [9] caaa=cc:

Critical pair: ccb=cbc.

Defines rule #2.

Referenced by [12].

Overlap of [11] ccb=cbc with [6] cbaab=ca:

Critical pair: cca=cbcaab.

Reduce RHS:

Defines rule #1.

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

Overlap of [12] cca=cac with [3] caab=aabc:

Critical pair: caabc=cacab.

Reduce LHS:

Flip LHS and RHS.

Referenced by [17].

Overlap of [12] cca=cac with [9] caaa=cc:

Critical pair: ccc=cacaa.

Flip LHS and RHS.

Referenced by [18].

Simplify [10] ccab=cabc.

Reduce LHS:

Defines rule #8.

Referenced by [16].

Overlap of [15] cacb=cabc with [6] cbaab=ca:

Critical pair: caca=cabcaab.

Reduce RHS:

Defines rule #7.

Referenced by [17], [18].

Overlap of [13] cacab=aabcc with [16] caca=caac:

Critical pair: caacb=aabcc.

Defines rule #13.

Overlap of [14] cacaa=ccc with [16] caca=caac:

Critical pair: caaca=ccc.

Defines rule #12.

Overlap of [1] abbaab=aba with [4] ababaab=abaa:

Critical pair: abbaabaa=abaabaab.

Reduce LHS:

Reduce RHS:

Defines rule #9.

Referenced by [20], [21], [22], [23].

Overlap of [1] abbaab=aba with [19] abaaa=abc:

Critical pair: abbaabc=abaaaa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #3.

Referenced by [21], [23], [24].

Overlap of [4] ababaab=abaa with [19] abaaa=abc:

Critical pair: ababaabc=abaaaaa.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #10.

Referenced by [24].

Overlap of [5] abaaab=abbc with [19] abaaa=abc:

Critical pair: abcb=abbc.

Defines rule #4.

Referenced by [25].

Overlap of [4] ababaab=abaa with [20] abca=abac:

Critical pair: ababaabac=abaaca.

Reduce LHS:

Flip LHS and RHS.

Defines rule #16.

Overlap of [20] abca=abac with [3] caab=aabc:

Critical pair: abaabc=abacab.

Reduce RHS:

Flip LHS and RHS.

Defines rule #17.

Overlap of [1] abbaab=aba with [22] abcb=abbc:

Critical pair: abbaabbc=abacb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #11.