Certificate for #4691 ⟨a, b | aabbaaba=baa⟩

Completion settings:

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

[1] aabbaaba=baa

Axiom: aabbaaba=baa.

Referenced by [3].

[2] bbaa=c

Axiom: bbaa=c.

Referenced by [3], [4].

[3] baa=aacba

Overlap of [1] aabbaaba=baa with [2] bbaa=c:

aa bbaaba bbaa

Critical pair: aacba=baa.

Flip LHS and RHS.

Defines rule #3.

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

[4] aacbacba=c

Overlap of [2] bbaa=c with [3] baa=aacba:

b baa baa

Critical pair: baacba=c.

Reduce LHS:

[3]	(baa)cba
	⇒ aacbacba

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

[5] bc=ccba

Overlap of [3] baa=aacba with [4] aacbacba=c:

b aa aacbacba

Critical pair: bc=aacbacbacba.

Reduce RHS:

[4]	(aacbacba)cba
	⇒ ccba

Defines rule #2.

[6] bac=aacccba

Overlap of [3] baa=aacba with [4] aacbacba=c:

ba a aacbacba

Critical pair: bac=aacbaacbacba.

Reduce RHS:

[3]	aac(baa)cbacba
[4]	⇒ aac(aacbacba)cba
	⇒ aacccba

Defines rule #4.

Referenced by [7], [8].

[7] aacaacccaacc=ca

Overlap of [4] aacbacba=c with [3] baa=aacba:

aacbac ba baa

Critical pair: aacbacaacba=ca.

Reduce LHS:

[6]	aac(bac)aacba
[3]	⇒ aacaaccc(baa)acba
[3]	⇒ aacaacccaac(baa)cba
[4]	⇒ aacaacccaac(aacbacba)
	⇒ aacaacccaacc

Defines rule #1.

[8] aacaacccbaba=c

Overlap of [4] aacbacba=c with [6] bac=aacccba:

aac bacba bac

Critical pair: aacaacccbaba=c.

Defines rule #5.