R
↳Dependency Pair Analysis
TIMES(x, plus(y, s(z))) -> PLUS(times(x, plus(y, times(s(z), 0))), times(x, s(z)))
TIMES(x, plus(y, s(z))) -> TIMES(x, plus(y, times(s(z), 0)))
TIMES(x, plus(y, s(z))) -> PLUS(y, times(s(z), 0))
TIMES(x, plus(y, s(z))) -> TIMES(s(z), 0)
TIMES(x, plus(y, s(z))) -> TIMES(x, s(z))
TIMES(x, s(y)) -> PLUS(times(x, y), x)
TIMES(x, s(y)) -> TIMES(x, y)
PLUS(x, s(y)) -> PLUS(x, y)
R
↳DPs
→DP Problem 1
↳Argument Filtering and Ordering
→DP Problem 2
↳Nar
PLUS(x, s(y)) -> PLUS(x, y)
times(x, plus(y, s(z))) -> plus(times(x, plus(y, times(s(z), 0))), times(x, s(z)))
times(x, 0) -> 0
times(x, s(y)) -> plus(times(x, y), x)
plus(x, 0) -> x
plus(x, s(y)) -> s(plus(x, y))
PLUS(x, s(y)) -> PLUS(x, y)
POL(PLUS(x1, x2)) = x1 + x2 POL(s(x1)) = 1 + x1
PLUS(x1, x2) -> PLUS(x1, x2)
s(x1) -> s(x1)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 3
↳Dependency Graph
→DP Problem 2
↳Nar
times(x, plus(y, s(z))) -> plus(times(x, plus(y, times(s(z), 0))), times(x, s(z)))
times(x, 0) -> 0
times(x, s(y)) -> plus(times(x, y), x)
plus(x, 0) -> x
plus(x, s(y)) -> s(plus(x, y))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Narrowing Transformation
TIMES(x, s(y)) -> TIMES(x, y)
TIMES(x, plus(y, s(z))) -> TIMES(x, s(z))
TIMES(x, plus(y, s(z))) -> TIMES(x, plus(y, times(s(z), 0)))
times(x, plus(y, s(z))) -> plus(times(x, plus(y, times(s(z), 0))), times(x, s(z)))
times(x, 0) -> 0
times(x, s(y)) -> plus(times(x, y), x)
plus(x, 0) -> x
plus(x, s(y)) -> s(plus(x, y))
one new Dependency Pair is created:
TIMES(x, plus(y, s(z))) -> TIMES(x, plus(y, times(s(z), 0)))
TIMES(x, plus(y, s(z'))) -> TIMES(x, plus(y, 0))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Argument Filtering and Ordering
TIMES(x, plus(y, s(z'))) -> TIMES(x, plus(y, 0))
TIMES(x, plus(y, s(z))) -> TIMES(x, s(z))
TIMES(x, s(y)) -> TIMES(x, y)
times(x, plus(y, s(z))) -> plus(times(x, plus(y, times(s(z), 0))), times(x, s(z)))
times(x, 0) -> 0
times(x, s(y)) -> plus(times(x, y), x)
plus(x, 0) -> x
plus(x, s(y)) -> s(plus(x, y))
TIMES(x, plus(y, s(z'))) -> TIMES(x, plus(y, 0))
TIMES(x, s(y)) -> TIMES(x, y)
plus(x, 0) -> x
plus(x, s(y)) -> s(plus(x, y))
POL(TIMES(x1, x2)) = 1 + x1 + x2 POL(plus(x1, x2)) = x1 + x2 POL(0) = 0 POL(s(x1)) = 1 + x1
TIMES(x1, x2) -> TIMES(x1, x2)
s(x1) -> s(x1)
plus(x1, x2) -> plus(x1, x2)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳AFS
...
→DP Problem 5
↳Dependency Graph
TIMES(x, plus(y, s(z))) -> TIMES(x, s(z))
times(x, plus(y, s(z))) -> plus(times(x, plus(y, times(s(z), 0))), times(x, s(z)))
times(x, 0) -> 0
times(x, s(y)) -> plus(times(x, y), x)
plus(x, 0) -> x
plus(x, s(y)) -> s(plus(x, y))