Term Rewriting System R:
[N, X, Y, X1, X2, XS]
afib(N) -> asel(mark(N), afib1(s(0), s(0)))
afib(X) -> fib(X)
afib1(X, Y) -> cons(mark(X), fib1(Y, add(X, Y)))
afib1(X1, X2) -> fib1(X1, X2)
aadd(0, X) -> mark(X)
aadd(s(X), Y) -> s(aadd(mark(X), mark(Y)))
aadd(X1, X2) -> add(X1, X2)
asel(0, cons(X, XS)) -> mark(X)
asel(s(N), cons(X, XS)) -> asel(mark(N), mark(XS))
asel(X1, X2) -> sel(X1, X2)
mark(fib(X)) -> afib(mark(X))
mark(sel(X1, X2)) -> asel(mark(X1), mark(X2))
mark(fib1(X1, X2)) -> afib1(mark(X1), mark(X2))
mark(add(X1, X2)) -> aadd(mark(X1), mark(X2))
mark(s(X)) -> s(mark(X))
mark(0) -> 0
mark(cons(X1, X2)) -> cons(mark(X1), X2)

Innermost Termination of R to be shown.



   R
Dependency Pair Analysis



R contains the following Dependency Pairs:

AFIB(N) -> ASEL(mark(N), afib1(s(0), s(0)))
AFIB(N) -> MARK(N)
AFIB(N) -> AFIB1(s(0), s(0))
AFIB1(X, Y) -> MARK(X)
AADD(0, X) -> MARK(X)
AADD(s(X), Y) -> AADD(mark(X), mark(Y))
AADD(s(X), Y) -> MARK(X)
AADD(s(X), Y) -> MARK(Y)
ASEL(0, cons(X, XS)) -> MARK(X)
ASEL(s(N), cons(X, XS)) -> ASEL(mark(N), mark(XS))
ASEL(s(N), cons(X, XS)) -> MARK(N)
ASEL(s(N), cons(X, XS)) -> MARK(XS)
MARK(fib(X)) -> AFIB(mark(X))
MARK(fib(X)) -> MARK(X)
MARK(sel(X1, X2)) -> ASEL(mark(X1), mark(X2))
MARK(sel(X1, X2)) -> MARK(X1)
MARK(sel(X1, X2)) -> MARK(X2)
MARK(fib1(X1, X2)) -> AFIB1(mark(X1), mark(X2))
MARK(fib1(X1, X2)) -> MARK(X1)
MARK(fib1(X1, X2)) -> MARK(X2)
MARK(add(X1, X2)) -> AADD(mark(X1), mark(X2))
MARK(add(X1, X2)) -> MARK(X1)
MARK(add(X1, X2)) -> MARK(X2)
MARK(s(X)) -> MARK(X)
MARK(cons(X1, X2)) -> MARK(X1)

Furthermore, R contains one SCC.


   R
DPs
       →DP Problem 1
Remaining Obligation(s)




The following remains to be proven:
Dependency Pairs:

AFIB(N) -> AFIB1(s(0), s(0))
ASEL(s(N), cons(X, XS)) -> MARK(XS)
AADD(s(X), Y) -> MARK(Y)
AADD(s(X), Y) -> MARK(X)
AADD(s(X), Y) -> AADD(mark(X), mark(Y))
MARK(cons(X1, X2)) -> MARK(X1)
MARK(s(X)) -> MARK(X)
MARK(add(X1, X2)) -> MARK(X2)
MARK(add(X1, X2)) -> MARK(X1)
AADD(0, X) -> MARK(X)
MARK(add(X1, X2)) -> AADD(mark(X1), mark(X2))
MARK(fib1(X1, X2)) -> MARK(X2)
MARK(fib1(X1, X2)) -> MARK(X1)
AFIB1(X, Y) -> MARK(X)
MARK(fib1(X1, X2)) -> AFIB1(mark(X1), mark(X2))
MARK(sel(X1, X2)) -> MARK(X2)
MARK(sel(X1, X2)) -> MARK(X1)
ASEL(s(N), cons(X, XS)) -> MARK(N)
ASEL(s(N), cons(X, XS)) -> ASEL(mark(N), mark(XS))
MARK(sel(X1, X2)) -> ASEL(mark(X1), mark(X2))
MARK(fib(X)) -> MARK(X)
AFIB(N) -> MARK(N)
MARK(fib(X)) -> AFIB(mark(X))
ASEL(0, cons(X, XS)) -> MARK(X)
AFIB(N) -> ASEL(mark(N), afib1(s(0), s(0)))


Rules:


afib(N) -> asel(mark(N), afib1(s(0), s(0)))
afib(X) -> fib(X)
afib1(X, Y) -> cons(mark(X), fib1(Y, add(X, Y)))
afib1(X1, X2) -> fib1(X1, X2)
aadd(0, X) -> mark(X)
aadd(s(X), Y) -> s(aadd(mark(X), mark(Y)))
aadd(X1, X2) -> add(X1, X2)
asel(0, cons(X, XS)) -> mark(X)
asel(s(N), cons(X, XS)) -> asel(mark(N), mark(XS))
asel(X1, X2) -> sel(X1, X2)
mark(fib(X)) -> afib(mark(X))
mark(sel(X1, X2)) -> asel(mark(X1), mark(X2))
mark(fib1(X1, X2)) -> afib1(mark(X1), mark(X2))
mark(add(X1, X2)) -> aadd(mark(X1), mark(X2))
mark(s(X)) -> s(mark(X))
mark(0) -> 0
mark(cons(X1, X2)) -> cons(mark(X1), X2)


Strategy:

innermost



The Proof could not be continued due to a Timeout.
Innermost Termination of R could not be shown.
Duration:
1:00 minutes