MAYBE Time: 0.062237 TRS: { prodIter(xs, x) -> ifProd(isempty xs, xs, x), prod xs -> prodIter(xs, s 0()), ifProd(true(), xs, x) -> x, ifProd(false(), xs, x) -> prodIter(tail xs, times(x, head xs)), isempty nil() -> true(), isempty cons(x, xs) -> false(), tail nil() -> nil(), tail cons(x, xs) -> xs, times(x, y) -> timesIter(x, y, 0(), 0()), head nil() -> error(), head cons(x, xs) -> x, plus(s x, y) -> s plus(x, y), plus(0(), y) -> y, timesIter(x, y, z, u) -> ifTimes(ge(u, x), x, y, z, u), ifTimes(true(), x, y, z, u) -> z, ifTimes(false(), x, y, z, u) -> timesIter(x, y, plus(y, z), s u), ge(x, 0()) -> true(), ge(s x, s y) -> ge(x, y), ge(0(), s y) -> false(), a() -> b(), a() -> c()} DP: DP: { prodIter#(xs, x) -> ifProd#(isempty xs, xs, x), prodIter#(xs, x) -> isempty# xs, prod# xs -> prodIter#(xs, s 0()), ifProd#(false(), xs, x) -> prodIter#(tail xs, times(x, head xs)), ifProd#(false(), xs, x) -> tail# xs, ifProd#(false(), xs, x) -> times#(x, head xs), ifProd#(false(), xs, x) -> head# xs, times#(x, y) -> timesIter#(x, y, 0(), 0()), plus#(s x, y) -> plus#(x, y), timesIter#(x, y, z, u) -> ifTimes#(ge(u, x), x, y, z, u), timesIter#(x, y, z, u) -> ge#(u, x), ifTimes#(false(), x, y, z, u) -> plus#(y, z), ifTimes#(false(), x, y, z, u) -> timesIter#(x, y, plus(y, z), s u), ge#(s x, s y) -> ge#(x, y)} TRS: { prodIter(xs, x) -> ifProd(isempty xs, xs, x), prod xs -> prodIter(xs, s 0()), ifProd(true(), xs, x) -> x, ifProd(false(), xs, x) -> prodIter(tail xs, times(x, head xs)), isempty nil() -> true(), isempty cons(x, xs) -> false(), tail nil() -> nil(), tail cons(x, xs) -> xs, times(x, y) -> timesIter(x, y, 0(), 0()), head nil() -> error(), head cons(x, xs) -> x, plus(s x, y) -> s plus(x, y), plus(0(), y) -> y, timesIter(x, y, z, u) -> ifTimes(ge(u, x), x, y, z, u), ifTimes(true(), x, y, z, u) -> z, ifTimes(false(), x, y, z, u) -> timesIter(x, y, plus(y, z), s u), ge(x, 0()) -> true(), ge(s x, s y) -> ge(x, y), ge(0(), s y) -> false(), a() -> b(), a() -> c()} UR: { isempty nil() -> true(), isempty cons(x, xs) -> false(), tail nil() -> nil(), tail cons(x, xs) -> xs, times(x, y) -> timesIter(x, y, 0(), 0()), head nil() -> error(), head cons(x, xs) -> x, plus(s x, y) -> s plus(x, y), plus(0(), y) -> y, timesIter(x, y, z, u) -> ifTimes(ge(u, x), x, y, z, u), ifTimes(true(), x, y, z, u) -> z, ifTimes(false(), x, y, z, u) -> timesIter(x, y, plus(y, z), s u), ge(x, 0()) -> true(), ge(s x, s y) -> ge(x, y), ge(0(), s y) -> false(), d(w, v) -> w, d(w, v) -> v} EDG: {(timesIter#(x, y, z, u) -> ifTimes#(ge(u, x), x, y, z, u), ifTimes#(false(), x, y, z, u) -> timesIter#(x, y, plus(y, z), s u)) (timesIter#(x, y, z, u) -> ifTimes#(ge(u, x), x, y, z, u), ifTimes#(false(), x, y, z, u) -> plus#(y, z)) (plus#(s x, y) -> plus#(x, y), plus#(s x, y) -> plus#(x, y)) (ifProd#(false(), xs, x) -> prodIter#(tail xs, times(x, head xs)), prodIter#(xs, x) -> isempty# xs) (ifProd#(false(), xs, x) -> prodIter#(tail xs, times(x, head xs)), prodIter#(xs, x) -> ifProd#(isempty xs, xs, x)) (ifProd#(false(), xs, x) -> times#(x, head xs), times#(x, y) -> timesIter#(x, y, 0(), 0())) (ifTimes#(false(), x, y, z, u) -> timesIter#(x, y, plus(y, z), s u), timesIter#(x, y, z, u) -> ge#(u, x)) (ifTimes#(false(), x, y, z, u) -> timesIter#(x, y, plus(y, z), s u), timesIter#(x, y, z, u) -> ifTimes#(ge(u, x), x, y, z, u)) (prodIter#(xs, x) -> ifProd#(isempty xs, xs, x), ifProd#(false(), xs, x) -> prodIter#(tail xs, times(x, head xs))) (prodIter#(xs, x) -> ifProd#(isempty xs, xs, x), ifProd#(false(), xs, x) -> tail# xs) (prodIter#(xs, x) -> ifProd#(isempty xs, xs, x), ifProd#(false(), xs, x) -> times#(x, head xs)) (prodIter#(xs, x) -> ifProd#(isempty xs, xs, x), ifProd#(false(), xs, x) -> head# xs) (times#(x, y) -> timesIter#(x, y, 0(), 0()), timesIter#(x, y, z, u) -> ifTimes#(ge(u, x), x, y, z, u)) (times#(x, y) -> timesIter#(x, y, 0(), 0()), timesIter#(x, y, z, u) -> ge#(u, x)) (ifTimes#(false(), x, y, z, u) -> plus#(y, z), plus#(s x, y) -> plus#(x, y)) (ge#(s x, s y) -> ge#(x, y), ge#(s x, s y) -> ge#(x, y)) (timesIter#(x, y, z, u) -> ge#(u, x), ge#(s x, s y) -> ge#(x, y)) (prod# xs -> prodIter#(xs, s 0()), prodIter#(xs, x) -> ifProd#(isempty xs, xs, x)) (prod# xs -> prodIter#(xs, s 0()), prodIter#(xs, x) -> isempty# xs)} STATUS: arrows: 0.903061 SCCS (4): Scc: { prodIter#(xs, x) -> ifProd#(isempty xs, xs, x), ifProd#(false(), xs, x) -> prodIter#(tail xs, times(x, head xs))} Scc: { timesIter#(x, y, z, u) -> ifTimes#(ge(u, x), x, y, z, u), ifTimes#(false(), x, y, z, u) -> timesIter#(x, y, plus(y, z), s u)} Scc: {ge#(s x, s y) -> ge#(x, y)} Scc: {plus#(s x, y) -> plus#(x, y)} SCC (2): Strict: { prodIter#(xs, x) -> ifProd#(isempty xs, xs, x), ifProd#(false(), xs, x) -> prodIter#(tail xs, times(x, head xs))} Weak: { prodIter(xs, x) -> ifProd(isempty xs, xs, x), prod xs -> prodIter(xs, s 0()), ifProd(true(), xs, x) -> x, ifProd(false(), xs, x) -> prodIter(tail xs, times(x, head xs)), isempty nil() -> true(), isempty cons(x, xs) -> false(), tail nil() -> nil(), tail cons(x, xs) -> xs, times(x, y) -> timesIter(x, y, 0(), 0()), head nil() -> error(), head cons(x, xs) -> x, plus(s x, y) -> s plus(x, y), plus(0(), y) -> y, timesIter(x, y, z, u) -> ifTimes(ge(u, x), x, y, z, u), ifTimes(true(), x, y, z, u) -> z, ifTimes(false(), x, y, z, u) -> timesIter(x, y, plus(y, z), s u), ge(x, 0()) -> true(), ge(s x, s y) -> ge(x, y), ge(0(), s y) -> false(), a() -> b(), a() -> c()} Fail SCC (2): Strict: { timesIter#(x, y, z, u) -> ifTimes#(ge(u, x), x, y, z, u), ifTimes#(false(), x, y, z, u) -> timesIter#(x, y, plus(y, z), s u)} Weak: { prodIter(xs, x) -> ifProd(isempty xs, xs, x), prod xs -> prodIter(xs, s 0()), ifProd(true(), xs, x) -> x, ifProd(false(), xs, x) -> prodIter(tail xs, times(x, head xs)), isempty nil() -> true(), isempty cons(x, xs) -> false(), tail nil() -> nil(), tail cons(x, xs) -> xs, times(x, y) -> timesIter(x, y, 0(), 0()), head nil() -> error(), head cons(x, xs) -> x, plus(s x, y) -> s plus(x, y), plus(0(), y) -> y, timesIter(x, y, z, u) -> ifTimes(ge(u, x), x, y, z, u), ifTimes(true(), x, y, z, u) -> z, ifTimes(false(), x, y, z, u) -> timesIter(x, y, plus(y, z), s u), ge(x, 0()) -> true(), ge(s x, s y) -> ge(x, y), ge(0(), s y) -> false(), a() -> b(), a() -> c()} Fail SCC (1): Strict: {ge#(s x, s y) -> ge#(x, y)} Weak: { prodIter(xs, x) -> ifProd(isempty xs, xs, x), prod xs -> prodIter(xs, s 0()), ifProd(true(), xs, x) -> x, ifProd(false(), xs, x) -> prodIter(tail xs, times(x, head xs)), isempty nil() -> true(), isempty cons(x, xs) -> false(), tail nil() -> nil(), tail cons(x, xs) -> xs, times(x, y) -> timesIter(x, y, 0(), 0()), head nil() -> error(), head cons(x, xs) -> x, plus(s x, y) -> s plus(x, y), plus(0(), y) -> y, timesIter(x, y, z, u) -> ifTimes(ge(u, x), x, y, z, u), ifTimes(true(), x, y, z, u) -> z, ifTimes(false(), x, y, z, u) -> timesIter(x, y, plus(y, z), s u), ge(x, 0()) -> true(), ge(s x, s y) -> ge(x, y), ge(0(), s y) -> false(), a() -> b(), a() -> c()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [ifTimes](x0, x1, x2, x3, x4) = x0 + x1 + x2, [timesIter](x0, x1, x2, x3) = x0 + x1 + x2, [ifProd](x0, x1, x2) = x0 + x1 + 1, [prodIter](x0, x1) = 0, [times](x0, x1) = x0, [plus](x0, x1) = x0 + 1, [ge](x0, x1) = x0 + x1, [cons](x0, x1) = 1, [s](x0) = x0 + 1, [prod](x0) = 0, [isempty](x0) = x0 + 1, [tail](x0) = x0 + 1, [head](x0) = 1, [0] = 1, [true] = 0, [false] = 1, [nil] = 1, [error] = 0, [b] = 0, [a] = 0, [c] = 0, [ge#](x0, x1) = x0 Strict: ge#(s x, s y) -> ge#(x, y) 1 + 0x + 1y >= 0 + 0x + 1y Weak: a() -> c() 0 >= 0 a() -> b() 0 >= 0 ge(0(), s y) -> false() 2 + 1y >= 1 ge(s x, s y) -> ge(x, y) 2 + 1x + 1y >= 0 + 1x + 1y ge(x, 0()) -> true() 1 + 1x >= 0 ifTimes(false(), x, y, z, u) -> timesIter(x, y, plus(y, z), s u) 1 + 1x + 0y + 1u + 0z >= 2 + 0x + 2y + 1u + 0z ifTimes(true(), x, y, z, u) -> z 0 + 1x + 0y + 1u + 0z >= 1z timesIter(x, y, z, u) -> ifTimes(ge(u, x), x, y, z, u) 0 + 0x + 1y + 1u + 1z >= 0 + 2x + 0y + 2u + 0z plus(0(), y) -> y 2 + 0y >= 1y plus(s x, y) -> s plus(x, y) 2 + 1x + 0y >= 2 + 1x + 0y head cons(x, xs) -> x 1 + 0xs + 0x >= 1x head nil() -> error() 1 >= 0 times(x, y) -> timesIter(x, y, 0(), 0()) 0 + 0x + 1y >= 2 + 0x + 1y tail cons(x, xs) -> xs 2 + 0xs + 0x >= 1xs tail nil() -> nil() 2 >= 1 isempty cons(x, xs) -> false() 2 + 0xs + 0x >= 1 isempty nil() -> true() 2 >= 0 ifProd(false(), xs, x) -> prodIter(tail xs, times(x, head xs)) 2 + 1xs + 0x >= 0 + 0xs + 0x ifProd(true(), xs, x) -> x 1 + 1xs + 0x >= 1x prod xs -> prodIter(xs, s 0()) 0 + 0xs >= 0 + 0xs prodIter(xs, x) -> ifProd(isempty xs, xs, x) 0 + 0xs + 0x >= 2 + 2xs + 0x Qed SCC (1): Strict: {plus#(s x, y) -> plus#(x, y)} Weak: { prodIter(xs, x) -> ifProd(isempty xs, xs, x), prod xs -> prodIter(xs, s 0()), ifProd(true(), xs, x) -> x, ifProd(false(), xs, x) -> prodIter(tail xs, times(x, head xs)), isempty nil() -> true(), isempty cons(x, xs) -> false(), tail nil() -> nil(), tail cons(x, xs) -> xs, times(x, y) -> timesIter(x, y, 0(), 0()), head nil() -> error(), head cons(x, xs) -> x, plus(s x, y) -> s plus(x, y), plus(0(), y) -> y, timesIter(x, y, z, u) -> ifTimes(ge(u, x), x, y, z, u), ifTimes(true(), x, y, z, u) -> z, ifTimes(false(), x, y, z, u) -> timesIter(x, y, plus(y, z), s u), ge(x, 0()) -> true(), ge(s x, s y) -> ge(x, y), ge(0(), s y) -> false(), a() -> b(), a() -> c()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [ifTimes](x0, x1, x2, x3, x4) = x0 + x1 + x2 + 1, [timesIter](x0, x1, x2, x3) = 0, [ifProd](x0, x1, x2) = x0 + x1 + 1, [prodIter](x0, x1) = 0, [times](x0, x1) = x0 + 1, [plus](x0, x1) = x0 + 1, [ge](x0, x1) = x0 + x1 + 1, [cons](x0, x1) = 1, [s](x0) = x0 + 1, [prod](x0) = 0, [isempty](x0) = x0 + 1, [tail](x0) = x0 + 1, [head](x0) = 1, [0] = 1, [true] = 0, [false] = 1, [nil] = 1, [error] = 0, [b] = 0, [a] = 0, [c] = 0, [plus#](x0, x1) = x0 Strict: plus#(s x, y) -> plus#(x, y) 1 + 1x + 0y >= 0 + 1x + 0y Weak: a() -> c() 0 >= 0 a() -> b() 0 >= 0 ge(0(), s y) -> false() 3 + 1y >= 1 ge(s x, s y) -> ge(x, y) 3 + 1x + 1y >= 1 + 1x + 1y ge(x, 0()) -> true() 2 + 1x >= 0 ifTimes(false(), x, y, z, u) -> timesIter(x, y, plus(y, z), s u) 2 + 1x + 0y + 1u + 0z >= 0 + 0x + 0y + 0u + 0z ifTimes(true(), x, y, z, u) -> z 1 + 1x + 0y + 1u + 0z >= 1z timesIter(x, y, z, u) -> ifTimes(ge(u, x), x, y, z, u) 0 + 0x + 0y + 0u + 0z >= 2 + 2x + 0y + 2u + 0z plus(0(), y) -> y 2 + 0y >= 1y plus(s x, y) -> s plus(x, y) 2 + 1x + 0y >= 2 + 1x + 0y head cons(x, xs) -> x 1 + 0xs + 0x >= 1x head nil() -> error() 1 >= 0 times(x, y) -> timesIter(x, y, 0(), 0()) 1 + 0x + 1y >= 0 + 0x + 0y tail cons(x, xs) -> xs 2 + 0xs + 0x >= 1xs tail nil() -> nil() 2 >= 1 isempty cons(x, xs) -> false() 2 + 0xs + 0x >= 1 isempty nil() -> true() 2 >= 0 ifProd(false(), xs, x) -> prodIter(tail xs, times(x, head xs)) 2 + 1xs + 0x >= 0 + 0xs + 0x ifProd(true(), xs, x) -> x 1 + 1xs + 0x >= 1x prod xs -> prodIter(xs, s 0()) 0 + 0xs >= 0 + 0xs prodIter(xs, x) -> ifProd(isempty xs, xs, x) 0 + 0xs + 0x >= 2 + 2xs + 0x Qed