Certificate for #4183 ⟨a, b | baa=abb, bbb=b⟩

Completion settings:

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

[1] baa=abb

Axiom: baa=abb.

Defines rule #1.

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

[2] bbb=b

Axiom: bbb=b.

Defines rule #3.

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

[3] bbabb=abb

Overlap of [2] bbb=b with [1] baa=abb:

bb b baa

Critical pair: bbabb=baa.

Reduce RHS:

[1]	(baa)
	⇒ abb

Referenced by [4], [5].

[4] bbab=ab

Overlap of [3] bbabb=abb with [2] bbb=b:

bba bb bbb

Critical pair: bbab=abbb.

Reduce RHS:

[2]	a(bbb)
	⇒ ab

Referenced by [5], [7].

[5] babb=aabb

Overlap of [3] bbabb=abb with [3] bbabb=abb:

bba bb bbabb

Critical pair: bbaabb=abbabb.

Reduce LHS:

[1]	b(baa)bb
[2]	⇒ ba(bbb)b
	⇒ babb

Reduce RHS:

[4]	a(bbab)b
	⇒ aabb

Referenced by [6], [7].

[6] bab=aab

Overlap of [5] babb=aabb with [2] bbb=b:

ba bb bbb

Critical pair: bab=aabbb.

Reduce RHS:

[2]	aa(bbb)
	⇒ aab

Defines rule #2.

[7] aaab=ab

Overlap of [5] babb=aabb with [4] bbab=ab:

ba bb bbab

Critical pair: baab=aabbab.

Reduce LHS:

[1]	(baa)b
[2]	⇒ a(bbb)
	⇒ ab

Reduce RHS:

[4]	aa(bbab)
	⇒ aaab

Flip LHS and RHS.

Defines rule #4.