Certificate for #4792 ⟨a, b | abaababa=aab⟩

Completion settings:

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

[1] abaababa=aab

Axiom: abaababa=aab.

Referenced by [3].

[2] ababa=c

Axiom: ababa=c.

Defines rule #7.

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

[3] aab=abac

Overlap of [1] abaababa=aab with [2] ababa=c:

aba ababa ababa

Critical pair: abac=aab.

Flip LHS and RHS.

Defines rule #3.

Referenced by [5], [6].

[4] cba=abc

Overlap of [2] ababa=c with [2] ababa=c:

ab aba ababa

Critical pair: abc=cba.

Flip LHS and RHS.

Defines rule #2.

Referenced by [5].

[5] cab=abcc

Overlap of [2] ababa=c with [3] aab=abac:

abab a aab

Critical pair: abababac=cab.

Reduce LHS:

[2]	(ababa)bac
[4]	⇒ (cba)c
	⇒ abcc

Flip LHS and RHS.

Defines rule #5.

Referenced by [6], [7].

[6] cccca=ac

Overlap of [3] aab=abac with [2] ababa=c:

a ab ababa

Critical pair: ac=abacaba.

Reduce RHS:

[5]	aba(cab)a
[3]	⇒ ab(aab)cca
[2]	⇒ (ababa)ccca
	⇒ cccca

Flip LHS and RHS.

Defines rule #1.

Referenced by [7].

[7] acb=abcccccccc

Overlap of [6] cccca=ac with [5] cab=abcc:

ccc ca cab

Critical pair: cccabcc=acb.

Reduce LHS:

[5]	cc(cab)cc
[5]	⇒ c(cab)cccc
[5]	⇒ (cab)cccccc
	⇒ abcccccccc

Flip LHS and RHS.

Defines rule #4.

Referenced by [8].

[8] ccb=cbcccccccc

Overlap of [2] ababa=c with [7] acb=abcccccccc:

abab a acb

Critical pair: abababcccccccc=ccb.

Reduce LHS:

[2]	(ababa)bcccccccc
	⇒ cbcccccccc

Flip LHS and RHS.

Defines rule #6.