Certificate for #4043 ⟨a, b | aaabbbaba=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] aaabbbaba=ba

Axiom: aaabbbaba=ba.

Referenced by [3].

[2] bba=c

Axiom: bba=c.

Defines rule #2.

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

[3] aaabcba=ba

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

aaab bbaba bba

Critical pair: aaabcba=ba.

Defines rule #4.

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

[4] caabcba=bc

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

bb a aaabcba

Critical pair: bbba=caabcba.

Reduce LHS:

[2]	b(bba)
	⇒ bc

Flip LHS and RHS.

Defines rule #6.

[5] aaabcc=c

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

aaabcb a aaabcba

Critical pair: aaabcbba=baaabcba.

Reduce LHS:

[2]	aaabc(bba)
	⇒ aaabcc

Reduce RHS:

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

Defines rule #1.

Referenced by [6], [7].

[6] bbc=caabcc

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

bb a aaabcc

Critical pair: bbc=caabcc.

Defines rule #3.

Referenced by [8].

[7] aaabcbc=bc

Overlap of [3] aaabcba=ba with [5] aaabcc=c:

aaabcb a aaabcc

Critical pair: aaabcbc=baaabcc.

Reduce RHS:

[5]	b(aaabcc)
	⇒ bc

Defines rule #5.

Referenced by [8].

[8] caabcbc=bcaabcc

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

bb a aaabcbc

Critical pair: bbbc=caabcbc.

Reduce LHS:

[6]	b(bbc)
	⇒ bcaabcc

Flip LHS and RHS.

Defines rule #7.