Certificate for #19595 ⟨a, b | aab=b, babba=bb⟩

Completion settings:

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

[1] aab=b

Axiom: aab=b.

Defines rule #6.

Referenced by [3], [7].

[2] babba=bb

Axiom: babba=bb.

Defines rule #5.

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

[3] babbb=bbab

Overlap of [2] babba=bb with [1] aab=b:

babb a aab

Critical pair: babbb=bbab.

Referenced by [4], [6].

[4] bbab=bbbba

Overlap of [2] babba=bb with [2] babba=bb:

bab ba babba

Critical pair: babbb=bbbba.

Reduce LHS:

[3]	(babbb)
	⇒ bbab

Defines rule #2.

Referenced by [5], [6], [7], [9].

[5] bbbbbbaa=bbb

Overlap of [4] bbab=bbbba with [2] babba=bb:

b bab babba

Critical pair: bbb=bbbbaba.

Reduce RHS:

[4]	bb(bbab)a
	⇒ bbbbbbaa

Flip LHS and RHS.

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

[6] babbb=bbbba

Simplify [3] babbb=bbab.

Reduce RHS:

[4]	(bbab)
	⇒ bbbba

Defines rule #3.

Referenced by [7], [9].

[7] bbbbbbb=bbbb

Overlap of [4] bbab=bbbba with [6] babbb=bbbba:

bba b babbb

Critical pair: bbabbbba=bbbbaabbb.

Reduce LHS:

[6]	b(babbb)ba
[4]	⇒ bbb(bbab)a
[5]	⇒ b(bbbbbbaa)
	⇒ bbbb

Reduce RHS:

[1]	bbbb(aab)bb
	⇒ bbbbbbb

Flip LHS and RHS.

Referenced by [8].

[8] bbbbaa=bbbb

Overlap of [7] bbbbbbb=bbbb with [5] bbbbbbaa=bbb:

b bbbbbb bbbbbbaa

Critical pair: bbbb=bbbbaa.

Flip LHS and RHS.

Referenced by [9], [11].

[9] bbbbbba=bbba

Overlap of [6] babbb=bbbba with [8] bbbbaa=bbbb:

ba bbb bbbbaa

Critical pair: babbbb=bbbbabaa.

Reduce LHS:

[6]	(babbb)b
[4]	⇒ bb(bbab)
	⇒ bbbbbba

Reduce RHS:

[4]	bb(bbab)aa
[5]	⇒ (bbbbbbaa)a
	⇒ bbba

Referenced by [10], [11].

[10] bbbaa=bbb

Overlap of [5] bbbbbbaa=bbb with [9] bbbbbba=bbba:

bbbbbbaa bbbbbba

Critical pair: bbbaa=bbb.

Defines rule #4.

Referenced by [11].

[11] bbbbbb=bbb

Overlap of [9] bbbbbba=bbba with [8] bbbbaa=bbbb:

bb bbbba bbbbaa

Critical pair: bbbbbb=bbbaa.

Reduce RHS:

[10]	(bbbaa)
	⇒ bbb

Defines rule #1.