Certificate for #3507 ⟨a, b | aaabbbaaab=a⟩

Back:⟨a, b | aaabbbaaab=a⟩

Completion settings:

[1] aaabbbaaab=a

Axiom: aaabbbaaab=a.

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

[2] aaabbba=abbaaab

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

aaabbb aaab aaabbbaaab

Critical pair: aaabbba=abbaaab.

Defines rule #1.

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

[3] abbaaabaab=a

Overlap of [1] aaabbbaaab=a with [2] aaabbba=abbaaab:

aaabbbaaab aaabbba

Critical pair: abbaaabaab=a.

Defines rule #4.

Referenced by [4], [5].

[4] abaaabaab=abbaaabaa

Overlap of [1] aaabbbaaab=a with [3] abbaaabaab=a:

aaabbbaa ab abbaaabaab

Critical pair: aaabbbaaa=abaaabaab.

Reduce LHS:

[2](aaabbba)aa
⇒ abbaaabaa

Flip LHS and RHS.

Defines rule #3.

Referenced by [5].

[5] aaaabaab=abaaabaa

Overlap of [1] aaabbbaaab=a with [4] abaaabaab=abbaaabaa:

aaabbbaa ab abaaabaab

Critical pair: aaabbbaaabbaaabaa=aaaabaab.

Reduce LHS:

[2](aaabbba)aabbaaabaa
[3]⇒ (abbaaabaab)baaabaa
⇒ abaaabaa

Flip LHS and RHS.

Defines rule #2.