R
↳Dependency Pair Analysis
F(X) -> IF(X, c, nf(true))
IF(false, X, Y) -> ACTIVATE(Y)
ACTIVATE(nf(X)) -> F(X)
R
↳DPs
→DP Problem 1
↳Polynomial Ordering
ACTIVATE(nf(X)) -> F(X)
IF(false, X, Y) -> ACTIVATE(Y)
F(X) -> IF(X, c, nf(true))
f(X) -> if(X, c, nf(true))
f(X) -> nf(X)
if(true, X, Y) -> X
if(false, X, Y) -> activate(Y)
activate(nf(X)) -> f(X)
activate(X) -> X
ACTIVATE(nf(X)) -> F(X)
f(X) -> if(X, c, nf(true))
f(X) -> nf(X)
if(true, X, Y) -> X
if(false, X, Y) -> activate(Y)
activate(nf(X)) -> f(X)
activate(X) -> X
POL(n__f(x1)) = x1 POL(activate(x1)) = x1 POL(if(x1, x2, x3)) = x2 + x3 POL(c) = 0 POL(false) = 1 POL(true) = 0 POL(ACTIVATE(x1)) = 1 + x1 POL(f(x1)) = x1 POL(F(x1)) = x1 POL(IF(x1, x2, x3)) = x1 + x3
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Dependency Graph
IF(false, X, Y) -> ACTIVATE(Y)
F(X) -> IF(X, c, nf(true))
f(X) -> if(X, c, nf(true))
f(X) -> nf(X)
if(true, X, Y) -> X
if(false, X, Y) -> activate(Y)
activate(nf(X)) -> f(X)
activate(X) -> X