Certificate for #19755 ⟨a, b | aba=b, abbbb=bb⟩

Completion settings:

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

[1] aba=b

Axiom: aba=b.

Defines rule #4.

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

[2] abbbb=bb

Axiom: abbbb=bb.

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

[3] bba=abb

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

ab a aba

Critical pair: abb=bba.

Flip LHS and RHS.

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

[4] abbb=bbbbb

Overlap of [1] aba=b with [2] abbbb=bb:

ab a abbbb

Critical pair: abbb=bbbbb.

Referenced by [5].

[5] abb=bbbbbbbb

Overlap of [2] abbbb=bb with [3] bba=abb:

abb bb bba

Critical pair: abbabb=bba.

Reduce LHS:

[3]	a(bba)bb
[4]	⇒ a(abbb)b
[4]	⇒ (abbb)bbb
	⇒ bbbbbbbb

Reduce RHS:

[3]	(bba)
	⇒ abb

Flip LHS and RHS.

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

[6] bbbbbbbbb=bbbbb

Overlap of [2] abbbb=bb with [3] bba=abb:

abbb b bba

Critical pair: abbbabb=bbba.

Reduce LHS:

[3]	ab(bba)bb
[1]	⇒ (aba)bbbb
	⇒ bbbbb

Reduce RHS:

[3]	b(bba)
[5]	⇒ b(abb)
	⇒ bbbbbbbbb

Flip LHS and RHS.

Referenced by [7].

[7] bbbbbbbb=bbbb

Overlap of [3] bba=abb with [2] abbbb=bb:

bb a abbbb

Critical pair: bbbb=abbbbbb.

Reduce RHS:

[5]	(abb)bbbb
[6]	⇒ (bbbbbbbbb)bbb
	⇒ bbbbbbbb

Flip LHS and RHS.

Referenced by [8].

[8] abb=bbbb

Simplify [5] abb=bbbbbbbb.

Reduce RHS:

[7]	(bbbbbbbb)
	⇒ bbbb

Defines rule #2.

Referenced by [9], [10].

[9] bbbbbb=bb

Overlap of [2] abbbb=bb with [8] abb=bbbb:

abbbb abb

Critical pair: bbbbbb=bb.

Defines rule #1.

[10] bba=bbbb

Simplify [3] bba=abb.

Reduce RHS:

[8]	(abb)
	⇒ bbbb

Defines rule #3.