YES Time: 0.041537 TRS: { from X -> cons(X, n__from n__s X), from X -> n__from X, first(X1, X2) -> n__first(X1, X2), first(0(), Z) -> nil(), first(s X, cons(Y, Z)) -> cons(Y, n__first(X, activate Z)), activate X -> X, activate n__from X -> from activate X, activate n__s X -> s activate X, activate n__first(X1, X2) -> first(activate X1, activate X2), s X -> n__s X, sel(0(), cons(X, Z)) -> X, sel(s X, cons(Y, Z)) -> sel(X, activate Z)} DP: DP: { first#(s X, cons(Y, Z)) -> activate# Z, activate# n__from X -> from# activate X, activate# n__from X -> activate# X, activate# n__s X -> activate# X, activate# n__s X -> s# activate X, activate# n__first(X1, X2) -> first#(activate X1, activate X2), activate# n__first(X1, X2) -> activate# X1, activate# n__first(X1, X2) -> activate# X2, sel#(s X, cons(Y, Z)) -> activate# Z, sel#(s X, cons(Y, Z)) -> sel#(X, activate Z)} TRS: { from X -> cons(X, n__from n__s X), from X -> n__from X, first(X1, X2) -> n__first(X1, X2), first(0(), Z) -> nil(), first(s X, cons(Y, Z)) -> cons(Y, n__first(X, activate Z)), activate X -> X, activate n__from X -> from activate X, activate n__s X -> s activate X, activate n__first(X1, X2) -> first(activate X1, activate X2), s X -> n__s X, sel(0(), cons(X, Z)) -> X, sel(s X, cons(Y, Z)) -> sel(X, activate Z)} UR: { from X -> cons(X, n__from n__s X), from X -> n__from X, first(X1, X2) -> n__first(X1, X2), first(0(), Z) -> nil(), first(s X, cons(Y, Z)) -> cons(Y, n__first(X, activate Z)), activate X -> X, activate n__from X -> from activate X, activate n__s X -> s activate X, activate n__first(X1, X2) -> first(activate X1, activate X2), s X -> n__s X, a(x, y) -> x, a(x, y) -> y} EDG: {(sel#(s X, cons(Y, Z)) -> activate# Z, activate# n__first(X1, X2) -> activate# X2) (sel#(s X, cons(Y, Z)) -> activate# Z, activate# n__first(X1, X2) -> activate# X1) (sel#(s X, cons(Y, Z)) -> activate# Z, activate# n__first(X1, X2) -> first#(activate X1, activate X2)) (sel#(s X, cons(Y, Z)) -> activate# Z, activate# n__s X -> s# activate X) (sel#(s X, cons(Y, Z)) -> activate# Z, activate# n__s X -> activate# X) (sel#(s X, cons(Y, Z)) -> activate# Z, activate# n__from X -> activate# X) (sel#(s X, cons(Y, Z)) -> activate# Z, activate# n__from X -> from# 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# 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 -> activate# X) (activate# n__first(X1, X2) -> activate# X2, activate# n__from X -> from# activate X) (sel#(s X, cons(Y, Z)) -> sel#(X, activate Z), sel#(s X, cons(Y, Z)) -> sel#(X, activate Z)) (sel#(s X, cons(Y, Z)) -> sel#(X, activate Z), sel#(s X, cons(Y, Z)) -> activate# Z) (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__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 -> activate# X) (activate# n__s X -> activate# X, activate# n__from X -> from# activate X) (activate# n__from X -> activate# X, activate# n__from X -> from# activate X) (activate# n__from X -> activate# X, activate# n__from X -> 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) (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__first(X1, X2) -> first#(activate X1, activate X2), first#(s X, cons(Y, Z)) -> activate# Z) (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__s X -> activate# X) (activate# n__first(X1, X2) -> activate# X1, activate# n__s X -> s# activate X) (activate# n__first(X1, X2) -> activate# X1, activate# n__first(X1, X2) -> first#(activate X1, 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) -> activate# X2) (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__from X -> 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) (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)} STATUS: arrows: 0.550000 SCCS (2): Scc: {sel#(s X, cons(Y, Z)) -> sel#(X, activate Z)} Scc: { first#(s X, cons(Y, Z)) -> activate# Z, activate# n__from X -> activate# X, activate# n__s X -> activate# X, activate# n__first(X1, X2) -> first#(activate X1, activate X2), activate# n__first(X1, X2) -> activate# X1, activate# n__first(X1, X2) -> activate# X2} SCC (1): Strict: {sel#(s X, cons(Y, Z)) -> sel#(X, activate Z)} Weak: { from X -> cons(X, n__from n__s X), from X -> n__from X, first(X1, X2) -> n__first(X1, X2), first(0(), Z) -> nil(), first(s X, cons(Y, Z)) -> cons(Y, n__first(X, activate Z)), activate X -> X, activate n__from X -> from activate X, activate n__s X -> s activate X, activate n__first(X1, X2) -> first(activate X1, activate X2), s X -> n__s X, sel(0(), cons(X, Z)) -> X, sel(s X, cons(Y, Z)) -> sel(X, activate Z)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = 0, [first](x0, x1) = x0 + 1, [n__first](x0, x1) = 0, [sel](x0, x1) = 0, [n__from](x0) = x0 + 1, [n__s](x0) = 1, [from](x0) = x0 + 1, [activate](x0) = x0 + 1, [s](x0) = x0 + 1, [nil] = 0, [0] = 0, [sel#](x0, x1) = x0 Strict: sel#(s X, cons(Y, Z)) -> sel#(X, activate Z) 1 + 1X + 0Z + 0Y >= 0 + 1X + 0Z Weak: sel(s X, cons(Y, Z)) -> sel(X, activate Z) 0 + 0X + 0Z + 0Y >= 0 + 0X + 0Z sel(0(), cons(X, Z)) -> X 0 + 0X + 0Z >= 1X s X -> n__s X 1 + 1X >= 1 + 0X activate n__first(X1, X2) -> first(activate X1, activate X2) 1 + 0X1 + 0X2 >= 2 + 1X1 + 0X2 activate n__s X -> s activate X 2 + 0X >= 2 + 1X activate n__from X -> from activate X 2 + 1X >= 2 + 1X activate X -> X 1 + 1X >= 1X first(s X, cons(Y, Z)) -> cons(Y, n__first(X, activate Z)) 2 + 1X + 0Z + 0Y >= 0 + 0X + 0Z + 0Y first(0(), Z) -> nil() 1 + 0Z >= 0 first(X1, X2) -> n__first(X1, X2) 1 + 1X1 + 0X2 >= 0 + 0X1 + 0X2 from X -> n__from X 1 + 1X >= 1 + 1X from X -> cons(X, n__from n__s X) 1 + 1X >= 0 + 0X Qed SCC (6): Strict: { first#(s X, cons(Y, Z)) -> activate# Z, activate# n__from X -> activate# X, activate# n__s X -> activate# X, activate# n__first(X1, X2) -> first#(activate X1, activate X2), activate# n__first(X1, X2) -> activate# X1, activate# n__first(X1, X2) -> activate# X2} Weak: { from X -> cons(X, n__from n__s X), from X -> n__from X, first(X1, X2) -> n__first(X1, X2), first(0(), Z) -> nil(), first(s X, cons(Y, Z)) -> cons(Y, n__first(X, activate Z)), activate X -> X, activate n__from X -> from activate X, activate n__s X -> s activate X, activate n__first(X1, X2) -> first(activate X1, activate X2), s X -> n__s X, sel(0(), cons(X, Z)) -> X, sel(s X, cons(Y, Z)) -> sel(X, activate Z)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = x0, [first](x0, x1) = x0 + x1 + 1, [n__first](x0, x1) = x0 + x1 + 1, [sel](x0, x1) = 1, [n__from](x0) = x0, [n__s](x0) = x0, [from](x0) = x0, [activate](x0) = x0, [s](x0) = x0, [nil] = 0, [0] = 1, [first#](x0, x1) = x0, [activate#](x0) = x0 Strict: 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 activate# n__s X -> activate# X 0 + 1X >= 0 + 1X activate# n__from X -> activate# X 0 + 1X >= 0 + 1X first#(s X, cons(Y, Z)) -> activate# Z 0 + 0X + 1Z + 0Y >= 0 + 1Z Weak: sel(s X, cons(Y, Z)) -> sel(X, activate Z) 1 + 0X + 0Z + 0Y >= 1 + 0X + 0Z sel(0(), cons(X, Z)) -> X 1 + 0X + 0Z >= 1X s X -> n__s X 0 + 1X >= 0 + 1X activate n__first(X1, X2) -> first(activate X1, activate X2) 1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2 activate n__s X -> s activate X 0 + 1X >= 0 + 1X activate n__from X -> from activate X 0 + 1X >= 0 + 1X activate X -> X 0 + 1X >= 1X first(s X, cons(Y, Z)) -> cons(Y, n__first(X, activate Z)) 1 + 1X + 1Z + 0Y >= 1 + 1X + 1Z + 0Y first(0(), Z) -> nil() 2 + 1Z >= 0 first(X1, X2) -> n__first(X1, X2) 1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2 from X -> n__from X 0 + 1X >= 0 + 1X from X -> cons(X, n__from n__s X) 0 + 1X >= 0 + 1X 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: { from X -> cons(X, n__from n__s X), from X -> n__from X, first(X1, X2) -> n__first(X1, X2), first(0(), Z) -> nil(), first(s X, cons(Y, Z)) -> cons(Y, n__first(X, activate Z)), activate X -> X, activate n__from X -> from activate X, activate n__s X -> s activate X, activate n__first(X1, X2) -> first(activate X1, activate X2), s X -> n__s X, sel(0(), cons(X, Z)) -> X, sel(s X, cons(Y, Z)) -> sel(X, activate Z)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = 0, [first](x0, x1) = x0 + 1, [n__first](x0, x1) = x0 + 1, [sel](x0, x1) = 0, [n__from](x0) = x0, [n__s](x0) = x0 + 1, [from](x0) = x0 + 1, [activate](x0) = 1, [s](x0) = 1, [nil] = 0, [0] = 1, [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: sel(s X, cons(Y, Z)) -> sel(X, activate Z) 0 + 0X + 0Z + 0Y >= 0 + 0X + 0Z sel(0(), cons(X, Z)) -> X 0 + 0X + 0Z >= 1X s X -> n__s X 1 + 0X >= 1 + 1X activate n__first(X1, X2) -> first(activate X1, activate X2) 1 + 0X1 + 0X2 >= 2 + 0X1 + 0X2 activate n__s X -> s activate X 1 + 0X >= 1 + 0X activate n__from X -> from activate X 1 + 0X >= 2 + 0X activate X -> X 1 + 0X >= 1X first(s X, cons(Y, Z)) -> cons(Y, n__first(X, activate Z)) 2 + 0X + 0Z + 0Y >= 0 + 0X + 0Z + 0Y first(0(), Z) -> nil() 2 + 0Z >= 0 first(X1, X2) -> n__first(X1, X2) 1 + 1X1 + 0X2 >= 1 + 0X1 + 1X2 from X -> n__from X 1 + 1X >= 0 + 1X from X -> cons(X, n__from n__s X) 1 + 1X >= 0 + 0X SCCS (1): Scc: {activate# n__from X -> activate# X} SCC (1): Strict: {activate# n__from X -> activate# X} Weak: { from X -> cons(X, n__from n__s X), from X -> n__from X, first(X1, X2) -> n__first(X1, X2), first(0(), Z) -> nil(), first(s X, cons(Y, Z)) -> cons(Y, n__first(X, activate Z)), activate X -> X, activate n__from X -> from activate X, activate n__s X -> s activate X, activate n__first(X1, X2) -> first(activate X1, activate X2), s X -> n__s X, sel(0(), cons(X, Z)) -> X, sel(s X, cons(Y, Z)) -> sel(X, activate Z)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = 0, [first](x0, x1) = x0 + 1, [n__first](x0, x1) = x0 + 1, [sel](x0, x1) = 0, [n__from](x0) = x0 + 1, [n__s](x0) = 1, [from](x0) = 0, [activate](x0) = x0 + 1, [s](x0) = 1, [nil] = 0, [0] = 1, [activate#](x0) = x0 Strict: activate# n__from X -> activate# X 1 + 1X >= 0 + 1X Weak: sel(s X, cons(Y, Z)) -> sel(X, activate Z) 0 + 0X + 0Z + 0Y >= 0 + 0X + 0Z sel(0(), cons(X, Z)) -> X 0 + 0X + 0Z >= 1X s X -> n__s X 1 + 0X >= 1 + 0X activate n__first(X1, X2) -> first(activate X1, activate X2) 2 + 0X1 + 1X2 >= 2 + 1X1 + 0X2 activate n__s X -> s activate X 2 + 0X >= 1 + 0X activate n__from X -> from activate X 2 + 1X >= 0 + 0X activate X -> X 1 + 1X >= 1X first(s X, cons(Y, Z)) -> cons(Y, n__first(X, activate Z)) 2 + 0X + 0Z + 0Y >= 0 + 0X + 0Z + 0Y first(0(), Z) -> nil() 2 + 0Z >= 0 first(X1, X2) -> n__first(X1, X2) 1 + 1X1 + 0X2 >= 1 + 0X1 + 1X2 from X -> n__from X 0 + 0X >= 1 + 1X from X -> cons(X, n__from n__s X) 0 + 0X >= 0 + 0X Qed