Certificate for #3222 ⟨a, b | abaabbbabab=1⟩

Back:⟨a, b | abaabbbabab=1⟩

Completion settings:

[1] abaabbbabab=1

Axiom: abaabbbabab=1.

Referenced by [2], [3].

[2] abaabbbab=aabbbabab

Overlap of [1] abaabbbabab=1 with [1] abaabbbabab=1:

abaabbbab ab abaabbbabab

Critical pair: abaabbbab=aabbbabab.

Referenced by [3], [4].

[3] aabbbababab=1

Overlap of [1] abaabbbabab=1 with [2] abaabbbab=aabbbabab:

abaabbbabab abaabbbab

Critical pair: aabbbababab=1.

Defines rule #2.

Referenced by [4], [5].

[4] abaabbbaabbbabab=aabbb

Overlap of [2] abaabbbab=aabbbabab with [2] abaabbbab=aabbbabab:

abaabbb ab abaabbbab

Critical pair: abaabbbaabbbabab=aabbbababaabbbab.

Reduce RHS:

[2]aabbbab(abaabbbab)
[2]⇒ aabbb(abaabbbab)ab
[3]⇒ aabbb(aabbbababab)
⇒ aabbb

Referenced by [5].

[5] abaabbb=aabbbab

Overlap of [4] abaabbbaabbbabab=aabbb with [3] aabbbababab=1:

abaabbb aabbbabab aabbbababab

Critical pair: abaabbb=aabbbab.

Defines rule #1.