MAYBE Time: 0.008020 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: DP: { 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)} 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)} EDG: {(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) (ifTimes#(false(), i, x, y, z) -> inc# i, inc# s x -> inc# x) (ifTimes#(false(), i, x, y, z) -> timesIter#(inc i, x, y, plus(z, y)), timesIter#(i, x, y, z) -> ge#(i, 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)) (p# s s x -> p# s x, p# s s x -> p# s x) (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) (timesIter#(i, x, y, z) -> ifTimes#(ge(i, x), i, x, y, z), ifTimes#(false(), i, x, y, z) -> inc# i) (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) -> timesIter#(inc i, x, y, plus(z, y))) (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) (isZero# s s x -> isZero# s x, isZero# s s x -> isZero# s x) (times#(x, y) -> timesIter#(0(), x, y, 0()), timesIter#(i, x, y, z) -> ifTimes#(ge(i, x), i, x, y, z)) (times#(x, y) -> timesIter#(0(), x, y, 0()), timesIter#(i, x, y, z) -> ge#(i, 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)) (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)} STATUS: arrows: 0.919668 SCCS (7): 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: { 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: {ifPlus#(false(), x, y) -> plus#(p x, y), plus#(x, y) -> ifPlus#(isZero x, x, inc y)} Scc: {inc# s x -> inc# x} Scc: {isZero# s s x -> isZero# s x} Scc: {p# s s x -> p# s x} SCC (2): 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)} Open SCC (3): 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)} Open SCC (1): 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)} Open SCC (2): 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)} Open SCC (1): 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)} Open SCC (1): 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)} Open SCC (1): 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)} Open