Certificate for #16509 ⟨a, b | aab=ba, abb=aaa⟩

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

Completion settings:

[1] ba=aab

Axiom: aab=ba.

Flip LHS and RHS.

Defines rule #2.

Referenced by [3], [4].

[2] abb=aaa

Axiom: abb=aaa.

Defines rule #3.

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

[3] aaaaaab=aaaab

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

b a abb

Critical pair: baaa=aabbb.

Reduce LHS:

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

Reduce RHS:

[2]a(abb)b
⇒ aaaab

Referenced by [5].

[4] aaaaaaa=aaaa

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

ab b ba

Critical pair: abaab=aaaa.

Reduce LHS:

[1]a(ba)ab
[1]⇒ aaa(ba)b
[2]⇒ aaaa(abb)
⇒ aaaaaaa

Referenced by [5], [6].

[5] aaaaaa=aaaaa

Overlap of [3] aaaaaab=aaaab with [2] abb=aaa:

aaaaa ab abb

Critical pair: aaaaaaaa=aaaabb.

Reduce LHS:

[4](aaaaaaa)a
⇒ aaaaa

Reduce RHS:

[2]aaa(abb)
⇒ aaaaaa

Flip LHS and RHS.

Referenced by [6].

[6] aaaaa=aaaa

Overlap of [4] aaaaaaa=aaaa with [5] aaaaaa=aaaaa:

aaaaaaa aaaaaa

Critical pair: aaaaaa=aaaa.

Reduce LHS:

[5](aaaaaa)
⇒ aaaaa

Defines rule #1.