MAYBE Time: 0.101947 TRS: { cons(X1, X2) -> n__cons(X1, X2), oddNs() -> incr pairNs(), pairNs() -> cons(0(), n__incr oddNs()), incr X -> n__incr X, incr cons(X, XS) -> cons(s X, n__incr activate XS), activate X -> X, activate n__incr X -> incr X, activate n__take(X1, X2) -> take(X1, X2), activate n__zip(X1, X2) -> zip(X1, X2), activate n__cons(X1, X2) -> cons(X1, X2), activate n__repItems X -> repItems X, take(X1, X2) -> n__take(X1, X2), take(0(), XS) -> nil(), take(s N, cons(X, XS)) -> cons(X, n__take(N, activate XS)), zip(X, nil()) -> nil(), zip(X1, X2) -> n__zip(X1, X2), zip(cons(X, XS), cons(Y, YS)) -> cons(pair(X, Y), n__zip(activate XS, activate YS)), zip(nil(), XS) -> nil(), tail cons(X, XS) -> activate XS, repItems X -> n__repItems X, repItems cons(X, XS) -> cons(X, n__cons(X, n__repItems activate XS)), repItems nil() -> nil()} DP: DP: { oddNs#() -> pairNs#(), oddNs#() -> incr# pairNs(), pairNs#() -> cons#(0(), n__incr oddNs()), pairNs#() -> oddNs#(), incr# cons(X, XS) -> cons#(s X, n__incr activate XS), incr# cons(X, XS) -> activate# XS, activate# n__incr X -> incr# X, activate# n__take(X1, X2) -> take#(X1, X2), activate# n__zip(X1, X2) -> zip#(X1, X2), activate# n__cons(X1, X2) -> cons#(X1, X2), activate# n__repItems X -> repItems# X, take#(s N, cons(X, XS)) -> cons#(X, n__take(N, activate XS)), take#(s N, cons(X, XS)) -> activate# XS, zip#(cons(X, XS), cons(Y, YS)) -> cons#(pair(X, Y), n__zip(activate XS, activate YS)), zip#(cons(X, XS), cons(Y, YS)) -> activate# XS, zip#(cons(X, XS), cons(Y, YS)) -> activate# YS, tail# cons(X, XS) -> activate# XS, repItems# cons(X, XS) -> cons#(X, n__cons(X, n__repItems activate XS)), repItems# cons(X, XS) -> activate# XS} TRS: { cons(X1, X2) -> n__cons(X1, X2), oddNs() -> incr pairNs(), pairNs() -> cons(0(), n__incr oddNs()), incr X -> n__incr X, incr cons(X, XS) -> cons(s X, n__incr activate XS), activate X -> X, activate n__incr X -> incr X, activate n__take(X1, X2) -> take(X1, X2), activate n__zip(X1, X2) -> zip(X1, X2), activate n__cons(X1, X2) -> cons(X1, X2), activate n__repItems X -> repItems X, take(X1, X2) -> n__take(X1, X2), take(0(), XS) -> nil(), take(s N, cons(X, XS)) -> cons(X, n__take(N, activate XS)), zip(X, nil()) -> nil(), zip(X1, X2) -> n__zip(X1, X2), zip(cons(X, XS), cons(Y, YS)) -> cons(pair(X, Y), n__zip(activate XS, activate YS)), zip(nil(), XS) -> nil(), tail cons(X, XS) -> activate XS, repItems X -> n__repItems X, repItems cons(X, XS) -> cons(X, n__cons(X, n__repItems activate XS)), repItems nil() -> nil()} UR: { cons(X1, X2) -> n__cons(X1, X2), oddNs() -> incr pairNs(), pairNs() -> cons(0(), n__incr oddNs()), incr X -> n__incr X, incr cons(X, XS) -> cons(s X, n__incr activate XS), activate X -> X, activate n__incr X -> incr X, activate n__take(X1, X2) -> take(X1, X2), activate n__zip(X1, X2) -> zip(X1, X2), activate n__cons(X1, X2) -> cons(X1, X2), activate n__repItems X -> repItems X, take(X1, X2) -> n__take(X1, X2), take(0(), XS) -> nil(), take(s N, cons(X, XS)) -> cons(X, n__take(N, activate XS)), zip(X, nil()) -> nil(), zip(X1, X2) -> n__zip(X1, X2), zip(cons(X, XS), cons(Y, YS)) -> cons(pair(X, Y), n__zip(activate XS, activate YS)), zip(nil(), XS) -> nil(), repItems X -> n__repItems X, repItems cons(X, XS) -> cons(X, n__cons(X, n__repItems activate XS)), repItems nil() -> nil(), a(x, y) -> x, a(x, y) -> y} EDG: {(activate# n__zip(X1, X2) -> zip#(X1, X2), zip#(cons(X, XS), cons(Y, YS)) -> activate# YS) (activate# n__zip(X1, X2) -> zip#(X1, X2), zip#(cons(X, XS), cons(Y, YS)) -> activate# XS) (activate# n__zip(X1, X2) -> zip#(X1, X2), zip#(cons(X, XS), cons(Y, YS)) -> cons#(pair(X, Y), n__zip(activate XS, activate YS))) (activate# n__incr X -> incr# X, incr# cons(X, XS) -> activate# XS) (activate# n__incr X -> incr# X, incr# cons(X, XS) -> cons#(s X, n__incr activate XS)) (zip#(cons(X, XS), cons(Y, YS)) -> activate# YS, activate# n__repItems X -> repItems# X) (zip#(cons(X, XS), cons(Y, YS)) -> activate# YS, activate# n__cons(X1, X2) -> cons#(X1, X2)) (zip#(cons(X, XS), cons(Y, YS)) -> activate# YS, activate# n__zip(X1, X2) -> zip#(X1, X2)) (zip#(cons(X, XS), cons(Y, YS)) -> activate# YS, activate# n__take(X1, X2) -> take#(X1, X2)) (zip#(cons(X, XS), cons(Y, YS)) -> activate# YS, activate# n__incr X -> incr# X) (pairNs#() -> oddNs#(), oddNs#() -> incr# pairNs()) (pairNs#() -> oddNs#(), oddNs#() -> pairNs#()) (take#(s N, cons(X, XS)) -> activate# XS, activate# n__repItems X -> repItems# X) (take#(s N, cons(X, XS)) -> activate# XS, activate# n__cons(X1, X2) -> cons#(X1, X2)) (take#(s N, cons(X, XS)) -> activate# XS, activate# n__zip(X1, X2) -> zip#(X1, X2)) (take#(s N, cons(X, XS)) -> activate# XS, activate# n__take(X1, X2) -> take#(X1, X2)) (take#(s N, cons(X, XS)) -> activate# XS, activate# n__incr X -> incr# X) (tail# cons(X, XS) -> activate# XS, activate# n__repItems X -> repItems# X) (tail# cons(X, XS) -> activate# XS, activate# n__cons(X1, X2) -> cons#(X1, X2)) (tail# cons(X, XS) -> activate# XS, activate# n__zip(X1, X2) -> zip#(X1, X2)) (tail# cons(X, XS) -> activate# XS, activate# n__take(X1, X2) -> take#(X1, X2)) (tail# cons(X, XS) -> activate# XS, activate# n__incr X -> incr# X) (repItems# cons(X, XS) -> activate# XS, activate# n__incr X -> incr# X) (repItems# cons(X, XS) -> activate# XS, activate# n__take(X1, X2) -> take#(X1, X2)) (repItems# cons(X, XS) -> activate# XS, activate# n__zip(X1, X2) -> zip#(X1, X2)) (repItems# cons(X, XS) -> activate# XS, activate# n__cons(X1, X2) -> cons#(X1, X2)) (repItems# cons(X, XS) -> activate# XS, activate# n__repItems X -> repItems# X) (zip#(cons(X, XS), cons(Y, YS)) -> activate# XS, activate# n__incr X -> incr# X) (zip#(cons(X, XS), cons(Y, YS)) -> activate# XS, activate# n__take(X1, X2) -> take#(X1, X2)) (zip#(cons(X, XS), cons(Y, YS)) -> activate# XS, activate# n__zip(X1, X2) -> zip#(X1, X2)) (zip#(cons(X, XS), cons(Y, YS)) -> activate# XS, activate# n__cons(X1, X2) -> cons#(X1, X2)) (zip#(cons(X, XS), cons(Y, YS)) -> activate# XS, activate# n__repItems X -> repItems# X) (incr# cons(X, XS) -> activate# XS, activate# n__incr X -> incr# X) (incr# cons(X, XS) -> activate# XS, activate# n__take(X1, X2) -> take#(X1, X2)) (incr# cons(X, XS) -> activate# XS, activate# n__zip(X1, X2) -> zip#(X1, X2)) (incr# cons(X, XS) -> activate# XS, activate# n__cons(X1, X2) -> cons#(X1, X2)) (incr# cons(X, XS) -> activate# XS, activate# n__repItems X -> repItems# X) (oddNs#() -> pairNs#(), pairNs#() -> cons#(0(), n__incr oddNs())) (oddNs#() -> pairNs#(), pairNs#() -> oddNs#()) (activate# n__repItems X -> repItems# X, repItems# cons(X, XS) -> cons#(X, n__cons(X, n__repItems activate XS))) (activate# n__repItems X -> repItems# X, repItems# cons(X, XS) -> activate# XS) (activate# n__take(X1, X2) -> take#(X1, X2), take#(s N, cons(X, XS)) -> cons#(X, n__take(N, activate XS))) (activate# n__take(X1, X2) -> take#(X1, X2), take#(s N, cons(X, XS)) -> activate# XS) (oddNs#() -> incr# pairNs(), incr# cons(X, XS) -> cons#(s X, n__incr activate XS)) (oddNs#() -> incr# pairNs(), incr# cons(X, XS) -> activate# XS)} STATUS: arrows: 0.875346 SCCS (2): Scc: { oddNs#() -> pairNs#(), pairNs#() -> oddNs#()} Scc: { incr# cons(X, XS) -> activate# XS, activate# n__incr X -> incr# X, activate# n__take(X1, X2) -> take#(X1, X2), activate# n__zip(X1, X2) -> zip#(X1, X2), activate# n__repItems X -> repItems# X, take#(s N, cons(X, XS)) -> activate# XS, zip#(cons(X, XS), cons(Y, YS)) -> activate# XS, zip#(cons(X, XS), cons(Y, YS)) -> activate# YS, repItems# cons(X, XS) -> activate# XS} SCC (2): Strict: { oddNs#() -> pairNs#(), pairNs#() -> oddNs#()} Weak: { cons(X1, X2) -> n__cons(X1, X2), oddNs() -> incr pairNs(), pairNs() -> cons(0(), n__incr oddNs()), incr X -> n__incr X, incr cons(X, XS) -> cons(s X, n__incr activate XS), activate X -> X, activate n__incr X -> incr X, activate n__take(X1, X2) -> take(X1, X2), activate n__zip(X1, X2) -> zip(X1, X2), activate n__cons(X1, X2) -> cons(X1, X2), activate n__repItems X -> repItems X, take(X1, X2) -> n__take(X1, X2), take(0(), XS) -> nil(), take(s N, cons(X, XS)) -> cons(X, n__take(N, activate XS)), zip(X, nil()) -> nil(), zip(X1, X2) -> n__zip(X1, X2), zip(cons(X, XS), cons(Y, YS)) -> cons(pair(X, Y), n__zip(activate XS, activate YS)), zip(nil(), XS) -> nil(), tail cons(X, XS) -> activate XS, repItems X -> n__repItems X, repItems cons(X, XS) -> cons(X, n__cons(X, n__repItems activate XS)), repItems nil() -> nil()} Fail SCC (9): Strict: { incr# cons(X, XS) -> activate# XS, activate# n__incr X -> incr# X, activate# n__take(X1, X2) -> take#(X1, X2), activate# n__zip(X1, X2) -> zip#(X1, X2), activate# n__repItems X -> repItems# X, take#(s N, cons(X, XS)) -> activate# XS, zip#(cons(X, XS), cons(Y, YS)) -> activate# XS, zip#(cons(X, XS), cons(Y, YS)) -> activate# YS, repItems# cons(X, XS) -> activate# XS} Weak: { cons(X1, X2) -> n__cons(X1, X2), oddNs() -> incr pairNs(), pairNs() -> cons(0(), n__incr oddNs()), incr X -> n__incr X, incr cons(X, XS) -> cons(s X, n__incr activate XS), activate X -> X, activate n__incr X -> incr X, activate n__take(X1, X2) -> take(X1, X2), activate n__zip(X1, X2) -> zip(X1, X2), activate n__cons(X1, X2) -> cons(X1, X2), activate n__repItems X -> repItems X, take(X1, X2) -> n__take(X1, X2), take(0(), XS) -> nil(), take(s N, cons(X, XS)) -> cons(X, n__take(N, activate XS)), zip(X, nil()) -> nil(), zip(X1, X2) -> n__zip(X1, X2), zip(cons(X, XS), cons(Y, YS)) -> cons(pair(X, Y), n__zip(activate XS, activate YS)), zip(nil(), XS) -> nil(), tail cons(X, XS) -> activate XS, repItems X -> n__repItems X, repItems cons(X, XS) -> cons(X, n__cons(X, n__repItems activate XS)), repItems nil() -> nil()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = x0 + 1, [take](x0, x1) = x0 + x1, [n__take](x0, x1) = x0 + 1, [zip](x0, x1) = x0, [pair](x0, x1) = 0, [n__zip](x0, x1) = x0 + x1 + 1, [n__cons](x0, x1) = x0, [n__incr](x0) = x0 + 1, [incr](x0) = x0 + 1, [s](x0) = 1, [activate](x0) = 1, [tail](x0) = x0 + 1, [repItems](x0) = 0, [n__repItems](x0) = x0 + 1, [0] = 0, [oddNs] = 1, [pairNs] = 1, [nil] = 0, [take#](x0, x1) = x0, [zip#](x0, x1) = x0 + x1 + 1, [incr#](x0) = x0 + 1, [activate#](x0) = x0 + 1, [repItems#](x0) = x0 + 1 Strict: repItems# cons(X, XS) -> activate# XS 2 + 0X + 1XS >= 1 + 1XS zip#(cons(X, XS), cons(Y, YS)) -> activate# YS 3 + 0X + 1XS + 0Y + 1YS >= 1 + 1YS zip#(cons(X, XS), cons(Y, YS)) -> activate# XS 3 + 0X + 1XS + 0Y + 1YS >= 1 + 1XS take#(s N, cons(X, XS)) -> activate# XS 1 + 0X + 1XS + 0N >= 1 + 1XS activate# n__repItems X -> repItems# X 2 + 1X >= 1 + 1X activate# n__zip(X1, X2) -> zip#(X1, X2) 2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2 activate# n__take(X1, X2) -> take#(X1, X2) 2 + 0X1 + 1X2 >= 0 + 0X1 + 1X2 activate# n__incr X -> incr# X 2 + 1X >= 1 + 1X incr# cons(X, XS) -> activate# XS 2 + 0X + 1XS >= 1 + 1XS Weak: repItems nil() -> nil() 0 >= 0 repItems cons(X, XS) -> cons(X, n__cons(X, n__repItems activate XS)) 0 + 0X + 0XS >= 3 + 0X + 0XS repItems X -> n__repItems X 0 + 0X >= 1 + 1X tail cons(X, XS) -> activate XS 2 + 0X + 1XS >= 1 + 0XS zip(nil(), XS) -> nil() 0 + 1XS >= 0 zip(cons(X, XS), cons(Y, YS)) -> cons(pair(X, Y), n__zip(activate XS, activate YS)) 1 + 0X + 0XS + 0Y + 1YS >= 4 + 0X + 0XS + 0Y + 0YS zip(X1, X2) -> n__zip(X1, X2) 0 + 0X1 + 1X2 >= 1 + 1X1 + 1X2 zip(X, nil()) -> nil() 0 + 0X >= 0 take(s N, cons(X, XS)) -> cons(X, n__take(N, activate XS)) 2 + 0X + 1XS + 0N >= 3 + 0X + 0XS + 0N take(0(), XS) -> nil() 0 + 1XS >= 0 take(X1, X2) -> n__take(X1, X2) 0 + 1X1 + 1X2 >= 1 + 0X1 + 1X2 activate n__repItems X -> repItems X 1 + 0X >= 0 + 0X activate n__cons(X1, X2) -> cons(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 1X2 activate n__zip(X1, X2) -> zip(X1, X2) 1 + 0X1 + 0X2 >= 0 + 0X1 + 1X2 activate n__take(X1, X2) -> take(X1, X2) 1 + 0X1 + 0X2 >= 0 + 1X1 + 1X2 activate n__incr X -> incr X 1 + 0X >= 1 + 1X activate X -> X 1 + 0X >= 1X incr cons(X, XS) -> cons(s X, n__incr activate XS) 2 + 0X + 1XS >= 3 + 0X + 0XS incr X -> n__incr X 1 + 1X >= 1 + 1X pairNs() -> cons(0(), n__incr oddNs()) 1 >= 3 oddNs() -> incr pairNs() 1 >= 2 cons(X1, X2) -> n__cons(X1, X2) 1 + 0X1 + 1X2 >= 0 + 0X1 + 1X2 SCCS (0):