YES Termination w.r.t. Q proof of Rubio_04_polo2.ari

Termination w.r.t. Q of the given QTRS could be proven:

0 QTRS
↳1 QTRSRRRProof (⇔, 78 ms)
↳2 QTRS
↳3 QTRSRRRProof (⇔, 0 ms)
↳4 QTRS
↳5 RisEmptyProof (⇔, 0 ms)
↳6 YES

(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

dx(X) → one
dx(a) → zero
dx(plus(ALPHA, BETA)) → plus(dx(ALPHA), dx(BETA))
dx(times(ALPHA, BETA)) → plus(times(BETA, dx(ALPHA)), times(ALPHA, dx(BETA)))
dx(minus(ALPHA, BETA)) → minus(dx(ALPHA), dx(BETA))
dx(neg(ALPHA)) → neg(dx(ALPHA))
dx(div(ALPHA, BETA)) → minus(div(dx(ALPHA), BETA), times(ALPHA, div(dx(BETA), exp(BETA, two))))
dx(ln(ALPHA)) → div(dx(ALPHA), ALPHA)
dx(exp(ALPHA, BETA)) → plus(times(BETA, times(exp(ALPHA, minus(BETA, one)), dx(ALPHA))), times(exp(ALPHA, BETA), times(ln(ALPHA), dx(BETA))))

Q is empty.

(1) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Recursive path order with status [RPO].
Quasi-Precedence:
[dx1, one, neg1] > zero > two
[dx1, one, neg1] > [minus2, exp2] > ln1 > [times2, div2] > plus2 > two
a > zero > two

Status:
dx1: multiset
one: multiset
a: multiset
zero: multiset
plus2: [1,2]
times2: [2,1]
minus2: [1,2]
neg1: multiset
div2: multiset
exp2: multiset
two: multiset
ln1: multiset

With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

dx(X) → one
dx(a) → zero
dx(plus(ALPHA, BETA)) → plus(dx(ALPHA), dx(BETA))
dx(times(ALPHA, BETA)) → plus(times(BETA, dx(ALPHA)), times(ALPHA, dx(BETA)))
dx(minus(ALPHA, BETA)) → minus(dx(ALPHA), dx(BETA))
dx(div(ALPHA, BETA)) → minus(div(dx(ALPHA), BETA), times(ALPHA, div(dx(BETA), exp(BETA, two))))
dx(ln(ALPHA)) → div(dx(ALPHA), ALPHA)
dx(exp(ALPHA, BETA)) → plus(times(BETA, times(exp(ALPHA, minus(BETA, one)), dx(ALPHA))), times(exp(ALPHA, BETA), times(ln(ALPHA), dx(BETA))))


(2) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

dx(neg(ALPHA)) → neg(dx(ALPHA))

Q is empty.

(3) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Knuth-Bendix order [KBO] with precedence:
dx1 > neg1

and weight map:

dx_1=2
neg_1=1

The variable weight is 1With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

dx(neg(ALPHA)) → neg(dx(ALPHA))


(4) Obligation:

Q restricted rewrite system:
R is empty.
Q is empty.

(5) RisEmptyProof (EQUIVALENT transformation)

The TRS R is empty. Hence, termination is trivially proven.

(6) YES