YES Time: 0.003703 TRS: { +(x, +(y, z)) -> +(+(x, y), z), +(*(x, y), +(x, z)) -> *(x, +(y, z)), +(*(x, y), +(*(x, z), u)) -> +(*(x, +(y, z)), u)} DP: DP: { +#(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)} TRS: { +(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, z)) -> +#(+(x, y), z), +#(*(x, y), +(*(x, z), u)) -> +#(*(x, +(y, z)), u)) (+#(x, +(y, z)) -> +#(+(x, y), z), +#(*(x, y), +(*(x, z), u)) -> +#(y, z)) (+#(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), +(*(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), +(*(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)) (+#(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)) -> +#(y, z)) (+#(x, +(y, z)) -> +#(x, y), +#(*(x, y), +(*(x, z), u)) -> +#(y, z)) (+#(x, +(y, z)) -> +#(x, y), +#(*(x, y), +(*(x, z), u)) -> +#(*(x, +(y, z)), u))} SCCS (1): 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 (5): 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), +(*(x, z), u)) -> +#(*(x, +(y, z)), u), +#(*(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), +(*(x, z), u)) -> +#(*(x, +(y, z)), u), +#(x, +(y, z)) -> +#(+(x, y), z)) (+#(*(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), +(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, 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)) -> +#(y, z)) (+#(x, +(y, z)) -> +#(x, y), +#(*(x, y), +(*(x, z), u)) -> +#(*(x, +(y, z)), u))} SCCS (1): 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 (4): 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), +(*(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)) (+#(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))} SCCS (1): Scc: { +#(x, +(y, z)) -> +#(x, y), +#(x, +(y, z)) -> +#(+(x, y), z), +#(*(x, y), +(*(x, z), u)) -> +#(*(x, +(y, z)), u)} SCC (3): 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), +(*(x, z), u)) -> +#(*(x, +(y, z)), u)} EDG: {(+#(*(x, y), +(*(x, z), u)) -> +#(*(x, +(y, z)), u), +#(*(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, z)) -> +#(x, y), +#(x, +(y, z)) -> +#(x, y)) (+#(x, +(y, z)) -> +#(x, y), +#(*(x, y), +(*(x, z), u)) -> +#(*(x, +(y, z)), u))} SCCS (1): Scc: { +#(x, +(y, z)) -> +#(x, y), +#(*(x, y), +(*(x, z), u)) -> +#(*(x, +(y, z)), u)} SCC (2): Strict: { +#(x, +(y, z)) -> +#(x, y), +#(*(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), +(*(x, z), u)) -> +#(*(x, +(y, z)), u)} EDG: {(+#(*(x, y), +(*(x, z), u)) -> +#(*(x, +(y, z)), u), +#(*(x, y), +(*(x, z), u)) -> +#(*(x, +(y, z)), u))} SCCS (1): Scc: {+#(*(x, y), +(*(x, z), u)) -> +#(*(x, +(y, z)), u)} SCC (1): Strict: {+#(*(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: {} Qed