Certificate for #1228 ⟨a, b | aabba=abab⟩

Completion settings:

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

Axiom: aabba=abab.

Referenced by [3].

Axiom: abba=c.

Defines rule #2.

Referenced by [3], [4], [5], [6], [8], [10], [11], [12], [13], [15], [18], [19], [20], [21].

Overlap of [1] aabba=abab with [2] abba=c:

Critical pair: ac=abab.

Flip LHS and RHS.

Defines rule #1.

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

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

Critical pair: abbc=cbba.

Defines rule #7.

Overlap of [2] abba=c with [3] abab=ac:

Critical pair: abbac=cbab.

Reduce LHS:

Flip LHS and RHS.

Defines rule #5.

Referenced by [8], [9], [10], [11], [17].

Overlap of [3] abab=ac with [2] abba=c:

Critical pair: abc=acba.

Defines rule #3.

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

Overlap of [3] abab=ac with [3] abab=ac:

Critical pair: abac=acab.

Defines rule #4.

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

Overlap of [5] cbab=cc with [2] abba=c:

Critical pair: cbc=ccba.

Defines rule #8.

Referenced by [14], [15], [16], [17].

Overlap of [5] cbab=cc with [3] abab=ac:

Critical pair: cbac=ccab.

Defines rule #9.

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

Overlap of [7] abac=acab with [5] cbab=cc:

Critical pair: abacc=acabbab.

Reduce LHS:

Reduce RHS:

Defines rule #6.

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

Overlap of [9] cbac=ccab with [5] cbab=cc:

Critical pair: cbacc=ccabbab.

Reduce LHS:

Reduce RHS:

Defines rule #12.

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

Overlap of [7] abac=acab with [10] acacba=accb:

Critical pair: abaccb=acabacba.

Reduce LHS:

Reduce RHS:

Defines rule #10.

Overlap of [9] cbac=ccab with [10] acacba=accb:

Critical pair: cbaccb=ccabacba.

Reduce LHS:

Reduce RHS:

Defines rule #14.

Referenced by [19], [20].

Overlap of [10] acacba=accb with [9] cbac=ccab:

Critical pair: acaccab=accbc.

Reduce RHS:

Flip LHS and RHS.

Defines rule #11.

Referenced by [15], [17].

Overlap of [7] abac=acab with [11] ccacba=cccb:

Critical pair: abacccb=acabcacba.

Reduce LHS:

Reduce RHS:

Defines rule #15.

Referenced by [17], [21].

Overlap of [11] ccacba=cccb with [9] cbac=ccab:

Critical pair: ccaccab=cccbc.

Reduce RHS:

Flip LHS and RHS.

Defines rule #16.

Overlap of [7] abac=acab with [14] acccba=acaccab:

Critical pair: abacaccab=acabccba.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #13.

Referenced by [18], [19].

Overlap of [2] abba=c with [17] acccca=acaccc:

Critical pair: abbacaccc=ccccca.

Reduce LHS:

Flip LHS and RHS.

Defines rule #17.

Referenced by [20].

Overlap of [17] acccca=acaccc with [2] abba=c:

Critical pair: accccc=acacccbba.

Reduce RHS:

Flip LHS and RHS.

Defines rule #18.

Overlap of [18] ccccca=ccaccc with [2] abba=c:

Critical pair: cccccc=ccacccbba.

Reduce RHS:

Flip LHS and RHS.

Defines rule #20.

Overlap of [2] abba=c with [15] acaccabb=acccc:

Critical pair: abbacccc=ccaccabb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #19.