Certificate for #896 ⟨a, b | aa=a, babb=a⟩

Back:⟨a, b | aa=a, babb=a⟩

Completion settings:

[1] aa=a

Axiom: aa=a.

Defines rule #3.

Referenced by [3], [4].

[2] babb=a

Axiom: babb=a.

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

[3] baba=abb

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

bab b babb

Critical pair: baba=aabb.

Reduce RHS:

[1](aa)bb
⇒ abb

Referenced by [4].

[4] ba=abbbb

Overlap of [3] baba=abb with [2] babb=a:

ba ba babb

Critical pair: baa=abbbb.

Reduce LHS:

[1]b(aa)
⇒ ba

Defines rule #2.

Referenced by [5].

[5] abbbbbb=a

Overlap of [2] babb=a with [4] ba=abbbb:

babb ba

Critical pair: abbbbbb=a.

Defines rule #1.