Certificate for #2429 ⟨a, b, c | aab=b, acca=1⟩

Completion settings:

Auxiliary generators:
1. d = aa
Reduction order:
- Left-to-right shortlex with a < b < c < d

[1] aab=b

Axiom: aab=b.

Referenced by [4].

[2] acca=1

Axiom: acca=1.

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

[3] aa=d

Axiom: aa=d.

Defines rule #1.

Referenced by [4], [5], [7], [8].

[4] db=b

Overlap of [1] aab=b with [3] aa=d:

aab aa

Critical pair: db=b.

Defines rule #3.

Referenced by [10].

[5] da=ad

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

a a aa

Critical pair: ad=da.

Flip LHS and RHS.

Defines rule #2.

Referenced by [8].

[6] cca=acc

Overlap of [2] acca=1 with [2] acca=1:

acc a acca

Critical pair: acc=cca.

Flip LHS and RHS.

Defines rule #5.

Referenced by [8].

[7] accd=a

Overlap of [2] acca=1 with [3] aa=d:

acc a aa

Critical pair: accd=a.

Referenced by [9].

[8] adcc=a

Overlap of [3] aa=d with [2] acca=1:

a a acca

Critical pair: a=dcca.

Reduce RHS:

[6]	d(cca)
[5]	⇒ (da)cc
	⇒ adcc

Flip LHS and RHS.

Referenced by [11].

[9] ccd=1

Overlap of [2] acca=1 with [7] accd=a:

acc a accd

Critical pair: acca=ccd.

Reduce LHS:

[2]	(acca)
	⇒ 1

Flip LHS and RHS.

Defines rule #7.

Referenced by [10], [12].

[10] ccb=b

Overlap of [9] ccd=1 with [4] db=b:

cc d db

Critical pair: ccb=b.

Defines rule #6.

[11] dcc=1

Overlap of [2] acca=1 with [8] adcc=a:

acc a adcc

Critical pair: acca=dcc.

Reduce LHS:

[2]	(acca)
	⇒ 1

Flip LHS and RHS.

Referenced by [12].

[12] dc=cd

Overlap of [11] dcc=1 with [9] ccd=1:

dc c ccd

Critical pair: dc=cd.

Defines rule #4.