Certificate for #2973 ⟨a, b | aaabbabbaaa=1⟩

Completion settings:

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

Axiom: aaabbabbaaa=1.

Referenced by [4].

Axiom: aaaaa=c.

Defines rule #5.

Referenced by [5], [6], [10], [12], [13], [21], [25].

Axiom: abb=d.

Referenced by [4], [7], [11], [12].

Overlap of [1] aaabbabbaaa=1 with [3] abb=d:

Critical pair: aadabbaaa=1.

Reduce LHS:

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

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

Critical pair: ac=ca.

Defines rule #2.

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

Overlap of [2] aaaaa=c with [4] aaddaaa=1:

Critical pair: aaa=cddaaa.

Flip LHS and RHS.

Referenced by [10].

Overlap of [4] aaddaaa=1 with [3] abb=d:

Critical pair: aaddaad=bb.

Flip LHS and RHS.

Referenced by [12], [14].

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

Critical pair: aadda=ddaaa.

Referenced by [9], [10], [12], [13], [14].

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

Critical pair: aaddaa=addaaa.

Reduce LHS:

Flip LHS and RHS.

Referenced by [10], [12].

Overlap of [6] cddaaa=aaa with [4] aaddaaa=1:

Critical pair: cdda=aaaddaaa.

Reduce RHS:

Flip LHS and RHS.

Referenced by [11].

Overlap of [10] ddca=cdda with [3] abb=d:

Critical pair: ddcd=cddabb.

Reduce RHS:

Referenced by [12].

Overlap of [3] abb=d with [7] bb=aaddaad:

Critical pair: aaaddaad=d.

Reduce LHS:

Referenced by [15], [16].

Overlap of [4] aaddaaa=1 with [8] aadda=ddaaa:

Critical pair: ddaaaaa=1.

Reduce LHS:

Referenced by [15], [16], [18], [21], [22].

Simplify [7] bb=aaddaad.

Reduce RHS:

Defines rule #8.

Referenced by [19].

Overlap of [12] cddd=d with [13] ddc=1:

Critical pair: cd=dc.

Flip LHS and RHS.

Defines rule #1.

Referenced by [22], [23].

Overlap of [12] cddd=d with [13] ddc=1:

Critical pair: cdd=ddc.

Reduce RHS:

Defines rule #3.

Referenced by [17], [20], [24], [26].

Overlap of [5] ac=ca with [16] cdd=1:

Critical pair: a=cadd.

Flip LHS and RHS.

Referenced by [18].

Overlap of [13] ddc=1 with [17] cadd=a:

Critical pair: dda=add.

Flip LHS and RHS.

Defines rule #4.

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

Overlap of [14] bb=ddaaaad with [14] bb=ddaaaad:

Critical pair: bddaaaad=ddaaaadb.

Flip LHS and RHS.

Referenced by [20], [21].

Overlap of [16] cdd=1 with [19] ddaaaadb=bddaaaad:

Critical pair: cbddaaaad=aaaadb.

Flip LHS and RHS.

Defines rule #7.

Overlap of [18] add=dda with [19] ddaaaadb=bddaaaad:

Critical pair: abddaaaad=ddaaaaadb.

Reduce RHS:

Referenced by [22].

Overlap of [21] abddaaaad=db with [15] dc=cd:

Critical pair: abddaaaacd=dbc.

Reduce LHS:

Referenced by [23].

Overlap of [22] abaaaad=dbc with [15] dc=cd:

Critical pair: abaaaacd=dbcc.

Reduce LHS:

Referenced by [24].

Overlap of [23] abcaaaad=dbcc with [18] add=dda:

Critical pair: abcaaadda=dbccd.

Reduce LHS:

Referenced by [25].

Overlap of [24] abaaaa=dbccd with [2] aaaaa=c:

Critical pair: abc=dbccda.

Referenced by [26].

Overlap of [25] abc=dbccda with [16] cdd=1:

Critical pair: ab=dbccdadd.

Reduce RHS:

Defines rule #6.