Certificate for #20135 ⟨a, b | aab=b, baba=bbb⟩

Completion settings:

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

[1] aab=b

Axiom: aab=b.

Defines rule #7.

Referenced by [3], [7].

[2] baba=bbb

Axiom: baba=bbb.

Defines rule #6.

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

[3] babb=bbbab

Overlap of [2] baba=bbb with [1] aab=b:

bab a aab

Critical pair: babb=bbbab.

Defines rule #4.

Referenced by [4], [5].

[4] bbbbbab=bbbba

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

ba ba baba

Critical pair: babbb=bbbba.

Reduce LHS:

[3]	(babb)b
[3]	⇒ bb(babb)
	⇒ bbbbbab

Referenced by [5], [6].

[5] bbbbab=bbbbbba

Overlap of [3] babb=bbbab with [2] baba=bbb:

bab b baba

Critical pair: babbbb=bbbababa.

Reduce LHS:

[3]	(babb)bb
[3]	⇒ bb(babb)b
[4]	⇒ (bbbbbab)b
	⇒ bbbbab

Reduce RHS:

[2]	bb(baba)ba
	⇒ bbbbbba

Defines rule #3.

Referenced by [6], [8].

[6] bbbbbbba=bbbba

Simplify [4] bbbbbab=bbbba.

Reduce LHS:

[5]	b(bbbbab)
	⇒ bbbbbbba

Defines rule #2.

Referenced by [7], [9].

[7] bbbbbbbb=bbbbb

Overlap of [6] bbbbbbba=bbbba with [1] aab=b:

bbbbbbb a aab

Critical pair: bbbbbbbb=bbbbaab.

Reduce RHS:

[1]	bbbb(aab)
	⇒ bbbbb

Defines rule #1.

[8] bbbbbbaa=bbbbbb

Overlap of [5] bbbbab=bbbbbba with [2] baba=bbb:

bbb bab baba

Critical pair: bbbbbb=bbbbbbaa.

Flip LHS and RHS.

Referenced by [9].

[9] bbbbaa=bbbbbbb

Overlap of [6] bbbbbbba=bbbba with [8] bbbbbbaa=bbbbbb:

b bbbbbba bbbbbbaa

Critical pair: bbbbbbb=bbbbaa.

Flip LHS and RHS.

Defines rule #5.