Certificate for #16255 ⟨a, b | aab=ba, babb=ba⟩

Back:⟨a, b | aab=ba, babb=ba⟩

Completion settings:

[1] ba=aab

Axiom: aab=ba.

Flip LHS and RHS.

Defines rule #2.

Referenced by [2], [3].

[2] aabbb=aab

Axiom: babb=ba.

Reduce LHS:

[1](ba)bb
⇒ aabbb

Reduce RHS:

[1](ba)
⇒ aab

Defines rule #3.

Referenced by [3].

[3] aaaaaaaaaab=aaaab

Overlap of [2] aabbb=aab with [1] ba=aab:

aabb b ba

Critical pair: aabbaab=aaba.

Reduce LHS:

[1]aab(ba)ab
[1]⇒ aa(ba)abab
[1]⇒ aaaa(ba)bab
[1]⇒ aaaaaab(ba)b
[1]⇒ aaaaaa(ba)abb
[1]⇒ aaaaaaaa(ba)bb
[2]⇒ aaaaaaaa(aabbb)
⇒ aaaaaaaaaab

Reduce RHS:

[1]aa(ba)
⇒ aaaab

Defines rule #1.