Certificate for #16300 ⟨a, b | aab=bb, abba=bb⟩

Completion settings:

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

[1] aab=bb

Axiom: aab=bb.

Defines rule #1.

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

[2] abba=bb

Axiom: abba=bb.

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

[3] bbba=abb

Overlap of [1] aab=bb with [2] abba=bb:

a ab abba

Critical pair: abb=bbba.

Flip LHS and RHS.

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

[4] babb=abbb

Overlap of [1] aab=bb with [3] bbba=abb:

aa b bbba

Critical pair: aaabb=bbbba.

Reduce LHS:

[1]	a(aab)b
	⇒ abbb

Reduce RHS:

[3]	b(bbba)
	⇒ babb

Flip LHS and RHS.

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

[5] bbbbb=bbb

Overlap of [3] bbba=abb with [1] aab=bb:

bbb a aab

Critical pair: bbbbb=abbab.

Reduce RHS:

[2]	(abba)b
	⇒ bbb

Referenced by [6].

[6] bbbb=bbb

Overlap of [2] abba=bb with [4] babb=abbb:

ab ba babb

Critical pair: ababbb=bbbb.

Reduce LHS:

[4]	a(babb)b
[1]	⇒ (aab)bbb
[5]	⇒ (bbbbb)
	⇒ bbb

Flip LHS and RHS.

Referenced by [7].

[7] abbb=abb

Overlap of [6] bbbb=bbb with [3] bbba=abb:

b bbb bbba

Critical pair: babb=bbba.

Reduce LHS:

[4]	(babb)
	⇒ abbb

Reduce RHS:

[3]	(bbba)
	⇒ abb

Referenced by [8], [10].

[8] bbb=bb

Overlap of [7] abbb=abb with [3] bbba=abb:

a bbb bbba

Critical pair: aabb=abba.

Reduce LHS:

[1]	(aab)b
	⇒ bbb

Reduce RHS:

[2]	(abba)
	⇒ bb

Defines rule #3.

Referenced by [9].

[9] bba=abb

Overlap of [3] bbba=abb with [8] bbb=bb:

bbba bbb

Critical pair: bba=abb.

Defines rule #2.

[10] babb=abb

Simplify [4] babb=abbb.

Reduce RHS:

[7]	(abbb)
	⇒ abb

Defines rule #4.