Certificate for #6205 ⟨a, b | aba=b, aaaabb=1⟩

Back:⟨a, b | aba=b, aaaabb=1⟩

Completion settings:

[1] aba=b

Axiom: aba=b.

Referenced by [3], [5], [6], [7], [8], [9], [10], [11], [13].

[2] aaaabb=1

Axiom: aaaabb=1.

Referenced by [4].

[3] abb=bba

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

ab a aba

Critical pair: abb=bba.

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

[4] bbaaaa=1

Simplify [2] aaaabb=1.

Reduce LHS:

[3]aaa(abb)
[3]⇒ aa(abb)a
[3]⇒ a(abb)aa
[3]⇒ (abb)aaa
⇒ bbaaaa

Referenced by [5], [9], [12].

[5] bbbaaa=ab

Overlap of [3] abb=bba with [4] bbaaaa=1:

ab b bbaaaa

Critical pair: ab=bbabaaaa.

Reduce RHS:

[1]bb(aba)aaa
⇒ bbbaaa

Flip LHS and RHS.

Referenced by [6].

[6] bbbaa=aab

Overlap of [3] abb=bba with [5] bbbaaa=ab:

a bb bbbaaa

Critical pair: aab=bbabaaa.

Reduce RHS:

[1]bb(aba)aa
⇒ bbbaa

Flip LHS and RHS.

Referenced by [7].

[7] bbba=aaab

Overlap of [3] abb=bba with [6] bbbaa=aab:

a bb bbbaa

Critical pair: aaab=bbabaa.

Reduce RHS:

[1]bb(aba)a
⇒ bbba

Flip LHS and RHS.

Referenced by [8], [9].

[8] bbb=aaaab

Overlap of [3] abb=bba with [7] bbba=aaab:

a bb bbba

Critical pair: aaaab=bbaba.

Reduce RHS:

[1]bb(aba)
⇒ bbb

Flip LHS and RHS.

Referenced by [9].

[9] baab=aa

Overlap of [3] abb=bba with [7] bbba=aaab:

ab b bbba

Critical pair: abaaab=bbabba.

Reduce LHS:

[1](aba)aab
⇒ baab

Reduce RHS:

[3]bb(abb)a
[8]⇒ (bbb)baa
[3]⇒ aaa(abb)aa
[3]⇒ aa(abb)aaa
[3]⇒ a(abb)aaaa
[3]⇒ (abb)aaaaa
[4]⇒ (bbaaaa)aa
⇒ aa

Referenced by [10].

[10] bab=aaa

Overlap of [1] aba=b with [9] baab=aa:

a ba baab

Critical pair: aaa=bab.

Flip LHS and RHS.

Referenced by [11].

[11] bb=aaaa

Overlap of [1] aba=b with [10] bab=aaa:

a ba bab

Critical pair: aaaa=bb.

Flip LHS and RHS.

Defines rule #3.

Referenced by [12].

[12] aaaaaaaa=1

Overlap of [4] bbaaaa=1 with [11] bb=aaaa:

bbaaaa bb

Critical pair: aaaaaaaa=1.

Defines rule #1.

Referenced by [13].

[13] ab=baaaaaaa

Overlap of [1] aba=b with [12] aaaaaaaa=1:

ab a aaaaaaaa

Critical pair: ab=baaaaaaa.

Defines rule #2.