Certificate for #704 ⟨a, b | abaabaaba=1⟩

Back:⟨a, b | abaabaaba=1⟩

Completion settings:

[1] abaabaaba=1

Axiom: abaabaaba=1.

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

[2] baabaaba=abaabaab

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

abaabaab a abaabaaba

Critical pair: abaabaab=baabaaba.

Flip LHS and RHS.

Defines rule #1.

Referenced by [3].

[3] baaabaabaab=ba

Overlap of [2] baabaaba=abaabaab with [2] baabaaba=abaabaab:

baa baaba baabaaba

Critical pair: baaabaabaab=abaabaababa.

Reduce RHS:

[1](abaabaaba)ba
⇒ ba

Referenced by [4].

[4] aabaabaab=1

Overlap of [1] abaabaaba=1 with [3] baaabaabaab=ba:

abaabaa ba baaabaabaab

Critical pair: abaabaaba=aabaabaab.

Reduce LHS:

[1](abaabaaba)
⇒ 1

Flip LHS and RHS.

Defines rule #2.