MAYBE Time: 0.038208 TRS: { plusIter(x, y, z) -> ifPlus(le(x, z), x, y, z), plus(x, y) -> plusIter(x, y, 0()), ifPlus(true(), x, y, z) -> y, ifPlus(false(), x, y, z) -> plusIter(x, s y, s z), le(0(), y) -> true(), le(s x, 0()) -> false(), le(s x, s y) -> le(x, y), sumIter(xs, x) -> ifSum(isempty xs, xs, x, plus(x, head xs)), sum xs -> sumIter(xs, 0()), ifSum(true(), xs, x, y) -> x, ifSum(false(), xs, x, y) -> sumIter(tail xs, y), isempty nil() -> true(), isempty cons(x, xs) -> false(), head nil() -> error(), head cons(x, xs) -> x, tail nil() -> nil(), tail cons(x, xs) -> xs, a() -> b(), a() -> c()} DP: DP: { plusIter#(x, y, z) -> ifPlus#(le(x, z), x, y, z), plusIter#(x, y, z) -> le#(x, z), plus#(x, y) -> plusIter#(x, y, 0()), ifPlus#(false(), x, y, z) -> plusIter#(x, s y, s z), le#(s x, s y) -> le#(x, y), sumIter#(xs, x) -> plus#(x, head xs), sumIter#(xs, x) -> ifSum#(isempty xs, xs, x, plus(x, head xs)), sumIter#(xs, x) -> isempty# xs, sumIter#(xs, x) -> head# xs, sum# xs -> sumIter#(xs, 0()), ifSum#(false(), xs, x, y) -> sumIter#(tail xs, y), ifSum#(false(), xs, x, y) -> tail# xs} TRS: { plusIter(x, y, z) -> ifPlus(le(x, z), x, y, z), plus(x, y) -> plusIter(x, y, 0()), ifPlus(true(), x, y, z) -> y, ifPlus(false(), x, y, z) -> plusIter(x, s y, s z), le(0(), y) -> true(), le(s x, 0()) -> false(), le(s x, s y) -> le(x, y), sumIter(xs, x) -> ifSum(isempty xs, xs, x, plus(x, head xs)), sum xs -> sumIter(xs, 0()), ifSum(true(), xs, x, y) -> x, ifSum(false(), xs, x, y) -> sumIter(tail xs, y), isempty nil() -> true(), isempty cons(x, xs) -> false(), head nil() -> error(), head cons(x, xs) -> x, tail nil() -> nil(), tail cons(x, xs) -> xs, a() -> b(), a() -> c()} UR: { plusIter(x, y, z) -> ifPlus(le(x, z), x, y, z), plus(x, y) -> plusIter(x, y, 0()), ifPlus(true(), x, y, z) -> y, ifPlus(false(), x, y, z) -> plusIter(x, s y, s z), le(0(), y) -> true(), le(s x, 0()) -> false(), le(s x, s y) -> le(x, y), isempty nil() -> true(), isempty cons(x, xs) -> false(), head nil() -> error(), head cons(x, xs) -> x, tail nil() -> nil(), tail cons(x, xs) -> xs, d(w, v) -> w, d(w, v) -> v} EDG: {(sumIter#(xs, x) -> ifSum#(isempty xs, xs, x, plus(x, head xs)), ifSum#(false(), xs, x, y) -> tail# xs) (sumIter#(xs, x) -> ifSum#(isempty xs, xs, x, plus(x, head xs)), ifSum#(false(), xs, x, y) -> sumIter#(tail xs, y)) (plusIter#(x, y, z) -> ifPlus#(le(x, z), x, y, z), ifPlus#(false(), x, y, z) -> plusIter#(x, s y, s z)) (plus#(x, y) -> plusIter#(x, y, 0()), plusIter#(x, y, z) -> le#(x, z)) (plus#(x, y) -> plusIter#(x, y, 0()), plusIter#(x, y, z) -> ifPlus#(le(x, z), x, y, z)) (ifPlus#(false(), x, y, z) -> plusIter#(x, s y, s z), plusIter#(x, y, z) -> le#(x, z)) (ifPlus#(false(), x, y, z) -> plusIter#(x, s y, s z), plusIter#(x, y, z) -> ifPlus#(le(x, z), x, y, z)) (ifSum#(false(), xs, x, y) -> sumIter#(tail xs, y), sumIter#(xs, x) -> plus#(x, head xs)) (ifSum#(false(), xs, x, y) -> sumIter#(tail xs, y), sumIter#(xs, x) -> ifSum#(isempty xs, xs, x, plus(x, head xs))) (ifSum#(false(), xs, x, y) -> sumIter#(tail xs, y), sumIter#(xs, x) -> isempty# xs) (ifSum#(false(), xs, x, y) -> sumIter#(tail xs, y), sumIter#(xs, x) -> head# xs) (le#(s x, s y) -> le#(x, y), le#(s x, s y) -> le#(x, y)) (plusIter#(x, y, z) -> le#(x, z), le#(s x, s y) -> le#(x, y)) (sum# xs -> sumIter#(xs, 0()), sumIter#(xs, x) -> plus#(x, head xs)) (sum# xs -> sumIter#(xs, 0()), sumIter#(xs, x) -> ifSum#(isempty xs, xs, x, plus(x, head xs))) (sum# xs -> sumIter#(xs, 0()), sumIter#(xs, x) -> isempty# xs) (sum# xs -> sumIter#(xs, 0()), sumIter#(xs, x) -> head# xs) (sumIter#(xs, x) -> plus#(x, head xs), plus#(x, y) -> plusIter#(x, y, 0()))} STATUS: arrows: 0.875000 SCCS (3): Scc: { sumIter#(xs, x) -> ifSum#(isempty xs, xs, x, plus(x, head xs)), ifSum#(false(), xs, x, y) -> sumIter#(tail xs, y)} Scc: { plusIter#(x, y, z) -> ifPlus#(le(x, z), x, y, z), ifPlus#(false(), x, y, z) -> plusIter#(x, s y, s z)} Scc: {le#(s x, s y) -> le#(x, y)} SCC (2): Strict: { sumIter#(xs, x) -> ifSum#(isempty xs, xs, x, plus(x, head xs)), ifSum#(false(), xs, x, y) -> sumIter#(tail xs, y)} Weak: { plusIter(x, y, z) -> ifPlus(le(x, z), x, y, z), plus(x, y) -> plusIter(x, y, 0()), ifPlus(true(), x, y, z) -> y, ifPlus(false(), x, y, z) -> plusIter(x, s y, s z), le(0(), y) -> true(), le(s x, 0()) -> false(), le(s x, s y) -> le(x, y), sumIter(xs, x) -> ifSum(isempty xs, xs, x, plus(x, head xs)), sum xs -> sumIter(xs, 0()), ifSum(true(), xs, x, y) -> x, ifSum(false(), xs, x, y) -> sumIter(tail xs, y), isempty nil() -> true(), isempty cons(x, xs) -> false(), head nil() -> error(), head cons(x, xs) -> x, tail nil() -> nil(), tail cons(x, xs) -> xs, a() -> b(), a() -> c()} Fail SCC (2): Strict: { plusIter#(x, y, z) -> ifPlus#(le(x, z), x, y, z), ifPlus#(false(), x, y, z) -> plusIter#(x, s y, s z)} Weak: { plusIter(x, y, z) -> ifPlus(le(x, z), x, y, z), plus(x, y) -> plusIter(x, y, 0()), ifPlus(true(), x, y, z) -> y, ifPlus(false(), x, y, z) -> plusIter(x, s y, s z), le(0(), y) -> true(), le(s x, 0()) -> false(), le(s x, s y) -> le(x, y), sumIter(xs, x) -> ifSum(isempty xs, xs, x, plus(x, head xs)), sum xs -> sumIter(xs, 0()), ifSum(true(), xs, x, y) -> x, ifSum(false(), xs, x, y) -> sumIter(tail xs, y), isempty nil() -> true(), isempty cons(x, xs) -> false(), head nil() -> error(), head cons(x, xs) -> x, tail nil() -> nil(), tail cons(x, xs) -> xs, a() -> b(), a() -> c()} Fail SCC (1): Strict: {le#(s x, s y) -> le#(x, y)} Weak: { plusIter(x, y, z) -> ifPlus(le(x, z), x, y, z), plus(x, y) -> plusIter(x, y, 0()), ifPlus(true(), x, y, z) -> y, ifPlus(false(), x, y, z) -> plusIter(x, s y, s z), le(0(), y) -> true(), le(s x, 0()) -> false(), le(s x, s y) -> le(x, y), sumIter(xs, x) -> ifSum(isempty xs, xs, x, plus(x, head xs)), sum xs -> sumIter(xs, 0()), ifSum(true(), xs, x, y) -> x, ifSum(false(), xs, x, y) -> sumIter(tail xs, y), isempty nil() -> true(), isempty cons(x, xs) -> false(), head nil() -> error(), head cons(x, xs) -> x, tail nil() -> nil(), tail cons(x, xs) -> xs, a() -> b(), a() -> c()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [ifPlus](x0, x1, x2, x3) = x0 + x1 + x2 + 1, [ifSum](x0, x1, x2, x3) = 0, [plusIter](x0, x1, x2) = x0 + x1 + 1, [plus](x0, x1) = 0, [le](x0, x1) = x0 + x1 + 1, [sumIter](x0, x1) = x0 + x1 + 1, [cons](x0, x1) = 0, [s](x0) = x0 + 1, [sum](x0) = 0, [isempty](x0) = x0 + 1, [head](x0) = 0, [tail](x0) = 1, [0] = 1, [true] = 1, [false] = 1, [nil] = 1, [error] = 0, [b] = 0, [a] = 0, [c] = 0, [le#](x0, x1) = x0 Strict: le#(s x, s y) -> le#(x, y) 1 + 0x + 1y >= 0 + 0x + 1y Weak: a() -> c() 0 >= 0 a() -> b() 0 >= 0 tail cons(x, xs) -> xs 1 + 0x + 0xs >= 1xs tail nil() -> nil() 1 >= 1 head cons(x, xs) -> x 0 + 0x + 0xs >= 1x head nil() -> error() 0 >= 0 isempty cons(x, xs) -> false() 1 + 0x + 0xs >= 1 isempty nil() -> true() 2 >= 1 ifSum(false(), xs, x, y) -> sumIter(tail xs, y) 0 + 0x + 0y + 0xs >= 2 + 1y + 0xs ifSum(true(), xs, x, y) -> x 0 + 0x + 0y + 0xs >= 1x sum xs -> sumIter(xs, 0()) 0 + 0xs >= 2 + 1xs sumIter(xs, x) -> ifSum(isempty xs, xs, x, plus(x, head xs)) 1 + 1x + 1xs >= 0 + 0x + 0xs le(s x, s y) -> le(x, y) 3 + 1x + 1y >= 1 + 1x + 1y le(s x, 0()) -> false() 3 + 1x >= 1 le(0(), y) -> true() 2 + 1y >= 1 ifPlus(false(), x, y, z) -> plusIter(x, s y, s z) 2 + 1x + 0y + 1z >= 3 + 0x + 1y + 1z ifPlus(true(), x, y, z) -> y 2 + 1x + 0y + 1z >= 1y plus(x, y) -> plusIter(x, y, 0()) 0 + 0x + 0y >= 2 + 0x + 1y plusIter(x, y, z) -> ifPlus(le(x, z), x, y, z) 1 + 0x + 1y + 1z >= 2 + 2x + 0y + 2z Qed