Certificate for #1808 ⟨a, b | abbabaaab=b⟩

Completion settings:

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

[1] abbabaaab=b

Axiom: abbabaaab=b.

Referenced by [4].

[2] ab=c

Axiom: ab=c.

Referenced by [4], [5], [9].

[3] bbc=d

Axiom: bbc=d.

Referenced by [5], [10].

[4] cbcaac=b

Overlap of [1] abbabaaab=b with [2] ab=c:

abbabaaab ab

Critical pair: cbabaaab=b.

Reduce LHS:

[2]	cb(ab)aaab
[2]	⇒ cbcaa(ab)
	⇒ cbcaac

Referenced by [7].

[5] cbc=ad

Overlap of [2] ab=c with [3] bbc=d:

a b bbc

Critical pair: ad=cbc.

Flip LHS and RHS.

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

[6] cbad=adbc

Overlap of [5] cbc=ad with [5] cbc=ad:

cb c cbc

Critical pair: cbad=adbc.

Referenced by [8].

[7] b=adaac

Simplify [4] cbcaac=b.

Reduce LHS:

[5]	(cbc)aac
	⇒ adaac

Flip LHS and RHS.

Defines rule #6.

Referenced by [8], [9], [10], [11].

[8] cadaacad=adadaacc

Simplify [6] cbad=adbc.

Reduce LHS:

[7]	c(b)ad
	⇒ cadaacad

Reduce RHS:

[7]	ad(b)c
	⇒ adadaacc

Referenced by [14], [19].

[9] aadaac=c

Overlap of [2] ab=c with [7] b=adaac:

a b b

Critical pair: aadaac=c.

Defines rule #4.

Referenced by [12], [15], [18], [19].

[10] adaaad=d

Overlap of [3] bbc=d with [7] b=adaac:

bbc b

Critical pair: adaacbc=d.

Reduce LHS:

[5]	adaa(cbc)
	⇒ adaaad

Defines rule #10.

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

[11] cadaacc=ad

Overlap of [5] cbc=ad with [7] b=adaac:

c bc b

Critical pair: cadaacc=ad.

Defines rule #5.

Referenced by [14].

[12] adac=daac

Overlap of [10] adaaad=d with [9] aadaac=c:

ada aad aadaac

Critical pair: adac=daac.

Defines rule #2.

[13] adaad=daaad

Overlap of [10] adaaad=d with [10] adaaad=d:

adaa ad adaaad

Critical pair: adaad=daaad.

Defines rule #9.

Referenced by [15], [16].

[14] adadaaccaacc=cd

Overlap of [8] cadaacad=adadaacc with [11] cadaacc=ad:

cadaa cad cadaacc

Critical pair: cadaaad=adadaaccaacc.

Reduce LHS:

[10]	c(adaaad)
	⇒ cd

Flip LHS and RHS.

Referenced by [18].

[15] adc=dac

Overlap of [13] adaad=daaad with [9] aadaac=c:

ad aad aadaac

Critical pair: adc=daaadaac.

Reduce RHS:

[9]	da(aadaac)
	⇒ dac

Defines rule #1.

[16] adad=daad

Overlap of [13] adaad=daaad with [10] adaaad=d:

ada ad adaaad

Critical pair: adad=daaadaaad.

Reduce RHS:

[10]	daa(adaaad)
	⇒ daad

Defines rule #8.

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

[17] add=dad

Overlap of [16] adad=daad with [10] adaaad=d:

ad ad adaaad

Critical pair: add=daadaaad.

Reduce RHS:

[10]	da(adaaad)
	⇒ dad

Defines rule #7.

[18] cd=dccaacc

Simplify [14] adadaaccaacc=cd.

Reduce LHS:

[16]	(adad)aaccaacc
[9]	⇒ d(aadaac)caacc
	⇒ dccaacc

Flip LHS and RHS.

Defines rule #3.

[19] cadaacad=dcc

Simplify [8] cadaacad=adadaacc.

Reduce RHS:

[16]	(adad)aacc
[9]	⇒ d(aadaac)c
	⇒ dcc

Defines rule #11.