Certificate for #5137 ⟨a, b | aabaaba=abaa⟩

Completion settings:

Reduction order:
- Right-to-left recursive path with deg(b) = deg(c) = 0, b < c; deg(a) = 1
Auxiliary generators:
1. aa=c

[1] aabaaba=abaa

Axiom: aabaaba=abaa.

Referenced by [3].

[2] aa=c

Axiom: aa=c.

Defines rule #5.

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

[3] aabaaba=abc

Simplify [1] aabaaba=abaa.

Reduce RHS:

[2]	ab(aa)
	⇒ abc

Referenced by [4].

[4] abc=cbcba

Overlap of [3] aabaaba=abc with [2] aa=c:

aabaaba aa

Critical pair: cbaaba=abc.

Reduce LHS:

[2]	cb(aa)ba
	⇒ cbcba

Flip LHS and RHS.

Defines rule #4.

Referenced by [6], [7].

[5] ac=ca

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

a a aa

Critical pair: ac=ca.

Defines rule #3.

Referenced by [6].

[6] ccbcbaba=cbc

Overlap of [2] aa=c with [4] abc=cbcba:

a a abc

Critical pair: acbcba=cbc.

Reduce LHS:

[5]	(ac)bcba
[4]	⇒ c(abc)ba
	⇒ ccbcbaba

Defines rule #6.

Referenced by [7].

[7] ccbcbcbcba=cbca

Overlap of [6] ccbcbaba=cbc with [2] aa=c:

ccbcbab a aa

Critical pair: ccbcbabc=cbca.

Reduce LHS:

[4]	ccbcb(abc)
	⇒ ccbcbcbcba

Defines rule #2.

Referenced by [8].

[8] ccbcbcbcbc=cbcc

Overlap of [7] ccbcbcbcba=cbca with [2] aa=c:

ccbcbcbcb a aa

Critical pair: ccbcbcbcbc=cbcaa.

Reduce RHS:

[2]	cbc(aa)
	⇒ cbcc

Defines rule #1.