YES Time: 0.019725 TRS: { from X -> cons(X, n__from s X), from X -> n__from X, head cons(X, XS) -> X, activate X -> X, activate n__from X -> from X, activate n__take(X1, X2) -> take(X1, X2), 2nd cons(X, XS) -> head activate XS, take(X1, X2) -> n__take(X1, X2), take(s N, cons(X, XS)) -> cons(X, n__take(N, activate XS)), take(0(), XS) -> nil(), sel(s N, cons(X, XS)) -> sel(N, activate XS), sel(0(), cons(X, XS)) -> X} DP: DP: { activate# n__from X -> from# X, activate# n__take(X1, X2) -> take#(X1, X2), 2nd# cons(X, XS) -> head# activate XS, 2nd# cons(X, XS) -> activate# XS, take#(s N, cons(X, XS)) -> activate# XS, sel#(s N, cons(X, XS)) -> activate# XS, sel#(s N, cons(X, XS)) -> sel#(N, activate XS)} TRS: { from X -> cons(X, n__from s X), from X -> n__from X, head cons(X, XS) -> X, activate X -> X, activate n__from X -> from X, activate n__take(X1, X2) -> take(X1, X2), 2nd cons(X, XS) -> head activate XS, take(X1, X2) -> n__take(X1, X2), take(s N, cons(X, XS)) -> cons(X, n__take(N, activate XS)), take(0(), XS) -> nil(), sel(s N, cons(X, XS)) -> sel(N, activate XS), sel(0(), cons(X, XS)) -> X} UR: { from X -> cons(X, n__from s X), from X -> n__from X, activate X -> X, activate n__from X -> from X, activate n__take(X1, X2) -> take(X1, X2), take(X1, X2) -> n__take(X1, X2), take(s N, cons(X, XS)) -> cons(X, n__take(N, activate XS)), take(0(), XS) -> nil(), a(x, y) -> x, a(x, y) -> y} EDG: {(sel#(s N, cons(X, XS)) -> sel#(N, activate XS), sel#(s N, cons(X, XS)) -> sel#(N, activate XS)) (sel#(s N, cons(X, XS)) -> sel#(N, activate XS), sel#(s N, cons(X, XS)) -> activate# XS) (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__from X -> from# X) (sel#(s N, cons(X, XS)) -> activate# XS, activate# n__from X -> from# X) (sel#(s N, cons(X, XS)) -> activate# XS, activate# n__take(X1, X2) -> take#(X1, X2)) (2nd# cons(X, XS) -> activate# XS, activate# n__from X -> from# X) (2nd# cons(X, XS) -> activate# XS, activate# n__take(X1, X2) -> take#(X1, X2)) (activate# n__take(X1, X2) -> take#(X1, X2), take#(s N, cons(X, XS)) -> activate# XS)} EDG: {(sel#(s N, cons(X, XS)) -> sel#(N, activate XS), sel#(s N, cons(X, XS)) -> sel#(N, activate XS)) (sel#(s N, cons(X, XS)) -> sel#(N, activate XS), sel#(s N, cons(X, XS)) -> activate# XS) (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__from X -> from# X) (sel#(s N, cons(X, XS)) -> activate# XS, activate# n__from X -> from# X) (sel#(s N, cons(X, XS)) -> activate# XS, activate# n__take(X1, X2) -> take#(X1, X2)) (2nd# cons(X, XS) -> activate# XS, activate# n__from X -> from# X) (2nd# cons(X, XS) -> activate# XS, activate# n__take(X1, X2) -> take#(X1, X2)) (activate# n__take(X1, X2) -> take#(X1, X2), take#(s N, cons(X, XS)) -> activate# XS)} EDG: {(sel#(s N, cons(X, XS)) -> sel#(N, activate XS), sel#(s N, cons(X, XS)) -> sel#(N, activate XS)) (sel#(s N, cons(X, XS)) -> sel#(N, activate XS), sel#(s N, cons(X, XS)) -> activate# XS) (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__from X -> from# X) (sel#(s N, cons(X, XS)) -> activate# XS, activate# n__from X -> from# X) (sel#(s N, cons(X, XS)) -> activate# XS, activate# n__take(X1, X2) -> take#(X1, X2)) (2nd# cons(X, XS) -> activate# XS, activate# n__from X -> from# X) (2nd# cons(X, XS) -> activate# XS, activate# n__take(X1, X2) -> take#(X1, X2)) (activate# n__take(X1, X2) -> take#(X1, X2), take#(s N, cons(X, XS)) -> activate# XS)} EDG: {(sel#(s N, cons(X, XS)) -> sel#(N, activate XS), sel#(s N, cons(X, XS)) -> sel#(N, activate XS)) (sel#(s N, cons(X, XS)) -> sel#(N, activate XS), sel#(s N, cons(X, XS)) -> activate# XS) (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__from X -> from# X) (sel#(s N, cons(X, XS)) -> activate# XS, activate# n__from X -> from# X) (sel#(s N, cons(X, XS)) -> activate# XS, activate# n__take(X1, X2) -> take#(X1, X2)) (2nd# cons(X, XS) -> activate# XS, activate# n__from X -> from# X) (2nd# cons(X, XS) -> activate# XS, activate# n__take(X1, X2) -> take#(X1, X2)) (activate# n__take(X1, X2) -> take#(X1, X2), take#(s N, cons(X, XS)) -> activate# XS)} STATUS: arrows: 0.816327 SCCS (2): Scc: {sel#(s N, cons(X, XS)) -> sel#(N, activate XS)} Scc: {activate# n__take(X1, X2) -> take#(X1, X2), take#(s N, cons(X, XS)) -> activate# XS} SCC (1): Strict: {sel#(s N, cons(X, XS)) -> sel#(N, activate XS)} Weak: { from X -> cons(X, n__from s X), from X -> n__from X, head cons(X, XS) -> X, activate X -> X, activate n__from X -> from X, activate n__take(X1, X2) -> take(X1, X2), 2nd cons(X, XS) -> head activate XS, take(X1, X2) -> n__take(X1, X2), take(s N, cons(X, XS)) -> cons(X, n__take(N, activate XS)), take(0(), XS) -> nil(), sel(s N, cons(X, XS)) -> sel(N, activate XS), sel(0(), cons(X, XS)) -> X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = 1, [take](x0, x1) = x0 + 1, [n__take](x0, x1) = 0, [sel](x0, x1) = x0 + x1, [n__from](x0) = x0, [s](x0) = x0 + 1, [from](x0) = 0, [head](x0) = x0 + 1, [activate](x0) = 0, [2nd](x0) = x0 + 1, [nil] = 0, [0] = 1, [sel#](x0, x1) = x0 Strict: sel#(s N, cons(X, XS)) -> sel#(N, activate XS) 1 + 0X + 0XS + 1N >= 0 + 0XS + 1N Weak: sel(0(), cons(X, XS)) -> X 2 + 0X + 0XS >= 1X sel(s N, cons(X, XS)) -> sel(N, activate XS) 2 + 0X + 0XS + 1N >= 0 + 0XS + 1N take(0(), XS) -> nil() 1 + 1XS >= 0 take(s N, cons(X, XS)) -> cons(X, n__take(N, activate XS)) 2 + 0X + 0XS + 0N >= 1 + 0X + 0XS + 0N take(X1, X2) -> n__take(X1, X2) 1 + 0X1 + 1X2 >= 0 + 0X1 + 0X2 2nd cons(X, XS) -> head activate XS 2 + 0X + 0XS >= 1 + 0XS activate n__take(X1, X2) -> take(X1, X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 1X2 activate n__from X -> from X 0 + 0X >= 0 + 0X activate X -> X 0 + 0X >= 1X head cons(X, XS) -> X 2 + 0X + 0XS >= 1X from X -> n__from X 0 + 0X >= 0 + 1X from X -> cons(X, n__from s X) 0 + 0X >= 1 + 0X Qed SCC (2): Strict: {activate# n__take(X1, X2) -> take#(X1, X2), take#(s N, cons(X, XS)) -> activate# XS} Weak: { from X -> cons(X, n__from s X), from X -> n__from X, head cons(X, XS) -> X, activate X -> X, activate n__from X -> from X, activate n__take(X1, X2) -> take(X1, X2), 2nd cons(X, XS) -> head activate XS, take(X1, X2) -> n__take(X1, X2), take(s N, cons(X, XS)) -> cons(X, n__take(N, activate XS)), take(0(), XS) -> nil(), sel(s N, cons(X, XS)) -> sel(N, activate XS), sel(0(), cons(X, XS)) -> X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = x0 + 1, [take](x0, x1) = x0 + x1 + 1, [n__take](x0, x1) = x0 + 1, [sel](x0, x1) = x0, [n__from](x0) = 0, [s](x0) = 0, [from](x0) = 0, [head](x0) = x0 + 1, [activate](x0) = 0, [2nd](x0) = x0 + 1, [nil] = 0, [0] = 1, [take#](x0, x1) = x0, [activate#](x0) = x0 Strict: take#(s N, cons(X, XS)) -> activate# XS 1 + 0X + 1XS + 0N >= 0 + 1XS activate# n__take(X1, X2) -> take#(X1, X2) 1 + 0X1 + 1X2 >= 0 + 0X1 + 1X2 Weak: sel(0(), cons(X, XS)) -> X 1 + 0X + 0XS >= 1X sel(s N, cons(X, XS)) -> sel(N, activate XS) 0 + 0X + 0XS + 0N >= 0 + 0XS + 1N take(0(), XS) -> nil() 2 + 1XS >= 0 take(s N, cons(X, XS)) -> cons(X, n__take(N, activate XS)) 2 + 0X + 1XS + 0N >= 2 + 0X + 0XS + 0N take(X1, X2) -> n__take(X1, X2) 1 + 1X1 + 1X2 >= 1 + 0X1 + 1X2 2nd cons(X, XS) -> head activate XS 2 + 0X + 1XS >= 1 + 0XS activate n__take(X1, X2) -> take(X1, X2) 0 + 0X1 + 0X2 >= 1 + 1X1 + 1X2 activate n__from X -> from X 0 + 0X >= 0 + 0X activate X -> X 0 + 0X >= 1X head cons(X, XS) -> X 2 + 0X + 1XS >= 1X from X -> n__from X 0 + 0X >= 0 + 0X from X -> cons(X, n__from s X) 0 + 0X >= 1 + 0X Qed