Certificate for #1648 ⟨a, b | aab=bb, abb=a⟩

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

[2] abb=a

Axiom: abb=a.

Defines rule #2.

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

[3] aa=bbb

Overlap of [1] aab=bb with [2] abb=a:

a ab abb

Critical pair: aa=bbb.

Defines rule #4.

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

[4] bbbb=bb

Overlap of [1] aab=bb with [3] aa=bbb:

aab aa

Critical pair: bbbb=bb.

Defines rule #1.

Referenced by [6], [7].

[5] bbba=ab

Overlap of [3] aa=bbb with [3] aa=bbb:

a a aa

Critical pair: abbb=bbba.

Reduce LHS:

[2]	(abb)b
	⇒ ab

Flip LHS and RHS.

Referenced by [6], [7].

[6] bba=a

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

aa b bbba

Critical pair: aaab=bbbba.

Reduce LHS:

[3]	(aa)ab
[5]	⇒ (bbba)b
[2]	⇒ (abb)
	⇒ a

Reduce RHS:

[4]	(bbbb)a
	⇒ bba

Flip LHS and RHS.

Referenced by [7].

[7] bab=a

Overlap of [4] bbbb=bb with [5] bbba=ab:

b bbb bbba

Critical pair: bab=bba.

Reduce RHS:

[6]	(bba)
	⇒ a

Referenced by [8].

[8] ba=ab

Overlap of [7] bab=a with [2] abb=a:

b ab abb

Critical pair: ba=ab.

Defines rule #3.