Certificate for #11515 ⟨a, b | ababa=b, abbaa=1⟩

Completion settings:

Reduction order:
- Left-to-right recursive path with deg(a) = 0; deg(b) = 1

[1] ababa=b

Axiom: ababa=b.

Referenced by [3], [4], [5], [9], [11], [13].

[2] abbaa=1

Axiom: abbaa=1.

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

[3] abb=bba

Overlap of [1] ababa=b with [1] ababa=b:

ab aba ababa

Critical pair: abb=bba.

Referenced by [5], [6], [7], [8], [9], [10], [11], [14], [15].

[4] bbbaa=abab

Overlap of [1] ababa=b with [2] abbaa=1:

abab a abbaa

Critical pair: abab=bbbaa.

Flip LHS and RHS.

Referenced by [7], [11].

[5] bbaab=baba

Overlap of [2] abbaa=1 with [1] ababa=b:

abba a ababa

Critical pair: abbab=baba.

Reduce LHS:

[3]	(abb)ab
	⇒ bbaab

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

[6] bbaaa=1

Overlap of [2] abbaa=1 with [3] abb=bba:

abbaa abb

Critical pair: bbaaa=1.

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

[7] bbabaa=aabab

Overlap of [3] abb=bba with [4] bbbaa=abab:

a bb bbbaa

Critical pair: aabab=bbabaa.

Flip LHS and RHS.

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

[8] aaabab=babaaa

Overlap of [3] abb=bba with [7] bbabaa=aabab:

a bb bbabaa

Critical pair: aaabab=bbaabaa.

Reduce RHS:

[5]	(bbaab)aa
	⇒ babaaa

Referenced by [11].

[9] abaabab=bbba

Overlap of [3] abb=bba with [7] bbabaa=aabab:

ab b bbabaa

Critical pair: abaabab=bbababaa.

Reduce RHS:

[1]	bb(ababa)a
	⇒ bbba

Referenced by [10], [11].

[10] bbbbba=babaaab

Overlap of [7] bbabaa=aabab with [9] abaabab=bbba:

bb abaa abaabab

Critical pair: bbbbba=aababbab.

Reduce RHS:

[3]	aab(abb)ab
[3]	⇒ a(abb)baab
[3]	⇒ (abb)abaab
[5]	⇒ (bbaab)aab
	⇒ babaaab

Referenced by [12].

[11] bbbbb=b

Overlap of [7] bbabaa=aabab with [9] abaabab=bbba:

bbaba a abaabab

Critical pair: bbababbba=aababbaabab.

Reduce LHS:

[3]	bbab(abb)ba
[3]	⇒ bb(abb)baba
[1]	⇒ bbbb(ababa)
	⇒ bbbbb

Reduce RHS:

[3]	aab(abb)aabab
[3]	⇒ a(abb)baaabab
[3]	⇒ (abb)abaaabab
[5]	⇒ (bbaab)aaabab
[8]	⇒ baba(aaabab)
[1]	⇒ b(ababa)baaa
[4]	⇒ (bbbaa)a
[1]	⇒ (ababa)
	⇒ b

Referenced by [12].

[12] babaaab=ba

Overlap of [10] bbbbba=babaaab with [11] bbbbb=b:

bbbbba bbbbb

Critical pair: ba=babaaab.

Flip LHS and RHS.

Referenced by [13], [14].

[13] baab=aba

Overlap of [1] ababa=b with [12] babaaab=ba:

a baba babaaab

Critical pair: aba=baab.

Flip LHS and RHS.

Defines rule #5.

Referenced by [14], [15].

[14] bab=aabaa

Overlap of [12] babaaab=ba with [3] abb=bba:

babaa ab abb

Critical pair: babaabba=bab.

Reduce LHS:

[13]	ba(baab)ba
[13]	⇒ (baab)aba
[13]	⇒ a(baab)a
	⇒ aabaa

Flip LHS and RHS.

Defines rule #4.

Referenced by [15].

[15] bbba=aaaba

Overlap of [14] bab=aabaa with [3] abb=bba:

b ab abb

Critical pair: bbba=aabaab.

Reduce RHS:

[13]	aa(baab)
	⇒ aaaba

Referenced by [16], [18].

[16] aaabaaa=b

Overlap of [15] bbba=aaaba with [6] bbaaa=1:

b bba bbaaa

Critical pair: b=aaabaaa.

Flip LHS and RHS.

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

[17] bbb=baaa

Overlap of [6] bbaaa=1 with [16] aaabaaa=b:

bb aaa aaabaaa

Critical pair: bbb=baaa.

Referenced by [18].

[18] baaab=1

Overlap of [15] bbba=aaaba with [16] aaabaaa=b:

bbb a aaabaaa

Critical pair: bbbb=aaabaaabaaa.

Reduce LHS:

[17]	(bbb)b
	⇒ baaab

Reduce RHS:

[16]	(aaabaaa)baaa
[6]	⇒ (bbaaa)
	⇒ 1

Referenced by [19].

[19] bb=aaa

Overlap of [16] aaabaaa=b with [18] baaab=1:

aaa baaa baaab

Critical pair: aaa=bb.

Flip LHS and RHS.

Defines rule #3.

Referenced by [20], [21].

[20] aaaaaa=1

Overlap of [6] bbaaa=1 with [19] bb=aaa:

bbaaa bb

Critical pair: aaaaaa=1.

Defines rule #1.

[21] aaab=baaa

Overlap of [19] bb=aaa with [19] bb=aaa:

b b bb

Critical pair: baaa=aaab.

Flip LHS and RHS.

Defines rule #2.