YES Time: 0.034776 TRS: { activate X -> X, activate n__add(X1, X2) -> add(X1, X2), activate n__first(X1, X2) -> first(X1, X2), activate n__from X -> from X, activate n__s X -> s X, and(true(), X) -> activate X, and(false(), Y) -> false(), if(true(), X, Y) -> activate X, if(false(), X, Y) -> activate Y, add(X1, X2) -> n__add(X1, X2), add(0(), X) -> activate X, add(s X, Y) -> s n__add(activate X, activate Y), s X -> n__s X, first(X1, X2) -> n__first(X1, X2), first(0(), X) -> nil(), first(s X, cons(Y, Z)) -> cons(activate Y, n__first(activate X, activate Z)), from X -> cons(activate X, n__from n__s activate X), from X -> n__from X} DP: DP: { activate# n__add(X1, X2) -> add#(X1, X2), activate# n__first(X1, X2) -> first#(X1, X2), activate# n__from X -> from# X, activate# n__s X -> s# X, and#(true(), X) -> activate# X, if#(true(), X, Y) -> activate# X, if#(false(), X, Y) -> activate# Y, add#(0(), X) -> activate# X, add#(s X, Y) -> activate# X, add#(s X, Y) -> activate# Y, add#(s X, Y) -> s# n__add(activate X, activate Y), first#(s X, cons(Y, Z)) -> activate# X, first#(s X, cons(Y, Z)) -> activate# Y, first#(s X, cons(Y, Z)) -> activate# Z, from# X -> activate# X} TRS: { activate X -> X, activate n__add(X1, X2) -> add(X1, X2), activate n__first(X1, X2) -> first(X1, X2), activate n__from X -> from X, activate n__s X -> s X, and(true(), X) -> activate X, and(false(), Y) -> false(), if(true(), X, Y) -> activate X, if(false(), X, Y) -> activate Y, add(X1, X2) -> n__add(X1, X2), add(0(), X) -> activate X, add(s X, Y) -> s n__add(activate X, activate Y), s X -> n__s X, first(X1, X2) -> n__first(X1, X2), first(0(), X) -> nil(), first(s X, cons(Y, Z)) -> cons(activate Y, n__first(activate X, activate Z)), from X -> cons(activate X, n__from n__s activate X), from X -> n__from X} UR: { activate X -> X, activate n__add(X1, X2) -> add(X1, X2), activate n__first(X1, X2) -> first(X1, X2), activate n__from X -> from X, activate n__s X -> s X, add(X1, X2) -> n__add(X1, X2), add(0(), X) -> activate X, add(s X, Y) -> s n__add(activate X, activate Y), s X -> n__s X, first(X1, X2) -> n__first(X1, X2), first(0(), X) -> nil(), first(s X, cons(Y, Z)) -> cons(activate Y, n__first(activate X, activate Z)), from X -> cons(activate X, n__from n__s activate X), from X -> n__from X, a(x, y) -> x, a(x, y) -> y} EDG: {(add#(s X, Y) -> activate# Y, activate# n__s X -> s# X) (add#(s X, Y) -> activate# Y, activate# n__from X -> from# X) (add#(s X, Y) -> activate# Y, activate# n__first(X1, X2) -> first#(X1, X2)) (add#(s X, Y) -> activate# Y, activate# n__add(X1, X2) -> add#(X1, X2)) (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__s X -> s# X) (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__from X -> from# X) (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__first(X1, X2) -> first#(X1, X2)) (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__add(X1, X2) -> add#(X1, X2)) (activate# n__first(X1, X2) -> first#(X1, X2), first#(s X, cons(Y, Z)) -> activate# Z) (activate# n__first(X1, X2) -> first#(X1, X2), first#(s X, cons(Y, Z)) -> activate# Y) (activate# n__first(X1, X2) -> first#(X1, X2), first#(s X, cons(Y, Z)) -> activate# X) (if#(true(), X, Y) -> activate# X, activate# n__s X -> s# X) (if#(true(), X, Y) -> activate# X, activate# n__from X -> from# X) (if#(true(), X, Y) -> activate# X, activate# n__first(X1, X2) -> first#(X1, X2)) (if#(true(), X, Y) -> activate# X, activate# n__add(X1, X2) -> add#(X1, X2)) (add#(s X, Y) -> activate# X, activate# n__s X -> s# X) (add#(s X, Y) -> activate# X, activate# n__from X -> from# X) (add#(s X, Y) -> activate# X, activate# n__first(X1, X2) -> first#(X1, X2)) (add#(s X, Y) -> activate# X, activate# n__add(X1, X2) -> add#(X1, X2)) (from# X -> activate# X, activate# n__s X -> s# X) (from# X -> activate# X, activate# n__from X -> from# X) (from# X -> activate# X, activate# n__first(X1, X2) -> first#(X1, X2)) (from# X -> activate# X, activate# n__add(X1, X2) -> add#(X1, X2)) (first#(s X, cons(Y, Z)) -> activate# X, activate# n__add(X1, X2) -> add#(X1, X2)) (first#(s X, cons(Y, Z)) -> activate# X, activate# n__first(X1, X2) -> first#(X1, X2)) (first#(s X, cons(Y, Z)) -> activate# X, activate# n__from X -> from# X) (first#(s X, cons(Y, Z)) -> activate# X, activate# n__s X -> s# X) (add#(0(), X) -> activate# X, activate# n__add(X1, X2) -> add#(X1, X2)) (add#(0(), X) -> activate# X, activate# n__first(X1, X2) -> first#(X1, X2)) (add#(0(), X) -> activate# X, activate# n__from X -> from# X) (add#(0(), X) -> activate# X, activate# n__s X -> s# X) (and#(true(), X) -> activate# X, activate# n__add(X1, X2) -> add#(X1, X2)) (and#(true(), X) -> activate# X, activate# n__first(X1, X2) -> first#(X1, X2)) (and#(true(), X) -> activate# X, activate# n__from X -> from# X) (and#(true(), X) -> activate# X, activate# n__s X -> s# X) (activate# n__from X -> from# X, from# X -> activate# X) (activate# n__add(X1, X2) -> add#(X1, X2), add#(0(), X) -> activate# X) (activate# n__add(X1, X2) -> add#(X1, X2), add#(s X, Y) -> activate# X) (activate# n__add(X1, X2) -> add#(X1, X2), add#(s X, Y) -> activate# Y) (activate# n__add(X1, X2) -> add#(X1, X2), add#(s X, Y) -> s# n__add(activate X, activate Y)) (first#(s X, cons(Y, Z)) -> activate# Y, activate# n__add(X1, X2) -> add#(X1, X2)) (first#(s X, cons(Y, Z)) -> activate# Y, activate# n__first(X1, X2) -> first#(X1, X2)) (first#(s X, cons(Y, Z)) -> activate# Y, activate# n__from X -> from# X) (first#(s X, cons(Y, Z)) -> activate# Y, activate# n__s X -> s# X) (if#(false(), X, Y) -> activate# Y, activate# n__add(X1, X2) -> add#(X1, X2)) (if#(false(), X, Y) -> activate# Y, activate# n__first(X1, X2) -> first#(X1, X2)) (if#(false(), X, Y) -> activate# Y, activate# n__from X -> from# X) (if#(false(), X, Y) -> activate# Y, activate# n__s X -> s# X)} STATUS: arrows: 0.786667 SCCS (1): Scc: { activate# n__add(X1, X2) -> add#(X1, X2), activate# n__first(X1, X2) -> first#(X1, X2), activate# n__from X -> from# X, add#(0(), X) -> activate# X, add#(s X, Y) -> activate# X, add#(s X, Y) -> activate# Y, first#(s X, cons(Y, Z)) -> activate# X, first#(s X, cons(Y, Z)) -> activate# Y, first#(s X, cons(Y, Z)) -> activate# Z, from# X -> activate# X} SCC (10): Strict: { activate# n__add(X1, X2) -> add#(X1, X2), activate# n__first(X1, X2) -> first#(X1, X2), activate# n__from X -> from# X, add#(0(), X) -> activate# X, add#(s X, Y) -> activate# X, add#(s X, Y) -> activate# Y, first#(s X, cons(Y, Z)) -> activate# X, first#(s X, cons(Y, Z)) -> activate# Y, first#(s X, cons(Y, Z)) -> activate# Z, from# X -> activate# X} Weak: { activate X -> X, activate n__add(X1, X2) -> add(X1, X2), activate n__first(X1, X2) -> first(X1, X2), activate n__from X -> from X, activate n__s X -> s X, and(true(), X) -> activate X, and(false(), Y) -> false(), if(true(), X, Y) -> activate X, if(false(), X, Y) -> activate Y, add(X1, X2) -> n__add(X1, X2), add(0(), X) -> activate X, add(s X, Y) -> s n__add(activate X, activate Y), s X -> n__s X, first(X1, X2) -> n__first(X1, X2), first(0(), X) -> nil(), first(s X, cons(Y, Z)) -> cons(activate Y, n__first(activate X, activate Z)), from X -> cons(activate X, n__from n__s activate X), from X -> n__from X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2) = x0 + 1, [and](x0, x1) = x0 + 1, [add](x0, x1) = 0, [n__add](x0, x1) = x0 + x1, [first](x0, x1) = 0, [cons](x0, x1) = x0 + x1, [n__first](x0, x1) = x0 + x1, [activate](x0) = 0, [s](x0) = x0, [n__from](x0) = x0 + 1, [n__s](x0) = 0, [from](x0) = 0, [true] = 1, [false] = 1, [0] = 0, [nil] = 0, [add#](x0, x1) = x0 + x1, [first#](x0, x1) = x0 + x1, [activate#](x0) = x0, [from#](x0) = x0 + 1 Strict: from# X -> activate# X 1 + 1X >= 0 + 1X first#(s X, cons(Y, Z)) -> activate# Z 0 + 1X + 1Y + 1Z >= 0 + 1Z first#(s X, cons(Y, Z)) -> activate# Y 0 + 1X + 1Y + 1Z >= 0 + 1Y first#(s X, cons(Y, Z)) -> activate# X 0 + 1X + 1Y + 1Z >= 0 + 1X add#(s X, Y) -> activate# Y 0 + 1X + 1Y >= 0 + 1Y add#(s X, Y) -> activate# X 0 + 1X + 1Y >= 0 + 1X add#(0(), X) -> activate# X 0 + 1X >= 0 + 1X activate# n__from X -> from# X 1 + 1X >= 1 + 1X activate# n__first(X1, X2) -> first#(X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 activate# n__add(X1, X2) -> add#(X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 Weak: from X -> n__from X 0 + 0X >= 1 + 1X from X -> cons(activate X, n__from n__s activate X) 0 + 0X >= 1 + 0X first(s X, cons(Y, Z)) -> cons(activate Y, n__first(activate X, activate Z)) 0 + 0X + 0Y + 0Z >= 0 + 0X + 0Y + 0Z first(0(), X) -> nil() 0 + 0X >= 0 first(X1, X2) -> n__first(X1, X2) 0 + 0X1 + 0X2 >= 0 + 1X1 + 1X2 s X -> n__s X 0 + 1X >= 0 + 0X add(s X, Y) -> s n__add(activate X, activate Y) 0 + 0X + 0Y >= 0 + 0X + 0Y add(0(), X) -> activate X 0 + 0X >= 0 + 0X add(X1, X2) -> n__add(X1, X2) 0 + 0X1 + 0X2 >= 0 + 1X1 + 1X2 if(false(), X, Y) -> activate Y 2 + 0X + 0Y >= 0 + 0Y if(true(), X, Y) -> activate X 2 + 0X + 0Y >= 0 + 0X and(false(), Y) -> false() 2 + 0Y >= 1 and(true(), X) -> activate X 2 + 0X >= 0 + 0X activate n__s X -> s X 0 + 0X >= 0 + 1X activate n__from X -> from X 0 + 0X >= 0 + 0X activate n__first(X1, X2) -> first(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 activate n__add(X1, X2) -> add(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 activate X -> X 0 + 0X >= 1X SCCS (1): Scc: { activate# n__add(X1, X2) -> add#(X1, X2), activate# n__first(X1, X2) -> first#(X1, X2), add#(0(), X) -> activate# X, add#(s X, Y) -> activate# X, add#(s X, Y) -> activate# Y, first#(s X, cons(Y, Z)) -> activate# X, first#(s X, cons(Y, Z)) -> activate# Y, first#(s X, cons(Y, Z)) -> activate# Z} SCC (8): Strict: { activate# n__add(X1, X2) -> add#(X1, X2), activate# n__first(X1, X2) -> first#(X1, X2), add#(0(), X) -> activate# X, add#(s X, Y) -> activate# X, add#(s X, Y) -> activate# Y, first#(s X, cons(Y, Z)) -> activate# X, first#(s X, cons(Y, Z)) -> activate# Y, first#(s X, cons(Y, Z)) -> activate# Z} Weak: { activate X -> X, activate n__add(X1, X2) -> add(X1, X2), activate n__first(X1, X2) -> first(X1, X2), activate n__from X -> from X, activate n__s X -> s X, and(true(), X) -> activate X, and(false(), Y) -> false(), if(true(), X, Y) -> activate X, if(false(), X, Y) -> activate Y, add(X1, X2) -> n__add(X1, X2), add(0(), X) -> activate X, add(s X, Y) -> s n__add(activate X, activate Y), s X -> n__s X, first(X1, X2) -> n__first(X1, X2), first(0(), X) -> nil(), first(s X, cons(Y, Z)) -> cons(activate Y, n__first(activate X, activate Z)), from X -> cons(activate X, n__from n__s activate X), from X -> n__from X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2) = x0 + 1, [and](x0, x1) = x0 + 1, [add](x0, x1) = x0 + 1, [n__add](x0, x1) = x0 + x1 + 1, [first](x0, x1) = x0 + 1, [cons](x0, x1) = x0 + x1 + 1, [n__first](x0, x1) = x0 + x1 + 1, [activate](x0) = 0, [s](x0) = x0 + 1, [n__from](x0) = 0, [n__s](x0) = 0, [from](x0) = 0, [true] = 1, [false] = 1, [0] = 1, [nil] = 0, [add#](x0, x1) = x0 + x1, [first#](x0, x1) = x0 + x1, [activate#](x0) = x0 + 1 Strict: first#(s X, cons(Y, Z)) -> activate# Z 2 + 1X + 1Y + 1Z >= 1 + 1Z first#(s X, cons(Y, Z)) -> activate# Y 2 + 1X + 1Y + 1Z >= 1 + 1Y first#(s X, cons(Y, Z)) -> activate# X 2 + 1X + 1Y + 1Z >= 1 + 1X add#(s X, Y) -> activate# Y 1 + 1X + 1Y >= 1 + 1Y add#(s X, Y) -> activate# X 1 + 1X + 1Y >= 1 + 1X add#(0(), X) -> activate# X 1 + 1X >= 1 + 1X activate# n__first(X1, X2) -> first#(X1, X2) 2 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 activate# n__add(X1, X2) -> add#(X1, X2) 2 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 Weak: from X -> n__from X 0 + 0X >= 0 + 0X from X -> cons(activate X, n__from n__s activate X) 0 + 0X >= 1 + 0X first(s X, cons(Y, Z)) -> cons(activate Y, n__first(activate X, activate Z)) 2 + 0X + 1Y + 1Z >= 2 + 0X + 0Y + 0Z first(0(), X) -> nil() 1 + 1X >= 0 first(X1, X2) -> n__first(X1, X2) 1 + 0X1 + 1X2 >= 1 + 1X1 + 1X2 s X -> n__s X 1 + 1X >= 0 + 0X add(s X, Y) -> s n__add(activate X, activate Y) 2 + 1X + 0Y >= 2 + 0X + 0Y add(0(), X) -> activate X 2 + 0X >= 0 + 0X add(X1, X2) -> n__add(X1, X2) 1 + 1X1 + 0X2 >= 1 + 1X1 + 1X2 if(false(), X, Y) -> activate Y 2 + 0X + 0Y >= 0 + 0Y if(true(), X, Y) -> activate X 2 + 0X + 0Y >= 0 + 0X and(false(), Y) -> false() 2 + 0Y >= 1 and(true(), X) -> activate X 2 + 0X >= 0 + 0X activate n__s X -> s X 0 + 0X >= 1 + 1X activate n__from X -> from X 0 + 0X >= 0 + 0X activate n__first(X1, X2) -> first(X1, X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 1X2 activate n__add(X1, X2) -> add(X1, X2) 0 + 0X1 + 0X2 >= 1 + 1X1 + 0X2 activate X -> X 0 + 0X >= 1X SCCS (0):