Certificate for #533 ⟨a, b | aabba=baa⟩

Completion settings:

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

[1] aabba=baa

Axiom: aabba=baa.

Referenced by [5].

[2] aabb=c

Axiom: aabb=c.

Referenced by [5], [6].

[3] abc=d

Axiom: abc=d.

Referenced by [7], [8], [11], [13], [15], [16].

[4] abb=e

Axiom: abb=e.

Defines rule #20.

Referenced by [6], [7], [9], [11], [13], [15], [20].

[5] baa=ca

Overlap of [1] aabba=baa with [2] aabb=c:

aabba aabb

Critical pair: ca=baa.

Flip LHS and RHS.

Defines rule #21.

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

[6] ae=c

Overlap of [2] aabb=c with [4] abb=e:

a abb abb

Critical pair: ae=c.

Defines rule #11.

Referenced by [9], [10], [12], [14], [21], [23].

[7] eaa=da

Overlap of [4] abb=e with [5] baa=ca:

ab b baa

Critical pair: abca=eaa.

Reduce LHS:

[3]	(abc)a
	⇒ da

Flip LHS and RHS.

Defines rule #17.

Referenced by [23], [24].

[8] bad=cd

Overlap of [5] baa=ca with [3] abc=d:

ba a abc

Critical pair: bad=cabc.

Reduce RHS:

[3]	c(abc)
	⇒ cd

Defines rule #15.

Referenced by [13].

[9] bc=ce

Overlap of [5] baa=ca with [4] abb=e:

ba a abb

Critical pair: bae=cabb.

Reduce LHS:

[6]	b(ae)
	⇒ bc

Reduce RHS:

[4]	c(abb)
	⇒ ce

Defines rule #4.

Referenced by [11], [16], [20].

[10] bac=cc

Overlap of [5] baa=ca with [6] ae=c:

ba a ae

Critical pair: bac=cae.

Reduce RHS:

[6]	c(ae)
	⇒ cc

Defines rule #16.

Referenced by [15], [17].

[11] ec=de

Overlap of [4] abb=e with [9] bc=ce:

ab b bc

Critical pair: abce=ec.

Reduce LHS:

[3]	(abc)e
	⇒ de

Flip LHS and RHS.

Defines rule #2.

Referenced by [12], [18].

[12] ade=cc

Overlap of [6] ae=c with [11] ec=de:

a e ec

Critical pair: ade=cc.

Defines rule #12.

[13] ead=dd

Overlap of [4] abb=e with [8] bad=cd:

ab b bad

Critical pair: abcd=ead.

Reduce LHS:

[3]	(abc)d
	⇒ dd

Flip LHS and RHS.

Defines rule #5.

Referenced by [14], [19].

[14] add=cad

Overlap of [6] ae=c with [13] ead=dd:

a e ead

Critical pair: add=cad.

Defines rule #7.

[15] eac=dc

Overlap of [4] abb=e with [10] bac=cc:

ab b bac

Critical pair: abcc=eac.

Reduce LHS:

[3]	(abc)c
	⇒ dc

Flip LHS and RHS.

Defines rule #6.

Referenced by [21], [22].

[16] ace=d

Overlap of [3] abc=d with [9] bc=ce:

a bc bc

Critical pair: ace=d.

Defines rule #13.

Referenced by [17], [18], [19], [20], [22], [24].

[17] bd=cce

Overlap of [10] bac=cc with [16] ace=d:

b ac ace

Critical pair: bd=cce.

Defines rule #3.

Referenced by [20].

[18] acde=dc

Overlap of [16] ace=d with [11] ec=de:

ac e ec

Critical pair: acde=dc.

Defines rule #14.

[19] acdd=dad

Overlap of [16] ace=d with [13] ead=dd:

ac e ead

Critical pair: acdd=dad.

Defines rule #9.

[20] ed=dce

Overlap of [4] abb=e with [17] bd=cce:

ab b bd

Critical pair: abcce=ed.

Reduce LHS:

[9]	a(bc)ce
[16]	⇒ (ace)ce
	⇒ dce

Flip LHS and RHS.

Defines rule #1.

[21] adc=cac

Overlap of [6] ae=c with [15] eac=dc:

a e eac

Critical pair: adc=cac.

Defines rule #8.

[22] acdc=dac

Overlap of [16] ace=d with [15] eac=dc:

ac e eac

Critical pair: acdc=dac.

Defines rule #10.

[23] ada=caa

Overlap of [6] ae=c with [7] eaa=da:

a e eaa

Critical pair: ada=caa.

Defines rule #18.

[24] acda=daa

Overlap of [16] ace=d with [7] eaa=da:

ac e eaa

Critical pair: acda=daa.

Defines rule #19.