Certification Problem

Input (TPDB SRS_Standard/Zantema_04/z078)

The rewrite relation of the following TRS is considered.

f(0(x1))	→	s(0(x1))	(1)
d(0(x1))	→	0(x1)	(2)
d(s(x1))	→	s(s(d(p(s(x1)))))	(3)
f(s(x1))	→	d(f(p(s(x1))))	(4)
p(s(x1))	→	x1	(5)

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.

d^#(s(x1))	→	p^#(s(x1))	(6)
f^#(s(x1))	→	p^#(s(x1))	(7)
f^#(s(x1))	→	d^#(f(p(s(x1))))	(8)
d^#(s(x1))	→	d^#(p(s(x1)))	(9)
f^#(s(x1))	→	f^#(p(s(x1)))	(10)

1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.

The 1^st component contains the pair

f^#(s(x1))

→

f^#(p(s(x1)))

(10)

1.1.1 Reduction Pair Processor with Usable Rules

Using the argument filter

in combination with the following Weighted Path Order with the following precedence and status

prec(d)	=	0	status(d)	=	[]	list-extension(d)	=	Lex
prec(s)	=	1	status(s)	=	[1]	list-extension(s)	=	Lex
prec(p^#)	=	0	status(p^#)	=	[]	list-extension(p^#)	=	Lex
prec(f)	=	0	status(f)	=	[]	list-extension(f)	=	Lex
prec(p)	=	0	status(p)	=	[]	list-extension(p)	=	Lex
prec(0)	=	0	status(0)	=	[]	list-extension(0)	=	Lex
prec(d^#)	=	0	status(d^#)	=	[]	list-extension(d^#)	=	Lex
prec(f^#)	=	0	status(f^#)	=	[1]	list-extension(f^#)	=	Lex

and the following Max-polynomial interpretation

[d(x₁)]	=	1
[s(x₁)]	=	x₁ + 7720
[p^#(x₁)]	=	1
[f(x₁)]	=	1
[p(x₁)]	=	x₁ + 0
[0(x₁)]	=	1
[d^#(x₁)]	=	1
[f^#(x₁)]	=	x₁ + 1

together with the usable rule

p(s(x1))

→

(5)

(w.r.t. the implicit argument filter of the reduction pair), the pair

f^#(s(x1))

→

f^#(p(s(x1)))

(10)

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

d^#(s(x1))

→

d^#(p(s(x1)))

(9)

1.1.2 Reduction Pair Processor with Usable Rules