Certificate for #27687 ⟨a, b | aa=1, abbbba=bbb⟩

Completion settings:

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

[1] aa=1

Axiom: aa=1.

Defines rule #4.

Referenced by [3], [4], [8], [9], [10].

[2] abbbba=bbb

Axiom: abbbba=bbb.

Referenced by [3], [4].

[3] bbbba=abbb

Overlap of [1] aa=1 with [2] abbbba=bbb:

a a abbbba

Critical pair: abbb=bbbba.

Flip LHS and RHS.

Referenced by [5].

[4] bbba=abbbb

Overlap of [2] abbbba=bbb with [1] aa=1:

abbbb a aa

Critical pair: abbbb=bbba.

Flip LHS and RHS.

Defines rule #3.

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

[5] babbbb=abbb

Simplify [3] bbbba=abbb.

Reduce LHS:

[4]	b(bbba)
	⇒ babbbb

Referenced by [6], [7], [10].

[6] babbabbb=ababbb

Overlap of [5] babbbb=abbb with [4] bbba=abbbb:

babbb b bbba

Critical pair: babbbabbbb=abbbbba.

Reduce LHS:

[5]	babb(babbbb)
	⇒ babbabbb

Reduce RHS:

[4]	abb(bbba)
[5]	⇒ ab(babbbb)
	⇒ ababbb

Referenced by [8].

[7] bbabbb=abbbbbbbb

Overlap of [4] bbba=abbbb with [5] babbbb=abbb:

bb ba babbbb

Critical pair: bbabbb=abbbbbbbb.

Referenced by [8].

[8] ababbb=bbbbbbbbb

Simplify [6] babbabbb=ababbb.

Reduce LHS:

[7]	ba(bbabbb)
[1]	⇒ b(aa)bbbbbbbb
	⇒ bbbbbbbbb

Flip LHS and RHS.

Referenced by [9], [10].

[9] babbb=abbbbbbbbb

Overlap of [1] aa=1 with [8] ababbb=bbbbbbbbb:

a a ababbb

Critical pair: abbbbbbbbb=babbb.

Flip LHS and RHS.

Defines rule #2.

[10] bbbbbbbbbb=bbb

Overlap of [8] ababbb=bbbbbbbbb with [5] babbbb=abbb:

a babbb babbbb

Critical pair: aabbb=bbbbbbbbbb.

Reduce LHS:

[1]	(aa)bbb
	⇒ bbb

Flip LHS and RHS.

Defines rule #1.