R
↳Dependency Pair Analysis
AF(g(X), Y) -> AF(mark(X), f(g(X), Y))
AF(g(X), Y) -> MARK(X)
MARK(f(X1, X2)) -> AF(mark(X1), X2)
MARK(f(X1, X2)) -> MARK(X1)
MARK(g(X)) -> MARK(X)
R
↳DPs
→DP Problem 1
↳Argument Filtering and Ordering
MARK(g(X)) -> MARK(X)
MARK(f(X1, X2)) -> MARK(X1)
MARK(f(X1, X2)) -> AF(mark(X1), X2)
AF(g(X), Y) -> MARK(X)
AF(g(X), Y) -> AF(mark(X), f(g(X), Y))
af(g(X), Y) -> af(mark(X), f(g(X), Y))
af(X1, X2) -> f(X1, X2)
mark(f(X1, X2)) -> af(mark(X1), X2)
mark(g(X)) -> g(mark(X))
MARK(g(X)) -> MARK(X)
MARK(f(X1, X2)) -> AF(mark(X1), X2)
AF(g(X), Y) -> AF(mark(X), f(g(X), Y))
mark(f(X1, X2)) -> af(mark(X1), X2)
mark(g(X)) -> g(mark(X))
af(g(X), Y) -> af(mark(X), f(g(X), Y))
af(X1, X2) -> f(X1, X2)
POL(MARK(x1)) = 1 + x1 POL(g(x1)) = 1 + x1 POL(mark(x1)) = x1
MARK(x1) -> MARK(x1)
AF(x1, x2) -> x1
f(x1, x2) -> x1
mark(x1) -> mark(x1)
g(x1) -> g(x1)
af(x1, x2) -> x1
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Dependency Graph
MARK(f(X1, X2)) -> MARK(X1)
AF(g(X), Y) -> MARK(X)
af(g(X), Y) -> af(mark(X), f(g(X), Y))
af(X1, X2) -> f(X1, X2)
mark(f(X1, X2)) -> af(mark(X1), X2)
mark(g(X)) -> g(mark(X))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳DGraph
...
→DP Problem 3
↳Argument Filtering and Ordering
MARK(f(X1, X2)) -> MARK(X1)
af(g(X), Y) -> af(mark(X), f(g(X), Y))
af(X1, X2) -> f(X1, X2)
mark(f(X1, X2)) -> af(mark(X1), X2)
mark(g(X)) -> g(mark(X))
MARK(f(X1, X2)) -> MARK(X1)
POL(MARK(x1)) = x1 POL(f(x1, x2)) = 1 + x1 + x2
MARK(x1) -> MARK(x1)
f(x1, x2) -> f(x1, x2)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳DGraph
...
→DP Problem 4
↳Dependency Graph
af(g(X), Y) -> af(mark(X), f(g(X), Y))
af(X1, X2) -> f(X1, X2)
mark(f(X1, X2)) -> af(mark(X1), X2)
mark(g(X)) -> g(mark(X))