Certificate for #783 ⟨a, b | aaabbbaa=a⟩

Back:⟨a, b | aaabbbaa=a⟩

Completion settings:

[1] aaabbbaa=a

Axiom: aaabbbaa=a.

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

[2] aabbbaa=aaabbba

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

aaabbb aa aaabbbaa

Critical pair: aaabbba=aabbbaa.

Flip LHS and RHS.

Referenced by [3], [4].

[3] abbbaa=aabbba

Overlap of [1] aaabbbaa=a with [2] aabbbaa=aaabbba:

aaabbb aa aabbbaa

Critical pair: aaabbbaaabbba=abbbaa.

Reduce LHS:

[1](aaabbbaa)abbba
⇒ aabbba

Flip LHS and RHS.

Defines rule #1.

[4] aaaabbba=a

Overlap of [1] aaabbbaa=a with [2] aabbbaa=aaabbba:

a aabbbaa aabbbaa

Critical pair: aaaabbba=a.

Defines rule #2.