Certificate for #22276 ⟨a, b | aaa=1, abbaab=bb⟩

Completion settings:

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

[1] aaa=1

Axiom: aaa=1.

Defines rule #5.

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

[2] abbaab=bb

Axiom: abbaab=bb.

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

[3] bbaab=aabb

Overlap of [1] aaa=1 with [2] abbaab=bb:

aa a abbaab

Critical pair: aabb=bbaab.

Flip LHS and RHS.

Defines rule #4.

Referenced by [4], [5].

[4] baabb=abbabb

Overlap of [2] abbaab=bb with [2] abbaab=bb:

abba ab abbaab

Critical pair: abbabb=bbbaab.

Reduce RHS:

[3]	b(bbaab)
	⇒ baabb

Flip LHS and RHS.

Referenced by [5], [6], [9].

[5] bbbbabb=abbb

Overlap of [3] bbaab=aabb with [4] baabb=abbabb:

bbaa b baabb

Critical pair: bbaaabbabb=aabbaabb.

Reduce LHS:

[1]	bb(aaa)bbabb
	⇒ bbbbabb

Reduce RHS:

[2]	a(abbaab)b
	⇒ abbb

Referenced by [7].

[6] babb=abbbb

Overlap of [4] baabb=abbabb with [2] abbaab=bb:

ba abb abbaab

Critical pair: babb=abbabbaab.

Reduce RHS:

[2]	abb(abbaab)
	⇒ abbbb

Defines rule #2.

Referenced by [7], [9].

[7] abbbbbbbbbb=abbb

Simplify [5] bbbbabb=abbb.

Reduce LHS:

[6]	bbb(babb)
[6]	⇒ bb(babb)bb
[6]	⇒ b(babb)bbbb
[6]	⇒ (babb)bbbbbb
	⇒ abbbbbbbbbb

Referenced by [8].

[8] bbbbbbbbbb=bbb

Overlap of [1] aaa=1 with [7] abbbbbbbbbb=abbb:

aa a abbbbbbbbbb

Critical pair: aaabbb=bbbbbbbbbb.

Reduce LHS:

[1]	(aaa)bbb
	⇒ bbb

Flip LHS and RHS.

Defines rule #1.

[9] baabb=aabbbbbb

Simplify [4] baabb=abbabb.

Reduce RHS:

[6]	ab(babb)
[6]	⇒ a(babb)bb
	⇒ aabbbbbb

Defines rule #3.