Certificate for #6431 ⟨a, b | aab=b, bbaaa=b⟩

Completion settings:

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

[1] aab=b

Axiom: aab=b.

Defines rule #1.

Referenced by [3], [4].

[2] bbaaa=b

Axiom: bbaaa=b.

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

[3] bbab=bb

Overlap of [2] bbaaa=b with [1] aab=b:

bba aa aab

Critical pair: bbab=bb.

Referenced by [6].

[4] bbb=bab

Overlap of [2] bbaaa=b with [1] aab=b:

bbaa a aab

Critical pair: bbaab=bab.

Reduce LHS:

[1]	bb(aab)
	⇒ bbb

Referenced by [5], [6], [9].

[5] babaaa=bb

Overlap of [4] bbb=bab with [2] bbaaa=b:

b bb bbaaa

Critical pair: bb=babaaa.

Flip LHS and RHS.

Referenced by [8].

[6] babb=bb

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

b bb bbb

Critical pair: bbab=babb.

Reduce LHS:

[3]	(bbab)
	⇒ bb

Flip LHS and RHS.

Referenced by [7].

[7] bab=b

Overlap of [6] babb=bb with [2] bbaaa=b:

ba bb bbaaa

Critical pair: bab=bbaaa.

Reduce RHS:

[2]	(bbaaa)
	⇒ b

Defines rule #2.

Referenced by [8], [9].

[8] baaa=bb

Simplify [5] babaaa=bb.

Reduce LHS:

[7]	(bab)aaa
	⇒ baaa

Defines rule #4.

[9] bbb=b

Simplify [4] bbb=bab.

Reduce RHS:

[7]	(bab)
	⇒ b

Defines rule #3.