Certificate for #5109 ⟨a, b | aaabbba=baaa⟩

Completion settings:

• Auxiliary generators:
  1. c = bbba
  2. d = ccc
  3. e = dadad
  4. f = eaa
• Reduction order:
  • Right-to-left recursive path with deg(a) = deg(f) = 0, a < f; deg(e) = 1; deg(d) = deg(c) = 2, d < c; deg(b) = 3

Axiom: aaabbba=baaa.

Referenced by [6].

Axiom: bbba=c.

Defines rule #24.

Referenced by [6], [13].

Axiom: ccc=d.

Defines rule #16.

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

Axiom: dadad=e.

Defines rule #14.

Referenced by [8], [9], [11], [14], [16], [27].

Axiom: eaa=f.

Defines rule #4.

Referenced by [10], [15], [16], [17], [18], [25].

Overlap of [1] aaabbba=baaa with [2] bbba=c:

Critical pair: aaac=baaa.

Flip LHS and RHS.

Defines rule #22.

Referenced by [13], [19], [20], [21].

Overlap of [3] ccc=d with [3] ccc=d:

Critical pair: cd=dc.

Flip LHS and RHS.

Defines rule #13.

Referenced by [9], [12].

Overlap of [4] dadad=e with [4] dadad=e:

Critical pair: dae=ead.

Defines rule #9.

Referenced by [10].

Overlap of [4] dadad=e with [7] dc=cd:

Critical pair: dadacd=ec.

Defines rule #17.

Referenced by [11], [12].

Overlap of [8] dae=ead with [5] eaa=f:

Critical pair: daf=eadaa.

Referenced by [15].

Overlap of [9] dadacd=ec with [4] dadad=e:

Critical pair: dadace=ecadad.

Defines rule #15.

Overlap of [9] dadacd=ec with [7] dc=cd:

Critical pair: dadaccd=ecc.

Defines rule #19.

Referenced by [27].

Overlap of [2] bbba=c with [6] baaa=aaac:

Critical pair: bbaaac=caa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #11.

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

Overlap of [3] ccc=d with [13] caa=aaad:

Critical pair: ccaaad=daa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #7.

Referenced by [15], [16], [23], [24].

Simplify [10] daf=eadaa.

Reduce RHS:

Defines rule #8.

Referenced by [22].

Overlap of [4] dadad=e with [14] daa=aaae:

Critical pair: dadaaaae=eaa.

Reduce LHS:

Reduce RHS:

Defines rule #2.

Referenced by [17], [18], [19], [20], [21], [22], [23], [24], [25].

Overlap of [5] eaa=f with [16] aaaffe=f:

Critical pair: ef=faffe.

Defines rule #3.

Referenced by [22], [23], [24], [26], [28], [29].

Overlap of [5] eaa=f with [16] aaaffe=f:

Critical pair: eaf=faaffe.

Defines rule #5.

Referenced by [24], [26], [28], [29].

Overlap of [6] baaa=aaac with [16] aaaffe=f:

Critical pair: bf=aaacffe.

Referenced by [26].

Overlap of [6] baaa=aaac with [16] aaaffe=f:

Critical pair: baf=aaacaffe.

Referenced by [28].

Overlap of [6] baaa=aaac with [16] aaaffe=f:

Critical pair: baaf=aaacaaffe.

Reduce RHS:

Referenced by [29].

Overlap of [13] caa=aaad with [16] aaaffe=f:

Critical pair: cf=aaadaffe.

Reduce RHS:

Defines rule #10.

Referenced by [26].

Overlap of [13] caa=aaad with [16] aaaffe=f:

Critical pair: caf=aaadaaffe.

Reduce RHS:

Defines rule #12.

Referenced by [28].

Overlap of [14] daa=aaae with [16] aaaffe=f:

Critical pair: df=aaaeaffe.

Reduce RHS:

Defines rule #6.

Referenced by [29].

Overlap of [16] aaaffe=f with [5] eaa=f:

Critical pair: aaafff=faa.

Defines rule #1.

Simplify [19] bf=aaacffe.

Reduce RHS:

Defines rule #20.

Overlap of [12] dadaccd=ecc with [4] dadad=e:

Critical pair: dadacce=eccadad.

Defines rule #18.

Simplify [20] baf=aaacaffe.

Reduce RHS:

Defines rule #21.

Simplify [21] baaf=aaaaaadffe.

Reduce RHS:

Defines rule #23.