Certificate for #20219 ⟨a, b | aba=a, abba=bbb⟩

Completion settings:

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

[1] aba=a

Axiom: aba=a.

Defines rule #4.

Referenced by [3], [4].

[2] abba=bbb

Axiom: abba=bbb.

Defines rule #5.

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

[3] abbbb=bbb

Overlap of [1] aba=a with [2] abba=bbb:

ab a abba

Critical pair: abbbb=abba.

Reduce RHS:

[2]	(abba)
	⇒ bbb

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

[4] bbbba=bbb

Overlap of [2] abba=bbb with [1] aba=a:

abb a aba

Critical pair: abba=bbbba.

Reduce LHS:

[2]	(abba)
	⇒ bbb

Flip LHS and RHS.

Referenced by [5], [6].

[5] bbba=abbb

Overlap of [3] abbbb=bbb with [4] bbbba=bbb:

a bbbb bbbba

Critical pair: abbb=bbba.

Flip LHS and RHS.

Referenced by [6], [8].

[6] bbbbbb=bbb

Overlap of [3] abbbb=bbb with [5] bbba=abbb:

abb bb bbba

Critical pair: abbabbb=bbbba.

Reduce LHS:

[2]	(abba)bbb
	⇒ bbbbbb

Reduce RHS:

[4]	(bbbba)
	⇒ bbb

Defines rule #1.

Referenced by [7].

[7] abbb=bbbbb

Overlap of [3] abbbb=bbb with [6] bbbbbb=bbb:

a bbbb bbbbbb

Critical pair: abbb=bbbbb.

Defines rule #2.

Referenced by [8].

[8] bbba=bbbbb

Simplify [5] bbba=abbb.

Reduce RHS:

[7]	(abbb)
	⇒ bbbbb

Defines rule #3.