Certificate for #4749 ⟨a, b | aabbbbba=baa⟩

Completion settings:

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

[1] aabbbbba=baa

Axiom: aabbbbba=baa.

Referenced by [5].

[2] bbbbba=c

Axiom: bbbbba=c.

Defines rule #16.

Referenced by [5], [7].

[3] ccccc=d

Axiom: ccccc=d.

Defines rule #12.

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

[4] da=e

Axiom: da=e.

Defines rule #3.

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

[5] baa=aac

Overlap of [1] aabbbbba=baa with [2] bbbbba=c:

aa bbbbba bbbbba

Critical pair: aac=baa.

Flip LHS and RHS.

Defines rule #14.

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

[6] dc=cd

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

c cccc ccccc

Critical pair: cd=dc.

Flip LHS and RHS.

Defines rule #8.

Referenced by [9], [14], [15], [16], [17].

[7] ca=aad

Overlap of [2] bbbbba=c with [5] baa=aac:

bbbb ba baa

Critical pair: bbbbaac=ca.

Reduce LHS:

[5]	bbb(baa)c
[5]	⇒ bb(baa)cc
[5]	⇒ b(baa)ccc
[5]	⇒ (baa)cccc
[3]	⇒ aa(ccccc)
	⇒ aad

Flip LHS and RHS.

Defines rule #5.

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

[8] aaeeeed=e

Overlap of [3] ccccc=d with [7] ca=aad:

cccc c ca

Critical pair: ccccaad=da.

Reduce LHS:

[7]	ccc(ca)ad
[7]	⇒ cc(ca)adad
[7]	⇒ c(ca)adadad
[7]	⇒ (ca)adadadad
[4]	⇒ aa(da)dadadad
[4]	⇒ aae(da)dadad
[4]	⇒ aaee(da)dad
[4]	⇒ aaeee(da)d
	⇒ aaeeeed

Reduce RHS:

[4]	(da)
	⇒ e

Defines rule #2.

Referenced by [11], [12], [13], [14].

[9] ce=ead

Overlap of [6] dc=cd with [7] ca=aad:

d c ca

Critical pair: daad=cda.

Reduce LHS:

[4]	(da)ad
	⇒ ead

Reduce RHS:

[4]	c(da)
	⇒ ce

Flip LHS and RHS.

Defines rule #6.

Referenced by [10], [11].

[10] de=eaeeeed

Overlap of [3] ccccc=d with [9] ce=ead:

cccc c ce

Critical pair: ccccead=de.

Reduce LHS:

[9]	ccc(ce)ad
[9]	⇒ cc(ce)adad
[9]	⇒ c(ce)adadad
[9]	⇒ (ce)adadadad
[4]	⇒ ea(da)dadadad
[4]	⇒ eae(da)dadad
[4]	⇒ eaee(da)dad
[4]	⇒ eaeee(da)d
	⇒ eaeeeed

Flip LHS and RHS.

Defines rule #4.

Referenced by [11], [12].

[11] be=aaeaeaeeeeeaeeeeeaeeeedd

Overlap of [5] baa=aac with [8] aaeeeed=e:

b aa aaeeeed

Critical pair: be=aaceeeed.

Reduce RHS:

[9]	aa(ce)eeed
[10]	⇒ aaea(de)eed
[10]	⇒ aaeaeaeeee(de)ed
[10]	⇒ aaeaeaeeeeeaeeee(de)d
	⇒ aaeaeaeeeeeaeeeeeaeeeedd

Defines rule #13.

[12] bae=aaaaeaeeeeeaeeeeeaeeeeeaeeeedd

Overlap of [5] baa=aac with [8] aaeeeed=e:

ba a aaeeeed

Critical pair: bae=aacaeeeed.

Reduce RHS:

[7]	aa(ca)eeeed
[10]	⇒ aaaa(de)eeed
[10]	⇒ aaaaeaeeee(de)eed
[10]	⇒ aaaaeaeeeeeaeeee(de)ed
[10]	⇒ aaaaeaeeeeeaeeeeeaeeee(de)d
	⇒ aaaaeaeeeeeaeeeeeaeeeeeaeeeedd