Certificate for #13190 ⟨a, b | abb=aaa, bbb=aa⟩

Completion settings:

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

[1] aaa=abb

Axiom: abb=aaa.

Flip LHS and RHS.

Referenced by [3].

[2] aa=bbb

Axiom: bbb=aa.

Flip LHS and RHS.

Defines rule #5.

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

[3] abb=bbba

Overlap of [1] aaa=abb with [2] aa=bbb:

aaa aa

Critical pair: bbba=abb.

Flip LHS and RHS.

Defines rule #4.

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

[4] bbbab=bbba

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

a a aa

Critical pair: abbb=bbba.

Reduce LHS:

[3]	(abb)b
	⇒ bbbab

Defines rule #3.

Referenced by [5], [6].

[5] bbbbbb=bbbbb

Overlap of [2] aa=bbb with [3] abb=bbba:

a a abb

Critical pair: abbba=bbbbb.

Reduce LHS:

[3]	(abb)ba
[4]	⇒ (bbbab)a
[2]	⇒ bbb(aa)
	⇒ bbbbbb

Defines rule #1.

Referenced by [6], [7].

[6] bbbbba=bbba

Overlap of [4] bbbab=bbba with [3] abb=bbba:

bbb ab abb

Critical pair: bbbbbba=bbbab.

Reduce LHS:

[5]	(bbbbbb)a
	⇒ bbbbba

Reduce RHS:

[4]	(bbbab)
	⇒ bbba

Referenced by [7].

[7] bbbba=bbba

Overlap of [5] bbbbbb=bbbbb with [6] bbbbba=bbba:

b bbbbb bbbbba

Critical pair: bbbba=bbbbba.

Reduce RHS:

[6]	(bbbbba)
	⇒ bbba

Defines rule #2.