Certificate for #12517 ⟨a, b | abab=aa, bbbb=b⟩

Back:⟨a, b | abab=aa, bbbb=b⟩

Completion settings:

[1] abab=aa

Axiom: abab=aa.

Defines rule #2.

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

[2] bbbb=b

Axiom: bbbb=b.

Defines rule #1.

Referenced by [4].

[3] aaab=abaa

Overlap of [1] abab=aa with [1] abab=aa:

ab ab abab

Critical pair: abaa=aaab.

Flip LHS and RHS.

Defines rule #3.

Referenced by [5], [6], [7].

[4] aabbb=aa

Overlap of [1] abab=aa with [2] bbbb=b:

aba b bbbb

Critical pair: abab=aabbb.

Reduce LHS:

[1](abab)
⇒ aa

Flip LHS and RHS.

Defines rule #4.

Referenced by [5].

[5] abaabb=aaa

Overlap of [3] aaab=abaa with [4] aabbb=aa:

a aab aabbb

Critical pair: aaa=abaabb.

Flip LHS and RHS.

Defines rule #5.

Referenced by [6].

[6] aabaab=abaaa

Overlap of [1] abab=aa with [5] abaabb=aaa:

ab ab abaabb

Critical pair: abaaa=aaaabb.

Reduce RHS:

[3]a(aaab)b
⇒ aabaab

Flip LHS and RHS.

Defines rule #6.

Referenced by [7].

[7] abaabaa=aabaaa

Overlap of [3] aaab=abaa with [6] aabaab=abaaa:

a aab aabaab

Critical pair: aabaaa=abaaaab.

Reduce RHS:

[3]aba(aaab)
⇒ abaabaa

Flip LHS and RHS.

Defines rule #7.