R
↳Dependency Pair Analysis
INCR(cons(X, L)) -> INCR(L)
ADX(cons(X, L)) -> INCR(cons(X, adx(L)))
ADX(cons(X, L)) -> ADX(L)
NATS -> ADX(zeros)
NATS -> ZEROS
ZEROS -> ZEROS
R
↳DPs
→DP Problem 1
↳Argument Filtering and Ordering
→DP Problem 2
↳Remaining
→DP Problem 3
↳Remaining
INCR(cons(X, L)) -> INCR(L)
incr(nil) -> nil
incr(cons(X, L)) -> cons(s(X), incr(L))
adx(nil) -> nil
adx(cons(X, L)) -> incr(cons(X, adx(L)))
nats -> adx(zeros)
zeros -> cons(0, zeros)
head(cons(X, L)) -> X
tail(cons(X, L)) -> L
innermost
INCR(cons(X, L)) -> INCR(L)
POL(cons(x1, x2)) = 1 + x1 + x2 POL(INCR(x1)) = x1
INCR(x1) -> INCR(x1)
cons(x1, x2) -> cons(x1, x2)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 4
↳Dependency Graph
→DP Problem 2
↳Remaining
→DP Problem 3
↳Remaining
incr(nil) -> nil
incr(cons(X, L)) -> cons(s(X), incr(L))
adx(nil) -> nil
adx(cons(X, L)) -> incr(cons(X, adx(L)))
nats -> adx(zeros)
zeros -> cons(0, zeros)
head(cons(X, L)) -> X
tail(cons(X, L)) -> L
innermost
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Remaining Obligation(s)
→DP Problem 3
↳Remaining Obligation(s)
ZEROS -> ZEROS
incr(nil) -> nil
incr(cons(X, L)) -> cons(s(X), incr(L))
adx(nil) -> nil
adx(cons(X, L)) -> incr(cons(X, adx(L)))
nats -> adx(zeros)
zeros -> cons(0, zeros)
head(cons(X, L)) -> X
tail(cons(X, L)) -> L
innermost
ADX(cons(X, L)) -> ADX(L)
incr(nil) -> nil
incr(cons(X, L)) -> cons(s(X), incr(L))
adx(nil) -> nil
adx(cons(X, L)) -> incr(cons(X, adx(L)))
nats -> adx(zeros)
zeros -> cons(0, zeros)
head(cons(X, L)) -> X
tail(cons(X, L)) -> L
innermost
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Remaining Obligation(s)
→DP Problem 3
↳Remaining Obligation(s)
ZEROS -> ZEROS
incr(nil) -> nil
incr(cons(X, L)) -> cons(s(X), incr(L))
adx(nil) -> nil
adx(cons(X, L)) -> incr(cons(X, adx(L)))
nats -> adx(zeros)
zeros -> cons(0, zeros)
head(cons(X, L)) -> X
tail(cons(X, L)) -> L
innermost
ADX(cons(X, L)) -> ADX(L)
incr(nil) -> nil
incr(cons(X, L)) -> cons(s(X), incr(L))
adx(nil) -> nil
adx(cons(X, L)) -> incr(cons(X, adx(L)))
nats -> adx(zeros)
zeros -> cons(0, zeros)
head(cons(X, L)) -> X
tail(cons(X, L)) -> L
innermost