Certificate for #16272 ⟨a, b | aab=ba, bbbb=bb⟩

Completion settings:

Reduction order:
- Right-to-left recursive path with deg(a) = 0; deg(b) = 1

[1] ba=aab

Axiom: aab=ba.

Flip LHS and RHS.

Defines rule #1.

Referenced by [3].

[2] bbbb=bb

Axiom: bbbb=bb.

Defines rule #3.

Referenced by [3].

[3] aaaaaaaaaaaaaaaabb=aaaabb

Overlap of [2] bbbb=bb with [1] ba=aab:

bbb b ba

Critical pair: bbbaab=bba.

Reduce LHS:

[1]	bb(ba)ab
[1]	⇒ b(ba)abab
[1]	⇒ (ba)ababab
[1]	⇒ aa(ba)babab
[1]	⇒ aaaab(ba)bab
[1]	⇒ aaaa(ba)abbab
[1]	⇒ aaaaaa(ba)bbab
[1]	⇒ aaaaaaaabb(ba)b
[1]	⇒ aaaaaaaab(ba)abb
[1]	⇒ aaaaaaaa(ba)ababb
[1]	⇒ aaaaaaaaaa(ba)babb
[1]	⇒ aaaaaaaaaaaab(ba)bb
[1]	⇒ aaaaaaaaaaaa(ba)abbb
[1]	⇒ aaaaaaaaaaaaaa(ba)bbb
[2]	⇒ aaaaaaaaaaaaaaaa(bbbb)
	⇒ aaaaaaaaaaaaaaaabb

Reduce RHS:

[1]	b(ba)
[1]	⇒ (ba)ab
[1]	⇒ aa(ba)b
	⇒ aaaabb

Defines rule #2.