Certificate for #5308 ⟨a, b | abaabab=aaab⟩

Completion settings:

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

[1] abaabab=aaab

Axiom: abaabab=aaab.

Referenced by [3].

[2] aaab=c

Axiom: aaab=c.

Defines rule #1.

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

[3] abaabab=c

Simplify [1] abaabab=aaab.

Reduce RHS:

[2]	(aaab)
	⇒ c

Defines rule #5.

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

[4] caabab=abaabc

Overlap of [3] abaabab=c with [3] abaabab=c:

abaab ab abaabab

Critical pair: abaabc=caabab.

Flip LHS and RHS.

Referenced by [5], [8].

[5] abaabc=aac

Overlap of [2] aaab=c with [3] abaabab=c:

aa ab abaabab

Critical pair: aac=caabab.

Reduce RHS:

[4]	(caabab)
	⇒ abaabc

Flip LHS and RHS.

Defines rule #2.

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

[6] abaabaac=caabc

Overlap of [3] abaabab=c with [5] abaabc=aac:

abaab ab abaabc

Critical pair: abaabaac=caabc.

Defines rule #7.

[7] aaaac=caabc

Overlap of [2] aaab=c with [5] abaabc=aac:

aa ab abaabc

Critical pair: aaaac=caabc.

Defines rule #4.

[8] caabab=aac

Simplify [4] caabab=abaabc.

Reduce RHS:

[5]	(abaabc)
	⇒ aac

Defines rule #3.

Referenced by [9].

[9] caabaac=aacaabc

Overlap of [8] caabab=aac with [5] abaabc=aac:

caab ab abaabc

Critical pair: caabaac=aacaabc.

Defines rule #6.