R
↳Dependency Pair Analysis
PURGE(.(x, y)) -> PURGE(remove(x, y))
PURGE(.(x, y)) -> REMOVE(x, y)
REMOVE(x, .(y, z)) -> REMOVE(x, z)
R
↳DPs
→DP Problem 1
↳Polynomial Ordering
→DP Problem 2
↳Polo
REMOVE(x, .(y, z)) -> REMOVE(x, z)
purge(nil) -> nil
purge(.(x, y)) -> .(x, purge(remove(x, y)))
remove(x, nil) -> nil
remove(x, .(y, z)) -> if(=(x, y), remove(x, z), .(y, remove(x, z)))
REMOVE(x, .(y, z)) -> REMOVE(x, z)
purge(nil) -> nil
purge(.(x, y)) -> .(x, purge(remove(x, y)))
remove(x, nil) -> nil
remove(x, .(y, z)) -> if(=(x, y), remove(x, z), .(y, remove(x, z)))
POL(remove(x1, x2)) = 0 POL(REMOVE(x1, x2)) = 1 + x2 POL(if(x1, x2, x3)) = 0 POL(=(x1, x2)) = 0 POL(nil) = 0 POL(.(x1, x2)) = 1 + x2 POL(purge(x1)) = x1
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 3
↳Dependency Graph
→DP Problem 2
↳Polo
purge(nil) -> nil
purge(.(x, y)) -> .(x, purge(remove(x, y)))
remove(x, nil) -> nil
remove(x, .(y, z)) -> if(=(x, y), remove(x, z), .(y, remove(x, z)))
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polynomial Ordering
PURGE(.(x, y)) -> PURGE(remove(x, y))
purge(nil) -> nil
purge(.(x, y)) -> .(x, purge(remove(x, y)))
remove(x, nil) -> nil
remove(x, .(y, z)) -> if(=(x, y), remove(x, z), .(y, remove(x, z)))
PURGE(.(x, y)) -> PURGE(remove(x, y))
purge(nil) -> nil
purge(.(x, y)) -> .(x, purge(remove(x, y)))
remove(x, nil) -> nil
remove(x, .(y, z)) -> if(=(x, y), remove(x, z), .(y, remove(x, z)))
POL(remove(x1, x2)) = 0 POL(if(x1, x2, x3)) = 0 POL(PURGE(x1)) = x1 POL(=(x1, x2)) = 0 POL(nil) = 0 POL(.(x1, x2)) = 1 POL(purge(x1)) = 1
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polo
→DP Problem 4
↳Dependency Graph
purge(nil) -> nil
purge(.(x, y)) -> .(x, purge(remove(x, y)))
remove(x, nil) -> nil
remove(x, .(y, z)) -> if(=(x, y), remove(x, z), .(y, remove(x, z)))