Certificate for #4118 ⟨a, b | bbb=aaa, abab=1⟩

Back:⟨a, b | bbb=aaa, abab=1⟩

Completion settings:

[1] bbb=aaa

Axiom: bbb=aaa.

Referenced by [3], [4].

[2] abab=1

Axiom: abab=1.

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

[3] aaab=baaa

Overlap of [1] bbb=aaa with [1] bbb=aaa:

b bb bbb

Critical pair: baaa=aaab.

Flip LHS and RHS.

Defines rule #2.

Referenced by [5], [7], [8], [9].

[4] bb=abaaaa

Overlap of [2] abab=1 with [1] bbb=aaa:

aba b bbb

Critical pair: abaaaa=bb.

Flip LHS and RHS.

Defines rule #3.

Referenced by [6], [8].

[5] babaaa=aa

Overlap of [3] aaab=baaa with [2] abab=1:

aa ab abab

Critical pair: aa=baaaab.

Reduce RHS:

[3]ba(aaab)
⇒ babaaa

Flip LHS and RHS.

Referenced by [9].

[6] abaabaaaa=b

Overlap of [2] abab=1 with [4] bb=abaaaa:

aba b bb

Critical pair: abaabaaaa=b.

Referenced by [7], [8].

[7] abaabaabaaa=bab

Overlap of [6] abaabaaaa=b with [3] aaab=baaa:

abaabaa aa aaab

Critical pair: abaabaabaaa=bab.

Referenced by [9].

[8] baab=aabaaaaaaaaaaaaaaaaa

Overlap of [6] abaabaaaa=b with [3] aaab=baaa:

abaabaaa a aaab

Critical pair: abaabaaabaaa=baab.

Reduce LHS:

[3]abaab(aaab)aaa
[4]⇒ abaa(bb)aaaaaa
[3]⇒ ab(aaab)aaaaaaaaaa
[4]⇒ a(bb)aaaaaaaaaaaaa
⇒ aabaaaaaaaaaaaaaaaaa

Flip LHS and RHS.

Defines rule #5.

Referenced by [9].

[9] bab=aaaaaaaaaaaaaaaaaaaaaaa

Simplify [7] abaabaabaaa=bab.

Reduce LHS:

[8]a(baab)aabaaa
[3]⇒ (aaab)aaaaaaaaaaaaaaaaaaabaaa
[3]⇒ baaaaaaaaaaaaaaaaaaa(aaab)aaa
[3]⇒ baaaaaaaaaaaaaaaa(aaab)aaaaaa
[3]⇒ baaaaaaaaaaaaa(aaab)aaaaaaaaa
[3]⇒ baaaaaaaaaa(aaab)aaaaaaaaaaaa
[3]⇒ baaaaaaa(aaab)aaaaaaaaaaaaaaa
[3]⇒ baaaa(aaab)aaaaaaaaaaaaaaaaaa
[3]⇒ ba(aaab)aaaaaaaaaaaaaaaaaaaaa
[5]⇒ (babaaa)aaaaaaaaaaaaaaaaaaaaa
⇒ aaaaaaaaaaaaaaaaaaaaaaa

Flip LHS and RHS.

Defines rule #4.

Referenced by [10].

[10] aaaaaaaaaaaaaaaaaaaaaaaa=1

Overlap of [2] abab=1 with [9] bab=aaaaaaaaaaaaaaaaaaaaaaa:

a bab bab

Critical pair: aaaaaaaaaaaaaaaaaaaaaaaa=1.

Defines rule #1.