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 AProVE @ termCOMP 2023)

1 Rule Removal

Using the
prec(dx) = 6 stat(dx) = mul
prec(one) = 6 stat(one) = mul
prec(a) = 0 stat(a) = mul
prec(zero) = 0 stat(zero) = mul
prec(plus) = 1 stat(plus) = lex
prec(times) = 1 stat(times) = mul
prec(minus) = 2 stat(minus) = mul
prec(div) = 3 stat(div) = mul
prec(exp) = 3 stat(exp) = mul
prec(two) = 4 stat(two) = mul
prec(ln) = 5 stat(ln) = mul

π(dx) = [1]
π(one) = []
π(a) = []
π(zero) = []
π(plus) = [2,1]
π(times) = [1,2]
π(minus) = [1,2]
π(neg) = 1
π(div) = [1,2]
π(exp) = [1,2]
π(two) = []
π(ln) = [1]

all of the following rules can be deleted.
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(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)

1.1 Rule Removal

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

1.1.1 R is empty

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