Certificate for #2317 ⟨a, b | abaabba=baa⟩

Completion settings:

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

[1] abaabba=baa

Axiom: abaabba=baa.

Referenced by [4].

[2] baabb=c

Axiom: baabb=c.

Referenced by [4], [5].

[3] acc=d

Axiom: acc=d.

Defines rule #6.

Referenced by [6], [7], [10], [24].

[4] baa=aca

Overlap of [1] abaabba=baa with [2] baabb=c:

a baabba baabb

Critical pair: aca=baa.

Flip LHS and RHS.

Defines rule #4.

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

[5] acabb=c

Overlap of [2] baabb=c with [4] baa=aca:

baabb baa

Critical pair: acabb=c.

Defines rule #15.

Referenced by [7], [8], [9], [11], [18], [23].

[6] bad=acd

Overlap of [4] baa=aca with [3] acc=d:

ba a acc

Critical pair: bad=acacc.

Reduce RHS:

[3]	ac(acc)
	⇒ acd

Defines rule #5.

Referenced by [9], [12], [15].

[7] bac=d

Overlap of [4] baa=aca with [5] acabb=c:

ba a acabb

Critical pair: bac=acacabb.

Reduce RHS:

[5]	ac(acabb)
[3]	⇒ (acc)
	⇒ d

Defines rule #11.

Referenced by [8], [9], [10], [11], [14], [15], [16].

[8] acada=caa

Overlap of [5] acabb=c with [4] baa=aca:

acab b baa

Critical pair: acabaca=caa.

Reduce LHS:

[7]	aca(bac)a
	⇒ acada

Defines rule #1.

Referenced by [18], [19].

[9] acadd=cad

Overlap of [5] acabb=c with [6] bad=acd:

acab b bad

Critical pair: acabacd=cad.

Reduce LHS:

[7]	aca(bac)d
	⇒ acadd

Defines rule #2.

Referenced by [20].

[10] bd=dc

Overlap of [7] bac=d with [3] acc=d:

b ac acc

Critical pair: bd=dc.

Defines rule #3.

Referenced by [13], [16], [17].

[11] dabb=bc

Overlap of [7] bac=d with [5] acabb=c:

b ac acabb

Critical pair: bc=dabb.

Flip LHS and RHS.

Defines rule #12.

Referenced by [12], [13], [14], [15], [16], [17], [19], [20], [21], [22].

[12] babc=acbc

Overlap of [6] bad=acd with [11] dabb=bc:

ba d dabb

Critical pair: babc=acdabb.

Reduce RHS:

[11]	ac(dabb)
	⇒ acbc

Defines rule #19.

[13] bbc=dcabb

Overlap of [10] bd=dc with [11] dabb=bc:

b d dabb

Critical pair: bbc=dcabb.

Defines rule #18.

[14] bcaa=dada

Overlap of [11] dabb=bc with [4] baa=aca:

dab b baa

Critical pair: dabaca=bcaa.

Reduce LHS:

[7]	da(bac)a
	⇒ dada

Flip LHS and RHS.

Defines rule #9.

[15] bcad=dadd

Overlap of [11] dabb=bc with [6] bad=acd:

dab b bad

Critical pair: dabacd=bcad.

Reduce LHS:

[7]	da(bac)d
	⇒ dadd

Flip LHS and RHS.

Defines rule #10.

Referenced by [22].

[16] bcac=dadc

Overlap of [11] dabb=bc with [7] bac=d:

dab b bac

Critical pair: dabd=bcac.

Reduce LHS:

[10]	da(bd)
	⇒ dadc

Flip LHS and RHS.

Defines rule #17.

Referenced by [23].

[17] bcd=dadcc

Overlap of [11] dabb=bc with [10] bd=dc:

dab b bd

Critical pair: dabdc=bcd.

Reduce LHS:

[10]	da(bd)c
	⇒ dadcc

Flip LHS and RHS.

Defines rule #8.

Referenced by [21].

[18] acadc=cac

Overlap of [8] acada=caa with [5] acabb=c:

acad a acabb

Critical pair: acadc=caacabb.

Reduce RHS:

[5]	ca(acabb)
	⇒ cac

Defines rule #7.

[19] caabb=acabc

Overlap of [8] acada=caa with [11] dabb=bc:

aca da dabb

Critical pair: acabc=caabb.

Flip LHS and RHS.

Defines rule #14.

Referenced by [24].

[20] acadbc=cabc

Overlap of [9] acadd=cad with [11] dabb=bc:

acad d dabb

Critical pair: acadbc=cadabb.

Reduce RHS:

[11]	ca(dabb)
	⇒ cabc

Defines rule #13.

[21] bcbc=dadccabb

Overlap of [17] bcd=dadcc with [11] dabb=bc:

bc d dabb

Critical pair: bcbc=dadccabb.

Defines rule #21.

[22] bcabc=dadbc

Overlap of [15] bcad=dadd with [11] dabb=bc:

bca d dabb

Critical pair: bcabc=daddabb.

Reduce RHS:

[11]	dad(dabb)
	⇒ dadbc

Defines rule #22.

[23] bcc=dadcabb

Overlap of [16] bcac=dadc with [5] acabb=c:

bc ac acabb

Critical pair: bcc=dadcabb.

Defines rule #16.

[24] acacabc=daabb

Overlap of [3] acc=d with [19] caabb=acabc:

ac c caabb

Critical pair: acacabc=daabb.

Defines rule #20.