Certificate for #5151 ⟨a, b | aab=ab, bbaa=b⟩

Completion settings:

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

[1] aab=ab

Axiom: aab=ab.

Defines rule #2.

Referenced by [3], [4].

[2] bbaa=b

Axiom: bbaa=b.

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

[3] bbab=bb

Overlap of [2] bbaa=b with [1] aab=ab:

bb aa aab

Critical pair: bbab=bb.

Referenced by [5].

[4] bab=bb

Overlap of [2] bbaa=b with [1] aab=ab:

bba a aab

Critical pair: bbaab=bab.

Reduce LHS:

[2]	(bbaa)b
	⇒ bb

Flip LHS and RHS.

Referenced by [5], [8].

[5] bbb=bb

Overlap of [4] bab=bb with [4] bab=bb:

ba b bab

Critical pair: babb=bbab.

Reduce LHS:

[4]	(bab)b
	⇒ bbb

Reduce RHS:

[3]	(bbab)
	⇒ bb

Referenced by [6].

[6] bb=b

Overlap of [5] bbb=bb with [2] bbaa=b:

b bb bbaa

Critical pair: bb=bbaa.

Reduce RHS:

[2]	(bbaa)
	⇒ b

Defines rule #1.

Referenced by [7], [8].

[7] baa=b

Overlap of [2] bbaa=b with [6] bb=b:

bbaa bb

Critical pair: baa=b.

Defines rule #3.

[8] bab=b

Simplify [4] bab=bb.

Reduce RHS:

[6]	(bb)
	⇒ b

Defines rule #4.