Certificate for #4476 ⟨a, b, c | aba=1, cbcc=b⟩

Completion settings:

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

[1] aba=1

Axiom: aba=1.

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

[2] cbcc=b

Axiom: cbcc=b.

Referenced by [12].

[3] bb=d

Axiom: bb=d.

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

[4] ab=ba

Overlap of [1] aba=1 with [1] aba=1:

ab a aba

Critical pair: ab=ba.

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

[5] bd=db

Overlap of [3] bb=d with [3] bb=d:

b b bb

Critical pair: bd=db.

Referenced by [11].

[6] baa=1

Overlap of [1] aba=1 with [4] ab=ba:

aba ab

Critical pair: baa=1.

Referenced by [9].

[7] b=daa

Overlap of [1] aba=1 with [4] ab=ba:

ab a ab

Critical pair: abba=b.

Reduce LHS:

[4]	(ab)ba
[4]	⇒ b(ab)a
[3]	⇒ (bb)aa
	⇒ daa

Flip LHS and RHS.

Defines rule #6.

Referenced by [8], [9], [10], [11], [12], [14].

[8] ddaaaaa=ad

Overlap of [4] ab=ba with [3] bb=d:

a b bb

Critical pair: ad=bab.

Reduce RHS:

[4]	b(ab)
[7]	⇒ (b)ba
[4]	⇒ da(ab)a
[4]	⇒ d(ab)aa
[7]	⇒ d(b)aaa
	⇒ ddaaaaa

Flip LHS and RHS.

Referenced by [10], [14].

[9] daaaa=1

Simplify [6] baa=1.

Reduce LHS:

[7]	(b)aa
	⇒ daaaa

Defines rule #3.

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

[10] ada=daa

Overlap of [9] daaaa=1 with [4] ab=ba:

daaa a ab

Critical pair: daaaba=b.

Reduce LHS:

[4]	daa(ab)a
[4]	⇒ da(ab)aa
[4]	⇒ d(ab)aaa
[7]	⇒ d(b)aaaa
[8]	⇒ (ddaaaaa)a
	⇒ ada

Reduce RHS:

[7]	(b)
	⇒ daa

Referenced by [14].

[11] daad=ddaa

Simplify [5] bd=db.

Reduce LHS:

[7]	(b)d
	⇒ daad

Reduce RHS:

[7]	d(b)
	⇒ ddaa

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

[12] cdaacc=daa

Simplify [2] cbcc=b.

Reduce LHS:

[7]	c(b)cc
	⇒ cdaacc

Reduce RHS:

[7]	(b)
	⇒ daa

Referenced by [13], [15], [17].

[13] cdaacdaa=dcc

Overlap of [12] cdaacc=daa with [12] cdaacc=daa:

cdaac c cdaacc

Critical pair: cdaacdaa=daadaacc.

Reduce RHS:

[11]	(daad)aacc
[9]	⇒ d(daaaa)cc
	⇒ dcc

Referenced by [15], [16].

[14] ad=da

Overlap of [1] aba=1 with [10] ada=daa:

ab a ada

Critical pair: abdaa=da.

Reduce LHS:

[4]	(ab)daa
[10]	⇒ b(ada)a
[7]	⇒ (b)daaa
[11]	⇒ (daad)aaa
[8]	⇒ (ddaaaaa)
	⇒ ad

Defines rule #4.

Referenced by [18], [19], [20], [21].

[15] cd=dcccc

Overlap of [13] cdaacdaa=dcc with [12] cdaacc=daa:

cdaa cdaa cdaacc

Critical pair: cdaadaa=dcccc.

Reduce LHS:

[11]	c(daad)aa
[9]	⇒ cd(daaaa)
	⇒ cd

Defines rule #5.

Referenced by [16], [17].

[16] dccccaac=dccaa

Overlap of [13] cdaacdaa=dcc with [9] daaaa=1:

cdaac daa daaaa

Critical pair: cdaac=dccaa.

Reduce LHS:

[15]	(cd)aac
	⇒ dccccaac

Referenced by [17].

[17] dccaac=daa

Overlap of [12] cdaacc=daa with [15] cd=dcccc:

cdaacc cd

Critical pair: dccccaacc=daa.

Reduce LHS:

[16]	(dccccaac)c
	⇒ dccaac

Referenced by [18].

[18] daccaac=daaa

Overlap of [14] ad=da with [17] dccaac=daa:

a d dccaac

Critical pair: adaa=daccaac.

Reduce LHS:

[14]	(ad)aa
	⇒ daaa

Flip LHS and RHS.

Referenced by [19].

[19] daaccaac=1

Overlap of [14] ad=da with [18] daccaac=daaa:

a d daccaac

Critical pair: adaaa=daaccaac.

Reduce LHS:

[14]	(ad)aaa
[9]	⇒ (daaaa)
	⇒ 1

Flip LHS and RHS.

Referenced by [20].

[20] daaaccaac=a

Overlap of [14] ad=da with [19] daaccaac=1:

a d daaccaac

Critical pair: a=daaaccaac.

Flip LHS and RHS.

Referenced by [21].

[21] ccaac=aa

Overlap of [14] ad=da with [20] daaaccaac=a:

a d daaaccaac

Critical pair: aa=daaaaccaac.

Reduce RHS:

[9]	(daaaa)ccaac
	⇒ ccaac

Flip LHS and RHS.

Defines rule #1.

Referenced by [22].

[22] ccaaaa=aacaac

Overlap of [21] ccaac=aa with [21] ccaac=aa:

ccaa c ccaac

Critical pair: ccaaaa=aacaac.

Defines rule #2.