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

Completion settings:

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

Axiom: aaabbba=baaa.

Referenced by [6].

Axiom: bbba=c.

Defines rule #21.

Referenced by [6], [11].

Axiom: ccc=d.

Defines rule #20.

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

Axiom: dadad=e.

Defines rule #18.

Referenced by [8], [9], [12], [13], [24], [27].

Axiom: eaa=f.

Defines rule #4.

Referenced by [10], [13], [14], [15], [16], [23].

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

Critical pair: aaac=baaa.

Flip LHS and RHS.

Defines rule #15.

Referenced by [11], [17], [18], [19].

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

Critical pair: cd=dc.

Flip LHS and RHS.

Defines rule #17.

Referenced by [9], [25].

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 #22.

Referenced by [24], [25].

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

Critical pair: daf=eadaa.

Referenced by [14].

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

Critical pair: bbaaac=caa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #11.

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

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

Critical pair: ccaaad=daa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #7.

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

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

Critical pair: dadaaaae=eaa.

Reduce LHS:

Reduce RHS:

Defines rule #2.

Referenced by [15], [16], [17], [18], [19], [20], [21], [22], [23].

Simplify [10] daf=eadaa.

Reduce RHS:

Defines rule #8.

Referenced by [20].

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

Critical pair: ef=faffe.

Defines rule #3.

Referenced by [20], [21], [22], [26], [28], [29].

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

Critical pair: eaf=faaffe.

Defines rule #5.

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

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

Critical pair: bf=aaacffe.

Referenced by [26].

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

Critical pair: baf=aaacaffe.

Referenced by [28].

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

Critical pair: baaf=aaacaaffe.

Reduce RHS:

Referenced by [29].

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

Critical pair: cf=aaadaffe.

Reduce RHS:

Defines rule #10.

Referenced by [26].

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

Critical pair: caf=aaadaaffe.

Reduce RHS:

Defines rule #12.

Referenced by [28].

Overlap of [12] daa=aaae with [13] aaaffe=f:

Critical pair: df=aaaeaffe.

Reduce RHS:

Defines rule #6.

Referenced by [29].

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

Critical pair: aaafff=faa.

Defines rule #1.

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

Critical pair: dadace=ecadad.

Defines rule #19.

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

Critical pair: dadaccd=ecc.

Defines rule #24.

Referenced by [27].

Simplify [17] bf=aaacffe.

Reduce RHS:

Defines rule #13.

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

Critical pair: dadacce=eccadad.

Defines rule #23.

Simplify [18] baf=aaacaffe.

Reduce RHS:

Defines rule #14.

Simplify [19] baaf=aaaaaadffe.

Reduce RHS:

Defines rule #16.