Certificate for #20305 ⟨a, b | aba=b, baab=bbb⟩

Completion settings:

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

[1] aba=b

Axiom: aba=b.

Defines rule #1.

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

[2] baab=bbb

Axiom: baab=bbb.

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

[3] bba=abb

Overlap of [1] aba=b with [1] aba=b:

ab a aba

Critical pair: abb=bba.

Flip LHS and RHS.

Defines rule #3.

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

[4] abbb=bab

Overlap of [1] aba=b with [2] baab=bbb:

a ba baab

Critical pair: abbb=bab.

Referenced by [6], [7].

[5] babb=bab

Overlap of [2] baab=bbb with [1] aba=b:

ba ab aba

Critical pair: bab=bbba.

Reduce RHS:

[3]	b(bba)
	⇒ babb

Flip LHS and RHS.

Referenced by [7].

[6] bbbb=bb

Overlap of [3] bba=abb with [2] baab=bbb:

b ba baab

Critical pair: bbbb=abbab.

Reduce RHS:

[3]	a(bba)b
[4]	⇒ a(abbb)
[1]	⇒ (aba)b
	⇒ bb

Referenced by [7], [9].

[7] bab=abb

Overlap of [6] bbbb=bb with [3] bba=abb:

bb bb bba

Critical pair: bbabb=bba.

Reduce LHS:

[3]	(bba)bb
[4]	⇒ (abbb)b
[5]	⇒ (babb)
	⇒ bab

Reduce RHS:

[3]	(bba)
	⇒ abb

Defines rule #2.

Referenced by [8].

[8] aabb=bb

Overlap of [1] aba=b with [7] bab=abb:

a ba bab

Critical pair: aabb=bb.

Defines rule #5.

Referenced by [9].

[9] bbb=bb

Overlap of [2] baab=bbb with [8] aabb=bb:

b aab aabb

Critical pair: bbb=bbbb.

Reduce RHS:

[6]	(bbbb)
	⇒ bb

Defines rule #4.

Referenced by [10].

[10] baab=bb

Simplify [2] baab=bbb.

Reduce RHS:

[9]	(bbb)
	⇒ bb

Defines rule #6.