Certificate for #12623 ⟨a, b | baab=ab, bbbb=b⟩

Completion settings:

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

[1] baab=ab

Axiom: baab=ab.

Defines rule #3.

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

[2] bbbb=b

Axiom: bbbb=b.

Defines rule #5.

Referenced by [4].

[3] baaab=aab

Overlap of [1] baab=ab with [1] baab=ab:

baa b baab

Critical pair: baaab=abaab.

Reduce RHS:

[1]	a(baab)
	⇒ aab

Defines rule #4.

Referenced by [6], [7].

[4] bbbab=ab

Overlap of [2] bbbb=b with [1] baab=ab:

bbb b baab

Critical pair: bbbab=baab.

Reduce RHS:

[1]	(baab)
	⇒ ab

Referenced by [5], [6].

[5] bbab=aab

Overlap of [4] bbbab=ab with [1] baab=ab:

bbba b baab

Critical pair: bbbaab=abaab.

Reduce LHS:

[1]	bb(baab)
	⇒ bbab

Reduce RHS:

[1]	a(baab)
	⇒ aab

Referenced by [6], [7].

[6] bab=aaab

Overlap of [4] bbbab=ab with [5] bbab=aab:

bbba b bbab

Critical pair: bbbaaab=abbab.

Reduce LHS:

[3]	bb(baaab)
[1]	⇒ b(baab)
	⇒ bab

Reduce RHS:

[5]	a(bbab)
	⇒ aaab

Defines rule #2.

[7] aaaab=ab

Overlap of [5] bbab=aab with [5] bbab=aab:

bba b bbab

Critical pair: bbaaab=aabbab.

Reduce LHS:

[3]	b(baaab)
[1]	⇒ (baab)
	⇒ ab

Reduce RHS:

[5]	aa(bbab)
	⇒ aaaab

Flip LHS and RHS.

Defines rule #1.