YES Time: 0.065290 TRS: { first(X1, X2) -> n__first(X1, X2), first(0(), X) -> nil(), first(s X, cons(Y, Z)) -> cons(Y, n__first(X, activate Z)), activate X -> X, activate n__first(X1, X2) -> first(activate X1, activate X2), activate n__from X -> from activate X, activate n__s X -> s activate X, s X -> n__s X, from X -> cons(X, n__from n__s X), from X -> n__from X} DP: DP: { first#(s X, cons(Y, Z)) -> activate# Z, activate# n__first(X1, X2) -> first#(activate X1, activate X2), activate# n__first(X1, X2) -> activate# X1, activate# n__first(X1, X2) -> activate# X2, activate# n__from X -> activate# X, activate# n__from X -> from# activate X, activate# n__s X -> activate# X, activate# n__s X -> s# activate X} TRS: { first(X1, X2) -> n__first(X1, X2), first(0(), X) -> nil(), first(s X, cons(Y, Z)) -> cons(Y, n__first(X, activate Z)), activate X -> X, activate n__first(X1, X2) -> first(activate X1, activate X2), activate n__from X -> from activate X, activate n__s X -> s activate X, s X -> n__s X, from X -> cons(X, n__from n__s X), from X -> n__from X} UR: { first(X1, X2) -> n__first(X1, X2), first(0(), X) -> nil(), first(s X, cons(Y, Z)) -> cons(Y, n__first(X, activate Z)), activate X -> X, activate n__first(X1, X2) -> first(activate X1, activate X2), activate n__from X -> from activate X, activate n__s X -> s activate X, s X -> n__s X, from X -> cons(X, n__from n__s X), from X -> n__from X, a(x, y) -> x, a(x, y) -> y} EDG: {(activate# n__s X -> activate# X, activate# n__s X -> s# activate X) (activate# n__s X -> activate# X, activate# n__s X -> activate# X) (activate# n__s X -> activate# X, activate# n__from X -> from# activate X) (activate# n__s X -> activate# X, activate# n__from X -> activate# X) (activate# n__s X -> activate# X, activate# n__first(X1, X2) -> activate# X2) (activate# n__s X -> activate# X, activate# n__first(X1, X2) -> activate# X1) (activate# n__s X -> activate# X, activate# n__first(X1, X2) -> first#(activate X1, activate X2)) (activate# n__first(X1, X2) -> activate# X2, activate# n__s X -> s# activate X) (activate# n__first(X1, X2) -> activate# X2, activate# n__s X -> activate# X) (activate# n__first(X1, X2) -> activate# X2, activate# n__from X -> from# activate X) (activate# n__first(X1, X2) -> activate# X2, activate# n__from X -> activate# X) (activate# n__first(X1, X2) -> activate# X2, activate# n__first(X1, X2) -> activate# X2) (activate# n__first(X1, X2) -> activate# X2, activate# n__first(X1, X2) -> activate# X1) (activate# n__first(X1, X2) -> activate# X2, activate# n__first(X1, X2) -> first#(activate X1, activate X2)) (activate# n__first(X1, X2) -> activate# X1, activate# n__s X -> s# activate X) (activate# n__first(X1, X2) -> activate# X1, activate# n__s X -> activate# X) (activate# n__first(X1, X2) -> activate# X1, activate# n__from X -> from# activate X) (activate# n__first(X1, X2) -> activate# X1, activate# n__from X -> activate# X) (activate# n__first(X1, X2) -> activate# X1, activate# n__first(X1, X2) -> activate# X2) (activate# n__first(X1, X2) -> activate# X1, activate# n__first(X1, X2) -> activate# X1) (activate# n__first(X1, X2) -> activate# X1, activate# n__first(X1, X2) -> first#(activate X1, activate X2)) (activate# n__first(X1, X2) -> first#(activate X1, activate X2), first#(s X, cons(Y, Z)) -> activate# Z) (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__first(X1, X2) -> first#(activate X1, activate X2)) (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__first(X1, X2) -> activate# X1) (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__first(X1, X2) -> activate# X2) (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__from X -> activate# X) (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__from X -> from# activate X) (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__s X -> activate# X) (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__s X -> s# activate X) (activate# n__from X -> activate# X, activate# n__first(X1, X2) -> first#(activate X1, activate X2)) (activate# n__from X -> activate# X, activate# n__first(X1, X2) -> activate# X1) (activate# n__from X -> activate# X, activate# n__first(X1, X2) -> activate# X2) (activate# n__from X -> activate# X, activate# n__from X -> activate# X) (activate# n__from X -> activate# X, activate# n__from X -> from# activate X) (activate# n__from X -> activate# X, activate# n__s X -> activate# X) (activate# n__from X -> activate# X, activate# n__s X -> s# activate X)} STATUS: arrows: 0.437500 SCCS (1): Scc: { first#(s X, cons(Y, Z)) -> activate# Z, activate# n__first(X1, X2) -> first#(activate X1, activate X2), activate# n__first(X1, X2) -> activate# X1, activate# n__first(X1, X2) -> activate# X2, activate# n__from X -> activate# X, activate# n__s X -> activate# X} SCC (6): Strict: { first#(s X, cons(Y, Z)) -> activate# Z, activate# n__first(X1, X2) -> first#(activate X1, activate X2), activate# n__first(X1, X2) -> activate# X1, activate# n__first(X1, X2) -> activate# X2, activate# n__from X -> activate# X, activate# n__s X -> activate# X} Weak: { first(X1, X2) -> n__first(X1, X2), first(0(), X) -> nil(), first(s X, cons(Y, Z)) -> cons(Y, n__first(X, activate Z)), activate X -> X, activate n__first(X1, X2) -> first(activate X1, activate X2), activate n__from X -> from activate X, activate n__s X -> s activate X, s X -> n__s X, from X -> cons(X, n__from n__s X), from X -> n__from X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [first](x0, x1) = x0 + x1 + 1, [cons](x0, x1) = x0, [n__first](x0, x1) = x0 + x1 + 1, [activate](x0) = x0, [s](x0) = x0, [n__from](x0) = x0, [n__s](x0) = x0, [from](x0) = x0, [nil] = 0, [0] = 1, [first#](x0, x1) = x0, [activate#](x0) = x0 Strict: activate# n__s X -> activate# X 0 + 1X >= 0 + 1X activate# n__from X -> activate# X 0 + 1X >= 0 + 1X activate# n__first(X1, X2) -> activate# X2 1 + 1X1 + 1X2 >= 0 + 1X2 activate# n__first(X1, X2) -> activate# X1 1 + 1X1 + 1X2 >= 0 + 1X1 activate# n__first(X1, X2) -> first#(activate X1, activate X2) 1 + 1X1 + 1X2 >= 0 + 0X1 + 1X2 first#(s X, cons(Y, Z)) -> activate# Z 0 + 0X + 0Y + 1Z >= 0 + 1Z Weak: from X -> n__from X 0 + 1X >= 0 + 1X from X -> cons(X, n__from n__s X) 0 + 1X >= 0 + 1X s X -> n__s X 0 + 1X >= 0 + 1X activate n__s X -> s activate X 0 + 1X >= 0 + 1X activate n__from X -> from activate X 0 + 1X >= 0 + 1X activate n__first(X1, X2) -> first(activate X1, activate X2) 1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2 activate X -> X 0 + 1X >= 1X first(s X, cons(Y, Z)) -> cons(Y, n__first(X, activate Z)) 1 + 1X + 0Y + 1Z >= 1 + 1X + 0Y + 1Z first(0(), X) -> nil() 2 + 1X >= 0 first(X1, X2) -> n__first(X1, X2) 1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2 SCCS (1): Scc: {activate# n__from X -> activate# X, activate# n__s X -> activate# X} SCC (2): Strict: {activate# n__from X -> activate# X, activate# n__s X -> activate# X} Weak: { first(X1, X2) -> n__first(X1, X2), first(0(), X) -> nil(), first(s X, cons(Y, Z)) -> cons(Y, n__first(X, activate Z)), activate X -> X, activate n__first(X1, X2) -> first(activate X1, activate X2), activate n__from X -> from activate X, activate n__s X -> s activate X, s X -> n__s X, from X -> cons(X, n__from n__s X), from X -> n__from X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [first](x0, x1) = 0, [cons](x0, x1) = x0, [n__first](x0, x1) = x0 + 1, [activate](x0) = x0 + 1, [s](x0) = 0, [n__from](x0) = x0, [n__s](x0) = x0 + 1, [from](x0) = x0 + 1, [nil] = 0, [0] = 0, [activate#](x0) = x0 Strict: activate# n__s X -> activate# X 1 + 1X >= 0 + 1X activate# n__from X -> activate# X 0 + 1X >= 0 + 1X Weak: from X -> n__from X 1 + 1X >= 0 + 1X from X -> cons(X, n__from n__s X) 1 + 1X >= 1 + 1X s X -> n__s X 0 + 0X >= 1 + 1X activate n__s X -> s activate X 2 + 1X >= 0 + 0X activate n__from X -> from activate X 1 + 1X >= 2 + 1X activate n__first(X1, X2) -> first(activate X1, activate X2) 2 + 0X1 + 1X2 >= 0 + 0X1 + 0X2 activate X -> X 1 + 1X >= 1X first(s X, cons(Y, Z)) -> cons(Y, n__first(X, activate Z)) 0 + 0X + 0Y + 0Z >= 2 + 0X + 0Y + 1Z first(0(), X) -> nil() 0 + 0X >= 0 first(X1, X2) -> n__first(X1, X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 1X2 SCCS (1): Scc: {activate# n__from X -> activate# X} SCC (1): Strict: {activate# n__from X -> activate# X} Weak: { first(X1, X2) -> n__first(X1, X2), first(0(), X) -> nil(), first(s X, cons(Y, Z)) -> cons(Y, n__first(X, activate Z)), activate X -> X, activate n__first(X1, X2) -> first(activate X1, activate X2), activate n__from X -> from activate X, activate n__s X -> s activate X, s X -> n__s X, from X -> cons(X, n__from n__s X), from X -> n__from X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [first](x0, x1) = x0 + x1, [cons](x0, x1) = x0 + 1, [n__first](x0, x1) = x0 + 1, [activate](x0) = x0 + 1, [s](x0) = 1, [n__from](x0) = x0 + 1, [n__s](x0) = 1, [from](x0) = x0 + 1, [nil] = 0, [0] = 0, [activate#](x0) = x0 Strict: activate# n__from X -> activate# X 1 + 1X >= 0 + 1X Weak: from X -> n__from X 1 + 1X >= 1 + 1X from X -> cons(X, n__from n__s X) 1 + 1X >= 3 + 0X s X -> n__s X 1 + 0X >= 1 + 0X activate n__s X -> s activate X 2 + 0X >= 1 + 0X activate n__from X -> from activate X 2 + 1X >= 2 + 1X activate n__first(X1, X2) -> first(activate X1, activate X2) 2 + 0X1 + 1X2 >= 2 + 1X1 + 1X2 activate X -> X 1 + 1X >= 1X first(s X, cons(Y, Z)) -> cons(Y, n__first(X, activate Z)) 2 + 0X + 0Y + 1Z >= 3 + 0X + 0Y + 1Z first(0(), X) -> nil() 0 + 1X >= 0 first(X1, X2) -> n__first(X1, X2) 0 + 1X1 + 1X2 >= 1 + 0X1 + 1X2 Qed