Certificate for #3663 ⟨a, b | aabbbaaaab=b⟩

Back:⟨a, b | aabbbaaaab=b⟩

Completion settings:

[1] aabbbaaaab=b

Axiom: aabbbaaaab=b.

Defines rule #3.

Referenced by [2], [3].

[2] aabbbaab=bbbaaaab

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

aabbbaa aab aabbbaaaab

Critical pair: aabbbaab=bbbaaaab.

Defines rule #2.

Referenced by [3].

[3] aabbbb=bbbaab

Overlap of [2] aabbbaab=bbbaaaab with [1] aabbbaaaab=b:

aabbb aab aabbbaaaab

Critical pair: aabbbb=bbbaaaabbbaaaab.

Reduce RHS:

[1]bbbaa(aabbbaaaab)
⇒ bbbaab

Defines rule #1.