(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
+(x, 0) → x
+(0, x) → x
+(s(x), s(y)) → s(s(+(x, y)))
+(+(x, y), z) → +(x, +(y, z))
*(x, 0) → 0
*(0, x) → 0
*(s(x), s(y)) → s(+(*(x, y), +(x, y)))
*(*(x, y), z) → *(x, *(y, z))
app(nil, l) → l
app(cons(x, l1), l2) → cons(x, app(l1, l2))
sum(nil) → 0
sum(cons(x, l)) → +(x, sum(l))
sum(app(l1, l2)) → +(sum(l1), sum(l2))
prod(nil) → s(0)
prod(cons(x, l)) → *(x, prod(l))
prod(app(l1, l2)) → *(prod(l1), prod(l2))
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:
+1(s(x), s(y)) → +1(x, y)
+1(+(x, y), z) → +1(x, +(y, z))
+1(+(x, y), z) → +1(y, z)
*1(s(x), s(y)) → +1(*(x, y), +(x, y))
*1(s(x), s(y)) → *1(x, y)
*1(s(x), s(y)) → +1(x, y)
*1(*(x, y), z) → *1(x, *(y, z))
*1(*(x, y), z) → *1(y, z)
APP(cons(x, l1), l2) → APP(l1, l2)
SUM(cons(x, l)) → +1(x, sum(l))
SUM(cons(x, l)) → SUM(l)
SUM(app(l1, l2)) → +1(sum(l1), sum(l2))
SUM(app(l1, l2)) → SUM(l1)
SUM(app(l1, l2)) → SUM(l2)
PROD(cons(x, l)) → *1(x, prod(l))
PROD(cons(x, l)) → PROD(l)
PROD(app(l1, l2)) → *1(prod(l1), prod(l2))
PROD(app(l1, l2)) → PROD(l1)
PROD(app(l1, l2)) → PROD(l2)
The TRS R consists of the following rules:
+(x, 0) → x
+(0, x) → x
+(s(x), s(y)) → s(s(+(x, y)))
+(+(x, y), z) → +(x, +(y, z))
*(x, 0) → 0
*(0, x) → 0
*(s(x), s(y)) → s(+(*(x, y), +(x, y)))
*(*(x, y), z) → *(x, *(y, z))
app(nil, l) → l
app(cons(x, l1), l2) → cons(x, app(l1, l2))
sum(nil) → 0
sum(cons(x, l)) → +(x, sum(l))
sum(app(l1, l2)) → +(sum(l1), sum(l2))
prod(nil) → s(0)
prod(cons(x, l)) → *(x, prod(l))
prod(app(l1, l2)) → *(prod(l1), prod(l2))
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 5 SCCs with 6 less nodes.
(4) Complex Obligation (AND)
(5) Obligation:
Q DP problem:
The TRS P consists of the following rules:
APP(cons(x, l1), l2) → APP(l1, l2)
The TRS R consists of the following rules:
+(x, 0) → x
+(0, x) → x
+(s(x), s(y)) → s(s(+(x, y)))
+(+(x, y), z) → +(x, +(y, z))
*(x, 0) → 0
*(0, x) → 0
*(s(x), s(y)) → s(+(*(x, y), +(x, y)))
*(*(x, y), z) → *(x, *(y, z))
app(nil, l) → l
app(cons(x, l1), l2) → cons(x, app(l1, l2))
sum(nil) → 0
sum(cons(x, l)) → +(x, sum(l))
sum(app(l1, l2)) → +(sum(l1), sum(l2))
prod(nil) → s(0)
prod(cons(x, l)) → *(x, prod(l))
prod(app(l1, l2)) → *(prod(l1), prod(l2))
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:
+1(+(x, y), z) → +1(x, +(y, z))
+1(s(x), s(y)) → +1(x, y)
+1(+(x, y), z) → +1(y, z)
The TRS R consists of the following rules:
+(x, 0) → x
+(0, x) → x
+(s(x), s(y)) → s(s(+(x, y)))
+(+(x, y), z) → +(x, +(y, z))
*(x, 0) → 0
*(0, x) → 0
*(s(x), s(y)) → s(+(*(x, y), +(x, y)))
*(*(x, y), z) → *(x, *(y, z))
app(nil, l) → l
app(cons(x, l1), l2) → cons(x, app(l1, l2))
sum(nil) → 0
sum(cons(x, l)) → +(x, sum(l))
sum(app(l1, l2)) → +(sum(l1), sum(l2))
prod(nil) → s(0)
prod(cons(x, l)) → *(x, prod(l))
prod(app(l1, l2)) → *(prod(l1), prod(l2))
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:
SUM(app(l1, l2)) → SUM(l1)
SUM(cons(x, l)) → SUM(l)
SUM(app(l1, l2)) → SUM(l2)
The TRS R consists of the following rules:
+(x, 0) → x
+(0, x) → x
+(s(x), s(y)) → s(s(+(x, y)))
+(+(x, y), z) → +(x, +(y, z))
*(x, 0) → 0
*(0, x) → 0
*(s(x), s(y)) → s(+(*(x, y), +(x, y)))
*(*(x, y), z) → *(x, *(y, z))
app(nil, l) → l
app(cons(x, l1), l2) → cons(x, app(l1, l2))
sum(nil) → 0
sum(cons(x, l)) → +(x, sum(l))
sum(app(l1, l2)) → +(sum(l1), sum(l2))
prod(nil) → s(0)
prod(cons(x, l)) → *(x, prod(l))
prod(app(l1, l2)) → *(prod(l1), prod(l2))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(8) Obligation:
Q DP problem:
The TRS P consists of the following rules:
*1(*(x, y), z) → *1(x, *(y, z))
*1(s(x), s(y)) → *1(x, y)
*1(*(x, y), z) → *1(y, z)
The TRS R consists of the following rules:
+(x, 0) → x
+(0, x) → x
+(s(x), s(y)) → s(s(+(x, y)))
+(+(x, y), z) → +(x, +(y, z))
*(x, 0) → 0
*(0, x) → 0
*(s(x), s(y)) → s(+(*(x, y), +(x, y)))
*(*(x, y), z) → *(x, *(y, z))
app(nil, l) → l
app(cons(x, l1), l2) → cons(x, app(l1, l2))
sum(nil) → 0
sum(cons(x, l)) → +(x, sum(l))
sum(app(l1, l2)) → +(sum(l1), sum(l2))
prod(nil) → s(0)
prod(cons(x, l)) → *(x, prod(l))
prod(app(l1, l2)) → *(prod(l1), prod(l2))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(9) Obligation:
Q DP problem:
The TRS P consists of the following rules:
PROD(app(l1, l2)) → PROD(l1)
PROD(cons(x, l)) → PROD(l)
PROD(app(l1, l2)) → PROD(l2)
The TRS R consists of the following rules:
+(x, 0) → x
+(0, x) → x
+(s(x), s(y)) → s(s(+(x, y)))
+(+(x, y), z) → +(x, +(y, z))
*(x, 0) → 0
*(0, x) → 0
*(s(x), s(y)) → s(+(*(x, y), +(x, y)))
*(*(x, y), z) → *(x, *(y, z))
app(nil, l) → l
app(cons(x, l1), l2) → cons(x, app(l1, l2))
sum(nil) → 0
sum(cons(x, l)) → +(x, sum(l))
sum(app(l1, l2)) → +(sum(l1), sum(l2))
prod(nil) → s(0)
prod(cons(x, l)) → *(x, prod(l))
prod(app(l1, l2)) → *(prod(l1), prod(l2))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.