Certificate for #12212 ⟨a, b | aaaa=bb, bbbb=a⟩

Completion settings:

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

[1] aaaa=bb

Axiom: aaaa=bb.

Referenced by [3].

[2] a=bbbb

Axiom: bbbb=a.

Flip LHS and RHS.

Defines rule #2.

Referenced by [3].

[3] bbbbbbbbbbbbbbbb=bb

Overlap of [1] aaaa=bb with [2] a=bbbb:

aaaa a

Critical pair: bbbbaaa=bb.

Reduce LHS:

[2]	bbbb(a)aa
[2]	⇒ bbbbbbbb(a)a
[2]	⇒ bbbbbbbbbbbb(a)
	⇒ bbbbbbbbbbbbbbbb

Defines rule #1.