Certificate for #19614 ⟨a, b | aab=b, bbabb=ba⟩

Completion settings:

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

[1] aab=b

Axiom: aab=b.

Defines rule #2.

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

[2] bbabb=ba

Axiom: bbabb=ba.

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

[3] bbaba=bbb

Overlap of [2] bbabb=ba with [2] bbabb=ba:

bba bb bbabb

Critical pair: bbaba=baabb.

Reduce RHS:

[1]	b(aab)b
	⇒ bbb

Referenced by [4], [6].

[4] bab=bba

Overlap of [2] bbabb=ba with [3] bbaba=bbb:

bba bb bbaba

Critical pair: bbabbb=baaba.

Reduce LHS:

[2]	(bbabb)b
	⇒ bab

Reduce RHS:

[1]	b(aab)a
	⇒ bba

Defines rule #1.

Referenced by [5], [6].

[5] bbaa=bb

Overlap of [2] bbabb=ba with [4] bab=bba:

bbab b bab

Critical pair: bbabbba=baab.

Reduce LHS:

[2]	(bbabb)ba
[4]	⇒ (bab)a
	⇒ bbaa

Reduce RHS:

[1]	b(aab)
	⇒ bb

Defines rule #4.

Referenced by [7].

[6] bbbb=baa

Overlap of [3] bbaba=bbb with [4] bab=bba:

bba ba bab

Critical pair: bbabba=bbbb.

Reduce LHS:

[2]	(bbabb)a
	⇒ baa

Flip LHS and RHS.

Defines rule #3.

[7] baaa=ba

Overlap of [2] bbabb=ba with [5] bbaa=bb:

bba bb bbaa

Critical pair: bbabb=baaa.

Reduce LHS:

[2]	(bbabb)
	⇒ ba

Flip LHS and RHS.

Defines rule #5.