Certificate for #3722 ⟨a, b | abaaabbaab=b⟩

Back:⟨a, b | abaaabbaab=b⟩

Completion settings:

[1] abaaabbaab=b

Axiom: abaaabbaab=b.

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

[2] baaabbaab=abaaabbab

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

abaaabba ab abaaabbaab

Critical pair: abaaabbab=baaabbaab.

Flip LHS and RHS.

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

[3] baaabbab=abaaabbb

Overlap of [2] baaabbaab=abaaabbab with [1] abaaabbaab=b:

baaabba ab abaaabbaab

Critical pair: baaabbab=abaaabbabaaabbaab.

Reduce RHS:

[1]abaaabb(abaaabbaab)
⇒ abaaabbb

Defines rule #1.

Referenced by [4], [5].

[4] aaabaaabbb=b

Overlap of [1] abaaabbaab=b with [2] baaabbaab=abaaabbab:

a baaabbaab baaabbaab

Critical pair: aabaaabbab=b.

Reduce LHS:

[3]aa(baaabbab)
⇒ aaabaaabbb

Defines rule #3.

[5] baaabbaab=aabaaabbb

Simplify [2] baaabbaab=abaaabbab.

Reduce RHS:

[3]a(baaabbab)
⇒ aabaaabbb

Defines rule #2.