Certificate for #19733 ⟨a, b | aba=b, aabbb=bb⟩

Completion settings:

Reduction order:
- Left-to-right shortlex with a < b

[1] aba=b

Axiom: aba=b.

Defines rule #1.

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

[2] aabbb=bb

Axiom: aabbb=bb.

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

[3] bba=abb

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

ab a aba

Critical pair: abb=bba.

Flip LHS and RHS.

Defines rule #2.

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

[4] abbb=abb

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

aab bb bba

Critical pair: aababb=bba.

Reduce LHS:

[1]	a(aba)bb
	⇒ abbb

Reduce RHS:

[3]	(bba)
	⇒ abb

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

[5] babb=abb

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

aabb b bba

Critical pair: aabbabb=bbba.

Reduce LHS:

[3]	aa(bba)bb
[2]	⇒ a(aabbb)b
[4]	⇒ (abbb)
	⇒ abb

Reduce RHS:

[3]	b(bba)
	⇒ babb

Flip LHS and RHS.

Defines rule #5.

[6] bbbb=bbb

Overlap of [1] aba=b with [4] abbb=abb:

ab a abbb

Critical pair: ababb=bbbb.

Reduce LHS:

[1]	(aba)bb
	⇒ bbb

Flip LHS and RHS.

Referenced by [8].

[7] aabb=bbb

Overlap of [4] abbb=abb with [3] bba=abb:

ab bb bba

Critical pair: ababb=abba.

Reduce LHS:

[1]	(aba)bb
	⇒ bbb

Reduce RHS:

[3]	a(bba)
	⇒ aabb

Flip LHS and RHS.

Referenced by [8], [9].

[8] bbb=bb

Overlap of [2] aabbb=bb with [7] aabb=bbb:

aabbb aabb

Critical pair: bbbb=bb.

Reduce LHS:

[6]	(bbbb)
	⇒ bbb

Defines rule #3.

Referenced by [9].

[9] aabb=bb

Simplify [7] aabb=bbb.

Reduce RHS:

[8]	(bbb)
	⇒ bb

Defines rule #4.