Certificate for #3476 ⟨a, b | aaababbbaa=a⟩

Back:⟨a, b | aaababbbaa=a⟩

Completion settings:

[1] aaababbbaa=a

Axiom: aaababbbaa=a.

Referenced by [2], [3], [4].

[2] aababbbaa=aaababbba

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

aaababbb aa aaababbbaa

Critical pair: aaababbba=aababbbaa.

Flip LHS and RHS.

Referenced by [3], [4].

[3] ababbbaa=aababbba

Overlap of [1] aaababbbaa=a with [2] aababbbaa=aaababbba:

aaababbb aa aababbbaa

Critical pair: aaababbbaaababbba=ababbbaa.

Reduce LHS:

[1](aaababbbaa)ababbba
⇒ aababbba

Flip LHS and RHS.

Defines rule #1.

[4] aaaababbba=a

Overlap of [1] aaababbbaa=a with [2] aababbbaa=aaababbba:

a aababbbaa aababbbaa

Critical pair: aaaababbba=a.

Defines rule #2.