Certification Problem

Input (TPDB TRS_Standard/Rubio_04/polo2)

The rewrite relation of the following TRS is considered.

dx(X)	→	one	(1)
dx(a)	→	zero	(2)
dx(plus(ALPHA,BETA))	→	plus(dx(ALPHA),dx(BETA))	(3)
dx(times(ALPHA,BETA))	→	plus(times(BETA,dx(ALPHA)),times(ALPHA,dx(BETA)))	(4)
dx(minus(ALPHA,BETA))	→	minus(dx(ALPHA),dx(BETA))	(5)
dx(neg(ALPHA))	→	neg(dx(ALPHA))	(6)
dx(div(ALPHA,BETA))	→	minus(div(dx(ALPHA),BETA),times(ALPHA,div(dx(BETA),exp(BETA,two))))	(7)
dx(ln(ALPHA))	→	div(dx(ALPHA),ALPHA)	(8)
dx(exp(ALPHA,BETA))	→	plus(times(BETA,times(exp(ALPHA,minus(BETA,one)),dx(ALPHA))),times(exp(ALPHA,BETA),times(ln(ALPHA),dx(BETA))))	(9)

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.

dx^#(exp(ALPHA,BETA))	→	dx^#(ALPHA)	(10)
dx^#(minus(ALPHA,BETA))	→	dx^#(ALPHA)	(11)
dx^#(plus(ALPHA,BETA))	→	dx^#(BETA)	(12)
dx^#(times(ALPHA,BETA))	→	dx^#(ALPHA)	(13)
dx^#(times(ALPHA,BETA))	→	dx^#(BETA)	(14)
dx^#(minus(ALPHA,BETA))	→	dx^#(BETA)	(15)
dx^#(ln(ALPHA))	→	dx^#(ALPHA)	(16)
dx^#(div(ALPHA,BETA))	→	dx^#(BETA)	(17)
dx^#(exp(ALPHA,BETA))	→	dx^#(BETA)	(18)
dx^#(neg(ALPHA))	→	dx^#(ALPHA)	(19)
dx^#(plus(ALPHA,BETA))	→	dx^#(ALPHA)	(20)
dx^#(div(ALPHA,BETA))	→	dx^#(ALPHA)	(21)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

dx^#(div(ALPHA,BETA))	→	dx^#(ALPHA)	(21)
dx^#(times(ALPHA,BETA))	→	dx^#(BETA)	(14)
dx^#(plus(ALPHA,BETA))	→	dx^#(ALPHA)	(20)
dx^#(neg(ALPHA))	→	dx^#(ALPHA)	(19)
dx^#(exp(ALPHA,BETA))	→	dx^#(BETA)	(18)
dx^#(times(ALPHA,BETA))	→	dx^#(ALPHA)	(13)
dx^#(plus(ALPHA,BETA))	→	dx^#(BETA)	(12)
dx^#(minus(ALPHA,BETA))	→	dx^#(ALPHA)	(11)
dx^#(div(ALPHA,BETA))	→	dx^#(BETA)	(17)
dx^#(ln(ALPHA))	→	dx^#(ALPHA)	(16)
dx^#(minus(ALPHA,BETA))	→	dx^#(BETA)	(15)
dx^#(exp(ALPHA,BETA))	→	dx^#(ALPHA)	(10)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[zero]	=	0
[a]	=	0
[ln(x₁)]	=	x₁ + 1
[minus(x₁, x₂)]	=	x₁ + x₂ + 1
[dx^#(x₁)]	=	x₁ + 0
[div(x₁, x₂)]	=	x₁ + x₂ + 1
[two]	=	0
[dx(x₁)]	=	0
[one]	=	0
[times(x₁, x₂)]	=	x₁ + x₂ + 1
[neg(x₁)]	=	x₁ + 1
[plus(x₁, x₂)]	=	x₁ + x₂ + 1
[exp(x₁, x₂)]	=	x₁ + x₂ + 1

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

dx^#(div(ALPHA,BETA))	→	dx^#(ALPHA)	(21)
dx^#(times(ALPHA,BETA))	→	dx^#(BETA)	(14)
dx^#(plus(ALPHA,BETA))	→	dx^#(ALPHA)	(20)
dx^#(neg(ALPHA))	→	dx^#(ALPHA)	(19)
dx^#(exp(ALPHA,BETA))	→	dx^#(BETA)	(18)
dx^#(times(ALPHA,BETA))	→	dx^#(ALPHA)	(13)
dx^#(plus(ALPHA,BETA))	→	dx^#(BETA)	(12)
dx^#(minus(ALPHA,BETA))	→	dx^#(ALPHA)	(11)
dx^#(div(ALPHA,BETA))	→	dx^#(BETA)	(17)
dx^#(ln(ALPHA))	→	dx^#(ALPHA)	(16)
dx^#(minus(ALPHA,BETA))	→	dx^#(BETA)	(15)
dx^#(exp(ALPHA,BETA))	→	dx^#(ALPHA)	(10)

could be deleted.

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.