Certificate for #6513 ⟨a, b | aba=b, abbbb=b⟩

Completion settings:

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

[1] aba=b

Axiom: aba=b.

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

[2] abbbb=b

Axiom: abbbb=b.

Referenced by [4], [5].

[3] bba=abb

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

ab a aba

Critical pair: abb=bba.

Flip LHS and RHS.

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

[4] ba=ab

Overlap of [2] abbbb=b with [3] bba=abb:

abb bb bba

Critical pair: abbabb=ba.

Reduce LHS:

[3]	a(bba)bb
[2]	⇒ a(abbbb)
	⇒ ab

Flip LHS and RHS.

Defines rule #1.

Referenced by [5], [6].

[5] bbbb=ab

Overlap of [2] abbbb=b with [4] ba=ab:

abbb b ba

Critical pair: abbbab=ba.

Reduce LHS:

[3]	ab(bba)b
[1]	⇒ (aba)bbb
	⇒ bbbb

Reduce RHS:

[4]	(ba)
	⇒ ab

Defines rule #3.

Referenced by [7].

[6] aabb=bb

Overlap of [4] ba=ab with [1] aba=b:

b a aba

Critical pair: bb=abba.

Reduce RHS:

[3]	a(bba)
	⇒ aabb

Flip LHS and RHS.

Referenced by [7].

[7] aaab=ab

Overlap of [6] aabb=bb with [5] bbbb=ab:

aa bb bbbb

Critical pair: aaab=bbbb.

Reduce RHS:

[5]	(bbbb)
	⇒ ab

Referenced by [8].

[8] aab=b

Overlap of [7] aaab=ab with [1] aba=b:

aa ab aba

Critical pair: aab=aba.

Reduce RHS:

[1]	(aba)
	⇒ b

Defines rule #2.