(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
p(0) → 0
p(s(x)) → x
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
minus(x, s(y)) → p(minus(x, y))
div(0, s(y)) → 0
div(s(x), s(y)) → s(div(minus(s(x), s(y)), s(y)))
log(s(0), s(s(y))) → 0
log(s(s(x)), s(s(y))) → s(log(div(minus(x, y), s(s(y))), s(s(y))))
Q is empty.
(1) DependencyPairsProof (EQUIVALENT transformation)
Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.
(2) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MINUS(s(x), s(y)) → MINUS(x, y)
MINUS(x, s(y)) → P(minus(x, y))
MINUS(x, s(y)) → MINUS(x, y)
DIV(s(x), s(y)) → DIV(minus(s(x), s(y)), s(y))
DIV(s(x), s(y)) → MINUS(s(x), s(y))
LOG(s(s(x)), s(s(y))) → LOG(div(minus(x, y), s(s(y))), s(s(y)))
LOG(s(s(x)), s(s(y))) → DIV(minus(x, y), s(s(y)))
LOG(s(s(x)), s(s(y))) → MINUS(x, y)
The TRS R consists of the following rules:
p(0) → 0
p(s(x)) → x
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
minus(x, s(y)) → p(minus(x, y))
div(0, s(y)) → 0
div(s(x), s(y)) → s(div(minus(s(x), s(y)), s(y)))
log(s(0), s(s(y))) → 0
log(s(s(x)), s(s(y))) → s(log(div(minus(x, y), s(s(y))), s(s(y))))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(3) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 3 SCCs with 4 less nodes.
(4) Complex Obligation (AND)
(5) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MINUS(x, s(y)) → MINUS(x, y)
MINUS(s(x), s(y)) → MINUS(x, y)
The TRS R consists of the following rules:
p(0) → 0
p(s(x)) → x
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
minus(x, s(y)) → p(minus(x, y))
div(0, s(y)) → 0
div(s(x), s(y)) → s(div(minus(s(x), s(y)), s(y)))
log(s(0), s(s(y))) → 0
log(s(s(x)), s(s(y))) → s(log(div(minus(x, y), s(s(y))), s(s(y))))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(6) Obligation:
Q DP problem:
The TRS P consists of the following rules:
DIV(s(x), s(y)) → DIV(minus(s(x), s(y)), s(y))
The TRS R consists of the following rules:
p(0) → 0
p(s(x)) → x
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
minus(x, s(y)) → p(minus(x, y))
div(0, s(y)) → 0
div(s(x), s(y)) → s(div(minus(s(x), s(y)), s(y)))
log(s(0), s(s(y))) → 0
log(s(s(x)), s(s(y))) → s(log(div(minus(x, y), s(s(y))), s(s(y))))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(7) Obligation:
Q DP problem:
The TRS P consists of the following rules:
LOG(s(s(x)), s(s(y))) → LOG(div(minus(x, y), s(s(y))), s(s(y)))
The TRS R consists of the following rules:
p(0) → 0
p(s(x)) → x
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
minus(x, s(y)) → p(minus(x, y))
div(0, s(y)) → 0
div(s(x), s(y)) → s(div(minus(s(x), s(y)), s(y)))
log(s(0), s(s(y))) → 0
log(s(s(x)), s(s(y))) → s(log(div(minus(x, y), s(s(y))), s(s(y))))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.