YES Time: 0.003126 TRS: { +(x, 0()) -> x, +(x, i x) -> 0(), +(+(x, y), z) -> +(x, +(y, z)), *(x, +(y, z)) -> +(*(x, y), *(x, z)), *(+(x, y), z) -> +(*(x, z), *(y, z))} DP: DP: {+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z), *#(x, +(y, z)) -> +#(*(x, y), *(x, z)), *#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z), *#(+(x, y), z) -> +#(*(x, z), *(y, z)), *#(+(x, y), z) -> *#(x, z), *#(+(x, y), z) -> *#(y, z)} TRS: { +(x, 0()) -> x, +(x, i x) -> 0(), +(+(x, y), z) -> +(x, +(y, z)), *(x, +(y, z)) -> +(*(x, y), *(x, z)), *(+(x, y), z) -> +(*(x, z), *(y, z))} EDG: {(*#(x, +(y, z)) -> +#(*(x, y), *(x, z)), +#(+(x, y), z) -> +#(y, z)) (*#(x, +(y, z)) -> +#(*(x, y), *(x, z)), +#(+(x, y), z) -> +#(x, +(y, z))) (*#(x, +(y, z)) -> *#(x, y), *#(+(x, y), z) -> *#(y, z)) (*#(x, +(y, z)) -> *#(x, y), *#(+(x, y), z) -> *#(x, z)) (*#(x, +(y, z)) -> *#(x, y), *#(+(x, y), z) -> +#(*(x, z), *(y, z))) (*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z)) (*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, y)) (*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> +#(*(x, y), *(x, z))) (*#(x, +(y, z)) -> *#(x, z), *#(+(x, y), z) -> *#(y, z)) (*#(x, +(y, z)) -> *#(x, z), *#(+(x, y), z) -> *#(x, z)) (*#(x, +(y, z)) -> *#(x, z), *#(+(x, y), z) -> +#(*(x, z), *(y, z))) (*#(x, +(y, z)) -> *#(x, z), *#(x, +(y, z)) -> *#(x, z)) (*#(x, +(y, z)) -> *#(x, z), *#(x, +(y, z)) -> *#(x, y)) (*#(x, +(y, z)) -> *#(x, z), *#(x, +(y, z)) -> +#(*(x, y), *(x, z))) (*#(+(x, y), z) -> *#(y, z), *#(+(x, y), z) -> *#(y, z)) (*#(+(x, y), z) -> *#(y, z), *#(+(x, y), z) -> *#(x, z)) (*#(+(x, y), z) -> *#(y, z), *#(+(x, y), z) -> +#(*(x, z), *(y, z))) (*#(+(x, y), z) -> *#(y, z), *#(x, +(y, z)) -> *#(x, z)) (*#(+(x, y), z) -> *#(y, z), *#(x, +(y, z)) -> *#(x, y)) (*#(+(x, y), z) -> *#(y, z), *#(x, +(y, z)) -> +#(*(x, y), *(x, z))) (*#(+(x, y), z) -> *#(x, z), *#(x, +(y, z)) -> +#(*(x, y), *(x, z))) (*#(+(x, y), z) -> *#(x, z), *#(x, +(y, z)) -> *#(x, y)) (*#(+(x, y), z) -> *#(x, z), *#(x, +(y, z)) -> *#(x, z)) (*#(+(x, y), z) -> *#(x, z), *#(+(x, y), z) -> +#(*(x, z), *(y, z))) (*#(+(x, y), z) -> *#(x, z), *#(+(x, y), z) -> *#(x, z)) (*#(+(x, y), z) -> *#(x, z), *#(+(x, y), z) -> *#(y, z)) (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(x, +(y, z))) (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(y, z)) (*#(+(x, y), z) -> +#(*(x, z), *(y, z)), +#(+(x, y), z) -> +#(x, +(y, z))) (*#(+(x, y), z) -> +#(*(x, 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) -> +#(y, z))} SCCS (2): Scc: {*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z), *#(+(x, y), z) -> *#(x, z), *#(+(x, y), z) -> *#(y, z)} Scc: {+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z)} SCC (4): Strict: {*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z), *#(+(x, y), z) -> *#(x, z), *#(+(x, y), z) -> *#(y, z)} Weak: { +(x, 0()) -> x, +(x, i x) -> 0(), +(+(x, y), z) -> +(x, +(y, z)), *(x, +(y, z)) -> +(*(x, y), *(x, z)), *(+(x, y), z) -> +(*(x, z), *(y, z))} SPSC: Simple Projection: pi(*#) = 1 Strict: {*#(x, +(y, z)) -> *#(x, z), *#(+(x, y), z) -> *#(x, z), *#(+(x, y), z) -> *#(y, z)} EDG: {(*#(+(x, y), z) -> *#(x, z), *#(+(x, y), z) -> *#(y, z)) (*#(+(x, y), z) -> *#(x, z), *#(+(x, y), z) -> *#(x, z)) (*#(+(x, y), z) -> *#(x, z), *#(x, +(y, z)) -> *#(x, z)) (*#(+(x, y), z) -> *#(y, z), *#(x, +(y, z)) -> *#(x, z)) (*#(+(x, y), z) -> *#(y, z), *#(+(x, y), z) -> *#(x, z)) (*#(+(x, y), z) -> *#(y, z), *#(+(x, y), z) -> *#(y, z)) (*#(x, +(y, z)) -> *#(x, z), *#(x, +(y, z)) -> *#(x, z)) (*#(x, +(y, z)) -> *#(x, z), *#(+(x, y), z) -> *#(x, z)) (*#(x, +(y, z)) -> *#(x, z), *#(+(x, y), z) -> *#(y, z))} SCCS (1): Scc: {*#(x, +(y, z)) -> *#(x, z), *#(+(x, y), z) -> *#(x, z), *#(+(x, y), z) -> *#(y, z)} SCC (3): Strict: {*#(x, +(y, z)) -> *#(x, z), *#(+(x, y), z) -> *#(x, z), *#(+(x, y), z) -> *#(y, z)} Weak: { +(x, 0()) -> x, +(x, i x) -> 0(), +(+(x, y), z) -> +(x, +(y, z)), *(x, +(y, z)) -> +(*(x, y), *(x, z)), *(+(x, y), z) -> +(*(x, z), *(y, z))} SPSC: Simple Projection: pi(*#) = 1 Strict: {*#(+(x, y), z) -> *#(x, z), *#(+(x, y), z) -> *#(y, z)} EDG: {(*#(+(x, y), z) -> *#(y, z), *#(+(x, y), z) -> *#(y, z)) (*#(+(x, y), z) -> *#(y, z), *#(+(x, y), z) -> *#(x, z)) (*#(+(x, y), z) -> *#(x, z), *#(+(x, y), z) -> *#(x, z)) (*#(+(x, y), z) -> *#(x, z), *#(+(x, y), z) -> *#(y, z))} SCCS (1): Scc: {*#(+(x, y), z) -> *#(x, z), *#(+(x, y), z) -> *#(y, z)} SCC (2): Strict: {*#(+(x, y), z) -> *#(x, z), *#(+(x, y), z) -> *#(y, z)} Weak: { +(x, 0()) -> x, +(x, i x) -> 0(), +(+(x, y), z) -> +(x, +(y, z)), *(x, +(y, z)) -> +(*(x, y), *(x, z)), *(+(x, y), z) -> +(*(x, z), *(y, z))} SPSC: Simple Projection: pi(*#) = 0 Strict: {*#(+(x, y), z) -> *#(y, z)} EDG: {(*#(+(x, y), z) -> *#(y, z), *#(+(x, y), z) -> *#(y, z))} SCCS (1): Scc: {*#(+(x, y), z) -> *#(y, z)} SCC (1): Strict: {*#(+(x, y), z) -> *#(y, z)} Weak: { +(x, 0()) -> x, +(x, i x) -> 0(), +(+(x, y), z) -> +(x, +(y, z)), *(x, +(y, z)) -> +(*(x, y), *(x, z)), *(+(x, y), z) -> +(*(x, z), *(y, z))} SPSC: Simple Projection: pi(*#) = 0 Strict: {} Qed SCC (2): Strict: {+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z)} Weak: { +(x, 0()) -> x, +(x, i x) -> 0(), +(+(x, y), z) -> +(x, +(y, z)), *(x, +(y, z)) -> +(*(x, y), *(x, z)), *(+(x, y), z) -> +(*(x, z), *(y, z))} SPSC: Simple Projection: pi(+#) = 0 Strict: {+#(+(x, y), z) -> +#(y, z)} EDG: {(+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(y, z))} SCCS (1): Scc: {+#(+(x, y), z) -> +#(y, z)} SCC (1): Strict: {+#(+(x, y), z) -> +#(y, z)} Weak: { +(x, 0()) -> x, +(x, i x) -> 0(), +(+(x, y), z) -> +(x, +(y, z)), *(x, +(y, z)) -> +(*(x, y), *(x, z)), *(+(x, y), z) -> +(*(x, z), *(y, z))} SPSC: Simple Projection: pi(+#) = 0 Strict: {} Qed