Certificate for #19679 ⟨a, b | aba=a, abbba=bb⟩

Completion settings:

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

[1] aba=a

Axiom: aba=a.

Defines rule #1.

Referenced by [3], [4].

[2] abbba=bb

Axiom: abbba=bb.

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

[3] abbb=bb

Overlap of [1] aba=a with [2] abbba=bb:

ab a abbba

Critical pair: abbb=abbba.

Reduce RHS:

[2]	(abbba)
	⇒ bb

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

[4] bbba=bba

Overlap of [2] abbba=bb with [1] aba=a:

abbb a aba

Critical pair: abbba=bbba.

Reduce LHS:

[3]	(abbb)a
	⇒ bba

Flip LHS and RHS.

Referenced by [5].

[5] bbbb=bba

Overlap of [2] abbba=bb with [2] abbba=bb:

abbb a abbba

Critical pair: abbbbb=bbbbba.

Reduce LHS:

[3]	(abbb)bb
	⇒ bbbb

Reduce RHS:

[4]	bb(bbba)
[4]	⇒ b(bbba)
[4]	⇒ (bbba)
	⇒ bba

Referenced by [7].

[6] bba=bb

Overlap of [2] abbba=bb with [3] abbb=bb:

abbba abbb

Critical pair: bba=bb.

Defines rule #3.

Referenced by [7].

[7] bbb=bb

Overlap of [2] abbba=bb with [3] abbb=bb:

abbb a abbb

Critical pair: abbbbb=bbbbb.

Reduce LHS:

[3]	(abbb)bb
[5]	⇒ (bbbb)
[6]	⇒ (bba)
	⇒ bb

Reduce RHS:

[5]	(bbbb)b
[6]	⇒ (bba)b
	⇒ bbb

Flip LHS and RHS.

Defines rule #4.

Referenced by [8].

[8] abb=bb

Overlap of [3] abbb=bb with [7] bbb=bb:

a bbb bbb

Critical pair: abb=bb.

Defines rule #2.