R
↳Dependency Pair Analysis
MINUS(s(x), s(y)) -> MINUS(x, y)
QUOT(s(x), s(y)) -> QUOT(minus(x, y), s(y))
QUOT(s(x), s(y)) -> MINUS(x, y)
PLUS(s(x), y) -> PLUS(x, y)
PLUS(minus(x, s(0)), minus(y, s(s(z)))) -> PLUS(minus(y, s(s(z))), minus(x, s(0)))
R
↳DPs
→DP Problem 1
↳Polynomial Ordering
→DP Problem 2
↳Polo
→DP Problem 3
↳Polo
MINUS(s(x), s(y)) -> MINUS(x, y)
minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
plus(minus(x, s(0)), minus(y, s(s(z)))) -> plus(minus(y, s(s(z))), minus(x, s(0)))
MINUS(s(x), s(y)) -> MINUS(x, y)
POL(MINUS(x1, x2)) = x1 POL(s(x1)) = 1 + x1
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 4
↳Dependency Graph
→DP Problem 2
↳Polo
→DP Problem 3
↳Polo
minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
plus(minus(x, s(0)), minus(y, s(s(z)))) -> plus(minus(y, s(s(z))), minus(x, s(0)))
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polynomial Ordering
→DP Problem 3
↳Polo
QUOT(s(x), s(y)) -> QUOT(minus(x, y), s(y))
minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
plus(minus(x, s(0)), minus(y, s(s(z)))) -> plus(minus(y, s(s(z))), minus(x, s(0)))
QUOT(s(x), s(y)) -> QUOT(minus(x, y), s(y))
minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
POL(QUOT(x1, x2)) = x1 POL(0) = 1 POL(minus(x1, x2)) = x1 POL(s(x1)) = 1 + x1
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polo
→DP Problem 5
↳Dependency Graph
→DP Problem 3
↳Polo
minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
plus(minus(x, s(0)), minus(y, s(s(z)))) -> plus(minus(y, s(s(z))), minus(x, s(0)))
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polo
→DP Problem 3
↳Polynomial Ordering
PLUS(minus(x, s(0)), minus(y, s(s(z)))) -> PLUS(minus(y, s(s(z))), minus(x, s(0)))
PLUS(s(x), y) -> PLUS(x, y)
minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
plus(minus(x, s(0)), minus(y, s(s(z)))) -> plus(minus(y, s(s(z))), minus(x, s(0)))
PLUS(s(x), y) -> PLUS(x, y)
minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
POL(PLUS(x1, x2)) = 1 + x1 + x2 POL(0) = 0 POL(minus(x1, x2)) = x1 POL(s(x1)) = 1 + x1
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polo
→DP Problem 3
↳Polo
→DP Problem 6
↳Narrowing Transformation
PLUS(minus(x, s(0)), minus(y, s(s(z)))) -> PLUS(minus(y, s(s(z))), minus(x, s(0)))
minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
plus(minus(x, s(0)), minus(y, s(s(z)))) -> plus(minus(y, s(s(z))), minus(x, s(0)))
two new Dependency Pairs are created:
PLUS(minus(x, s(0)), minus(y, s(s(z)))) -> PLUS(minus(y, s(s(z))), minus(x, s(0)))
PLUS(minus(x, s(0)), minus(s(x''), s(s(z')))) -> PLUS(minus(x'', s(z')), minus(x, s(0)))
PLUS(minus(s(x''), s(0)), minus(y, s(s(z)))) -> PLUS(minus(y, s(s(z))), minus(x'', 0))
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polo
→DP Problem 3
↳Polo
→DP Problem 6
↳Nar
...
→DP Problem 7
↳Polynomial Ordering
PLUS(minus(s(x''), s(0)), minus(y, s(s(z)))) -> PLUS(minus(y, s(s(z))), minus(x'', 0))
PLUS(minus(x, s(0)), minus(s(x''), s(s(z')))) -> PLUS(minus(x'', s(z')), minus(x, s(0)))
minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
plus(minus(x, s(0)), minus(y, s(s(z)))) -> plus(minus(y, s(s(z))), minus(x, s(0)))
PLUS(minus(s(x''), s(0)), minus(y, s(s(z)))) -> PLUS(minus(y, s(s(z))), minus(x'', 0))
PLUS(minus(x, s(0)), minus(s(x''), s(s(z')))) -> PLUS(minus(x'', s(z')), minus(x, s(0)))
minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
POL(PLUS(x1, x2)) = 1 + x1 + x2 POL(0) = 0 POL(minus(x1, x2)) = x1 POL(s(x1)) = 1 + x1
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polo
→DP Problem 3
↳Polo
→DP Problem 6
↳Nar
...
→DP Problem 8
↳Dependency Graph
minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
plus(minus(x, s(0)), minus(y, s(s(z)))) -> plus(minus(y, s(s(z))), minus(x, s(0)))