Certificate for #4177 ⟨a, b | aabbababa=ba⟩

Completion settings:

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

[1] aabbababa=ba

Axiom: aabbababa=ba.

Referenced by [3].

[2] bba=c

Axiom: bba=c.

Defines rule #2.

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

[3] aacbaba=ba

Overlap of [1] aabbababa=ba with [2] bba=c:

aa bbababa bba

Critical pair: aacbaba=ba.

Defines rule #4.

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

[4] cacbaba=bc

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

bb a aacbaba

Critical pair: bbba=cacbaba.

Reduce LHS:

[2]	b(bba)
	⇒ bc

Flip LHS and RHS.

Defines rule #6.

[5] aacbac=c

Overlap of [3] aacbaba=ba with [3] aacbaba=ba:

aacbab a aacbaba

Critical pair: aacbabba=baacbaba.

Reduce LHS:

[2]	aacba(bba)
	⇒ aacbac

Reduce RHS:

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

Defines rule #1.

Referenced by [6], [7].

[6] bbc=cacbac

Overlap of [2] bba=c with [5] aacbac=c:

bb a aacbac

Critical pair: bbc=cacbac.

Defines rule #3.

Referenced by [8].

[7] aacbabc=bc

Overlap of [3] aacbaba=ba with [5] aacbac=c:

aacbab a aacbac

Critical pair: aacbabc=baacbac.

Reduce RHS:

[5]	b(aacbac)
	⇒ bc

Defines rule #5.

Referenced by [8].

[8] cacbabc=bcacbac

Overlap of [2] bba=c with [7] aacbabc=bc:

bb a aacbabc

Critical pair: bbbc=cacbabc.

Reduce LHS:

[6]	b(bbc)
	⇒ bcacbac

Flip LHS and RHS.

Defines rule #7.