YES Time: 0.018639 TRS: { activate X -> X, activate n__cons(X1, X2) -> cons(activate X1, X2), activate n__from X -> from activate X, activate n__s X -> s activate X, 2nd cons(X, n__cons(Y, Z)) -> activate Y, cons(X1, X2) -> n__cons(X1, X2), from X -> cons(X, n__from n__s X), from X -> n__from X, s X -> n__s X} DP: DP: { activate# n__cons(X1, X2) -> activate# X1, activate# n__cons(X1, X2) -> cons#(activate X1, 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, 2nd# cons(X, n__cons(Y, Z)) -> activate# Y, from# X -> cons#(X, n__from n__s X)} TRS: { activate X -> X, activate n__cons(X1, X2) -> cons(activate X1, X2), activate n__from X -> from activate X, activate n__s X -> s activate X, 2nd cons(X, n__cons(Y, Z)) -> activate Y, cons(X1, X2) -> n__cons(X1, X2), from X -> cons(X, n__from n__s X), from X -> n__from X, s X -> n__s X} UR: { activate X -> X, activate n__cons(X1, X2) -> cons(activate X1, X2), activate n__from X -> from activate X, activate n__s X -> s activate X, cons(X1, X2) -> n__cons(X1, X2), from X -> cons(X, n__from n__s X), from X -> n__from X, s X -> n__s X, a(x, y) -> x, a(x, y) -> y} EDG: {(2nd# cons(X, n__cons(Y, Z)) -> activate# Y, activate# n__s X -> s# activate X) (2nd# cons(X, n__cons(Y, Z)) -> activate# Y, activate# n__s X -> activate# X) (2nd# cons(X, n__cons(Y, Z)) -> activate# Y, activate# n__from X -> from# activate X) (2nd# cons(X, n__cons(Y, Z)) -> activate# Y, activate# n__from X -> activate# X) (2nd# cons(X, n__cons(Y, Z)) -> activate# Y, activate# n__cons(X1, X2) -> cons#(activate X1, X2)) (2nd# cons(X, n__cons(Y, Z)) -> activate# Y, activate# n__cons(X1, X2) -> activate# X1) (activate# n__from X -> activate# X, activate# n__s X -> s# activate X) (activate# n__from X -> activate# X, activate# n__s X -> 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__cons(X1, X2) -> cons#(activate X1, X2)) (activate# n__from X -> activate# X, activate# n__cons(X1, X2) -> activate# X1) (activate# n__cons(X1, X2) -> activate# X1, activate# n__s X -> s# activate X) (activate# n__cons(X1, X2) -> activate# X1, activate# n__s X -> activate# X) (activate# n__cons(X1, X2) -> activate# X1, activate# n__from X -> from# activate X) (activate# n__cons(X1, X2) -> activate# X1, activate# n__from X -> activate# X) (activate# n__cons(X1, X2) -> activate# X1, activate# n__cons(X1, X2) -> cons#(activate X1, X2)) (activate# n__cons(X1, X2) -> activate# X1, activate# n__cons(X1, X2) -> activate# X1) (activate# n__s X -> activate# X, activate# n__cons(X1, X2) -> activate# X1) (activate# n__s X -> activate# X, activate# n__cons(X1, X2) -> cons#(activate X1, X2)) (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__s X -> activate# X, activate# n__s X -> activate# X) (activate# n__s X -> activate# X, activate# n__s X -> s# activate X) (activate# n__from X -> from# activate X, from# X -> cons#(X, n__from n__s X))} STATUS: arrows: 0.609375 SCCS (1): Scc: {activate# n__cons(X1, X2) -> activate# X1, activate# n__from X -> activate# X, activate# n__s X -> activate# X} SCC (3): Strict: {activate# n__cons(X1, X2) -> activate# X1, activate# n__from X -> activate# X, activate# n__s X -> activate# X} Weak: { activate X -> X, activate n__cons(X1, X2) -> cons(activate X1, X2), activate n__from X -> from activate X, activate n__s X -> s activate X, 2nd cons(X, n__cons(Y, Z)) -> activate Y, cons(X1, X2) -> n__cons(X1, X2), from X -> cons(X, n__from n__s X), from X -> n__from X, s X -> n__s X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = 0, [n__cons](x0, x1) = x0, [activate](x0) = 0, [2nd](x0) = 0, [n__from](x0) = x0, [n__s](x0) = x0 + 1, [from](x0) = 0, [s](x0) = 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 activate# n__cons(X1, X2) -> activate# X1 0 + 1X1 + 0X2 >= 0 + 1X1 Weak: s X -> n__s X 0 + 0X >= 1 + 1X from X -> n__from X 0 + 0X >= 0 + 1X from X -> cons(X, n__from n__s X) 0 + 0X >= 0 + 0X cons(X1, X2) -> n__cons(X1, X2) 0 + 0X1 + 0X2 >= 0 + 1X1 + 0X2 2nd cons(X, n__cons(Y, Z)) -> activate Y 0 + 0Y + 0X + 0Z >= 0 + 0Y activate n__s X -> s activate X 0 + 0X >= 0 + 0X activate n__from X -> from activate X 0 + 0X >= 0 + 0X activate n__cons(X1, X2) -> cons(activate X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 activate X -> X 0 + 0X >= 1X SCCS (1): Scc: {activate# n__cons(X1, X2) -> activate# X1, activate# n__from X -> activate# X} SCC (2): Strict: {activate# n__cons(X1, X2) -> activate# X1, activate# n__from X -> activate# X} Weak: { activate X -> X, activate n__cons(X1, X2) -> cons(activate X1, X2), activate n__from X -> from activate X, activate n__s X -> s activate X, 2nd cons(X, n__cons(Y, Z)) -> activate Y, cons(X1, X2) -> n__cons(X1, X2), from X -> cons(X, n__from n__s X), from X -> n__from X, s X -> n__s X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = 0, [n__cons](x0, x1) = x0, [activate](x0) = 0, [2nd](x0) = 0, [n__from](x0) = x0 + 1, [n__s](x0) = 0, [from](x0) = 0, [s](x0) = 0, [activate#](x0) = x0 Strict: activate# n__from X -> activate# X 1 + 1X >= 0 + 1X activate# n__cons(X1, X2) -> activate# X1 0 + 1X1 + 0X2 >= 0 + 1X1 Weak: s X -> n__s X 0 + 0X >= 0 + 0X from X -> n__from X 0 + 0X >= 1 + 1X from X -> cons(X, n__from n__s X) 0 + 0X >= 0 + 0X cons(X1, X2) -> n__cons(X1, X2) 0 + 0X1 + 0X2 >= 0 + 1X1 + 0X2 2nd cons(X, n__cons(Y, Z)) -> activate Y 0 + 0Y + 0X + 0Z >= 0 + 0Y activate n__s X -> s activate X 0 + 0X >= 0 + 0X activate n__from X -> from activate X 0 + 0X >= 0 + 0X activate n__cons(X1, X2) -> cons(activate X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 activate X -> X 0 + 0X >= 1X SCCS (1): Scc: {activate# n__cons(X1, X2) -> activate# X1} SCC (1): Strict: {activate# n__cons(X1, X2) -> activate# X1} Weak: { activate X -> X, activate n__cons(X1, X2) -> cons(activate X1, X2), activate n__from X -> from activate X, activate n__s X -> s activate X, 2nd cons(X, n__cons(Y, Z)) -> activate Y, cons(X1, X2) -> n__cons(X1, X2), from X -> cons(X, n__from n__s X), from X -> n__from X, s X -> n__s X} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = x0 + x1 + 1, [n__cons](x0, x1) = x0 + 1, [activate](x0) = x0 + 1, [2nd](x0) = 0, [n__from](x0) = 1, [n__s](x0) = 1, [from](x0) = x0 + 1, [s](x0) = x0 + 1, [activate#](x0) = x0 Strict: activate# n__cons(X1, X2) -> activate# X1 1 + 1X1 + 0X2 >= 0 + 1X1 Weak: s X -> n__s X 1 + 1X >= 1 + 0X from X -> n__from X 1 + 1X >= 1 + 0X from X -> cons(X, n__from n__s X) 1 + 1X >= 2 + 1X cons(X1, X2) -> n__cons(X1, X2) 1 + 1X1 + 1X2 >= 1 + 1X1 + 0X2 2nd cons(X, n__cons(Y, Z)) -> activate Y 0 + 0Y + 0X + 0Z >= 1 + 1Y activate n__s X -> s activate X 2 + 0X >= 2 + 1X activate n__from X -> from activate X 2 + 0X >= 2 + 1X activate n__cons(X1, X2) -> cons(activate X1, X2) 2 + 1X1 + 0X2 >= 2 + 1X1 + 1X2 activate X -> X 1 + 1X >= 1X Qed