Certificate for #2006 ⟨a, b | aabbbaba=ba⟩

Completion settings:

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

[1] aabbbaba=ba

Axiom: aabbbaba=ba.

Referenced by [3].

[2] bba=c

Axiom: bba=c.

Defines rule #2.

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

[3] aabcba=ba

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

aab bbaba bba

Critical pair: aabcba=ba.

Defines rule #4.

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

[4] cabcba=bc

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

bb a aabcba

Critical pair: bbba=cabcba.

Reduce LHS:

[2]	b(bba)
	⇒ bc

Flip LHS and RHS.

Defines rule #6.

[5] aabcc=c

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

aabcb a aabcba

Critical pair: aabcbba=baabcba.

Reduce LHS:

[2]	aabc(bba)
	⇒ aabcc

Reduce RHS:

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

Defines rule #1.

Referenced by [6], [7].

[6] bbc=cabcc

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

bb a aabcc

Critical pair: bbc=cabcc.

Defines rule #3.

Referenced by [8].

[7] aabcbc=bc

Overlap of [3] aabcba=ba with [5] aabcc=c:

aabcb a aabcc

Critical pair: aabcbc=baabcc.

Reduce RHS:

[5]	b(aabcc)
	⇒ bc

Defines rule #5.

Referenced by [8].

[8] cabcbc=bcabcc

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

bb a aabcbc

Critical pair: bbbc=cabcbc.

Reduce LHS:

[6]	b(bbc)
	⇒ bcabcc

Flip LHS and RHS.

Defines rule #7.