R
↳Dependency Pair Analysis
MINUS(s(x), s(y)) -> MINUS(p(s(x)), p(s(y)))
MINUS(s(x), s(y)) -> P(s(x))
MINUS(s(x), s(y)) -> P(s(y))
MINUS(x, plus(y, z)) -> MINUS(minus(x, y), z)
MINUS(x, plus(y, z)) -> MINUS(x, y)
P(s(s(x))) -> P(s(x))
DIV(s(x), s(y)) -> DIV(minus(x, y), s(y))
DIV(s(x), s(y)) -> MINUS(x, y)
DIV(plus(x, y), z) -> PLUS(div(x, z), div(y, z))
DIV(plus(x, y), z) -> DIV(x, z)
DIV(plus(x, y), z) -> DIV(y, z)
PLUS(s(x), y) -> PLUS(y, minus(s(x), s(0)))
PLUS(s(x), y) -> MINUS(s(x), s(0))
R
↳DPs
→DP Problem 1
↳Argument Filtering and Ordering
→DP Problem 2
↳Nar
→DP Problem 3
↳Remaining
→DP Problem 4
↳Remaining
P(s(s(x))) -> P(s(x))
minus(x, 0) -> x
minus(0, y) -> 0
minus(s(x), s(y)) -> minus(p(s(x)), p(s(y)))
minus(x, plus(y, z)) -> minus(minus(x, y), z)
p(s(s(x))) -> s(p(s(x)))
p(0) -> s(s(0))
div(s(x), s(y)) -> s(div(minus(x, y), s(y)))
div(plus(x, y), z) -> plus(div(x, z), div(y, z))
plus(0, y) -> y
plus(s(x), y) -> s(plus(y, minus(s(x), s(0))))
P(s(s(x))) -> P(s(x))
P(x1) -> P(x1)
s(x1) -> s(x1)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 5
↳Dependency Graph
→DP Problem 2
↳Nar
→DP Problem 3
↳Remaining
→DP Problem 4
↳Remaining
minus(x, 0) -> x
minus(0, y) -> 0
minus(s(x), s(y)) -> minus(p(s(x)), p(s(y)))
minus(x, plus(y, z)) -> minus(minus(x, y), z)
p(s(s(x))) -> s(p(s(x)))
p(0) -> s(s(0))
div(s(x), s(y)) -> s(div(minus(x, y), s(y)))
div(plus(x, y), z) -> plus(div(x, z), div(y, z))
plus(0, y) -> y
plus(s(x), y) -> s(plus(y, minus(s(x), s(0))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Narrowing Transformation
→DP Problem 3
↳Remaining
→DP Problem 4
↳Remaining
MINUS(x, plus(y, z)) -> MINUS(x, y)
MINUS(x, plus(y, z)) -> MINUS(minus(x, y), z)
MINUS(s(x), s(y)) -> MINUS(p(s(x)), p(s(y)))
minus(x, 0) -> x
minus(0, y) -> 0
minus(s(x), s(y)) -> minus(p(s(x)), p(s(y)))
minus(x, plus(y, z)) -> minus(minus(x, y), z)
p(s(s(x))) -> s(p(s(x)))
p(0) -> s(s(0))
div(s(x), s(y)) -> s(div(minus(x, y), s(y)))
div(plus(x, y), z) -> plus(div(x, z), div(y, z))
plus(0, y) -> y
plus(s(x), y) -> s(plus(y, minus(s(x), s(0))))
two new Dependency Pairs are created:
MINUS(s(x), s(y)) -> MINUS(p(s(x)), p(s(y)))
MINUS(s(s(x'')), s(y)) -> MINUS(s(p(s(x''))), p(s(y)))
MINUS(s(x), s(s(x''))) -> MINUS(p(s(x)), s(p(s(x''))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 6
↳Narrowing Transformation
→DP Problem 3
↳Remaining
→DP Problem 4
↳Remaining
MINUS(s(x), s(s(x''))) -> MINUS(p(s(x)), s(p(s(x''))))
MINUS(s(s(x'')), s(y)) -> MINUS(s(p(s(x''))), p(s(y)))
MINUS(x, plus(y, z)) -> MINUS(minus(x, y), z)
MINUS(x, plus(y, z)) -> MINUS(x, y)
minus(x, 0) -> x
minus(0, y) -> 0
minus(s(x), s(y)) -> minus(p(s(x)), p(s(y)))
minus(x, plus(y, z)) -> minus(minus(x, y), z)
p(s(s(x))) -> s(p(s(x)))
p(0) -> s(s(0))
div(s(x), s(y)) -> s(div(minus(x, y), s(y)))
div(plus(x, y), z) -> plus(div(x, z), div(y, z))
plus(0, y) -> y
plus(s(x), y) -> s(plus(y, minus(s(x), s(0))))
two new Dependency Pairs are created:
MINUS(s(s(x'')), s(y)) -> MINUS(s(p(s(x''))), p(s(y)))
MINUS(s(s(s(x'))), s(y)) -> MINUS(s(s(p(s(x')))), p(s(y)))
MINUS(s(s(x'')), s(s(x'))) -> MINUS(s(p(s(x''))), s(p(s(x'))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 6
↳Nar
...
→DP Problem 7
↳Narrowing Transformation
→DP Problem 3
↳Remaining
→DP Problem 4
↳Remaining
MINUS(s(s(x'')), s(s(x'))) -> MINUS(s(p(s(x''))), s(p(s(x'))))
MINUS(x, plus(y, z)) -> MINUS(x, y)
MINUS(x, plus(y, z)) -> MINUS(minus(x, y), z)
MINUS(s(s(s(x'))), s(y)) -> MINUS(s(s(p(s(x')))), p(s(y)))
MINUS(s(x), s(s(x''))) -> MINUS(p(s(x)), s(p(s(x''))))
minus(x, 0) -> x
minus(0, y) -> 0
minus(s(x), s(y)) -> minus(p(s(x)), p(s(y)))
minus(x, plus(y, z)) -> minus(minus(x, y), z)
p(s(s(x))) -> s(p(s(x)))
p(0) -> s(s(0))
div(s(x), s(y)) -> s(div(minus(x, y), s(y)))
div(plus(x, y), z) -> plus(div(x, z), div(y, z))
plus(0, y) -> y
plus(s(x), y) -> s(plus(y, minus(s(x), s(0))))
two new Dependency Pairs are created:
MINUS(s(x), s(s(x''))) -> MINUS(p(s(x)), s(p(s(x''))))
MINUS(s(s(x''')), s(s(x''))) -> MINUS(s(p(s(x'''))), s(p(s(x''))))
MINUS(s(x), s(s(s(x''')))) -> MINUS(p(s(x)), s(s(p(s(x''')))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 6
↳Nar
...
→DP Problem 8
↳Argument Filtering and Ordering
→DP Problem 3
↳Remaining
→DP Problem 4
↳Remaining
MINUS(s(x), s(s(s(x''')))) -> MINUS(p(s(x)), s(s(p(s(x''')))))
MINUS(s(s(x''')), s(s(x''))) -> MINUS(s(p(s(x'''))), s(p(s(x''))))
MINUS(x, plus(y, z)) -> MINUS(x, y)
MINUS(x, plus(y, z)) -> MINUS(minus(x, y), z)
MINUS(s(s(s(x'))), s(y)) -> MINUS(s(s(p(s(x')))), p(s(y)))
MINUS(s(s(x'')), s(s(x'))) -> MINUS(s(p(s(x''))), s(p(s(x'))))
minus(x, 0) -> x
minus(0, y) -> 0
minus(s(x), s(y)) -> minus(p(s(x)), p(s(y)))
minus(x, plus(y, z)) -> minus(minus(x, y), z)
p(s(s(x))) -> s(p(s(x)))
p(0) -> s(s(0))
div(s(x), s(y)) -> s(div(minus(x, y), s(y)))
div(plus(x, y), z) -> plus(div(x, z), div(y, z))
plus(0, y) -> y
plus(s(x), y) -> s(plus(y, minus(s(x), s(0))))
MINUS(x, plus(y, z)) -> MINUS(x, y)
MINUS(x, plus(y, z)) -> MINUS(minus(x, y), z)
minus(x, 0) -> x
minus(0, y) -> 0
minus(s(x), s(y)) -> minus(p(s(x)), p(s(y)))
minus(x, plus(y, z)) -> minus(minus(x, y), z)
p(s(s(x))) -> s(p(s(x)))
p(0) -> s(s(0))
MINUS(x1, x2) -> MINUS(x1, x2)
plus(x1, x2) -> plus(x1, x2)
minus(x1, x2) -> x1
s(x1) -> x1
p(x1) -> x1
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 6
↳Nar
...
→DP Problem 9
↳Narrowing Transformation
→DP Problem 3
↳Remaining
→DP Problem 4
↳Remaining
MINUS(s(x), s(s(s(x''')))) -> MINUS(p(s(x)), s(s(p(s(x''')))))
MINUS(s(s(x''')), s(s(x''))) -> MINUS(s(p(s(x'''))), s(p(s(x''))))
MINUS(s(s(s(x'))), s(y)) -> MINUS(s(s(p(s(x')))), p(s(y)))
MINUS(s(s(x'')), s(s(x'))) -> MINUS(s(p(s(x''))), s(p(s(x'))))
minus(x, 0) -> x
minus(0, y) -> 0
minus(s(x), s(y)) -> minus(p(s(x)), p(s(y)))
minus(x, plus(y, z)) -> minus(minus(x, y), z)
p(s(s(x))) -> s(p(s(x)))
p(0) -> s(s(0))
div(s(x), s(y)) -> s(div(minus(x, y), s(y)))
div(plus(x, y), z) -> plus(div(x, z), div(y, z))
plus(0, y) -> y
plus(s(x), y) -> s(plus(y, minus(s(x), s(0))))
two new Dependency Pairs are created:
MINUS(s(s(s(x'))), s(y)) -> MINUS(s(s(p(s(x')))), p(s(y)))
MINUS(s(s(s(s(x'')))), s(y)) -> MINUS(s(s(s(p(s(x''))))), p(s(y)))
MINUS(s(s(s(x'))), s(s(x''))) -> MINUS(s(s(p(s(x')))), s(p(s(x''))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 6
↳Nar
...
→DP Problem 10
↳Narrowing Transformation
→DP Problem 3
↳Remaining
→DP Problem 4
↳Remaining
MINUS(s(s(s(x'))), s(s(x''))) -> MINUS(s(s(p(s(x')))), s(p(s(x''))))
MINUS(s(s(s(s(x'')))), s(y)) -> MINUS(s(s(s(p(s(x''))))), p(s(y)))
MINUS(s(s(x''')), s(s(x''))) -> MINUS(s(p(s(x'''))), s(p(s(x''))))
MINUS(s(s(x'')), s(s(x'))) -> MINUS(s(p(s(x''))), s(p(s(x'))))
MINUS(s(x), s(s(s(x''')))) -> MINUS(p(s(x)), s(s(p(s(x''')))))
minus(x, 0) -> x
minus(0, y) -> 0
minus(s(x), s(y)) -> minus(p(s(x)), p(s(y)))
minus(x, plus(y, z)) -> minus(minus(x, y), z)
p(s(s(x))) -> s(p(s(x)))
p(0) -> s(s(0))
div(s(x), s(y)) -> s(div(minus(x, y), s(y)))
div(plus(x, y), z) -> plus(div(x, z), div(y, z))
plus(0, y) -> y
plus(s(x), y) -> s(plus(y, minus(s(x), s(0))))
two new Dependency Pairs are created:
MINUS(s(s(x'')), s(s(x'))) -> MINUS(s(p(s(x''))), s(p(s(x'))))
MINUS(s(s(s(x0))), s(s(x'))) -> MINUS(s(s(p(s(x0)))), s(p(s(x'))))
MINUS(s(s(x'')), s(s(s(x0)))) -> MINUS(s(p(s(x''))), s(s(p(s(x0)))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 6
↳Nar
...
→DP Problem 11
↳Narrowing Transformation
→DP Problem 3
↳Remaining
→DP Problem 4
↳Remaining
MINUS(s(s(x'')), s(s(s(x0)))) -> MINUS(s(p(s(x''))), s(s(p(s(x0)))))
MINUS(s(s(s(x0))), s(s(x'))) -> MINUS(s(s(p(s(x0)))), s(p(s(x'))))
MINUS(s(s(s(s(x'')))), s(y)) -> MINUS(s(s(s(p(s(x''))))), p(s(y)))
MINUS(s(x), s(s(s(x''')))) -> MINUS(p(s(x)), s(s(p(s(x''')))))
MINUS(s(s(x''')), s(s(x''))) -> MINUS(s(p(s(x'''))), s(p(s(x''))))
MINUS(s(s(s(x'))), s(s(x''))) -> MINUS(s(s(p(s(x')))), s(p(s(x''))))
minus(x, 0) -> x
minus(0, y) -> 0
minus(s(x), s(y)) -> minus(p(s(x)), p(s(y)))
minus(x, plus(y, z)) -> minus(minus(x, y), z)
p(s(s(x))) -> s(p(s(x)))
p(0) -> s(s(0))
div(s(x), s(y)) -> s(div(minus(x, y), s(y)))
div(plus(x, y), z) -> plus(div(x, z), div(y, z))
plus(0, y) -> y
plus(s(x), y) -> s(plus(y, minus(s(x), s(0))))
two new Dependency Pairs are created:
MINUS(s(s(x''')), s(s(x''))) -> MINUS(s(p(s(x'''))), s(p(s(x''))))
MINUS(s(s(s(x'))), s(s(x''))) -> MINUS(s(s(p(s(x')))), s(p(s(x''))))
MINUS(s(s(x''')), s(s(s(x')))) -> MINUS(s(p(s(x'''))), s(s(p(s(x')))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 6
↳Nar
...
→DP Problem 12
↳Narrowing Transformation
→DP Problem 3
↳Remaining
→DP Problem 4
↳Remaining
MINUS(s(s(x''')), s(s(s(x')))) -> MINUS(s(p(s(x'''))), s(s(p(s(x')))))
MINUS(s(s(s(x'))), s(s(x''))) -> MINUS(s(s(p(s(x')))), s(p(s(x''))))
MINUS(s(s(s(x0))), s(s(x'))) -> MINUS(s(s(p(s(x0)))), s(p(s(x'))))
MINUS(s(s(s(x'))), s(s(x''))) -> MINUS(s(s(p(s(x')))), s(p(s(x''))))
MINUS(s(s(s(s(x'')))), s(y)) -> MINUS(s(s(s(p(s(x''))))), p(s(y)))
MINUS(s(x), s(s(s(x''')))) -> MINUS(p(s(x)), s(s(p(s(x''')))))
MINUS(s(s(x'')), s(s(s(x0)))) -> MINUS(s(p(s(x''))), s(s(p(s(x0)))))
minus(x, 0) -> x
minus(0, y) -> 0
minus(s(x), s(y)) -> minus(p(s(x)), p(s(y)))
minus(x, plus(y, z)) -> minus(minus(x, y), z)
p(s(s(x))) -> s(p(s(x)))
p(0) -> s(s(0))
div(s(x), s(y)) -> s(div(minus(x, y), s(y)))
div(plus(x, y), z) -> plus(div(x, z), div(y, z))
plus(0, y) -> y
plus(s(x), y) -> s(plus(y, minus(s(x), s(0))))
two new Dependency Pairs are created:
MINUS(s(x), s(s(s(x''')))) -> MINUS(p(s(x)), s(s(p(s(x''')))))
MINUS(s(s(x'')), s(s(s(x''')))) -> MINUS(s(p(s(x''))), s(s(p(s(x''')))))
MINUS(s(x), s(s(s(s(x''))))) -> MINUS(p(s(x)), s(s(s(p(s(x''))))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 6
↳Nar
...
→DP Problem 13
↳Narrowing Transformation
→DP Problem 3
↳Remaining
→DP Problem 4
↳Remaining
MINUS(s(x), s(s(s(s(x''))))) -> MINUS(p(s(x)), s(s(s(p(s(x''))))))
MINUS(s(s(x'')), s(s(s(x''')))) -> MINUS(s(p(s(x''))), s(s(p(s(x''')))))
MINUS(s(s(s(x'))), s(s(x''))) -> MINUS(s(s(p(s(x')))), s(p(s(x''))))
MINUS(s(s(x'')), s(s(s(x0)))) -> MINUS(s(p(s(x''))), s(s(p(s(x0)))))
MINUS(s(s(s(x0))), s(s(x'))) -> MINUS(s(s(p(s(x0)))), s(p(s(x'))))
MINUS(s(s(s(x'))), s(s(x''))) -> MINUS(s(s(p(s(x')))), s(p(s(x''))))
MINUS(s(s(s(s(x'')))), s(y)) -> MINUS(s(s(s(p(s(x''))))), p(s(y)))
MINUS(s(s(x''')), s(s(s(x')))) -> MINUS(s(p(s(x'''))), s(s(p(s(x')))))
minus(x, 0) -> x
minus(0, y) -> 0
minus(s(x), s(y)) -> minus(p(s(x)), p(s(y)))
minus(x, plus(y, z)) -> minus(minus(x, y), z)
p(s(s(x))) -> s(p(s(x)))
p(0) -> s(s(0))
div(s(x), s(y)) -> s(div(minus(x, y), s(y)))
div(plus(x, y), z) -> plus(div(x, z), div(y, z))
plus(0, y) -> y
plus(s(x), y) -> s(plus(y, minus(s(x), s(0))))
two new Dependency Pairs are created:
MINUS(s(s(s(s(x'')))), s(y)) -> MINUS(s(s(s(p(s(x''))))), p(s(y)))
MINUS(s(s(s(s(s(x'))))), s(y)) -> MINUS(s(s(s(s(p(s(x')))))), p(s(y)))
MINUS(s(s(s(s(x'')))), s(s(x'))) -> MINUS(s(s(s(p(s(x''))))), s(p(s(x'))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 6
↳Nar
...
→DP Problem 14
↳Narrowing Transformation
→DP Problem 3
↳Remaining
→DP Problem 4
↳Remaining
MINUS(s(s(s(s(x'')))), s(s(x'))) -> MINUS(s(s(s(p(s(x''))))), s(p(s(x'))))
MINUS(s(s(s(s(s(x'))))), s(y)) -> MINUS(s(s(s(s(p(s(x')))))), p(s(y)))
MINUS(s(s(x'')), s(s(s(x''')))) -> MINUS(s(p(s(x''))), s(s(p(s(x''')))))
MINUS(s(s(x''')), s(s(s(x')))) -> MINUS(s(p(s(x'''))), s(s(p(s(x')))))
MINUS(s(s(s(x'))), s(s(x''))) -> MINUS(s(s(p(s(x')))), s(p(s(x''))))
MINUS(s(s(x'')), s(s(s(x0)))) -> MINUS(s(p(s(x''))), s(s(p(s(x0)))))
MINUS(s(s(s(x0))), s(s(x'))) -> MINUS(s(s(p(s(x0)))), s(p(s(x'))))
MINUS(s(s(s(x'))), s(s(x''))) -> MINUS(s(s(p(s(x')))), s(p(s(x''))))
MINUS(s(x), s(s(s(s(x''))))) -> MINUS(p(s(x)), s(s(s(p(s(x''))))))
minus(x, 0) -> x
minus(0, y) -> 0
minus(s(x), s(y)) -> minus(p(s(x)), p(s(y)))
minus(x, plus(y, z)) -> minus(minus(x, y), z)
p(s(s(x))) -> s(p(s(x)))
p(0) -> s(s(0))
div(s(x), s(y)) -> s(div(minus(x, y), s(y)))
div(plus(x, y), z) -> plus(div(x, z), div(y, z))
plus(0, y) -> y
plus(s(x), y) -> s(plus(y, minus(s(x), s(0))))
two new Dependency Pairs are created:
MINUS(s(s(s(x'))), s(s(x''))) -> MINUS(s(s(p(s(x')))), s(p(s(x''))))
MINUS(s(s(s(s(x0)))), s(s(x''))) -> MINUS(s(s(s(p(s(x0))))), s(p(s(x''))))
MINUS(s(s(s(x'))), s(s(s(x0)))) -> MINUS(s(s(p(s(x')))), s(s(p(s(x0)))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 6
↳Nar
...
→DP Problem 15
↳Narrowing Transformation
→DP Problem 3
↳Remaining
→DP Problem 4
↳Remaining
MINUS(s(s(s(x'))), s(s(s(x0)))) -> MINUS(s(s(p(s(x')))), s(s(p(s(x0)))))
MINUS(s(s(s(s(x0)))), s(s(x''))) -> MINUS(s(s(s(p(s(x0))))), s(p(s(x''))))
MINUS(s(s(s(s(s(x'))))), s(y)) -> MINUS(s(s(s(s(p(s(x')))))), p(s(y)))
MINUS(s(x), s(s(s(s(x''))))) -> MINUS(p(s(x)), s(s(s(p(s(x''))))))
MINUS(s(s(x'')), s(s(s(x''')))) -> MINUS(s(p(s(x''))), s(s(p(s(x''')))))
MINUS(s(s(x''')), s(s(s(x')))) -> MINUS(s(p(s(x'''))), s(s(p(s(x')))))
MINUS(s(s(s(x'))), s(s(x''))) -> MINUS(s(s(p(s(x')))), s(p(s(x''))))
MINUS(s(s(x'')), s(s(s(x0)))) -> MINUS(s(p(s(x''))), s(s(p(s(x0)))))
MINUS(s(s(s(x0))), s(s(x'))) -> MINUS(s(s(p(s(x0)))), s(p(s(x'))))
MINUS(s(s(s(s(x'')))), s(s(x'))) -> MINUS(s(s(s(p(s(x''))))), s(p(s(x'))))
minus(x, 0) -> x
minus(0, y) -> 0
minus(s(x), s(y)) -> minus(p(s(x)), p(s(y)))
minus(x, plus(y, z)) -> minus(minus(x, y), z)
p(s(s(x))) -> s(p(s(x)))
p(0) -> s(s(0))
div(s(x), s(y)) -> s(div(minus(x, y), s(y)))
div(plus(x, y), z) -> plus(div(x, z), div(y, z))
plus(0, y) -> y
plus(s(x), y) -> s(plus(y, minus(s(x), s(0))))
two new Dependency Pairs are created:
MINUS(s(s(s(x0))), s(s(x'))) -> MINUS(s(s(p(s(x0)))), s(p(s(x'))))
MINUS(s(s(s(s(x'')))), s(s(x'))) -> MINUS(s(s(s(p(s(x''))))), s(p(s(x'))))
MINUS(s(s(s(x0))), s(s(s(x'')))) -> MINUS(s(s(p(s(x0)))), s(s(p(s(x'')))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 6
↳Nar
...
→DP Problem 16
↳Narrowing Transformation
→DP Problem 3
↳Remaining
→DP Problem 4
↳Remaining
MINUS(s(s(s(x0))), s(s(s(x'')))) -> MINUS(s(s(p(s(x0)))), s(s(p(s(x'')))))
MINUS(s(s(s(s(x'')))), s(s(x'))) -> MINUS(s(s(s(p(s(x''))))), s(p(s(x'))))
MINUS(s(s(s(s(x0)))), s(s(x''))) -> MINUS(s(s(s(p(s(x0))))), s(p(s(x''))))
MINUS(s(s(s(s(x'')))), s(s(x'))) -> MINUS(s(s(s(p(s(x''))))), s(p(s(x'))))
MINUS(s(s(s(s(s(x'))))), s(y)) -> MINUS(s(s(s(s(p(s(x')))))), p(s(y)))
MINUS(s(x), s(s(s(s(x''))))) -> MINUS(p(s(x)), s(s(s(p(s(x''))))))
MINUS(s(s(x'')), s(s(s(x''')))) -> MINUS(s(p(s(x''))), s(s(p(s(x''')))))
MINUS(s(s(x''')), s(s(s(x')))) -> MINUS(s(p(s(x'''))), s(s(p(s(x')))))
MINUS(s(s(s(x'))), s(s(x''))) -> MINUS(s(s(p(s(x')))), s(p(s(x''))))
MINUS(s(s(x'')), s(s(s(x0)))) -> MINUS(s(p(s(x''))), s(s(p(s(x0)))))
MINUS(s(s(s(x'))), s(s(s(x0)))) -> MINUS(s(s(p(s(x')))), s(s(p(s(x0)))))
minus(x, 0) -> x
minus(0, y) -> 0
minus(s(x), s(y)) -> minus(p(s(x)), p(s(y)))
minus(x, plus(y, z)) -> minus(minus(x, y), z)
p(s(s(x))) -> s(p(s(x)))
p(0) -> s(s(0))
div(s(x), s(y)) -> s(div(minus(x, y), s(y)))
div(plus(x, y), z) -> plus(div(x, z), div(y, z))
plus(0, y) -> y
plus(s(x), y) -> s(plus(y, minus(s(x), s(0))))
two new Dependency Pairs are created:
MINUS(s(s(x'')), s(s(s(x0)))) -> MINUS(s(p(s(x''))), s(s(p(s(x0)))))
MINUS(s(s(s(x'))), s(s(s(x0)))) -> MINUS(s(s(p(s(x')))), s(s(p(s(x0)))))
MINUS(s(s(x'')), s(s(s(s(x'))))) -> MINUS(s(p(s(x''))), s(s(s(p(s(x'))))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 6
↳Nar
...
→DP Problem 17
↳Narrowing Transformation
→DP Problem 3
↳Remaining
→DP Problem 4
↳Remaining
MINUS(s(s(x'')), s(s(s(s(x'))))) -> MINUS(s(p(s(x''))), s(s(s(p(s(x'))))))
MINUS(s(s(s(x'))), s(s(s(x0)))) -> MINUS(s(s(p(s(x')))), s(s(p(s(x0)))))
MINUS(s(s(s(s(x'')))), s(s(x'))) -> MINUS(s(s(s(p(s(x''))))), s(p(s(x'))))
MINUS(s(s(s(x'))), s(s(s(x0)))) -> MINUS(s(s(p(s(x')))), s(s(p(s(x0)))))
MINUS(s(s(s(s(x0)))), s(s(x''))) -> MINUS(s(s(s(p(s(x0))))), s(p(s(x''))))
MINUS(s(s(s(s(x'')))), s(s(x'))) -> MINUS(s(s(s(p(s(x''))))), s(p(s(x'))))
MINUS(s(s(s(s(s(x'))))), s(y)) -> MINUS(s(s(s(s(p(s(x')))))), p(s(y)))
MINUS(s(x), s(s(s(s(x''))))) -> MINUS(p(s(x)), s(s(s(p(s(x''))))))
MINUS(s(s(x'')), s(s(s(x''')))) -> MINUS(s(p(s(x''))), s(s(p(s(x''')))))
MINUS(s(s(x''')), s(s(s(x')))) -> MINUS(s(p(s(x'''))), s(s(p(s(x')))))
MINUS(s(s(s(x'))), s(s(x''))) -> MINUS(s(s(p(s(x')))), s(p(s(x''))))
MINUS(s(s(s(x0))), s(s(s(x'')))) -> MINUS(s(s(p(s(x0)))), s(s(p(s(x'')))))
minus(x, 0) -> x
minus(0, y) -> 0
minus(s(x), s(y)) -> minus(p(s(x)), p(s(y)))
minus(x, plus(y, z)) -> minus(minus(x, y), z)
p(s(s(x))) -> s(p(s(x)))
p(0) -> s(s(0))
div(s(x), s(y)) -> s(div(minus(x, y), s(y)))
div(plus(x, y), z) -> plus(div(x, z), div(y, z))
plus(0, y) -> y
plus(s(x), y) -> s(plus(y, minus(s(x), s(0))))
two new Dependency Pairs are created:
MINUS(s(s(s(x'))), s(s(x''))) -> MINUS(s(s(p(s(x')))), s(p(s(x''))))
MINUS(s(s(s(s(x0)))), s(s(x''))) -> MINUS(s(s(s(p(s(x0))))), s(p(s(x''))))
MINUS(s(s(s(x'))), s(s(s(x0)))) -> MINUS(s(s(p(s(x')))), s(s(p(s(x0)))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 6
↳Nar
...
→DP Problem 18
↳Narrowing Transformation
→DP Problem 3
↳Remaining
→DP Problem 4
↳Remaining
MINUS(s(s(s(x'))), s(s(s(x0)))) -> MINUS(s(s(p(s(x')))), s(s(p(s(x0)))))
MINUS(s(s(s(s(x0)))), s(s(x''))) -> MINUS(s(s(s(p(s(x0))))), s(p(s(x''))))
MINUS(s(s(s(x'))), s(s(s(x0)))) -> MINUS(s(s(p(s(x')))), s(s(p(s(x0)))))
MINUS(s(s(s(x0))), s(s(s(x'')))) -> MINUS(s(s(p(s(x0)))), s(s(p(s(x'')))))
MINUS(s(s(s(s(x'')))), s(s(x'))) -> MINUS(s(s(s(p(s(x''))))), s(p(s(x'))))
MINUS(s(s(s(x'))), s(s(s(x0)))) -> MINUS(s(s(p(s(x')))), s(s(p(s(x0)))))
MINUS(s(s(s(s(x0)))), s(s(x''))) -> MINUS(s(s(s(p(s(x0))))), s(p(s(x''))))
MINUS(s(s(s(s(x'')))), s(s(x'))) -> MINUS(s(s(s(p(s(x''))))), s(p(s(x'))))
MINUS(s(s(s(s(s(x'))))), s(y)) -> MINUS(s(s(s(s(p(s(x')))))), p(s(y)))
MINUS(s(x), s(s(s(s(x''))))) -> MINUS(p(s(x)), s(s(s(p(s(x''))))))
MINUS(s(s(x'')), s(s(s(x''')))) -> MINUS(s(p(s(x''))), s(s(p(s(x''')))))
MINUS(s(s(x''')), s(s(s(x')))) -> MINUS(s(p(s(x'''))), s(s(p(s(x')))))
MINUS(s(s(x'')), s(s(s(s(x'))))) -> MINUS(s(p(s(x''))), s(s(s(p(s(x'))))))
minus(x, 0) -> x
minus(0, y) -> 0
minus(s(x), s(y)) -> minus(p(s(x)), p(s(y)))
minus(x, plus(y, z)) -> minus(minus(x, y), z)
p(s(s(x))) -> s(p(s(x)))
p(0) -> s(s(0))
div(s(x), s(y)) -> s(div(minus(x, y), s(y)))
div(plus(x, y), z) -> plus(div(x, z), div(y, z))
plus(0, y) -> y
plus(s(x), y) -> s(plus(y, minus(s(x), s(0))))
two new Dependency Pairs are created:
MINUS(s(s(x''')), s(s(s(x')))) -> MINUS(s(p(s(x'''))), s(s(p(s(x')))))
MINUS(s(s(s(x''))), s(s(s(x')))) -> MINUS(s(s(p(s(x'')))), s(s(p(s(x')))))
MINUS(s(s(x''')), s(s(s(s(x''))))) -> MINUS(s(p(s(x'''))), s(s(s(p(s(x''))))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 6
↳Nar
...
→DP Problem 19
↳Narrowing Transformation
→DP Problem 3
↳Remaining
→DP Problem 4
↳Remaining
MINUS(s(s(x''')), s(s(s(s(x''))))) -> MINUS(s(p(s(x'''))), s(s(s(p(s(x''))))))
MINUS(s(s(s(x''))), s(s(s(x')))) -> MINUS(s(s(p(s(x'')))), s(s(p(s(x')))))
MINUS(s(s(s(s(x0)))), s(s(x''))) -> MINUS(s(s(s(p(s(x0))))), s(p(s(x''))))
MINUS(s(s(x'')), s(s(s(s(x'))))) -> MINUS(s(p(s(x''))), s(s(s(p(s(x'))))))
MINUS(s(s(s(x'))), s(s(s(x0)))) -> MINUS(s(s(p(s(x')))), s(s(p(s(x0)))))
MINUS(s(s(s(x0))), s(s(s(x'')))) -> MINUS(s(s(p(s(x0)))), s(s(p(s(x'')))))
MINUS(s(s(s(s(x'')))), s(s(x'))) -> MINUS(s(s(s(p(s(x''))))), s(p(s(x'))))
MINUS(s(s(s(x'))), s(s(s(x0)))) -> MINUS(s(s(p(s(x')))), s(s(p(s(x0)))))
MINUS(s(s(s(s(x0)))), s(s(x''))) -> MINUS(s(s(s(p(s(x0))))), s(p(s(x''))))
MINUS(s(s(s(s(x'')))), s(s(x'))) -> MINUS(s(s(s(p(s(x''))))), s(p(s(x'))))
MINUS(s(s(s(s(s(x'))))), s(y)) -> MINUS(s(s(s(s(p(s(x')))))), p(s(y)))
MINUS(s(x), s(s(s(s(x''))))) -> MINUS(p(s(x)), s(s(s(p(s(x''))))))
MINUS(s(s(x'')), s(s(s(x''')))) -> MINUS(s(p(s(x''))), s(s(p(s(x''')))))
MINUS(s(s(s(x'))), s(s(s(x0)))) -> MINUS(s(s(p(s(x')))), s(s(p(s(x0)))))
minus(x, 0) -> x
minus(0, y) -> 0
minus(s(x), s(y)) -> minus(p(s(x)), p(s(y)))
minus(x, plus(y, z)) -> minus(minus(x, y), z)
p(s(s(x))) -> s(p(s(x)))
p(0) -> s(s(0))
div(s(x), s(y)) -> s(div(minus(x, y), s(y)))
div(plus(x, y), z) -> plus(div(x, z), div(y, z))
plus(0, y) -> y
plus(s(x), y) -> s(plus(y, minus(s(x), s(0))))
two new Dependency Pairs are created:
MINUS(s(s(x'')), s(s(s(x''')))) -> MINUS(s(p(s(x''))), s(s(p(s(x''')))))
MINUS(s(s(s(x'))), s(s(s(x''')))) -> MINUS(s(s(p(s(x')))), s(s(p(s(x''')))))
MINUS(s(s(x'')), s(s(s(s(x'))))) -> MINUS(s(p(s(x''))), s(s(s(p(s(x'))))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 6
↳Nar
...
→DP Problem 20
↳Narrowing Transformation
→DP Problem 3
↳Remaining
→DP Problem 4
↳Remaining
MINUS(s(s(x'')), s(s(s(s(x'))))) -> MINUS(s(p(s(x''))), s(s(s(p(s(x'))))))
MINUS(s(s(s(x'))), s(s(s(x''')))) -> MINUS(s(s(p(s(x')))), s(s(p(s(x''')))))
MINUS(s(s(s(x''))), s(s(s(x')))) -> MINUS(s(s(p(s(x'')))), s(s(p(s(x')))))
MINUS(s(s(s(x'))), s(s(s(x0)))) -> MINUS(s(s(p(s(x')))), s(s(p(s(x0)))))
MINUS(s(s(s(s(x0)))), s(s(x''))) -> MINUS(s(s(s(p(s(x0))))), s(p(s(x''))))
MINUS(s(s(x'')), s(s(s(s(x'))))) -> MINUS(s(p(s(x''))), s(s(s(p(s(x'))))))
MINUS(s(s(s(x'))), s(s(s(x0)))) -> MINUS(s(s(p(s(x')))), s(s(p(s(x0)))))
MINUS(s(s(s(x0))), s(s(s(x'')))) -> MINUS(s(s(p(s(x0)))), s(s(p(s(x'')))))
MINUS(s(s(s(s(x'')))), s(s(x'))) -> MINUS(s(s(s(p(s(x''))))), s(p(s(x'))))
MINUS(s(s(s(x'))), s(s(s(x0)))) -> MINUS(s(s(p(s(x')))), s(s(p(s(x0)))))
MINUS(s(s(s(s(x0)))), s(s(x''))) -> MINUS(s(s(s(p(s(x0))))), s(p(s(x''))))
MINUS(s(s(s(s(x'')))), s(s(x'))) -> MINUS(s(s(s(p(s(x''))))), s(p(s(x'))))
MINUS(s(s(s(s(s(x'))))), s(y)) -> MINUS(s(s(s(s(p(s(x')))))), p(s(y)))
MINUS(s(x), s(s(s(s(x''))))) -> MINUS(p(s(x)), s(s(s(p(s(x''))))))
MINUS(s(s(x''')), s(s(s(s(x''))))) -> MINUS(s(p(s(x'''))), s(s(s(p(s(x''))))))
minus(x, 0) -> x
minus(0, y) -> 0
minus(s(x), s(y)) -> minus(p(s(x)), p(s(y)))
minus(x, plus(y, z)) -> minus(minus(x, y), z)
p(s(s(x))) -> s(p(s(x)))
p(0) -> s(s(0))
div(s(x), s(y)) -> s(div(minus(x, y), s(y)))
div(plus(x, y), z) -> plus(div(x, z), div(y, z))
plus(0, y) -> y
plus(s(x), y) -> s(plus(y, minus(s(x), s(0))))
two new Dependency Pairs are created:
MINUS(s(x), s(s(s(s(x''))))) -> MINUS(p(s(x)), s(s(s(p(s(x''))))))
MINUS(s(s(x''')), s(s(s(s(x''))))) -> MINUS(s(p(s(x'''))), s(s(s(p(s(x''))))))
MINUS(s(x), s(s(s(s(s(x''')))))) -> MINUS(p(s(x)), s(s(s(s(p(s(x''')))))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 6
↳Nar
...
→DP Problem 21
↳Narrowing Transformation
→DP Problem 3
↳Remaining
→DP Problem 4
↳Remaining
MINUS(s(x), s(s(s(s(s(x''')))))) -> MINUS(p(s(x)), s(s(s(s(p(s(x''')))))))
MINUS(s(s(x''')), s(s(s(s(x''))))) -> MINUS(s(p(s(x'''))), s(s(s(p(s(x''))))))
MINUS(s(s(s(x'))), s(s(s(x''')))) -> MINUS(s(s(p(s(x')))), s(s(p(s(x''')))))
MINUS(s(s(x''')), s(s(s(s(x''))))) -> MINUS(s(p(s(x'''))), s(s(s(p(s(x''))))))
MINUS(s(s(s(x''))), s(s(s(x')))) -> MINUS(s(s(p(s(x'')))), s(s(p(s(x')))))
MINUS(s(s(s(x'))), s(s(s(x0)))) -> MINUS(s(s(p(s(x')))), s(s(p(s(x0)))))
MINUS(s(s(s(s(x0)))), s(s(x''))) -> MINUS(s(s(s(p(s(x0))))), s(p(s(x''))))
MINUS(s(s(x'')), s(s(s(s(x'))))) -> MINUS(s(p(s(x''))), s(s(s(p(s(x'))))))
MINUS(s(s(s(x'))), s(s(s(x0)))) -> MINUS(s(s(p(s(x')))), s(s(p(s(x0)))))
MINUS(s(s(s(x0))), s(s(s(x'')))) -> MINUS(s(s(p(s(x0)))), s(s(p(s(x'')))))
MINUS(s(s(s(s(x'')))), s(s(x'))) -> MINUS(s(s(s(p(s(x''))))), s(p(s(x'))))
MINUS(s(s(s(x'))), s(s(s(x0)))) -> MINUS(s(s(p(s(x')))), s(s(p(s(x0)))))
MINUS(s(s(s(s(x0)))), s(s(x''))) -> MINUS(s(s(s(p(s(x0))))), s(p(s(x''))))
MINUS(s(s(s(s(x'')))), s(s(x'))) -> MINUS(s(s(s(p(s(x''))))), s(p(s(x'))))
MINUS(s(s(s(s(s(x'))))), s(y)) -> MINUS(s(s(s(s(p(s(x')))))), p(s(y)))
MINUS(s(s(x'')), s(s(s(s(x'))))) -> MINUS(s(p(s(x''))), s(s(s(p(s(x'))))))
minus(x, 0) -> x
minus(0, y) -> 0
minus(s(x), s(y)) -> minus(p(s(x)), p(s(y)))
minus(x, plus(y, z)) -> minus(minus(x, y), z)
p(s(s(x))) -> s(p(s(x)))
p(0) -> s(s(0))
div(s(x), s(y)) -> s(div(minus(x, y), s(y)))
div(plus(x, y), z) -> plus(div(x, z), div(y, z))
plus(0, y) -> y
plus(s(x), y) -> s(plus(y, minus(s(x), s(0))))
two new Dependency Pairs are created:
MINUS(s(s(s(s(s(x'))))), s(y)) -> MINUS(s(s(s(s(p(s(x')))))), p(s(y)))
MINUS(s(s(s(s(s(s(x'')))))), s(y)) -> MINUS(s(s(s(s(s(p(s(x''))))))), p(s(y)))
MINUS(s(s(s(s(s(x'))))), s(s(x''))) -> MINUS(s(s(s(s(p(s(x')))))), s(p(s(x''))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 6
↳Nar
...
→DP Problem 22
↳Narrowing Transformation
→DP Problem 3
↳Remaining
→DP Problem 4
↳Remaining
MINUS(s(s(s(s(s(x'))))), s(s(x''))) -> MINUS(s(s(s(s(p(s(x')))))), s(p(s(x''))))
MINUS(s(s(s(s(s(s(x'')))))), s(y)) -> MINUS(s(s(s(s(s(p(s(x''))))))), p(s(y)))
MINUS(s(s(x''')), s(s(s(s(x''))))) -> MINUS(s(p(s(x'''))), s(s(s(p(s(x''))))))
MINUS(s(s(x'')), s(s(s(s(x'))))) -> MINUS(s(p(s(x''))), s(s(s(p(s(x'))))))
MINUS(s(s(s(x'))), s(s(s(x''')))) -> MINUS(s(s(p(s(x')))), s(s(p(s(x''')))))
MINUS(s(s(x''')), s(s(s(s(x''))))) -> MINUS(s(p(s(x'''))), s(s(s(p(s(x''))))))
MINUS(s(s(s(x''))), s(s(s(x')))) -> MINUS(s(s(p(s(x'')))), s(s(p(s(x')))))
MINUS(s(s(s(x'))), s(s(s(x0)))) -> MINUS(s(s(p(s(x')))), s(s(p(s(x0)))))
MINUS(s(s(s(s(x0)))), s(s(x''))) -> MINUS(s(s(s(p(s(x0))))), s(p(s(x''))))
MINUS(s(s(x'')), s(s(s(s(x'))))) -> MINUS(s(p(s(x''))), s(s(s(p(s(x'))))))
MINUS(s(s(s(x'))), s(s(s(x0)))) -> MINUS(s(s(p(s(x')))), s(s(p(s(x0)))))
MINUS(s(s(s(x0))), s(s(s(x'')))) -> MINUS(s(s(p(s(x0)))), s(s(p(s(x'')))))
MINUS(s(s(s(s(x'')))), s(s(x'))) -> MINUS(s(s(s(p(s(x''))))), s(p(s(x'))))
MINUS(s(s(s(x'))), s(s(s(x0)))) -> MINUS(s(s(p(s(x')))), s(s(p(s(x0)))))
MINUS(s(s(s(s(x0)))), s(s(x''))) -> MINUS(s(s(s(p(s(x0))))), s(p(s(x''))))
MINUS(s(s(s(s(x'')))), s(s(x'))) -> MINUS(s(s(s(p(s(x''))))), s(p(s(x'))))
MINUS(s(x), s(s(s(s(s(x''')))))) -> MINUS(p(s(x)), s(s(s(s(p(s(x''')))))))
minus(x, 0) -> x
minus(0, y) -> 0
minus(s(x), s(y)) -> minus(p(s(x)), p(s(y)))
minus(x, plus(y, z)) -> minus(minus(x, y), z)
p(s(s(x))) -> s(p(s(x)))
p(0) -> s(s(0))
div(s(x), s(y)) -> s(div(minus(x, y), s(y)))
div(plus(x, y), z) -> plus(div(x, z), div(y, z))
plus(0, y) -> y
plus(s(x), y) -> s(plus(y, minus(s(x), s(0))))
two new Dependency Pairs are created:
MINUS(s(s(s(s(x'')))), s(s(x'))) -> MINUS(s(s(s(p(s(x''))))), s(p(s(x'))))
MINUS(s(s(s(s(s(x0))))), s(s(x'))) -> MINUS(s(s(s(s(p(s(x0)))))), s(p(s(x'))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 6
↳Nar
...
→DP Problem 23
↳Narrowing Transformation
→DP Problem 3
↳Remaining
→DP Problem 4
↳Remaining
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(s(s(x0))))), s(s(x'))) -> MINUS(s(s(s(s(p(s(x0)))))), s(p(s(x'))))
MINUS(s(s(s(s(s(s(x'')))))), s(y)) -> MINUS(s(s(s(s(s(p(s(x''))))))), p(s(y)))
MINUS(s(x), s(s(s(s(s(x''')))))) -> MINUS(p(s(x)), s(s(s(s(p(s(x''')))))))
MINUS(s(s(x''')), s(s(s(s(x''))))) -> MINUS(s(p(s(x'''))), s(s(s(p(s(x''))))))
MINUS(s(s(x'')), s(s(s(s(x'))))) -> MINUS(s(p(s(x''))), s(s(s(p(s(x'))))))
MINUS(s(s(s(x'))), s(s(s(x''')))) -> MINUS(s(s(p(s(x')))), s(s(p(s(x''')))))
MINUS(s(s(x''')), s(s(s(s(x''))))) -> MINUS(s(p(s(x'''))), s(s(s(p(s(x''))))))
MINUS(s(s(s(x''))), s(s(s(x')))) -> MINUS(s(s(p(s(x'')))), s(s(p(s(x')))))
MINUS(s(s(s(x'))), s(s(s(x0)))) -> MINUS(s(s(p(s(x')))), s(s(p(s(x0)))))
MINUS(s(s(s(s(x0)))), s(s(x''))) -> MINUS(s(s(s(p(s(x0))))), s(p(s(x''))))
MINUS(s(s(x'')), s(s(s(s(x'))))) -> MINUS(s(p(s(x''))), s(s(s(p(s(x'))))))
MINUS(s(s(s(x'))), s(s(s(x0)))) -> MINUS(s(s(p(s(x')))), s(s(p(s(x0)))))
MINUS(s(s(s(x0))), s(s(s(x'')))) -> MINUS(s(s(p(s(x0)))), s(s(p(s(x'')))))
MINUS(s(s(s(s(x'')))), s(s(x'))) -> MINUS(s(s(s(p(s(x''))))), s(p(s(x'))))
MINUS(s(s(s(x'))), s(s(s(x0)))) -> MINUS(s(s(p(s(x')))), s(s(p(s(x0)))))
MINUS(s(s(s(s(x0)))), s(s(x''))) -> MINUS(s(s(s(p(s(x0))))), s(p(s(x''))))
MINUS(s(s(s(s(s(x'))))), s(s(x''))) -> MINUS(s(s(s(s(p(s(x')))))), s(p(s(x''))))
minus(x, 0) -> x
minus(0, y) -> 0
minus(s(x), s(y)) -> minus(p(s(x)), p(s(y)))
minus(x, plus(y, z)) -> minus(minus(x, y), z)
p(s(s(x))) -> s(p(s(x)))
p(0) -> s(s(0))
div(s(x), s(y)) -> s(div(minus(x, y), s(y)))
div(plus(x, y), z) -> plus(div(x, z), div(y, z))
plus(0, y) -> y
plus(s(x), y) -> s(plus(y, minus(s(x), s(0))))
two new Dependency Pairs are created:
MINUS(s(s(s(s(x0)))), s(s(x''))) -> MINUS(s(s(s(p(s(x0))))), s(p(s(x''))))
MINUS(s(s(s(s(s(x'))))), s(s(x''))) -> MINUS(s(s(s(s(p(s(x')))))), s(p(s(x''))))
MINUS(s(s(s(s(x0)))), s(s(s(x')))) -> MINUS(s(s(s(p(s(x0))))), s(s(p(s(x')))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 6
↳Nar
...
→DP Problem 24
↳Narrowing Transformation
→DP Problem 3
↳Remaining
→DP Problem 4
↳Remaining
MINUS(s(s(s(s(x0)))), s(s(s(x')))) -> MINUS(s(s(s(p(s(x0))))), s(s(p(s(x')))))
MINUS(s(s(s(s(s(x'))))), s(s(x''))) -> MINUS(s(s(s(s(p(s(x')))))), s(p(s(x''))))
MINUS(s(s(s(s(s(x0))))), s(s(x'))) -> MINUS(s(s(s(s(p(s(x0)))))), s(p(s(x'))))
MINUS(s(s(s(s(s(x'))))), s(s(x''))) -> MINUS(s(s(s(s(p(s(x')))))), s(p(s(x''))))
MINUS(s(s(s(s(s(s(x'')))))), s(y)) -> MINUS(s(s(s(s(s(p(s(x''))))))), p(s(y)))
MINUS(s(x), s(s(s(s(s(x''')))))) -> MINUS(p(s(x)), s(s(s(s(p(s(x''')))))))
MINUS(s(s(x''')), s(s(s(s(x''))))) -> MINUS(s(p(s(x'''))), s(s(s(p(s(x''))))))
MINUS(s(s(x'')), s(s(s(s(x'))))) -> MINUS(s(p(s(x''))), s(s(s(p(s(x'))))))
MINUS(s(s(s(x'))), s(s(s(x''')))) -> MINUS(s(s(p(s(x')))), s(s(p(s(x''')))))
MINUS(s(s(x''')), s(s(s(s(x''))))) -> MINUS(s(p(s(x'''))), s(s(s(p(s(x''))))))
MINUS(s(s(s(x''))), s(s(s(x')))) -> MINUS(s(s(p(s(x'')))), s(s(p(s(x')))))
MINUS(s(s(s(x'))), s(s(s(x0)))) -> MINUS(s(s(p(s(x')))), s(s(p(s(x0)))))
MINUS(s(s(s(s(x0)))), s(s(x''))) -> MINUS(s(s(s(p(s(x0))))), s(p(s(x''))))
MINUS(s(s(x'')), s(s(s(s(x'))))) -> MINUS(s(p(s(x''))), s(s(s(p(s(x'))))))
MINUS(s(s(s(x'))), s(s(s(x0)))) -> MINUS(s(s(p(s(x')))), s(s(p(s(x0)))))
MINUS(s(s(s(x0))), s(s(s(x'')))) -> MINUS(s(s(p(s(x0)))), s(s(p(s(x'')))))
MINUS(s(s(s(s(x'')))), s(s(x'))) -> MINUS(s(s(s(p(s(x''))))), s(p(s(x'))))
MINUS(s(s(s(x'))), s(s(s(x0)))) -> MINUS(s(s(p(s(x')))), s(s(p(s(x0)))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
minus(x, 0) -> x
minus(0, y) -> 0
minus(s(x), s(y)) -> minus(p(s(x)), p(s(y)))
minus(x, plus(y, z)) -> minus(minus(x, y), z)
p(s(s(x))) -> s(p(s(x)))
p(0) -> s(s(0))
div(s(x), s(y)) -> s(div(minus(x, y), s(y)))
div(plus(x, y), z) -> plus(div(x, z), div(y, z))
plus(0, y) -> y
plus(s(x), y) -> s(plus(y, minus(s(x), s(0))))
two new Dependency Pairs are created:
MINUS(s(s(s(x'))), s(s(s(x0)))) -> MINUS(s(s(p(s(x')))), s(s(p(s(x0)))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(x'))), s(s(s(s(x''))))) -> MINUS(s(s(p(s(x')))), s(s(s(p(s(x''))))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 6
↳Nar
...
→DP Problem 25
↳Narrowing Transformation
→DP Problem 3
↳Remaining
→DP Problem 4
↳Remaining
MINUS(s(s(s(x'))), s(s(s(s(x''))))) -> MINUS(s(s(p(s(x')))), s(s(s(p(s(x''))))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(s(s(x'))))), s(s(x''))) -> MINUS(s(s(s(s(p(s(x')))))), s(p(s(x''))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(s(s(x0))))), s(s(x'))) -> MINUS(s(s(s(s(p(s(x0)))))), s(p(s(x'))))
MINUS(s(s(s(s(s(x'))))), s(s(x''))) -> MINUS(s(s(s(s(p(s(x')))))), s(p(s(x''))))
MINUS(s(s(s(s(s(s(x'')))))), s(y)) -> MINUS(s(s(s(s(s(p(s(x''))))))), p(s(y)))
MINUS(s(x), s(s(s(s(s(x''')))))) -> MINUS(p(s(x)), s(s(s(s(p(s(x''')))))))
MINUS(s(s(x''')), s(s(s(s(x''))))) -> MINUS(s(p(s(x'''))), s(s(s(p(s(x''))))))
MINUS(s(s(x'')), s(s(s(s(x'))))) -> MINUS(s(p(s(x''))), s(s(s(p(s(x'))))))
MINUS(s(s(s(x'))), s(s(s(x''')))) -> MINUS(s(s(p(s(x')))), s(s(p(s(x''')))))
MINUS(s(s(x''')), s(s(s(s(x''))))) -> MINUS(s(p(s(x'''))), s(s(s(p(s(x''))))))
MINUS(s(s(s(x''))), s(s(s(x')))) -> MINUS(s(s(p(s(x'')))), s(s(p(s(x')))))
MINUS(s(s(s(x'))), s(s(s(x0)))) -> MINUS(s(s(p(s(x')))), s(s(p(s(x0)))))
MINUS(s(s(s(s(x0)))), s(s(x''))) -> MINUS(s(s(s(p(s(x0))))), s(p(s(x''))))
MINUS(s(s(x'')), s(s(s(s(x'))))) -> MINUS(s(p(s(x''))), s(s(s(p(s(x'))))))
MINUS(s(s(s(x'))), s(s(s(x0)))) -> MINUS(s(s(p(s(x')))), s(s(p(s(x0)))))
MINUS(s(s(s(x0))), s(s(s(x'')))) -> MINUS(s(s(p(s(x0)))), s(s(p(s(x'')))))
MINUS(s(s(s(s(x'')))), s(s(x'))) -> MINUS(s(s(s(p(s(x''))))), s(p(s(x'))))
MINUS(s(s(s(s(x0)))), s(s(s(x')))) -> MINUS(s(s(s(p(s(x0))))), s(s(p(s(x')))))
minus(x, 0) -> x
minus(0, y) -> 0
minus(s(x), s(y)) -> minus(p(s(x)), p(s(y)))
minus(x, plus(y, z)) -> minus(minus(x, y), z)
p(s(s(x))) -> s(p(s(x)))
p(0) -> s(s(0))
div(s(x), s(y)) -> s(div(minus(x, y), s(y)))
div(plus(x, y), z) -> plus(div(x, z), div(y, z))
plus(0, y) -> y
plus(s(x), y) -> s(plus(y, minus(s(x), s(0))))
two new Dependency Pairs are created:
MINUS(s(s(s(s(x'')))), s(s(x'))) -> MINUS(s(s(s(p(s(x''))))), s(p(s(x'))))
MINUS(s(s(s(s(s(x0))))), s(s(x'))) -> MINUS(s(s(s(s(p(s(x0)))))), s(p(s(x'))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 6
↳Nar
...
→DP Problem 26
↳Narrowing Transformation
→DP Problem 3
↳Remaining
→DP Problem 4
↳Remaining
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(s(s(x0))))), s(s(x'))) -> MINUS(s(s(s(s(p(s(x0)))))), s(p(s(x'))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(s(x0)))), s(s(s(x')))) -> MINUS(s(s(s(p(s(x0))))), s(s(p(s(x')))))
MINUS(s(s(s(s(s(x'))))), s(s(x''))) -> MINUS(s(s(s(s(p(s(x')))))), s(p(s(x''))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(s(s(x0))))), s(s(x'))) -> MINUS(s(s(s(s(p(s(x0)))))), s(p(s(x'))))
MINUS(s(s(s(s(s(x'))))), s(s(x''))) -> MINUS(s(s(s(s(p(s(x')))))), s(p(s(x''))))
MINUS(s(s(s(s(s(s(x'')))))), s(y)) -> MINUS(s(s(s(s(s(p(s(x''))))))), p(s(y)))
MINUS(s(x), s(s(s(s(s(x''')))))) -> MINUS(p(s(x)), s(s(s(s(p(s(x''')))))))
MINUS(s(s(x''')), s(s(s(s(x''))))) -> MINUS(s(p(s(x'''))), s(s(s(p(s(x''))))))
MINUS(s(s(x'')), s(s(s(s(x'))))) -> MINUS(s(p(s(x''))), s(s(s(p(s(x'))))))
MINUS(s(s(s(x'))), s(s(s(x''')))) -> MINUS(s(s(p(s(x')))), s(s(p(s(x''')))))
MINUS(s(s(x''')), s(s(s(s(x''))))) -> MINUS(s(p(s(x'''))), s(s(s(p(s(x''))))))
MINUS(s(s(s(x''))), s(s(s(x')))) -> MINUS(s(s(p(s(x'')))), s(s(p(s(x')))))
MINUS(s(s(s(x'))), s(s(s(x0)))) -> MINUS(s(s(p(s(x')))), s(s(p(s(x0)))))
MINUS(s(s(s(s(x0)))), s(s(x''))) -> MINUS(s(s(s(p(s(x0))))), s(p(s(x''))))
MINUS(s(s(x'')), s(s(s(s(x'))))) -> MINUS(s(p(s(x''))), s(s(s(p(s(x'))))))
MINUS(s(s(s(x'))), s(s(s(x0)))) -> MINUS(s(s(p(s(x')))), s(s(p(s(x0)))))
MINUS(s(s(s(x0))), s(s(s(x'')))) -> MINUS(s(s(p(s(x0)))), s(s(p(s(x'')))))
MINUS(s(s(s(x'))), s(s(s(s(x''))))) -> MINUS(s(s(p(s(x')))), s(s(s(p(s(x''))))))
minus(x, 0) -> x
minus(0, y) -> 0
minus(s(x), s(y)) -> minus(p(s(x)), p(s(y)))
minus(x, plus(y, z)) -> minus(minus(x, y), z)
p(s(s(x))) -> s(p(s(x)))
p(0) -> s(s(0))
div(s(x), s(y)) -> s(div(minus(x, y), s(y)))
div(plus(x, y), z) -> plus(div(x, z), div(y, z))
plus(0, y) -> y
plus(s(x), y) -> s(plus(y, minus(s(x), s(0))))
two new Dependency Pairs are created:
MINUS(s(s(s(x0))), s(s(s(x'')))) -> MINUS(s(s(p(s(x0)))), s(s(p(s(x'')))))
MINUS(s(s(s(s(x')))), s(s(s(x'')))) -> MINUS(s(s(s(p(s(x'))))), s(s(p(s(x'')))))
MINUS(s(s(s(x0))), s(s(s(s(x'))))) -> MINUS(s(s(p(s(x0)))), s(s(s(p(s(x'))))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 6
↳Nar
...
→DP Problem 27
↳Narrowing Transformation
→DP Problem 3
↳Remaining
→DP Problem 4
↳Remaining
MINUS(s(s(s(x0))), s(s(s(s(x'))))) -> MINUS(s(s(p(s(x0)))), s(s(s(p(s(x'))))))
MINUS(s(s(s(s(x')))), s(s(s(x'')))) -> MINUS(s(s(s(p(s(x'))))), s(s(p(s(x'')))))
MINUS(s(s(s(s(s(x0))))), s(s(x'))) -> MINUS(s(s(s(s(p(s(x0)))))), s(p(s(x'))))
MINUS(s(s(s(x'))), s(s(s(s(x''))))) -> MINUS(s(s(p(s(x')))), s(s(s(p(s(x''))))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(s(x0)))), s(s(s(x')))) -> MINUS(s(s(s(p(s(x0))))), s(s(p(s(x')))))
MINUS(s(s(s(s(s(x'))))), s(s(x''))) -> MINUS(s(s(s(s(p(s(x')))))), s(p(s(x''))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(s(s(x0))))), s(s(x'))) -> MINUS(s(s(s(s(p(s(x0)))))), s(p(s(x'))))
MINUS(s(s(s(s(s(x'))))), s(s(x''))) -> MINUS(s(s(s(s(p(s(x')))))), s(p(s(x''))))
MINUS(s(s(s(s(s(s(x'')))))), s(y)) -> MINUS(s(s(s(s(s(p(s(x''))))))), p(s(y)))
MINUS(s(x), s(s(s(s(s(x''')))))) -> MINUS(p(s(x)), s(s(s(s(p(s(x''')))))))
MINUS(s(s(x''')), s(s(s(s(x''))))) -> MINUS(s(p(s(x'''))), s(s(s(p(s(x''))))))
MINUS(s(s(x'')), s(s(s(s(x'))))) -> MINUS(s(p(s(x''))), s(s(s(p(s(x'))))))
MINUS(s(s(s(x'))), s(s(s(x''')))) -> MINUS(s(s(p(s(x')))), s(s(p(s(x''')))))
MINUS(s(s(x''')), s(s(s(s(x''))))) -> MINUS(s(p(s(x'''))), s(s(s(p(s(x''))))))
MINUS(s(s(s(x''))), s(s(s(x')))) -> MINUS(s(s(p(s(x'')))), s(s(p(s(x')))))
MINUS(s(s(s(x'))), s(s(s(x0)))) -> MINUS(s(s(p(s(x')))), s(s(p(s(x0)))))
MINUS(s(s(s(s(x0)))), s(s(x''))) -> MINUS(s(s(s(p(s(x0))))), s(p(s(x''))))
MINUS(s(s(x'')), s(s(s(s(x'))))) -> MINUS(s(p(s(x''))), s(s(s(p(s(x'))))))
MINUS(s(s(s(x'))), s(s(s(x0)))) -> MINUS(s(s(p(s(x')))), s(s(p(s(x0)))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
minus(x, 0) -> x
minus(0, y) -> 0
minus(s(x), s(y)) -> minus(p(s(x)), p(s(y)))
minus(x, plus(y, z)) -> minus(minus(x, y), z)
p(s(s(x))) -> s(p(s(x)))
p(0) -> s(s(0))
div(s(x), s(y)) -> s(div(minus(x, y), s(y)))
div(plus(x, y), z) -> plus(div(x, z), div(y, z))
plus(0, y) -> y
plus(s(x), y) -> s(plus(y, minus(s(x), s(0))))
two new Dependency Pairs are created:
MINUS(s(s(s(x'))), s(s(s(x0)))) -> MINUS(s(s(p(s(x')))), s(s(p(s(x0)))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(x'))), s(s(s(s(x''))))) -> MINUS(s(s(p(s(x')))), s(s(s(p(s(x''))))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 6
↳Nar
...
→DP Problem 28
↳Narrowing Transformation
→DP Problem 3
↳Remaining
→DP Problem 4
↳Remaining
MINUS(s(s(s(x'))), s(s(s(s(x''))))) -> MINUS(s(s(p(s(x')))), s(s(s(p(s(x''))))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(s(x')))), s(s(s(x'')))) -> MINUS(s(s(s(p(s(x'))))), s(s(p(s(x'')))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(s(s(x0))))), s(s(x'))) -> MINUS(s(s(s(s(p(s(x0)))))), s(p(s(x'))))
MINUS(s(s(s(x'))), s(s(s(s(x''))))) -> MINUS(s(s(p(s(x')))), s(s(s(p(s(x''))))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(s(x0)))), s(s(s(x')))) -> MINUS(s(s(s(p(s(x0))))), s(s(p(s(x')))))
MINUS(s(s(s(s(s(x'))))), s(s(x''))) -> MINUS(s(s(s(s(p(s(x')))))), s(p(s(x''))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(s(s(x0))))), s(s(x'))) -> MINUS(s(s(s(s(p(s(x0)))))), s(p(s(x'))))
MINUS(s(s(s(s(s(x'))))), s(s(x''))) -> MINUS(s(s(s(s(p(s(x')))))), s(p(s(x''))))
MINUS(s(s(s(s(s(s(x'')))))), s(y)) -> MINUS(s(s(s(s(s(p(s(x''))))))), p(s(y)))
MINUS(s(x), s(s(s(s(s(x''')))))) -> MINUS(p(s(x)), s(s(s(s(p(s(x''')))))))
MINUS(s(s(x''')), s(s(s(s(x''))))) -> MINUS(s(p(s(x'''))), s(s(s(p(s(x''))))))
MINUS(s(s(x'')), s(s(s(s(x'))))) -> MINUS(s(p(s(x''))), s(s(s(p(s(x'))))))
MINUS(s(s(s(x'))), s(s(s(x''')))) -> MINUS(s(s(p(s(x')))), s(s(p(s(x''')))))
MINUS(s(s(x''')), s(s(s(s(x''))))) -> MINUS(s(p(s(x'''))), s(s(s(p(s(x''))))))
MINUS(s(s(s(x''))), s(s(s(x')))) -> MINUS(s(s(p(s(x'')))), s(s(p(s(x')))))
MINUS(s(s(s(x'))), s(s(s(x0)))) -> MINUS(s(s(p(s(x')))), s(s(p(s(x0)))))
MINUS(s(s(s(s(x0)))), s(s(x''))) -> MINUS(s(s(s(p(s(x0))))), s(p(s(x''))))
MINUS(s(s(x'')), s(s(s(s(x'))))) -> MINUS(s(p(s(x''))), s(s(s(p(s(x'))))))
MINUS(s(s(s(x0))), s(s(s(s(x'))))) -> MINUS(s(s(p(s(x0)))), s(s(s(p(s(x'))))))
minus(x, 0) -> x
minus(0, y) -> 0
minus(s(x), s(y)) -> minus(p(s(x)), p(s(y)))
minus(x, plus(y, z)) -> minus(minus(x, y), z)
p(s(s(x))) -> s(p(s(x)))
p(0) -> s(s(0))
div(s(x), s(y)) -> s(div(minus(x, y), s(y)))
div(plus(x, y), z) -> plus(div(x, z), div(y, z))
plus(0, y) -> y
plus(s(x), y) -> s(plus(y, minus(s(x), s(0))))
two new Dependency Pairs are created:
MINUS(s(s(x'')), s(s(s(s(x'))))) -> MINUS(s(p(s(x''))), s(s(s(p(s(x'))))))
MINUS(s(s(s(x0))), s(s(s(s(x'))))) -> MINUS(s(s(p(s(x0)))), s(s(s(p(s(x'))))))
MINUS(s(s(x'')), s(s(s(s(s(x0)))))) -> MINUS(s(p(s(x''))), s(s(s(s(p(s(x0)))))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 6
↳Nar
...
→DP Problem 29
↳Narrowing Transformation
→DP Problem 3
↳Remaining
→DP Problem 4
↳Remaining
MINUS(s(s(x'')), s(s(s(s(s(x0)))))) -> MINUS(s(p(s(x''))), s(s(s(s(p(s(x0)))))))
MINUS(s(s(s(x0))), s(s(s(s(x'))))) -> MINUS(s(s(p(s(x0)))), s(s(s(p(s(x'))))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(x0))), s(s(s(s(x'))))) -> MINUS(s(s(p(s(x0)))), s(s(s(p(s(x'))))))
MINUS(s(s(s(s(x')))), s(s(s(x'')))) -> MINUS(s(s(s(p(s(x'))))), s(s(p(s(x'')))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(s(s(x0))))), s(s(x'))) -> MINUS(s(s(s(s(p(s(x0)))))), s(p(s(x'))))
MINUS(s(s(s(x'))), s(s(s(s(x''))))) -> MINUS(s(s(p(s(x')))), s(s(s(p(s(x''))))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(s(x0)))), s(s(s(x')))) -> MINUS(s(s(s(p(s(x0))))), s(s(p(s(x')))))
MINUS(s(s(s(s(s(x'))))), s(s(x''))) -> MINUS(s(s(s(s(p(s(x')))))), s(p(s(x''))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(s(s(x0))))), s(s(x'))) -> MINUS(s(s(s(s(p(s(x0)))))), s(p(s(x'))))
MINUS(s(s(s(s(s(x'))))), s(s(x''))) -> MINUS(s(s(s(s(p(s(x')))))), s(p(s(x''))))
MINUS(s(s(s(s(s(s(x'')))))), s(y)) -> MINUS(s(s(s(s(s(p(s(x''))))))), p(s(y)))
MINUS(s(x), s(s(s(s(s(x''')))))) -> MINUS(p(s(x)), s(s(s(s(p(s(x''')))))))
MINUS(s(s(x''')), s(s(s(s(x''))))) -> MINUS(s(p(s(x'''))), s(s(s(p(s(x''))))))
MINUS(s(s(x'')), s(s(s(s(x'))))) -> MINUS(s(p(s(x''))), s(s(s(p(s(x'))))))
MINUS(s(s(s(x'))), s(s(s(x''')))) -> MINUS(s(s(p(s(x')))), s(s(p(s(x''')))))
MINUS(s(s(x''')), s(s(s(s(x''))))) -> MINUS(s(p(s(x'''))), s(s(s(p(s(x''))))))
MINUS(s(s(s(x''))), s(s(s(x')))) -> MINUS(s(s(p(s(x'')))), s(s(p(s(x')))))
MINUS(s(s(s(x'))), s(s(s(x0)))) -> MINUS(s(s(p(s(x')))), s(s(p(s(x0)))))
MINUS(s(s(s(s(x0)))), s(s(x''))) -> MINUS(s(s(s(p(s(x0))))), s(p(s(x''))))
MINUS(s(s(s(x'))), s(s(s(s(x''))))) -> MINUS(s(s(p(s(x')))), s(s(s(p(s(x''))))))
minus(x, 0) -> x
minus(0, y) -> 0
minus(s(x), s(y)) -> minus(p(s(x)), p(s(y)))
minus(x, plus(y, z)) -> minus(minus(x, y), z)
p(s(s(x))) -> s(p(s(x)))
p(0) -> s(s(0))
div(s(x), s(y)) -> s(div(minus(x, y), s(y)))
div(plus(x, y), z) -> plus(div(x, z), div(y, z))
plus(0, y) -> y
plus(s(x), y) -> s(plus(y, minus(s(x), s(0))))
two new Dependency Pairs are created:
MINUS(s(s(s(s(x0)))), s(s(x''))) -> MINUS(s(s(s(p(s(x0))))), s(p(s(x''))))
MINUS(s(s(s(s(s(x'))))), s(s(x''))) -> MINUS(s(s(s(s(p(s(x')))))), s(p(s(x''))))
MINUS(s(s(s(s(x0)))), s(s(s(x')))) -> MINUS(s(s(s(p(s(x0))))), s(s(p(s(x')))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 6
↳Nar
...
→DP Problem 30
↳Narrowing Transformation
→DP Problem 3
↳Remaining
→DP Problem 4
↳Remaining
MINUS(s(s(s(s(x0)))), s(s(s(x')))) -> MINUS(s(s(s(p(s(x0))))), s(s(p(s(x')))))
MINUS(s(s(s(s(s(x'))))), s(s(x''))) -> MINUS(s(s(s(s(p(s(x')))))), s(p(s(x''))))
MINUS(s(s(s(x0))), s(s(s(s(x'))))) -> MINUS(s(s(p(s(x0)))), s(s(s(p(s(x'))))))
MINUS(s(s(s(x'))), s(s(s(s(x''))))) -> MINUS(s(s(p(s(x')))), s(s(s(p(s(x''))))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(x0))), s(s(s(s(x'))))) -> MINUS(s(s(p(s(x0)))), s(s(s(p(s(x'))))))
MINUS(s(s(s(s(x')))), s(s(s(x'')))) -> MINUS(s(s(s(p(s(x'))))), s(s(p(s(x'')))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(s(s(x0))))), s(s(x'))) -> MINUS(s(s(s(s(p(s(x0)))))), s(p(s(x'))))
MINUS(s(s(s(x'))), s(s(s(s(x''))))) -> MINUS(s(s(p(s(x')))), s(s(s(p(s(x''))))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(s(x0)))), s(s(s(x')))) -> MINUS(s(s(s(p(s(x0))))), s(s(p(s(x')))))
MINUS(s(s(s(s(s(x'))))), s(s(x''))) -> MINUS(s(s(s(s(p(s(x')))))), s(p(s(x''))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(s(s(x0))))), s(s(x'))) -> MINUS(s(s(s(s(p(s(x0)))))), s(p(s(x'))))
MINUS(s(s(s(s(s(x'))))), s(s(x''))) -> MINUS(s(s(s(s(p(s(x')))))), s(p(s(x''))))
MINUS(s(s(s(s(s(s(x'')))))), s(y)) -> MINUS(s(s(s(s(s(p(s(x''))))))), p(s(y)))
MINUS(s(x), s(s(s(s(s(x''')))))) -> MINUS(p(s(x)), s(s(s(s(p(s(x''')))))))
MINUS(s(s(x''')), s(s(s(s(x''))))) -> MINUS(s(p(s(x'''))), s(s(s(p(s(x''))))))
MINUS(s(s(x'')), s(s(s(s(x'))))) -> MINUS(s(p(s(x''))), s(s(s(p(s(x'))))))
MINUS(s(s(s(x'))), s(s(s(x''')))) -> MINUS(s(s(p(s(x')))), s(s(p(s(x''')))))
MINUS(s(s(x''')), s(s(s(s(x''))))) -> MINUS(s(p(s(x'''))), s(s(s(p(s(x''))))))
MINUS(s(s(s(x''))), s(s(s(x')))) -> MINUS(s(s(p(s(x'')))), s(s(p(s(x')))))
MINUS(s(s(s(x'))), s(s(s(x0)))) -> MINUS(s(s(p(s(x')))), s(s(p(s(x0)))))
MINUS(s(s(x'')), s(s(s(s(s(x0)))))) -> MINUS(s(p(s(x''))), s(s(s(s(p(s(x0)))))))
minus(x, 0) -> x
minus(0, y) -> 0
minus(s(x), s(y)) -> minus(p(s(x)), p(s(y)))
minus(x, plus(y, z)) -> minus(minus(x, y), z)
p(s(s(x))) -> s(p(s(x)))
p(0) -> s(s(0))
div(s(x), s(y)) -> s(div(minus(x, y), s(y)))
div(plus(x, y), z) -> plus(div(x, z), div(y, z))
plus(0, y) -> y
plus(s(x), y) -> s(plus(y, minus(s(x), s(0))))
two new Dependency Pairs are created:
MINUS(s(s(s(x'))), s(s(s(x0)))) -> MINUS(s(s(p(s(x')))), s(s(p(s(x0)))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(x'))), s(s(s(s(x''))))) -> MINUS(s(s(p(s(x')))), s(s(s(p(s(x''))))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 6
↳Nar
...
→DP Problem 31
↳Narrowing Transformation
→DP Problem 3
↳Remaining
→DP Problem 4
↳Remaining
MINUS(s(s(s(x'))), s(s(s(s(x''))))) -> MINUS(s(s(p(s(x')))), s(s(s(p(s(x''))))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(s(s(x'))))), s(s(x''))) -> MINUS(s(s(s(s(p(s(x')))))), s(p(s(x''))))
MINUS(s(s(x'')), s(s(s(s(s(x0)))))) -> MINUS(s(p(s(x''))), s(s(s(s(p(s(x0)))))))
MINUS(s(s(s(x0))), s(s(s(s(x'))))) -> MINUS(s(s(p(s(x0)))), s(s(s(p(s(x'))))))
MINUS(s(s(s(x'))), s(s(s(s(x''))))) -> MINUS(s(s(p(s(x')))), s(s(s(p(s(x''))))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(x0))), s(s(s(s(x'))))) -> MINUS(s(s(p(s(x0)))), s(s(s(p(s(x'))))))
MINUS(s(s(s(s(x')))), s(s(s(x'')))) -> MINUS(s(s(s(p(s(x'))))), s(s(p(s(x'')))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(s(s(x0))))), s(s(x'))) -> MINUS(s(s(s(s(p(s(x0)))))), s(p(s(x'))))
MINUS(s(s(s(x'))), s(s(s(s(x''))))) -> MINUS(s(s(p(s(x')))), s(s(s(p(s(x''))))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(s(x0)))), s(s(s(x')))) -> MINUS(s(s(s(p(s(x0))))), s(s(p(s(x')))))
MINUS(s(s(s(s(s(x'))))), s(s(x''))) -> MINUS(s(s(s(s(p(s(x')))))), s(p(s(x''))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(s(s(x0))))), s(s(x'))) -> MINUS(s(s(s(s(p(s(x0)))))), s(p(s(x'))))
MINUS(s(s(s(s(s(x'))))), s(s(x''))) -> MINUS(s(s(s(s(p(s(x')))))), s(p(s(x''))))
MINUS(s(s(s(s(s(s(x'')))))), s(y)) -> MINUS(s(s(s(s(s(p(s(x''))))))), p(s(y)))
MINUS(s(x), s(s(s(s(s(x''')))))) -> MINUS(p(s(x)), s(s(s(s(p(s(x''')))))))
MINUS(s(s(x''')), s(s(s(s(x''))))) -> MINUS(s(p(s(x'''))), s(s(s(p(s(x''))))))
MINUS(s(s(x'')), s(s(s(s(x'))))) -> MINUS(s(p(s(x''))), s(s(s(p(s(x'))))))
MINUS(s(s(s(x'))), s(s(s(x''')))) -> MINUS(s(s(p(s(x')))), s(s(p(s(x''')))))
MINUS(s(s(x''')), s(s(s(s(x''))))) -> MINUS(s(p(s(x'''))), s(s(s(p(s(x''))))))
MINUS(s(s(s(x''))), s(s(s(x')))) -> MINUS(s(s(p(s(x'')))), s(s(p(s(x')))))
MINUS(s(s(s(s(x0)))), s(s(s(x')))) -> MINUS(s(s(s(p(s(x0))))), s(s(p(s(x')))))
minus(x, 0) -> x
minus(0, y) -> 0
minus(s(x), s(y)) -> minus(p(s(x)), p(s(y)))
minus(x, plus(y, z)) -> minus(minus(x, y), z)
p(s(s(x))) -> s(p(s(x)))
p(0) -> s(s(0))
div(s(x), s(y)) -> s(div(minus(x, y), s(y)))
div(plus(x, y), z) -> plus(div(x, z), div(y, z))
plus(0, y) -> y
plus(s(x), y) -> s(plus(y, minus(s(x), s(0))))
two new Dependency Pairs are created:
MINUS(s(s(s(x''))), s(s(s(x')))) -> MINUS(s(s(p(s(x'')))), s(s(p(s(x')))))
MINUS(s(s(s(s(x0)))), s(s(s(x')))) -> MINUS(s(s(s(p(s(x0))))), s(s(p(s(x')))))
MINUS(s(s(s(x''))), s(s(s(s(x0))))) -> MINUS(s(s(p(s(x'')))), s(s(s(p(s(x0))))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 6
↳Nar
...
→DP Problem 32
↳Narrowing Transformation
→DP Problem 3
↳Remaining
→DP Problem 4
↳Remaining
MINUS(s(s(s(x''))), s(s(s(s(x0))))) -> MINUS(s(s(p(s(x'')))), s(s(s(p(s(x0))))))
MINUS(s(s(s(s(x0)))), s(s(s(x')))) -> MINUS(s(s(s(p(s(x0))))), s(s(p(s(x')))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(s(x0)))), s(s(s(x')))) -> MINUS(s(s(s(p(s(x0))))), s(s(p(s(x')))))
MINUS(s(s(s(s(s(x'))))), s(s(x''))) -> MINUS(s(s(s(s(p(s(x')))))), s(p(s(x''))))
MINUS(s(s(x'')), s(s(s(s(s(x0)))))) -> MINUS(s(p(s(x''))), s(s(s(s(p(s(x0)))))))
MINUS(s(s(s(x0))), s(s(s(s(x'))))) -> MINUS(s(s(p(s(x0)))), s(s(s(p(s(x'))))))
MINUS(s(s(s(x'))), s(s(s(s(x''))))) -> MINUS(s(s(p(s(x')))), s(s(s(p(s(x''))))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(x0))), s(s(s(s(x'))))) -> MINUS(s(s(p(s(x0)))), s(s(s(p(s(x'))))))
MINUS(s(s(s(s(x')))), s(s(s(x'')))) -> MINUS(s(s(s(p(s(x'))))), s(s(p(s(x'')))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(s(s(x0))))), s(s(x'))) -> MINUS(s(s(s(s(p(s(x0)))))), s(p(s(x'))))
MINUS(s(s(s(x'))), s(s(s(s(x''))))) -> MINUS(s(s(p(s(x')))), s(s(s(p(s(x''))))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(s(x0)))), s(s(s(x')))) -> MINUS(s(s(s(p(s(x0))))), s(s(p(s(x')))))
MINUS(s(s(s(s(s(x'))))), s(s(x''))) -> MINUS(s(s(s(s(p(s(x')))))), s(p(s(x''))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(s(s(x0))))), s(s(x'))) -> MINUS(s(s(s(s(p(s(x0)))))), s(p(s(x'))))
MINUS(s(s(s(s(s(x'))))), s(s(x''))) -> MINUS(s(s(s(s(p(s(x')))))), s(p(s(x''))))
MINUS(s(s(s(s(s(s(x'')))))), s(y)) -> MINUS(s(s(s(s(s(p(s(x''))))))), p(s(y)))
MINUS(s(x), s(s(s(s(s(x''')))))) -> MINUS(p(s(x)), s(s(s(s(p(s(x''')))))))
MINUS(s(s(x''')), s(s(s(s(x''))))) -> MINUS(s(p(s(x'''))), s(s(s(p(s(x''))))))
MINUS(s(s(x'')), s(s(s(s(x'))))) -> MINUS(s(p(s(x''))), s(s(s(p(s(x'))))))
MINUS(s(s(s(x'))), s(s(s(x''')))) -> MINUS(s(s(p(s(x')))), s(s(p(s(x''')))))
MINUS(s(s(x''')), s(s(s(s(x''))))) -> MINUS(s(p(s(x'''))), s(s(s(p(s(x''))))))
MINUS(s(s(s(x'))), s(s(s(s(x''))))) -> MINUS(s(s(p(s(x')))), s(s(s(p(s(x''))))))
minus(x, 0) -> x
minus(0, y) -> 0
minus(s(x), s(y)) -> minus(p(s(x)), p(s(y)))
minus(x, plus(y, z)) -> minus(minus(x, y), z)
p(s(s(x))) -> s(p(s(x)))
p(0) -> s(s(0))
div(s(x), s(y)) -> s(div(minus(x, y), s(y)))
div(plus(x, y), z) -> plus(div(x, z), div(y, z))
plus(0, y) -> y
plus(s(x), y) -> s(plus(y, minus(s(x), s(0))))
two new Dependency Pairs are created:
MINUS(s(s(x''')), s(s(s(s(x''))))) -> MINUS(s(p(s(x'''))), s(s(s(p(s(x''))))))
MINUS(s(s(s(x'))), s(s(s(s(x''))))) -> MINUS(s(s(p(s(x')))), s(s(s(p(s(x''))))))
MINUS(s(s(x''')), s(s(s(s(s(x')))))) -> MINUS(s(p(s(x'''))), s(s(s(s(p(s(x')))))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 6
↳Nar
...
→DP Problem 33
↳Narrowing Transformation
→DP Problem 3
↳Remaining
→DP Problem 4
↳Remaining
MINUS(s(s(x''')), s(s(s(s(s(x')))))) -> MINUS(s(p(s(x'''))), s(s(s(s(p(s(x')))))))
MINUS(s(s(s(x'))), s(s(s(s(x''))))) -> MINUS(s(s(p(s(x')))), s(s(s(p(s(x''))))))
MINUS(s(s(s(s(x0)))), s(s(s(x')))) -> MINUS(s(s(s(p(s(x0))))), s(s(p(s(x')))))
MINUS(s(s(s(x'))), s(s(s(s(x''))))) -> MINUS(s(s(p(s(x')))), s(s(s(p(s(x''))))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(s(x0)))), s(s(s(x')))) -> MINUS(s(s(s(p(s(x0))))), s(s(p(s(x')))))
MINUS(s(s(s(s(s(x'))))), s(s(x''))) -> MINUS(s(s(s(s(p(s(x')))))), s(p(s(x''))))
MINUS(s(s(x'')), s(s(s(s(s(x0)))))) -> MINUS(s(p(s(x''))), s(s(s(s(p(s(x0)))))))
MINUS(s(s(s(x0))), s(s(s(s(x'))))) -> MINUS(s(s(p(s(x0)))), s(s(s(p(s(x'))))))
MINUS(s(s(s(x'))), s(s(s(s(x''))))) -> MINUS(s(s(p(s(x')))), s(s(s(p(s(x''))))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(x0))), s(s(s(s(x'))))) -> MINUS(s(s(p(s(x0)))), s(s(s(p(s(x'))))))
MINUS(s(s(s(s(x')))), s(s(s(x'')))) -> MINUS(s(s(s(p(s(x'))))), s(s(p(s(x'')))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(s(s(x0))))), s(s(x'))) -> MINUS(s(s(s(s(p(s(x0)))))), s(p(s(x'))))
MINUS(s(s(s(x'))), s(s(s(s(x''))))) -> MINUS(s(s(p(s(x')))), s(s(s(p(s(x''))))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(s(x0)))), s(s(s(x')))) -> MINUS(s(s(s(p(s(x0))))), s(s(p(s(x')))))
MINUS(s(s(s(s(s(x'))))), s(s(x''))) -> MINUS(s(s(s(s(p(s(x')))))), s(p(s(x''))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(s(s(x0))))), s(s(x'))) -> MINUS(s(s(s(s(p(s(x0)))))), s(p(s(x'))))
MINUS(s(s(s(s(s(x'))))), s(s(x''))) -> MINUS(s(s(s(s(p(s(x')))))), s(p(s(x''))))
MINUS(s(s(s(s(s(s(x'')))))), s(y)) -> MINUS(s(s(s(s(s(p(s(x''))))))), p(s(y)))
MINUS(s(x), s(s(s(s(s(x''')))))) -> MINUS(p(s(x)), s(s(s(s(p(s(x''')))))))
MINUS(s(s(x''')), s(s(s(s(x''))))) -> MINUS(s(p(s(x'''))), s(s(s(p(s(x''))))))
MINUS(s(s(x'')), s(s(s(s(x'))))) -> MINUS(s(p(s(x''))), s(s(s(p(s(x'))))))
MINUS(s(s(s(x'))), s(s(s(x''')))) -> MINUS(s(s(p(s(x')))), s(s(p(s(x''')))))
MINUS(s(s(s(x''))), s(s(s(s(x0))))) -> MINUS(s(s(p(s(x'')))), s(s(s(p(s(x0))))))
minus(x, 0) -> x
minus(0, y) -> 0
minus(s(x), s(y)) -> minus(p(s(x)), p(s(y)))
minus(x, plus(y, z)) -> minus(minus(x, y), z)
p(s(s(x))) -> s(p(s(x)))
p(0) -> s(s(0))
div(s(x), s(y)) -> s(div(minus(x, y), s(y)))
div(plus(x, y), z) -> plus(div(x, z), div(y, z))
plus(0, y) -> y
plus(s(x), y) -> s(plus(y, minus(s(x), s(0))))
two new Dependency Pairs are created:
MINUS(s(s(s(x'))), s(s(s(x''')))) -> MINUS(s(s(p(s(x')))), s(s(p(s(x''')))))
MINUS(s(s(s(s(x'')))), s(s(s(x''')))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x''')))))
MINUS(s(s(s(x'))), s(s(s(s(x''))))) -> MINUS(s(s(p(s(x')))), s(s(s(p(s(x''))))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 6
↳Nar
...
→DP Problem 34
↳Narrowing Transformation
→DP Problem 3
↳Remaining
→DP Problem 4
↳Remaining
MINUS(s(s(s(x'))), s(s(s(s(x''))))) -> MINUS(s(s(p(s(x')))), s(s(s(p(s(x''))))))
MINUS(s(s(s(s(x'')))), s(s(s(x''')))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x''')))))
MINUS(s(s(s(x'))), s(s(s(s(x''))))) -> MINUS(s(s(p(s(x')))), s(s(s(p(s(x''))))))
MINUS(s(s(s(x''))), s(s(s(s(x0))))) -> MINUS(s(s(p(s(x'')))), s(s(s(p(s(x0))))))
MINUS(s(s(s(s(x0)))), s(s(s(x')))) -> MINUS(s(s(s(p(s(x0))))), s(s(p(s(x')))))
MINUS(s(s(s(x'))), s(s(s(s(x''))))) -> MINUS(s(s(p(s(x')))), s(s(s(p(s(x''))))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(s(x0)))), s(s(s(x')))) -> MINUS(s(s(s(p(s(x0))))), s(s(p(s(x')))))
MINUS(s(s(s(s(s(x'))))), s(s(x''))) -> MINUS(s(s(s(s(p(s(x')))))), s(p(s(x''))))
MINUS(s(s(x'')), s(s(s(s(s(x0)))))) -> MINUS(s(p(s(x''))), s(s(s(s(p(s(x0)))))))
MINUS(s(s(s(x0))), s(s(s(s(x'))))) -> MINUS(s(s(p(s(x0)))), s(s(s(p(s(x'))))))
MINUS(s(s(s(x'))), s(s(s(s(x''))))) -> MINUS(s(s(p(s(x')))), s(s(s(p(s(x''))))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(x0))), s(s(s(s(x'))))) -> MINUS(s(s(p(s(x0)))), s(s(s(p(s(x'))))))
MINUS(s(s(s(s(x')))), s(s(s(x'')))) -> MINUS(s(s(s(p(s(x'))))), s(s(p(s(x'')))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(s(s(x0))))), s(s(x'))) -> MINUS(s(s(s(s(p(s(x0)))))), s(p(s(x'))))
MINUS(s(s(s(x'))), s(s(s(s(x''))))) -> MINUS(s(s(p(s(x')))), s(s(s(p(s(x''))))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(s(x0)))), s(s(s(x')))) -> MINUS(s(s(s(p(s(x0))))), s(s(p(s(x')))))
MINUS(s(s(s(s(s(x'))))), s(s(x''))) -> MINUS(s(s(s(s(p(s(x')))))), s(p(s(x''))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(s(s(x0))))), s(s(x'))) -> MINUS(s(s(s(s(p(s(x0)))))), s(p(s(x'))))
MINUS(s(s(s(s(s(x'))))), s(s(x''))) -> MINUS(s(s(s(s(p(s(x')))))), s(p(s(x''))))
MINUS(s(s(s(s(s(s(x'')))))), s(y)) -> MINUS(s(s(s(s(s(p(s(x''))))))), p(s(y)))
MINUS(s(x), s(s(s(s(s(x''')))))) -> MINUS(p(s(x)), s(s(s(s(p(s(x''')))))))
MINUS(s(s(x''')), s(s(s(s(x''))))) -> MINUS(s(p(s(x'''))), s(s(s(p(s(x''))))))
MINUS(s(s(x'')), s(s(s(s(x'))))) -> MINUS(s(p(s(x''))), s(s(s(p(s(x'))))))
MINUS(s(s(x''')), s(s(s(s(s(x')))))) -> MINUS(s(p(s(x'''))), s(s(s(s(p(s(x')))))))
minus(x, 0) -> x
minus(0, y) -> 0
minus(s(x), s(y)) -> minus(p(s(x)), p(s(y)))
minus(x, plus(y, z)) -> minus(minus(x, y), z)
p(s(s(x))) -> s(p(s(x)))
p(0) -> s(s(0))
div(s(x), s(y)) -> s(div(minus(x, y), s(y)))
div(plus(x, y), z) -> plus(div(x, z), div(y, z))
plus(0, y) -> y
plus(s(x), y) -> s(plus(y, minus(s(x), s(0))))
two new Dependency Pairs are created:
MINUS(s(s(x'')), s(s(s(s(x'))))) -> MINUS(s(p(s(x''))), s(s(s(p(s(x'))))))
MINUS(s(s(s(x0))), s(s(s(s(x'))))) -> MINUS(s(s(p(s(x0)))), s(s(s(p(s(x'))))))
MINUS(s(s(x'')), s(s(s(s(s(x0)))))) -> MINUS(s(p(s(x''))), s(s(s(s(p(s(x0)))))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 6
↳Nar
...
→DP Problem 35
↳Narrowing Transformation
→DP Problem 3
↳Remaining
→DP Problem 4
↳Remaining
MINUS(s(s(x'')), s(s(s(s(s(x0)))))) -> MINUS(s(p(s(x''))), s(s(s(s(p(s(x0)))))))
MINUS(s(s(s(x0))), s(s(s(s(x'))))) -> MINUS(s(s(p(s(x0)))), s(s(s(p(s(x'))))))
MINUS(s(s(s(s(x'')))), s(s(s(x''')))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x''')))))
MINUS(s(s(x''')), s(s(s(s(s(x')))))) -> MINUS(s(p(s(x'''))), s(s(s(s(p(s(x')))))))
MINUS(s(s(s(x'))), s(s(s(s(x''))))) -> MINUS(s(s(p(s(x')))), s(s(s(p(s(x''))))))
MINUS(s(s(s(x''))), s(s(s(s(x0))))) -> MINUS(s(s(p(s(x'')))), s(s(s(p(s(x0))))))
MINUS(s(s(s(s(x0)))), s(s(s(x')))) -> MINUS(s(s(s(p(s(x0))))), s(s(p(s(x')))))
MINUS(s(s(s(x'))), s(s(s(s(x''))))) -> MINUS(s(s(p(s(x')))), s(s(s(p(s(x''))))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(s(x0)))), s(s(s(x')))) -> MINUS(s(s(s(p(s(x0))))), s(s(p(s(x')))))
MINUS(s(s(s(s(s(x'))))), s(s(x''))) -> MINUS(s(s(s(s(p(s(x')))))), s(p(s(x''))))
MINUS(s(s(x'')), s(s(s(s(s(x0)))))) -> MINUS(s(p(s(x''))), s(s(s(s(p(s(x0)))))))
MINUS(s(s(s(x0))), s(s(s(s(x'))))) -> MINUS(s(s(p(s(x0)))), s(s(s(p(s(x'))))))
MINUS(s(s(s(x'))), s(s(s(s(x''))))) -> MINUS(s(s(p(s(x')))), s(s(s(p(s(x''))))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(x0))), s(s(s(s(x'))))) -> MINUS(s(s(p(s(x0)))), s(s(s(p(s(x'))))))
MINUS(s(s(s(s(x')))), s(s(s(x'')))) -> MINUS(s(s(s(p(s(x'))))), s(s(p(s(x'')))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(s(s(x0))))), s(s(x'))) -> MINUS(s(s(s(s(p(s(x0)))))), s(p(s(x'))))
MINUS(s(s(s(x'))), s(s(s(s(x''))))) -> MINUS(s(s(p(s(x')))), s(s(s(p(s(x''))))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(s(x0)))), s(s(s(x')))) -> MINUS(s(s(s(p(s(x0))))), s(s(p(s(x')))))
MINUS(s(s(s(s(s(x'))))), s(s(x''))) -> MINUS(s(s(s(s(p(s(x')))))), s(p(s(x''))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(s(s(x0))))), s(s(x'))) -> MINUS(s(s(s(s(p(s(x0)))))), s(p(s(x'))))
MINUS(s(s(s(s(s(x'))))), s(s(x''))) -> MINUS(s(s(s(s(p(s(x')))))), s(p(s(x''))))
MINUS(s(s(s(s(s(s(x'')))))), s(y)) -> MINUS(s(s(s(s(s(p(s(x''))))))), p(s(y)))
MINUS(s(x), s(s(s(s(s(x''')))))) -> MINUS(p(s(x)), s(s(s(s(p(s(x''')))))))
MINUS(s(s(x''')), s(s(s(s(x''))))) -> MINUS(s(p(s(x'''))), s(s(s(p(s(x''))))))
MINUS(s(s(s(x'))), s(s(s(s(x''))))) -> MINUS(s(s(p(s(x')))), s(s(s(p(s(x''))))))
minus(x, 0) -> x
minus(0, y) -> 0
minus(s(x), s(y)) -> minus(p(s(x)), p(s(y)))
minus(x, plus(y, z)) -> minus(minus(x, y), z)
p(s(s(x))) -> s(p(s(x)))
p(0) -> s(s(0))
div(s(x), s(y)) -> s(div(minus(x, y), s(y)))
div(plus(x, y), z) -> plus(div(x, z), div(y, z))
plus(0, y) -> y
plus(s(x), y) -> s(plus(y, minus(s(x), s(0))))
two new Dependency Pairs are created:
MINUS(s(s(x''')), s(s(s(s(x''))))) -> MINUS(s(p(s(x'''))), s(s(s(p(s(x''))))))
MINUS(s(s(s(x'))), s(s(s(s(x''))))) -> MINUS(s(s(p(s(x')))), s(s(s(p(s(x''))))))
MINUS(s(s(x''')), s(s(s(s(s(x')))))) -> MINUS(s(p(s(x'''))), s(s(s(s(p(s(x')))))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 6
↳Nar
...
→DP Problem 36
↳Narrowing Transformation
→DP Problem 3
↳Remaining
→DP Problem 4
↳Remaining
MINUS(s(s(x''')), s(s(s(s(s(x')))))) -> MINUS(s(p(s(x'''))), s(s(s(s(p(s(x')))))))
MINUS(s(s(s(x'))), s(s(s(s(x''))))) -> MINUS(s(s(p(s(x')))), s(s(s(p(s(x''))))))
MINUS(s(s(s(x0))), s(s(s(s(x'))))) -> MINUS(s(s(p(s(x0)))), s(s(s(p(s(x'))))))
MINUS(s(s(s(x'))), s(s(s(s(x''))))) -> MINUS(s(s(p(s(x')))), s(s(s(p(s(x''))))))
MINUS(s(s(s(s(x'')))), s(s(s(x''')))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x''')))))
MINUS(s(s(x''')), s(s(s(s(s(x')))))) -> MINUS(s(p(s(x'''))), s(s(s(s(p(s(x')))))))
MINUS(s(s(s(x'))), s(s(s(s(x''))))) -> MINUS(s(s(p(s(x')))), s(s(s(p(s(x''))))))
MINUS(s(s(s(x''))), s(s(s(s(x0))))) -> MINUS(s(s(p(s(x'')))), s(s(s(p(s(x0))))))
MINUS(s(s(s(s(x0)))), s(s(s(x')))) -> MINUS(s(s(s(p(s(x0))))), s(s(p(s(x')))))
MINUS(s(s(s(x'))), s(s(s(s(x''))))) -> MINUS(s(s(p(s(x')))), s(s(s(p(s(x''))))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(s(x0)))), s(s(s(x')))) -> MINUS(s(s(s(p(s(x0))))), s(s(p(s(x')))))
MINUS(s(s(s(s(s(x'))))), s(s(x''))) -> MINUS(s(s(s(s(p(s(x')))))), s(p(s(x''))))
MINUS(s(s(x'')), s(s(s(s(s(x0)))))) -> MINUS(s(p(s(x''))), s(s(s(s(p(s(x0)))))))
MINUS(s(s(s(x0))), s(s(s(s(x'))))) -> MINUS(s(s(p(s(x0)))), s(s(s(p(s(x'))))))
MINUS(s(s(s(x'))), s(s(s(s(x''))))) -> MINUS(s(s(p(s(x')))), s(s(s(p(s(x''))))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(x0))), s(s(s(s(x'))))) -> MINUS(s(s(p(s(x0)))), s(s(s(p(s(x'))))))
MINUS(s(s(s(s(x')))), s(s(s(x'')))) -> MINUS(s(s(s(p(s(x'))))), s(s(p(s(x'')))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(s(s(x0))))), s(s(x'))) -> MINUS(s(s(s(s(p(s(x0)))))), s(p(s(x'))))
MINUS(s(s(s(x'))), s(s(s(s(x''))))) -> MINUS(s(s(p(s(x')))), s(s(s(p(s(x''))))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(s(x0)))), s(s(s(x')))) -> MINUS(s(s(s(p(s(x0))))), s(s(p(s(x')))))
MINUS(s(s(s(s(s(x'))))), s(s(x''))) -> MINUS(s(s(s(s(p(s(x')))))), s(p(s(x''))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(s(s(x0))))), s(s(x'))) -> MINUS(s(s(s(s(p(s(x0)))))), s(p(s(x'))))
MINUS(s(s(s(s(s(x'))))), s(s(x''))) -> MINUS(s(s(s(s(p(s(x')))))), s(p(s(x''))))
MINUS(s(s(s(s(s(s(x'')))))), s(y)) -> MINUS(s(s(s(s(s(p(s(x''))))))), p(s(y)))
MINUS(s(x), s(s(s(s(s(x''')))))) -> MINUS(p(s(x)), s(s(s(s(p(s(x''')))))))
MINUS(s(s(x'')), s(s(s(s(s(x0)))))) -> MINUS(s(p(s(x''))), s(s(s(s(p(s(x0)))))))
minus(x, 0) -> x
minus(0, y) -> 0
minus(s(x), s(y)) -> minus(p(s(x)), p(s(y)))
minus(x, plus(y, z)) -> minus(minus(x, y), z)
p(s(s(x))) -> s(p(s(x)))
p(0) -> s(s(0))
div(s(x), s(y)) -> s(div(minus(x, y), s(y)))
div(plus(x, y), z) -> plus(div(x, z), div(y, z))
plus(0, y) -> y
plus(s(x), y) -> s(plus(y, minus(s(x), s(0))))
two new Dependency Pairs are created:
MINUS(s(x), s(s(s(s(s(x''')))))) -> MINUS(p(s(x)), s(s(s(s(p(s(x''')))))))
MINUS(s(s(x'')), s(s(s(s(s(x''')))))) -> MINUS(s(p(s(x''))), s(s(s(s(p(s(x''')))))))
MINUS(s(x), s(s(s(s(s(s(x''))))))) -> MINUS(p(s(x)), s(s(s(s(s(p(s(x''))))))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 3
↳Remaining Obligation(s)
→DP Problem 4
↳Remaining Obligation(s)
MINUS(s(x), s(s(s(s(s(s(x''))))))) -> MINUS(p(s(x)), s(s(s(s(s(p(s(x''))))))))
MINUS(s(s(x'')), s(s(s(s(s(x''')))))) -> MINUS(s(p(s(x''))), s(s(s(s(p(s(x''')))))))
MINUS(s(s(s(x'))), s(s(s(s(x''))))) -> MINUS(s(s(p(s(x')))), s(s(s(p(s(x''))))))
MINUS(s(s(x'')), s(s(s(s(s(x0)))))) -> MINUS(s(p(s(x''))), s(s(s(s(p(s(x0)))))))
MINUS(s(s(s(x0))), s(s(s(s(x'))))) -> MINUS(s(s(p(s(x0)))), s(s(s(p(s(x'))))))
MINUS(s(s(s(x'))), s(s(s(s(x''))))) -> MINUS(s(s(p(s(x')))), s(s(s(p(s(x''))))))
MINUS(s(s(s(s(x'')))), s(s(s(x''')))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x''')))))
MINUS(s(s(x''')), s(s(s(s(s(x')))))) -> MINUS(s(p(s(x'''))), s(s(s(s(p(s(x')))))))
MINUS(s(s(s(x'))), s(s(s(s(x''))))) -> MINUS(s(s(p(s(x')))), s(s(s(p(s(x''))))))
MINUS(s(s(s(x''))), s(s(s(s(x0))))) -> MINUS(s(s(p(s(x'')))), s(s(s(p(s(x0))))))
MINUS(s(s(s(s(x0)))), s(s(s(x')))) -> MINUS(s(s(s(p(s(x0))))), s(s(p(s(x')))))
MINUS(s(s(s(x'))), s(s(s(s(x''))))) -> MINUS(s(s(p(s(x')))), s(s(s(p(s(x''))))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(s(x0)))), s(s(s(x')))) -> MINUS(s(s(s(p(s(x0))))), s(s(p(s(x')))))
MINUS(s(s(s(s(s(x'))))), s(s(x''))) -> MINUS(s(s(s(s(p(s(x')))))), s(p(s(x''))))
MINUS(s(s(x'')), s(s(s(s(s(x0)))))) -> MINUS(s(p(s(x''))), s(s(s(s(p(s(x0)))))))
MINUS(s(s(s(x0))), s(s(s(s(x'))))) -> MINUS(s(s(p(s(x0)))), s(s(s(p(s(x'))))))
MINUS(s(s(s(x'))), s(s(s(s(x''))))) -> MINUS(s(s(p(s(x')))), s(s(s(p(s(x''))))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(x0))), s(s(s(s(x'))))) -> MINUS(s(s(p(s(x0)))), s(s(s(p(s(x'))))))
MINUS(s(s(s(s(x')))), s(s(s(x'')))) -> MINUS(s(s(s(p(s(x'))))), s(s(p(s(x'')))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(s(s(x0))))), s(s(x'))) -> MINUS(s(s(s(s(p(s(x0)))))), s(p(s(x'))))
MINUS(s(s(s(x'))), s(s(s(s(x''))))) -> MINUS(s(s(p(s(x')))), s(s(s(p(s(x''))))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(s(x0)))), s(s(s(x')))) -> MINUS(s(s(s(p(s(x0))))), s(s(p(s(x')))))
MINUS(s(s(s(s(s(x'))))), s(s(x''))) -> MINUS(s(s(s(s(p(s(x')))))), s(p(s(x''))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(s(s(x0))))), s(s(x'))) -> MINUS(s(s(s(s(p(s(x0)))))), s(p(s(x'))))
MINUS(s(s(s(s(s(x'))))), s(s(x''))) -> MINUS(s(s(s(s(p(s(x')))))), s(p(s(x''))))
MINUS(s(s(s(s(s(s(x'')))))), s(y)) -> MINUS(s(s(s(s(s(p(s(x''))))))), p(s(y)))
MINUS(s(s(x''')), s(s(s(s(s(x')))))) -> MINUS(s(p(s(x'''))), s(s(s(s(p(s(x')))))))
minus(x, 0) -> x
minus(0, y) -> 0
minus(s(x), s(y)) -> minus(p(s(x)), p(s(y)))
minus(x, plus(y, z)) -> minus(minus(x, y), z)
p(s(s(x))) -> s(p(s(x)))
p(0) -> s(s(0))
div(s(x), s(y)) -> s(div(minus(x, y), s(y)))
div(plus(x, y), z) -> plus(div(x, z), div(y, z))
plus(0, y) -> y
plus(s(x), y) -> s(plus(y, minus(s(x), s(0))))
PLUS(s(x), y) -> PLUS(y, minus(s(x), s(0)))
minus(x, 0) -> x
minus(0, y) -> 0
minus(s(x), s(y)) -> minus(p(s(x)), p(s(y)))
minus(x, plus(y, z)) -> minus(minus(x, y), z)
p(s(s(x))) -> s(p(s(x)))
p(0) -> s(s(0))
div(s(x), s(y)) -> s(div(minus(x, y), s(y)))
div(plus(x, y), z) -> plus(div(x, z), div(y, z))
plus(0, y) -> y
plus(s(x), y) -> s(plus(y, minus(s(x), s(0))))
DIV(plus(x, y), z) -> DIV(y, z)
DIV(plus(x, y), z) -> DIV(x, z)
DIV(s(x), s(y)) -> DIV(minus(x, y), s(y))
minus(x, 0) -> x
minus(0, y) -> 0
minus(s(x), s(y)) -> minus(p(s(x)), p(s(y)))
minus(x, plus(y, z)) -> minus(minus(x, y), z)
p(s(s(x))) -> s(p(s(x)))
p(0) -> s(s(0))
div(s(x), s(y)) -> s(div(minus(x, y), s(y)))
div(plus(x, y), z) -> plus(div(x, z), div(y, z))
plus(0, y) -> y
plus(s(x), y) -> s(plus(y, minus(s(x), s(0))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 3
↳Remaining Obligation(s)
→DP Problem 4
↳Remaining Obligation(s)
MINUS(s(x), s(s(s(s(s(s(x''))))))) -> MINUS(p(s(x)), s(s(s(s(s(p(s(x''))))))))
MINUS(s(s(x'')), s(s(s(s(s(x''')))))) -> MINUS(s(p(s(x''))), s(s(s(s(p(s(x''')))))))
MINUS(s(s(s(x'))), s(s(s(s(x''))))) -> MINUS(s(s(p(s(x')))), s(s(s(p(s(x''))))))
MINUS(s(s(x'')), s(s(s(s(s(x0)))))) -> MINUS(s(p(s(x''))), s(s(s(s(p(s(x0)))))))
MINUS(s(s(s(x0))), s(s(s(s(x'))))) -> MINUS(s(s(p(s(x0)))), s(s(s(p(s(x'))))))
MINUS(s(s(s(x'))), s(s(s(s(x''))))) -> MINUS(s(s(p(s(x')))), s(s(s(p(s(x''))))))
MINUS(s(s(s(s(x'')))), s(s(s(x''')))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x''')))))
MINUS(s(s(x''')), s(s(s(s(s(x')))))) -> MINUS(s(p(s(x'''))), s(s(s(s(p(s(x')))))))
MINUS(s(s(s(x'))), s(s(s(s(x''))))) -> MINUS(s(s(p(s(x')))), s(s(s(p(s(x''))))))
MINUS(s(s(s(x''))), s(s(s(s(x0))))) -> MINUS(s(s(p(s(x'')))), s(s(s(p(s(x0))))))
MINUS(s(s(s(s(x0)))), s(s(s(x')))) -> MINUS(s(s(s(p(s(x0))))), s(s(p(s(x')))))
MINUS(s(s(s(x'))), s(s(s(s(x''))))) -> MINUS(s(s(p(s(x')))), s(s(s(p(s(x''))))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(s(x0)))), s(s(s(x')))) -> MINUS(s(s(s(p(s(x0))))), s(s(p(s(x')))))
MINUS(s(s(s(s(s(x'))))), s(s(x''))) -> MINUS(s(s(s(s(p(s(x')))))), s(p(s(x''))))
MINUS(s(s(x'')), s(s(s(s(s(x0)))))) -> MINUS(s(p(s(x''))), s(s(s(s(p(s(x0)))))))
MINUS(s(s(s(x0))), s(s(s(s(x'))))) -> MINUS(s(s(p(s(x0)))), s(s(s(p(s(x'))))))
MINUS(s(s(s(x'))), s(s(s(s(x''))))) -> MINUS(s(s(p(s(x')))), s(s(s(p(s(x''))))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(x0))), s(s(s(s(x'))))) -> MINUS(s(s(p(s(x0)))), s(s(s(p(s(x'))))))
MINUS(s(s(s(s(x')))), s(s(s(x'')))) -> MINUS(s(s(s(p(s(x'))))), s(s(p(s(x'')))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(s(s(x0))))), s(s(x'))) -> MINUS(s(s(s(s(p(s(x0)))))), s(p(s(x'))))
MINUS(s(s(s(x'))), s(s(s(s(x''))))) -> MINUS(s(s(p(s(x')))), s(s(s(p(s(x''))))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(s(x0)))), s(s(s(x')))) -> MINUS(s(s(s(p(s(x0))))), s(s(p(s(x')))))
MINUS(s(s(s(s(s(x'))))), s(s(x''))) -> MINUS(s(s(s(s(p(s(x')))))), s(p(s(x''))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(s(s(x0))))), s(s(x'))) -> MINUS(s(s(s(s(p(s(x0)))))), s(p(s(x'))))
MINUS(s(s(s(s(s(x'))))), s(s(x''))) -> MINUS(s(s(s(s(p(s(x')))))), s(p(s(x''))))
MINUS(s(s(s(s(s(s(x'')))))), s(y)) -> MINUS(s(s(s(s(s(p(s(x''))))))), p(s(y)))
MINUS(s(s(x''')), s(s(s(s(s(x')))))) -> MINUS(s(p(s(x'''))), s(s(s(s(p(s(x')))))))
minus(x, 0) -> x
minus(0, y) -> 0
minus(s(x), s(y)) -> minus(p(s(x)), p(s(y)))
minus(x, plus(y, z)) -> minus(minus(x, y), z)
p(s(s(x))) -> s(p(s(x)))
p(0) -> s(s(0))
div(s(x), s(y)) -> s(div(minus(x, y), s(y)))
div(plus(x, y), z) -> plus(div(x, z), div(y, z))
plus(0, y) -> y
plus(s(x), y) -> s(plus(y, minus(s(x), s(0))))
PLUS(s(x), y) -> PLUS(y, minus(s(x), s(0)))
minus(x, 0) -> x
minus(0, y) -> 0
minus(s(x), s(y)) -> minus(p(s(x)), p(s(y)))
minus(x, plus(y, z)) -> minus(minus(x, y), z)
p(s(s(x))) -> s(p(s(x)))
p(0) -> s(s(0))
div(s(x), s(y)) -> s(div(minus(x, y), s(y)))
div(plus(x, y), z) -> plus(div(x, z), div(y, z))
plus(0, y) -> y
plus(s(x), y) -> s(plus(y, minus(s(x), s(0))))
DIV(plus(x, y), z) -> DIV(y, z)
DIV(plus(x, y), z) -> DIV(x, z)
DIV(s(x), s(y)) -> DIV(minus(x, y), s(y))
minus(x, 0) -> x
minus(0, y) -> 0
minus(s(x), s(y)) -> minus(p(s(x)), p(s(y)))
minus(x, plus(y, z)) -> minus(minus(x, y), z)
p(s(s(x))) -> s(p(s(x)))
p(0) -> s(s(0))
div(s(x), s(y)) -> s(div(minus(x, y), s(y)))
div(plus(x, y), z) -> plus(div(x, z), div(y, z))
plus(0, y) -> y
plus(s(x), y) -> s(plus(y, minus(s(x), s(0))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 3
↳Remaining Obligation(s)
→DP Problem 4
↳Remaining Obligation(s)
MINUS(s(x), s(s(s(s(s(s(x''))))))) -> MINUS(p(s(x)), s(s(s(s(s(p(s(x''))))))))
MINUS(s(s(x'')), s(s(s(s(s(x''')))))) -> MINUS(s(p(s(x''))), s(s(s(s(p(s(x''')))))))
MINUS(s(s(s(x'))), s(s(s(s(x''))))) -> MINUS(s(s(p(s(x')))), s(s(s(p(s(x''))))))
MINUS(s(s(x'')), s(s(s(s(s(x0)))))) -> MINUS(s(p(s(x''))), s(s(s(s(p(s(x0)))))))
MINUS(s(s(s(x0))), s(s(s(s(x'))))) -> MINUS(s(s(p(s(x0)))), s(s(s(p(s(x'))))))
MINUS(s(s(s(x'))), s(s(s(s(x''))))) -> MINUS(s(s(p(s(x')))), s(s(s(p(s(x''))))))
MINUS(s(s(s(s(x'')))), s(s(s(x''')))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x''')))))
MINUS(s(s(x''')), s(s(s(s(s(x')))))) -> MINUS(s(p(s(x'''))), s(s(s(s(p(s(x')))))))
MINUS(s(s(s(x'))), s(s(s(s(x''))))) -> MINUS(s(s(p(s(x')))), s(s(s(p(s(x''))))))
MINUS(s(s(s(x''))), s(s(s(s(x0))))) -> MINUS(s(s(p(s(x'')))), s(s(s(p(s(x0))))))
MINUS(s(s(s(s(x0)))), s(s(s(x')))) -> MINUS(s(s(s(p(s(x0))))), s(s(p(s(x')))))
MINUS(s(s(s(x'))), s(s(s(s(x''))))) -> MINUS(s(s(p(s(x')))), s(s(s(p(s(x''))))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(s(x0)))), s(s(s(x')))) -> MINUS(s(s(s(p(s(x0))))), s(s(p(s(x')))))
MINUS(s(s(s(s(s(x'))))), s(s(x''))) -> MINUS(s(s(s(s(p(s(x')))))), s(p(s(x''))))
MINUS(s(s(x'')), s(s(s(s(s(x0)))))) -> MINUS(s(p(s(x''))), s(s(s(s(p(s(x0)))))))
MINUS(s(s(s(x0))), s(s(s(s(x'))))) -> MINUS(s(s(p(s(x0)))), s(s(s(p(s(x'))))))
MINUS(s(s(s(x'))), s(s(s(s(x''))))) -> MINUS(s(s(p(s(x')))), s(s(s(p(s(x''))))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(x0))), s(s(s(s(x'))))) -> MINUS(s(s(p(s(x0)))), s(s(s(p(s(x'))))))
MINUS(s(s(s(s(x')))), s(s(s(x'')))) -> MINUS(s(s(s(p(s(x'))))), s(s(p(s(x'')))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(s(s(x0))))), s(s(x'))) -> MINUS(s(s(s(s(p(s(x0)))))), s(p(s(x'))))
MINUS(s(s(s(x'))), s(s(s(s(x''))))) -> MINUS(s(s(p(s(x')))), s(s(s(p(s(x''))))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(s(x0)))), s(s(s(x')))) -> MINUS(s(s(s(p(s(x0))))), s(s(p(s(x')))))
MINUS(s(s(s(s(s(x'))))), s(s(x''))) -> MINUS(s(s(s(s(p(s(x')))))), s(p(s(x''))))
MINUS(s(s(s(s(x'')))), s(s(s(x0)))) -> MINUS(s(s(s(p(s(x''))))), s(s(p(s(x0)))))
MINUS(s(s(s(s(s(x0))))), s(s(x'))) -> MINUS(s(s(s(s(p(s(x0)))))), s(p(s(x'))))
MINUS(s(s(s(s(s(x'))))), s(s(x''))) -> MINUS(s(s(s(s(p(s(x')))))), s(p(s(x''))))
MINUS(s(s(s(s(s(s(x'')))))), s(y)) -> MINUS(s(s(s(s(s(p(s(x''))))))), p(s(y)))
MINUS(s(s(x''')), s(s(s(s(s(x')))))) -> MINUS(s(p(s(x'''))), s(s(s(s(p(s(x')))))))
minus(x, 0) -> x
minus(0, y) -> 0
minus(s(x), s(y)) -> minus(p(s(x)), p(s(y)))
minus(x, plus(y, z)) -> minus(minus(x, y), z)
p(s(s(x))) -> s(p(s(x)))
p(0) -> s(s(0))
div(s(x), s(y)) -> s(div(minus(x, y), s(y)))
div(plus(x, y), z) -> plus(div(x, z), div(y, z))
plus(0, y) -> y
plus(s(x), y) -> s(plus(y, minus(s(x), s(0))))
PLUS(s(x), y) -> PLUS(y, minus(s(x), s(0)))
minus(x, 0) -> x
minus(0, y) -> 0
minus(s(x), s(y)) -> minus(p(s(x)), p(s(y)))
minus(x, plus(y, z)) -> minus(minus(x, y), z)
p(s(s(x))) -> s(p(s(x)))
p(0) -> s(s(0))
div(s(x), s(y)) -> s(div(minus(x, y), s(y)))
div(plus(x, y), z) -> plus(div(x, z), div(y, z))
plus(0, y) -> y
plus(s(x), y) -> s(plus(y, minus(s(x), s(0))))
DIV(plus(x, y), z) -> DIV(y, z)
DIV(plus(x, y), z) -> DIV(x, z)
DIV(s(x), s(y)) -> DIV(minus(x, y), s(y))
minus(x, 0) -> x
minus(0, y) -> 0
minus(s(x), s(y)) -> minus(p(s(x)), p(s(y)))
minus(x, plus(y, z)) -> minus(minus(x, y), z)
p(s(s(x))) -> s(p(s(x)))
p(0) -> s(s(0))
div(s(x), s(y)) -> s(div(minus(x, y), s(y)))
div(plus(x, y), z) -> plus(div(x, z), div(y, z))
plus(0, y) -> y
plus(s(x), y) -> s(plus(y, minus(s(x), s(0))))