Certificate for #15954 ⟨a, b | aaa=aa, aaba=ba⟩

Completion settings:

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

[1] aaa=aa

Axiom: aaa=aa.

Defines rule #1.

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

[2] aaba=ba

Axiom: aaba=ba.

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

[3] bba=c

Axiom: bba=c.

Defines rule #6.

Referenced by [4], [6], [7].

[4] caa=ca

Overlap of [3] bba=c with [1] aaa=aa:

bb a aaa

Critical pair: bbaa=caa.

Reduce LHS:

[3]	(bba)a
	⇒ ca

Flip LHS and RHS.

Defines rule #2.

[5] aba=ba

Overlap of [1] aaa=aa with [2] aaba=ba:

a aa aaba

Critical pair: aba=aaba.

Reduce RHS:

[2]	(aaba)
	⇒ ba

Defines rule #4.

Referenced by [7].

[6] aac=c

Overlap of [2] aaba=ba with [2] aaba=ba:

aab a aaba

Critical pair: aabba=baaba.

Reduce LHS:

[3]	aa(bba)
	⇒ aac

Reduce RHS:

[2]	b(aaba)
[3]	⇒ (bba)
	⇒ c

Referenced by [8].

[7] bc=cba

Overlap of [3] bba=c with [2] aaba=ba:

bb a aaba

Critical pair: bbba=caba.

Reduce LHS:

[3]	b(bba)
	⇒ bc

Reduce RHS:

[5]	c(aba)
	⇒ cba

Defines rule #5.

[8] ac=c

Overlap of [1] aaa=aa with [6] aac=c:

a aa aac

Critical pair: ac=aac.

Reduce RHS:

[6]	(aac)
	⇒ c

Defines rule #3.