Certificate for #19175 ⟨a, b | aba=b, aaabbb=b⟩

Completion settings:

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

[1] aba=b

Axiom: aba=b.

Referenced by [3], [5], [7], [8], [11].

[2] aaabbb=b

Axiom: aaabbb=b.

Referenced by [4].

[3] abb=bba

Overlap of [1] aba=b with [1] aba=b:

ab a aba

Critical pair: abb=bba.

Referenced by [4], [6].

[4] bbaaab=b

Simplify [2] aaabbb=b.

Reduce LHS:

[3]	aa(abb)b
[3]	⇒ a(abb)ab
[3]	⇒ (abb)aab
	⇒ bbaaab

Referenced by [5], [6].

[5] bbaab=ba

Overlap of [4] bbaaab=b with [1] aba=b:

bbaa ab aba

Critical pair: bbaab=ba.

Referenced by [7].

[6] bbaaaab=ab

Overlap of [3] abb=bba with [4] bbaaab=b:

a bb bbaaab

Critical pair: ab=bbaaaab.

Flip LHS and RHS.

Referenced by [10].

[7] bbab=baa

Overlap of [5] bbaab=ba with [1] aba=b:

bba ab aba

Critical pair: bbab=baa.

Referenced by [8], [9].

[8] bbb=baaa

Overlap of [7] bbab=baa with [1] aba=b:

bb ab aba

Critical pair: bbb=baaa.

Defines rule #3.

Referenced by [9], [10].

[9] baaaab=bbaa

Overlap of [8] bbb=baaa with [7] bbab=baa:

b bb bbab

Critical pair: bbaa=baaaab.

Flip LHS and RHS.

Referenced by [10].

[10] ab=baaaaa

Simplify [6] bbaaaab=ab.

Reduce LHS:

[9]	b(baaaab)
[8]	⇒ (bbb)aa
	⇒ baaaaa

Flip LHS and RHS.

Defines rule #2.

Referenced by [11].

[11] baaaaaa=b

Overlap of [1] aba=b with [10] ab=baaaaa:

aba ab

Critical pair: baaaaaa=b.

Defines rule #1.