Certificate for #15975 ⟨a, b | aaa=aa, babb=ab⟩

Completion settings:

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

[1] aaa=aa

Axiom: aaa=aa.

Defines rule #1.

Referenced by [5], [7].

[2] babb=ab

Axiom: babb=ab.

Defines rule #3.

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

[3] babab=aab

Overlap of [2] babb=ab with [2] babb=ab:

bab b babb

Critical pair: babab=ababb.

Reduce RHS:

[2]	a(babb)
	⇒ aab

Defines rule #6.

Referenced by [4], [5].

[4] baab=aabb

Overlap of [3] babab=aab with [2] babb=ab:

ba bab babb

Critical pair: baab=aabb.

Defines rule #2.

Referenced by [5], [6].

[5] aabab=aabb

Overlap of [3] babab=aab with [3] babab=aab:

ba bab babab

Critical pair: baaab=aabab.

Reduce LHS:

[1]	b(aaa)b
[4]	⇒ (baab)
	⇒ aabb

Flip LHS and RHS.

Defines rule #4.

Referenced by [6], [7].

[6] aabbab=aabbb

Overlap of [4] baab=aabb with [5] aabab=aabb:

b aab aabab

Critical pair: baabb=aabbab.

Reduce LHS:

[4]	(baab)b
	⇒ aabbb

Flip LHS and RHS.

Referenced by [8].

[7] aabbb=aab

Overlap of [5] aabab=aabb with [2] babb=ab:

aa bab babb

Critical pair: aaab=aabbb.

Reduce LHS:

[1]	(aaa)b
	⇒ aab

Flip LHS and RHS.

Defines rule #5.

Referenced by [8].

[8] aabbab=aab

Simplify [6] aabbab=aabbb.

Reduce RHS:

[7]	(aabbb)
	⇒ aab

Defines rule #7.