Certificate for #16515 ⟨a, b | aab=ba, bbb=aaa⟩

Back:⟨a, b | aab=ba, bbb=aaa⟩

Completion settings:

[1] ba=aab

Axiom: aab=ba.

Flip LHS and RHS.

Defines rule #3.

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

[2] bbb=aaa

Axiom: bbb=aaa.

Defines rule #4.

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

[3] aaaaaaaaaaa=aaaa

Overlap of [2] bbb=aaa with [1] ba=aab:

bb b ba

Critical pair: bbaab=aaaa.

Reduce LHS:

[1]b(ba)ab
[1]⇒ (ba)abab
[1]⇒ aa(ba)bab
[1]⇒ aaaab(ba)b
[1]⇒ aaaa(ba)abb
[1]⇒ aaaaaa(ba)bb
[2]⇒ aaaaaaaa(bbb)
⇒ aaaaaaaaaaa

Referenced by [6].

[4] aaaaaab=aaab

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

b bb bbb

Critical pair: baaa=aaab.

Reduce LHS:

[1](ba)aa
[1]⇒ aa(ba)a
[1]⇒ aaaa(ba)
⇒ aaaaaab

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

[5] aaaaaaaaa=aaaaaa

Overlap of [4] aaaaaab=aaab with [2] bbb=aaa:

aaaaaa b bbb

Critical pair: aaaaaaaaa=aaabbb.

Reduce RHS:

[2]aaa(bbb)
⇒ aaaaaa

Referenced by [6], [8].

[6] aaaaaaaa=aaaa

Simplify [3] aaaaaaaaaaa=aaaa.

Reduce LHS:

[5](aaaaaaaaa)aa
⇒ aaaaaaaa

Referenced by [7], [8], [10].

[7] aaaaab=aaaab

Overlap of [1] ba=aab with [6] aaaaaaaa=aaaa:

b a aaaaaaaa

Critical pair: baaaa=aabaaaaaaa.

Reduce LHS:

[1](ba)aaa
[1]⇒ aa(ba)aa
[1]⇒ aaaa(ba)a
[4]⇒ (aaaaaab)a
[1]⇒ aaa(ba)
⇒ aaaaab

Reduce RHS:

[1]aa(ba)aaaaaa
[1]⇒ aaaa(ba)aaaaa
[4]⇒ (aaaaaab)aaaaa
[1]⇒ aaa(ba)aaaa
[1]⇒ aaaaa(ba)aaa
[4]⇒ a(aaaaaab)aaa
[1]⇒ aaaa(ba)aa
[4]⇒ (aaaaaab)aa
[1]⇒ aaa(ba)a
[1]⇒ aaaaa(ba)
[4]⇒ a(aaaaaab)
⇒ aaaab

Referenced by [9].

[8] aaaaaa=aaaaa

Overlap of [5] aaaaaaaaa=aaaaaa with [6] aaaaaaaa=aaaa:

aaaaaaaaa aaaaaaaa

Critical pair: aaaaa=aaaaaa.

Flip LHS and RHS.

Referenced by [9], [10].

[9] aaaab=aaab

Overlap of [4] aaaaaab=aaab with [8] aaaaaa=aaaaa:

aaaaaab aaaaaa

Critical pair: aaaaab=aaab.

Reduce LHS:

[7](aaaaab)
⇒ aaaab

Defines rule #2.

[10] aaaaa=aaaa

Overlap of [6] aaaaaaaa=aaaa with [8] aaaaaa=aaaaa:

aaaaaaaa aaaaaa

Critical pair: aaaaaaa=aaaa.

Reduce LHS:

[8](aaaaaa)a
[8]⇒ (aaaaaa)
⇒ aaaaa

Defines rule #1.