Certificate for #16314 ⟨a, b | aab=bb, baba=ab⟩

Completion settings:

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

[1] aab=bb

Axiom: aab=bb.

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

[2] baba=ab

Axiom: baba=ab.

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

[3] bab=abb

Overlap of [1] aab=bb with [2] baba=ab:

aa b baba

Critical pair: aaab=bbaba.

Reduce LHS:

[1]	a(aab)
	⇒ abb

Reduce RHS:

[2]	b(baba)
	⇒ bab

Flip LHS and RHS.

Referenced by [5], [6].

[4] abba=bbb

Overlap of [2] baba=ab with [2] baba=ab:

ba ba baba

Critical pair: baab=abba.

Reduce LHS:

[1]	b(aab)
	⇒ bbb

Flip LHS and RHS.

Referenced by [5], [7].

[5] ab=bbb

Overlap of [2] baba=ab with [3] bab=abb:

baba bab

Critical pair: abba=ab.

Reduce LHS:

[4]	(abba)
	⇒ bbb

Flip LHS and RHS.

Defines rule #2.

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

[6] bbbbbb=bbb

Overlap of [5] ab=bbb with [3] bab=abb:

a b bab

Critical pair: aabb=bbbab.

Reduce LHS:

[1]	(aab)b
	⇒ bbb

Reduce RHS:

[3]	bb(bab)
[3]	⇒ b(bab)b
[3]	⇒ (bab)bb
[5]	⇒ (ab)bbb
	⇒ bbbbbb

Flip LHS and RHS.

Referenced by [8].

[7] bbbba=bbb

Simplify [4] abba=bbb.

Reduce LHS:

[5]	(ab)ba
	⇒ bbbba

Referenced by [8].

[8] bbba=bbbbb

Overlap of [5] ab=bbb with [7] bbbba=bbb:

a b bbbba

Critical pair: abbb=bbbbbba.

Reduce LHS:

[5]	(ab)bb
	⇒ bbbbb

Reduce RHS:

[6]	(bbbbbb)a
	⇒ bbba

Flip LHS and RHS.

Referenced by [10].

[9] bbbbb=bb

Overlap of [1] aab=bb with [5] ab=bbb:

a ab ab

Critical pair: abbb=bb.

Reduce LHS:

[5]	(ab)bb
	⇒ bbbbb

Defines rule #1.

Referenced by [10], [11].

[10] bbba=bb

Simplify [8] bbba=bbbbb.

Reduce RHS:

[9]	(bbbbb)
	⇒ bb

Referenced by [11].

[11] bba=bbbb

Overlap of [9] bbbbb=bb with [10] bbba=bb:

bb bbb bbba

Critical pair: bbbb=bba.

Flip LHS and RHS.

Defines rule #3.