Certificate for #5246 ⟨a, b | aabbbaa=baab⟩

Completion settings:

• Reduction order:
  • Left-to-right recursive path with deg(f) = deg(b) = deg(d) = deg(c) = deg(e) = 0, f < b < d < c < e; deg(a) = 1
• Auxiliary generators:
  1. aa=c
  2. cb=d
  3. db=e
  4. eb=f

Axiom: aabbbaa=baab.

Referenced by [6].

Axiom: aa=c.

Defines rule #32.

Referenced by [6], [7], [8].

Axiom: cb=d.

Defines rule #5.

Referenced by [6], [7], [9], [12], [13], [17], [29], [30].

Axiom: db=e.

Defines rule #4.

Referenced by [7], [10], [12], [14], [16], [18], [31], [32].

Axiom: eb=f.

Defines rule #6.

Referenced by [7], [11], [15], [16], [19], [21], [23], [25], [33], [34].

Simplify [1] aabbbaa=baab.

Reduce RHS:

Referenced by [7].

Overlap of [6] aabbbaa=bd with [2] aa=c:

Critical pair: cbbbaa=bd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #2.

Referenced by [9], [10], [11], [12], [26], [27].

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

Critical pair: ac=ca.

Flip LHS and RHS.

Defines rule #22.

Referenced by [20], [22], [24].

Overlap of [3] cb=d with [7] bd=fc:

Critical pair: cfc=dd.

Defines rule #12.

Referenced by [22].

Overlap of [4] db=e with [7] bd=fc:

Critical pair: dfc=ed.

Defines rule #8.

Referenced by [20].

Overlap of [5] eb=f with [7] bd=fc:

Critical pair: efc=fd.

Defines rule #17.

Referenced by [24].

Overlap of [7] bd=fc with [4] db=e:

Critical pair: be=fcb.

Reduce RHS:

Defines rule #3.

Referenced by [13], [14], [15], [16], [27], [28].

Overlap of [3] cb=d with [12] be=fd:

Critical pair: cfd=de.

Defines rule #11.

Overlap of [4] db=e with [12] be=fd:

Critical pair: dfd=ee.

Defines rule #7.

Overlap of [5] eb=f with [12] be=fd:

Critical pair: efd=fe.

Defines rule #16.

Overlap of [12] be=fd with [5] eb=f:

Critical pair: bf=fdb.

Reduce RHS:

Defines rule #1.

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

Overlap of [3] cb=d with [16] bf=fe:

Critical pair: cfe=df.

Defines rule #13.

Referenced by [23].

Overlap of [4] db=e with [16] bf=fe:

Critical pair: dfe=ef.

Defines rule #9.

Referenced by [21].

Overlap of [5] eb=f with [16] bf=fe:

Critical pair: efe=ff.

Defines rule #18.

Referenced by [25].

Overlap of [10] dfc=ed with [8] ca=ac:

Critical pair: dfac=eda.

Flip LHS and RHS.

Defines rule #31.

Overlap of [18] dfe=ef with [5] eb=f:

Critical pair: dff=efb.

Flip LHS and RHS.

Defines rule #15.

Referenced by [26], [27], [28].

Overlap of [9] cfc=dd with [8] ca=ac:

Critical pair: cfac=dda.

Defines rule #25.

Referenced by [29].

Overlap of [17] cfe=df with [5] eb=f:

Critical pair: cff=dfb.

Defines rule #10.

Overlap of [11] efc=fd with [8] ca=ac:

Critical pair: efac=fda.

Defines rule #29.

Referenced by [30].

Overlap of [19] efe=ff with [5] eb=f:

Critical pair: eff=ffb.

Defines rule #14.

Referenced by [26], [27], [28].

Overlap of [21] efb=dff with [7] bd=fc:

Critical pair: effc=dffd.

Reduce LHS:

Flip LHS and RHS.

Defines rule #20.

Overlap of [21] efb=dff with [12] be=fd:

Critical pair: effd=dffe.

Reduce LHS:

Flip LHS and RHS.

Defines rule #21.

Overlap of [21] efb=dff with [16] bf=fe:

Critical pair: effe=dfff.

Reduce LHS:

Flip LHS and RHS.

Defines rule #19.

Overlap of [22] cfac=dda with [3] cb=d:

Critical pair: cfad=ddab.

Defines rule #24.

Referenced by [31].

Overlap of [24] efac=fda with [3] cb=d:

Critical pair: efad=fdab.

Defines rule #28.

Referenced by [32].

Overlap of [29] cfad=ddab with [4] db=e:

Critical pair: cfae=ddabb.

Defines rule #26.

Referenced by [33].

Overlap of [30] efad=fdab with [4] db=e:

Critical pair: efae=fdabb.

Defines rule #30.

Referenced by [34].

Overlap of [31] cfae=ddabb with [5] eb=f:

Critical pair: cfaf=ddabbb.

Defines rule #23.

Overlap of [32] efae=fdabb with [5] eb=f:

Critical pair: efaf=fdabbb.

Defines rule #27.