Certification Problem

Input (TPDB TRS_Standard/Der95/11)

The rewrite relation of the following TRS is considered.

D(t) → 1 (1)
D(constant) → 0 (2)
D(+(x,y)) → +(D(x),D(y)) (3)
D(*(x,y)) → +(*(y,D(x)),*(x,D(y))) (4)
D(-(x,y)) → -(D(x),D(y)) (5)
D(minus(x)) → minus(D(x)) (6)
D(div(x,y)) → -(div(D(x),y),div(*(x,D(y)),pow(y,2))) (7)
D(ln(x)) → div(D(x),x) (8)
D(pow(x,y)) → +(*(*(y,pow(x,-(y,1))),D(x)),*(*(pow(x,y),ln(x)),D(y))) (9)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Rule Removal

Using the
prec(D) = 4 stat(D) = mul
prec(t) = 4 stat(t) = mul
prec(1) = 4 stat(1) = mul
prec(constant) = 5 stat(constant) = mul
prec(0) = 0 stat(0) = mul
prec(+) = 1 stat(+) = mul
prec(*) = 1 stat(*) = mul
prec(-) = 2 stat(-) = mul
prec(div) = 3 stat(div) = mul
prec(pow) = 4 stat(pow) = mul
prec(2) = 3 stat(2) = mul
prec(ln) = 4 stat(ln) = mul

π(D) = [1]
π(t) = []
π(1) = []
π(constant) = []
π(0) = []
π(+) = [1,2]
π(*) = [1,2]
π(-) = [1,2]
π(minus) = 1
π(div) = [1,2]
π(pow) = [1,2]
π(2) = []
π(ln) = [1]

all of the following rules can be deleted.
D(t) → 1 (1)
D(constant) → 0 (2)
D(+(x,y)) → +(D(x),D(y)) (3)
D(*(x,y)) → +(*(y,D(x)),*(x,D(y))) (4)
D(-(x,y)) → -(D(x),D(y)) (5)
D(div(x,y)) → -(div(D(x),y),div(*(x,D(y)),pow(y,2))) (7)
D(ln(x)) → div(D(x),x) (8)
D(pow(x,y)) → +(*(*(y,pow(x,-(y,1))),D(x)),*(*(pow(x,y),ln(x)),D(y))) (9)

1.1 Rule Removal

Using the Knuth Bendix order with w0 = 1 and the following precedence and weight functions
prec(D) = 1 weight(D) = 2
prec(minus) = 0 weight(minus) = 1
all of the following rules can be deleted.
D(minus(x)) → minus(D(x)) (6)

1.1.1 R is empty

There are no rules in the TRS. Hence, it is terminating.