R
↳Dependency Pair Analysis
MINUS(s(x), s(y)) -> MINUS(x, y)
DOUBLE(s(x)) -> DOUBLE(x)
PLUS(s(x), y) -> PLUS(x, y)
PLUS(s(x), y) -> PLUS(x, s(y))
PLUS(s(x), y) -> PLUS(minus(x, y), double(y))
PLUS(s(x), y) -> MINUS(x, y)
PLUS(s(x), y) -> DOUBLE(y)
PLUS(s(plus(x, y)), z) -> PLUS(plus(x, y), z)
R
↳DPs
→DP Problem 1
↳Argument Filtering and Ordering
→DP Problem 2
↳AFS
→DP Problem 3
↳Nar
MINUS(s(x), s(y)) -> MINUS(x, y)
minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
double(0) -> 0
double(s(x)) -> s(s(double(x)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
plus(s(x), y) -> plus(x, s(y))
plus(s(x), y) -> s(plus(minus(x, y), double(y)))
plus(s(plus(x, y)), z) -> s(plus(plus(x, y), z))
MINUS(s(x), s(y)) -> MINUS(x, y)
MINUS(x1, x2) -> MINUS(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
minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
double(0) -> 0
double(s(x)) -> s(s(double(x)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
plus(s(x), y) -> plus(x, s(y))
plus(s(x), y) -> s(plus(minus(x, y), double(y)))
plus(s(plus(x, y)), z) -> s(plus(plus(x, y), z))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Argument Filtering and Ordering
→DP Problem 3
↳Nar
DOUBLE(s(x)) -> DOUBLE(x)
minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
double(0) -> 0
double(s(x)) -> s(s(double(x)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
plus(s(x), y) -> plus(x, s(y))
plus(s(x), y) -> s(plus(minus(x, y), double(y)))
plus(s(plus(x, y)), z) -> s(plus(plus(x, y), z))
DOUBLE(s(x)) -> DOUBLE(x)
DOUBLE(x1) -> DOUBLE(x1)
s(x1) -> s(x1)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 5
↳Dependency Graph
→DP Problem 3
↳Nar
minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
double(0) -> 0
double(s(x)) -> s(s(double(x)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
plus(s(x), y) -> plus(x, s(y))
plus(s(x), y) -> s(plus(minus(x, y), double(y)))
plus(s(plus(x, y)), z) -> s(plus(plus(x, y), z))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳Narrowing Transformation
PLUS(s(plus(x, y)), z) -> PLUS(plus(x, y), z)
PLUS(s(x), y) -> PLUS(minus(x, y), double(y))
PLUS(s(x), y) -> PLUS(x, s(y))
PLUS(s(x), y) -> PLUS(x, y)
minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
double(0) -> 0
double(s(x)) -> s(s(double(x)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
plus(s(x), y) -> plus(x, s(y))
plus(s(x), y) -> s(plus(minus(x, y), double(y)))
plus(s(plus(x, y)), z) -> s(plus(plus(x, y), z))
five new Dependency Pairs are created:
PLUS(s(plus(x, y)), z) -> PLUS(plus(x, y), z)
PLUS(s(plus(0, y'')), z) -> PLUS(y'', z)
PLUS(s(plus(s(x''), y'')), z) -> PLUS(s(plus(x'', y'')), z)
PLUS(s(plus(s(x''), y'')), z) -> PLUS(plus(x'', s(y'')), z)
PLUS(s(plus(s(x''), y'')), z) -> PLUS(s(plus(minus(x'', y''), double(y''))), z)
PLUS(s(plus(s(plus(x'', y'')), y0)), z) -> PLUS(s(plus(plus(x'', y''), y0)), z)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳Nar
→DP Problem 6
↳Argument Filtering and Ordering
PLUS(s(plus(s(plus(x'', y'')), y0)), z) -> PLUS(s(plus(plus(x'', y''), y0)), z)
PLUS(s(plus(s(x''), y'')), z) -> PLUS(s(plus(minus(x'', y''), double(y''))), z)
PLUS(s(plus(s(x''), y'')), z) -> PLUS(plus(x'', s(y'')), z)
PLUS(s(plus(s(x''), y'')), z) -> PLUS(s(plus(x'', y'')), z)
PLUS(s(plus(0, y'')), z) -> PLUS(y'', z)
PLUS(s(x), y) -> PLUS(x, s(y))
PLUS(s(x), y) -> PLUS(x, y)
PLUS(s(x), y) -> PLUS(minus(x, y), double(y))
minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
double(0) -> 0
double(s(x)) -> s(s(double(x)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
plus(s(x), y) -> plus(x, s(y))
plus(s(x), y) -> s(plus(minus(x, y), double(y)))
plus(s(plus(x, y)), z) -> s(plus(plus(x, y), z))
PLUS(s(plus(0, y'')), z) -> PLUS(y'', z)
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
plus(s(x), y) -> plus(x, s(y))
plus(s(x), y) -> s(plus(minus(x, y), double(y)))
plus(s(plus(x, y)), z) -> s(plus(plus(x, y), z))
minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
double(0) -> 0
double(s(x)) -> s(s(double(x)))
PLUS(x1, x2) -> PLUS(x1, x2)
s(x1) -> x1
plus(x1, x2) -> plus(x1, x2)
minus(x1, x2) -> x1
double(x1) -> x1
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳Nar
→DP Problem 6
↳AFS
...
→DP Problem 7
↳Remaining Obligation(s)
PLUS(s(plus(s(plus(x'', y'')), y0)), z) -> PLUS(s(plus(plus(x'', y''), y0)), z)
PLUS(s(plus(s(x''), y'')), z) -> PLUS(s(plus(minus(x'', y''), double(y''))), z)
PLUS(s(plus(s(x''), y'')), z) -> PLUS(plus(x'', s(y'')), z)
PLUS(s(plus(s(x''), y'')), z) -> PLUS(s(plus(x'', y'')), z)
PLUS(s(x), y) -> PLUS(x, s(y))
PLUS(s(x), y) -> PLUS(x, y)
PLUS(s(x), y) -> PLUS(minus(x, y), double(y))
minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
double(0) -> 0
double(s(x)) -> s(s(double(x)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
plus(s(x), y) -> plus(x, s(y))
plus(s(x), y) -> s(plus(minus(x, y), double(y)))
plus(s(plus(x, y)), z) -> s(plus(plus(x, y), z))