Certificate for #816 ⟨a, b | aabbaabb=a⟩

Back:⟨a, b | aabbaabb=a⟩

Completion settings:

[1] aabbaabb=a

Axiom: aabbaabb=a.

Referenced by [2], [3].

[2] aabba=aaabb

Overlap of [1] aabbaabb=a with [1] aabbaabb=a:

aabb aabb aabbaabb

Critical pair: aabba=aaabb.

Defines rule #1.

Referenced by [3].

[3] aaaabbbb=a

Overlap of [1] aabbaabb=a with [2] aabba=aaabb:

aabbaabb aabba

Critical pair: aaabbabb=a.

Reduce LHS:

[2]a(aabba)bb
⇒ aaaabbbb

Defines rule #2.