Certificate for #846 ⟨a, b | ababaaab=a⟩

Completion settings:

• Auxiliary generators:
  1. c = aaa
  2. d = ba
  3. e = ad
• Reduction order:
  • Right-to-left recursive path with deg(d) = deg(e) = 0, d < e; deg(c) = deg(a) = 1, c < a; deg(b) = 2

Axiom: ababaaab=a.

Referenced by [5].

Axiom: aaa=c.

Referenced by [7], [8], [9], [11], [16].

Axiom: ba=d.

Defines rule #34.

Referenced by [5], [6], [9], [12], [14], [17].

Axiom: ad=e.

Defines rule #4.

Referenced by [5], [6], [8], [10], [12], [19], [27], [28], [29], [36], [39], [40].

Overlap of [1] ababaaab=a with [3] ba=d:

Critical pair: adbaaab=a.

Reduce LHS:

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

Overlap of [3] ba=d with [4] ad=e:

Critical pair: be=dd.

Defines rule #32.

Referenced by [14], [17].

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

Critical pair: ac=ca.

Flip LHS and RHS.

Defines rule #13.

Referenced by [10], [33], [43].

Overlap of [2] aaa=c with [4] ad=e:

Critical pair: aae=cd.

Referenced by [15], [18].

Overlap of [3] ba=d with [2] aaa=c:

Critical pair: bc=daa.

Referenced by [13], [22].

Overlap of [7] ca=ac with [4] ad=e:

Critical pair: ce=acd.

Flip LHS and RHS.

Referenced by [11], [35].

Overlap of [2] aaa=c with [10] acd=ce:

Critical pair: aace=ccd.

Referenced by [23].

Overlap of [5] edaab=a with [3] ba=d:

Critical pair: edaad=aa.

Reduce LHS:

Flip LHS and RHS.

Defines rule #16.

Referenced by [13], [14], [15], [16], [17], [18], [19], [20], [21], [22], [23], [32], [33], [34], [36], [37], [38], [39].

Overlap of [5] edaab=a with [9] bc=daa:

Critical pair: edaadaa=ac.

Reduce LHS:

Referenced by [24].

Overlap of [6] be=dd with [5] edaab=a:

Critical pair: ba=dddaab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #25.

Referenced by [40].

Overlap of [8] aae=cd with [5] edaab=a:

Critical pair: aaa=cddaab.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Referenced by [25].

Overlap of [2] aaa=c with [12] aa=edae:

Critical pair: edaea=c.

Defines rule #17.

Referenced by [20], [25], [31].

Overlap of [3] ba=d with [12] aa=edae:

Critical pair: bedae=da.

Reduce LHS:

Defines rule #7.

Referenced by [27], [28], [32], [36], [41], [43].

Overlap of [8] aae=cd with [12] aa=edae:

Critical pair: edaee=cd.

Defines rule #10.

Referenced by [24], [32], [34], [42].

Overlap of [12] aa=edae with [4] ad=e:

Critical pair: ae=edaed.

Flip LHS and RHS.

Defines rule #9.

Referenced by [24], [30], [37], [43].

Overlap of [12] aa=edae with [12] aa=edae:

Critical pair: aedae=edaea.

Reduce RHS:

Defines rule #19.

Referenced by [26], [28], [29], [30], [38], [41], [43], [44].

Overlap of [5] edaab=a with [12] aa=edae:

Critical pair: ededaeb=a.

Defines rule #22.

Referenced by [36], [37], [38], [39].

Simplify [9] bc=daa.

Reduce RHS:

Defines rule #33.

Overlap of [11] aace=ccd with [12] aa=edae:

Critical pair: edaece=ccd.

Referenced by [33].

Overlap of [13] ededaededae=ac with [19] edaed=ae:

Critical pair: edaeedae=ac.

Reduce LHS:

Defines rule #15.

Referenced by [33], [42], [43].

Simplify [15] cddedaeb=edaea.

Reduce RHS:

Defines rule #30.

Overlap of [20] aedae=c with [20] aedae=c:

Critical pair: aedc=cdae.

Flip LHS and RHS.

Defines rule #14.

Overlap of [4] ad=e with [17] dddae=da:

Critical pair: ada=eddae.

Reduce LHS:

Flip LHS and RHS.

Defines rule #8.

Referenced by [29], [34], [39], [44].

Overlap of [17] dddae=da with [20] aedae=c:

Critical pair: dddc=dadae.

Reduce RHS:

Flip LHS and RHS.

Defines rule #5.

Overlap of [27] eddae=ea with [20] aedae=c:

Critical pair: eddc=eadae.

Reduce RHS:

Flip LHS and RHS.

Defines rule #6.

Overlap of [19] edaed=ae with [20] aedae=c:

Critical pair: edc=aeae.

Flip LHS and RHS.

Defines rule #18.

Referenced by [31], [32], [33], [34].

Overlap of [16] edaea=c with [30] aeae=edc:

Critical pair: ededc=ce.

Flip LHS and RHS.

Defines rule #3.

Referenced by [35], [43].

Overlap of [17] dddae=da with [30] aeae=edc:

Critical pair: dddedc=daae.

Reduce RHS:

Flip LHS and RHS.

Defines rule #1.

Referenced by [43].

Overlap of [24] cddae=ac with [30] aeae=edc:

Critical pair: cddedc=acae.

Reduce RHS:

Flip LHS and RHS.

Defines rule #11.

Overlap of [27] eddae=ea with [30] aeae=edc:

Critical pair: eddedc=eaae.

Reduce RHS:

Flip LHS and RHS.

Defines rule #2.

Simplify [10] acd=ce.

Reduce RHS:

Defines rule #12.

Overlap of [17] dddae=da with [21] ededaeb=a:

Critical pair: dddaa=dadedaeb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #23.

Overlap of [19] edaed=ae with [21] ededaeb=a:

Critical pair: edaa=aeedaeb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #31.

Referenced by [41], [42], [43], [44].

Overlap of [20] aedae=c with [21] ededaeb=a:

Critical pair: aedaa=cdedaeb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #29.

Overlap of [27] eddae=ea with [21] ededaeb=a:

Critical pair: eddaa=eadedaeb.

Reduce LHS:

Reduce RHS:

Flip LHS and RHS.

Defines rule #24.

Overlap of [4] ad=e with [14] dddedaeb=d:

Critical pair: ad=eddedaeb.

Reduce LHS:

Flip LHS and RHS.

Defines rule #26.

Overlap of [17] dddae=da with [37] aeedaeb=ededae:

Critical pair: dddededae=daedaeb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #20.

Overlap of [18] edaee=cd with [37] aeedaeb=ededae:

Critical pair: edededae=cddaeb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #28.

Overlap of [24] cddae=ac with [37] aeedaeb=ededae:

Critical pair: cddededae=acedaeb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #27.

Overlap of [27] eddae=ea with [37] aeedaeb=ededae:

Critical pair: eddededae=eaedaeb.

Reduce RHS:

Flip LHS and RHS.

Defines rule #21.