Certificate for #15963 ⟨a, b | aaa=aa, abab=bb⟩

Back:⟨a, b | aaa=aa, abab=bb⟩

Completion settings:

[1] aaa=aa

Axiom: aaa=aa.

Defines rule #1.

Referenced by [3].

[2] abab=bb

Axiom: abab=bb.

Defines rule #3.

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

[3] aabb=abb

Overlap of [1] aaa=aa with [2] abab=bb:

aa a abab

Critical pair: aabb=aabab.

Reduce RHS:

[2]a(abab)
⇒ abb

Defines rule #2.

Referenced by [5], [6].

[4] bbab=abbb

Overlap of [2] abab=bb with [2] abab=bb:

ab ab abab

Critical pair: abbb=bbab.

Flip LHS and RHS.

Defines rule #4.

Referenced by [5], [6].

[5] babbb=bbbb

Overlap of [2] abab=bb with [4] bbab=abbb:

aba b bbab

Critical pair: abaabbb=bbbab.

Reduce LHS:

[3]ab(aabb)b
[2]⇒ (abab)bb
⇒ bbbb

Reduce RHS:

[4]b(bbab)
⇒ babbb

Flip LHS and RHS.

Defines rule #6.

[6] abbbb=bbbb

Overlap of [3] aabb=abb with [4] bbab=abbb:

aab b bbab

Critical pair: aababbb=abbbab.

Reduce LHS:

[2]a(abab)bb
⇒ abbbb

Reduce RHS:

[4]ab(bbab)
[2]⇒ (abab)bb
⇒ bbbb

Defines rule #5.