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