Certificate for #16237 ⟨a, b | aab=ba, abbb=aa⟩

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 #2.

Referenced by [3], [4].

[2] abbb=aa

Axiom: abbb=aa.

Defines rule #3.

Referenced by [3], [4].

[3] aaaab=aaab

Overlap of [1] ba=aab with [2] abbb=aa:

b a abbb

Critical pair: baa=aabbbb.

Reduce LHS:

[1]	(ba)a
[1]	⇒ aa(ba)
	⇒ aaaab

Reduce RHS:

[2]	a(abbb)b
	⇒ aaab

Referenced by [4].

[4] aaaa=aaa

Overlap of [2] abbb=aa with [1] ba=aab:

abb b ba

Critical pair: abbaab=aaa.

Reduce LHS:

[1]	ab(ba)ab
[1]	⇒ a(ba)abab
[1]	⇒ aaa(ba)bab
[3]	⇒ a(aaaab)bab
[3]	⇒ (aaaab)bab
[1]	⇒ aaab(ba)b
[1]	⇒ aaa(ba)abb
[3]	⇒ a(aaaab)abb
[3]	⇒ (aaaab)abb
[1]	⇒ aaa(ba)bb
[3]	⇒ a(aaaab)bb
[3]	⇒ (aaaab)bb
[2]	⇒ aa(abbb)
	⇒ aaaa

Defines rule #1.