R
↳Dependency Pair Analysis
EVEN(s(s(x))) -> EVEN(x)
HALF(s(s(x))) -> HALF(x)
PLUS(s(x), y) -> PLUS(x, y)
TIMES(s(x), y) -> IFTIMES(even(s(x)), s(x), y)
TIMES(s(x), y) -> EVEN(s(x))
IFTIMES(true, s(x), y) -> PLUS(times(half(s(x)), y), times(half(s(x)), y))
IFTIMES(true, s(x), y) -> TIMES(half(s(x)), y)
IFTIMES(true, s(x), y) -> HALF(s(x))
IFTIMES(false, s(x), y) -> PLUS(y, times(x, y))
IFTIMES(false, s(x), y) -> TIMES(x, y)
R
↳DPs
→DP Problem 1
↳Usable Rules (Innermost)
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
→DP Problem 4
↳UsableRules
EVEN(s(s(x))) -> EVEN(x)
even(0) -> true
even(s(0)) -> false
even(s(s(x))) -> even(x)
half(0) -> 0
half(s(s(x))) -> s(half(x))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
times(0, y) -> 0
times(s(x), y) -> iftimes(even(s(x)), s(x), y)
iftimes(true, s(x), y) -> plus(times(half(s(x)), y), times(half(s(x)), y))
iftimes(false, s(x), y) -> plus(y, times(x, y))
innermost
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 5
↳Size-Change Principle
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
→DP Problem 4
↳UsableRules
EVEN(s(s(x))) -> EVEN(x)
none
innermost
|
|
trivial
s(x1) -> s(x1)
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳Usable Rules (Innermost)
→DP Problem 3
↳UsableRules
→DP Problem 4
↳UsableRules
HALF(s(s(x))) -> HALF(x)
even(0) -> true
even(s(0)) -> false
even(s(s(x))) -> even(x)
half(0) -> 0
half(s(s(x))) -> s(half(x))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
times(0, y) -> 0
times(s(x), y) -> iftimes(even(s(x)), s(x), y)
iftimes(true, s(x), y) -> plus(times(half(s(x)), y), times(half(s(x)), y))
iftimes(false, s(x), y) -> plus(y, times(x, y))
innermost
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 6
↳Size-Change Principle
→DP Problem 3
↳UsableRules
→DP Problem 4
↳UsableRules
HALF(s(s(x))) -> HALF(x)
none
innermost
|
|
trivial
s(x1) -> s(x1)
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 3
↳Usable Rules (Innermost)
→DP Problem 4
↳UsableRules
PLUS(s(x), y) -> PLUS(x, y)
even(0) -> true
even(s(0)) -> false
even(s(s(x))) -> even(x)
half(0) -> 0
half(s(s(x))) -> s(half(x))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
times(0, y) -> 0
times(s(x), y) -> iftimes(even(s(x)), s(x), y)
iftimes(true, s(x), y) -> plus(times(half(s(x)), y), times(half(s(x)), y))
iftimes(false, s(x), y) -> plus(y, times(x, y))
innermost
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
→DP Problem 7
↳Size-Change Principle
→DP Problem 4
↳UsableRules
PLUS(s(x), y) -> PLUS(x, y)
none
innermost
|
|
trivial
s(x1) -> s(x1)
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
→DP Problem 4
↳Usable Rules (Innermost)
IFTIMES(false, s(x), y) -> TIMES(x, y)
IFTIMES(true, s(x), y) -> TIMES(half(s(x)), y)
TIMES(s(x), y) -> IFTIMES(even(s(x)), s(x), y)
even(0) -> true
even(s(0)) -> false
even(s(s(x))) -> even(x)
half(0) -> 0
half(s(s(x))) -> s(half(x))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
times(0, y) -> 0
times(s(x), y) -> iftimes(even(s(x)), s(x), y)
iftimes(true, s(x), y) -> plus(times(half(s(x)), y), times(half(s(x)), y))
iftimes(false, s(x), y) -> plus(y, times(x, y))
innermost
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
→DP Problem 4
↳UsableRules
→DP Problem 8
↳Negative Polynomial Order
IFTIMES(false, s(x), y) -> TIMES(x, y)
IFTIMES(true, s(x), y) -> TIMES(half(s(x)), y)
TIMES(s(x), y) -> IFTIMES(even(s(x)), s(x), y)
half(0) -> 0
half(s(s(x))) -> s(half(x))
even(s(0)) -> false
even(s(s(x))) -> even(x)
even(0) -> true
innermost
IFTIMES(false, s(x), y) -> TIMES(x, y)
half(0) -> 0
half(s(s(x))) -> s(half(x))
even(s(0)) -> false
even(s(s(x))) -> even(x)
even(0) -> true
POL( IFTIMES(x1, ..., x3) ) = x2
POL( s(x1) ) = x1 + 1
POL( TIMES(x1, x2) ) = x1
POL( half(x1) ) = x1
POL( 0 ) = 0
POL( even(x1) ) = 0
POL( false ) = 0
POL( true ) = 0
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
→DP Problem 4
↳UsableRules
→DP Problem 8
↳Neg POLO
...
→DP Problem 9
↳Narrowing Transformation
IFTIMES(true, s(x), y) -> TIMES(half(s(x)), y)
TIMES(s(x), y) -> IFTIMES(even(s(x)), s(x), y)
half(0) -> 0
half(s(s(x))) -> s(half(x))
even(s(0)) -> false
even(s(s(x))) -> even(x)
even(0) -> true
innermost
one new Dependency Pair is created:
IFTIMES(true, s(x), y) -> TIMES(half(s(x)), y)
IFTIMES(true, s(s(x'')), y) -> TIMES(s(half(x'')), y)
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
→DP Problem 4
↳UsableRules
→DP Problem 8
↳Neg POLO
...
→DP Problem 10
↳Narrowing Transformation
IFTIMES(true, s(s(x'')), y) -> TIMES(s(half(x'')), y)
TIMES(s(x), y) -> IFTIMES(even(s(x)), s(x), y)
half(0) -> 0
half(s(s(x))) -> s(half(x))
even(s(0)) -> false
even(s(s(x))) -> even(x)
even(0) -> true
innermost
two new Dependency Pairs are created:
TIMES(s(x), y) -> IFTIMES(even(s(x)), s(x), y)
TIMES(s(0), y) -> IFTIMES(false, s(0), y)
TIMES(s(s(x'')), y) -> IFTIMES(even(x''), s(s(x'')), y)
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
→DP Problem 4
↳UsableRules
→DP Problem 8
↳Neg POLO
...
→DP Problem 11
↳Negative Polynomial Order
TIMES(s(s(x'')), y) -> IFTIMES(even(x''), s(s(x'')), y)
IFTIMES(true, s(s(x'')), y) -> TIMES(s(half(x'')), y)
half(0) -> 0
half(s(s(x))) -> s(half(x))
even(s(0)) -> false
even(s(s(x))) -> even(x)
even(0) -> true
innermost
TIMES(s(s(x'')), y) -> IFTIMES(even(x''), s(s(x'')), y)
even(s(0)) -> false
even(s(s(x))) -> even(x)
even(0) -> true
half(0) -> 0
half(s(s(x))) -> s(half(x))
POL( TIMES(x1, x2) ) = x1 + 1
POL( s(x1) ) = x1 + 1
POL( IFTIMES(x1, ..., x3) ) = x2
POL( half(x1) ) = x1
POL( even(x1) ) = 0
POL( false ) = 0
POL( true ) = 0
POL( 0 ) = 0
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
→DP Problem 4
↳UsableRules
→DP Problem 8
↳Neg POLO
...
→DP Problem 12
↳Dependency Graph
IFTIMES(true, s(s(x'')), y) -> TIMES(s(half(x'')), y)
half(0) -> 0
half(s(s(x))) -> s(half(x))
even(s(0)) -> false
even(s(s(x))) -> even(x)
even(0) -> true
innermost