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