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