Certificate for #3195 ⟨a, b | abaaabbabab=1⟩

Back:⟨a, b | abaaabbabab=1⟩

Completion settings:

[1] abaaabbabab=1

Axiom: abaaabbabab=1.

Referenced by [2], [3].

[2] abaaabbab=aaabbabab

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

abaaabbab ab abaaabbabab

Critical pair: abaaabbab=aaabbabab.

Referenced by [3], [4].

[3] aaabbababab=1

Overlap of [1] abaaabbabab=1 with [2] abaaabbab=aaabbabab:

abaaabbabab abaaabbab

Critical pair: aaabbababab=1.

Defines rule #2.

Referenced by [4], [5].

[4] abaaabbaaabbabab=aaabb

Overlap of [2] abaaabbab=aaabbabab with [2] abaaabbab=aaabbabab:

abaaabb ab abaaabbab

Critical pair: abaaabbaaabbabab=aaabbababaaabbab.

Reduce RHS:

[2]aaabbab(abaaabbab)
[2]⇒ aaabb(abaaabbab)ab
[3]⇒ aaabb(aaabbababab)
⇒ aaabb

Referenced by [5].

[5] abaaabb=aaabbab

Overlap of [4] abaaabbaaabbabab=aaabb with [3] aaabbababab=1:

abaaabb aaabbabab aaabbababab

Critical pair: abaaabb=aaabbab.

Defines rule #1.