Certificate for #5410 ⟨a, b | aab=bb, bab=aa⟩

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].

[2] aa=bab

Axiom: bab=aa.

Flip LHS and RHS.

Defines rule #4.

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

[3] babb=bb

Overlap of [1] aab=bb with [2] aa=bab:

aab aa

Critical pair: babb=bb.

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

[4] baba=abab

Overlap of [2] aa=bab with [2] aa=bab:

a a aa

Critical pair: abab=baba.

Flip LHS and RHS.

Defines rule #5.

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

[5] abbab=abb

Overlap of [3] babb=bb with [4] baba=abab:

bab b baba

Critical pair: bababab=bbaba.

Reduce LHS:

[4]	(baba)bab
[3]	⇒ a(babb)ab
	⇒ abbab

Reduce RHS:

[4]	b(baba)
[4]	⇒ (baba)b
[3]	⇒ a(babb)
	⇒ abb

Referenced by [9].

[6] abbb=bb

Overlap of [4] baba=abab with [3] babb=bb:

ba ba babb

Critical pair: babb=ababbb.

Reduce LHS:

[3]	(babb)
	⇒ bb

Reduce RHS:

[3]	a(babb)b
	⇒ abbb

Flip LHS and RHS.

Referenced by [7], [8].

[7] abb=bbbb

Overlap of [2] aa=bab with [6] abbb=bb:

a a abbb

Critical pair: abb=babbbb.

Reduce RHS:

[3]	(babb)bb
	⇒ bbbb

Defines rule #2.

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

[8] bbbbb=bb

Overlap of [6] abbb=bb with [7] abb=bbbb:

abbb abb

Critical pair: bbbbb=bb.

Defines rule #1.

Referenced by [10].

[9] bbbbab=bbbb

Simplify [5] abbab=abb.

Reduce LHS:

[7]	(abb)ab
	⇒ bbbbab

Reduce RHS:

[7]	(abb)
	⇒ bbbb

Referenced by [10].

[10] bbab=bb

Overlap of [8] bbbbb=bb with [9] bbbbab=bbbb:

b bbbb bbbbab

Critical pair: bbbbb=bbab.

Reduce LHS:

[8]	(bbbbb)
	⇒ bb

Flip LHS and RHS.

Referenced by [11].

[11] bba=bbbb

Overlap of [10] bbab=bb with [4] baba=abab:

b bab baba

Critical pair: babab=bba.

Reduce LHS:

[4]	(baba)b
[3]	⇒ a(babb)
[7]	⇒ (abb)
	⇒ bbbb

Flip LHS and RHS.

Defines rule #3.