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

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
dx#(plus(ALPHA,BETA)) → dx#(BETA) (10)
dx#(plus(ALPHA,BETA)) → dx#(ALPHA) (11)
dx#(times(ALPHA,BETA)) → dx#(BETA) (12)
dx#(times(ALPHA,BETA)) → dx#(ALPHA) (13)
dx#(minus(ALPHA,BETA)) → dx#(BETA) (14)
dx#(minus(ALPHA,BETA)) → dx#(ALPHA) (15)
dx#(neg(ALPHA)) → dx#(ALPHA) (16)
dx#(div(ALPHA,BETA)) → dx#(BETA) (17)
dx#(div(ALPHA,BETA)) → dx#(ALPHA) (18)
dx#(ln(ALPHA)) → dx#(ALPHA) (19)
dx#(exp(ALPHA,BETA)) → dx#(BETA) (20)
dx#(exp(ALPHA,BETA)) → dx#(ALPHA) (21)

1.1 Size-Change Termination

Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

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

As there is no critical graph in the transitive closure, there are no infinite chains.