R
↳Dependency Pair Analysis
P(p(s(x))) -> P(x)
LE(p(s(x)), x) -> LE(x, x)
LE(s(x), s(y)) -> LE(x, y)
MINUS(x, y) -> IF(le(x, y), x, y)
MINUS(x, y) -> LE(x, y)
IF(false, x, y) -> MINUS(p(x), y)
IF(false, x, y) -> P(x)
R
↳DPs
→DP Problem 1
↳Argument Filtering and Ordering
→DP Problem 2
↳Nar
LE(s(x), s(y)) -> LE(x, y)
p(0) -> s(s(0))
p(s(x)) -> x
p(p(s(x))) -> p(x)
le(p(s(x)), x) -> le(x, x)
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
minus(x, y) -> if(le(x, y), x, y)
if(true, x, y) -> 0
if(false, x, y) -> s(minus(p(x), y))
innermost
LE(s(x), s(y)) -> LE(x, y)
trivial
LE(x1, x2) -> LE(x1, x2)
s(x1) -> s(x1)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 3
↳Dependency Graph
→DP Problem 2
↳Nar
p(0) -> s(s(0))
p(s(x)) -> x
p(p(s(x))) -> p(x)
le(p(s(x)), x) -> le(x, x)
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
minus(x, y) -> if(le(x, y), x, y)
if(true, x, y) -> 0
if(false, x, y) -> s(minus(p(x), y))
innermost
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Narrowing Transformation
IF(false, x, y) -> MINUS(p(x), y)
MINUS(x, y) -> IF(le(x, y), x, y)
p(0) -> s(s(0))
p(s(x)) -> x
p(p(s(x))) -> p(x)
le(p(s(x)), x) -> le(x, x)
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
minus(x, y) -> if(le(x, y), x, y)
if(true, x, y) -> 0
if(false, x, y) -> s(minus(p(x), y))
innermost
three new Dependency Pairs are created:
MINUS(x, y) -> IF(le(x, y), x, y)
MINUS(0, y'') -> IF(true, 0, y'')
MINUS(s(x''), 0) -> IF(false, s(x''), 0)
MINUS(s(x''), s(y'')) -> IF(le(x'', y''), s(x''), s(y''))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Narrowing Transformation
MINUS(s(x''), s(y'')) -> IF(le(x'', y''), s(x''), s(y''))
MINUS(s(x''), 0) -> IF(false, s(x''), 0)
IF(false, x, y) -> MINUS(p(x), y)
p(0) -> s(s(0))
p(s(x)) -> x
p(p(s(x))) -> p(x)
le(p(s(x)), x) -> le(x, x)
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
minus(x, y) -> if(le(x, y), x, y)
if(true, x, y) -> 0
if(false, x, y) -> s(minus(p(x), y))
innermost
two new Dependency Pairs are created:
IF(false, x, y) -> MINUS(p(x), y)
IF(false, 0, y) -> MINUS(s(s(0)), y)
IF(false, s(x''), y) -> MINUS(x'', y)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Nar
...
→DP Problem 5
↳Instantiation Transformation
MINUS(s(x''), 0) -> IF(false, s(x''), 0)
IF(false, s(x''), y) -> MINUS(x'', y)
MINUS(s(x''), s(y'')) -> IF(le(x'', y''), s(x''), s(y''))
p(0) -> s(s(0))
p(s(x)) -> x
p(p(s(x))) -> p(x)
le(p(s(x)), x) -> le(x, x)
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
minus(x, y) -> if(le(x, y), x, y)
if(true, x, y) -> 0
if(false, x, y) -> s(minus(p(x), y))
innermost
two new Dependency Pairs are created:
IF(false, s(x''), y) -> MINUS(x'', y)
IF(false, s(x''''), 0) -> MINUS(x'''', 0)
IF(false, s(x''''), s(y'''')) -> MINUS(x'''', s(y''''))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Nar
...
→DP Problem 6
↳Argument Filtering and Ordering
IF(false, s(x''''), 0) -> MINUS(x'''', 0)
MINUS(s(x''), 0) -> IF(false, s(x''), 0)
p(0) -> s(s(0))
p(s(x)) -> x
p(p(s(x))) -> p(x)
le(p(s(x)), x) -> le(x, x)
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
minus(x, y) -> if(le(x, y), x, y)
if(true, x, y) -> 0
if(false, x, y) -> s(minus(p(x), y))
innermost
IF(false, s(x''''), 0) -> MINUS(x'''', 0)
MINUS(s(x''), 0) -> IF(false, s(x''), 0)
{0, s, false} > {MINUS, IF}
IF(x1, x2, x3) -> IF(x1, x2, x3)
MINUS(x1, x2) -> MINUS(x1, x2)
s(x1) -> s(x1)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Nar
...
→DP Problem 8
↳Dependency Graph
p(0) -> s(s(0))
p(s(x)) -> x
p(p(s(x))) -> p(x)
le(p(s(x)), x) -> le(x, x)
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
minus(x, y) -> if(le(x, y), x, y)
if(true, x, y) -> 0
if(false, x, y) -> s(minus(p(x), y))
innermost
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Nar
...
→DP Problem 7
↳Argument Filtering and Ordering
IF(false, s(x''''), s(y'''')) -> MINUS(x'''', s(y''''))
MINUS(s(x''), s(y'')) -> IF(le(x'', y''), s(x''), s(y''))
p(0) -> s(s(0))
p(s(x)) -> x
p(p(s(x))) -> p(x)
le(p(s(x)), x) -> le(x, x)
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
minus(x, y) -> if(le(x, y), x, y)
if(true, x, y) -> 0
if(false, x, y) -> s(minus(p(x), y))
innermost
IF(false, s(x''''), s(y'''')) -> MINUS(x'''', s(y''''))
trivial
IF(x1, x2, x3) -> x2
s(x1) -> s(x1)
MINUS(x1, x2) -> x1
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Nar
...
→DP Problem 9
↳Dependency Graph
MINUS(s(x''), s(y'')) -> IF(le(x'', y''), s(x''), s(y''))
p(0) -> s(s(0))
p(s(x)) -> x
p(p(s(x))) -> p(x)
le(p(s(x)), x) -> le(x, x)
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
minus(x, y) -> if(le(x, y), x, y)
if(true, x, y) -> 0
if(false, x, y) -> s(minus(p(x), y))
innermost