Certificate for #147 ⟨a, b | aabbaba=1⟩

Completion settings:

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

[1] aabbaba=1

Axiom: aabbaba=1.

Referenced by [4].

[2] aaa=c

Axiom: aaa=c.

Defines rule #5.

Referenced by [5], [6], [12], [16], [18], [20].

[3] bbab=d

Axiom: bbab=d.

Defines rule #13.

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

[4] aada=1

Overlap of [1] aabbaba=1 with [3] bbab=d:

aa bbaba bbab

Critical pair: aada=1.

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

[5] ac=ca

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

a aa aaa

Critical pair: ac=ca.

Defines rule #3.

Referenced by [17], [21].

[6] cda=a

Overlap of [2] aaa=c with [4] aada=1:

a aa aada

Critical pair: a=cda.

Flip LHS and RHS.

Referenced by [8].

[7] aad=ada

Overlap of [4] aada=1 with [4] aada=1:

aad a aada

Critical pair: aad=ada.

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

[8] adaa=cd

Overlap of [6] cda=a with [4] aada=1:

cd a aada

Critical pair: cd=aada.

Reduce RHS:

[7]	(aad)a
	⇒ adaa

Flip LHS and RHS.

Referenced by [10], [11].

[9] dbab=bbad

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

bba b bbab

Critical pair: bbad=dbab.

Flip LHS and RHS.

Referenced by [13].

[10] cd=1

Overlap of [4] aada=1 with [7] aad=ada:

aada aad

Critical pair: adaa=1.

Reduce LHS:

[8]	(adaa)
	⇒ cd

Defines rule #1.

Referenced by [11], [12], [14], [18], [22].

[11] ad=da

Overlap of [4] aada=1 with [7] aad=ada:

aad a aad

Critical pair: aadada=ad.

Reduce LHS:

[7]	(aad)ada
[8]	⇒ (adaa)da
[10]	⇒ (cd)da
	⇒ da

Flip LHS and RHS.

Defines rule #4.

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

[12] dc=1

Overlap of [2] aaa=c with [11] ad=da:

aa a ad

Critical pair: aada=cd.

Reduce LHS:

[7]	(aad)a
[11]	⇒ (ad)aa
[2]	⇒ d(aaa)
	⇒ dc

Reduce RHS:

[10]	(cd)
	⇒ 1

Defines rule #2.

Referenced by [16], [24].

[13] dbab=bbda

Simplify [9] dbab=bbad.

Reduce RHS:

[11]	bb(ad)
	⇒ bbda

Defines rule #7.

Referenced by [14], [15].

[14] cbbda=bab

Overlap of [10] cd=1 with [13] dbab=bbda:

c d dbab

Critical pair: cbbda=bab.

Referenced by [16].

[15] dabab=abbda

Overlap of [11] ad=da with [13] dbab=bbda:

a d dbab

Critical pair: abbda=dabab.

Flip LHS and RHS.

Defines rule #10.

[16] cbb=babaa

Overlap of [14] cbbda=bab with [2] aaa=c:

cbbd a aaa

Critical pair: cbbdc=babaa.

Reduce LHS:

[12]	cbb(dc)
	⇒ cbb

Defines rule #6.

Referenced by [17], [18].

[17] cabb=ababaa

Overlap of [5] ac=ca with [16] cbb=babaa:

a c cbb

Critical pair: ababaa=cabb.

Flip LHS and RHS.

Defines rule #9.

Referenced by [21].

[18] babcb=1

Overlap of [16] cbb=babaa with [3] bbab=d:

c bb bbab

Critical pair: cd=babaaab.

Reduce LHS:

[10]	(cd)
	⇒ 1

Reduce RHS:

[2]	bab(aaa)b
	⇒ babcb

Flip LHS and RHS.

Referenced by [19].

[19] abcb=babc

Overlap of [18] babcb=1 with [18] babcb=1:

babc b babcb

Critical pair: babc=abcb.

Flip LHS and RHS.

Defines rule #8.

Referenced by [20].

[20] aababc=cbcb

Overlap of [2] aaa=c with [19] abcb=babc:

aa a abcb

Critical pair: aababc=cbcb.

Referenced by [22].

[21] caabb=aababaa

Overlap of [5] ac=ca with [17] cabb=ababaa:

a c cabb

Critical pair: aababaa=caabb.

Flip LHS and RHS.

Referenced by [23].

[22] aabab=cbcbd

Overlap of [20] aababc=cbcb with [10] cd=1:

aabab c cd

Critical pair: aabab=cbcbd.

Defines rule #12.

Referenced by [23].

[23] caabb=cbcbdaa

Simplify [21] caabb=aababaa.

Reduce RHS:

[22]	(aabab)aa
	⇒ cbcbdaa

Referenced by [24].

[24] aabb=bcbdaa

Overlap of [12] dc=1 with [23] caabb=cbcbdaa:

d c caabb

Critical pair: dcbcbdaa=aabb.

Reduce LHS:

[12]	(dc)bcbdaa
	⇒ bcbdaa

Flip LHS and RHS.

Defines rule #11.