Certificate for #3513 ⟨a, b | aaabbbabaa=a⟩

Back:⟨a, b | aaabbbabaa=a⟩

Completion settings:

[1] aaabbbabaa=a

Axiom: aaabbbabaa=a.

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

[2] aabbbabaa=aaabbbaba

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

aaabbbab aa aaabbbabaa

Critical pair: aaabbbaba=aabbbabaa.

Flip LHS and RHS.

Referenced by [3], [4].

[3] abbbabaa=aabbbaba

Overlap of [1] aaabbbabaa=a with [2] aabbbabaa=aaabbbaba:

aaabbbab aa aabbbabaa

Critical pair: aaabbbabaaabbbaba=abbbabaa.

Reduce LHS:

[1](aaabbbabaa)abbbaba
⇒ aabbbaba

Flip LHS and RHS.

Defines rule #1.

[4] aaaabbbaba=a

Overlap of [1] aaabbbabaa=a with [2] aabbbabaa=aaabbbaba:

a aabbbabaa aabbbabaa

Critical pair: aaaabbbaba=a.

Defines rule #2.