YES
TRS:
{ 0(#()) -> #(),
+(x, #()) -> x,
+(#(), x) -> x,
+(0(x), 0(y)) -> 0(+(x, y)),
+(0(x), 1(y)) -> 1(+(x, y)),
+(1(x), 0(y)) -> 1(+(x, y)),
+(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
*(#(), x) -> #(),
*(0(x), y) -> 0(*(x, y)),
*(1(x), y) -> +(0(*(x, y)), y),
sum(nil()) -> 0(#()),
sum(cons(x, l)) -> +(x, sum(l)),
prod(nil()) -> 1(#()),
prod(cons(x, l)) -> *(x, prod(l))}
DP:
Strict:
{ +#(0(x), 0(y)) -> 0#(+(x, y)),
+#(0(x), 0(y)) -> +#(x, y),
+#(0(x), 1(y)) -> +#(x, y),
+#(1(x), 0(y)) -> +#(x, y),
+#(1(x), 1(y)) -> 0#(+(+(x, y), 1(#()))),
+#(1(x), 1(y)) -> +#(x, y),
+#(1(x), 1(y)) -> +#(+(x, y), 1(#())),
*#(0(x), y) -> 0#(*(x, y)),
*#(0(x), y) -> *#(x, y),
*#(1(x), y) -> 0#(*(x, y)),
*#(1(x), y) -> +#(0(*(x, y)), y),
*#(1(x), y) -> *#(x, y),
sum#(nil()) -> 0#(#()),
sum#(cons(x, l)) -> +#(x, sum(l)),
sum#(cons(x, l)) -> sum#(l),
prod#(cons(x, l)) -> *#(x, prod(l)),
prod#(cons(x, l)) -> prod#(l)}
Weak:
{ 0(#()) -> #(),
+(x, #()) -> x,
+(#(), x) -> x,
+(0(x), 0(y)) -> 0(+(x, y)),
+(0(x), 1(y)) -> 1(+(x, y)),
+(1(x), 0(y)) -> 1(+(x, y)),
+(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
*(#(), x) -> #(),
*(0(x), y) -> 0(*(x, y)),
*(1(x), y) -> +(0(*(x, y)), y),
sum(nil()) -> 0(#()),
sum(cons(x, l)) -> +(x, sum(l)),
prod(nil()) -> 1(#()),
prod(cons(x, l)) -> *(x, prod(l))}
EDG:
{(sum#(cons(x, l)) -> +#(x, sum(l)), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))
(sum#(cons(x, l)) -> +#(x, sum(l)), +#(1(x), 1(y)) -> +#(x, y))
(sum#(cons(x, l)) -> +#(x, sum(l)), +#(1(x), 1(y)) -> 0#(+(+(x, y), 1(#()))))
(sum#(cons(x, l)) -> +#(x, sum(l)), +#(1(x), 0(y)) -> +#(x, y))
(sum#(cons(x, l)) -> +#(x, sum(l)), +#(0(x), 1(y)) -> +#(x, y))
(sum#(cons(x, l)) -> +#(x, sum(l)), +#(0(x), 0(y)) -> +#(x, y))
(sum#(cons(x, l)) -> +#(x, sum(l)), +#(0(x), 0(y)) -> 0#(+(x, y)))
(+#(0(x), 0(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))
(+#(0(x), 0(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(x, y))
(+#(0(x), 0(y)) -> +#(x, y), +#(1(x), 1(y)) -> 0#(+(+(x, y), 1(#()))))
(+#(0(x), 0(y)) -> +#(x, y), +#(1(x), 0(y)) -> +#(x, y))
(+#(0(x), 0(y)) -> +#(x, y), +#(0(x), 1(y)) -> +#(x, y))
(+#(0(x), 0(y)) -> +#(x, y), +#(0(x), 0(y)) -> +#(x, y))
(+#(0(x), 0(y)) -> +#(x, y), +#(0(x), 0(y)) -> 0#(+(x, y)))
(+#(1(x), 0(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))
(+#(1(x), 0(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(x, y))
(+#(1(x), 0(y)) -> +#(x, y), +#(1(x), 1(y)) -> 0#(+(+(x, y), 1(#()))))
(+#(1(x), 0(y)) -> +#(x, y), +#(1(x), 0(y)) -> +#(x, y))
(+#(1(x), 0(y)) -> +#(x, y), +#(0(x), 1(y)) -> +#(x, y))
(+#(1(x), 0(y)) -> +#(x, y), +#(0(x), 0(y)) -> +#(x, y))
(+#(1(x), 0(y)) -> +#(x, y), +#(0(x), 0(y)) -> 0#(+(x, y)))
(*#(0(x), y) -> *#(x, y), *#(1(x), y) -> *#(x, y))
(*#(0(x), y) -> *#(x, y), *#(1(x), y) -> +#(0(*(x, y)), y))
(*#(0(x), y) -> *#(x, y), *#(1(x), y) -> 0#(*(x, y)))
(*#(0(x), y) -> *#(x, y), *#(0(x), y) -> *#(x, y))
(*#(0(x), y) -> *#(x, y), *#(0(x), y) -> 0#(*(x, y)))
(sum#(cons(x, l)) -> sum#(l), sum#(cons(x, l)) -> sum#(l))
(sum#(cons(x, l)) -> sum#(l), sum#(cons(x, l)) -> +#(x, sum(l)))
(sum#(cons(x, l)) -> sum#(l), sum#(nil()) -> 0#(#()))
(+#(1(x), 1(y)) -> +#(+(x, y), 1(#())), +#(0(x), 1(y)) -> +#(x, y))
(+#(1(x), 1(y)) -> +#(+(x, y), 1(#())), +#(1(x), 1(y)) -> 0#(+(+(x, y), 1(#()))))
(+#(1(x), 1(y)) -> +#(+(x, y), 1(#())), +#(1(x), 1(y)) -> +#(x, y))
(+#(1(x), 1(y)) -> +#(+(x, y), 1(#())), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))
(prod#(cons(x, l)) -> prod#(l), prod#(cons(x, l)) -> *#(x, prod(l)))
(prod#(cons(x, l)) -> prod#(l), prod#(cons(x, l)) -> prod#(l))
(*#(1(x), y) -> *#(x, y), *#(0(x), y) -> 0#(*(x, y)))
(*#(1(x), y) -> *#(x, y), *#(0(x), y) -> *#(x, y))
(*#(1(x), y) -> *#(x, y), *#(1(x), y) -> 0#(*(x, y)))
(*#(1(x), y) -> *#(x, y), *#(1(x), y) -> +#(0(*(x, y)), y))
(*#(1(x), y) -> *#(x, y), *#(1(x), y) -> *#(x, y))
(+#(1(x), 1(y)) -> +#(x, y), +#(0(x), 0(y)) -> 0#(+(x, y)))
(+#(1(x), 1(y)) -> +#(x, y), +#(0(x), 0(y)) -> +#(x, y))
(+#(1(x), 1(y)) -> +#(x, y), +#(0(x), 1(y)) -> +#(x, y))
(+#(1(x), 1(y)) -> +#(x, y), +#(1(x), 0(y)) -> +#(x, y))
(+#(1(x), 1(y)) -> +#(x, y), +#(1(x), 1(y)) -> 0#(+(+(x, y), 1(#()))))
(+#(1(x), 1(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(x, y))
(+#(1(x), 1(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))
(+#(0(x), 1(y)) -> +#(x, y), +#(0(x), 0(y)) -> 0#(+(x, y)))
(+#(0(x), 1(y)) -> +#(x, y), +#(0(x), 0(y)) -> +#(x, y))
(+#(0(x), 1(y)) -> +#(x, y), +#(0(x), 1(y)) -> +#(x, y))
(+#(0(x), 1(y)) -> +#(x, y), +#(1(x), 0(y)) -> +#(x, y))
(+#(0(x), 1(y)) -> +#(x, y), +#(1(x), 1(y)) -> 0#(+(+(x, y), 1(#()))))
(+#(0(x), 1(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(x, y))
(+#(0(x), 1(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))
(prod#(cons(x, l)) -> *#(x, prod(l)), *#(0(x), y) -> 0#(*(x, y)))
(prod#(cons(x, l)) -> *#(x, prod(l)), *#(0(x), y) -> *#(x, y))
(prod#(cons(x, l)) -> *#(x, prod(l)), *#(1(x), y) -> 0#(*(x, y)))
(prod#(cons(x, l)) -> *#(x, prod(l)), *#(1(x), y) -> +#(0(*(x, y)), y))
(prod#(cons(x, l)) -> *#(x, prod(l)), *#(1(x), y) -> *#(x, y))
(*#(1(x), y) -> +#(0(*(x, y)), y), +#(0(x), 0(y)) -> 0#(+(x, y)))
(*#(1(x), y) -> +#(0(*(x, y)), y), +#(0(x), 0(y)) -> +#(x, y))
(*#(1(x), y) -> +#(0(*(x, y)), y), +#(0(x), 1(y)) -> +#(x, y))
(*#(1(x), y) -> +#(0(*(x, y)), y), +#(1(x), 0(y)) -> +#(x, y))
(*#(1(x), y) -> +#(0(*(x, y)), y), +#(1(x), 1(y)) -> 0#(+(+(x, y), 1(#()))))
(*#(1(x), y) -> +#(0(*(x, y)), y), +#(1(x), 1(y)) -> +#(x, y))
(*#(1(x), y) -> +#(0(*(x, y)), y), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))}
SCCS:
Scc:
{prod#(cons(x, l)) -> prod#(l)}
Scc:
{sum#(cons(x, l)) -> sum#(l)}
Scc:
{*#(0(x), y) -> *#(x, y),
*#(1(x), y) -> *#(x, y)}
Scc:
{+#(0(x), 0(y)) -> +#(x, y),
+#(0(x), 1(y)) -> +#(x, y),
+#(1(x), 0(y)) -> +#(x, y),
+#(1(x), 1(y)) -> +#(x, y),
+#(1(x), 1(y)) -> +#(+(x, y), 1(#()))}
SCC:
Strict:
{prod#(cons(x, l)) -> prod#(l)}
Weak:
{ 0(#()) -> #(),
+(x, #()) -> x,
+(#(), x) -> x,
+(0(x), 0(y)) -> 0(+(x, y)),
+(0(x), 1(y)) -> 1(+(x, y)),
+(1(x), 0(y)) -> 1(+(x, y)),
+(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
*(#(), x) -> #(),
*(0(x), y) -> 0(*(x, y)),
*(1(x), y) -> +(0(*(x, y)), y),
sum(nil()) -> 0(#()),
sum(cons(x, l)) -> +(x, sum(l)),
prod(nil()) -> 1(#()),
prod(cons(x, l)) -> *(x, prod(l))}
SPSC:
Simple Projection:
pi(prod#) = 0
Strict:
{}
Qed
SCC:
Strict:
{sum#(cons(x, l)) -> sum#(l)}
Weak:
{ 0(#()) -> #(),
+(x, #()) -> x,
+(#(), x) -> x,
+(0(x), 0(y)) -> 0(+(x, y)),
+(0(x), 1(y)) -> 1(+(x, y)),
+(1(x), 0(y)) -> 1(+(x, y)),
+(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
*(#(), x) -> #(),
*(0(x), y) -> 0(*(x, y)),
*(1(x), y) -> +(0(*(x, y)), y),
sum(nil()) -> 0(#()),
sum(cons(x, l)) -> +(x, sum(l)),
prod(nil()) -> 1(#()),
prod(cons(x, l)) -> *(x, prod(l))}
SPSC:
Simple Projection:
pi(sum#) = 0
Strict:
{}
Qed
SCC:
Strict:
{*#(0(x), y) -> *#(x, y),
*#(1(x), y) -> *#(x, y)}
Weak:
{ 0(#()) -> #(),
+(x, #()) -> x,
+(#(), x) -> x,
+(0(x), 0(y)) -> 0(+(x, y)),
+(0(x), 1(y)) -> 1(+(x, y)),
+(1(x), 0(y)) -> 1(+(x, y)),
+(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
*(#(), x) -> #(),
*(0(x), y) -> 0(*(x, y)),
*(1(x), y) -> +(0(*(x, y)), y),
sum(nil()) -> 0(#()),
sum(cons(x, l)) -> +(x, sum(l)),
prod(nil()) -> 1(#()),
prod(cons(x, l)) -> *(x, prod(l))}
SPSC:
Simple Projection:
pi(*#) = 0
Strict:
{*#(0(x), y) -> *#(x, y)}
EDG:
{(*#(0(x), y) -> *#(x, y), *#(0(x), y) -> *#(x, y))}
SCCS:
Scc:
{*#(0(x), y) -> *#(x, y)}
SCC:
Strict:
{*#(0(x), y) -> *#(x, y)}
Weak:
{ 0(#()) -> #(),
+(x, #()) -> x,
+(#(), x) -> x,
+(0(x), 0(y)) -> 0(+(x, y)),
+(0(x), 1(y)) -> 1(+(x, y)),
+(1(x), 0(y)) -> 1(+(x, y)),
+(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
*(#(), x) -> #(),
*(0(x), y) -> 0(*(x, y)),
*(1(x), y) -> +(0(*(x, y)), y),
sum(nil()) -> 0(#()),
sum(cons(x, l)) -> +(x, sum(l)),
prod(nil()) -> 1(#()),
prod(cons(x, l)) -> *(x, prod(l))}
SPSC:
Simple Projection:
pi(*#) = 0
Strict:
{}
Qed
SCC:
Strict:
{+#(0(x), 0(y)) -> +#(x, y),
+#(0(x), 1(y)) -> +#(x, y),
+#(1(x), 0(y)) -> +#(x, y),
+#(1(x), 1(y)) -> +#(x, y),
+#(1(x), 1(y)) -> +#(+(x, y), 1(#()))}
Weak:
{ 0(#()) -> #(),
+(x, #()) -> x,
+(#(), x) -> x,
+(0(x), 0(y)) -> 0(+(x, y)),
+(0(x), 1(y)) -> 1(+(x, y)),
+(1(x), 0(y)) -> 1(+(x, y)),
+(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
*(#(), x) -> #(),
*(0(x), y) -> 0(*(x, y)),
*(1(x), y) -> +(0(*(x, y)), y),
sum(nil()) -> 0(#()),
sum(cons(x, l)) -> +(x, sum(l)),
prod(nil()) -> 1(#()),
prod(cons(x, l)) -> *(x, prod(l))}
POLY:
Argument Filtering:
pi(prod) = [], pi(cons) = [], pi(nil) = [], pi(sum) = [], pi(*) = [], pi(1) = [0], pi(+#) = [1], pi(+) = [], pi(0) = 0, pi(#) = []
Usable Rules:
{}
Interpretation:
[+#](x0) = x0 + 1,
[1](x0) = x0 + 1,
[#] = 0
Strict:
{+#(0(x), 0(y)) -> +#(x, y),
+#(1(x), 0(y)) -> +#(x, y),
+#(1(x), 1(y)) -> +#(+(x, y), 1(#()))}
Weak:
{ 0(#()) -> #(),
+(x, #()) -> x,
+(#(), x) -> x,
+(0(x), 0(y)) -> 0(+(x, y)),
+(0(x), 1(y)) -> 1(+(x, y)),
+(1(x), 0(y)) -> 1(+(x, y)),
+(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
*(#(), x) -> #(),
*(0(x), y) -> 0(*(x, y)),
*(1(x), y) -> +(0(*(x, y)), y),
sum(nil()) -> 0(#()),
sum(cons(x, l)) -> +(x, sum(l)),
prod(nil()) -> 1(#()),
prod(cons(x, l)) -> *(x, prod(l))}
EDG:
{(+#(1(x), 0(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))
(+#(1(x), 0(y)) -> +#(x, y), +#(1(x), 0(y)) -> +#(x, y))
(+#(1(x), 0(y)) -> +#(x, y), +#(0(x), 0(y)) -> +#(x, y))
(+#(1(x), 1(y)) -> +#(+(x, y), 1(#())), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))
(+#(0(x), 0(y)) -> +#(x, y), +#(0(x), 0(y)) -> +#(x, y))
(+#(0(x), 0(y)) -> +#(x, y), +#(1(x), 0(y)) -> +#(x, y))
(+#(0(x), 0(y)) -> +#(x, y), +#(1(x), 1(y)) -> +#(+(x, y), 1(#())))}
SCCS:
Scc:
{+#(1(x), 1(y)) -> +#(+(x, y), 1(#()))}
Scc:
{+#(0(x), 0(y)) -> +#(x, y),
+#(1(x), 0(y)) -> +#(x, y)}
SCC:
Strict:
{+#(1(x), 1(y)) -> +#(+(x, y), 1(#()))}
Weak:
{ 0(#()) -> #(),
+(x, #()) -> x,
+(#(), x) -> x,
+(0(x), 0(y)) -> 0(+(x, y)),
+(0(x), 1(y)) -> 1(+(x, y)),
+(1(x), 0(y)) -> 1(+(x, y)),
+(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
*(#(), x) -> #(),
*(0(x), y) -> 0(*(x, y)),
*(1(x), y) -> +(0(*(x, y)), y),
sum(nil()) -> 0(#()),
sum(cons(x, l)) -> +(x, sum(l)),
prod(nil()) -> 1(#()),
prod(cons(x, l)) -> *(x, prod(l))}
POLY:
Argument Filtering:
pi(prod) = [], pi(cons) = [], pi(nil) = [], pi(sum) = [], pi(*) = [], pi(1) = [0], pi(+#) = [0,1], pi(+) = [0,1], pi(0) = 0, pi(#) = []
Usable Rules:
{}
Interpretation:
[+#](x0, x1) = x0 + x1 + 1,
[+](x0, x1) = x0 + x1,
[1](x0) = x0 + 1,
[#] = 0
Strict:
{}
Weak:
{ 0(#()) -> #(),
+(x, #()) -> x,
+(#(), x) -> x,
+(0(x), 0(y)) -> 0(+(x, y)),
+(0(x), 1(y)) -> 1(+(x, y)),
+(1(x), 0(y)) -> 1(+(x, y)),
+(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
*(#(), x) -> #(),
*(0(x), y) -> 0(*(x, y)),
*(1(x), y) -> +(0(*(x, y)), y),
sum(nil()) -> 0(#()),
sum(cons(x, l)) -> +(x, sum(l)),
prod(nil()) -> 1(#()),
prod(cons(x, l)) -> *(x, prod(l))}
Qed
SCC:
Strict:
{+#(0(x), 0(y)) -> +#(x, y),
+#(1(x), 0(y)) -> +#(x, y)}
Weak:
{ 0(#()) -> #(),
+(x, #()) -> x,
+(#(), x) -> x,
+(0(x), 0(y)) -> 0(+(x, y)),
+(0(x), 1(y)) -> 1(+(x, y)),
+(1(x), 0(y)) -> 1(+(x, y)),
+(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
*(#(), x) -> #(),
*(0(x), y) -> 0(*(x, y)),
*(1(x), y) -> +(0(*(x, y)), y),
sum(nil()) -> 0(#()),
sum(cons(x, l)) -> +(x, sum(l)),
prod(nil()) -> 1(#()),
prod(cons(x, l)) -> *(x, prod(l))}
SPSC:
Simple Projection:
pi(+#) = 0
Strict:
{+#(0(x), 0(y)) -> +#(x, y)}
EDG:
{(+#(0(x), 0(y)) -> +#(x, y), +#(0(x), 0(y)) -> +#(x, y))}
SCCS:
Scc:
{+#(0(x), 0(y)) -> +#(x, y)}
SCC:
Strict:
{+#(0(x), 0(y)) -> +#(x, y)}
Weak:
{ 0(#()) -> #(),
+(x, #()) -> x,
+(#(), x) -> x,
+(0(x), 0(y)) -> 0(+(x, y)),
+(0(x), 1(y)) -> 1(+(x, y)),
+(1(x), 0(y)) -> 1(+(x, y)),
+(1(x), 1(y)) -> 0(+(+(x, y), 1(#()))),
*(#(), x) -> #(),
*(0(x), y) -> 0(*(x, y)),
*(1(x), y) -> +(0(*(x, y)), y),
sum(nil()) -> 0(#()),
sum(cons(x, l)) -> +(x, sum(l)),
prod(nil()) -> 1(#()),
prod(cons(x, l)) -> *(x, prod(l))}
SPSC:
Simple Projection:
pi(+#) = 0
Strict:
{}
Qed