R
↳Dependency Pair Analysis
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) -> 0
p(s(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)
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) -> 0
p(s(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) -> 0
p(s(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) -> 0
p(s(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(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) -> 0
p(s(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
↳Forward Instantiation Transformation
IF(false, s(x''''), 0) -> MINUS(x'''', 0)
MINUS(s(x''), 0) -> IF(false, s(x''), 0)
p(0) -> 0
p(s(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
one new Dependency Pair is created:
IF(false, s(x''''), 0) -> MINUS(x'''', 0)
IF(false, s(s(x''''')), 0) -> MINUS(s(x'''''), 0)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Nar
...
→DP Problem 8
↳Forward Instantiation Transformation
IF(false, s(s(x''''')), 0) -> MINUS(s(x'''''), 0)
MINUS(s(x''), 0) -> IF(false, s(x''), 0)
p(0) -> 0
p(s(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
one new Dependency Pair is created:
MINUS(s(x''), 0) -> IF(false, s(x''), 0)
MINUS(s(s(x''''''')), 0) -> IF(false, s(s(x''''''')), 0)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Nar
...
→DP Problem 10
↳Argument Filtering and Ordering
MINUS(s(s(x''''''')), 0) -> IF(false, s(s(x''''''')), 0)
IF(false, s(s(x''''')), 0) -> MINUS(s(x'''''), 0)
p(0) -> 0
p(s(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(s(x''''')), 0) -> MINUS(s(x'''''), 0)
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 12
↳Dependency Graph
MINUS(s(s(x''''''')), 0) -> IF(false, s(s(x''''''')), 0)
p(0) -> 0
p(s(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
↳Forward Instantiation Transformation
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) -> 0
p(s(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
one new Dependency Pair is created:
IF(false, s(x''''), s(y'''')) -> MINUS(x'''', s(y''''))
IF(false, s(s(x''''')), s(y''''')) -> MINUS(s(x'''''), s(y'''''))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Nar
...
→DP Problem 9
↳Forward Instantiation Transformation
IF(false, s(s(x''''')), s(y''''')) -> MINUS(s(x'''''), s(y'''''))
MINUS(s(x''), s(y'')) -> IF(le(x'', y''), s(x''), s(y''))
p(0) -> 0
p(s(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
one new Dependency Pair is created:
MINUS(s(x''), s(y'')) -> IF(le(x'', y''), s(x''), s(y''))
MINUS(s(s(x''''''')), s(y''')) -> IF(le(s(x'''''''), y'''), s(s(x''''''')), s(y'''))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Nar
...
→DP Problem 11
↳Argument Filtering and Ordering
MINUS(s(s(x''''''')), s(y''')) -> IF(le(s(x'''''''), y'''), s(s(x''''''')), s(y'''))
IF(false, s(s(x''''')), s(y''''')) -> MINUS(s(x'''''), s(y'''''))
p(0) -> 0
p(s(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(s(x''''')), s(y''''')) -> MINUS(s(x'''''), s(y'''''))
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 13
↳Dependency Graph
MINUS(s(s(x''''''')), s(y''')) -> IF(le(s(x'''''''), y'''), s(s(x''''''')), s(y'''))
p(0) -> 0
p(s(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