Certificate for #2265 ⟨a, b | aabbaba=baa⟩

Completion settings:

Auxiliary generators:
1. c = abba
2. d = acb
Reduction order:
- Right-to-left recursive path with deg(c) = deg(d) = 0, c < d; deg(b) = 1; deg(a) = 2

[1] aabbaba=baa

Axiom: aabbaba=baa.

Referenced by [4].

[2] abba=c

Axiom: abba=c.

Defines rule #18.

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

[3] acb=d

Axiom: acb=d.

Defines rule #11.

Referenced by [4], [5], [6], [7], [13], [14].

[4] baa=da

Overlap of [1] aabbaba=baa with [2] abba=c:

a abbaba abba

Critical pair: acba=baa.

Reduce LHS:

[3]	(acb)a
	⇒ da

Flip LHS and RHS.

Defines rule #14.

Referenced by [5], [6], [9], [11], [21].

[5] acda=daa

Overlap of [3] acb=d with [4] baa=da:

ac b baa

Critical pair: acda=daa.

Defines rule #15.

[6] bad=dd

Overlap of [4] baa=da with [3] acb=d:

ba a acb

Critical pair: bad=dacb.

Reduce RHS:

[3]	d(acb)
	⇒ dd

Defines rule #6.

Referenced by [7], [10], [16], [18], [20], [22].

[7] acdd=dad

Overlap of [3] acb=d with [6] bad=dd:

ac b bad

Critical pair: acdd=dad.

Defines rule #8.

[8] abbc=cbba

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

abb a abba

Critical pair: abbc=cbba.

Defines rule #13.

[9] abda=ca

Overlap of [2] abba=c with [4] baa=da:

ab ba baa

Critical pair: abda=ca.

Referenced by [19].

[10] abdd=cd

Overlap of [2] abba=c with [6] bad=dd:

ab ba bad

Critical pair: abdd=cd.

Referenced by [17].

[11] bac=dc

Overlap of [4] baa=da with [2] abba=c:

ba a abba

Critical pair: bac=dabba.

Reduce RHS:

[2]	d(abba)
	⇒ dc

Defines rule #5.

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

[12] abdc=cc

Overlap of [2] abba=c with [11] bac=dc:

ab ba bac

Critical pair: abdc=cc.

Referenced by [15].

[13] acdc=dac

Overlap of [3] acb=d with [11] bac=dc:

ac b bac

Critical pair: acdc=dac.

Defines rule #7.

[14] bd=dcb

Overlap of [11] bac=dc with [3] acb=d:

b ac acb

Critical pair: bd=dcb.

Defines rule #1.

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

[15] adcbc=cc

Simplify [12] abdc=cc.

Reduce LHS:

[14]	a(bd)c
	⇒ adcbc

Defines rule #12.

Referenced by [16].

[16] bcc=ddcbc

Overlap of [6] bad=dd with [15] adcbc=cc:

b ad adcbc

Critical pair: bcc=ddcbc.

Defines rule #2.

[17] adcdcb=cd

Simplify [10] abdd=cd.

Reduce LHS:

[14]	a(bd)d
[14]	⇒ adc(bd)
	⇒ adcdcb

Referenced by [18].

[18] bcd=ddcdcb

Overlap of [6] bad=dd with [17] adcdcb=cd:

b ad adcdcb

Critical pair: bcd=ddcdcb.

Defines rule #3.

[19] adcba=ca

Simplify [9] abda=ca.

Reduce LHS:

[14]	a(bd)a
	⇒ adcba

Defines rule #17.

Referenced by [20], [21], [22], [23].

[20] bca=ddcba

Overlap of [6] bad=dd with [19] adcba=ca:

b ad adcba

Critical pair: bca=ddcba.

Defines rule #4.

[21] adcda=caa

Overlap of [19] adcba=ca with [4] baa=da:

adc ba baa

Critical pair: adcda=caa.

Defines rule #16.

[22] adcdd=cad

Overlap of [19] adcba=ca with [6] bad=dd:

adc ba bad

Critical pair: adcdd=cad.

Defines rule #10.

[23] adcdc=cac

Overlap of [19] adcba=ca with [11] bac=dc:

adc ba bac

Critical pair: adcdc=cac.

Defines rule #9.