Certificate for #4345 ⟨a, b | abbababba=ab⟩

Completion settings:

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

[1] abbababba=ab

Axiom: abbababba=ab.

Referenced by [3].

[2] abb=c

Axiom: abb=c.

Defines rule #8.

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

[3] cabca=ab

Overlap of [1] abbababba=ab with [2] abb=c:

abbababba abb

Critical pair: cababba=ab.

Reduce LHS:

[2]	cab(abb)a
	⇒ cabca

Referenced by [4], [5], [6], [7], [8], [9], [10], [16], [17].

[4] cabcc=cb

Overlap of [3] cabca=ab with [2] abb=c:

cabc a abb

Critical pair: cabcc=abbb.

Reduce RHS:

[2]	(abb)b
	⇒ cb

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

[5] cabab=cca

Overlap of [3] cabca=ab with [3] cabca=ab:

cab ca cabca

Critical pair: cabab=abbca.

Reduce RHS:

[2]	(abb)ca
	⇒ cca

Referenced by [18].

[6] cabcb=ccc

Overlap of [3] cabca=ab with [4] cabcc=cb:

cab ca cabcc

Critical pair: cabcb=abbcc.

Reduce RHS:

[2]	(abb)cc
	⇒ ccc

Referenced by [8], [9].

[7] cbabca=c

Overlap of [4] cabcc=cb with [3] cabca=ab:

cabc c cabca

Critical pair: cabcab=cbabca.

Reduce LHS:

[3]	(cabca)b
[2]	⇒ (abb)
	⇒ c

Flip LHS and RHS.

Referenced by [9], [10], [11].

[8] cbc=ccb

Overlap of [3] cabca=ab with [6] cabcb=ccc:

cab ca cabcb

Critical pair: cabccc=abbcb.

Reduce LHS:

[4]	(cabcc)c
	⇒ cbc

Reduce RHS:

[2]	(abb)cb
	⇒ ccb

Defines rule #1.

Referenced by [10], [12], [13].

[9] cabc=ccab

Overlap of [6] cabcb=ccc with [7] cbabca=c:

cab cb cbabca

Critical pair: cabc=cccabca.

Reduce RHS:

[3]	cc(cabca)
	⇒ ccab

Referenced by [12], [13], [19].

[10] cbab=cc

Overlap of [8] cbc=ccb with [3] cabca=ab:

cb c cabca

Critical pair: cbab=ccbabca.

Reduce RHS:

[7]	c(cbabca)
	⇒ cc

Defines rule #7.

Referenced by [11].

[11] ccca=c

Overlap of [7] cbabca=c with [10] cbab=cc:

cbabca cbab

Critical pair: ccca=c.

Defines rule #3.

Referenced by [12], [13], [14], [15].

[12] ccab=ccba

Overlap of [4] cabcc=cb with [11] ccca=c:

cab cc ccca

Critical pair: cabc=cbca.

Reduce LHS:

[9]	(cabc)
	⇒ ccab

Reduce RHS:

[8]	(cbc)a
	⇒ ccba

Referenced by [13], [15], [16], [19].

[13] ccbac=cccba

Overlap of [4] cabcc=cb with [11] ccca=c:

cabc c ccca

Critical pair: cabcc=cbcca.

Reduce LHS:

[9]	(cabc)c
[12]	⇒ (ccab)c
	⇒ ccbac

Reduce RHS:

[8]	(cbc)ca
[8]	⇒ c(cbc)a
	⇒ cccba

Referenced by [16].

[14] cbb=cccc

Overlap of [11] ccca=c with [2] abb=c:

ccc a abb

Critical pair: cccc=cbb.

Flip LHS and RHS.

Defines rule #2.

[15] cccba=cb

Overlap of [11] ccca=c with [12] ccab=ccba:

c cca ccab

Critical pair: cccba=cb.

Defines rule #4.

Referenced by [16].

[16] cab=cba

Overlap of [12] ccab=ccba with [3] cabca=ab:

c cab cabca

Critical pair: cab=ccbaca.

Reduce RHS:

[13]	(ccbac)a
[15]	⇒ (cccba)a
	⇒ cba

Defines rule #6.

Referenced by [17], [18], [20].

[17] cbaca=ab

Overlap of [3] cabca=ab with [16] cab=cba:

cabca cab

Critical pair: cbaca=ab.

Referenced by [21].

[18] cbaab=cca

Overlap of [5] cabab=cca with [16] cab=cba:

cabab cab

Critical pair: cbaab=cca.

Defines rule #10.

[19] cabc=ccba

Simplify [9] cabc=ccab.

Reduce RHS:

[12]	(ccab)
	⇒ ccba

Referenced by [20].

[20] cbac=ccba

Overlap of [19] cabc=ccba with [16] cab=cba:

cabc cab

Critical pair: cbac=ccba.

Defines rule #5.

Referenced by [21].

[21] ccbaa=ab

Simplify [17] cbaca=ab.

Reduce LHS:

[20]	(cbac)a
	⇒ ccbaa

Defines rule #9.