MAYBE Problem: a__fib(N) -> a__sel(mark(N),a__fib1(s(0()),s(0()))) a__fib1(X,Y) -> cons(mark(X),fib1(Y,add(X,Y))) a__add(0(),X) -> mark(X) a__add(s(X),Y) -> s(a__add(mark(X),mark(Y))) a__sel(0(),cons(X,XS)) -> mark(X) a__sel(s(N),cons(X,XS)) -> a__sel(mark(N),mark(XS)) mark(fib(X)) -> a__fib(mark(X)) mark(sel(X1,X2)) -> a__sel(mark(X1),mark(X2)) mark(fib1(X1,X2)) -> a__fib1(mark(X1),mark(X2)) mark(add(X1,X2)) -> a__add(mark(X1),mark(X2)) mark(s(X)) -> s(mark(X)) mark(0()) -> 0() mark(cons(X1,X2)) -> cons(mark(X1),X2) a__fib(X) -> fib(X) a__sel(X1,X2) -> sel(X1,X2) a__fib1(X1,X2) -> fib1(X1,X2) a__add(X1,X2) -> add(X1,X2) Proof: DP Processor: DPs: a__fib#(N) -> a__fib1#(s(0()),s(0())) a__fib#(N) -> mark#(N) a__fib#(N) -> a__sel#(mark(N),a__fib1(s(0()),s(0()))) a__fib1#(X,Y) -> mark#(X) a__add#(0(),X) -> mark#(X) a__add#(s(X),Y) -> mark#(Y) a__add#(s(X),Y) -> mark#(X) a__add#(s(X),Y) -> a__add#(mark(X),mark(Y)) a__sel#(0(),cons(X,XS)) -> mark#(X) a__sel#(s(N),cons(X,XS)) -> mark#(XS) a__sel#(s(N),cons(X,XS)) -> mark#(N) a__sel#(s(N),cons(X,XS)) -> a__sel#(mark(N),mark(XS)) mark#(fib(X)) -> mark#(X) mark#(fib(X)) -> a__fib#(mark(X)) mark#(sel(X1,X2)) -> mark#(X2) mark#(sel(X1,X2)) -> mark#(X1) mark#(sel(X1,X2)) -> a__sel#(mark(X1),mark(X2)) mark#(fib1(X1,X2)) -> mark#(X2) mark#(fib1(X1,X2)) -> mark#(X1) mark#(fib1(X1,X2)) -> a__fib1#(mark(X1),mark(X2)) mark#(add(X1,X2)) -> mark#(X2) mark#(add(X1,X2)) -> mark#(X1) mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2)) mark#(s(X)) -> mark#(X) mark#(cons(X1,X2)) -> mark#(X1) TRS: a__fib(N) -> a__sel(mark(N),a__fib1(s(0()),s(0()))) a__fib1(X,Y) -> cons(mark(X),fib1(Y,add(X,Y))) a__add(0(),X) -> mark(X) a__add(s(X),Y) -> s(a__add(mark(X),mark(Y))) a__sel(0(),cons(X,XS)) -> mark(X) a__sel(s(N),cons(X,XS)) -> a__sel(mark(N),mark(XS)) mark(fib(X)) -> a__fib(mark(X)) mark(sel(X1,X2)) -> a__sel(mark(X1),mark(X2)) mark(fib1(X1,X2)) -> a__fib1(mark(X1),mark(X2)) mark(add(X1,X2)) -> a__add(mark(X1),mark(X2)) mark(s(X)) -> s(mark(X)) mark(0()) -> 0() mark(cons(X1,X2)) -> cons(mark(X1),X2) a__fib(X) -> fib(X) a__sel(X1,X2) -> sel(X1,X2) a__fib1(X1,X2) -> fib1(X1,X2) a__add(X1,X2) -> add(X1,X2) TDG Processor: DPs: a__fib#(N) -> a__fib1#(s(0()),s(0())) a__fib#(N) -> mark#(N) a__fib#(N) -> a__sel#(mark(N),a__fib1(s(0()),s(0()))) a__fib1#(X,Y) -> mark#(X) a__add#(0(),X) -> mark#(X) a__add#(s(X),Y) -> mark#(Y) a__add#(s(X),Y) -> mark#(X) a__add#(s(X),Y) -> a__add#(mark(X),mark(Y)) a__sel#(0(),cons(X,XS)) -> mark#(X) a__sel#(s(N),cons(X,XS)) -> mark#(XS) a__sel#(s(N),cons(X,XS)) -> mark#(N) a__sel#(s(N),cons(X,XS)) -> a__sel#(mark(N),mark(XS)) mark#(fib(X)) -> mark#(X) mark#(fib(X)) -> a__fib#(mark(X)) mark#(sel(X1,X2)) -> mark#(X2) mark#(sel(X1,X2)) -> mark#(X1) mark#(sel(X1,X2)) -> a__sel#(mark(X1),mark(X2)) mark#(fib1(X1,X2)) -> mark#(X2) mark#(fib1(X1,X2)) -> mark#(X1) mark#(fib1(X1,X2)) -> a__fib1#(mark(X1),mark(X2)) mark#(add(X1,X2)) -> mark#(X2) mark#(add(X1,X2)) -> mark#(X1) mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2)) mark#(s(X)) -> mark#(X) mark#(cons(X1,X2)) -> mark#(X1) TRS: a__fib(N) -> a__sel(mark(N),a__fib1(s(0()),s(0()))) a__fib1(X,Y) -> cons(mark(X),fib1(Y,add(X,Y))) a__add(0(),X) -> mark(X) a__add(s(X),Y) -> s(a__add(mark(X),mark(Y))) a__sel(0(),cons(X,XS)) -> mark(X) a__sel(s(N),cons(X,XS)) -> a__sel(mark(N),mark(XS)) mark(fib(X)) -> a__fib(mark(X)) mark(sel(X1,X2)) -> a__sel(mark(X1),mark(X2)) mark(fib1(X1,X2)) -> a__fib1(mark(X1),mark(X2)) mark(add(X1,X2)) -> a__add(mark(X1),mark(X2)) mark(s(X)) -> s(mark(X)) mark(0()) -> 0() mark(cons(X1,X2)) -> cons(mark(X1),X2) a__fib(X) -> fib(X) a__sel(X1,X2) -> sel(X1,X2) a__fib1(X1,X2) -> fib1(X1,X2) a__add(X1,X2) -> add(X1,X2) graph: a__add#(s(X),Y) -> a__add#(mark(X),mark(Y)) -> a__add#(s(X),Y) -> a__add#(mark(X),mark(Y)) a__add#(s(X),Y) -> a__add#(mark(X),mark(Y)) -> a__add#(s(X),Y) -> mark#(X) a__add#(s(X),Y) -> a__add#(mark(X),mark(Y)) -> a__add#(s(X),Y) -> mark#(Y) a__add#(s(X),Y) -> a__add#(mark(X),mark(Y)) -> a__add#(0(),X) -> mark#(X) a__add#(s(X),Y) -> mark#(Y) -> mark#(cons(X1,X2)) -> mark#(X1) a__add#(s(X),Y) -> mark#(Y) -> mark#(s(X)) -> mark#(X) a__add#(s(X),Y) -> mark#(Y) -> mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2)) a__add#(s(X),Y) -> mark#(Y) -> mark#(add(X1,X2)) -> mark#(X1) a__add#(s(X),Y) -> mark#(Y) -> mark#(add(X1,X2)) -> mark#(X2) a__add#(s(X),Y) -> mark#(Y) -> mark#(fib1(X1,X2)) -> a__fib1#(mark(X1),mark(X2)) a__add#(s(X),Y) -> mark#(Y) -> mark#(fib1(X1,X2)) -> mark#(X1) a__add#(s(X),Y) -> mark#(Y) -> mark#(fib1(X1,X2)) -> mark#(X2) a__add#(s(X),Y) -> mark#(Y) -> mark#(sel(X1,X2)) -> a__sel#(mark(X1),mark(X2)) a__add#(s(X),Y) -> mark#(Y) -> mark#(sel(X1,X2)) -> mark#(X1) a__add#(s(X),Y) -> mark#(Y) -> mark#(sel(X1,X2)) -> mark#(X2) a__add#(s(X),Y) -> mark#(Y) -> mark#(fib(X)) -> a__fib#(mark(X)) a__add#(s(X),Y) -> mark#(Y) -> mark#(fib(X)) -> mark#(X) a__add#(s(X),Y) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1) a__add#(s(X),Y) -> mark#(X) -> mark#(s(X)) -> mark#(X) a__add#(s(X),Y) -> mark#(X) -> mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2)) a__add#(s(X),Y) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X1) a__add#(s(X),Y) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X2) a__add#(s(X),Y) -> mark#(X) -> mark#(fib1(X1,X2)) -> a__fib1#(mark(X1),mark(X2)) a__add#(s(X),Y) -> mark#(X) -> mark#(fib1(X1,X2)) -> mark#(X1) a__add#(s(X),Y) -> mark#(X) -> mark#(fib1(X1,X2)) -> mark#(X2) a__add#(s(X),Y) -> mark#(X) -> mark#(sel(X1,X2)) -> a__sel#(mark(X1),mark(X2)) a__add#(s(X),Y) -> mark#(X) -> mark#(sel(X1,X2)) -> mark#(X1) a__add#(s(X),Y) -> mark#(X) -> mark#(sel(X1,X2)) -> mark#(X2) a__add#(s(X),Y) -> mark#(X) -> mark#(fib(X)) -> a__fib#(mark(X)) a__add#(s(X),Y) -> mark#(X) -> mark#(fib(X)) -> mark#(X) a__add#(0(),X) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1) a__add#(0(),X) -> mark#(X) -> mark#(s(X)) -> mark#(X) a__add#(0(),X) -> mark#(X) -> mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2)) a__add#(0(),X) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X1) a__add#(0(),X) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X2) a__add#(0(),X) -> mark#(X) -> mark#(fib1(X1,X2)) -> a__fib1#(mark(X1),mark(X2)) a__add#(0(),X) -> mark#(X) -> mark#(fib1(X1,X2)) -> mark#(X1) a__add#(0(),X) -> mark#(X) -> mark#(fib1(X1,X2)) -> mark#(X2) a__add#(0(),X) -> mark#(X) -> mark#(sel(X1,X2)) -> a__sel#(mark(X1),mark(X2)) a__add#(0(),X) -> mark#(X) -> mark#(sel(X1,X2)) -> mark#(X1) a__add#(0(),X) -> mark#(X) -> mark#(sel(X1,X2)) -> mark#(X2) a__add#(0(),X) -> mark#(X) -> mark#(fib(X)) -> a__fib#(mark(X)) a__add#(0(),X) -> mark#(X) -> mark#(fib(X)) -> mark#(X) a__sel#(s(N),cons(X,XS)) -> a__sel#(mark(N),mark(XS)) -> a__sel#(s(N),cons(X,XS)) -> a__sel#(mark(N),mark(XS)) a__sel#(s(N),cons(X,XS)) -> a__sel#(mark(N),mark(XS)) -> a__sel#(s(N),cons(X,XS)) -> mark#(N) a__sel#(s(N),cons(X,XS)) -> a__sel#(mark(N),mark(XS)) -> a__sel#(s(N),cons(X,XS)) -> mark#(XS) a__sel#(s(N),cons(X,XS)) -> a__sel#(mark(N),mark(XS)) -> a__sel#(0(),cons(X,XS)) -> mark#(X) a__sel#(s(N),cons(X,XS)) -> mark#(XS) -> mark#(cons(X1,X2)) -> mark#(X1) a__sel#(s(N),cons(X,XS)) -> mark#(XS) -> mark#(s(X)) -> mark#(X) a__sel#(s(N),cons(X,XS)) -> mark#(XS) -> mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2)) a__sel#(s(N),cons(X,XS)) -> mark#(XS) -> mark#(add(X1,X2)) -> mark#(X1) a__sel#(s(N),cons(X,XS)) -> mark#(XS) -> mark#(add(X1,X2)) -> mark#(X2) a__sel#(s(N),cons(X,XS)) -> mark#(XS) -> mark#(fib1(X1,X2)) -> a__fib1#(mark(X1),mark(X2)) a__sel#(s(N),cons(X,XS)) -> mark#(XS) -> mark#(fib1(X1,X2)) -> mark#(X1) a__sel#(s(N),cons(X,XS)) -> mark#(XS) -> mark#(fib1(X1,X2)) -> mark#(X2) a__sel#(s(N),cons(X,XS)) -> mark#(XS) -> mark#(sel(X1,X2)) -> a__sel#(mark(X1),mark(X2)) a__sel#(s(N),cons(X,XS)) -> mark#(XS) -> mark#(sel(X1,X2)) -> mark#(X1) a__sel#(s(N),cons(X,XS)) -> mark#(XS) -> mark#(sel(X1,X2)) -> mark#(X2) a__sel#(s(N),cons(X,XS)) -> mark#(XS) -> mark#(fib(X)) -> a__fib#(mark(X)) a__sel#(s(N),cons(X,XS)) -> mark#(XS) -> mark#(fib(X)) -> mark#(X) a__sel#(s(N),cons(X,XS)) -> mark#(N) -> mark#(cons(X1,X2)) -> mark#(X1) a__sel#(s(N),cons(X,XS)) -> mark#(N) -> mark#(s(X)) -> mark#(X) a__sel#(s(N),cons(X,XS)) -> mark#(N) -> mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2)) a__sel#(s(N),cons(X,XS)) -> mark#(N) -> mark#(add(X1,X2)) -> mark#(X1) a__sel#(s(N),cons(X,XS)) -> mark#(N) -> mark#(add(X1,X2)) -> mark#(X2) a__sel#(s(N),cons(X,XS)) -> mark#(N) -> mark#(fib1(X1,X2)) -> a__fib1#(mark(X1),mark(X2)) a__sel#(s(N),cons(X,XS)) -> mark#(N) -> mark#(fib1(X1,X2)) -> mark#(X1) a__sel#(s(N),cons(X,XS)) -> mark#(N) -> mark#(fib1(X1,X2)) -> mark#(X2) a__sel#(s(N),cons(X,XS)) -> mark#(N) -> mark#(sel(X1,X2)) -> a__sel#(mark(X1),mark(X2)) a__sel#(s(N),cons(X,XS)) -> mark#(N) -> mark#(sel(X1,X2)) -> mark#(X1) a__sel#(s(N),cons(X,XS)) -> mark#(N) -> mark#(sel(X1,X2)) -> mark#(X2) a__sel#(s(N),cons(X,XS)) -> mark#(N) -> mark#(fib(X)) -> a__fib#(mark(X)) a__sel#(s(N),cons(X,XS)) -> mark#(N) -> mark#(fib(X)) -> mark#(X) a__sel#(0(),cons(X,XS)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1) a__sel#(0(),cons(X,XS)) -> mark#(X) -> mark#(s(X)) -> mark#(X) a__sel#(0(),cons(X,XS)) -> mark#(X) -> mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2)) a__sel#(0(),cons(X,XS)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X1) a__sel#(0(),cons(X,XS)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X2) a__sel#(0(),cons(X,XS)) -> mark#(X) -> mark#(fib1(X1,X2)) -> a__fib1#(mark(X1),mark(X2)) a__sel#(0(),cons(X,XS)) -> mark#(X) -> mark#(fib1(X1,X2)) -> mark#(X1) a__sel#(0(),cons(X,XS)) -> mark#(X) -> mark#(fib1(X1,X2)) -> mark#(X2) a__sel#(0(),cons(X,XS)) -> mark#(X) -> mark#(sel(X1,X2)) -> a__sel#(mark(X1),mark(X2)) a__sel#(0(),cons(X,XS)) -> mark#(X) -> mark#(sel(X1,X2)) -> mark#(X1) a__sel#(0(),cons(X,XS)) -> mark#(X) -> mark#(sel(X1,X2)) -> mark#(X2) a__sel#(0(),cons(X,XS)) -> mark#(X) -> mark#(fib(X)) -> a__fib#(mark(X)) a__sel#(0(),cons(X,XS)) -> mark#(X) -> mark#(fib(X)) -> mark#(X) mark#(sel(X1,X2)) -> a__sel#(mark(X1),mark(X2)) -> a__sel#(s(N),cons(X,XS)) -> a__sel#(mark(N),mark(XS)) mark#(sel(X1,X2)) -> a__sel#(mark(X1),mark(X2)) -> a__sel#(s(N),cons(X,XS)) -> mark#(N) mark#(sel(X1,X2)) -> a__sel#(mark(X1),mark(X2)) -> a__sel#(s(N),cons(X,XS)) -> mark#(XS) mark#(sel(X1,X2)) -> a__sel#(mark(X1),mark(X2)) -> a__sel#(0(),cons(X,XS)) -> mark#(X) mark#(sel(X1,X2)) -> mark#(X2) -> mark#(cons(X1,X2)) -> mark#(X1) mark#(sel(X1,X2)) -> mark#(X2) -> mark#(s(X)) -> mark#(X) mark#(sel(X1,X2)) -> mark#(X2) -> mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2)) mark#(sel(X1,X2)) -> mark#(X2) -> mark#(add(X1,X2)) -> mark#(X1) mark#(sel(X1,X2)) -> mark#(X2) -> mark#(add(X1,X2)) -> mark#(X2) mark#(sel(X1,X2)) -> mark#(X2) -> mark#(fib1(X1,X2)) -> a__fib1#(mark(X1),mark(X2)) mark#(sel(X1,X2)) -> mark#(X2) -> mark#(fib1(X1,X2)) -> mark#(X1) mark#(sel(X1,X2)) -> mark#(X2) -> mark#(fib1(X1,X2)) -> mark#(X2) mark#(sel(X1,X2)) -> mark#(X2) -> mark#(sel(X1,X2)) -> a__sel#(mark(X1),mark(X2)) mark#(sel(X1,X2)) -> mark#(X2) -> mark#(sel(X1,X2)) -> mark#(X1) mark#(sel(X1,X2)) -> mark#(X2) -> mark#(sel(X1,X2)) -> mark#(X2) mark#(sel(X1,X2)) -> mark#(X2) -> mark#(fib(X)) -> a__fib#(mark(X)) mark#(sel(X1,X2)) -> mark#(X2) -> mark#(fib(X)) -> mark#(X) mark#(sel(X1,X2)) -> mark#(X1) -> mark#(cons(X1,X2)) -> mark#(X1) mark#(sel(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> mark#(X) mark#(sel(X1,X2)) -> mark#(X1) -> mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2)) mark#(sel(X1,X2)) -> mark#(X1) -> mark#(add(X1,X2)) -> mark#(X1) mark#(sel(X1,X2)) -> mark#(X1) -> mark#(add(X1,X2)) -> mark#(X2) mark#(sel(X1,X2)) -> mark#(X1) -> mark#(fib1(X1,X2)) -> a__fib1#(mark(X1),mark(X2)) mark#(sel(X1,X2)) -> mark#(X1) -> mark#(fib1(X1,X2)) -> mark#(X1) mark#(sel(X1,X2)) -> mark#(X1) -> mark#(fib1(X1,X2)) -> mark#(X2) mark#(sel(X1,X2)) -> mark#(X1) -> mark#(sel(X1,X2)) -> a__sel#(mark(X1),mark(X2)) mark#(sel(X1,X2)) -> mark#(X1) -> mark#(sel(X1,X2)) -> mark#(X1) mark#(sel(X1,X2)) -> mark#(X1) -> mark#(sel(X1,X2)) -> mark#(X2) mark#(sel(X1,X2)) -> mark#(X1) -> mark#(fib(X)) -> a__fib#(mark(X)) mark#(sel(X1,X2)) -> mark#(X1) -> mark#(fib(X)) -> mark#(X) mark#(fib(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1) mark#(fib(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X) mark#(fib(X)) -> mark#(X) -> mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2)) mark#(fib(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X1) mark#(fib(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X2) mark#(fib(X)) -> mark#(X) -> mark#(fib1(X1,X2)) -> a__fib1#(mark(X1),mark(X2)) mark#(fib(X)) -> mark#(X) -> mark#(fib1(X1,X2)) -> mark#(X1) mark#(fib(X)) -> mark#(X) -> mark#(fib1(X1,X2)) -> mark#(X2) mark#(fib(X)) -> mark#(X) -> mark#(sel(X1,X2)) -> a__sel#(mark(X1),mark(X2)) mark#(fib(X)) -> mark#(X) -> mark#(sel(X1,X2)) -> mark#(X1) mark#(fib(X)) -> mark#(X) -> mark#(sel(X1,X2)) -> mark#(X2) mark#(fib(X)) -> mark#(X) -> mark#(fib(X)) -> a__fib#(mark(X)) mark#(fib(X)) -> mark#(X) -> mark#(fib(X)) -> mark#(X) mark#(fib(X)) -> a__fib#(mark(X)) -> a__fib#(N) -> a__sel#(mark(N),a__fib1(s(0()),s(0()))) mark#(fib(X)) -> a__fib#(mark(X)) -> a__fib#(N) -> mark#(N) mark#(fib(X)) -> a__fib#(mark(X)) -> a__fib#(N) -> a__fib1#(s(0()),s(0())) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(cons(X1,X2)) -> mark#(X1) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> mark#(X) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2)) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(add(X1,X2)) -> mark#(X1) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(add(X1,X2)) -> mark#(X2) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(fib1(X1,X2)) -> a__fib1#(mark(X1),mark(X2)) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(fib1(X1,X2)) -> mark#(X1) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(fib1(X1,X2)) -> mark#(X2) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(sel(X1,X2)) -> a__sel#(mark(X1),mark(X2)) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(sel(X1,X2)) -> mark#(X1) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(sel(X1,X2)) -> mark#(X2) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(fib(X)) -> a__fib#(mark(X)) mark#(cons(X1,X2)) -> mark#(X1) -> mark#(fib(X)) -> mark#(X) mark#(fib1(X1,X2)) -> mark#(X2) -> mark#(cons(X1,X2)) -> mark#(X1) mark#(fib1(X1,X2)) -> mark#(X2) -> mark#(s(X)) -> mark#(X) mark#(fib1(X1,X2)) -> mark#(X2) -> mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2)) mark#(fib1(X1,X2)) -> mark#(X2) -> mark#(add(X1,X2)) -> mark#(X1) mark#(fib1(X1,X2)) -> mark#(X2) -> mark#(add(X1,X2)) -> mark#(X2) mark#(fib1(X1,X2)) -> mark#(X2) -> mark#(fib1(X1,X2)) -> a__fib1#(mark(X1),mark(X2)) mark#(fib1(X1,X2)) -> mark#(X2) -> mark#(fib1(X1,X2)) -> mark#(X1) mark#(fib1(X1,X2)) -> mark#(X2) -> mark#(fib1(X1,X2)) -> mark#(X2) mark#(fib1(X1,X2)) -> mark#(X2) -> mark#(sel(X1,X2)) -> a__sel#(mark(X1),mark(X2)) mark#(fib1(X1,X2)) -> mark#(X2) -> mark#(sel(X1,X2)) -> mark#(X1) mark#(fib1(X1,X2)) -> mark#(X2) -> mark#(sel(X1,X2)) -> mark#(X2) mark#(fib1(X1,X2)) -> mark#(X2) -> mark#(fib(X)) -> a__fib#(mark(X)) mark#(fib1(X1,X2)) -> mark#(X2) -> mark#(fib(X)) -> mark#(X) mark#(fib1(X1,X2)) -> mark#(X1) -> mark#(cons(X1,X2)) -> mark#(X1) mark#(fib1(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> mark#(X) mark#(fib1(X1,X2)) -> mark#(X1) -> mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2)) mark#(fib1(X1,X2)) -> mark#(X1) -> mark#(add(X1,X2)) -> mark#(X1) mark#(fib1(X1,X2)) -> mark#(X1) -> mark#(add(X1,X2)) -> mark#(X2) mark#(fib1(X1,X2)) -> mark#(X1) -> mark#(fib1(X1,X2)) -> a__fib1#(mark(X1),mark(X2)) mark#(fib1(X1,X2)) -> mark#(X1) -> mark#(fib1(X1,X2)) -> mark#(X1) mark#(fib1(X1,X2)) -> mark#(X1) -> mark#(fib1(X1,X2)) -> mark#(X2) mark#(fib1(X1,X2)) -> mark#(X1) -> mark#(sel(X1,X2)) -> a__sel#(mark(X1),mark(X2)) mark#(fib1(X1,X2)) -> mark#(X1) -> mark#(sel(X1,X2)) -> mark#(X1) mark#(fib1(X1,X2)) -> mark#(X1) -> mark#(sel(X1,X2)) -> mark#(X2) mark#(fib1(X1,X2)) -> mark#(X1) -> mark#(fib(X)) -> a__fib#(mark(X)) mark#(fib1(X1,X2)) -> mark#(X1) -> mark#(fib(X)) -> mark#(X) mark#(fib1(X1,X2)) -> a__fib1#(mark(X1),mark(X2)) -> a__fib1#(X,Y) -> mark#(X) mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2)) -> a__add#(s(X),Y) -> a__add#(mark(X),mark(Y)) mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2)) -> a__add#(s(X),Y) -> mark#(X) mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2)) -> a__add#(s(X),Y) -> mark#(Y) mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2)) -> a__add#(0(),X) -> mark#(X) mark#(add(X1,X2)) -> mark#(X2) -> mark#(cons(X1,X2)) -> mark#(X1) mark#(add(X1,X2)) -> mark#(X2) -> mark#(s(X)) -> mark#(X) mark#(add(X1,X2)) -> mark#(X2) -> mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2)) mark#(add(X1,X2)) -> mark#(X2) -> mark#(add(X1,X2)) -> mark#(X1) mark#(add(X1,X2)) -> mark#(X2) -> mark#(add(X1,X2)) -> mark#(X2) mark#(add(X1,X2)) -> mark#(X2) -> mark#(fib1(X1,X2)) -> a__fib1#(mark(X1),mark(X2)) mark#(add(X1,X2)) -> mark#(X2) -> mark#(fib1(X1,X2)) -> mark#(X1) mark#(add(X1,X2)) -> mark#(X2) -> mark#(fib1(X1,X2)) -> mark#(X2) mark#(add(X1,X2)) -> mark#(X2) -> mark#(sel(X1,X2)) -> a__sel#(mark(X1),mark(X2)) mark#(add(X1,X2)) -> mark#(X2) -> mark#(sel(X1,X2)) -> mark#(X1) mark#(add(X1,X2)) -> mark#(X2) -> mark#(sel(X1,X2)) -> mark#(X2) mark#(add(X1,X2)) -> mark#(X2) -> mark#(fib(X)) -> a__fib#(mark(X)) mark#(add(X1,X2)) -> mark#(X2) -> mark#(fib(X)) -> mark#(X) mark#(add(X1,X2)) -> mark#(X1) -> mark#(cons(X1,X2)) -> mark#(X1) mark#(add(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> mark#(X) mark#(add(X1,X2)) -> mark#(X1) -> mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2)) mark#(add(X1,X2)) -> mark#(X1) -> mark#(add(X1,X2)) -> mark#(X1) mark#(add(X1,X2)) -> mark#(X1) -> mark#(add(X1,X2)) -> mark#(X2) mark#(add(X1,X2)) -> mark#(X1) -> mark#(fib1(X1,X2)) -> a__fib1#(mark(X1),mark(X2)) mark#(add(X1,X2)) -> mark#(X1) -> mark#(fib1(X1,X2)) -> mark#(X1) mark#(add(X1,X2)) -> mark#(X1) -> mark#(fib1(X1,X2)) -> mark#(X2) mark#(add(X1,X2)) -> mark#(X1) -> mark#(sel(X1,X2)) -> a__sel#(mark(X1),mark(X2)) mark#(add(X1,X2)) -> mark#(X1) -> mark#(sel(X1,X2)) -> mark#(X1) mark#(add(X1,X2)) -> mark#(X1) -> mark#(sel(X1,X2)) -> mark#(X2) mark#(add(X1,X2)) -> mark#(X1) -> mark#(fib(X)) -> a__fib#(mark(X)) mark#(add(X1,X2)) -> mark#(X1) -> mark#(fib(X)) -> mark#(X) mark#(s(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1) mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X) mark#(s(X)) -> mark#(X) -> mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2)) mark#(s(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X1) mark#(s(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X2) mark#(s(X)) -> mark#(X) -> mark#(fib1(X1,X2)) -> a__fib1#(mark(X1),mark(X2)) mark#(s(X)) -> mark#(X) -> mark#(fib1(X1,X2)) -> mark#(X1) mark#(s(X)) -> mark#(X) -> mark#(fib1(X1,X2)) -> mark#(X2) mark#(s(X)) -> mark#(X) -> mark#(sel(X1,X2)) -> a__sel#(mark(X1),mark(X2)) mark#(s(X)) -> mark#(X) -> mark#(sel(X1,X2)) -> mark#(X1) mark#(s(X)) -> mark#(X) -> mark#(sel(X1,X2)) -> mark#(X2) mark#(s(X)) -> mark#(X) -> mark#(fib(X)) -> a__fib#(mark(X)) mark#(s(X)) -> mark#(X) -> mark#(fib(X)) -> mark#(X) a__fib1#(X,Y) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1) a__fib1#(X,Y) -> mark#(X) -> mark#(s(X)) -> mark#(X) a__fib1#(X,Y) -> mark#(X) -> mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2)) a__fib1#(X,Y) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X1) a__fib1#(X,Y) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X2) a__fib1#(X,Y) -> mark#(X) -> mark#(fib1(X1,X2)) -> a__fib1#(mark(X1),mark(X2)) a__fib1#(X,Y) -> mark#(X) -> mark#(fib1(X1,X2)) -> mark#(X1) a__fib1#(X,Y) -> mark#(X) -> mark#(fib1(X1,X2)) -> mark#(X2) a__fib1#(X,Y) -> mark#(X) -> mark#(sel(X1,X2)) -> a__sel#(mark(X1),mark(X2)) a__fib1#(X,Y) -> mark#(X) -> mark#(sel(X1,X2)) -> mark#(X1) a__fib1#(X,Y) -> mark#(X) -> mark#(sel(X1,X2)) -> mark#(X2) a__fib1#(X,Y) -> mark#(X) -> mark#(fib(X)) -> a__fib#(mark(X)) a__fib1#(X,Y) -> mark#(X) -> mark#(fib(X)) -> mark#(X) a__fib#(N) -> a__sel#(mark(N),a__fib1(s(0()),s(0()))) -> a__sel#(s(N),cons(X,XS)) -> a__sel#(mark(N),mark(XS)) a__fib#(N) -> a__sel#(mark(N),a__fib1(s(0()),s(0()))) -> a__sel#(s(N),cons(X,XS)) -> mark#(N) a__fib#(N) -> a__sel#(mark(N),a__fib1(s(0()),s(0()))) -> a__sel#(s(N),cons(X,XS)) -> mark#(XS) a__fib#(N) -> a__sel#(mark(N),a__fib1(s(0()),s(0()))) -> a__sel#(0(),cons(X,XS)) -> mark#(X) a__fib#(N) -> mark#(N) -> mark#(cons(X1,X2)) -> mark#(X1) a__fib#(N) -> mark#(N) -> mark#(s(X)) -> mark#(X) a__fib#(N) -> mark#(N) -> mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2)) a__fib#(N) -> mark#(N) -> mark#(add(X1,X2)) -> mark#(X1) a__fib#(N) -> mark#(N) -> mark#(add(X1,X2)) -> mark#(X2) a__fib#(N) -> mark#(N) -> mark#(fib1(X1,X2)) -> a__fib1#(mark(X1),mark(X2)) a__fib#(N) -> mark#(N) -> mark#(fib1(X1,X2)) -> mark#(X1) a__fib#(N) -> mark#(N) -> mark#(fib1(X1,X2)) -> mark#(X2) a__fib#(N) -> mark#(N) -> mark#(sel(X1,X2)) -> a__sel#(mark(X1),mark(X2)) a__fib#(N) -> mark#(N) -> mark#(sel(X1,X2)) -> mark#(X1) a__fib#(N) -> mark#(N) -> mark#(sel(X1,X2)) -> mark#(X2) a__fib#(N) -> mark#(N) -> mark#(fib(X)) -> a__fib#(mark(X)) a__fib#(N) -> mark#(N) -> mark#(fib(X)) -> mark#(X) a__fib#(N) -> a__fib1#(s(0()),s(0())) -> a__fib1#(X,Y) -> mark#(X) SCC Processor: #sccs: 1 #rules: 25 #arcs: 246/625 DPs: a__add#(s(X),Y) -> a__add#(mark(X),mark(Y)) a__add#(0(),X) -> mark#(X) mark#(fib(X)) -> mark#(X) mark#(fib(X)) -> a__fib#(mark(X)) a__fib#(N) -> a__fib1#(s(0()),s(0())) a__fib1#(X,Y) -> mark#(X) mark#(sel(X1,X2)) -> mark#(X2) mark#(sel(X1,X2)) -> mark#(X1) mark#(sel(X1,X2)) -> a__sel#(mark(X1),mark(X2)) a__sel#(0(),cons(X,XS)) -> mark#(X) mark#(fib1(X1,X2)) -> mark#(X2) mark#(fib1(X1,X2)) -> mark#(X1) mark#(fib1(X1,X2)) -> a__fib1#(mark(X1),mark(X2)) mark#(add(X1,X2)) -> mark#(X2) mark#(add(X1,X2)) -> mark#(X1) mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2)) a__add#(s(X),Y) -> mark#(Y) mark#(s(X)) -> mark#(X) mark#(cons(X1,X2)) -> mark#(X1) a__add#(s(X),Y) -> mark#(X) a__sel#(s(N),cons(X,XS)) -> mark#(XS) a__sel#(s(N),cons(X,XS)) -> mark#(N) a__sel#(s(N),cons(X,XS)) -> a__sel#(mark(N),mark(XS)) a__fib#(N) -> mark#(N) a__fib#(N) -> a__sel#(mark(N),a__fib1(s(0()),s(0()))) TRS: a__fib(N) -> a__sel(mark(N),a__fib1(s(0()),s(0()))) a__fib1(X,Y) -> cons(mark(X),fib1(Y,add(X,Y))) a__add(0(),X) -> mark(X) a__add(s(X),Y) -> s(a__add(mark(X),mark(Y))) a__sel(0(),cons(X,XS)) -> mark(X) a__sel(s(N),cons(X,XS)) -> a__sel(mark(N),mark(XS)) mark(fib(X)) -> a__fib(mark(X)) mark(sel(X1,X2)) -> a__sel(mark(X1),mark(X2)) mark(fib1(X1,X2)) -> a__fib1(mark(X1),mark(X2)) mark(add(X1,X2)) -> a__add(mark(X1),mark(X2)) mark(s(X)) -> s(mark(X)) mark(0()) -> 0() mark(cons(X1,X2)) -> cons(mark(X1),X2) a__fib(X) -> fib(X) a__sel(X1,X2) -> sel(X1,X2) a__fib1(X1,X2) -> fib1(X1,X2) a__add(X1,X2) -> add(X1,X2) Open