Certificate for #19073 ⟨a, b | aab=b, bbbaaa=b⟩

Completion settings:

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

[1] aab=b

Axiom: aab=b.

Defines rule #3.

Referenced by [3], [4].

[2] bbbaaa=b

Axiom: bbbaaa=b.

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

[3] bbbab=bb

Overlap of [2] bbbaaa=b with [1] aab=b:

bbba aa aab

Critical pair: bbbab=bb.

Referenced by [5].

[4] bab=bbbb

Overlap of [2] bbbaaa=b with [1] aab=b:

bbbaa a aab

Critical pair: bbbaab=bab.

Reduce LHS:

[1]	bbb(aab)
	⇒ bbbb

Flip LHS and RHS.

Defines rule #2.

Referenced by [5], [8].

[5] bbbbbb=bb

Simplify [3] bbbab=bb.

Reduce LHS:

[4]	bb(bab)
	⇒ bbbbbb

Referenced by [6], [7].

[6] bbaaa=bbbb

Overlap of [5] bbbbbb=bb with [2] bbbaaa=b:

bbb bbb bbbaaa

Critical pair: bbbb=bbaaa.

Flip LHS and RHS.

Referenced by [7], [8].

[7] bbbbb=b

Overlap of [5] bbbbbb=bb with [6] bbaaa=bbbb:

bbbbb b bbaaa

Critical pair: bbbbbbbbb=bbbaaa.

Reduce LHS:

[5]	(bbbbbb)bbb
	⇒ bbbbb

Reduce RHS:

[2]	(bbbaaa)
	⇒ b

Defines rule #1.

Referenced by [8].

[8] baaa=bbb

Overlap of [4] bab=bbbb with [6] bbaaa=bbbb:

ba b bbaaa

Critical pair: babbbb=bbbbbaaa.

Reduce LHS:

[4]	(bab)bbb
[7]	⇒ (bbbbb)bb
	⇒ bbb

Reduce RHS:

[7]	(bbbbb)aaa
	⇒ baaa

Flip LHS and RHS.

Defines rule #4.