Certificate for #3487 ⟨a, b | aaabbaaabb=b⟩

Back:⟨a, b | aaabbaaabb=b⟩

Completion settings:

[1] aaabbaaabb=b

Axiom: aaabbaaabb=b.

Referenced by [2], [3].

[2] baaabb=aaabbb

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

aaabb aaabb aaabbaaabb

Critical pair: aaabbb=baaabb.

Flip LHS and RHS.

Defines rule #1.

Referenced by [3].

[3] aaaaaabbbb=b

Overlap of [1] aaabbaaabb=b with [2] baaabb=aaabbb:

aaab baaabb baaabb

Critical pair: aaabaaabbb=b.

Reduce LHS:

[2]aaa(baaabb)b
⇒ aaaaaabbbb

Defines rule #2.