R
↳Dependency Pair Analysis
ACTIVE(f(x)) -> F(f(x))
CHK(no(f(x))) -> F(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x)))
CHK(no(f(x))) -> CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x))
CHK(no(f(x))) -> MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), x)
CHK(no(f(x))) -> F(f(f(f(f(f(f(f(f(f(X))))))))))
CHK(no(f(x))) -> F(f(f(f(f(f(f(f(f(X)))))))))
CHK(no(f(x))) -> F(f(f(f(f(f(f(f(X))))))))
CHK(no(f(x))) -> F(f(f(f(f(f(f(X)))))))
CHK(no(f(x))) -> F(f(f(f(f(f(X))))))
CHK(no(f(x))) -> F(f(f(f(f(X)))))
CHK(no(f(x))) -> F(f(f(f(X))))
CHK(no(f(x))) -> F(f(f(X)))
CHK(no(f(x))) -> F(f(X))
CHK(no(f(x))) -> F(X)
CHK(no(c)) -> ACTIVE(c)
MAT(f(x), f(y)) -> F(mat(x, y))
MAT(f(x), f(y)) -> MAT(x, y)
F(active(x)) -> ACTIVE(f(x))
F(active(x)) -> F(x)
F(no(x)) -> F(x)
F(mark(x)) -> F(x)
TP(mark(x)) -> TP(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x)))
TP(mark(x)) -> CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x))
TP(mark(x)) -> MAT(f(f(f(f(f(f(f(f(f(f(X)))))))))), x)
TP(mark(x)) -> F(f(f(f(f(f(f(f(f(f(X))))))))))
TP(mark(x)) -> F(f(f(f(f(f(f(f(f(X)))))))))
TP(mark(x)) -> F(f(f(f(f(f(f(f(X))))))))
TP(mark(x)) -> F(f(f(f(f(f(f(X)))))))
TP(mark(x)) -> F(f(f(f(f(f(X))))))
TP(mark(x)) -> F(f(f(f(f(X)))))
TP(mark(x)) -> F(f(f(f(X))))
TP(mark(x)) -> F(f(f(X)))
TP(mark(x)) -> F(f(X))
TP(mark(x)) -> F(X)
R
↳DPs
→DP Problem 1
↳Narrowing Transformation
→DP Problem 2
↳Nar
→DP Problem 3
↳Nar
F(mark(x)) -> F(x)
F(no(x)) -> F(x)
F(active(x)) -> F(x)
F(active(x)) -> ACTIVE(f(x))
ACTIVE(f(x)) -> F(f(x))
active(f(x)) -> mark(f(f(x)))
chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x)))
chk(no(c)) -> active(c)
mat(f(x), f(y)) -> f(mat(x, y))
mat(f(x), c) -> no(c)
f(active(x)) -> active(f(x))
f(no(x)) -> no(f(x))
f(mark(x)) -> mark(f(x))
tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x)))
three new Dependency Pairs are created:
ACTIVE(f(x)) -> F(f(x))
ACTIVE(f(active(x''))) -> F(active(f(x'')))
ACTIVE(f(no(x''))) -> F(no(f(x'')))
ACTIVE(f(mark(x''))) -> F(mark(f(x'')))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 4
↳Argument Filtering and Ordering
→DP Problem 2
↳Nar
→DP Problem 3
↳Nar
ACTIVE(f(mark(x''))) -> F(mark(f(x'')))
ACTIVE(f(no(x''))) -> F(no(f(x'')))
F(no(x)) -> F(x)
F(active(x)) -> F(x)
ACTIVE(f(active(x''))) -> F(active(f(x'')))
F(active(x)) -> ACTIVE(f(x))
F(mark(x)) -> F(x)
active(f(x)) -> mark(f(f(x)))
chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x)))
chk(no(c)) -> active(c)
mat(f(x), f(y)) -> f(mat(x, y))
mat(f(x), c) -> no(c)
f(active(x)) -> active(f(x))
f(no(x)) -> no(f(x))
f(mark(x)) -> mark(f(x))
tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x)))
F(active(x)) -> F(x)
F(active(x)) -> ACTIVE(f(x))
f(active(x)) -> active(f(x))
f(no(x)) -> no(f(x))
f(mark(x)) -> mark(f(x))
active(f(x)) -> mark(f(f(x)))
POL(active(x1)) = 1 + x1 POL(ACTIVE(x1)) = x1 POL(no(x1)) = x1 POL(mark(x1)) = x1 POL(F(x1)) = x1 POL(f(x1)) = x1
F(x1) -> F(x1)
active(x1) -> active(x1)
mark(x1) -> mark(x1)
ACTIVE(x1) -> ACTIVE(x1)
no(x1) -> no(x1)
f(x1) -> f(x1)
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 4
↳AFS
...
→DP Problem 5
↳Dependency Graph
→DP Problem 2
↳Nar
→DP Problem 3
↳Nar
ACTIVE(f(mark(x''))) -> F(mark(f(x'')))
ACTIVE(f(no(x''))) -> F(no(f(x'')))
F(no(x)) -> F(x)
ACTIVE(f(active(x''))) -> F(active(f(x'')))
F(mark(x)) -> F(x)
active(f(x)) -> mark(f(f(x)))
chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x)))
chk(no(c)) -> active(c)
mat(f(x), f(y)) -> f(mat(x, y))
mat(f(x), c) -> no(c)
f(active(x)) -> active(f(x))
f(no(x)) -> no(f(x))
f(mark(x)) -> mark(f(x))
tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x)))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 4
↳AFS
...
→DP Problem 6
↳Argument Filtering and Ordering
→DP Problem 2
↳Nar
→DP Problem 3
↳Nar
F(no(x)) -> F(x)
F(mark(x)) -> F(x)
active(f(x)) -> mark(f(f(x)))
chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x)))
chk(no(c)) -> active(c)
mat(f(x), f(y)) -> f(mat(x, y))
mat(f(x), c) -> no(c)
f(active(x)) -> active(f(x))
f(no(x)) -> no(f(x))
f(mark(x)) -> mark(f(x))
tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x)))
F(mark(x)) -> F(x)
POL(no(x1)) = x1 POL(mark(x1)) = 1 + x1 POL(F(x1)) = x1
F(x1) -> F(x1)
mark(x1) -> mark(x1)
no(x1) -> no(x1)
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 4
↳AFS
...
→DP Problem 7
↳Argument Filtering and Ordering
→DP Problem 2
↳Nar
→DP Problem 3
↳Nar
F(no(x)) -> F(x)
active(f(x)) -> mark(f(f(x)))
chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x)))
chk(no(c)) -> active(c)
mat(f(x), f(y)) -> f(mat(x, y))
mat(f(x), c) -> no(c)
f(active(x)) -> active(f(x))
f(no(x)) -> no(f(x))
f(mark(x)) -> mark(f(x))
tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x)))
F(no(x)) -> F(x)
POL(no(x1)) = 1 + x1 POL(F(x1)) = x1
F(x1) -> F(x1)
no(x1) -> no(x1)
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 4
↳AFS
...
→DP Problem 8
↳Dependency Graph
→DP Problem 2
↳Nar
→DP Problem 3
↳Nar
active(f(x)) -> mark(f(f(x)))
chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x)))
chk(no(c)) -> active(c)
mat(f(x), f(y)) -> f(mat(x, y))
mat(f(x), c) -> no(c)
f(active(x)) -> active(f(x))
f(no(x)) -> no(f(x))
f(mark(x)) -> mark(f(x))
tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x)))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Narrowing Transformation
→DP Problem 3
↳Nar
CHK(no(f(x))) -> CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x))
active(f(x)) -> mark(f(f(x)))
chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x)))
chk(no(c)) -> active(c)
mat(f(x), f(y)) -> f(mat(x, y))
mat(f(x), c) -> no(c)
f(active(x)) -> active(f(x))
f(no(x)) -> no(f(x))
f(mark(x)) -> mark(f(x))
tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x)))
two new Dependency Pairs are created:
CHK(no(f(x))) -> CHK(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x))
CHK(no(f(f(y)))) -> CHK(f(mat(f(f(f(f(f(f(f(f(f(X))))))))), y)))
CHK(no(f(c))) -> CHK(no(c))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
→DP Problem 9
↳Narrowing Transformation
→DP Problem 3
↳Nar
CHK(no(f(f(y)))) -> CHK(f(mat(f(f(f(f(f(f(f(f(f(X))))))))), y)))
active(f(x)) -> mark(f(f(x)))
chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x)))
chk(no(c)) -> active(c)
mat(f(x), f(y)) -> f(mat(x, y))
mat(f(x), c) -> no(c)
f(active(x)) -> active(f(x))
f(no(x)) -> no(f(x))
f(mark(x)) -> mark(f(x))
tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x)))
no new Dependency Pairs are created.
CHK(no(f(f(y)))) -> CHK(f(mat(f(f(f(f(f(f(f(f(f(X))))))))), y)))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
→DP Problem 3
↳Narrowing Transformation
TP(mark(x)) -> TP(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x)))
active(f(x)) -> mark(f(f(x)))
chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x)))
chk(no(c)) -> active(c)
mat(f(x), f(y)) -> f(mat(x, y))
mat(f(x), c) -> no(c)
f(active(x)) -> active(f(x))
f(no(x)) -> no(f(x))
f(mark(x)) -> mark(f(x))
tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x)))
two new Dependency Pairs are created:
TP(mark(x)) -> TP(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x)))
TP(mark(f(y))) -> TP(chk(f(mat(f(f(f(f(f(f(f(f(f(X))))))))), y))))
TP(mark(c)) -> TP(chk(no(c)))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
→DP Problem 3
↳Nar
→DP Problem 10
↳Narrowing Transformation
TP(mark(c)) -> TP(chk(no(c)))
TP(mark(f(y))) -> TP(chk(f(mat(f(f(f(f(f(f(f(f(f(X))))))))), y))))
active(f(x)) -> mark(f(f(x)))
chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x)))
chk(no(c)) -> active(c)
mat(f(x), f(y)) -> f(mat(x, y))
mat(f(x), c) -> no(c)
f(active(x)) -> active(f(x))
f(no(x)) -> no(f(x))
f(mark(x)) -> mark(f(x))
tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x)))
no new Dependency Pairs are created.
TP(mark(f(y))) -> TP(chk(f(mat(f(f(f(f(f(f(f(f(f(X))))))))), y))))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
→DP Problem 3
↳Nar
→DP Problem 10
↳Nar
...
→DP Problem 11
↳Narrowing Transformation
TP(mark(c)) -> TP(chk(no(c)))
active(f(x)) -> mark(f(f(x)))
chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x)))
chk(no(c)) -> active(c)
mat(f(x), f(y)) -> f(mat(x, y))
mat(f(x), c) -> no(c)
f(active(x)) -> active(f(x))
f(no(x)) -> no(f(x))
f(mark(x)) -> mark(f(x))
tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x)))
one new Dependency Pair is created:
TP(mark(c)) -> TP(chk(no(c)))
TP(mark(c)) -> TP(active(c))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
→DP Problem 3
↳Nar
→DP Problem 10
↳Nar
...
→DP Problem 12
↳Narrowing Transformation
TP(mark(c)) -> TP(active(c))
active(f(x)) -> mark(f(f(x)))
chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x)))
chk(no(c)) -> active(c)
mat(f(x), f(y)) -> f(mat(x, y))
mat(f(x), c) -> no(c)
f(active(x)) -> active(f(x))
f(no(x)) -> no(f(x))
f(mark(x)) -> mark(f(x))
tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X)))))))))), x)))
no new Dependency Pairs are created.
TP(mark(c)) -> TP(active(c))