Certificate for #657 ⟨a, b | bb=aa, aba=b⟩

Completion settings:

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

[1] aa=bb

Axiom: bb=aa.

Flip LHS and RHS.

Defines rule #3.

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

[2] aba=b

Axiom: aba=b.

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

[3] bba=abb

Overlap of [1] aa=bb with [1] aa=bb:

a a aa

Critical pair: abb=bba.

Flip LHS and RHS.

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

[4] babb=ab

Overlap of [1] aa=bb with [2] aba=b:

a a aba

Critical pair: ab=bbba.

Reduce RHS:

[3]	b(bba)
	⇒ babb

Flip LHS and RHS.

Referenced by [7].

[5] ba=abbb

Overlap of [2] aba=b with [1] aa=bb:

ab a aa

Critical pair: abbb=ba.

Flip LHS and RHS.

Defines rule #2.

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

[6] bbbbbb=bb

Overlap of [5] ba=abbb with [2] aba=b:

b a aba

Critical pair: bb=abbbba.

Reduce RHS:

[3]	abb(bba)
[3]	⇒ a(bba)bb
[1]	⇒ (aa)bbbb
	⇒ bbbbbb

Flip LHS and RHS.

Referenced by [8].

[7] abbbbb=ab

Simplify [4] babb=ab.

Reduce LHS:

[5]	(ba)bb
	⇒ abbbbb

Referenced by [8].

[8] bbbbb=b

Overlap of [7] abbbbb=ab with [5] ba=abbb:

abbbb b ba

Critical pair: abbbbabbb=aba.

Reduce LHS:

[3]	abb(bba)bbb
[3]	⇒ a(bba)bbbbb
[1]	⇒ (aa)bbbbbbb
[6]	⇒ (bbbbbb)bbb
	⇒ bbbbb

Reduce RHS:

[2]	(aba)
	⇒ b

Defines rule #1.