Certificate for #1670 ⟨a, b, c | aab=ba, cba=1⟩

Completion settings:

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

[1] aab=ba

Axiom: aab=ba.

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

[2] cba=1

Axiom: cba=1.

Defines rule #4.

Referenced by [4], [6].

[3] bba=d

Axiom: bba=d.

Defines rule #5.

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

[4] ab=cd

Overlap of [2] cba=1 with [1] aab=ba:

cb a aab

Critical pair: cbba=ab.

Reduce LHS:

[3]	c(bba)
	⇒ cd

Flip LHS and RHS.

Defines rule #8.

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

[5] bd=dcd

Overlap of [3] bba=d with [1] aab=ba:

bb a aab

Critical pair: bbba=dab.

Reduce LHS:

[3]	b(bba)
	⇒ bd

Reduce RHS:

[4]	d(ab)
	⇒ dcd

Defines rule #1.

[6] cbcd=b

Overlap of [2] cba=1 with [4] ab=cd:

cb a ab

Critical pair: cbcd=b.

Defines rule #2.

[7] bbcd=db

Overlap of [3] bba=d with [4] ab=cd:

bb a ab

Critical pair: bbcd=db.

Defines rule #3.

[8] ad=cdba

Overlap of [4] ab=cd with [3] bba=d:

a b bba

Critical pair: ad=cdba.

Defines rule #6.

[9] acd=ba

Overlap of [1] aab=ba with [4] ab=cd:

a ab ab

Critical pair: acd=ba.

Defines rule #7.