R
↳Dependency Pair Analysis
G(s(X)) -> G(X)
SEL(s(X), cons(Y, Z)) -> SEL(X, activate(Z))
SEL(s(X), cons(Y, Z)) -> ACTIVATE(Z)
ACTIVATE(nf(X)) -> F(activate(X))
ACTIVATE(nf(X)) -> ACTIVATE(X)
ACTIVATE(ng(X)) -> G(activate(X))
ACTIVATE(ng(X)) -> ACTIVATE(X)
R
↳DPs
→DP Problem 1
↳Argument Filtering and Ordering
→DP Problem 2
↳AFS
→DP Problem 3
↳Nar
G(s(X)) -> G(X)
f(X) -> cons(X, nf(ng(X)))
f(X) -> nf(X)
g(0) -> s(0)
g(s(X)) -> s(s(g(X)))
g(X) -> ng(X)
sel(0, cons(X, Y)) -> X
sel(s(X), cons(Y, Z)) -> sel(X, activate(Z))
activate(nf(X)) -> f(activate(X))
activate(ng(X)) -> g(activate(X))
activate(X) -> X
G(s(X)) -> G(X)
POL(G(x1)) = x1 POL(s(x1)) = 1 + x1
G(x1) -> G(x1)
s(x1) -> s(x1)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 4
↳Dependency Graph
→DP Problem 2
↳AFS
→DP Problem 3
↳Nar
f(X) -> cons(X, nf(ng(X)))
f(X) -> nf(X)
g(0) -> s(0)
g(s(X)) -> s(s(g(X)))
g(X) -> ng(X)
sel(0, cons(X, Y)) -> X
sel(s(X), cons(Y, Z)) -> sel(X, activate(Z))
activate(nf(X)) -> f(activate(X))
activate(ng(X)) -> g(activate(X))
activate(X) -> X
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Argument Filtering and Ordering
→DP Problem 3
↳Nar
ACTIVATE(ng(X)) -> ACTIVATE(X)
ACTIVATE(nf(X)) -> ACTIVATE(X)
f(X) -> cons(X, nf(ng(X)))
f(X) -> nf(X)
g(0) -> s(0)
g(s(X)) -> s(s(g(X)))
g(X) -> ng(X)
sel(0, cons(X, Y)) -> X
sel(s(X), cons(Y, Z)) -> sel(X, activate(Z))
activate(nf(X)) -> f(activate(X))
activate(ng(X)) -> g(activate(X))
activate(X) -> X
ACTIVATE(ng(X)) -> ACTIVATE(X)
POL(n__f(x1)) = x1 POL(n__g(x1)) = 1 + x1 POL(ACTIVATE(x1)) = x1
ACTIVATE(x1) -> ACTIVATE(x1)
ng(x1) -> ng(x1)
nf(x1) -> nf(x1)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 5
↳Argument Filtering and Ordering
→DP Problem 3
↳Nar
ACTIVATE(nf(X)) -> ACTIVATE(X)
f(X) -> cons(X, nf(ng(X)))
f(X) -> nf(X)
g(0) -> s(0)
g(s(X)) -> s(s(g(X)))
g(X) -> ng(X)
sel(0, cons(X, Y)) -> X
sel(s(X), cons(Y, Z)) -> sel(X, activate(Z))
activate(nf(X)) -> f(activate(X))
activate(ng(X)) -> g(activate(X))
activate(X) -> X
ACTIVATE(nf(X)) -> ACTIVATE(X)
POL(n__f(x1)) = 1 + x1 POL(ACTIVATE(x1)) = x1
ACTIVATE(x1) -> ACTIVATE(x1)
nf(x1) -> nf(x1)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 5
↳AFS
...
→DP Problem 6
↳Dependency Graph
→DP Problem 3
↳Nar
f(X) -> cons(X, nf(ng(X)))
f(X) -> nf(X)
g(0) -> s(0)
g(s(X)) -> s(s(g(X)))
g(X) -> ng(X)
sel(0, cons(X, Y)) -> X
sel(s(X), cons(Y, Z)) -> sel(X, activate(Z))
activate(nf(X)) -> f(activate(X))
activate(ng(X)) -> g(activate(X))
activate(X) -> X
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳Narrowing Transformation
SEL(s(X), cons(Y, Z)) -> SEL(X, activate(Z))
f(X) -> cons(X, nf(ng(X)))
f(X) -> nf(X)
g(0) -> s(0)
g(s(X)) -> s(s(g(X)))
g(X) -> ng(X)
sel(0, cons(X, Y)) -> X
sel(s(X), cons(Y, Z)) -> sel(X, activate(Z))
activate(nf(X)) -> f(activate(X))
activate(ng(X)) -> g(activate(X))
activate(X) -> X
three new Dependency Pairs are created:
SEL(s(X), cons(Y, Z)) -> SEL(X, activate(Z))
SEL(s(X), cons(Y, nf(X''))) -> SEL(X, f(activate(X'')))
SEL(s(X), cons(Y, ng(X''))) -> SEL(X, g(activate(X'')))
SEL(s(X), cons(Y, Z')) -> SEL(X, Z')
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳Nar
→DP Problem 7
↳Narrowing Transformation
SEL(s(X), cons(Y, Z')) -> SEL(X, Z')
SEL(s(X), cons(Y, ng(X''))) -> SEL(X, g(activate(X'')))
SEL(s(X), cons(Y, nf(X''))) -> SEL(X, f(activate(X'')))
f(X) -> cons(X, nf(ng(X)))
f(X) -> nf(X)
g(0) -> s(0)
g(s(X)) -> s(s(g(X)))
g(X) -> ng(X)
sel(0, cons(X, Y)) -> X
sel(s(X), cons(Y, Z)) -> sel(X, activate(Z))
activate(nf(X)) -> f(activate(X))
activate(ng(X)) -> g(activate(X))
activate(X) -> X
five new Dependency Pairs are created:
SEL(s(X), cons(Y, nf(X''))) -> SEL(X, f(activate(X'')))
SEL(s(X), cons(Y, nf(X'''))) -> SEL(X, cons(activate(X'''), nf(ng(activate(X''')))))
SEL(s(X), cons(Y, nf(X'''))) -> SEL(X, nf(activate(X''')))
SEL(s(X), cons(Y, nf(nf(X''')))) -> SEL(X, f(f(activate(X'''))))
SEL(s(X), cons(Y, nf(ng(X''')))) -> SEL(X, f(g(activate(X'''))))
SEL(s(X), cons(Y, nf(X'''))) -> SEL(X, f(X'''))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳Nar
→DP Problem 7
↳Nar
...
→DP Problem 8
↳Narrowing Transformation
SEL(s(X), cons(Y, nf(X'''))) -> SEL(X, f(X'''))
SEL(s(X), cons(Y, nf(nf(X''')))) -> SEL(X, f(f(activate(X'''))))
SEL(s(X), cons(Y, nf(ng(X''')))) -> SEL(X, f(g(activate(X'''))))
SEL(s(X), cons(Y, nf(X'''))) -> SEL(X, cons(activate(X'''), nf(ng(activate(X''')))))
SEL(s(X), cons(Y, ng(X''))) -> SEL(X, g(activate(X'')))
SEL(s(X), cons(Y, Z')) -> SEL(X, Z')
f(X) -> cons(X, nf(ng(X)))
f(X) -> nf(X)
g(0) -> s(0)
g(s(X)) -> s(s(g(X)))
g(X) -> ng(X)
sel(0, cons(X, Y)) -> X
sel(s(X), cons(Y, Z)) -> sel(X, activate(Z))
activate(nf(X)) -> f(activate(X))
activate(ng(X)) -> g(activate(X))
activate(X) -> X
four new Dependency Pairs are created:
SEL(s(X), cons(Y, ng(X''))) -> SEL(X, g(activate(X'')))
SEL(s(X), cons(Y, ng(X'''))) -> SEL(X, ng(activate(X''')))
SEL(s(X), cons(Y, ng(nf(X''')))) -> SEL(X, g(f(activate(X'''))))
SEL(s(X), cons(Y, ng(ng(X''')))) -> SEL(X, g(g(activate(X'''))))
SEL(s(X), cons(Y, ng(X'''))) -> SEL(X, g(X'''))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳Nar
→DP Problem 7
↳Nar
...
→DP Problem 9
↳Argument Filtering and Ordering
SEL(s(X), cons(Y, ng(X'''))) -> SEL(X, g(X'''))
SEL(s(X), cons(Y, ng(ng(X''')))) -> SEL(X, g(g(activate(X'''))))
SEL(s(X), cons(Y, ng(nf(X''')))) -> SEL(X, g(f(activate(X'''))))
SEL(s(X), cons(Y, nf(nf(X''')))) -> SEL(X, f(f(activate(X'''))))
SEL(s(X), cons(Y, nf(ng(X''')))) -> SEL(X, f(g(activate(X'''))))
SEL(s(X), cons(Y, nf(X'''))) -> SEL(X, cons(activate(X'''), nf(ng(activate(X''')))))
SEL(s(X), cons(Y, Z')) -> SEL(X, Z')
SEL(s(X), cons(Y, nf(X'''))) -> SEL(X, f(X'''))
f(X) -> cons(X, nf(ng(X)))
f(X) -> nf(X)
g(0) -> s(0)
g(s(X)) -> s(s(g(X)))
g(X) -> ng(X)
sel(0, cons(X, Y)) -> X
sel(s(X), cons(Y, Z)) -> sel(X, activate(Z))
activate(nf(X)) -> f(activate(X))
activate(ng(X)) -> g(activate(X))
activate(X) -> X
SEL(s(X), cons(Y, ng(X'''))) -> SEL(X, g(X'''))
SEL(s(X), cons(Y, Z')) -> SEL(X, Z')
f(X) -> cons(X, nf(ng(X)))
f(X) -> nf(X)
g(0) -> s(0)
g(s(X)) -> s(s(g(X)))
g(X) -> ng(X)
activate(nf(X)) -> f(activate(X))
activate(ng(X)) -> g(activate(X))
activate(X) -> X
POL(n__f) = 0 POL(activate(x1)) = 1 + x1 POL(0) = 0 POL(g(x1)) = x1 POL(SEL(x1, x2)) = 1 + x1 + x2 POL(cons(x1)) = 1 + x1 POL(s(x1)) = x1 POL(n__g(x1)) = x1 POL(f) = 1
SEL(x1, x2) -> SEL(x1, x2)
s(x1) -> s(x1)
cons(x1, x2) -> cons(x2)
nf(x1) -> nf
f(x1) -> f
ng(x1) -> ng(x1)
g(x1) -> g(x1)
activate(x1) -> activate(x1)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳Nar
→DP Problem 7
↳Nar
...
→DP Problem 10
↳Argument Filtering and Ordering
SEL(s(X), cons(Y, ng(ng(X''')))) -> SEL(X, g(g(activate(X'''))))
SEL(s(X), cons(Y, ng(nf(X''')))) -> SEL(X, g(f(activate(X'''))))
SEL(s(X), cons(Y, nf(nf(X''')))) -> SEL(X, f(f(activate(X'''))))
SEL(s(X), cons(Y, nf(ng(X''')))) -> SEL(X, f(g(activate(X'''))))
SEL(s(X), cons(Y, nf(X'''))) -> SEL(X, cons(activate(X'''), nf(ng(activate(X''')))))
SEL(s(X), cons(Y, nf(X'''))) -> SEL(X, f(X'''))
f(X) -> cons(X, nf(ng(X)))
f(X) -> nf(X)
g(0) -> s(0)
g(s(X)) -> s(s(g(X)))
g(X) -> ng(X)
sel(0, cons(X, Y)) -> X
sel(s(X), cons(Y, Z)) -> sel(X, activate(Z))
activate(nf(X)) -> f(activate(X))
activate(ng(X)) -> g(activate(X))
activate(X) -> X
SEL(s(X), cons(Y, ng(ng(X''')))) -> SEL(X, g(g(activate(X'''))))
SEL(s(X), cons(Y, ng(nf(X''')))) -> SEL(X, g(f(activate(X'''))))
f(X) -> cons(X, nf(ng(X)))
f(X) -> nf(X)
g(0) -> s(0)
g(s(X)) -> s(s(g(X)))
g(X) -> ng(X)
POL(n__f) = 0 POL(0) = 0 POL(g) = 0 POL(SEL(x1, x2)) = x1 + x2 POL(cons) = 1 POL(s(x1)) = x1 POL(n__g) = 0 POL(f) = 1
SEL(x1, x2) -> SEL(x1, x2)
s(x1) -> s(x1)
cons(x1, x2) -> cons
f(x1) -> f
g(x1) -> g
nf(x1) -> nf
ng(x1) -> ng
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳Nar
→DP Problem 7
↳Nar
...
→DP Problem 11
↳Argument Filtering and Ordering
SEL(s(X), cons(Y, nf(nf(X''')))) -> SEL(X, f(f(activate(X'''))))
SEL(s(X), cons(Y, nf(ng(X''')))) -> SEL(X, f(g(activate(X'''))))
SEL(s(X), cons(Y, nf(X'''))) -> SEL(X, cons(activate(X'''), nf(ng(activate(X''')))))
SEL(s(X), cons(Y, nf(X'''))) -> SEL(X, f(X'''))
f(X) -> cons(X, nf(ng(X)))
f(X) -> nf(X)
g(0) -> s(0)
g(s(X)) -> s(s(g(X)))
g(X) -> ng(X)
sel(0, cons(X, Y)) -> X
sel(s(X), cons(Y, Z)) -> sel(X, activate(Z))
activate(nf(X)) -> f(activate(X))
activate(ng(X)) -> g(activate(X))
activate(X) -> X
SEL(s(X), cons(Y, nf(nf(X''')))) -> SEL(X, f(f(activate(X'''))))
SEL(s(X), cons(Y, nf(ng(X''')))) -> SEL(X, f(g(activate(X'''))))
SEL(s(X), cons(Y, nf(X'''))) -> SEL(X, cons(activate(X'''), nf(ng(activate(X''')))))
SEL(s(X), cons(Y, nf(X'''))) -> SEL(X, f(X'''))
f(X) -> cons(X, nf(ng(X)))
f(X) -> nf(X)
POL(n__f) = 0 POL(SEL(x1, x2)) = x1 + x2 POL(s(x1)) = 1 + x1 POL(f) = 0
SEL(x1, x2) -> SEL(x1, x2)
s(x1) -> s(x1)
cons(x1, x2) -> x2
nf(x1) -> nf
f(x1) -> f
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳Nar
→DP Problem 7
↳Nar
...
→DP Problem 12
↳Dependency Graph
f(X) -> cons(X, nf(ng(X)))
f(X) -> nf(X)
g(0) -> s(0)
g(s(X)) -> s(s(g(X)))
g(X) -> ng(X)
sel(0, cons(X, Y)) -> X
sel(s(X), cons(Y, Z)) -> sel(X, activate(Z))
activate(nf(X)) -> f(activate(X))
activate(ng(X)) -> g(activate(X))
activate(X) -> X