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

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

Completion settings:

[1] abab=aa

Axiom: abab=aa.

Referenced by [3], [4].

[2] bbbb=1

Axiom: bbbb=1.

Defines rule #1.

Referenced by [4], [6].

[3] abaa=aaab

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

ab ab abab

Critical pair: abaa=aaab.

Referenced by [5].

[4] aba=aabbb

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

aba b bbbb

Critical pair: aba=aabbb.

Defines rule #2.

Referenced by [5], [6].

[5] aabbba=aaab

Simplify [3] abaa=aaab.

Reduce LHS:

[4](aba)a
⇒ aabbba

Defines rule #3.

Referenced by [6].

[6] aaabba=aaaabb

Overlap of [5] aabbba=aaab with [4] aba=aabbb:

aabbb a aba

Critical pair: aabbbaabbb=aaabba.

Reduce LHS:

[5](aabbba)abbb
[4]⇒ aa(aba)bbb
[2]⇒ aaaa(bbbb)bb
⇒ aaaabb

Flip LHS and RHS.

Defines rule #4.