Certificate for #13259 ⟨a, b | bab=aba, bbb=aa⟩

Completion settings:

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

[1] aba=bab

Axiom: bab=aba.

Flip LHS and RHS.

Defines rule #7.

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

[2] aa=bbb

Axiom: bbb=aa.

Flip LHS and RHS.

Defines rule #6.

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

[3] bbba=abbb

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

a a aa

Critical pair: abbb=bbba.

Flip LHS and RHS.

Defines rule #5.

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

[4] babba=abbab

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

ab a aba

Critical pair: abbab=babba.

Flip LHS and RHS.

Referenced by [7], [8].

[5] bbab=abbbb

Overlap of [1] aba=bab with [2] aa=bbb:

ab a aa

Critical pair: abbbb=baba.

Reduce RHS:

[1]	b(aba)
	⇒ bbab

Flip LHS and RHS.

Referenced by [7], [8], [9], [10], [12].

[6] babbb=babb

Overlap of [2] aa=bbb with [1] aba=bab:

a a aba

Critical pair: abab=bbbba.

Reduce LHS:

[1]	(aba)b
	⇒ babb

Reduce RHS:

[3]	b(bbba)
	⇒ babbb

Flip LHS and RHS.

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

[7] abbbbb=bbbbbbb

Overlap of [6] babbb=babb with [3] bbba=abbb:

bab bb bbba

Critical pair: bababbb=babbba.

Reduce LHS:

[1]	b(aba)bbb
[6]	⇒ b(babbb)b
[6]	⇒ b(babbb)
[5]	⇒ (bbab)b
	⇒ abbbbb

Reduce RHS:

[6]	(babbb)a
[4]	⇒ (babba)
[5]	⇒ a(bbab)
[2]	⇒ (aa)bbbb
	⇒ bbbbbbb

Referenced by [10].

[8] bbbbbbbb=bbbbbbb

Overlap of [6] babbb=babb with [3] bbba=abbb:

babb b bbba

Critical pair: babbabbb=babbbba.

Reduce LHS:

[4]	(babba)bbb
[6]	⇒ ab(babbb)b
[6]	⇒ ab(babbb)
[5]	⇒ a(bbab)b
[2]	⇒ (aa)bbbbb
	⇒ bbbbbbbb

Reduce RHS:

[6]	(babbb)ba
[6]	⇒ (babbb)a
[4]	⇒ (babba)
[5]	⇒ a(bbab)
[2]	⇒ (aa)bbbb
	⇒ bbbbbbb

Defines rule #1.

Referenced by [10].

[9] babb=abbbb

Overlap of [3] bbba=abbb with [5] bbab=abbbb:

b bba bbab

Critical pair: babbbb=abbbb.

Reduce LHS:

[6]	(babbb)b
[6]	⇒ (babbb)
	⇒ babb

Referenced by [10], [11].

[10] abbbb=bbbbbbb

Overlap of [5] bbab=abbbb with [1] aba=bab:

bb ab aba

Critical pair: bbbab=abbbba.

Reduce LHS:

[3]	(bbba)b
	⇒ abbbb

Reduce RHS:

[3]	ab(bbba)
[1]	⇒ (aba)bbb
[9]	⇒ (babb)bb
[7]	⇒ (abbbbb)b
[8]	⇒ (bbbbbbbb)
	⇒ bbbbbbb

Defines rule #2.

Referenced by [11], [12].

[11] babb=bbbbbbb

Simplify [9] babb=abbbb.

Reduce RHS:

[10]	(abbbb)
	⇒ bbbbbbb

Defines rule #3.

[12] bbab=bbbbbbb

Simplify [5] bbab=abbbb.

Reduce RHS:

[10]	(abbbb)
	⇒ bbbbbbb

Defines rule #4.