YES Time: 0.180779 TRS: { sel(s N, cons(X, XS)) -> sel(N, activate XS), sel(0(), cons(X, XS)) -> X, fib1(X, Y) -> cons(X, n__fib1(Y, n__add(X, Y))), fib1(X1, X2) -> n__fib1(X1, X2), fib N -> sel(N, fib1(s 0(), s 0())), add(X1, X2) -> n__add(X1, X2), add(s X, Y) -> s add(X, Y), add(0(), X) -> X, activate X -> X, activate n__fib1(X1, X2) -> fib1(activate X1, activate X2), activate n__add(X1, X2) -> add(activate X1, activate X2)} DP: DP: { sel#(s N, cons(X, XS)) -> sel#(N, activate XS), sel#(s N, cons(X, XS)) -> activate# XS, fib# N -> sel#(N, fib1(s 0(), s 0())), fib# N -> fib1#(s 0(), s 0()), add#(s X, Y) -> add#(X, Y), activate# n__fib1(X1, X2) -> fib1#(activate X1, activate X2), activate# n__fib1(X1, X2) -> activate# X1, activate# n__fib1(X1, X2) -> activate# X2, activate# n__add(X1, X2) -> add#(activate X1, activate X2), activate# n__add(X1, X2) -> activate# X1, activate# n__add(X1, X2) -> activate# X2} TRS: { sel(s N, cons(X, XS)) -> sel(N, activate XS), sel(0(), cons(X, XS)) -> X, fib1(X, Y) -> cons(X, n__fib1(Y, n__add(X, Y))), fib1(X1, X2) -> n__fib1(X1, X2), fib N -> sel(N, fib1(s 0(), s 0())), add(X1, X2) -> n__add(X1, X2), add(s X, Y) -> s add(X, Y), add(0(), X) -> X, activate X -> X, activate n__fib1(X1, X2) -> fib1(activate X1, activate X2), activate n__add(X1, X2) -> add(activate X1, activate X2)} UR: { fib1(X, Y) -> cons(X, n__fib1(Y, n__add(X, Y))), fib1(X1, X2) -> n__fib1(X1, X2), add(X1, X2) -> n__add(X1, X2), add(s X, Y) -> s add(X, Y), add(0(), X) -> X, activate X -> X, activate n__fib1(X1, X2) -> fib1(activate X1, activate X2), activate n__add(X1, X2) -> add(activate X1, activate X2), a(x, y) -> x, a(x, y) -> y} EDG: {(sel#(s N, cons(X, XS)) -> activate# XS, activate# n__add(X1, X2) -> activate# X2) (sel#(s N, cons(X, XS)) -> activate# XS, activate# n__add(X1, X2) -> activate# X1) (sel#(s N, cons(X, XS)) -> activate# XS, activate# n__add(X1, X2) -> add#(activate X1, activate X2)) (sel#(s N, cons(X, XS)) -> activate# XS, activate# n__fib1(X1, X2) -> activate# X2) (sel#(s N, cons(X, XS)) -> activate# XS, activate# n__fib1(X1, X2) -> activate# X1) (sel#(s N, cons(X, XS)) -> activate# XS, activate# n__fib1(X1, X2) -> fib1#(activate X1, activate X2)) (activate# n__add(X1, X2) -> activate# X1, activate# n__add(X1, X2) -> activate# X2) (activate# n__add(X1, X2) -> activate# X1, activate# n__add(X1, X2) -> activate# X1) (activate# n__add(X1, X2) -> activate# X1, activate# n__add(X1, X2) -> add#(activate X1, activate X2)) (activate# n__add(X1, X2) -> activate# X1, activate# n__fib1(X1, X2) -> activate# X2) (activate# n__add(X1, X2) -> activate# X1, activate# n__fib1(X1, X2) -> activate# X1) (activate# n__add(X1, X2) -> activate# X1, activate# n__fib1(X1, X2) -> fib1#(activate X1, activate X2)) (activate# n__fib1(X1, X2) -> activate# X2, activate# n__add(X1, X2) -> activate# X2) (activate# n__fib1(X1, X2) -> activate# X2, activate# n__add(X1, X2) -> activate# X1) (activate# n__fib1(X1, X2) -> activate# X2, activate# n__add(X1, X2) -> add#(activate X1, activate X2)) (activate# n__fib1(X1, X2) -> activate# X2, activate# n__fib1(X1, X2) -> activate# X2) (activate# n__fib1(X1, X2) -> activate# X2, activate# n__fib1(X1, X2) -> activate# X1) (activate# n__fib1(X1, X2) -> activate# X2, activate# n__fib1(X1, X2) -> fib1#(activate X1, activate X2)) (add#(s X, Y) -> add#(X, Y), add#(s X, Y) -> add#(X, Y)) (activate# n__add(X1, X2) -> activate# X2, activate# n__fib1(X1, X2) -> fib1#(activate X1, activate X2)) (activate# n__add(X1, X2) -> activate# X2, activate# n__fib1(X1, X2) -> activate# X1) (activate# n__add(X1, X2) -> activate# X2, activate# n__fib1(X1, X2) -> activate# X2) (activate# n__add(X1, X2) -> activate# X2, activate# n__add(X1, X2) -> add#(activate X1, activate X2)) (activate# n__add(X1, X2) -> activate# X2, activate# n__add(X1, X2) -> activate# X1) (activate# n__add(X1, X2) -> activate# X2, activate# n__add(X1, X2) -> activate# X2) (fib# N -> sel#(N, fib1(s 0(), s 0())), sel#(s N, cons(X, XS)) -> sel#(N, activate XS)) (fib# N -> sel#(N, fib1(s 0(), s 0())), sel#(s N, cons(X, XS)) -> activate# XS) (activate# n__fib1(X1, X2) -> activate# X1, activate# n__fib1(X1, X2) -> fib1#(activate X1, activate X2)) (activate# n__fib1(X1, X2) -> activate# X1, activate# n__fib1(X1, X2) -> activate# X1) (activate# n__fib1(X1, X2) -> activate# X1, activate# n__fib1(X1, X2) -> activate# X2) (activate# n__fib1(X1, X2) -> activate# X1, activate# n__add(X1, X2) -> add#(activate X1, activate X2)) (activate# n__fib1(X1, X2) -> activate# X1, activate# n__add(X1, X2) -> activate# X1) (activate# n__fib1(X1, X2) -> activate# X1, activate# n__add(X1, X2) -> activate# X2) (activate# n__add(X1, X2) -> add#(activate X1, activate X2), add#(s X, Y) -> add#(X, Y)) (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)} STATUS: arrows: 0.702479 SCCS (3): Scc: {sel#(s N, cons(X, XS)) -> sel#(N, activate XS)} Scc: {activate# n__fib1(X1, X2) -> activate# X1, activate# n__fib1(X1, X2) -> activate# X2, activate# n__add(X1, X2) -> activate# X1, activate# n__add(X1, X2) -> activate# X2} Scc: {add#(s X, Y) -> add#(X, Y)} SCC (1): Strict: {sel#(s N, cons(X, XS)) -> sel#(N, activate XS)} Weak: { sel(s N, cons(X, XS)) -> sel(N, activate XS), sel(0(), cons(X, XS)) -> X, fib1(X, Y) -> cons(X, n__fib1(Y, n__add(X, Y))), fib1(X1, X2) -> n__fib1(X1, X2), fib N -> sel(N, fib1(s 0(), s 0())), add(X1, X2) -> n__add(X1, X2), add(s X, Y) -> s add(X, Y), add(0(), X) -> X, activate X -> X, activate n__fib1(X1, X2) -> fib1(activate X1, activate X2), activate n__add(X1, X2) -> add(activate X1, activate X2)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [sel](x0, x1) = 0, [fib1](x0, x1) = x0 + x1, [cons](x0, x1) = x0, [n__fib1](x0, x1) = x0, [n__add](x0, x1) = 1, [add](x0, x1) = 0, [s](x0) = x0 + 1, [fib](x0) = 0, [activate](x0) = 0, [0] = 0, [sel#](x0, x1) = x0 Strict: sel#(s N, cons(X, XS)) -> sel#(N, activate XS) 1 + 1N + 0X + 0XS >= 0 + 1N + 0XS Weak: activate n__add(X1, X2) -> add(activate X1, activate X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 activate n__fib1(X1, X2) -> fib1(activate X1, activate X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 activate X -> X 0 + 0X >= 1X add(0(), X) -> X 0 + 0X >= 1X add(s X, Y) -> s add(X, Y) 0 + 0X + 0Y >= 1 + 0X + 0Y add(X1, X2) -> n__add(X1, X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 fib N -> sel(N, fib1(s 0(), s 0())) 0 + 0N >= 0 + 0N fib1(X1, X2) -> n__fib1(X1, X2) 0 + 1X1 + 1X2 >= 0 + 0X1 + 1X2 fib1(X, Y) -> cons(X, n__fib1(Y, n__add(X, Y))) 0 + 1X + 1Y >= 1 + 0X + 0Y sel(0(), cons(X, XS)) -> X 0 + 0X + 0XS >= 1X sel(s N, cons(X, XS)) -> sel(N, activate XS) 0 + 0N + 0X + 0XS >= 0 + 0N + 0XS Qed SCC (4): Strict: {activate# n__fib1(X1, X2) -> activate# X1, activate# n__fib1(X1, X2) -> activate# X2, activate# n__add(X1, X2) -> activate# X1, activate# n__add(X1, X2) -> activate# X2} Weak: { sel(s N, cons(X, XS)) -> sel(N, activate XS), sel(0(), cons(X, XS)) -> X, fib1(X, Y) -> cons(X, n__fib1(Y, n__add(X, Y))), fib1(X1, X2) -> n__fib1(X1, X2), fib N -> sel(N, fib1(s 0(), s 0())), add(X1, X2) -> n__add(X1, X2), add(s X, Y) -> s add(X, Y), add(0(), X) -> X, activate X -> X, activate n__fib1(X1, X2) -> fib1(activate X1, activate X2), activate n__add(X1, X2) -> add(activate X1, activate X2)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [sel](x0, x1) = x0 + 1, [fib1](x0, x1) = x0 + 1, [cons](x0, x1) = 1, [n__fib1](x0, x1) = x0 + x1, [n__add](x0, x1) = x0 + x1 + 1, [add](x0, x1) = 0, [s](x0) = x0 + 1, [fib](x0) = 0, [activate](x0) = 1, [0] = 1, [activate#](x0) = x0 Strict: activate# n__add(X1, X2) -> activate# X2 1 + 1X1 + 1X2 >= 0 + 1X2 activate# n__add(X1, X2) -> activate# X1 1 + 1X1 + 1X2 >= 0 + 1X1 activate# n__fib1(X1, X2) -> activate# X2 0 + 1X1 + 1X2 >= 0 + 1X2 activate# n__fib1(X1, X2) -> activate# X1 0 + 1X1 + 1X2 >= 0 + 1X1 Weak: activate n__add(X1, X2) -> add(activate X1, activate X2) 1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 activate n__fib1(X1, X2) -> fib1(activate X1, activate X2) 1 + 0X1 + 0X2 >= 2 + 0X1 + 0X2 activate X -> X 1 + 0X >= 1X add(0(), X) -> X 0 + 0X >= 1X add(s X, Y) -> s add(X, Y) 0 + 0X + 0Y >= 1 + 0X + 0Y add(X1, X2) -> n__add(X1, X2) 0 + 0X1 + 0X2 >= 1 + 1X1 + 1X2 fib N -> sel(N, fib1(s 0(), s 0())) 0 + 0N >= 4 + 0N fib1(X1, X2) -> n__fib1(X1, X2) 1 + 0X1 + 1X2 >= 0 + 1X1 + 1X2 fib1(X, Y) -> cons(X, n__fib1(Y, n__add(X, Y))) 1 + 0X + 1Y >= 1 + 0X + 0Y sel(0(), cons(X, XS)) -> X 2 + 0X + 0XS >= 1X sel(s N, cons(X, XS)) -> sel(N, activate XS) 2 + 0N + 0X + 0XS >= 2 + 0N + 0XS SCCS (1): Scc: {activate# n__fib1(X1, X2) -> activate# X1, activate# n__fib1(X1, X2) -> activate# X2} SCC (2): Strict: {activate# n__fib1(X1, X2) -> activate# X1, activate# n__fib1(X1, X2) -> activate# X2} Weak: { sel(s N, cons(X, XS)) -> sel(N, activate XS), sel(0(), cons(X, XS)) -> X, fib1(X, Y) -> cons(X, n__fib1(Y, n__add(X, Y))), fib1(X1, X2) -> n__fib1(X1, X2), fib N -> sel(N, fib1(s 0(), s 0())), add(X1, X2) -> n__add(X1, X2), add(s X, Y) -> s add(X, Y), add(0(), X) -> X, activate X -> X, activate n__fib1(X1, X2) -> fib1(activate X1, activate X2), activate n__add(X1, X2) -> add(activate X1, activate X2)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [sel](x0, x1) = x0 + 1, [fib1](x0, x1) = x0 + 1, [cons](x0, x1) = 1, [n__fib1](x0, x1) = x0 + x1 + 1, [n__add](x0, x1) = x0 + 1, [add](x0, x1) = 0, [s](x0) = x0 + 1, [fib](x0) = 0, [activate](x0) = 1, [0] = 1, [activate#](x0) = x0 Strict: activate# n__fib1(X1, X2) -> activate# X2 1 + 1X1 + 1X2 >= 0 + 1X2 activate# n__fib1(X1, X2) -> activate# X1 1 + 1X1 + 1X2 >= 0 + 1X1 Weak: activate n__add(X1, X2) -> add(activate X1, activate X2) 1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 activate n__fib1(X1, X2) -> fib1(activate X1, activate X2) 1 + 0X1 + 0X2 >= 2 + 0X1 + 0X2 activate X -> X 1 + 0X >= 1X add(0(), X) -> X 0 + 0X >= 1X add(s X, Y) -> s add(X, Y) 0 + 0X + 0Y >= 1 + 0X + 0Y add(X1, X2) -> n__add(X1, X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 1X2 fib N -> sel(N, fib1(s 0(), s 0())) 0 + 0N >= 4 + 0N fib1(X1, X2) -> n__fib1(X1, X2) 1 + 0X1 + 1X2 >= 1 + 1X1 + 1X2 fib1(X, Y) -> cons(X, n__fib1(Y, n__add(X, Y))) 1 + 0X + 1Y >= 1 + 0X + 0Y sel(0(), cons(X, XS)) -> X 2 + 0X + 0XS >= 1X sel(s N, cons(X, XS)) -> sel(N, activate XS) 2 + 0N + 0X + 0XS >= 2 + 0N + 0XS Qed SCC (1): Strict: {add#(s X, Y) -> add#(X, Y)} Weak: { sel(s N, cons(X, XS)) -> sel(N, activate XS), sel(0(), cons(X, XS)) -> X, fib1(X, Y) -> cons(X, n__fib1(Y, n__add(X, Y))), fib1(X1, X2) -> n__fib1(X1, X2), fib N -> sel(N, fib1(s 0(), s 0())), add(X1, X2) -> n__add(X1, X2), add(s X, Y) -> s add(X, Y), add(0(), X) -> X, activate X -> X, activate n__fib1(X1, X2) -> fib1(activate X1, activate X2), activate n__add(X1, X2) -> add(activate X1, activate X2)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [sel](x0, x1) = x0 + 1, [fib1](x0, x1) = x0 + 1, [cons](x0, x1) = 1, [n__fib1](x0, x1) = x0 + x1 + 1, [n__add](x0, x1) = x0 + 1, [add](x0, x1) = x0 + 1, [s](x0) = x0 + 1, [fib](x0) = 0, [activate](x0) = 1, [0] = 1, [add#](x0, x1) = x0 Strict: add#(s X, Y) -> add#(X, Y) 1 + 1X + 0Y >= 0 + 1X + 0Y Weak: activate n__add(X1, X2) -> add(activate X1, activate X2) 1 + 0X1 + 0X2 >= 2 + 0X1 + 0X2 activate n__fib1(X1, X2) -> fib1(activate X1, activate X2) 1 + 0X1 + 0X2 >= 2 + 0X1 + 0X2 activate X -> X 1 + 0X >= 1X add(0(), X) -> X 2 + 0X >= 1X add(s X, Y) -> s add(X, Y) 2 + 1X + 0Y >= 2 + 1X + 0Y add(X1, X2) -> n__add(X1, X2) 1 + 1X1 + 0X2 >= 1 + 0X1 + 1X2 fib N -> sel(N, fib1(s 0(), s 0())) 0 + 0N >= 4 + 0N fib1(X1, X2) -> n__fib1(X1, X2) 1 + 1X1 + 0X2 >= 1 + 1X1 + 1X2 fib1(X, Y) -> cons(X, n__fib1(Y, n__add(X, Y))) 1 + 1X + 0Y >= 1 + 0X + 0Y sel(0(), cons(X, XS)) -> X 2 + 0X + 0XS >= 1X sel(s N, cons(X, XS)) -> sel(N, activate XS) 2 + 0N + 0X + 0XS >= 2 + 0N + 0XS Qed