Certificate for #22822 ⟨a, b | aaa=1, abbbb=bba⟩

Completion settings:

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

[1] aaa=1

Axiom: aaa=1.

Defines rule #3.

Referenced by [3].

[2] bba=abbbb

Axiom: abbbb=bba.

Flip LHS and RHS.

Defines rule #2.

Referenced by [3].

[3] bbbbbbbbbbbbbbbb=bb

Overlap of [2] bba=abbbb with [1] aaa=1:

bb a aaa

Critical pair: bb=abbbbaa.

Reduce RHS:

[2]	abb(bba)a
[2]	⇒ a(bba)bbbba
[2]	⇒ aabbbbbb(bba)
[2]	⇒ aabbbb(bba)bbbb
[2]	⇒ aabb(bba)bbbbbbbb
[2]	⇒ aa(bba)bbbbbbbbbbbb
[1]	⇒ (aaa)bbbbbbbbbbbbbbbb
	⇒ bbbbbbbbbbbbbbbb

Flip LHS and RHS.

Defines rule #1.