Certification Problem

Input (TPDB TRS_Standard/SK90/2.49)

The rewrite relation of the following TRS is considered.

a(c(d(x)))	→	c(x)	(1)
u(b(d(d(x))))	→	b(x)	(2)
v(a(a(x)))	→	u(v(x))	(3)
v(a(c(x)))	→	u(b(d(x)))	(4)
v(c(x))	→	b(x)	(5)
w(a(a(x)))	→	u(w(x))	(6)
w(a(c(x)))	→	u(b(d(x)))	(7)
w(c(x))	→	b(x)	(8)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by NaTT @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

w^#(a(a(x)))	→	w^#(x)	(9)
v^#(a(c(x)))	→	u^#(b(d(x)))	(10)
v^#(a(a(x)))	→	v^#(x)	(11)
w^#(a(c(x)))	→	u^#(b(d(x)))	(12)
w^#(a(a(x)))	→	u^#(w(x))	(13)
v^#(a(a(x)))	→	u^#(v(x))	(14)

1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.

The 1^st component contains the pair

v^#(a(a(x)))

→

v^#(x)

(11)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a(x₁)]	=	x₁ + 1
[d(x₁)]	=	0
[v(x₁)]	=	0
[w^#(x₁)]	=	0
[b(x₁)]	=	0
[u(x₁)]	=	0
[u^#(x₁)]	=	0
[w(x₁)]	=	0
[c(x₁)]	=	0
[v^#(x₁)]	=	x₁ + 0
[a^#(x₁)]	=	0

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the pair

v^#(a(a(x)))

→

v^#(x)

(11)

could be deleted.

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 2^nd component contains the pair

w^#(a(a(x)))

→

w^#(x)

(9)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a(x₁)]	=	x₁ + 1
[d(x₁)]	=	0
[v(x₁)]	=	0
[w^#(x₁)]	=	x₁ + 0
[b(x₁)]	=	0
[u(x₁)]	=	0
[u^#(x₁)]	=	0
[w(x₁)]	=	0
[c(x₁)]	=	0
[v^#(x₁)]	=	0
[a^#(x₁)]	=	0

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the pair

w^#(a(a(x)))

→

w^#(x)

(9)

could be deleted.

1.1.2.1 Dependency Graph Processor

The dependency pairs are split into 0 components.