R
↳Dependency Pair Analysis
AFROM(X) -> MARK(X)
ALENGTH(cons(X, Y)) -> ALENGTH1(Y)
ALENGTH1(X) -> ALENGTH(X)
MARK(from(X)) -> AFROM(mark(X))
MARK(from(X)) -> MARK(X)
MARK(length(X)) -> ALENGTH(X)
MARK(length1(X)) -> ALENGTH1(X)
MARK(cons(X1, X2)) -> MARK(X1)
MARK(s(X)) -> MARK(X)
R
↳DPs
→DP Problem 1
↳Argument Filtering and Ordering
→DP Problem 2
↳AFS
ALENGTH1(X) -> ALENGTH(X)
ALENGTH(cons(X, Y)) -> ALENGTH1(Y)
afrom(X) -> cons(mark(X), from(s(X)))
afrom(X) -> from(X)
alength(nil) -> 0
alength(cons(X, Y)) -> s(alength1(Y))
alength(X) -> length(X)
alength1(X) -> alength(X)
alength1(X) -> length1(X)
mark(from(X)) -> afrom(mark(X))
mark(length(X)) -> alength(X)
mark(length1(X)) -> alength1(X)
mark(cons(X1, X2)) -> cons(mark(X1), X2)
mark(s(X)) -> s(mark(X))
mark(nil) -> nil
mark(0) -> 0
ALENGTH1(X) -> ALENGTH(X)
POL(A__LENGTH1(x1)) = 1 + x1 POL(cons(x1, x2)) = 1 + x1 + x2 POL(A__LENGTH(x1)) = x1
ALENGTH1(x1) -> ALENGTH1(x1)
ALENGTH(x1) -> ALENGTH(x1)
cons(x1, x2) -> cons(x1, x2)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 3
↳Dependency Graph
→DP Problem 2
↳AFS
ALENGTH(cons(X, Y)) -> ALENGTH1(Y)
afrom(X) -> cons(mark(X), from(s(X)))
afrom(X) -> from(X)
alength(nil) -> 0
alength(cons(X, Y)) -> s(alength1(Y))
alength(X) -> length(X)
alength1(X) -> alength(X)
alength1(X) -> length1(X)
mark(from(X)) -> afrom(mark(X))
mark(length(X)) -> alength(X)
mark(length1(X)) -> alength1(X)
mark(cons(X1, X2)) -> cons(mark(X1), X2)
mark(s(X)) -> s(mark(X))
mark(nil) -> nil
mark(0) -> 0
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Argument Filtering and Ordering
MARK(s(X)) -> MARK(X)
MARK(cons(X1, X2)) -> MARK(X1)
MARK(from(X)) -> MARK(X)
MARK(from(X)) -> AFROM(mark(X))
AFROM(X) -> MARK(X)
afrom(X) -> cons(mark(X), from(s(X)))
afrom(X) -> from(X)
alength(nil) -> 0
alength(cons(X, Y)) -> s(alength1(Y))
alength(X) -> length(X)
alength1(X) -> alength(X)
alength1(X) -> length1(X)
mark(from(X)) -> afrom(mark(X))
mark(length(X)) -> alength(X)
mark(length1(X)) -> alength1(X)
mark(cons(X1, X2)) -> cons(mark(X1), X2)
mark(s(X)) -> s(mark(X))
mark(nil) -> nil
mark(0) -> 0
MARK(from(X)) -> MARK(X)
MARK(from(X)) -> AFROM(mark(X))
mark(from(X)) -> afrom(mark(X))
mark(length(X)) -> alength(X)
mark(length1(X)) -> alength1(X)
mark(cons(X1, X2)) -> cons(mark(X1), X2)
mark(s(X)) -> s(mark(X))
mark(nil) -> nil
mark(0) -> 0
afrom(X) -> cons(mark(X), from(s(X)))
afrom(X) -> from(X)
alength(nil) -> 0
alength(cons(X, Y)) -> s(alength1(Y))
alength(X) -> length(X)
alength1(X) -> alength(X)
alength1(X) -> length1(X)
POL(from(x1)) = 1 + x1 POL(MARK(x1)) = x1 POL(a__length) = 0 POL(0) = 0 POL(A__FROM(x1)) = x1 POL(nil) = 0 POL(s(x1)) = x1 POL(mark(x1)) = x1 POL(a__from(x1)) = 1 + x1 POL(a__length1) = 0 POL(length) = 0 POL(length1) = 0
MARK(x1) -> MARK(x1)
from(x1) -> from(x1)
AFROM(x1) -> AFROM(x1)
s(x1) -> s(x1)
cons(x1, x2) -> x1
mark(x1) -> mark(x1)
afrom(x1) -> afrom(x1)
length(x1) -> length
alength(x1) -> alength
length1(x1) -> length1
alength1(x1) -> alength1
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 4
↳Dependency Graph
MARK(s(X)) -> MARK(X)
MARK(cons(X1, X2)) -> MARK(X1)
AFROM(X) -> MARK(X)
afrom(X) -> cons(mark(X), from(s(X)))
afrom(X) -> from(X)
alength(nil) -> 0
alength(cons(X, Y)) -> s(alength1(Y))
alength(X) -> length(X)
alength1(X) -> alength(X)
alength1(X) -> length1(X)
mark(from(X)) -> afrom(mark(X))
mark(length(X)) -> alength(X)
mark(length1(X)) -> alength1(X)
mark(cons(X1, X2)) -> cons(mark(X1), X2)
mark(s(X)) -> s(mark(X))
mark(nil) -> nil
mark(0) -> 0
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 4
↳DGraph
...
→DP Problem 5
↳Argument Filtering and Ordering
MARK(cons(X1, X2)) -> MARK(X1)
MARK(s(X)) -> MARK(X)
afrom(X) -> cons(mark(X), from(s(X)))
afrom(X) -> from(X)
alength(nil) -> 0
alength(cons(X, Y)) -> s(alength1(Y))
alength(X) -> length(X)
alength1(X) -> alength(X)
alength1(X) -> length1(X)
mark(from(X)) -> afrom(mark(X))
mark(length(X)) -> alength(X)
mark(length1(X)) -> alength1(X)
mark(cons(X1, X2)) -> cons(mark(X1), X2)
mark(s(X)) -> s(mark(X))
mark(nil) -> nil
mark(0) -> 0
MARK(s(X)) -> MARK(X)
POL(MARK(x1)) = x1 POL(cons(x1, x2)) = x1 + x2 POL(s(x1)) = 1 + x1
MARK(x1) -> MARK(x1)
s(x1) -> s(x1)
cons(x1, x2) -> cons(x1, x2)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 4
↳DGraph
...
→DP Problem 6
↳Argument Filtering and Ordering
MARK(cons(X1, X2)) -> MARK(X1)
afrom(X) -> cons(mark(X), from(s(X)))
afrom(X) -> from(X)
alength(nil) -> 0
alength(cons(X, Y)) -> s(alength1(Y))
alength(X) -> length(X)
alength1(X) -> alength(X)
alength1(X) -> length1(X)
mark(from(X)) -> afrom(mark(X))
mark(length(X)) -> alength(X)
mark(length1(X)) -> alength1(X)
mark(cons(X1, X2)) -> cons(mark(X1), X2)
mark(s(X)) -> s(mark(X))
mark(nil) -> nil
mark(0) -> 0
MARK(cons(X1, X2)) -> MARK(X1)
POL(MARK(x1)) = x1 POL(cons(x1, x2)) = 1 + x1 + x2
MARK(x1) -> MARK(x1)
cons(x1, x2) -> cons(x1, x2)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 4
↳DGraph
...
→DP Problem 7
↳Dependency Graph
afrom(X) -> cons(mark(X), from(s(X)))
afrom(X) -> from(X)
alength(nil) -> 0
alength(cons(X, Y)) -> s(alength1(Y))
alength(X) -> length(X)
alength1(X) -> alength(X)
alength1(X) -> length1(X)
mark(from(X)) -> afrom(mark(X))
mark(length(X)) -> alength(X)
mark(length1(X)) -> alength1(X)
mark(cons(X1, X2)) -> cons(mark(X1), X2)
mark(s(X)) -> s(mark(X))
mark(nil) -> nil
mark(0) -> 0