Certificate for #2332 ⟨a, b | abababa=abb⟩

Completion settings:

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

[1] abababa=abb

Axiom: abababa=abb.

Referenced by [3].

[2] abb=c

Axiom: abb=c.

Defines rule #2.

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

[3] abababa=c

Simplify [1] abababa=abb.

Reduce RHS:

[2]	(abb)
	⇒ c

Defines rule #3.

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

[4] abc=cba

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

ab ababa abababa

Critical pair: abc=cba.

Defines rule #1.

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

[5] cbababa=cbb

Overlap of [3] abababa=c with [2] abb=c:

ababab a abb

Critical pair: abababc=cbb.

Reduce LHS:

[4]	abab(abc)
[4]	⇒ ab(abc)ba
[4]	⇒ (abc)baba
	⇒ cbababa

Defines rule #5.

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

[6] cbbba=cbc

Overlap of [3] abababa=c with [4] abc=cba:

ababab a abc

Critical pair: abababcba=cbc.

Reduce LHS:

[4]	abab(abc)ba
[4]	⇒ ab(abc)baba
[4]	⇒ (abc)bababa
[5]	⇒ (cbababa)ba
	⇒ cbbba

Defines rule #4.

Referenced by [7].

[7] cbbbc=cbcbb

Overlap of [6] cbbba=cbc with [3] abababa=c:

cbbb a abababa

Critical pair: cbbbc=cbcbababa.

Reduce RHS:

[5]	cb(cbababa)
	⇒ cbcbb

Defines rule #6.

[8] cbbbb=cbcbaba

Overlap of [5] cbababa=cbb with [2] abb=c:

cbabab a abb

Critical pair: cbababc=cbbbb.

Reduce LHS:

[4]	cbab(abc)
[4]	⇒ cb(abc)ba
	⇒ cbcbaba

Flip LHS and RHS.

Defines rule #7.