Certificate for #5686 ⟨a, b | aababa=abaab⟩

Completion settings:

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

[1] aababa=abaab

Axiom: aababa=abaab.

Defines rule #13.

Referenced by [3], [4], [5], [6], [9], [13], [15], [21], [22], [23].

[2] babaab=c

Axiom: babaab=c.

Defines rule #16.

Referenced by [3], [4], [5], [7], [10], [11], [12], [13], [23], [25], [26], [27], [29], [30], [31], [32].

[3] abaabab=aac

Overlap of [1] aababa=abaab with [2] babaab=c:

aa baba babaab

Critical pair: aac=abaabab.

Flip LHS and RHS.

Defines rule #17.

Referenced by [11], [12], [13], [14], [22].

[4] abaabbaab=aabac

Overlap of [1] aababa=abaab with [2] babaab=c:

aaba ba babaab

Critical pair: aabac=abaabbaab.

Flip LHS and RHS.

Defines rule #20.

Referenced by [31], [32].

[5] caba=bac

Overlap of [2] babaab=c with [1] aababa=abaab:

bab aab aababa

Critical pair: bababaab=caba.

Reduce LHS:

[2]	ba(babaab)
	⇒ bac

Flip LHS and RHS.

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

[6] bacbaab=babacba

Overlap of [5] caba=bac with [1] aababa=abaab:

cab a aababa

Critical pair: cababaab=bacababa.

Reduce LHS:

[5]	(caba)baab
	⇒ bacbaab

Reduce RHS:

[5]	ba(caba)ba
	⇒ babacba

Referenced by [7].

[7] babacba=cac

Overlap of [5] caba=bac with [2] babaab=c:

ca ba babaab

Critical pair: cac=bacbaab.

Reduce RHS:

[6]	(bacbaab)
	⇒ babacba

Flip LHS and RHS.

Referenced by [8], [9], [10], [16].

[8] bacbacba=cacac

Overlap of [5] caba=bac with [7] babacba=cac:

ca ba babacba

Critical pair: cacac=bacbacba.

Flip LHS and RHS.

Referenced by [23].

[9] cacbaab=baccba

Overlap of [7] babacba=cac with [1] aababa=abaab:

babacb a aababa

Critical pair: babacbabaab=cacababa.

Reduce LHS:

[7]	(babacba)baab
	⇒ cacbaab

Reduce RHS:

[5]	ca(caba)ba
[5]	⇒ (caba)cba
	⇒ baccba

Referenced by [10].

[10] baccba=babacc

Overlap of [7] babacba=cac with [2] babaab=c:

babac ba babaab

Critical pair: babacc=cacbaab.

Reduce RHS:

[9]	(cacbaab)
	⇒ baccba

Flip LHS and RHS.

Referenced by [23].

[11] cab=baac

Overlap of [2] babaab=c with [3] abaabab=aac:

b abaab abaabab

Critical pair: baac=cab.

Flip LHS and RHS.

Defines rule #6.

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

[12] caabab=babaaac

Overlap of [2] babaab=c with [3] abaabab=aac:

baba ab abaabab

Critical pair: babaaac=caabab.

Flip LHS and RHS.

Defines rule #14.

[13] aaca=ac

Overlap of [3] abaabab=aac with [1] aababa=abaab:

ab aabab aababa

Critical pair: ababaab=aaca.

Reduce LHS:

[2]	a(babaab)
	⇒ ac

Flip LHS and RHS.

Defines rule #1.

Referenced by [14], [15], [16], [17], [18], [19], [20], [22], [23], [26].

[14] babacb=caac

Overlap of [5] caba=bac with [3] abaabab=aac:

c aba abaabab

Critical pair: caac=bacabab.

Reduce RHS:

[11]	ba(cab)ab
[13]	⇒ bab(aaca)b
	⇒ babacb

Flip LHS and RHS.

Referenced by [16].

[15] abaabaca=abaabc

Overlap of [1] aababa=abaab with [13] aaca=ac:

aabab a aaca

Critical pair: aababac=abaabaca.

Reduce LHS:

[1]	(aababa)c
	⇒ abaabc

Flip LHS and RHS.

Defines rule #10.

Referenced by [29], [30].

[16] cacaca=cacc

Overlap of [7] babacba=cac with [13] aaca=ac:

babacb a aaca

Critical pair: babacbac=cacaca.

Reduce LHS:

[14]	(babacb)ac
[13]	⇒ c(aaca)c
	⇒ cacc

Flip LHS and RHS.

Referenced by [24].

[17] acaca=acc

Overlap of [13] aaca=ac with [13] aaca=ac:

aac a aaca

Critical pair: aacac=acaca.

Reduce LHS:

[13]	(aaca)c
	⇒ acc

Flip LHS and RHS.

Referenced by [19], [20], [28].

[18] acb=aabaac

Overlap of [13] aaca=ac with [11] cab=baac:

aa ca cab

Critical pair: aabaac=acb.

Flip LHS and RHS.

Defines rule #5.

Referenced by [22], [23].

[19] acca=aacc

Overlap of [13] aaca=ac with [17] acaca=acc:

a aca acaca

Critical pair: aacc=acca.

Flip LHS and RHS.

Defines rule #2.

Referenced by [21], [27].

[20] accb=abacac

Overlap of [17] acaca=acc with [11] cab=baac:

aca ca cab

Critical pair: acabaac=accb.

Reduce LHS:

[11]	a(cab)aac
[13]	⇒ ab(aaca)ac
	⇒ abacac

Flip LHS and RHS.

Referenced by [27].

[21] abaabcca=abaabacc

Overlap of [1] aababa=abaab with [19] acca=aacc:

aabab a acca

Critical pair: aababaacc=abaabcca.

Reduce LHS:

[1]	(aababa)acc
	⇒ abaabacc

Flip LHS and RHS.

Defines rule #11.

[22] abaabcb=acac

Overlap of [1] aababa=abaab with [18] acb=aabaac:

aabab a acb

Critical pair: aababaabaac=abaabcb.

Reduce LHS:

[1]	(aababa)abaac
[3]	⇒ (abaabab)aac
[13]	⇒ (aaca)ac
	⇒ acac

Flip LHS and RHS.

Defines rule #18.

Referenced by [25], [26].

[23] cacac=ccc

Overlap of [8] bacbacba=cacac with [18] acb=aabaac:

b acbacba acb

Critical pair: baabaacacba=cacac.

Reduce LHS:

[13]	baab(aaca)cba
[10]	⇒ baa(baccba)
[1]	⇒ b(aababa)cc
[2]	⇒ (babaab)cc
	⇒ ccc

Flip LHS and RHS.

Referenced by [24], [27].

[24] ccca=cacc

Overlap of [16] cacaca=cacc with [23] cacac=ccc:

cacaca cacac

Critical pair: ccca=cacc.

Defines rule #4.

Referenced by [27].

[25] ccb=bacac

Overlap of [2] babaab=c with [22] abaabcb=acac:

b abaab abaabcb

Critical pair: bacac=ccb.

Flip LHS and RHS.

Defines rule #7.

[26] caabcb=babacc

Overlap of [2] babaab=c with [22] abaabcb=acac:

baba ab abaabcb

Critical pair: babaacac=caabcb.

Reduce LHS:

[13]	bab(aaca)c
	⇒ babacc

Flip LHS and RHS.

Defines rule #15.

Referenced by [27].

[27] caabacac=caabcc

Overlap of [26] caabcb=babacc with [2] babaab=c:

caabc b babaab

Critical pair: caabcc=babaccabaab.

Reduce RHS:

[19]	bab(acca)baab
[20]	⇒ baba(accb)aab
[2]	⇒ (babaab)acacaab
[23]	⇒ (cacac)aab
[24]	⇒ (ccca)ab
[19]	⇒ c(acca)b
[20]	⇒ ca(accb)
	⇒ caabacac

Flip LHS and RHS.

Referenced by [28].

[28] caabcca=caabacc

Overlap of [27] caabacac=caabcc with [17] acaca=acc:

caab acac acaca

Critical pair: caabacc=caabcca.

Flip LHS and RHS.

Defines rule #9.

[29] caca=cc

Overlap of [2] babaab=c with [15] abaabaca=abaabc:

b abaab abaabaca

Critical pair: babaabc=caca.

Reduce LHS:

[2]	(babaab)c
	⇒ cc

Flip LHS and RHS.

Defines rule #3.

[30] caabaca=caabc

Overlap of [2] babaab=c with [15] abaabaca=abaabc:

baba ab abaabaca

Critical pair: babaabaabc=caabaca.

Reduce LHS:

[2]	(babaab)aabc
	⇒ caabc

Flip LHS and RHS.

Defines rule #8.

[31] cbaab=baabac

Overlap of [2] babaab=c with [4] abaabbaab=aabac:

b abaab abaabbaab

Critical pair: baabac=cbaab.

Flip LHS and RHS.

Defines rule #12.

[32] caabbaab=babaaabac

Overlap of [2] babaab=c with [4] abaabbaab=aabac:

baba ab abaabbaab

Critical pair: babaaabac=caabbaab.

Flip LHS and RHS.

Defines rule #19.