Certificate for #4171 ⟨a, b | aabbabaab=aa⟩

Back:⟨a, b | aabbabaab=aa⟩

Completion settings:

[1] aabbabaab=aa

Axiom: aabbabaab=aa.

Defines rule #3.

Referenced by [2], [3].

[2] aababaab=aabbabaa

Overlap of [1] aabbabaab=aa with [1] aabbabaab=aa:

aabbab aab aabbabaab

Critical pair: aabbabaa=aababaab.

Flip LHS and RHS.

Defines rule #2.

Referenced by [3].

[3] aaabaab=aababaa

Overlap of [1] aabbabaab=aa with [2] aababaab=aabbabaa:

aabbab aab aababaab

Critical pair: aabbabaabbabaa=aaabaab.

Reduce LHS:

[1](aabbabaab)babaa
⇒ aababaa

Flip LHS and RHS.

Defines rule #1.