Certificate for #16472 ⟨a, b | aba=bb, bbbb=bb⟩

Completion settings:

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

[1] aba=bb

Axiom: aba=bb.

Defines rule #1.

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

[2] bbbb=bb

Axiom: bbbb=bb.

Defines rule #5.

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

[3] bbba=abbb

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

ab a aba

Critical pair: abbb=bbba.

Flip LHS and RHS.

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

[4] babbb=bba

Overlap of [2] bbbb=bb with [3] bbba=abbb:

b bbb bbba

Critical pair: babbb=bba.

Referenced by [9].

[5] abba=bbb

Overlap of [3] bbba=abbb with [1] aba=bb:

bbb a aba

Critical pair: bbbbb=abbbba.

Reduce LHS:

[2]	(bbbb)b
	⇒ bbb

Reduce RHS:

[2]	a(bbbb)a
	⇒ abba

Flip LHS and RHS.

Referenced by [6], [7].

[6] bba=abb

Overlap of [1] aba=bb with [5] abba=bbb:

ab a abba

Critical pair: abbbb=bbbba.

Reduce LHS:

[2]	a(bbbb)
	⇒ abb

Reduce RHS:

[2]	(bbbb)a
	⇒ bba

Flip LHS and RHS.

Defines rule #2.

Referenced by [9].

[7] aabbb=bb

Overlap of [3] bbba=abbb with [5] abba=bbb:

bbb a abba

Critical pair: bbbbbb=abbbbba.

Reduce LHS:

[2]	(bbbb)bb
[2]	⇒ (bbbb)
	⇒ bb

Reduce RHS:

[2]	a(bbbb)ba
[3]	⇒ a(bbba)
	⇒ aabbb

Flip LHS and RHS.

Referenced by [8].

[8] aabb=bbb

Overlap of [7] aabbb=bb with [2] bbbb=bb:

aa bbb bbbb

Critical pair: aabb=bbb.

Defines rule #3.

[9] babbb=abb

Simplify [4] babbb=bba.

Reduce RHS:

[6]	(bba)
	⇒ abb

Referenced by [10].

[10] babb=abbb

Overlap of [9] babbb=abb with [2] bbbb=bb:

ba bbb bbbb

Critical pair: babb=abbb.

Defines rule #4.