(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
times(x, plus(y, s(z))) → plus(times(x, plus(y, times(s(z), 0))), times(x, s(z)))
times(x, 0) → 0
times(x, s(y)) → plus(times(x, y), x)
plus(s(x), s(y)) → s(s(plus(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
plus(s(x), x) → plus(if(gt(x, x), id(x), id(x)), s(x))
plus(zero, y) → y
plus(id(x), s(y)) → s(plus(x, if(gt(s(y), y), y, s(y))))
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
gt(s(x), zero) → true
gt(zero, y) → false
gt(s(x), s(y)) → gt(x, 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:
TIMES(x, plus(y, s(z))) → PLUS(times(x, plus(y, times(s(z), 0))), times(x, s(z)))
TIMES(x, plus(y, s(z))) → TIMES(x, plus(y, times(s(z), 0)))
TIMES(x, plus(y, s(z))) → PLUS(y, times(s(z), 0))
TIMES(x, plus(y, s(z))) → TIMES(s(z), 0)
TIMES(x, plus(y, s(z))) → TIMES(x, s(z))
TIMES(x, s(y)) → PLUS(times(x, y), x)
TIMES(x, s(y)) → TIMES(x, y)
PLUS(s(x), s(y)) → PLUS(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))
PLUS(s(x), s(y)) → IF(gt(x, y), x, y)
PLUS(s(x), s(y)) → GT(x, y)
PLUS(s(x), s(y)) → IF(not(gt(x, y)), id(x), id(y))
PLUS(s(x), s(y)) → NOT(gt(x, y))
PLUS(s(x), s(y)) → ID(x)
PLUS(s(x), s(y)) → ID(y)
PLUS(s(x), x) → PLUS(if(gt(x, x), id(x), id(x)), s(x))
PLUS(s(x), x) → IF(gt(x, x), id(x), id(x))
PLUS(s(x), x) → GT(x, x)
PLUS(s(x), x) → ID(x)
PLUS(id(x), s(y)) → PLUS(x, if(gt(s(y), y), y, s(y)))
PLUS(id(x), s(y)) → IF(gt(s(y), y), y, s(y))
PLUS(id(x), s(y)) → GT(s(y), y)
NOT(x) → IF(x, false, true)
GT(s(x), s(y)) → GT(x, y)
The TRS R consists of the following rules:
times(x, plus(y, s(z))) → plus(times(x, plus(y, times(s(z), 0))), times(x, s(z)))
times(x, 0) → 0
times(x, s(y)) → plus(times(x, y), x)
plus(s(x), s(y)) → s(s(plus(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
plus(s(x), x) → plus(if(gt(x, x), id(x), id(x)), s(x))
plus(zero, y) → y
plus(id(x), s(y)) → s(plus(x, if(gt(s(y), y), y, s(y))))
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
gt(s(x), zero) → true
gt(zero, y) → false
gt(s(x), s(y)) → gt(x, 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 16 less nodes.
(4) Complex Obligation (AND)
(5) Obligation:
Q DP problem:
The TRS P consists of the following rules:
GT(s(x), s(y)) → GT(x, y)
The TRS R consists of the following rules:
times(x, plus(y, s(z))) → plus(times(x, plus(y, times(s(z), 0))), times(x, s(z)))
times(x, 0) → 0
times(x, s(y)) → plus(times(x, y), x)
plus(s(x), s(y)) → s(s(plus(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
plus(s(x), x) → plus(if(gt(x, x), id(x), id(x)), s(x))
plus(zero, y) → y
plus(id(x), s(y)) → s(plus(x, if(gt(s(y), y), y, s(y))))
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
gt(s(x), zero) → true
gt(zero, y) → false
gt(s(x), s(y)) → gt(x, 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:
PLUS(s(x), x) → PLUS(if(gt(x, x), id(x), id(x)), s(x))
PLUS(s(x), s(y)) → PLUS(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))
PLUS(id(x), s(y)) → PLUS(x, if(gt(s(y), y), y, s(y)))
The TRS R consists of the following rules:
times(x, plus(y, s(z))) → plus(times(x, plus(y, times(s(z), 0))), times(x, s(z)))
times(x, 0) → 0
times(x, s(y)) → plus(times(x, y), x)
plus(s(x), s(y)) → s(s(plus(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
plus(s(x), x) → plus(if(gt(x, x), id(x), id(x)), s(x))
plus(zero, y) → y
plus(id(x), s(y)) → s(plus(x, if(gt(s(y), y), y, s(y))))
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
gt(s(x), zero) → true
gt(zero, y) → false
gt(s(x), s(y)) → gt(x, 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:
TIMES(x, plus(y, s(z))) → TIMES(x, s(z))
TIMES(x, s(y)) → TIMES(x, y)
TIMES(x, plus(y, s(z))) → TIMES(x, plus(y, times(s(z), 0)))
The TRS R consists of the following rules:
times(x, plus(y, s(z))) → plus(times(x, plus(y, times(s(z), 0))), times(x, s(z)))
times(x, 0) → 0
times(x, s(y)) → plus(times(x, y), x)
plus(s(x), s(y)) → s(s(plus(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
plus(s(x), x) → plus(if(gt(x, x), id(x), id(x)), s(x))
plus(zero, y) → y
plus(id(x), s(y)) → s(plus(x, if(gt(s(y), y), y, s(y))))
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
gt(s(x), zero) → true
gt(zero, y) → false
gt(s(x), s(y)) → gt(x, y)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.