Certificate for #15703 ⟨a, b | aab=ba, abbbb=a⟩

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].

[2] abbbb=a

Axiom: abbbb=a.

Defines rule #3.

Referenced by [3].

[3] aaaaaaaaaaaaaaaaa=aa

Overlap of [2] abbbb=a with [1] ba=aab:

abbb b ba

Critical pair: abbbaab=aa.

Reduce LHS:

[1]	abb(ba)ab
[1]	⇒ ab(ba)abab
[1]	⇒ a(ba)ababab
[1]	⇒ aaa(ba)babab
[1]	⇒ aaaaab(ba)bab
[1]	⇒ aaaaa(ba)abbab
[1]	⇒ aaaaaaa(ba)bbab
[1]	⇒ aaaaaaaaabb(ba)b
[1]	⇒ aaaaaaaaab(ba)abb
[1]	⇒ aaaaaaaaa(ba)ababb
[1]	⇒ aaaaaaaaaaa(ba)babb
[1]	⇒ aaaaaaaaaaaaab(ba)bb
[1]	⇒ aaaaaaaaaaaaa(ba)abbb
[1]	⇒ aaaaaaaaaaaaaaa(ba)bbb
[2]	⇒ aaaaaaaaaaaaaaaa(abbbb)
	⇒ aaaaaaaaaaaaaaaaa

Defines rule #1.