(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:
Combined order from the following AFS and order.
dx(
x1) =
dx(
x1)
one =
one
a =
a
zero =
zero
plus(
x1,
x2) =
plus(
x1,
x2)
times(
x1,
x2) =
times(
x1,
x2)
minus(
x1,
x2) =
minus(
x1,
x2)
neg(
x1) =
x1
div(
x1,
x2) =
div(
x1,
x2)
exp(
x1,
x2) =
exp(
x1,
x2)
two =
two
ln(
x1) =
ln(
x1)
Recursive path order with status [RPO].
Quasi-Precedence:
[dx1, one, two] > [a, zero] > minus2
[dx1, one, two] > plus2 > minus2
[dx1, one, two] > [times2, div2, ln1] > exp2 > minus2
Status:
ln1: multiset
plus2: multiset
a: multiset
exp2: multiset
zero: multiset
dx1: [1]
minus2: multiset
div2: multiset
one: multiset
times2: [1,2]
two: 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:
Polynomial interpretation [POLO]:
POL(dx(x1)) = 2 + 2·x1
POL(neg(x1)) = 1 + x1
With 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) TRUE
(7) RisEmptyProof (EQUIVALENT transformation)
The TRS R is empty. Hence, termination is trivially proven.
(8) TRUE