Certificate for #19268 ⟨a, b | aaa=a, ababa=bb⟩

Completion settings:

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

[1] aaa=a

Axiom: aaa=a.

Defines rule #1.

Referenced by [3], [4].

[2] ababa=bb

Axiom: ababa=bb.

Defines rule #5.

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

[3] aabb=bb

Overlap of [1] aaa=a with [2] ababa=bb:

aa a ababa

Critical pair: aabb=ababa.

Reduce RHS:

[2]	(ababa)
	⇒ bb

Defines rule #2.

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

[4] bbaa=bb

Overlap of [2] ababa=bb with [1] aaa=a:

abab a aaa

Critical pair: ababa=bbaa.

Reduce LHS:

[2]	(ababa)
	⇒ bb

Flip LHS and RHS.

Defines rule #3.

[5] bbba=abbb

Overlap of [2] ababa=bb with [2] ababa=bb:

ab aba ababa

Critical pair: abbb=bbba.

Flip LHS and RHS.

Defines rule #4.

Referenced by [7], [8].

[6] ababbb=bbabb

Overlap of [2] ababa=bb with [3] aabb=bb:

abab a aabb

Critical pair: ababbb=bbabb.

Defines rule #6.

Referenced by [7], [8].

[7] abbabb=babbb

Overlap of [3] aabb=bb with [5] bbba=abbb:

aab b bbba

Critical pair: aababbb=bbbba.

Reduce LHS:

[6]	a(ababbb)
	⇒ abbabb

Reduce RHS:

[5]	b(bbba)
	⇒ babbb

Defines rule #7.

[8] bbabba=abbbb

Overlap of [6] ababbb=bbabb with [5] bbba=abbb:

aba bbb bbba

Critical pair: abaabbb=bbabba.

Reduce LHS:

[3]	ab(aabb)b
	⇒ abbbb

Flip LHS and RHS.

Defines rule #8.