Certificate for #12483 ⟨a, b | aabb=ba, bbbb=b⟩

Completion settings:

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

[1] aabb=ba

Axiom: aabb=ba.

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

[2] bbbb=b

Axiom: bbbb=b.

Defines rule #1.

Referenced by [3].

[3] aab=babb

Overlap of [1] aabb=ba with [2] bbbb=b:

aa bb bbbb

Critical pair: aab=babb.

Defines rule #4.

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

[4] babbb=ba

Overlap of [1] aabb=ba with [3] aab=babb:

aabb aab

Critical pair: babbb=ba.

Defines rule #2.

Referenced by [5], [6].

[5] baa=bbab

Overlap of [1] aabb=ba with [4] babbb=ba:

aab b babbb

Critical pair: aabba=baabbb.

Reduce LHS:

[3]	(aab)ba
[4]	⇒ (babbb)a
	⇒ baa

Reduce RHS:

[3]	b(aab)bb
[4]	⇒ b(babbb)b
	⇒ bbab

Defines rule #3.

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

[6] babab=bbaba

Overlap of [1] aabb=ba with [5] baa=bbab:

aab b baa

Critical pair: aabbbab=baaa.

Reduce LHS:

[3]	(aab)bbab
[4]	⇒ (babbb)bab
	⇒ babab

Reduce RHS:

[5]	(baa)a
	⇒ bbaba

Defines rule #5.

Referenced by [7].

[7] babbaba=bbabbabb

Overlap of [6] babab=bbaba with [6] babab=bbaba:

ba bab babab

Critical pair: babbaba=bbabaab.

Reduce RHS:

[5]	bba(baa)b
	⇒ bbabbabb

Defines rule #6.

Referenced by [8].

[8] babbabbab=bbabbabba

Overlap of [7] babbaba=bbabbabb with [5] baa=bbab:

babba ba baa

Critical pair: babbabbab=bbabbabba.

Defines rule #7.