Certificate for #1710 ⟨a, b | aabbaaaab=b⟩

Back:⟨a, b | aabbaaaab=b⟩

Completion settings:

[1] aabbaaaab=b

Axiom: aabbaaaab=b.

Defines rule #3.

Referenced by [2], [3].

[2] aabbaab=bbaaaab

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

aabbaa aab aabbaaaab

Critical pair: aabbaab=bbaaaab.

Defines rule #2.

Referenced by [3].

[3] aabbb=bbaab

Overlap of [2] aabbaab=bbaaaab with [1] aabbaaaab=b:

aabb aab aabbaaaab

Critical pair: aabbb=bbaaaabbaaaab.

Reduce RHS:

[1]bbaa(aabbaaaab)
⇒ bbaab

Defines rule #1.