Certificate for #16303 ⟨a, b | aab=bb, abbb=ba⟩

Completion settings:

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

[1] aab=bb

Axiom: aab=bb.

Defines rule #3.

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

[2] ba=abbb

Axiom: abbb=ba.

Flip LHS and RHS.

Defines rule #2.

Referenced by [3], [4].

[3] abbbbbb=abbbb

Overlap of [1] aab=bb with [2] ba=abbb:

aa b ba

Critical pair: aaabbb=bba.

Reduce LHS:

[1]	a(aab)bb
	⇒ abbbb

Reduce RHS:

[2]	b(ba)
[2]	⇒ (ba)bbb
	⇒ abbbbbb

Flip LHS and RHS.

Referenced by [4], [5].

[4] bbbbbbbbb=bbb

Overlap of [2] ba=abbb with [1] aab=bb:

b a aab

Critical pair: bbb=abbbab.

Reduce RHS:

[2]	abb(ba)b
[2]	⇒ ab(ba)bbbb
[3]	⇒ ab(abbbbbb)b
[2]	⇒ a(ba)bbbbb
[1]	⇒ (aab)bbbbbbb
	⇒ bbbbbbbbb

Flip LHS and RHS.

Referenced by [5], [7].

[5] abbbbb=abbb

Overlap of [3] abbbbbb=abbbb with [4] bbbbbbbbb=bbb:

a bbbbbb bbbbbbbbb

Critical pair: abbb=abbbbbbb.

Reduce RHS:

[3]	(abbbbbb)b
	⇒ abbbbb

Flip LHS and RHS.

Referenced by [6].

[6] bbbbbb=bbbb

Overlap of [1] aab=bb with [5] abbbbb=abbb:

a ab abbbbb

Critical pair: aabbb=bbbbbb.

Reduce LHS:

[1]	(aab)bb
	⇒ bbbb

Flip LHS and RHS.

Referenced by [7].

[7] bbbbb=bbb

Overlap of [4] bbbbbbbbb=bbb with [6] bbbbbb=bbbb:

bbbbbbbbb bbbbbb

Critical pair: bbbbbbb=bbb.

Reduce LHS:

[6]	(bbbbbb)b
	⇒ bbbbb

Defines rule #1.