Certificate for #8887 ⟨a, b | aa=a, abbba=bb⟩

Back:⟨a, b | aa=a, abbba=bb⟩

Completion settings:

[1] aa=a

Axiom: aa=a.

Defines rule #1.

Referenced by [3], [4].

[2] abbba=bb

Axiom: abbba=bb.

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

[3] abb=bb

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

a a abbba

Critical pair: abb=abbba.

Reduce RHS:

[2](abbba)
⇒ bb

Defines rule #2.

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

[4] bbba=bba

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

abbb a aa

Critical pair: abbba=bba.

Reduce LHS:

[3](abb)ba
⇒ bbba

Referenced by [5], [6].

[5] bba=bb

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

abbba abb

Critical pair: bbba=bb.

Reduce LHS:

[4](bbba)
⇒ bba

Defines rule #3.

Referenced by [6].

[6] bbb=bb

Overlap of [3] abb=bb with [5] bba=bb:

ab b bba

Critical pair: abbb=bbba.

Reduce LHS:

[3](abb)b
⇒ bbb

Reduce RHS:

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

Defines rule #4.