LMPO
YES(?,ELEMENTARY)
We consider the following Problem:
Strict Trs:
{ 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))))}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,ELEMENTARY)
Proof:
The input was oriented with the instance of
Lightweight Multiset Path Order () as induced by the safe mapping
safe(dx) = {}, safe(one) = {}, safe(a) = {}, safe(zero) = {},
safe(plus) = {1, 2}, safe(times) = {1, 2}, safe(minus) = {1, 2},
safe(neg) = {1}, safe(div) = {1, 2}, safe(exp) = {1, 2},
safe(two) = {}, safe(ln) = {1}
and precedence
empty .
Following symbols are considered recursive:
{dx}
The recursion depth is 1 .
For your convenience, here are the oriented rules in predicative
notation (possibly applying argument filtering):
Strict DPs: {}
Weak DPs : {}
Strict Trs:
{ 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;))))}
Weak Trs : {}
Hurray, we answered YES(?,ELEMENTARY)
MPO
YES(?,PRIMREC)
We consider the following Problem:
Strict Trs:
{ 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))))}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,PRIMREC)
Proof:
The input was oriented with the instance of
'multiset path orders' as induced by the precedence
dx > one, dx > plus, dx > times, dx > minus, dx > neg, dx > div,
dx > exp, dx > two, dx > ln, a ~ zero .
Hurray, we answered YES(?,PRIMREC)
POP*
MAYBE
We consider the following Problem:
Strict Trs:
{ 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))))}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..
POP* (PS)
MAYBE
We consider the following Problem:
Strict Trs:
{ 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))))}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..
Small POP*
MAYBE
We consider the following Problem:
Strict Trs:
{ 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))))}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..
Small POP* (PS)
MAYBE
We consider the following Problem:
Strict Trs:
{ 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))))}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..