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
innermost
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
innermost
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
innermost
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
innermost
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
innermost
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
innermost
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
↳Forward Instantiation 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
innermost
three new Dependency Pairs are created:
SEL(s(X), cons(Y, Z')) -> SEL(X, Z')
SEL(s(s(X'')), cons(Y, cons(Y'', nf(X'''')))) -> SEL(s(X''), cons(Y'', nf(X'''')))
SEL(s(s(X'')), cons(Y, cons(Y'', ng(X'''')))) -> SEL(s(X''), cons(Y'', ng(X'''')))
SEL(s(s(X'')), cons(Y, cons(Y'', Z'''))) -> SEL(s(X''), cons(Y'', Z'''))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳Nar
→DP Problem 7
↳FwdInst
...
→DP Problem 8
↳Argument Filtering and Ordering
SEL(s(s(X'')), cons(Y, cons(Y'', Z'''))) -> SEL(s(X''), cons(Y'', Z'''))
SEL(s(s(X'')), cons(Y, cons(Y'', ng(X'''')))) -> SEL(s(X''), cons(Y'', ng(X'''')))
SEL(s(s(X'')), cons(Y, cons(Y'', nf(X'''')))) -> SEL(s(X''), cons(Y'', nf(X'''')))
SEL(s(X), cons(Y, nf(X''))) -> SEL(X, f(activate(X'')))
SEL(s(X), cons(Y, ng(X''))) -> SEL(X, g(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
innermost
SEL(s(X), cons(Y, ng(X''))) -> SEL(X, g(activate(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
f(X) -> cons(X, nf(ng(X)))
f(X) -> nf(X)
POL(activate(x1)) = x1 POL(n__f) = 1 POL(0) = 0 POL(g) = 0 POL(SEL(x1, x2)) = 1 + 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
g(x1) -> g
f(x1) -> f
ng(x1) -> ng
activate(x1) -> activate(x1)
nf(x1) -> nf
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳Nar
→DP Problem 7
↳FwdInst
...
→DP Problem 9
↳Dependency Graph
SEL(s(s(X'')), cons(Y, cons(Y'', Z'''))) -> SEL(s(X''), cons(Y'', Z'''))
SEL(s(s(X'')), cons(Y, cons(Y'', ng(X'''')))) -> SEL(s(X''), cons(Y'', ng(X'''')))
SEL(s(s(X'')), cons(Y, cons(Y'', nf(X'''')))) -> SEL(s(X''), cons(Y'', nf(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
innermost
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳Nar
→DP Problem 7
↳FwdInst
...
→DP Problem 10
↳Argument Filtering and Ordering
SEL(s(s(X'')), cons(Y, cons(Y'', nf(X'''')))) -> SEL(s(X''), cons(Y'', nf(X'''')))
SEL(s(X), cons(Y, nf(X''))) -> SEL(X, f(activate(X'')))
SEL(s(s(X'')), cons(Y, cons(Y'', Z'''))) -> SEL(s(X''), cons(Y'', 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
innermost
SEL(s(s(X'')), cons(Y, cons(Y'', nf(X'''')))) -> SEL(s(X''), cons(Y'', nf(X'''')))
SEL(s(s(X'')), cons(Y, cons(Y'', Z'''))) -> SEL(s(X''), cons(Y'', Z'''))
f(X) -> cons(X, nf(ng(X)))
f(X) -> nf(X)
activate(nf(X)) -> f(activate(X))
activate(ng(X)) -> g(activate(X))
activate(X) -> X
g(0) -> s(0)
g(s(X)) -> s(s(g(X)))
g(X) -> ng(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
activate(x1) -> activate(x1)
ng(x1) -> ng(x1)
g(x1) -> g(x1)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳Nar
→DP Problem 7
↳FwdInst
...
→DP Problem 11
↳Remaining Obligation(s)
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
innermost