MAYBE Time: 0.035959 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))} UR: { +(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)), a(w, v) -> w, a(w, v) -> v} 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))} 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))} 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))} 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))} STATUS: arrows: 0.500000 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))} Open 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))} Open