MAYBE TRS: { ifPlus(true(), x, y) -> p(y), ifPlus(false(), x, y) -> plus(p(x), y), isZero(0()) -> true(), isZero(s(0())) -> false(), isZero(s(s(x))) -> isZero(s(x)), inc(x) -> s(x), inc(0()) -> s(0()), inc(s(x)) -> s(inc(x)), plus(x, y) -> ifPlus(isZero(x), x, inc(y)), p(0()) -> 0(), p(s(x)) -> x, p(s(s(x))) -> s(p(s(x))), timesIter(i, x, y, z) -> ifTimes(ge(i, x), i, x, y, z), times(x, y) -> timesIter(0(), x, y, 0()), ifTimes(true(), i, x, y, z) -> z, ifTimes(false(), i, x, y, z) -> timesIter(inc(i), x, y, plus(z, y)), ge(x, 0()) -> true(), ge(0(), s(y)) -> false(), ge(s(x), s(y)) -> ge(x, y), f1(x, y, z) -> f2(x, y, z), f1(x, y, z) -> c(), f0(x, y, z) -> d(), f0(0(), y, x) -> f1(x, y, x), f2(x, 1(), z) -> f0(x, z, z)} DP: Strict: { ifPlus#(true(), x, y) -> p#(y), ifPlus#(false(), x, y) -> plus#(p(x), y), ifPlus#(false(), x, y) -> p#(x), isZero#(s(s(x))) -> isZero#(s(x)), inc#(s(x)) -> inc#(x), plus#(x, y) -> ifPlus#(isZero(x), x, inc(y)), plus#(x, y) -> isZero#(x), plus#(x, y) -> inc#(y), p#(s(s(x))) -> p#(s(x)), timesIter#(i, x, y, z) -> ifTimes#(ge(i, x), i, x, y, z), timesIter#(i, x, y, z) -> ge#(i, x), times#(x, y) -> timesIter#(0(), x, y, 0()), ifTimes#(false(), i, x, y, z) -> inc#(i), ifTimes#(false(), i, x, y, z) -> plus#(z, y), ifTimes#(false(), i, x, y, z) -> timesIter#(inc(i), x, y, plus(z, y)), ge#(s(x), s(y)) -> ge#(x, y), f1#(x, y, z) -> f2#(x, y, z), f0#(0(), y, x) -> f1#(x, y, x), f2#(x, 1(), z) -> f0#(x, z, z)} Weak: { ifPlus(true(), x, y) -> p(y), ifPlus(false(), x, y) -> plus(p(x), y), isZero(0()) -> true(), isZero(s(0())) -> false(), isZero(s(s(x))) -> isZero(s(x)), inc(x) -> s(x), inc(0()) -> s(0()), inc(s(x)) -> s(inc(x)), plus(x, y) -> ifPlus(isZero(x), x, inc(y)), p(0()) -> 0(), p(s(x)) -> x, p(s(s(x))) -> s(p(s(x))), timesIter(i, x, y, z) -> ifTimes(ge(i, x), i, x, y, z), times(x, y) -> timesIter(0(), x, y, 0()), ifTimes(true(), i, x, y, z) -> z, ifTimes(false(), i, x, y, z) -> timesIter(inc(i), x, y, plus(z, y)), ge(x, 0()) -> true(), ge(0(), s(y)) -> false(), ge(s(x), s(y)) -> ge(x, y), f1(x, y, z) -> f2(x, y, z), f1(x, y, z) -> c(), f0(x, y, z) -> d(), f0(0(), y, x) -> f1(x, y, x), f2(x, 1(), z) -> f0(x, z, z)} EDG: {(times#(x, y) -> timesIter#(0(), x, y, 0()), timesIter#(i, x, y, z) -> ge#(i, x)) (times#(x, y) -> timesIter#(0(), x, y, 0()), timesIter#(i, x, y, z) -> ifTimes#(ge(i, x), i, x, y, z)) (ge#(s(x), s(y)) -> ge#(x, y), ge#(s(x), s(y)) -> ge#(x, y)) (f2#(x, 1(), z) -> f0#(x, z, z), f0#(0(), y, x) -> f1#(x, y, x)) (plus#(x, y) -> inc#(y), inc#(s(x)) -> inc#(x)) (isZero#(s(s(x))) -> isZero#(s(x)), isZero#(s(s(x))) -> isZero#(s(x))) (ifPlus#(false(), x, y) -> plus#(p(x), y), plus#(x, y) -> inc#(y)) (ifPlus#(false(), x, y) -> plus#(p(x), y), plus#(x, y) -> isZero#(x)) (ifPlus#(false(), x, y) -> plus#(p(x), y), plus#(x, y) -> ifPlus#(isZero(x), x, inc(y))) (f0#(0(), y, x) -> f1#(x, y, x), f1#(x, y, z) -> f2#(x, y, z)) (inc#(s(x)) -> inc#(x), inc#(s(x)) -> inc#(x)) (timesIter#(i, x, y, z) -> ifTimes#(ge(i, x), i, x, y, z), ifTimes#(false(), i, x, y, z) -> timesIter#(inc(i), x, y, plus(z, y))) (timesIter#(i, x, y, z) -> ifTimes#(ge(i, x), i, x, y, z), ifTimes#(false(), i, x, y, z) -> plus#(z, y)) (timesIter#(i, x, y, z) -> ifTimes#(ge(i, x), i, x, y, z), ifTimes#(false(), i, x, y, z) -> inc#(i)) (ifTimes#(false(), i, x, y, z) -> inc#(i), inc#(s(x)) -> inc#(x)) (plus#(x, y) -> isZero#(x), isZero#(s(s(x))) -> isZero#(s(x))) (ifPlus#(false(), x, y) -> p#(x), p#(s(s(x))) -> p#(s(x))) (timesIter#(i, x, y, z) -> ge#(i, x), ge#(s(x), s(y)) -> ge#(x, y)) (p#(s(s(x))) -> p#(s(x)), p#(s(s(x))) -> p#(s(x))) (ifTimes#(false(), i, x, y, z) -> timesIter#(inc(i), x, y, plus(z, y)), timesIter#(i, x, y, z) -> ifTimes#(ge(i, x), i, x, y, z)) (ifTimes#(false(), i, x, y, z) -> timesIter#(inc(i), x, y, plus(z, y)), timesIter#(i, x, y, z) -> ge#(i, x)) (ifPlus#(true(), x, y) -> p#(y), p#(s(s(x))) -> p#(s(x))) (f1#(x, y, z) -> f2#(x, y, z), f2#(x, 1(), z) -> f0#(x, z, z)) (ifTimes#(false(), i, x, y, z) -> plus#(z, y), plus#(x, y) -> ifPlus#(isZero(x), x, inc(y))) (ifTimes#(false(), i, x, y, z) -> plus#(z, y), plus#(x, y) -> isZero#(x)) (ifTimes#(false(), i, x, y, z) -> plus#(z, y), plus#(x, y) -> inc#(y)) (plus#(x, y) -> ifPlus#(isZero(x), x, inc(y)), ifPlus#(true(), x, y) -> p#(y)) (plus#(x, y) -> ifPlus#(isZero(x), x, inc(y)), ifPlus#(false(), x, y) -> plus#(p(x), y)) (plus#(x, y) -> ifPlus#(isZero(x), x, inc(y)), ifPlus#(false(), x, y) -> p#(x))} SCCS: Scc: { f1#(x, y, z) -> f2#(x, y, z), f0#(0(), y, x) -> f1#(x, y, x), f2#(x, 1(), z) -> f0#(x, z, z)} Scc: {ge#(s(x), s(y)) -> ge#(x, y)} Scc: { timesIter#(i, x, y, z) -> ifTimes#(ge(i, x), i, x, y, z), ifTimes#(false(), i, x, y, z) -> timesIter#(inc(i), x, y, plus(z, y))} Scc: {p#(s(s(x))) -> p#(s(x))} Scc: {inc#(s(x)) -> inc#(x)} Scc: {isZero#(s(s(x))) -> isZero#(s(x))} Scc: {ifPlus#(false(), x, y) -> plus#(p(x), y), plus#(x, y) -> ifPlus#(isZero(x), x, inc(y))} SCC: Strict: { f1#(x, y, z) -> f2#(x, y, z), f0#(0(), y, x) -> f1#(x, y, x), f2#(x, 1(), z) -> f0#(x, z, z)} Weak: { ifPlus(true(), x, y) -> p(y), ifPlus(false(), x, y) -> plus(p(x), y), isZero(0()) -> true(), isZero(s(0())) -> false(), isZero(s(s(x))) -> isZero(s(x)), inc(x) -> s(x), inc(0()) -> s(0()), inc(s(x)) -> s(inc(x)), plus(x, y) -> ifPlus(isZero(x), x, inc(y)), p(0()) -> 0(), p(s(x)) -> x, p(s(s(x))) -> s(p(s(x))), timesIter(i, x, y, z) -> ifTimes(ge(i, x), i, x, y, z), times(x, y) -> timesIter(0(), x, y, 0()), ifTimes(true(), i, x, y, z) -> z, ifTimes(false(), i, x, y, z) -> timesIter(inc(i), x, y, plus(z, y)), ge(x, 0()) -> true(), ge(0(), s(y)) -> false(), ge(s(x), s(y)) -> ge(x, y), f1(x, y, z) -> f2(x, y, z), f1(x, y, z) -> c(), f0(x, y, z) -> d(), f0(0(), y, x) -> f1(x, y, x), f2(x, 1(), z) -> f0(x, z, z)} Fail SCC: Strict: {ge#(s(x), s(y)) -> ge#(x, y)} Weak: { ifPlus(true(), x, y) -> p(y), ifPlus(false(), x, y) -> plus(p(x), y), isZero(0()) -> true(), isZero(s(0())) -> false(), isZero(s(s(x))) -> isZero(s(x)), inc(x) -> s(x), inc(0()) -> s(0()), inc(s(x)) -> s(inc(x)), plus(x, y) -> ifPlus(isZero(x), x, inc(y)), p(0()) -> 0(), p(s(x)) -> x, p(s(s(x))) -> s(p(s(x))), timesIter(i, x, y, z) -> ifTimes(ge(i, x), i, x, y, z), times(x, y) -> timesIter(0(), x, y, 0()), ifTimes(true(), i, x, y, z) -> z, ifTimes(false(), i, x, y, z) -> timesIter(inc(i), x, y, plus(z, y)), ge(x, 0()) -> true(), ge(0(), s(y)) -> false(), ge(s(x), s(y)) -> ge(x, y), f1(x, y, z) -> f2(x, y, z), f1(x, y, z) -> c(), f0(x, y, z) -> d(), f0(0(), y, x) -> f1(x, y, x), f2(x, 1(), z) -> f0(x, z, z)} SPSC: Simple Projection: pi(ge#) = 0 Strict: {} Qed SCC: Strict: { timesIter#(i, x, y, z) -> ifTimes#(ge(i, x), i, x, y, z), ifTimes#(false(), i, x, y, z) -> timesIter#(inc(i), x, y, plus(z, y))} Weak: { ifPlus(true(), x, y) -> p(y), ifPlus(false(), x, y) -> plus(p(x), y), isZero(0()) -> true(), isZero(s(0())) -> false(), isZero(s(s(x))) -> isZero(s(x)), inc(x) -> s(x), inc(0()) -> s(0()), inc(s(x)) -> s(inc(x)), plus(x, y) -> ifPlus(isZero(x), x, inc(y)), p(0()) -> 0(), p(s(x)) -> x, p(s(s(x))) -> s(p(s(x))), timesIter(i, x, y, z) -> ifTimes(ge(i, x), i, x, y, z), times(x, y) -> timesIter(0(), x, y, 0()), ifTimes(true(), i, x, y, z) -> z, ifTimes(false(), i, x, y, z) -> timesIter(inc(i), x, y, plus(z, y)), ge(x, 0()) -> true(), ge(0(), s(y)) -> false(), ge(s(x), s(y)) -> ge(x, y), f1(x, y, z) -> f2(x, y, z), f1(x, y, z) -> c(), f0(x, y, z) -> d(), f0(0(), y, x) -> f1(x, y, x), f2(x, 1(), z) -> f0(x, z, z)} Fail SCC: Strict: {p#(s(s(x))) -> p#(s(x))} Weak: { ifPlus(true(), x, y) -> p(y), ifPlus(false(), x, y) -> plus(p(x), y), isZero(0()) -> true(), isZero(s(0())) -> false(), isZero(s(s(x))) -> isZero(s(x)), inc(x) -> s(x), inc(0()) -> s(0()), inc(s(x)) -> s(inc(x)), plus(x, y) -> ifPlus(isZero(x), x, inc(y)), p(0()) -> 0(), p(s(x)) -> x, p(s(s(x))) -> s(p(s(x))), timesIter(i, x, y, z) -> ifTimes(ge(i, x), i, x, y, z), times(x, y) -> timesIter(0(), x, y, 0()), ifTimes(true(), i, x, y, z) -> z, ifTimes(false(), i, x, y, z) -> timesIter(inc(i), x, y, plus(z, y)), ge(x, 0()) -> true(), ge(0(), s(y)) -> false(), ge(s(x), s(y)) -> ge(x, y), f1(x, y, z) -> f2(x, y, z), f1(x, y, z) -> c(), f0(x, y, z) -> d(), f0(0(), y, x) -> f1(x, y, x), f2(x, 1(), z) -> f0(x, z, z)} SPSC: Simple Projection: pi(p#) = 0 Strict: {} Qed SCC: Strict: {inc#(s(x)) -> inc#(x)} Weak: { ifPlus(true(), x, y) -> p(y), ifPlus(false(), x, y) -> plus(p(x), y), isZero(0()) -> true(), isZero(s(0())) -> false(), isZero(s(s(x))) -> isZero(s(x)), inc(x) -> s(x), inc(0()) -> s(0()), inc(s(x)) -> s(inc(x)), plus(x, y) -> ifPlus(isZero(x), x, inc(y)), p(0()) -> 0(), p(s(x)) -> x, p(s(s(x))) -> s(p(s(x))), timesIter(i, x, y, z) -> ifTimes(ge(i, x), i, x, y, z), times(x, y) -> timesIter(0(), x, y, 0()), ifTimes(true(), i, x, y, z) -> z, ifTimes(false(), i, x, y, z) -> timesIter(inc(i), x, y, plus(z, y)), ge(x, 0()) -> true(), ge(0(), s(y)) -> false(), ge(s(x), s(y)) -> ge(x, y), f1(x, y, z) -> f2(x, y, z), f1(x, y, z) -> c(), f0(x, y, z) -> d(), f0(0(), y, x) -> f1(x, y, x), f2(x, 1(), z) -> f0(x, z, z)} SPSC: Simple Projection: pi(inc#) = 0 Strict: {} Qed SCC: Strict: {isZero#(s(s(x))) -> isZero#(s(x))} Weak: { ifPlus(true(), x, y) -> p(y), ifPlus(false(), x, y) -> plus(p(x), y), isZero(0()) -> true(), isZero(s(0())) -> false(), isZero(s(s(x))) -> isZero(s(x)), inc(x) -> s(x), inc(0()) -> s(0()), inc(s(x)) -> s(inc(x)), plus(x, y) -> ifPlus(isZero(x), x, inc(y)), p(0()) -> 0(), p(s(x)) -> x, p(s(s(x))) -> s(p(s(x))), timesIter(i, x, y, z) -> ifTimes(ge(i, x), i, x, y, z), times(x, y) -> timesIter(0(), x, y, 0()), ifTimes(true(), i, x, y, z) -> z, ifTimes(false(), i, x, y, z) -> timesIter(inc(i), x, y, plus(z, y)), ge(x, 0()) -> true(), ge(0(), s(y)) -> false(), ge(s(x), s(y)) -> ge(x, y), f1(x, y, z) -> f2(x, y, z), f1(x, y, z) -> c(), f0(x, y, z) -> d(), f0(0(), y, x) -> f1(x, y, x), f2(x, 1(), z) -> f0(x, z, z)} SPSC: Simple Projection: pi(isZero#) = 0 Strict: {} Qed SCC: Strict: {ifPlus#(false(), x, y) -> plus#(p(x), y), plus#(x, y) -> ifPlus#(isZero(x), x, inc(y))} Weak: { ifPlus(true(), x, y) -> p(y), ifPlus(false(), x, y) -> plus(p(x), y), isZero(0()) -> true(), isZero(s(0())) -> false(), isZero(s(s(x))) -> isZero(s(x)), inc(x) -> s(x), inc(0()) -> s(0()), inc(s(x)) -> s(inc(x)), plus(x, y) -> ifPlus(isZero(x), x, inc(y)), p(0()) -> 0(), p(s(x)) -> x, p(s(s(x))) -> s(p(s(x))), timesIter(i, x, y, z) -> ifTimes(ge(i, x), i, x, y, z), times(x, y) -> timesIter(0(), x, y, 0()), ifTimes(true(), i, x, y, z) -> z, ifTimes(false(), i, x, y, z) -> timesIter(inc(i), x, y, plus(z, y)), ge(x, 0()) -> true(), ge(0(), s(y)) -> false(), ge(s(x), s(y)) -> ge(x, y), f1(x, y, z) -> f2(x, y, z), f1(x, y, z) -> c(), f0(x, y, z) -> d(), f0(0(), y, x) -> f1(x, y, x), f2(x, 1(), z) -> f0(x, z, z)} Fail