R
↳Dependency Pair Analysis
FUNCTION(p, s(s(x)), dummy, dummy2) -> FUNCTION(p, s(x), x, x)
FUNCTION(plus, dummy, x, y) -> FUNCTION(if, function(iszero, x, x, x), x, y)
FUNCTION(plus, dummy, x, y) -> FUNCTION(iszero, x, x, x)
FUNCTION(if, false, x, y) -> FUNCTION(plus, function(third, x, y, y), function(p, x, x, y), s(y))
FUNCTION(if, false, x, y) -> FUNCTION(third, x, y, y)
FUNCTION(if, false, x, y) -> FUNCTION(p, x, x, y)
R
↳DPs
→DP Problem 1
↳Usable Rules (Innermost)
→DP Problem 2
↳UsableRules
FUNCTION(p, s(s(x)), dummy, dummy2) -> FUNCTION(p, s(x), x, x)
function(iszero, 0, dummy, dummy2) -> true
function(iszero, s(x), dummy, dummy2) -> false
function(p, 0, dummy, dummy2) -> 0
function(p, s(0), dummy, dummy2) -> 0
function(p, s(s(x)), dummy, dummy2) -> s(function(p, s(x), x, x))
function(plus, dummy, x, y) -> function(if, function(iszero, x, x, x), x, y)
function(if, true, x, y) -> y
function(if, false, x, y) -> function(plus, function(third, x, y, y), function(p, x, x, y), s(y))
function(third, x, y, z) -> z
innermost
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 3
↳Size-Change Principle
→DP Problem 2
↳UsableRules
FUNCTION(p, s(s(x)), dummy, dummy2) -> FUNCTION(p, s(x), x, x)
none
innermost
|
|
trivial
s(x1) -> s(x1)
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳Usable Rules (Innermost)
FUNCTION(if, false, x, y) -> FUNCTION(plus, function(third, x, y, y), function(p, x, x, y), s(y))
FUNCTION(plus, dummy, x, y) -> FUNCTION(if, function(iszero, x, x, x), x, y)
function(iszero, 0, dummy, dummy2) -> true
function(iszero, s(x), dummy, dummy2) -> false
function(p, 0, dummy, dummy2) -> 0
function(p, s(0), dummy, dummy2) -> 0
function(p, s(s(x)), dummy, dummy2) -> s(function(p, s(x), x, x))
function(plus, dummy, x, y) -> function(if, function(iszero, x, x, x), x, y)
function(if, true, x, y) -> y
function(if, false, x, y) -> function(plus, function(third, x, y, y), function(p, x, x, y), s(y))
function(third, x, y, z) -> z
innermost
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 4
↳Rewriting Transformation
FUNCTION(if, false, x, y) -> FUNCTION(plus, function(third, x, y, y), function(p, x, x, y), s(y))
FUNCTION(plus, dummy, x, y) -> FUNCTION(if, function(iszero, x, x, x), x, y)
function(p, s(s(x)), dummy, dummy2) -> s(function(p, s(x), x, x))
function(p, 0, dummy, dummy2) -> 0
function(p, s(0), dummy, dummy2) -> 0
function(third, x, y, z) -> z
function(iszero, 0, dummy, dummy2) -> true
function(iszero, s(x), dummy, dummy2) -> false
innermost
one new Dependency Pair is created:
FUNCTION(if, false, x, y) -> FUNCTION(plus, function(third, x, y, y), function(p, x, x, y), s(y))
FUNCTION(if, false, x, y) -> FUNCTION(plus, y, function(p, x, x, y), s(y))
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 4
↳Rw
...
→DP Problem 5
↳Usable Rules (Innermost)
FUNCTION(if, false, x, y) -> FUNCTION(plus, y, function(p, x, x, y), s(y))
FUNCTION(plus, dummy, x, y) -> FUNCTION(if, function(iszero, x, x, x), x, y)
function(p, s(s(x)), dummy, dummy2) -> s(function(p, s(x), x, x))
function(p, 0, dummy, dummy2) -> 0
function(p, s(0), dummy, dummy2) -> 0
function(third, x, y, z) -> z
function(iszero, 0, dummy, dummy2) -> true
function(iszero, s(x), dummy, dummy2) -> false
innermost
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 4
↳Rw
...
→DP Problem 6
↳Narrowing Transformation
FUNCTION(if, false, x, y) -> FUNCTION(plus, y, function(p, x, x, y), s(y))
FUNCTION(plus, dummy, x, y) -> FUNCTION(if, function(iszero, x, x, x), x, y)
function(p, s(s(x)), dummy, dummy2) -> s(function(p, s(x), x, x))
function(p, 0, dummy, dummy2) -> 0
function(p, s(0), dummy, dummy2) -> 0
function(iszero, 0, dummy, dummy2) -> true
function(iszero, s(x), dummy, dummy2) -> false
innermost
two new Dependency Pairs are created:
FUNCTION(plus, dummy, x, y) -> FUNCTION(if, function(iszero, x, x, x), x, y)
FUNCTION(plus, dummy, 0, y) -> FUNCTION(if, true, 0, y)
FUNCTION(plus, dummy, s(x''), y) -> FUNCTION(if, false, s(x''), y)
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 4
↳Rw
...
→DP Problem 7
↳Narrowing Transformation
FUNCTION(plus, dummy, s(x''), y) -> FUNCTION(if, false, s(x''), y)
FUNCTION(if, false, x, y) -> FUNCTION(plus, y, function(p, x, x, y), s(y))
function(p, s(s(x)), dummy, dummy2) -> s(function(p, s(x), x, x))
function(p, 0, dummy, dummy2) -> 0
function(p, s(0), dummy, dummy2) -> 0
function(iszero, 0, dummy, dummy2) -> true
function(iszero, s(x), dummy, dummy2) -> false
innermost
three new Dependency Pairs are created:
FUNCTION(if, false, x, y) -> FUNCTION(plus, y, function(p, x, x, y), s(y))
FUNCTION(if, false, s(s(x'')), y') -> FUNCTION(plus, y', s(function(p, s(x''), x'', x'')), s(y'))
FUNCTION(if, false, 0, y') -> FUNCTION(plus, y', 0, s(y'))
FUNCTION(if, false, s(0), y') -> FUNCTION(plus, y', 0, s(y'))
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 4
↳Rw
...
→DP Problem 8
↳Instantiation Transformation
FUNCTION(if, false, s(s(x'')), y') -> FUNCTION(plus, y', s(function(p, s(x''), x'', x'')), s(y'))
FUNCTION(plus, dummy, s(x''), y) -> FUNCTION(if, false, s(x''), y)
function(p, s(s(x)), dummy, dummy2) -> s(function(p, s(x), x, x))
function(p, 0, dummy, dummy2) -> 0
function(p, s(0), dummy, dummy2) -> 0
function(iszero, 0, dummy, dummy2) -> true
function(iszero, s(x), dummy, dummy2) -> false
innermost
one new Dependency Pair is created:
FUNCTION(plus, dummy, s(x''), y) -> FUNCTION(if, false, s(x''), y)
FUNCTION(plus, dummy', s(x'''), s(dummy')) -> FUNCTION(if, false, s(x'''), s(dummy'))
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 4
↳Rw
...
→DP Problem 9
↳Instantiation Transformation
FUNCTION(plus, dummy', s(x'''), s(dummy')) -> FUNCTION(if, false, s(x'''), s(dummy'))
FUNCTION(if, false, s(s(x'')), y') -> FUNCTION(plus, y', s(function(p, s(x''), x'', x'')), s(y'))
function(p, s(s(x)), dummy, dummy2) -> s(function(p, s(x), x, x))
function(p, 0, dummy, dummy2) -> 0
function(p, s(0), dummy, dummy2) -> 0
function(iszero, 0, dummy, dummy2) -> true
function(iszero, s(x), dummy, dummy2) -> false
innermost
one new Dependency Pair is created:
FUNCTION(if, false, s(s(x'')), y') -> FUNCTION(plus, y', s(function(p, s(x''), x'', x'')), s(y'))
FUNCTION(if, false, s(s(x''')), s(dummy''')) -> FUNCTION(plus, s(dummy'''), s(function(p, s(x'''), x''', x''')), s(s(dummy''')))
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 4
↳Rw
...
→DP Problem 10
↳Usable Rules (Innermost)
FUNCTION(if, false, s(s(x''')), s(dummy''')) -> FUNCTION(plus, s(dummy'''), s(function(p, s(x'''), x''', x''')), s(s(dummy''')))
FUNCTION(plus, dummy', s(x'''), s(dummy')) -> FUNCTION(if, false, s(x'''), s(dummy'))
function(p, s(s(x)), dummy, dummy2) -> s(function(p, s(x), x, x))
function(p, 0, dummy, dummy2) -> 0
function(p, s(0), dummy, dummy2) -> 0
function(iszero, 0, dummy, dummy2) -> true
function(iszero, s(x), dummy, dummy2) -> false
innermost
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 4
↳Rw
...
→DP Problem 11
↳Instantiation Transformation
FUNCTION(if, false, s(s(x''')), s(dummy''')) -> FUNCTION(plus, s(dummy'''), s(function(p, s(x'''), x''', x''')), s(s(dummy''')))
FUNCTION(plus, dummy', s(x'''), s(dummy')) -> FUNCTION(if, false, s(x'''), s(dummy'))
function(p, s(s(x)), dummy, dummy2) -> s(function(p, s(x), x, x))
function(p, s(0), dummy, dummy2) -> 0
innermost
one new Dependency Pair is created:
FUNCTION(plus, dummy', s(x'''), s(dummy')) -> FUNCTION(if, false, s(x'''), s(dummy'))
FUNCTION(plus, s(dummy'''''), s(x''''), s(s(dummy'''''))) -> FUNCTION(if, false, s(x''''), s(s(dummy''''')))
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 4
↳Rw
...
→DP Problem 12
↳Instantiation Transformation
FUNCTION(plus, s(dummy'''''), s(x''''), s(s(dummy'''''))) -> FUNCTION(if, false, s(x''''), s(s(dummy''''')))
FUNCTION(if, false, s(s(x''')), s(dummy''')) -> FUNCTION(plus, s(dummy'''), s(function(p, s(x'''), x''', x''')), s(s(dummy''')))
function(p, s(s(x)), dummy, dummy2) -> s(function(p, s(x), x, x))
function(p, s(0), dummy, dummy2) -> 0
innermost
one new Dependency Pair is created:
FUNCTION(if, false, s(s(x''')), s(dummy''')) -> FUNCTION(plus, s(dummy'''), s(function(p, s(x'''), x''', x''')), s(s(dummy''')))
FUNCTION(if, false, s(s(x'''')), s(s(dummy'''''''))) -> FUNCTION(plus, s(s(dummy''''''')), s(function(p, s(x''''), x'''', x'''')), s(s(s(dummy'''''''))))
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 4
↳Rw
...
→DP Problem 13
↳Negative Polynomial Order
FUNCTION(if, false, s(s(x'''')), s(s(dummy'''''''))) -> FUNCTION(plus, s(s(dummy''''''')), s(function(p, s(x''''), x'''', x'''')), s(s(s(dummy'''''''))))
FUNCTION(plus, s(dummy'''''), s(x''''), s(s(dummy'''''))) -> FUNCTION(if, false, s(x''''), s(s(dummy''''')))
function(p, s(s(x)), dummy, dummy2) -> s(function(p, s(x), x, x))
function(p, s(0), dummy, dummy2) -> 0
innermost
FUNCTION(if, false, s(s(x'''')), s(s(dummy'''''''))) -> FUNCTION(plus, s(s(dummy''''''')), s(function(p, s(x''''), x'''', x'''')), s(s(s(dummy'''''''))))
function(p, s(s(x)), dummy, dummy2) -> s(function(p, s(x), x, x))
function(p, s(0), dummy, dummy2) -> 0
POL( FUNCTION(x1, ..., x4) ) = max{0, x3 - 1}
POL( s(x1) ) = x1 + 1
POL( function(x1, ..., x4) ) = max{0, x2 - 1}
POL( 0 ) = 0
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 4
↳Rw
...
→DP Problem 14
↳Dependency Graph
FUNCTION(plus, s(dummy'''''), s(x''''), s(s(dummy'''''))) -> FUNCTION(if, false, s(x''''), s(s(dummy''''')))
function(p, s(s(x)), dummy, dummy2) -> s(function(p, s(x), x, x))
function(p, s(0), dummy, dummy2) -> 0
innermost