R
↳Dependency Pair Analysis
SUM(cons(s(n), x), cons(m, y)) -> SUM(cons(n, x), cons(s(m), y))
SUM(cons(0, x), y) -> SUM(x, y)
WEIGHT(cons(n, cons(m, x))) -> WEIGHT(sum(cons(n, cons(m, x)), cons(0, x)))
WEIGHT(cons(n, cons(m, x))) -> SUM(cons(n, cons(m, x)), cons(0, x))
R
↳DPs
→DP Problem 1
↳Argument Filtering and Ordering
→DP Problem 2
↳AFS
SUM(cons(0, x), y) -> SUM(x, y)
SUM(cons(s(n), x), cons(m, y)) -> SUM(cons(n, x), cons(s(m), y))
sum(cons(s(n), x), cons(m, y)) -> sum(cons(n, x), cons(s(m), y))
sum(cons(0, x), y) -> sum(x, y)
sum(nil, y) -> y
weight(cons(n, cons(m, x))) -> weight(sum(cons(n, cons(m, x)), cons(0, x)))
weight(cons(n, nil)) -> n
SUM(cons(0, x), y) -> SUM(x, y)
POL(SUM(x1, x2)) = 1 + x1 + x2 POL(0) = 0 POL(cons(x1, x2)) = 1 + x1 + x2 POL(s(x1)) = x1
SUM(x1, x2) -> SUM(x1, x2)
cons(x1, x2) -> cons(x1, x2)
s(x1) -> s(x1)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 3
↳Instantiation Transformation
→DP Problem 2
↳AFS
SUM(cons(s(n), x), cons(m, y)) -> SUM(cons(n, x), cons(s(m), y))
sum(cons(s(n), x), cons(m, y)) -> sum(cons(n, x), cons(s(m), y))
sum(cons(0, x), y) -> sum(x, y)
sum(nil, y) -> y
weight(cons(n, cons(m, x))) -> weight(sum(cons(n, cons(m, x)), cons(0, x)))
weight(cons(n, nil)) -> n
one new Dependency Pair is created:
SUM(cons(s(n), x), cons(m, y)) -> SUM(cons(n, x), cons(s(m), y))
SUM(cons(s(n''), x''), cons(s(m''), y'')) -> SUM(cons(n'', x''), cons(s(s(m'')), y''))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 3
↳Inst
...
→DP Problem 4
↳Instantiation Transformation
→DP Problem 2
↳AFS
SUM(cons(s(n''), x''), cons(s(m''), y'')) -> SUM(cons(n'', x''), cons(s(s(m'')), y''))
sum(cons(s(n), x), cons(m, y)) -> sum(cons(n, x), cons(s(m), y))
sum(cons(0, x), y) -> sum(x, y)
sum(nil, y) -> y
weight(cons(n, cons(m, x))) -> weight(sum(cons(n, cons(m, x)), cons(0, x)))
weight(cons(n, nil)) -> n
one new Dependency Pair is created:
SUM(cons(s(n''), x''), cons(s(m''), y'')) -> SUM(cons(n'', x''), cons(s(s(m'')), y''))
SUM(cons(s(n''''), x''''), cons(s(s(m'''')), y'''')) -> SUM(cons(n'''', x''''), cons(s(s(s(m''''))), y''''))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 3
↳Inst
...
→DP Problem 5
↳Argument Filtering and Ordering
→DP Problem 2
↳AFS
SUM(cons(s(n''''), x''''), cons(s(s(m'''')), y'''')) -> SUM(cons(n'''', x''''), cons(s(s(s(m''''))), y''''))
sum(cons(s(n), x), cons(m, y)) -> sum(cons(n, x), cons(s(m), y))
sum(cons(0, x), y) -> sum(x, y)
sum(nil, y) -> y
weight(cons(n, cons(m, x))) -> weight(sum(cons(n, cons(m, x)), cons(0, x)))
weight(cons(n, nil)) -> n
SUM(cons(s(n''''), x''''), cons(s(s(m'''')), y'''')) -> SUM(cons(n'''', x''''), cons(s(s(s(m''''))), y''''))
POL(cons(x1, x2)) = x1 + x2 POL(s(x1)) = 1 + x1
SUM(x1, x2) -> x1
cons(x1, x2) -> cons(x1, x2)
s(x1) -> s(x1)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 3
↳Inst
...
→DP Problem 6
↳Dependency Graph
→DP Problem 2
↳AFS
sum(cons(s(n), x), cons(m, y)) -> sum(cons(n, x), cons(s(m), y))
sum(cons(0, x), y) -> sum(x, y)
sum(nil, y) -> y
weight(cons(n, cons(m, x))) -> weight(sum(cons(n, cons(m, x)), cons(0, x)))
weight(cons(n, nil)) -> n
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Argument Filtering and Ordering
WEIGHT(cons(n, cons(m, x))) -> WEIGHT(sum(cons(n, cons(m, x)), cons(0, x)))
sum(cons(s(n), x), cons(m, y)) -> sum(cons(n, x), cons(s(m), y))
sum(cons(0, x), y) -> sum(x, y)
sum(nil, y) -> y
weight(cons(n, cons(m, x))) -> weight(sum(cons(n, cons(m, x)), cons(0, x)))
weight(cons(n, nil)) -> n
WEIGHT(cons(n, cons(m, x))) -> WEIGHT(sum(cons(n, cons(m, x)), cons(0, x)))
sum(cons(s(n), x), cons(m, y)) -> sum(cons(n, x), cons(s(m), y))
sum(cons(0, x), y) -> sum(x, y)
sum(nil, y) -> y
POL(0) = 0 POL(cons(x1, x2)) = 1 + x1 + x2 POL(WEIGHT(x1)) = 1 + x1 POL(s(x1)) = x1
WEIGHT(x1) -> WEIGHT(x1)
cons(x1, x2) -> cons(x1, x2)
sum(x1, x2) -> x2
s(x1) -> s(x1)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 7
↳Dependency Graph
sum(cons(s(n), x), cons(m, y)) -> sum(cons(n, x), cons(s(m), y))
sum(cons(0, x), y) -> sum(x, y)
sum(nil, y) -> y
weight(cons(n, cons(m, x))) -> weight(sum(cons(n, cons(m, x)), cons(0, x)))
weight(cons(n, nil)) -> n