R
↳Dependency Pair Analysis
ACTIVE(f(X, g(X), Y)) -> F(Y, Y, Y)
ACTIVE(g(X)) -> G(active(X))
ACTIVE(g(X)) -> ACTIVE(X)
G(mark(X)) -> G(X)
G(ok(X)) -> G(X)
PROPER(f(X1, X2, X3)) -> F(proper(X1), proper(X2), proper(X3))
PROPER(f(X1, X2, X3)) -> PROPER(X1)
PROPER(f(X1, X2, X3)) -> PROPER(X2)
PROPER(f(X1, X2, X3)) -> PROPER(X3)
PROPER(g(X)) -> G(proper(X))
PROPER(g(X)) -> PROPER(X)
F(ok(X1), ok(X2), ok(X3)) -> F(X1, X2, X3)
TOP(mark(X)) -> TOP(proper(X))
TOP(mark(X)) -> PROPER(X)
TOP(ok(X)) -> TOP(active(X))
TOP(ok(X)) -> ACTIVE(X)
R
↳DPs
→DP Problem 1
↳Argument Filtering and Ordering
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳Remaining
F(ok(X1), ok(X2), ok(X3)) -> F(X1, X2, X3)
active(f(X, g(X), Y)) -> mark(f(Y, Y, Y))
active(g(b)) -> mark(c)
active(b) -> mark(c)
active(g(X)) -> g(active(X))
g(mark(X)) -> mark(g(X))
g(ok(X)) -> ok(g(X))
proper(f(X1, X2, X3)) -> f(proper(X1), proper(X2), proper(X3))
proper(g(X)) -> g(proper(X))
proper(b) -> ok(b)
proper(c) -> ok(c)
f(ok(X1), ok(X2), ok(X3)) -> ok(f(X1, X2, X3))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))
F(ok(X1), ok(X2), ok(X3)) -> F(X1, X2, X3)
active(f(X, g(X), Y)) -> mark(f(Y, Y, Y))
active(g(b)) -> mark(c)
active(b) -> mark(c)
active(g(X)) -> g(active(X))
g(mark(X)) -> mark(g(X))
g(ok(X)) -> ok(g(X))
proper(f(X1, X2, X3)) -> f(proper(X1), proper(X2), proper(X3))
proper(g(X)) -> g(proper(X))
proper(b) -> ok(b)
proper(c) -> ok(c)
f(ok(X1), ok(X2), ok(X3)) -> ok(f(X1, X2, X3))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))
POL(top(x1)) = x1 POL(active(x1)) = 1 + x1 POL(proper(x1)) = 1 + x1 POL(c) = 0 POL(g(x1)) = x1 POL(b) = 0 POL(mark(x1)) = 1 + x1 POL(ok(x1)) = 1 + x1 POL(F(x1, x2, x3)) = x1 + x2 + x3
F(x1, x2, x3) -> F(x1, x2, x3)
ok(x1) -> ok(x1)
active(x1) -> active(x1)
mark(x1) -> mark(x1)
f(x1, x2, x3) -> x3
g(x1) -> g(x1)
proper(x1) -> proper(x1)
top(x1) -> top(x1)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 6
↳Dependency Graph
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳Remaining
active(f(X, g(X), Y)) -> mark(f(Y, Y, Y))
active(g(b)) -> mark(c)
active(b) -> mark(c)
active(g(X)) -> g(active(X))
g(mark(X)) -> mark(g(X))
g(ok(X)) -> ok(g(X))
proper(f(X1, X2, X3)) -> f(proper(X1), proper(X2), proper(X3))
proper(g(X)) -> g(proper(X))
proper(b) -> ok(b)
proper(c) -> ok(c)
f(ok(X1), ok(X2), ok(X3)) -> ok(f(X1, X2, X3))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Argument Filtering and Ordering
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳Remaining
G(ok(X)) -> G(X)
G(mark(X)) -> G(X)
active(f(X, g(X), Y)) -> mark(f(Y, Y, Y))
active(g(b)) -> mark(c)
active(b) -> mark(c)
active(g(X)) -> g(active(X))
g(mark(X)) -> mark(g(X))
g(ok(X)) -> ok(g(X))
proper(f(X1, X2, X3)) -> f(proper(X1), proper(X2), proper(X3))
proper(g(X)) -> g(proper(X))
proper(b) -> ok(b)
proper(c) -> ok(c)
f(ok(X1), ok(X2), ok(X3)) -> ok(f(X1, X2, X3))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))
G(ok(X)) -> G(X)
G(mark(X)) -> G(X)
active(f(X, g(X), Y)) -> mark(f(Y, Y, Y))
active(g(b)) -> mark(c)
active(b) -> mark(c)
active(g(X)) -> g(active(X))
g(mark(X)) -> mark(g(X))
g(ok(X)) -> ok(g(X))
proper(f(X1, X2, X3)) -> f(proper(X1), proper(X2), proper(X3))
proper(g(X)) -> g(proper(X))
proper(b) -> ok(b)
proper(c) -> ok(c)
f(ok(X1), ok(X2), ok(X3)) -> ok(f(X1, X2, X3))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))
POL(top(x1)) = x1 POL(active(x1)) = 1 + x1 POL(proper(x1)) = 1 + x1 POL(c) = 0 POL(g(x1)) = x1 POL(G(x1)) = x1 POL(b) = 0 POL(mark(x1)) = 1 + x1 POL(ok(x1)) = 1 + x1
G(x1) -> G(x1)
ok(x1) -> ok(x1)
mark(x1) -> mark(x1)
active(x1) -> active(x1)
f(x1, x2, x3) -> x3
g(x1) -> g(x1)
proper(x1) -> proper(x1)
top(x1) -> top(x1)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 7
↳Dependency Graph
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳Remaining
active(f(X, g(X), Y)) -> mark(f(Y, Y, Y))
active(g(b)) -> mark(c)
active(b) -> mark(c)
active(g(X)) -> g(active(X))
g(mark(X)) -> mark(g(X))
g(ok(X)) -> ok(g(X))
proper(f(X1, X2, X3)) -> f(proper(X1), proper(X2), proper(X3))
proper(g(X)) -> g(proper(X))
proper(b) -> ok(b)
proper(c) -> ok(c)
f(ok(X1), ok(X2), ok(X3)) -> ok(f(X1, X2, X3))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳Argument Filtering and Ordering
→DP Problem 4
↳AFS
→DP Problem 5
↳Remaining
ACTIVE(g(X)) -> ACTIVE(X)
active(f(X, g(X), Y)) -> mark(f(Y, Y, Y))
active(g(b)) -> mark(c)
active(b) -> mark(c)
active(g(X)) -> g(active(X))
g(mark(X)) -> mark(g(X))
g(ok(X)) -> ok(g(X))
proper(f(X1, X2, X3)) -> f(proper(X1), proper(X2), proper(X3))
proper(g(X)) -> g(proper(X))
proper(b) -> ok(b)
proper(c) -> ok(c)
f(ok(X1), ok(X2), ok(X3)) -> ok(f(X1, X2, X3))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))
ACTIVE(g(X)) -> ACTIVE(X)
active(f(X, g(X), Y)) -> mark(f(Y, Y, Y))
active(g(b)) -> mark(c)
active(b) -> mark(c)
active(g(X)) -> g(active(X))
g(mark(X)) -> mark(g(X))
g(ok(X)) -> ok(g(X))
proper(f(X1, X2, X3)) -> f(proper(X1), proper(X2), proper(X3))
proper(g(X)) -> g(proper(X))
proper(b) -> ok(b)
proper(c) -> ok(c)
f(ok(X1), ok(X2), ok(X3)) -> ok(f(X1, X2, X3))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))
POL(top(x1)) = 1 + x1 POL(ACTIVE(x1)) = x1 POL(active(x1)) = x1 POL(proper(x1)) = x1 POL(c) = 0 POL(g(x1)) = 1 + x1 POL(b) = 0 POL(mark(x1)) = x1 POL(ok(x1)) = x1
ACTIVE(x1) -> ACTIVE(x1)
g(x1) -> g(x1)
active(x1) -> active(x1)
mark(x1) -> mark(x1)
f(x1, x2, x3) -> x3
ok(x1) -> ok(x1)
proper(x1) -> proper(x1)
top(x1) -> top(x1)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 8
↳Dependency Graph
→DP Problem 4
↳AFS
→DP Problem 5
↳Remaining
active(f(X, g(X), Y)) -> mark(f(Y, Y, Y))
active(g(b)) -> mark(c)
active(b) -> mark(c)
active(g(X)) -> g(active(X))
g(mark(X)) -> mark(g(X))
g(ok(X)) -> ok(g(X))
proper(f(X1, X2, X3)) -> f(proper(X1), proper(X2), proper(X3))
proper(g(X)) -> g(proper(X))
proper(b) -> ok(b)
proper(c) -> ok(c)
f(ok(X1), ok(X2), ok(X3)) -> ok(f(X1, X2, X3))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳Argument Filtering and Ordering
→DP Problem 5
↳Remaining
PROPER(g(X)) -> PROPER(X)
PROPER(f(X1, X2, X3)) -> PROPER(X3)
PROPER(f(X1, X2, X3)) -> PROPER(X2)
PROPER(f(X1, X2, X3)) -> PROPER(X1)
active(f(X, g(X), Y)) -> mark(f(Y, Y, Y))
active(g(b)) -> mark(c)
active(b) -> mark(c)
active(g(X)) -> g(active(X))
g(mark(X)) -> mark(g(X))
g(ok(X)) -> ok(g(X))
proper(f(X1, X2, X3)) -> f(proper(X1), proper(X2), proper(X3))
proper(g(X)) -> g(proper(X))
proper(b) -> ok(b)
proper(c) -> ok(c)
f(ok(X1), ok(X2), ok(X3)) -> ok(f(X1, X2, X3))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))
PROPER(f(X1, X2, X3)) -> PROPER(X3)
PROPER(f(X1, X2, X3)) -> PROPER(X2)
PROPER(f(X1, X2, X3)) -> PROPER(X1)
active(f(X, g(X), Y)) -> mark(f(Y, Y, Y))
active(g(b)) -> mark(c)
active(b) -> mark(c)
active(g(X)) -> g(active(X))
g(mark(X)) -> mark(g(X))
g(ok(X)) -> ok(g(X))
proper(f(X1, X2, X3)) -> f(proper(X1), proper(X2), proper(X3))
proper(g(X)) -> g(proper(X))
proper(b) -> ok(b)
proper(c) -> ok(c)
f(ok(X1), ok(X2), ok(X3)) -> ok(f(X1, X2, X3))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))
POL(top) = 0 POL(active(x1)) = x1 POL(proper(x1)) = x1 POL(c) = 0 POL(g(x1)) = x1 POL(PROPER(x1)) = x1 POL(b) = 0 POL(mark) = 0 POL(ok(x1)) = x1 POL(f(x1, x2, x3)) = 1 + x1 + x2 + x3
PROPER(x1) -> PROPER(x1)
f(x1, x2, x3) -> f(x1, x2, x3)
g(x1) -> g(x1)
active(x1) -> active(x1)
mark(x1) -> mark
ok(x1) -> ok(x1)
proper(x1) -> proper(x1)
top(x1) -> top
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 9
↳Argument Filtering and Ordering
→DP Problem 5
↳Remaining
PROPER(g(X)) -> PROPER(X)
active(f(X, g(X), Y)) -> mark(f(Y, Y, Y))
active(g(b)) -> mark(c)
active(b) -> mark(c)
active(g(X)) -> g(active(X))
g(mark(X)) -> mark(g(X))
g(ok(X)) -> ok(g(X))
proper(f(X1, X2, X3)) -> f(proper(X1), proper(X2), proper(X3))
proper(g(X)) -> g(proper(X))
proper(b) -> ok(b)
proper(c) -> ok(c)
f(ok(X1), ok(X2), ok(X3)) -> ok(f(X1, X2, X3))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))
PROPER(g(X)) -> PROPER(X)
active(f(X, g(X), Y)) -> mark(f(Y, Y, Y))
active(g(b)) -> mark(c)
active(b) -> mark(c)
active(g(X)) -> g(active(X))
g(mark(X)) -> mark(g(X))
g(ok(X)) -> ok(g(X))
proper(f(X1, X2, X3)) -> f(proper(X1), proper(X2), proper(X3))
proper(g(X)) -> g(proper(X))
proper(b) -> ok(b)
proper(c) -> ok(c)
f(ok(X1), ok(X2), ok(X3)) -> ok(f(X1, X2, X3))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))
POL(top(x1)) = 1 + x1 POL(active(x1)) = x1 POL(proper(x1)) = x1 POL(c) = 0 POL(g(x1)) = 1 + x1 POL(PROPER(x1)) = x1 POL(b) = 0 POL(mark(x1)) = x1 POL(ok(x1)) = x1
PROPER(x1) -> PROPER(x1)
g(x1) -> g(x1)
active(x1) -> active(x1)
mark(x1) -> mark(x1)
f(x1, x2, x3) -> x3
ok(x1) -> ok(x1)
proper(x1) -> proper(x1)
top(x1) -> top(x1)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 9
↳AFS
...
→DP Problem 10
↳Dependency Graph
→DP Problem 5
↳Remaining
active(f(X, g(X), Y)) -> mark(f(Y, Y, Y))
active(g(b)) -> mark(c)
active(b) -> mark(c)
active(g(X)) -> g(active(X))
g(mark(X)) -> mark(g(X))
g(ok(X)) -> ok(g(X))
proper(f(X1, X2, X3)) -> f(proper(X1), proper(X2), proper(X3))
proper(g(X)) -> g(proper(X))
proper(b) -> ok(b)
proper(c) -> ok(c)
f(ok(X1), ok(X2), ok(X3)) -> ok(f(X1, X2, X3))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳Remaining Obligation(s)
TOP(ok(X)) -> TOP(active(X))
TOP(mark(X)) -> TOP(proper(X))
active(f(X, g(X), Y)) -> mark(f(Y, Y, Y))
active(g(b)) -> mark(c)
active(b) -> mark(c)
active(g(X)) -> g(active(X))
g(mark(X)) -> mark(g(X))
g(ok(X)) -> ok(g(X))
proper(f(X1, X2, X3)) -> f(proper(X1), proper(X2), proper(X3))
proper(g(X)) -> g(proper(X))
proper(b) -> ok(b)
proper(c) -> ok(c)
f(ok(X1), ok(X2), ok(X3)) -> ok(f(X1, X2, X3))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))