Certificate for #1756 ⟨a, b | abaaabaab=b⟩

Back:⟨a, b | abaaabaab=b⟩

Completion settings:

[1] abaaabaab=b

Axiom: abaaabaab=b.

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

[2] baaabaab=abaaabab

Overlap of [1] abaaabaab=b with [1] abaaabaab=b:

abaaaba ab abaaabaab

Critical pair: abaaabab=baaabaab.

Flip LHS and RHS.

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

[3] baaabab=abaaabb

Overlap of [2] baaabaab=abaaabab with [1] abaaabaab=b:

baaaba ab abaaabaab

Critical pair: baaabab=abaaababaaabaab.

Reduce RHS:

[1]abaaab(abaaabaab)
⇒ abaaabb

Defines rule #1.

Referenced by [4], [5].

[4] aaabaaabb=b

Overlap of [1] abaaabaab=b with [2] baaabaab=abaaabab:

a baaabaab baaabaab

Critical pair: aabaaabab=b.

Reduce LHS:

[3]aa(baaabab)
⇒ aaabaaabb

Defines rule #3.

[5] baaabaab=aabaaabb

Simplify [2] baaabaab=abaaabab.

Reduce RHS:

[3]a(baaabab)
⇒ aabaaabb

Defines rule #2.