R
↳Dependency Pair Analysis
ACTIVE(f(x)) -> F(active(x))
ACTIVE(f(x)) -> ACTIVE(x)
TOP(active(c)) -> TOP(mark(c))
TOP(mark(x)) -> TOP(check(x))
TOP(mark(x)) -> CHECK(x)
TOP(found(x)) -> TOP(active(x))
TOP(found(x)) -> ACTIVE(x)
CHECK(f(x)) -> F(check(x))
CHECK(f(x)) -> CHECK(x)
CHECK(x) -> START(match(f(X), x))
CHECK(x) -> MATCH(f(X), x)
CHECK(x) -> F(X)
MATCH(f(x), f(y)) -> F(match(x, y))
MATCH(f(x), f(y)) -> MATCH(x, y)
MATCH(X, x) -> PROPER(x)
PROPER(f(x)) -> F(proper(x))
PROPER(f(x)) -> PROPER(x)
F(ok(x)) -> F(x)
F(found(x)) -> F(x)
F(mark(x)) -> F(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
↳AFS
→DP Problem 6
↳Nar
F(mark(x)) -> F(x)
F(found(x)) -> F(x)
F(ok(x)) -> F(x)
active(f(x)) -> mark(x)
active(f(x)) -> f(active(x))
top(active(c)) -> top(mark(c))
top(mark(x)) -> top(check(x))
top(found(x)) -> top(active(x))
check(f(x)) -> f(check(x))
check(x) -> start(match(f(X), x))
match(f(x), f(y)) -> f(match(x, y))
match(X, x) -> proper(x)
proper(c) -> ok(c)
proper(f(x)) -> f(proper(x))
f(ok(x)) -> ok(f(x))
f(found(x)) -> found(f(x))
f(mark(x)) -> mark(f(x))
start(ok(x)) -> found(x)
F(mark(x)) -> F(x)
F(found(x)) -> F(x)
F(ok(x)) -> F(x)
F(x1) -> F(x1)
ok(x1) -> ok(x1)
mark(x1) -> mark(x1)
found(x1) -> found(x1)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 7
↳Dependency Graph
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 6
↳Nar
active(f(x)) -> mark(x)
active(f(x)) -> f(active(x))
top(active(c)) -> top(mark(c))
top(mark(x)) -> top(check(x))
top(found(x)) -> top(active(x))
check(f(x)) -> f(check(x))
check(x) -> start(match(f(X), x))
match(f(x), f(y)) -> f(match(x, y))
match(X, x) -> proper(x)
proper(c) -> ok(c)
proper(f(x)) -> f(proper(x))
f(ok(x)) -> ok(f(x))
f(found(x)) -> found(f(x))
f(mark(x)) -> mark(f(x))
start(ok(x)) -> found(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
↳AFS
→DP Problem 6
↳Nar
ACTIVE(f(x)) -> ACTIVE(x)
active(f(x)) -> mark(x)
active(f(x)) -> f(active(x))
top(active(c)) -> top(mark(c))
top(mark(x)) -> top(check(x))
top(found(x)) -> top(active(x))
check(f(x)) -> f(check(x))
check(x) -> start(match(f(X), x))
match(f(x), f(y)) -> f(match(x, y))
match(X, x) -> proper(x)
proper(c) -> ok(c)
proper(f(x)) -> f(proper(x))
f(ok(x)) -> ok(f(x))
f(found(x)) -> found(f(x))
f(mark(x)) -> mark(f(x))
start(ok(x)) -> found(x)
ACTIVE(f(x)) -> ACTIVE(x)
ACTIVE(x1) -> ACTIVE(x1)
f(x1) -> f(x1)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 8
↳Dependency Graph
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 6
↳Nar
active(f(x)) -> mark(x)
active(f(x)) -> f(active(x))
top(active(c)) -> top(mark(c))
top(mark(x)) -> top(check(x))
top(found(x)) -> top(active(x))
check(f(x)) -> f(check(x))
check(x) -> start(match(f(X), x))
match(f(x), f(y)) -> f(match(x, y))
match(X, x) -> proper(x)
proper(c) -> ok(c)
proper(f(x)) -> f(proper(x))
f(ok(x)) -> ok(f(x))
f(found(x)) -> found(f(x))
f(mark(x)) -> mark(f(x))
start(ok(x)) -> found(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
↳AFS
→DP Problem 6
↳Nar
PROPER(f(x)) -> PROPER(x)
active(f(x)) -> mark(x)
active(f(x)) -> f(active(x))
top(active(c)) -> top(mark(c))
top(mark(x)) -> top(check(x))
top(found(x)) -> top(active(x))
check(f(x)) -> f(check(x))
check(x) -> start(match(f(X), x))
match(f(x), f(y)) -> f(match(x, y))
match(X, x) -> proper(x)
proper(c) -> ok(c)
proper(f(x)) -> f(proper(x))
f(ok(x)) -> ok(f(x))
f(found(x)) -> found(f(x))
f(mark(x)) -> mark(f(x))
start(ok(x)) -> found(x)
PROPER(f(x)) -> PROPER(x)
PROPER(x1) -> PROPER(x1)
f(x1) -> f(x1)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 9
↳Dependency Graph
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 6
↳Nar
active(f(x)) -> mark(x)
active(f(x)) -> f(active(x))
top(active(c)) -> top(mark(c))
top(mark(x)) -> top(check(x))
top(found(x)) -> top(active(x))
check(f(x)) -> f(check(x))
check(x) -> start(match(f(X), x))
match(f(x), f(y)) -> f(match(x, y))
match(X, x) -> proper(x)
proper(c) -> ok(c)
proper(f(x)) -> f(proper(x))
f(ok(x)) -> ok(f(x))
f(found(x)) -> found(f(x))
f(mark(x)) -> mark(f(x))
start(ok(x)) -> found(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
↳AFS
→DP Problem 6
↳Nar
MATCH(f(x), f(y)) -> MATCH(x, y)
active(f(x)) -> mark(x)
active(f(x)) -> f(active(x))
top(active(c)) -> top(mark(c))
top(mark(x)) -> top(check(x))
top(found(x)) -> top(active(x))
check(f(x)) -> f(check(x))
check(x) -> start(match(f(X), x))
match(f(x), f(y)) -> f(match(x, y))
match(X, x) -> proper(x)
proper(c) -> ok(c)
proper(f(x)) -> f(proper(x))
f(ok(x)) -> ok(f(x))
f(found(x)) -> found(f(x))
f(mark(x)) -> mark(f(x))
start(ok(x)) -> found(x)
MATCH(f(x), f(y)) -> MATCH(x, y)
MATCH(x1, x2) -> MATCH(x1, x2)
f(x1) -> f(x1)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 10
↳Dependency Graph
→DP Problem 5
↳AFS
→DP Problem 6
↳Nar
active(f(x)) -> mark(x)
active(f(x)) -> f(active(x))
top(active(c)) -> top(mark(c))
top(mark(x)) -> top(check(x))
top(found(x)) -> top(active(x))
check(f(x)) -> f(check(x))
check(x) -> start(match(f(X), x))
match(f(x), f(y)) -> f(match(x, y))
match(X, x) -> proper(x)
proper(c) -> ok(c)
proper(f(x)) -> f(proper(x))
f(ok(x)) -> ok(f(x))
f(found(x)) -> found(f(x))
f(mark(x)) -> mark(f(x))
start(ok(x)) -> found(x)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳Argument Filtering and Ordering
→DP Problem 6
↳Nar
CHECK(f(x)) -> CHECK(x)
active(f(x)) -> mark(x)
active(f(x)) -> f(active(x))
top(active(c)) -> top(mark(c))
top(mark(x)) -> top(check(x))
top(found(x)) -> top(active(x))
check(f(x)) -> f(check(x))
check(x) -> start(match(f(X), x))
match(f(x), f(y)) -> f(match(x, y))
match(X, x) -> proper(x)
proper(c) -> ok(c)
proper(f(x)) -> f(proper(x))
f(ok(x)) -> ok(f(x))
f(found(x)) -> found(f(x))
f(mark(x)) -> mark(f(x))
start(ok(x)) -> found(x)
CHECK(f(x)) -> CHECK(x)
CHECK(x1) -> CHECK(x1)
f(x1) -> f(x1)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 11
↳Dependency Graph
→DP Problem 6
↳Nar
active(f(x)) -> mark(x)
active(f(x)) -> f(active(x))
top(active(c)) -> top(mark(c))
top(mark(x)) -> top(check(x))
top(found(x)) -> top(active(x))
check(f(x)) -> f(check(x))
check(x) -> start(match(f(X), x))
match(f(x), f(y)) -> f(match(x, y))
match(X, x) -> proper(x)
proper(c) -> ok(c)
proper(f(x)) -> f(proper(x))
f(ok(x)) -> ok(f(x))
f(found(x)) -> found(f(x))
f(mark(x)) -> mark(f(x))
start(ok(x)) -> found(x)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 6
↳Narrowing Transformation
TOP(found(x)) -> TOP(active(x))
TOP(mark(x)) -> TOP(check(x))
TOP(active(c)) -> TOP(mark(c))
active(f(x)) -> mark(x)
active(f(x)) -> f(active(x))
top(active(c)) -> top(mark(c))
top(mark(x)) -> top(check(x))
top(found(x)) -> top(active(x))
check(f(x)) -> f(check(x))
check(x) -> start(match(f(X), x))
match(f(x), f(y)) -> f(match(x, y))
match(X, x) -> proper(x)
proper(c) -> ok(c)
proper(f(x)) -> f(proper(x))
f(ok(x)) -> ok(f(x))
f(found(x)) -> found(f(x))
f(mark(x)) -> mark(f(x))
start(ok(x)) -> found(x)
two new Dependency Pairs are created:
TOP(mark(x)) -> TOP(check(x))
TOP(mark(f(x''))) -> TOP(f(check(x'')))
TOP(mark(x'')) -> TOP(start(match(f(X), x'')))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 6
↳Nar
→DP Problem 12
↳Narrowing Transformation
TOP(mark(f(x''))) -> TOP(f(check(x'')))
TOP(mark(x'')) -> TOP(start(match(f(X), x'')))
TOP(active(c)) -> TOP(mark(c))
TOP(found(x)) -> TOP(active(x))
active(f(x)) -> mark(x)
active(f(x)) -> f(active(x))
top(active(c)) -> top(mark(c))
top(mark(x)) -> top(check(x))
top(found(x)) -> top(active(x))
check(f(x)) -> f(check(x))
check(x) -> start(match(f(X), x))
match(f(x), f(y)) -> f(match(x, y))
match(X, x) -> proper(x)
proper(c) -> ok(c)
proper(f(x)) -> f(proper(x))
f(ok(x)) -> ok(f(x))
f(found(x)) -> found(f(x))
f(mark(x)) -> mark(f(x))
start(ok(x)) -> found(x)
two new Dependency Pairs are created:
TOP(mark(f(x''))) -> TOP(f(check(x'')))
TOP(mark(f(f(x')))) -> TOP(f(f(check(x'))))
TOP(mark(f(x'''))) -> TOP(f(start(match(f(X), x'''))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 6
↳Nar
→DP Problem 12
↳Nar
...
→DP Problem 13
↳Narrowing Transformation
TOP(mark(f(x'''))) -> TOP(f(start(match(f(X), x'''))))
TOP(mark(f(f(x')))) -> TOP(f(f(check(x'))))
TOP(found(x)) -> TOP(active(x))
TOP(active(c)) -> TOP(mark(c))
TOP(mark(x'')) -> TOP(start(match(f(X), x'')))
active(f(x)) -> mark(x)
active(f(x)) -> f(active(x))
top(active(c)) -> top(mark(c))
top(mark(x)) -> top(check(x))
top(found(x)) -> top(active(x))
check(f(x)) -> f(check(x))
check(x) -> start(match(f(X), x))
match(f(x), f(y)) -> f(match(x, y))
match(X, x) -> proper(x)
proper(c) -> ok(c)
proper(f(x)) -> f(proper(x))
f(ok(x)) -> ok(f(x))
f(found(x)) -> found(f(x))
f(mark(x)) -> mark(f(x))
start(ok(x)) -> found(x)
one new Dependency Pair is created:
TOP(mark(x'')) -> TOP(start(match(f(X), x'')))
TOP(mark(f(y'))) -> TOP(start(f(match(X, y'))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 6
↳Nar
→DP Problem 12
↳Nar
...
→DP Problem 14
↳Narrowing Transformation
TOP(mark(f(y'))) -> TOP(start(f(match(X, y'))))
TOP(mark(f(f(x')))) -> TOP(f(f(check(x'))))
TOP(found(x)) -> TOP(active(x))
TOP(mark(f(x'''))) -> TOP(f(start(match(f(X), x'''))))
active(f(x)) -> mark(x)
active(f(x)) -> f(active(x))
top(active(c)) -> top(mark(c))
top(mark(x)) -> top(check(x))
top(found(x)) -> top(active(x))
check(f(x)) -> f(check(x))
check(x) -> start(match(f(X), x))
match(f(x), f(y)) -> f(match(x, y))
match(X, x) -> proper(x)
proper(c) -> ok(c)
proper(f(x)) -> f(proper(x))
f(ok(x)) -> ok(f(x))
f(found(x)) -> found(f(x))
f(mark(x)) -> mark(f(x))
start(ok(x)) -> found(x)
two new Dependency Pairs are created:
TOP(found(x)) -> TOP(active(x))
TOP(found(f(x''))) -> TOP(mark(x''))
TOP(found(f(x''))) -> TOP(f(active(x'')))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 6
↳Nar
→DP Problem 12
↳Nar
...
→DP Problem 15
↳Narrowing Transformation
TOP(found(f(x''))) -> TOP(f(active(x'')))
TOP(found(f(x''))) -> TOP(mark(x''))
TOP(mark(f(x'''))) -> TOP(f(start(match(f(X), x'''))))
TOP(mark(f(f(x')))) -> TOP(f(f(check(x'))))
TOP(mark(f(y'))) -> TOP(start(f(match(X, y'))))
active(f(x)) -> mark(x)
active(f(x)) -> f(active(x))
top(active(c)) -> top(mark(c))
top(mark(x)) -> top(check(x))
top(found(x)) -> top(active(x))
check(f(x)) -> f(check(x))
check(x) -> start(match(f(X), x))
match(f(x), f(y)) -> f(match(x, y))
match(X, x) -> proper(x)
proper(c) -> ok(c)
proper(f(x)) -> f(proper(x))
f(ok(x)) -> ok(f(x))
f(found(x)) -> found(f(x))
f(mark(x)) -> mark(f(x))
start(ok(x)) -> found(x)
two new Dependency Pairs are created:
TOP(found(f(x''))) -> TOP(f(active(x'')))
TOP(found(f(f(x')))) -> TOP(f(mark(x')))
TOP(found(f(f(x')))) -> TOP(f(f(active(x'))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 6
↳Nar
→DP Problem 12
↳Nar
...
→DP Problem 16
↳Argument Filtering and Ordering
TOP(found(f(f(x')))) -> TOP(f(f(active(x'))))
TOP(found(f(f(x')))) -> TOP(f(mark(x')))
TOP(mark(f(y'))) -> TOP(start(f(match(X, y'))))
TOP(mark(f(x'''))) -> TOP(f(start(match(f(X), x'''))))
TOP(mark(f(f(x')))) -> TOP(f(f(check(x'))))
TOP(found(f(x''))) -> TOP(mark(x''))
active(f(x)) -> mark(x)
active(f(x)) -> f(active(x))
top(active(c)) -> top(mark(c))
top(mark(x)) -> top(check(x))
top(found(x)) -> top(active(x))
check(f(x)) -> f(check(x))
check(x) -> start(match(f(X), x))
match(f(x), f(y)) -> f(match(x, y))
match(X, x) -> proper(x)
proper(c) -> ok(c)
proper(f(x)) -> f(proper(x))
f(ok(x)) -> ok(f(x))
f(found(x)) -> found(f(x))
f(mark(x)) -> mark(f(x))
start(ok(x)) -> found(x)
TOP(found(f(f(x')))) -> TOP(f(mark(x')))
TOP(found(f(x''))) -> TOP(mark(x''))
match(f(x), f(y)) -> f(match(x, y))
match(X, x) -> proper(x)
f(ok(x)) -> ok(f(x))
f(found(x)) -> found(f(x))
f(mark(x)) -> mark(f(x))
start(ok(x)) -> found(x)
check(f(x)) -> f(check(x))
check(x) -> start(match(f(X), x))
active(f(x)) -> mark(x)
active(f(x)) -> f(active(x))
proper(c) -> ok(c)
proper(f(x)) -> f(proper(x))
TOP(x1) -> TOP(x1)
mark(x1) -> x1
f(x1) -> f(x1)
start(x1) -> x1
match(x1, x2) -> x2
found(x1) -> x1
check(x1) -> x1
active(x1) -> x1
proper(x1) -> x1
ok(x1) -> x1
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 6
↳Nar
→DP Problem 12
↳Nar
...
→DP Problem 17
↳Narrowing Transformation
TOP(found(f(f(x')))) -> TOP(f(f(active(x'))))
TOP(mark(f(y'))) -> TOP(start(f(match(X, y'))))
TOP(mark(f(x'''))) -> TOP(f(start(match(f(X), x'''))))
TOP(mark(f(f(x')))) -> TOP(f(f(check(x'))))
active(f(x)) -> mark(x)
active(f(x)) -> f(active(x))
top(active(c)) -> top(mark(c))
top(mark(x)) -> top(check(x))
top(found(x)) -> top(active(x))
check(f(x)) -> f(check(x))
check(x) -> start(match(f(X), x))
match(f(x), f(y)) -> f(match(x, y))
match(X, x) -> proper(x)
proper(c) -> ok(c)
proper(f(x)) -> f(proper(x))
f(ok(x)) -> ok(f(x))
f(found(x)) -> found(f(x))
f(mark(x)) -> mark(f(x))
start(ok(x)) -> found(x)
two new Dependency Pairs are created:
TOP(mark(f(f(x')))) -> TOP(f(f(check(x'))))
TOP(mark(f(f(f(x''))))) -> TOP(f(f(f(check(x'')))))
TOP(mark(f(f(x'')))) -> TOP(f(f(start(match(f(X), x'')))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 6
↳Nar
→DP Problem 12
↳Nar
...
→DP Problem 18
↳Narrowing Transformation
TOP(mark(f(f(x'')))) -> TOP(f(f(start(match(f(X), x'')))))
TOP(mark(f(f(f(x''))))) -> TOP(f(f(f(check(x'')))))
TOP(mark(f(y'))) -> TOP(start(f(match(X, y'))))
TOP(mark(f(x'''))) -> TOP(f(start(match(f(X), x'''))))
TOP(found(f(f(x')))) -> TOP(f(f(active(x'))))
active(f(x)) -> mark(x)
active(f(x)) -> f(active(x))
top(active(c)) -> top(mark(c))
top(mark(x)) -> top(check(x))
top(found(x)) -> top(active(x))
check(f(x)) -> f(check(x))
check(x) -> start(match(f(X), x))
match(f(x), f(y)) -> f(match(x, y))
match(X, x) -> proper(x)
proper(c) -> ok(c)
proper(f(x)) -> f(proper(x))
f(ok(x)) -> ok(f(x))
f(found(x)) -> found(f(x))
f(mark(x)) -> mark(f(x))
start(ok(x)) -> found(x)
one new Dependency Pair is created:
TOP(mark(f(x'''))) -> TOP(f(start(match(f(X), x'''))))
TOP(mark(f(f(y')))) -> TOP(f(start(f(match(X, y')))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 6
↳Nar
→DP Problem 12
↳Nar
...
→DP Problem 19
↳Narrowing Transformation
TOP(mark(f(f(y')))) -> TOP(f(start(f(match(X, y')))))
TOP(mark(f(f(f(x''))))) -> TOP(f(f(f(check(x'')))))
TOP(found(f(f(x')))) -> TOP(f(f(active(x'))))
TOP(mark(f(y'))) -> TOP(start(f(match(X, y'))))
TOP(mark(f(f(x'')))) -> TOP(f(f(start(match(f(X), x'')))))
active(f(x)) -> mark(x)
active(f(x)) -> f(active(x))
top(active(c)) -> top(mark(c))
top(mark(x)) -> top(check(x))
top(found(x)) -> top(active(x))
check(f(x)) -> f(check(x))
check(x) -> start(match(f(X), x))
match(f(x), f(y)) -> f(match(x, y))
match(X, x) -> proper(x)
proper(c) -> ok(c)
proper(f(x)) -> f(proper(x))
f(ok(x)) -> ok(f(x))
f(found(x)) -> found(f(x))
f(mark(x)) -> mark(f(x))
start(ok(x)) -> found(x)
one new Dependency Pair is created:
TOP(mark(f(y'))) -> TOP(start(f(match(X, y'))))
TOP(mark(f(y''))) -> TOP(start(f(proper(y''))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 6
↳Nar
→DP Problem 12
↳Nar
...
→DP Problem 20
↳Narrowing Transformation
TOP(mark(f(y''))) -> TOP(start(f(proper(y''))))
TOP(mark(f(f(x'')))) -> TOP(f(f(start(match(f(X), x'')))))
TOP(mark(f(f(f(x''))))) -> TOP(f(f(f(check(x'')))))
TOP(found(f(f(x')))) -> TOP(f(f(active(x'))))
TOP(mark(f(f(y')))) -> TOP(f(start(f(match(X, y')))))
active(f(x)) -> mark(x)
active(f(x)) -> f(active(x))
top(active(c)) -> top(mark(c))
top(mark(x)) -> top(check(x))
top(found(x)) -> top(active(x))
check(f(x)) -> f(check(x))
check(x) -> start(match(f(X), x))
match(f(x), f(y)) -> f(match(x, y))
match(X, x) -> proper(x)
proper(c) -> ok(c)
proper(f(x)) -> f(proper(x))
f(ok(x)) -> ok(f(x))
f(found(x)) -> found(f(x))
f(mark(x)) -> mark(f(x))
start(ok(x)) -> found(x)
two new Dependency Pairs are created:
TOP(found(f(f(x')))) -> TOP(f(f(active(x'))))
TOP(found(f(f(f(x''))))) -> TOP(f(f(mark(x''))))
TOP(found(f(f(f(x''))))) -> TOP(f(f(f(active(x'')))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 6
↳Nar
→DP Problem 12
↳Nar
...
→DP Problem 21
↳Narrowing Transformation
TOP(found(f(f(f(x''))))) -> TOP(f(f(f(active(x'')))))
TOP(found(f(f(f(x''))))) -> TOP(f(f(mark(x''))))
TOP(mark(f(f(y')))) -> TOP(f(start(f(match(X, y')))))
TOP(mark(f(f(x'')))) -> TOP(f(f(start(match(f(X), x'')))))
TOP(mark(f(f(f(x''))))) -> TOP(f(f(f(check(x'')))))
TOP(mark(f(y''))) -> TOP(start(f(proper(y''))))
active(f(x)) -> mark(x)
active(f(x)) -> f(active(x))
top(active(c)) -> top(mark(c))
top(mark(x)) -> top(check(x))
top(found(x)) -> top(active(x))
check(f(x)) -> f(check(x))
check(x) -> start(match(f(X), x))
match(f(x), f(y)) -> f(match(x, y))
match(X, x) -> proper(x)
proper(c) -> ok(c)
proper(f(x)) -> f(proper(x))
f(ok(x)) -> ok(f(x))
f(found(x)) -> found(f(x))
f(mark(x)) -> mark(f(x))
start(ok(x)) -> found(x)
two new Dependency Pairs are created:
TOP(mark(f(f(f(x''))))) -> TOP(f(f(f(check(x'')))))
TOP(mark(f(f(f(f(x')))))) -> TOP(f(f(f(f(check(x'))))))
TOP(mark(f(f(f(x'''))))) -> TOP(f(f(f(start(match(f(X), x'''))))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 6
↳Nar
→DP Problem 12
↳Nar
...
→DP Problem 22
↳Narrowing Transformation
TOP(mark(f(f(f(x'''))))) -> TOP(f(f(f(start(match(f(X), x'''))))))
TOP(mark(f(f(f(f(x')))))) -> TOP(f(f(f(f(check(x'))))))
TOP(found(f(f(f(x''))))) -> TOP(f(f(mark(x''))))
TOP(mark(f(y''))) -> TOP(start(f(proper(y''))))
TOP(mark(f(f(y')))) -> TOP(f(start(f(match(X, y')))))
TOP(mark(f(f(x'')))) -> TOP(f(f(start(match(f(X), x'')))))
TOP(found(f(f(f(x''))))) -> TOP(f(f(f(active(x'')))))
active(f(x)) -> mark(x)
active(f(x)) -> f(active(x))
top(active(c)) -> top(mark(c))
top(mark(x)) -> top(check(x))
top(found(x)) -> top(active(x))
check(f(x)) -> f(check(x))
check(x) -> start(match(f(X), x))
match(f(x), f(y)) -> f(match(x, y))
match(X, x) -> proper(x)
proper(c) -> ok(c)
proper(f(x)) -> f(proper(x))
f(ok(x)) -> ok(f(x))
f(found(x)) -> found(f(x))
f(mark(x)) -> mark(f(x))
start(ok(x)) -> found(x)
one new Dependency Pair is created:
TOP(mark(f(f(x'')))) -> TOP(f(f(start(match(f(X), x'')))))
TOP(mark(f(f(f(y'))))) -> TOP(f(f(start(f(match(X, y'))))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 6
↳Nar
→DP Problem 12
↳Nar
...
→DP Problem 23
↳Narrowing Transformation
TOP(mark(f(f(f(y'))))) -> TOP(f(f(start(f(match(X, y'))))))
TOP(mark(f(f(f(f(x')))))) -> TOP(f(f(f(f(check(x'))))))
TOP(found(f(f(f(x''))))) -> TOP(f(f(f(active(x'')))))
TOP(found(f(f(f(x''))))) -> TOP(f(f(mark(x''))))
TOP(mark(f(y''))) -> TOP(start(f(proper(y''))))
TOP(mark(f(f(y')))) -> TOP(f(start(f(match(X, y')))))
TOP(mark(f(f(f(x'''))))) -> TOP(f(f(f(start(match(f(X), x'''))))))
active(f(x)) -> mark(x)
active(f(x)) -> f(active(x))
top(active(c)) -> top(mark(c))
top(mark(x)) -> top(check(x))
top(found(x)) -> top(active(x))
check(f(x)) -> f(check(x))
check(x) -> start(match(f(X), x))
match(f(x), f(y)) -> f(match(x, y))
match(X, x) -> proper(x)
proper(c) -> ok(c)
proper(f(x)) -> f(proper(x))
f(ok(x)) -> ok(f(x))
f(found(x)) -> found(f(x))
f(mark(x)) -> mark(f(x))
start(ok(x)) -> found(x)
one new Dependency Pair is created:
TOP(mark(f(f(y')))) -> TOP(f(start(f(match(X, y')))))
TOP(mark(f(f(y'')))) -> TOP(f(start(f(proper(y'')))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 6
↳Nar
→DP Problem 12
↳Nar
...
→DP Problem 24
↳Narrowing Transformation
TOP(mark(f(f(y'')))) -> TOP(f(start(f(proper(y'')))))
TOP(mark(f(f(f(x'''))))) -> TOP(f(f(f(start(match(f(X), x'''))))))
TOP(mark(f(f(f(f(x')))))) -> TOP(f(f(f(f(check(x'))))))
TOP(found(f(f(f(x''))))) -> TOP(f(f(f(active(x'')))))
TOP(found(f(f(f(x''))))) -> TOP(f(f(mark(x''))))
TOP(mark(f(y''))) -> TOP(start(f(proper(y''))))
TOP(mark(f(f(f(y'))))) -> TOP(f(f(start(f(match(X, y'))))))
active(f(x)) -> mark(x)
active(f(x)) -> f(active(x))
top(active(c)) -> top(mark(c))
top(mark(x)) -> top(check(x))
top(found(x)) -> top(active(x))
check(f(x)) -> f(check(x))
check(x) -> start(match(f(X), x))
match(f(x), f(y)) -> f(match(x, y))
match(X, x) -> proper(x)
proper(c) -> ok(c)
proper(f(x)) -> f(proper(x))
f(ok(x)) -> ok(f(x))
f(found(x)) -> found(f(x))
f(mark(x)) -> mark(f(x))
start(ok(x)) -> found(x)
two new Dependency Pairs are created:
TOP(mark(f(y''))) -> TOP(start(f(proper(y''))))
TOP(mark(f(c))) -> TOP(start(f(ok(c))))
TOP(mark(f(f(x')))) -> TOP(start(f(f(proper(x')))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 6
↳Nar
→DP Problem 12
↳Nar
...
→DP Problem 25
↳Narrowing Transformation
TOP(mark(f(f(x')))) -> TOP(start(f(f(proper(x')))))
TOP(mark(f(c))) -> TOP(start(f(ok(c))))
TOP(mark(f(f(f(y'))))) -> TOP(f(f(start(f(match(X, y'))))))
TOP(mark(f(f(f(x'''))))) -> TOP(f(f(f(start(match(f(X), x'''))))))
TOP(mark(f(f(f(f(x')))))) -> TOP(f(f(f(f(check(x'))))))
TOP(found(f(f(f(x''))))) -> TOP(f(f(f(active(x'')))))
TOP(found(f(f(f(x''))))) -> TOP(f(f(mark(x''))))
TOP(mark(f(f(y'')))) -> TOP(f(start(f(proper(y'')))))
active(f(x)) -> mark(x)
active(f(x)) -> f(active(x))
top(active(c)) -> top(mark(c))
top(mark(x)) -> top(check(x))
top(found(x)) -> top(active(x))
check(f(x)) -> f(check(x))
check(x) -> start(match(f(X), x))
match(f(x), f(y)) -> f(match(x, y))
match(X, x) -> proper(x)
proper(c) -> ok(c)
proper(f(x)) -> f(proper(x))
f(ok(x)) -> ok(f(x))
f(found(x)) -> found(f(x))
f(mark(x)) -> mark(f(x))
start(ok(x)) -> found(x)
one new Dependency Pair is created:
TOP(found(f(f(f(x''))))) -> TOP(f(f(mark(x''))))
TOP(found(f(f(f(x'''))))) -> TOP(f(mark(f(x'''))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 6
↳Nar
→DP Problem 12
↳Nar
...
→DP Problem 26
↳Narrowing Transformation
TOP(found(f(f(f(x'''))))) -> TOP(f(mark(f(x'''))))
TOP(mark(f(c))) -> TOP(start(f(ok(c))))
TOP(mark(f(f(y'')))) -> TOP(f(start(f(proper(y'')))))
TOP(mark(f(f(f(y'))))) -> TOP(f(f(start(f(match(X, y'))))))
TOP(mark(f(f(f(x'''))))) -> TOP(f(f(f(start(match(f(X), x'''))))))
TOP(mark(f(f(f(f(x')))))) -> TOP(f(f(f(f(check(x'))))))
TOP(found(f(f(f(x''))))) -> TOP(f(f(f(active(x'')))))
TOP(mark(f(f(x')))) -> TOP(start(f(f(proper(x')))))
active(f(x)) -> mark(x)
active(f(x)) -> f(active(x))
top(active(c)) -> top(mark(c))
top(mark(x)) -> top(check(x))
top(found(x)) -> top(active(x))
check(f(x)) -> f(check(x))
check(x) -> start(match(f(X), x))
match(f(x), f(y)) -> f(match(x, y))
match(X, x) -> proper(x)
proper(c) -> ok(c)
proper(f(x)) -> f(proper(x))
f(ok(x)) -> ok(f(x))
f(found(x)) -> found(f(x))
f(mark(x)) -> mark(f(x))
start(ok(x)) -> found(x)
two new Dependency Pairs are created:
TOP(found(f(f(f(x''))))) -> TOP(f(f(f(active(x'')))))
TOP(found(f(f(f(f(x')))))) -> TOP(f(f(f(mark(x')))))
TOP(found(f(f(f(f(x')))))) -> TOP(f(f(f(f(active(x'))))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 6
↳Nar
→DP Problem 12
↳Nar
...
→DP Problem 27
↳Narrowing Transformation
TOP(found(f(f(f(f(x')))))) -> TOP(f(f(f(f(active(x'))))))
TOP(found(f(f(f(f(x')))))) -> TOP(f(f(f(mark(x')))))
TOP(mark(f(f(x')))) -> TOP(start(f(f(proper(x')))))
TOP(mark(f(c))) -> TOP(start(f(ok(c))))
TOP(mark(f(f(y'')))) -> TOP(f(start(f(proper(y'')))))
TOP(mark(f(f(f(y'))))) -> TOP(f(f(start(f(match(X, y'))))))
TOP(mark(f(f(f(x'''))))) -> TOP(f(f(f(start(match(f(X), x'''))))))
TOP(mark(f(f(f(f(x')))))) -> TOP(f(f(f(f(check(x'))))))
TOP(found(f(f(f(x'''))))) -> TOP(f(mark(f(x'''))))
active(f(x)) -> mark(x)
active(f(x)) -> f(active(x))
top(active(c)) -> top(mark(c))
top(mark(x)) -> top(check(x))
top(found(x)) -> top(active(x))
check(f(x)) -> f(check(x))
check(x) -> start(match(f(X), x))
match(f(x), f(y)) -> f(match(x, y))
match(X, x) -> proper(x)
proper(c) -> ok(c)
proper(f(x)) -> f(proper(x))
f(ok(x)) -> ok(f(x))
f(found(x)) -> found(f(x))
f(mark(x)) -> mark(f(x))
start(ok(x)) -> found(x)
two new Dependency Pairs are created:
TOP(mark(f(f(f(f(x')))))) -> TOP(f(f(f(f(check(x'))))))
TOP(mark(f(f(f(f(f(x''))))))) -> TOP(f(f(f(f(f(check(x'')))))))
TOP(mark(f(f(f(f(x'')))))) -> TOP(f(f(f(f(start(match(f(X), x'')))))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 6
↳Nar
→DP Problem 12
↳Nar
...
→DP Problem 28
↳Narrowing Transformation
TOP(mark(f(f(f(f(x'')))))) -> TOP(f(f(f(f(start(match(f(X), x'')))))))
TOP(mark(f(f(f(f(f(x''))))))) -> TOP(f(f(f(f(f(check(x'')))))))
TOP(found(f(f(f(f(x')))))) -> TOP(f(f(f(mark(x')))))
TOP(found(f(f(f(x'''))))) -> TOP(f(mark(f(x'''))))
TOP(mark(f(f(x')))) -> TOP(start(f(f(proper(x')))))
TOP(mark(f(c))) -> TOP(start(f(ok(c))))
TOP(mark(f(f(y'')))) -> TOP(f(start(f(proper(y'')))))
TOP(mark(f(f(f(y'))))) -> TOP(f(f(start(f(match(X, y'))))))
TOP(mark(f(f(f(x'''))))) -> TOP(f(f(f(start(match(f(X), x'''))))))
TOP(found(f(f(f(f(x')))))) -> TOP(f(f(f(f(active(x'))))))
active(f(x)) -> mark(x)
active(f(x)) -> f(active(x))
top(active(c)) -> top(mark(c))
top(mark(x)) -> top(check(x))
top(found(x)) -> top(active(x))
check(f(x)) -> f(check(x))
check(x) -> start(match(f(X), x))
match(f(x), f(y)) -> f(match(x, y))
match(X, x) -> proper(x)
proper(c) -> ok(c)
proper(f(x)) -> f(proper(x))
f(ok(x)) -> ok(f(x))
f(found(x)) -> found(f(x))
f(mark(x)) -> mark(f(x))
start(ok(x)) -> found(x)
one new Dependency Pair is created:
TOP(mark(f(f(f(x'''))))) -> TOP(f(f(f(start(match(f(X), x'''))))))
TOP(mark(f(f(f(f(y')))))) -> TOP(f(f(f(start(f(match(X, y')))))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 6
↳Nar
→DP Problem 12
↳Nar
...
→DP Problem 29
↳Narrowing Transformation
TOP(mark(f(f(f(f(y')))))) -> TOP(f(f(f(start(f(match(X, y')))))))
TOP(mark(f(f(f(f(f(x''))))))) -> TOP(f(f(f(f(f(check(x'')))))))
TOP(found(f(f(f(f(x')))))) -> TOP(f(f(f(f(active(x'))))))
TOP(found(f(f(f(f(x')))))) -> TOP(f(f(f(mark(x')))))
TOP(found(f(f(f(x'''))))) -> TOP(f(mark(f(x'''))))
TOP(mark(f(f(x')))) -> TOP(start(f(f(proper(x')))))
TOP(mark(f(c))) -> TOP(start(f(ok(c))))
TOP(mark(f(f(y'')))) -> TOP(f(start(f(proper(y'')))))
TOP(mark(f(f(f(y'))))) -> TOP(f(f(start(f(match(X, y'))))))
TOP(mark(f(f(f(f(x'')))))) -> TOP(f(f(f(f(start(match(f(X), x'')))))))
active(f(x)) -> mark(x)
active(f(x)) -> f(active(x))
top(active(c)) -> top(mark(c))
top(mark(x)) -> top(check(x))
top(found(x)) -> top(active(x))
check(f(x)) -> f(check(x))
check(x) -> start(match(f(X), x))
match(f(x), f(y)) -> f(match(x, y))
match(X, x) -> proper(x)
proper(c) -> ok(c)
proper(f(x)) -> f(proper(x))
f(ok(x)) -> ok(f(x))
f(found(x)) -> found(f(x))
f(mark(x)) -> mark(f(x))
start(ok(x)) -> found(x)
one new Dependency Pair is created:
TOP(mark(f(f(f(y'))))) -> TOP(f(f(start(f(match(X, y'))))))
TOP(mark(f(f(f(y''))))) -> TOP(f(f(start(f(proper(y''))))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 6
↳Nar
→DP Problem 12
↳Nar
...
→DP Problem 30
↳Narrowing Transformation
TOP(mark(f(f(f(y''))))) -> TOP(f(f(start(f(proper(y''))))))
TOP(mark(f(f(f(f(x'')))))) -> TOP(f(f(f(f(start(match(f(X), x'')))))))
TOP(mark(f(f(f(f(f(x''))))))) -> TOP(f(f(f(f(f(check(x'')))))))
TOP(found(f(f(f(f(x')))))) -> TOP(f(f(f(f(active(x'))))))
TOP(found(f(f(f(f(x')))))) -> TOP(f(f(f(mark(x')))))
TOP(found(f(f(f(x'''))))) -> TOP(f(mark(f(x'''))))
TOP(mark(f(f(x')))) -> TOP(start(f(f(proper(x')))))
TOP(mark(f(c))) -> TOP(start(f(ok(c))))
TOP(mark(f(f(y'')))) -> TOP(f(start(f(proper(y'')))))
TOP(mark(f(f(f(f(y')))))) -> TOP(f(f(f(start(f(match(X, y')))))))
active(f(x)) -> mark(x)
active(f(x)) -> f(active(x))
top(active(c)) -> top(mark(c))
top(mark(x)) -> top(check(x))
top(found(x)) -> top(active(x))
check(f(x)) -> f(check(x))
check(x) -> start(match(f(X), x))
match(f(x), f(y)) -> f(match(x, y))
match(X, x) -> proper(x)
proper(c) -> ok(c)
proper(f(x)) -> f(proper(x))
f(ok(x)) -> ok(f(x))
f(found(x)) -> found(f(x))
f(mark(x)) -> mark(f(x))
start(ok(x)) -> found(x)
two new Dependency Pairs are created:
TOP(mark(f(f(y'')))) -> TOP(f(start(f(proper(y'')))))
TOP(mark(f(f(c)))) -> TOP(f(start(f(ok(c)))))
TOP(mark(f(f(f(x'))))) -> TOP(f(start(f(f(proper(x'))))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 6
↳Nar
→DP Problem 12
↳Nar
...
→DP Problem 31
↳Narrowing Transformation
TOP(mark(f(f(f(x'))))) -> TOP(f(start(f(f(proper(x'))))))
TOP(mark(f(f(c)))) -> TOP(f(start(f(ok(c)))))
TOP(mark(f(f(f(f(y')))))) -> TOP(f(f(f(start(f(match(X, y')))))))
TOP(mark(f(f(f(f(x'')))))) -> TOP(f(f(f(f(start(match(f(X), x'')))))))
TOP(mark(f(f(f(f(f(x''))))))) -> TOP(f(f(f(f(f(check(x'')))))))
TOP(found(f(f(f(f(x')))))) -> TOP(f(f(f(f(active(x'))))))
TOP(found(f(f(f(f(x')))))) -> TOP(f(f(f(mark(x')))))
TOP(found(f(f(f(x'''))))) -> TOP(f(mark(f(x'''))))
TOP(mark(f(f(x')))) -> TOP(start(f(f(proper(x')))))
TOP(mark(f(c))) -> TOP(start(f(ok(c))))
TOP(mark(f(f(f(y''))))) -> TOP(f(f(start(f(proper(y''))))))
active(f(x)) -> mark(x)
active(f(x)) -> f(active(x))
top(active(c)) -> top(mark(c))
top(mark(x)) -> top(check(x))
top(found(x)) -> top(active(x))
check(f(x)) -> f(check(x))
check(x) -> start(match(f(X), x))
match(f(x), f(y)) -> f(match(x, y))
match(X, x) -> proper(x)
proper(c) -> ok(c)
proper(f(x)) -> f(proper(x))
f(ok(x)) -> ok(f(x))
f(found(x)) -> found(f(x))
f(mark(x)) -> mark(f(x))
start(ok(x)) -> found(x)
one new Dependency Pair is created:
TOP(mark(f(c))) -> TOP(start(f(ok(c))))
TOP(mark(f(c))) -> TOP(start(ok(f(c))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 6
↳Nar
→DP Problem 12
↳Nar
...
→DP Problem 32
↳Narrowing Transformation
TOP(mark(f(c))) -> TOP(start(ok(f(c))))
TOP(mark(f(f(c)))) -> TOP(f(start(f(ok(c)))))
TOP(mark(f(f(f(y''))))) -> TOP(f(f(start(f(proper(y''))))))
TOP(mark(f(f(f(f(y')))))) -> TOP(f(f(f(start(f(match(X, y')))))))
TOP(mark(f(f(f(f(x'')))))) -> TOP(f(f(f(f(start(match(f(X), x'')))))))
TOP(mark(f(f(f(f(f(x''))))))) -> TOP(f(f(f(f(f(check(x'')))))))
TOP(found(f(f(f(f(x')))))) -> TOP(f(f(f(f(active(x'))))))
TOP(found(f(f(f(f(x')))))) -> TOP(f(f(f(mark(x')))))
TOP(found(f(f(f(x'''))))) -> TOP(f(mark(f(x'''))))
TOP(mark(f(f(x')))) -> TOP(start(f(f(proper(x')))))
TOP(mark(f(f(f(x'))))) -> TOP(f(start(f(f(proper(x'))))))
active(f(x)) -> mark(x)
active(f(x)) -> f(active(x))
top(active(c)) -> top(mark(c))
top(mark(x)) -> top(check(x))
top(found(x)) -> top(active(x))
check(f(x)) -> f(check(x))
check(x) -> start(match(f(X), x))
match(f(x), f(y)) -> f(match(x, y))
match(X, x) -> proper(x)
proper(c) -> ok(c)
proper(f(x)) -> f(proper(x))
f(ok(x)) -> ok(f(x))
f(found(x)) -> found(f(x))
f(mark(x)) -> mark(f(x))
start(ok(x)) -> found(x)
two new Dependency Pairs are created:
TOP(mark(f(f(x')))) -> TOP(start(f(f(proper(x')))))
TOP(mark(f(f(c)))) -> TOP(start(f(f(ok(c)))))
TOP(mark(f(f(f(x''))))) -> TOP(start(f(f(f(proper(x''))))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 6
↳Nar
→DP Problem 12
↳Nar
...
→DP Problem 33
↳Narrowing Transformation
TOP(mark(f(f(f(x''))))) -> TOP(start(f(f(f(proper(x''))))))
TOP(mark(f(f(c)))) -> TOP(start(f(f(ok(c)))))
TOP(mark(f(f(f(x'))))) -> TOP(f(start(f(f(proper(x'))))))
TOP(mark(f(f(c)))) -> TOP(f(start(f(ok(c)))))
TOP(mark(f(f(f(y''))))) -> TOP(f(f(start(f(proper(y''))))))
TOP(mark(f(f(f(f(y')))))) -> TOP(f(f(f(start(f(match(X, y')))))))
TOP(mark(f(f(f(f(x'')))))) -> TOP(f(f(f(f(start(match(f(X), x'')))))))
TOP(mark(f(f(f(f(f(x''))))))) -> TOP(f(f(f(f(f(check(x'')))))))
TOP(found(f(f(f(f(x')))))) -> TOP(f(f(f(f(active(x'))))))
TOP(found(f(f(f(f(x')))))) -> TOP(f(f(f(mark(x')))))
TOP(found(f(f(f(x'''))))) -> TOP(f(mark(f(x'''))))
TOP(mark(f(c))) -> TOP(start(ok(f(c))))
active(f(x)) -> mark(x)
active(f(x)) -> f(active(x))
top(active(c)) -> top(mark(c))
top(mark(x)) -> top(check(x))
top(found(x)) -> top(active(x))
check(f(x)) -> f(check(x))
check(x) -> start(match(f(X), x))
match(f(x), f(y)) -> f(match(x, y))
match(X, x) -> proper(x)
proper(c) -> ok(c)
proper(f(x)) -> f(proper(x))
f(ok(x)) -> ok(f(x))
f(found(x)) -> found(f(x))
f(mark(x)) -> mark(f(x))
start(ok(x)) -> found(x)
four new Dependency Pairs are created:
TOP(found(f(f(f(x'''))))) -> TOP(f(mark(f(x'''))))
TOP(found(f(f(f(x''''))))) -> TOP(mark(f(f(x''''))))
TOP(found(f(f(f(ok(x')))))) -> TOP(f(mark(ok(f(x')))))
TOP(found(f(f(f(found(x')))))) -> TOP(f(mark(found(f(x')))))
TOP(found(f(f(f(mark(x')))))) -> TOP(f(mark(mark(f(x')))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 6
↳Nar
→DP Problem 12
↳Nar
...
→DP Problem 34
↳Narrowing Transformation
TOP(found(f(f(f(mark(x')))))) -> TOP(f(mark(mark(f(x')))))
TOP(found(f(f(f(found(x')))))) -> TOP(f(mark(found(f(x')))))
TOP(found(f(f(f(ok(x')))))) -> TOP(f(mark(ok(f(x')))))
TOP(found(f(f(f(x''''))))) -> TOP(mark(f(f(x''''))))
TOP(mark(f(f(c)))) -> TOP(start(f(f(ok(c)))))
TOP(mark(f(c))) -> TOP(start(ok(f(c))))
TOP(mark(f(f(f(x'))))) -> TOP(f(start(f(f(proper(x'))))))
TOP(mark(f(f(c)))) -> TOP(f(start(f(ok(c)))))
TOP(mark(f(f(f(y''))))) -> TOP(f(f(start(f(proper(y''))))))
TOP(mark(f(f(f(f(y')))))) -> TOP(f(f(f(start(f(match(X, y')))))))
TOP(mark(f(f(f(f(x'')))))) -> TOP(f(f(f(f(start(match(f(X), x'')))))))
TOP(mark(f(f(f(f(f(x''))))))) -> TOP(f(f(f(f(f(check(x'')))))))
TOP(found(f(f(f(f(x')))))) -> TOP(f(f(f(f(active(x'))))))
TOP(found(f(f(f(f(x')))))) -> TOP(f(f(f(mark(x')))))
TOP(mark(f(f(f(x''))))) -> TOP(start(f(f(f(proper(x''))))))
active(f(x)) -> mark(x)
active(f(x)) -> f(active(x))
top(active(c)) -> top(mark(c))
top(mark(x)) -> top(check(x))
top(found(x)) -> top(active(x))
check(f(x)) -> f(check(x))
check(x) -> start(match(f(X), x))
match(f(x), f(y)) -> f(match(x, y))
match(X, x) -> proper(x)
proper(c) -> ok(c)
proper(f(x)) -> f(proper(x))
f(ok(x)) -> ok(f(x))
f(found(x)) -> found(f(x))
f(mark(x)) -> mark(f(x))
start(ok(x)) -> found(x)
one new Dependency Pair is created:
TOP(found(f(f(f(f(x')))))) -> TOP(f(f(f(mark(x')))))
TOP(found(f(f(f(f(x'')))))) -> TOP(f(f(mark(f(x'')))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 6
↳Nar
→DP Problem 12
↳Nar
...
→DP Problem 35
↳Narrowing Transformation
TOP(found(f(f(f(f(x'')))))) -> TOP(f(f(mark(f(x'')))))
TOP(found(f(f(f(found(x')))))) -> TOP(f(mark(found(f(x')))))
TOP(found(f(f(f(ok(x')))))) -> TOP(f(mark(ok(f(x')))))
TOP(found(f(f(f(x''''))))) -> TOP(mark(f(f(x''''))))
TOP(mark(f(f(f(x''))))) -> TOP(start(f(f(f(proper(x''))))))
TOP(mark(f(f(c)))) -> TOP(start(f(f(ok(c)))))
TOP(mark(f(c))) -> TOP(start(ok(f(c))))
TOP(mark(f(f(f(x'))))) -> TOP(f(start(f(f(proper(x'))))))
TOP(mark(f(f(c)))) -> TOP(f(start(f(ok(c)))))
TOP(mark(f(f(f(y''))))) -> TOP(f(f(start(f(proper(y''))))))
TOP(mark(f(f(f(f(y')))))) -> TOP(f(f(f(start(f(match(X, y')))))))
TOP(mark(f(f(f(f(x'')))))) -> TOP(f(f(f(f(start(match(f(X), x'')))))))
TOP(mark(f(f(f(f(f(x''))))))) -> TOP(f(f(f(f(f(check(x'')))))))
TOP(found(f(f(f(f(x')))))) -> TOP(f(f(f(f(active(x'))))))
TOP(found(f(f(f(mark(x')))))) -> TOP(f(mark(mark(f(x')))))
active(f(x)) -> mark(x)
active(f(x)) -> f(active(x))
top(active(c)) -> top(mark(c))
top(mark(x)) -> top(check(x))
top(found(x)) -> top(active(x))
check(f(x)) -> f(check(x))
check(x) -> start(match(f(X), x))
match(f(x), f(y)) -> f(match(x, y))
match(X, x) -> proper(x)
proper(c) -> ok(c)
proper(f(x)) -> f(proper(x))
f(ok(x)) -> ok(f(x))
f(found(x)) -> found(f(x))
f(mark(x)) -> mark(f(x))
start(ok(x)) -> found(x)
two new Dependency Pairs are created:
TOP(found(f(f(f(f(x')))))) -> TOP(f(f(f(f(active(x'))))))
TOP(found(f(f(f(f(f(x''))))))) -> TOP(f(f(f(f(mark(x''))))))
TOP(found(f(f(f(f(f(x''))))))) -> TOP(f(f(f(f(f(active(x'')))))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 6
↳Nar
→DP Problem 12
↳Nar
...
→DP Problem 36
↳Argument Filtering and Ordering
TOP(found(f(f(f(f(f(x''))))))) -> TOP(f(f(f(f(f(active(x'')))))))
TOP(found(f(f(f(f(f(x''))))))) -> TOP(f(f(f(f(mark(x''))))))
TOP(found(f(f(f(mark(x')))))) -> TOP(f(mark(mark(f(x')))))
TOP(found(f(f(f(found(x')))))) -> TOP(f(mark(found(f(x')))))
TOP(found(f(f(f(ok(x')))))) -> TOP(f(mark(ok(f(x')))))
TOP(found(f(f(f(x''''))))) -> TOP(mark(f(f(x''''))))
TOP(mark(f(f(f(x''))))) -> TOP(start(f(f(f(proper(x''))))))
TOP(mark(f(f(c)))) -> TOP(start(f(f(ok(c)))))
TOP(mark(f(c))) -> TOP(start(ok(f(c))))
TOP(mark(f(f(f(x'))))) -> TOP(f(start(f(f(proper(x'))))))
TOP(mark(f(f(c)))) -> TOP(f(start(f(ok(c)))))
TOP(mark(f(f(f(y''))))) -> TOP(f(f(start(f(proper(y''))))))
TOP(mark(f(f(f(f(y')))))) -> TOP(f(f(f(start(f(match(X, y')))))))
TOP(mark(f(f(f(f(x'')))))) -> TOP(f(f(f(f(start(match(f(X), x'')))))))
TOP(mark(f(f(f(f(f(x''))))))) -> TOP(f(f(f(f(f(check(x'')))))))
TOP(found(f(f(f(f(x'')))))) -> TOP(f(f(mark(f(x'')))))
active(f(x)) -> mark(x)
active(f(x)) -> f(active(x))
top(active(c)) -> top(mark(c))
top(mark(x)) -> top(check(x))
top(found(x)) -> top(active(x))
check(f(x)) -> f(check(x))
check(x) -> start(match(f(X), x))
match(f(x), f(y)) -> f(match(x, y))
match(X, x) -> proper(x)
proper(c) -> ok(c)
proper(f(x)) -> f(proper(x))
f(ok(x)) -> ok(f(x))
f(found(x)) -> found(f(x))
f(mark(x)) -> mark(f(x))
start(ok(x)) -> found(x)
TOP(found(f(f(f(f(f(x''))))))) -> TOP(f(f(f(f(mark(x''))))))
TOP(found(f(f(f(mark(x')))))) -> TOP(f(mark(mark(f(x')))))
TOP(found(f(f(f(found(x')))))) -> TOP(f(mark(found(f(x')))))
TOP(found(f(f(f(ok(x')))))) -> TOP(f(mark(ok(f(x')))))
TOP(found(f(f(f(x''''))))) -> TOP(mark(f(f(x''''))))
TOP(found(f(f(f(f(x'')))))) -> TOP(f(f(mark(f(x'')))))
f(ok(x)) -> ok(f(x))
f(found(x)) -> found(f(x))
f(mark(x)) -> mark(f(x))
check(f(x)) -> f(check(x))
check(x) -> start(match(f(X), x))
start(ok(x)) -> found(x)
proper(c) -> ok(c)
proper(f(x)) -> f(proper(x))
match(f(x), f(y)) -> f(match(x, y))
match(X, x) -> proper(x)
active(f(x)) -> mark(x)
active(f(x)) -> f(active(x))
TOP(x1) -> TOP(x1)
found(x1) -> x1
f(x1) -> f(x1)
mark(x1) -> x1
check(x1) -> x1
start(x1) -> x1
ok(x1) -> x1
proper(x1) -> x1
match(x1, x2) -> x2
active(x1) -> x1
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 6
↳Nar
→DP Problem 12
↳Nar
...
→DP Problem 37
↳Remaining Obligation(s)
TOP(found(f(f(f(f(f(x''))))))) -> TOP(f(f(f(f(f(active(x'')))))))
TOP(mark(f(f(f(x''))))) -> TOP(start(f(f(f(proper(x''))))))
TOP(mark(f(f(c)))) -> TOP(start(f(f(ok(c)))))
TOP(mark(f(c))) -> TOP(start(ok(f(c))))
TOP(mark(f(f(f(x'))))) -> TOP(f(start(f(f(proper(x'))))))
TOP(mark(f(f(c)))) -> TOP(f(start(f(ok(c)))))
TOP(mark(f(f(f(y''))))) -> TOP(f(f(start(f(proper(y''))))))
TOP(mark(f(f(f(f(y')))))) -> TOP(f(f(f(start(f(match(X, y')))))))
TOP(mark(f(f(f(f(x'')))))) -> TOP(f(f(f(f(start(match(f(X), x'')))))))
TOP(mark(f(f(f(f(f(x''))))))) -> TOP(f(f(f(f(f(check(x'')))))))
active(f(x)) -> mark(x)
active(f(x)) -> f(active(x))
top(active(c)) -> top(mark(c))
top(mark(x)) -> top(check(x))
top(found(x)) -> top(active(x))
check(f(x)) -> f(check(x))
check(x) -> start(match(f(X), x))
match(f(x), f(y)) -> f(match(x, y))
match(X, x) -> proper(x)
proper(c) -> ok(c)
proper(f(x)) -> f(proper(x))
f(ok(x)) -> ok(f(x))
f(found(x)) -> found(f(x))
f(mark(x)) -> mark(f(x))
start(ok(x)) -> found(x)