MAYBE Time: 0.121755 TRS: {sel(s N, cons(X, XS)) -> sel(N, XS), sel(0(), cons(X, XS)) -> X, fib1(X, Y) -> cons(X, fib1(Y, add(X, Y))), fib N -> sel(N, fib1(s 0(), s 0())), add(s X, Y) -> s add(X, Y), add(0(), X) -> X} DP: DP: {sel#(s N, cons(X, XS)) -> sel#(N, XS), fib1#(X, Y) -> fib1#(Y, add(X, Y)), fib1#(X, Y) -> add#(X, Y), fib# N -> sel#(N, fib1(s 0(), s 0())), fib# N -> fib1#(s 0(), s 0()), add#(s X, Y) -> add#(X, Y)} TRS: {sel(s N, cons(X, XS)) -> sel(N, XS), sel(0(), cons(X, XS)) -> X, fib1(X, Y) -> cons(X, fib1(Y, add(X, Y))), fib N -> sel(N, fib1(s 0(), s 0())), add(s X, Y) -> s add(X, Y), add(0(), X) -> X} EDG: {(fib1#(X, Y) -> fib1#(Y, add(X, Y)), fib1#(X, Y) -> add#(X, Y)) (fib1#(X, Y) -> fib1#(Y, add(X, Y)), fib1#(X, Y) -> fib1#(Y, add(X, Y))) (add#(s X, Y) -> add#(X, Y), add#(s X, Y) -> add#(X, Y)) (fib# N -> sel#(N, fib1(s 0(), s 0())), sel#(s N, cons(X, XS)) -> sel#(N, XS)) (fib# N -> fib1#(s 0(), s 0()), fib1#(X, Y) -> fib1#(Y, add(X, Y))) (fib# N -> fib1#(s 0(), s 0()), fib1#(X, Y) -> add#(X, Y)) (fib1#(X, Y) -> add#(X, Y), add#(s X, Y) -> add#(X, Y)) (sel#(s N, cons(X, XS)) -> sel#(N, XS), sel#(s N, cons(X, XS)) -> sel#(N, XS))} STATUS: arrows: 0.777778 SCCS (3): Scc: {fib1#(X, Y) -> fib1#(Y, add(X, Y))} Scc: {add#(s X, Y) -> add#(X, Y)} Scc: {sel#(s N, cons(X, XS)) -> sel#(N, XS)} SCC (1): Strict: {fib1#(X, Y) -> fib1#(Y, add(X, Y))} Weak: {sel(s N, cons(X, XS)) -> sel(N, XS), sel(0(), cons(X, XS)) -> X, fib1(X, Y) -> cons(X, fib1(Y, add(X, Y))), fib N -> sel(N, fib1(s 0(), s 0())), add(s X, Y) -> s add(X, Y), add(0(), X) -> X} Open SCC (1): Strict: {add#(s X, Y) -> add#(X, Y)} Weak: {sel(s N, cons(X, XS)) -> sel(N, XS), sel(0(), cons(X, XS)) -> X, fib1(X, Y) -> cons(X, fib1(Y, add(X, Y))), fib N -> sel(N, fib1(s 0(), s 0())), add(s X, Y) -> s add(X, Y), add(0(), X) -> X} Open SCC (1): Strict: {sel#(s N, cons(X, XS)) -> sel#(N, XS)} Weak: {sel(s N, cons(X, XS)) -> sel(N, XS), sel(0(), cons(X, XS)) -> X, fib1(X, Y) -> cons(X, fib1(Y, add(X, Y))), fib N -> sel(N, fib1(s 0(), s 0())), add(s X, Y) -> s add(X, Y), add(0(), X) -> X} Open