R
↳Dependency Pair Analysis
MIN(s(X), s(Y)) -> MIN(X, Y)
QUOT(s(X), s(Y)) -> QUOT(min(X, Y), s(Y))
QUOT(s(X), s(Y)) -> MIN(X, Y)
LOG(s(s(X))) -> LOG(s(quot(X, s(s(0)))))
LOG(s(s(X))) -> QUOT(X, s(s(0)))
R
↳DPs
→DP Problem 1
↳Argument Filtering and Ordering
→DP Problem 2
↳AFS
→DP Problem 3
↳Nar
MIN(s(X), s(Y)) -> MIN(X, Y)
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
log(s(0)) -> 0
log(s(s(X))) -> s(log(s(quot(X, s(s(0))))))
MIN(s(X), s(Y)) -> MIN(X, Y)
MIN(x1, x2) -> MIN(x1, x2)
s(x1) -> s(x1)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 4
↳Dependency Graph
→DP Problem 2
↳AFS
→DP Problem 3
↳Nar
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
log(s(0)) -> 0
log(s(s(X))) -> s(log(s(quot(X, s(s(0))))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Argument Filtering and Ordering
→DP Problem 3
↳Nar
QUOT(s(X), s(Y)) -> QUOT(min(X, Y), s(Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
log(s(0)) -> 0
log(s(s(X))) -> s(log(s(quot(X, s(s(0))))))
QUOT(s(X), s(Y)) -> QUOT(min(X, Y), s(Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
QUOT(x1, x2) -> QUOT(x1, x2)
s(x1) -> s(x1)
min(x1, x2) -> x1
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 5
↳Dependency Graph
→DP Problem 3
↳Nar
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
log(s(0)) -> 0
log(s(s(X))) -> s(log(s(quot(X, s(s(0))))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳Narrowing Transformation
LOG(s(s(X))) -> LOG(s(quot(X, s(s(0)))))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
log(s(0)) -> 0
log(s(s(X))) -> s(log(s(quot(X, s(s(0))))))
two new Dependency Pairs are created:
LOG(s(s(X))) -> LOG(s(quot(X, s(s(0)))))
LOG(s(s(0))) -> LOG(s(0))
LOG(s(s(s(X'')))) -> LOG(s(s(quot(min(X'', s(0)), s(s(0))))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳Nar
→DP Problem 6
↳Narrowing Transformation
LOG(s(s(s(X'')))) -> LOG(s(s(quot(min(X'', s(0)), s(s(0))))))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
log(s(0)) -> 0
log(s(s(X))) -> s(log(s(quot(X, s(s(0))))))
one new Dependency Pair is created:
LOG(s(s(s(X'')))) -> LOG(s(s(quot(min(X'', s(0)), s(s(0))))))
LOG(s(s(s(s(X'))))) -> LOG(s(s(quot(min(X', 0), s(s(0))))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳Nar
→DP Problem 6
↳Nar
...
→DP Problem 7
↳Argument Filtering and Ordering
LOG(s(s(s(s(X'))))) -> LOG(s(s(quot(min(X', 0), s(s(0))))))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
log(s(0)) -> 0
log(s(s(X))) -> s(log(s(quot(X, s(s(0))))))
LOG(s(s(s(s(X'))))) -> LOG(s(s(quot(min(X', 0), s(s(0))))))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
LOG(x1) -> LOG(x1)
s(x1) -> s(x1)
quot(x1, x2) -> x1
min(x1, x2) -> x1
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳Nar
→DP Problem 6
↳Nar
...
→DP Problem 8
↳Dependency Graph
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
log(s(0)) -> 0
log(s(s(X))) -> s(log(s(quot(X, s(s(0))))))