YES TRS: { 0(#()) -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0(x), 0(y)) -> 0(+(x, y)), +(0(x), 1(y)) -> 1(+(x, y)), +(+(x, y), z) -> +(x, +(y, z)), +(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), *(*(x, y), z) -> *(x, *(y, z)), 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), +#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z), +#(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), *#(*(x, y), z) -> *#(x, *(y, z)), *#(*(x, y), z) -> *#(y, z), 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)), +(+(x, y), z) -> +(x, +(y, z)), +(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), *(*(x, y), z) -> *(x, *(y, z)), sum(nil()) -> 0(#()), sum(cons(x, l)) -> +(x, sum(l)), prod(nil()) -> 1(#()), prod(cons(x, l)) -> *(x, prod(l))} EDG: {(+#(+(x, y), z) -> +#(x, +(y, z)), +#(1(x), 1(y)) -> +#(+(x, y), 1(#()))) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(1(x), 1(y)) -> +#(x, y)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(1(x), 1(y)) -> 0#(+(+(x, y), 1(#())))) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(1(x), 0(y)) -> +#(x, y)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(0(x), 1(y)) -> +#(x, y)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(0(x), 0(y)) -> +#(x, y)) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(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), +#(+(x, y), z) -> +#(y, z)) (+#(0(x), 0(y)) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(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), +#(+(x, y), z) -> +#(y, z)) (+#(1(x), 0(y)) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(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), *#(*(x, y), z) -> *#(y, z)) (*#(0(x), y) -> *#(x, y), *#(*(x, y), z) -> *#(x, *(y, z))) (*#(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)) -> +#(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)), +#(+(x, y), z) -> +#(y, z)) (sum#(cons(x, l)) -> +#(x, sum(l)), +#(+(x, y), z) -> +#(x, +(y, z))) (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))) (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#(#())) (+#(+(x, y), z) -> +#(y, z), +#(1(x), 1(y)) -> +#(+(x, y), 1(#()))) (+#(+(x, y), z) -> +#(y, z), +#(1(x), 1(y)) -> +#(x, y)) (+#(+(x, y), z) -> +#(y, z), +#(1(x), 1(y)) -> 0#(+(+(x, y), 1(#())))) (+#(+(x, y), z) -> +#(y, z), +#(1(x), 0(y)) -> +#(x, y)) (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(y, z)) (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(+(x, y), z) -> +#(y, z), +#(0(x), 1(y)) -> +#(x, y)) (+#(+(x, y), z) -> +#(y, z), +#(0(x), 0(y)) -> +#(x, y)) (+#(+(x, y), z) -> +#(y, z), +#(0(x), 0(y)) -> 0#(+(x, y))) (*#(1(x), y) -> +#(0(*(x, y)), y), +#(1(x), 1(y)) -> +#(+(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)) -> 0#(+(+(x, y), 1(#())))) (*#(1(x), y) -> +#(0(*(x, y)), y), +#(1(x), 0(y)) -> +#(x, y)) (*#(1(x), y) -> +#(0(*(x, y)), y), +#(+(x, y), z) -> +#(y, z)) (*#(1(x), y) -> +#(0(*(x, y)), y), +#(+(x, y), z) -> +#(x, +(y, z))) (*#(1(x), y) -> +#(0(*(x, y)), y), +#(0(x), 1(y)) -> +#(x, y)) (*#(1(x), y) -> +#(0(*(x, y)), y), +#(0(x), 0(y)) -> +#(x, y)) (*#(1(x), y) -> +#(0(*(x, y)), y), +#(0(x), 0(y)) -> 0#(+(x, y))) (+#(1(x), 1(y)) -> +#(+(x, y), 1(#())), +#(0(x), 1(y)) -> +#(x, y)) (+#(1(x), 1(y)) -> +#(+(x, y), 1(#())), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(1(x), 1(y)) -> +#(+(x, y), 1(#())), +#(+(x, y), z) -> +#(y, z)) (+#(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(#()))) (*#(*(x, y), z) -> *#(y, z), *#(0(x), y) -> 0#(*(x, y))) (*#(*(x, y), z) -> *#(y, z), *#(0(x), y) -> *#(x, y)) (*#(*(x, y), z) -> *#(y, z), *#(1(x), y) -> 0#(*(x, y))) (*#(*(x, y), z) -> *#(y, z), *#(1(x), y) -> +#(0(*(x, y)), y)) (*#(*(x, y), z) -> *#(y, z), *#(1(x), y) -> *#(x, y)) (*#(*(x, y), z) -> *#(y, z), *#(*(x, y), z) -> *#(x, *(y, z))) (*#(*(x, y), z) -> *#(y, z), *#(*(x, y), z) -> *#(y, z)) (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)) (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)) (prod#(cons(x, l)) -> *#(x, prod(l)), *#(*(x, y), z) -> *#(x, *(y, z))) (prod#(cons(x, l)) -> *#(x, prod(l)), *#(*(x, y), z) -> *#(y, z)) (*#(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), y) -> *#(x, y), *#(*(x, y), z) -> *#(x, *(y, z))) (*#(1(x), y) -> *#(x, y), *#(*(x, y), z) -> *#(y, z)) (+#(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), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(1(x), 1(y)) -> +#(x, y), +#(+(x, y), z) -> +#(y, z)) (+#(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), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(0(x), 1(y)) -> +#(x, y), +#(+(x, y), z) -> +#(y, z)) (+#(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(#()))) (*#(*(x, y), z) -> *#(x, *(y, z)), *#(0(x), y) -> 0#(*(x, y))) (*#(*(x, y), z) -> *#(x, *(y, z)), *#(0(x), y) -> *#(x, y)) (*#(*(x, y), z) -> *#(x, *(y, z)), *#(1(x), y) -> 0#(*(x, y))) (*#(*(x, y), z) -> *#(x, *(y, z)), *#(1(x), y) -> +#(0(*(x, y)), y)) (*#(*(x, y), z) -> *#(x, *(y, z)), *#(1(x), y) -> *#(x, y)) (*#(*(x, y), z) -> *#(x, *(y, z)), *#(*(x, y), z) -> *#(x, *(y, z))) (*#(*(x, y), z) -> *#(x, *(y, z)), *#(*(x, y), z) -> *#(y, z))} 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), *#(*(x, y), z) -> *#(x, *(y, z)), *#(*(x, y), z) -> *#(y, z)} Scc: {+#(0(x), 0(y)) -> +#(x, y), +#(0(x), 1(y)) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z), +#(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)), +(+(x, y), z) -> +(x, +(y, z)), +(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), *(*(x, y), z) -> *(x, *(y, z)), 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)), +(+(x, y), z) -> +(x, +(y, z)), +(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), *(*(x, y), z) -> *(x, *(y, z)), 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), *#(*(x, y), z) -> *#(x, *(y, z)), *#(*(x, y), z) -> *#(y, z)} Weak: { 0(#()) -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0(x), 0(y)) -> 0(+(x, y)), +(0(x), 1(y)) -> 1(+(x, y)), +(+(x, y), z) -> +(x, +(y, z)), +(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), *(*(x, y), z) -> *(x, *(y, z)), 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), *#(1(x), y) -> *#(x, y), *#(*(x, y), z) -> *#(y, z)} EDG: {(*#(0(x), y) -> *#(x, y), *#(*(x, y), z) -> *#(y, z)) (*#(0(x), y) -> *#(x, y), *#(1(x), y) -> *#(x, y)) (*#(0(x), y) -> *#(x, y), *#(0(x), y) -> *#(x, y)) (*#(1(x), y) -> *#(x, y), *#(0(x), y) -> *#(x, y)) (*#(1(x), y) -> *#(x, y), *#(1(x), y) -> *#(x, y)) (*#(1(x), y) -> *#(x, y), *#(*(x, y), z) -> *#(y, z)) (*#(*(x, y), z) -> *#(y, z), *#(0(x), y) -> *#(x, y)) (*#(*(x, y), z) -> *#(y, z), *#(1(x), y) -> *#(x, y)) (*#(*(x, y), z) -> *#(y, z), *#(*(x, y), z) -> *#(y, z))} SCCS: Scc: { *#(0(x), y) -> *#(x, y), *#(1(x), y) -> *#(x, y), *#(*(x, y), z) -> *#(y, z)} SCC: Strict: { *#(0(x), y) -> *#(x, y), *#(1(x), y) -> *#(x, y), *#(*(x, y), z) -> *#(y, z)} Weak: { 0(#()) -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0(x), 0(y)) -> 0(+(x, y)), +(0(x), 1(y)) -> 1(+(x, y)), +(+(x, y), z) -> +(x, +(y, z)), +(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), *(*(x, y), z) -> *(x, *(y, z)), 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), *#(1(x), y) -> *#(x, y)} EDG: {(*#(1(x), y) -> *#(x, y), *#(1(x), y) -> *#(x, y)) (*#(1(x), y) -> *#(x, y), *#(0(x), y) -> *#(x, y)) (*#(0(x), y) -> *#(x, y), *#(0(x), y) -> *#(x, y)) (*#(0(x), y) -> *#(x, y), *#(1(x), y) -> *#(x, y))} SCCS: Scc: {*#(0(x), y) -> *#(x, y), *#(1(x), y) -> *#(x, y)} 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)), +(+(x, y), z) -> +(x, +(y, z)), +(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), *(*(x, y), z) -> *(x, *(y, z)), 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)), +(+(x, y), z) -> +(x, +(y, z)), +(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), *(*(x, y), z) -> *(x, *(y, z)), 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), +#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z), +#(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)), +(+(x, y), z) -> +(x, +(y, z)), +(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), *(*(x, y), z) -> *(x, *(y, z)), 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](x0) = x0 + 1, [#] = 0 Strict: {+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z)} Weak: { 0(#()) -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0(x), 0(y)) -> 0(+(x, y)), +(0(x), 1(y)) -> 1(+(x, y)), +(+(x, y), z) -> +(x, +(y, z)), +(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), *(*(x, y), z) -> *(x, *(y, z)), sum(nil()) -> 0(#()), sum(cons(x, l)) -> +(x, sum(l)), prod(nil()) -> 1(#()), prod(cons(x, l)) -> *(x, prod(l))} EDG: {(+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(y, z)) (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z))} SCCS: Scc: {+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z)} SCC: Strict: {+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z)} Weak: { 0(#()) -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0(x), 0(y)) -> 0(+(x, y)), +(0(x), 1(y)) -> 1(+(x, y)), +(+(x, y), z) -> +(x, +(y, z)), +(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), *(*(x, y), z) -> *(x, *(y, z)), 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: {+#(+(x, y), z) -> +#(y, z)} EDG: {(+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(y, z))} SCCS: Scc: {+#(+(x, y), z) -> +#(y, z)} SCC: Strict: {+#(+(x, y), z) -> +#(y, z)} Weak: { 0(#()) -> #(), +(x, #()) -> x, +(#(), x) -> x, +(0(x), 0(y)) -> 0(+(x, y)), +(0(x), 1(y)) -> 1(+(x, y)), +(+(x, y), z) -> +(x, +(y, z)), +(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), *(*(x, y), z) -> *(x, *(y, z)), 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