Certificate for #19279 ⟨a, b | aaa=a, abbba=bb⟩

Completion settings:

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

[1] aaa=a

Axiom: aaa=a.

Defines rule #5.

Referenced by [3], [4].

[2] abbba=bb

Axiom: abbba=bb.

Referenced by [3], [4], [5], [6], [8].

[3] aabb=bb

Overlap of [1] aaa=a with [2] abbba=bb:

aa a abbba

Critical pair: aabb=abbba.

Reduce RHS:

[2]	(abbba)
	⇒ bb

Defines rule #4.

Referenced by [5], [10].

[4] bbaa=bb

Overlap of [2] abbba=bb with [1] aaa=a:

abbb a aaa

Critical pair: abbba=bbaa.

Reduce LHS:

[2]	(abbba)
	⇒ bb

Flip LHS and RHS.

Referenced by [6].

[5] bbba=abb

Overlap of [3] aabb=bb with [2] abbba=bb:

a abb abbba

Critical pair: abb=bbba.

Flip LHS and RHS.

Referenced by [7].

[6] bba=abbb

Overlap of [2] abbba=bb with [4] bbaa=bb:

ab bba bbaa

Critical pair: abbb=bba.

Flip LHS and RHS.

Defines rule #3.

Referenced by [7], [8], [9].

[7] babbb=abb

Simplify [5] bbba=abb.

Reduce LHS:

[6]	b(bba)
	⇒ babbb

Referenced by [8], [9].

[8] bababb=bb

Overlap of [7] babbb=abb with [6] bba=abbb:

babb b bba

Critical pair: babbabbb=abbba.

Reduce LHS:

[7]	bab(babbb)
	⇒ bababb

Reduce RHS:

[2]	(abbba)
	⇒ bb

Referenced by [10].

[9] babb=abbbbbb

Overlap of [6] bba=abbb with [7] babbb=abb:

b ba babbb

Critical pair: babb=abbbbbb.

Defines rule #2.

Referenced by [10].

[10] bbbbbbb=bb

Simplify [8] bababb=bb.

Reduce LHS:

[9]	ba(babb)
[3]	⇒ b(aabb)bbbb
	⇒ bbbbbbb

Defines rule #1.