Certificate for #15895 ⟨a, b | aba=ab, bbabb=a⟩

Completion settings:

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

[1] aba=ab

Axiom: aba=ab.

Defines rule #2.

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

[2] bbabb=a

Axiom: bbabb=a.

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

[3] abba=abb

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

ab a aba

Critical pair: abab=abba.

Reduce LHS:

[1]	(aba)b
	⇒ abb

Flip LHS and RHS.

Referenced by [6].

[4] bbaa=aabb

Overlap of [2] bbabb=a with [2] bbabb=a:

bba bb bbabb

Critical pair: bbaa=aabb.

Referenced by [8].

[5] bbab=abbb

Overlap of [2] bbabb=a with [2] bbabb=a:

bbab b bbabb

Critical pair: bbaba=ababb.

Reduce LHS:

[1]	bb(aba)
	⇒ bbab

Reduce RHS:

[1]	(aba)bb
	⇒ abbb

Referenced by [6], [9].

[6] abbbb=aa

Overlap of [2] bbabb=a with [3] abba=abb:

bb abb abba

Critical pair: bbabb=aa.

Reduce LHS:

[5]	(bbab)b
	⇒ abbbb

Referenced by [7], [9], [11].

[7] aab=ab

Overlap of [1] aba=ab with [6] abbbb=aa:

ab a abbbb

Critical pair: abaa=abbbbb.

Reduce LHS:

[1]	(aba)a
[1]	⇒ (aba)
	⇒ ab

Reduce RHS:

[6]	(abbbb)b
	⇒ aab

Flip LHS and RHS.

Referenced by [8].

[8] bbaa=abb

Simplify [4] bbaa=aabb.

Reduce RHS:

[7]	(aab)b
	⇒ abb

Referenced by [10].

[9] aa=a

Overlap of [2] bbabb=a with [5] bbab=abbb:

bbabb bbab

Critical pair: abbbb=a.

Reduce LHS:

[6]	(abbbb)
	⇒ aa

Defines rule #1.

Referenced by [10], [11].

[10] bba=abb

Overlap of [8] bbaa=abb with [9] aa=a:

bb aa aa

Critical pair: bba=abb.

Defines rule #3.

[11] abbbb=a

Simplify [6] abbbb=aa.

Reduce RHS:

[9]	(aa)
	⇒ a

Defines rule #4.