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