Certificate for #19563 ⟨a, b | aab=b, abbba=bb⟩

Completion settings:

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

[1] aab=b

Axiom: aab=b.

Defines rule #4.

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

[2] abbba=bb

Axiom: abbba=bb.

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

[3] bbba=abb

Overlap of [1] aab=b with [2] abbba=bb:

a ab abbba

Critical pair: abb=bbba.

Flip LHS and RHS.

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

[4] bbab=abbbb

Overlap of [2] abbba=bb with [1] aab=b:

abbb a aab

Critical pair: abbbb=bbab.

Flip LHS and RHS.

Referenced by [5], [7].

[5] babbbb=abbb

Overlap of [3] bbba=abb with [4] bbab=abbbb:

b bba bbab

Critical pair: babbbb=abbb.

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

[6] bababb=bb

Overlap of [5] babbbb=abbb with [3] bbba=abb:

bab bbb bbba

Critical pair: bababb=abbba.

Reduce RHS:

[2]	(abbba)
	⇒ bb

Referenced by [8].

[7] ababb=bbbbbb

Overlap of [5] babbbb=abbb with [3] bbba=abb:

babb bb bbba

Critical pair: babbabb=abbbba.

Reduce LHS:

[4]	ba(bbab)b
[1]	⇒ b(aab)bbbb
	⇒ bbbbbb

Reduce RHS:

[3]	ab(bbba)
	⇒ ababb

Flip LHS and RHS.

Referenced by [8].

[8] bbbbbbb=bb

Simplify [6] bababb=bb.

Reduce LHS:

[7]	b(ababb)
	⇒ bbbbbbb

Defines rule #1.

Referenced by [9], [10].

[9] babb=abbbbbb

Overlap of [5] babbbb=abbb with [8] bbbbbbb=bb:

ba bbbb bbbbbbb

Critical pair: babb=abbbbbb.

Defines rule #2.

Referenced by [10].

[10] bba=abbb

Overlap of [8] bbbbbbb=bb with [3] bbba=abb:

bbbb bbb bbba

Critical pair: bbbbabb=bba.

Reduce LHS:

[3]	b(bbba)bb
[9]	⇒ (babb)bb
[8]	⇒ a(bbbbbbb)b
	⇒ abbb

Flip LHS and RHS.

Defines rule #3.