R
↳Dependency Pair Analysis
MINUS(s(x), s(y)) -> MINUS(x, y)
DOUBLE(s(x)) -> DOUBLE(x)
PLUS(s(x), y) -> PLUS(x, y)
PLUS(s(x), y) -> PLUS(x, s(y))
PLUS(s(x), y) -> PLUS(minus(x, y), double(y))
PLUS(s(x), y) -> MINUS(x, y)
PLUS(s(x), y) -> DOUBLE(y)
PLUS(s(plus(x, y)), z) -> PLUS(plus(x, y), z)
R
↳DPs
→DP Problem 1
↳Polynomial Ordering
→DP Problem 2
↳Polo
→DP Problem 3
↳Nar
MINUS(s(x), s(y)) -> MINUS(x, y)
minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
double(0) -> 0
double(s(x)) -> s(s(double(x)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
plus(s(x), y) -> plus(x, s(y))
plus(s(x), y) -> s(plus(minus(x, y), double(y)))
plus(s(plus(x, y)), z) -> s(plus(plus(x, y), z))
innermost
MINUS(s(x), s(y)) -> MINUS(x, y)
POL(MINUS(x1, x2)) = x1 POL(s(x1)) = 1 + x1
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 4
↳Dependency Graph
→DP Problem 2
↳Polo
→DP Problem 3
↳Nar
minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
double(0) -> 0
double(s(x)) -> s(s(double(x)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
plus(s(x), y) -> plus(x, s(y))
plus(s(x), y) -> s(plus(minus(x, y), double(y)))
plus(s(plus(x, y)), z) -> s(plus(plus(x, y), z))
innermost
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polynomial Ordering
→DP Problem 3
↳Nar
DOUBLE(s(x)) -> DOUBLE(x)
minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
double(0) -> 0
double(s(x)) -> s(s(double(x)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
plus(s(x), y) -> plus(x, s(y))
plus(s(x), y) -> s(plus(minus(x, y), double(y)))
plus(s(plus(x, y)), z) -> s(plus(plus(x, y), z))
innermost
DOUBLE(s(x)) -> DOUBLE(x)
POL(DOUBLE(x1)) = x1 POL(s(x1)) = 1 + x1
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polo
→DP Problem 5
↳Dependency Graph
→DP Problem 3
↳Nar
minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
double(0) -> 0
double(s(x)) -> s(s(double(x)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
plus(s(x), y) -> plus(x, s(y))
plus(s(x), y) -> s(plus(minus(x, y), double(y)))
plus(s(plus(x, y)), z) -> s(plus(plus(x, y), z))
innermost
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polo
→DP Problem 3
↳Narrowing Transformation
PLUS(s(x), y) -> PLUS(minus(x, y), double(y))
PLUS(s(x), y) -> PLUS(x, s(y))
PLUS(s(x), y) -> PLUS(x, y)
minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
double(0) -> 0
double(s(x)) -> s(s(double(x)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
plus(s(x), y) -> plus(x, s(y))
plus(s(x), y) -> s(plus(minus(x, y), double(y)))
plus(s(plus(x, y)), z) -> s(plus(plus(x, y), z))
innermost
four new Dependency Pairs are created:
PLUS(s(x), y) -> PLUS(minus(x, y), double(y))
PLUS(s(x''), 0) -> PLUS(x'', double(0))
PLUS(s(s(x'')), s(y'')) -> PLUS(minus(x'', y''), double(s(y'')))
PLUS(s(x), 0) -> PLUS(minus(x, 0), 0)
PLUS(s(x), s(x'')) -> PLUS(minus(x, s(x'')), s(s(double(x''))))
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polo
→DP Problem 3
↳Nar
→DP Problem 6
↳Rewriting Transformation
PLUS(s(x), s(x'')) -> PLUS(minus(x, s(x'')), s(s(double(x''))))
PLUS(s(x), 0) -> PLUS(minus(x, 0), 0)
PLUS(s(s(x'')), s(y'')) -> PLUS(minus(x'', y''), double(s(y'')))
PLUS(s(x''), 0) -> PLUS(x'', double(0))
PLUS(s(x), y) -> PLUS(x, y)
PLUS(s(x), y) -> PLUS(x, s(y))
minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
double(0) -> 0
double(s(x)) -> s(s(double(x)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
plus(s(x), y) -> plus(x, s(y))
plus(s(x), y) -> s(plus(minus(x, y), double(y)))
plus(s(plus(x, y)), z) -> s(plus(plus(x, y), z))
innermost
one new Dependency Pair is created:
PLUS(s(x''), 0) -> PLUS(x'', double(0))
PLUS(s(x''), 0) -> PLUS(x'', 0)
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polo
→DP Problem 3
↳Nar
→DP Problem 6
↳Rw
...
→DP Problem 7
↳Rewriting Transformation
PLUS(s(x''), 0) -> PLUS(x'', 0)
PLUS(s(x), 0) -> PLUS(minus(x, 0), 0)
PLUS(s(s(x'')), s(y'')) -> PLUS(minus(x'', y''), double(s(y'')))
PLUS(s(x), y) -> PLUS(x, s(y))
PLUS(s(x), y) -> PLUS(x, y)
PLUS(s(x), s(x'')) -> PLUS(minus(x, s(x'')), s(s(double(x''))))
minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
double(0) -> 0
double(s(x)) -> s(s(double(x)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
plus(s(x), y) -> plus(x, s(y))
plus(s(x), y) -> s(plus(minus(x, y), double(y)))
plus(s(plus(x, y)), z) -> s(plus(plus(x, y), z))
innermost
one new Dependency Pair is created:
PLUS(s(s(x'')), s(y'')) -> PLUS(minus(x'', y''), double(s(y'')))
PLUS(s(s(x'')), s(y'')) -> PLUS(minus(x'', y''), s(s(double(y''))))
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polo
→DP Problem 3
↳Nar
→DP Problem 6
↳Rw
...
→DP Problem 8
↳Rewriting Transformation
PLUS(s(x), 0) -> PLUS(minus(x, 0), 0)
PLUS(s(s(x'')), s(y'')) -> PLUS(minus(x'', y''), s(s(double(y''))))
PLUS(s(x), s(x'')) -> PLUS(minus(x, s(x'')), s(s(double(x''))))
PLUS(s(x), y) -> PLUS(x, s(y))
PLUS(s(x), y) -> PLUS(x, y)
PLUS(s(x''), 0) -> PLUS(x'', 0)
minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
double(0) -> 0
double(s(x)) -> s(s(double(x)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
plus(s(x), y) -> plus(x, s(y))
plus(s(x), y) -> s(plus(minus(x, y), double(y)))
plus(s(plus(x, y)), z) -> s(plus(plus(x, y), z))
innermost
one new Dependency Pair is created:
PLUS(s(x), 0) -> PLUS(minus(x, 0), 0)
PLUS(s(x), 0) -> PLUS(x, 0)
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polo
→DP Problem 3
↳Nar
→DP Problem 6
↳Rw
...
→DP Problem 9
↳Forward Instantiation Transformation
PLUS(s(x), 0) -> PLUS(x, 0)
PLUS(s(x''), 0) -> PLUS(x'', 0)
PLUS(s(x), s(x'')) -> PLUS(minus(x, s(x'')), s(s(double(x''))))
PLUS(s(x), y) -> PLUS(x, s(y))
PLUS(s(x), y) -> PLUS(x, y)
PLUS(s(s(x'')), s(y'')) -> PLUS(minus(x'', y''), s(s(double(y''))))
minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
double(0) -> 0
double(s(x)) -> s(s(double(x)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
plus(s(x), y) -> plus(x, s(y))
plus(s(x), y) -> s(plus(minus(x, y), double(y)))
plus(s(plus(x, y)), z) -> s(plus(plus(x, y), z))
innermost
five new Dependency Pairs are created:
PLUS(s(x), y) -> PLUS(x, y)
PLUS(s(s(x'')), y'') -> PLUS(s(x''), y'')
PLUS(s(s(x'')), s(x'''')) -> PLUS(s(x''), s(x''''))
PLUS(s(s(x'''')), 0) -> PLUS(s(x''''), 0)
PLUS(s(s(s(x''''))), s(y'''')) -> PLUS(s(s(x'''')), s(y''''))
PLUS(s(s(x'')), 0) -> PLUS(s(x''), 0)
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polo
→DP Problem 3
↳Nar
→DP Problem 6
↳Rw
...
→DP Problem 10
↳Forward Instantiation Transformation
PLUS(s(s(s(x''''))), s(y'''')) -> PLUS(s(s(x'''')), s(y''''))
PLUS(s(s(x'')), s(x'''')) -> PLUS(s(x''), s(x''''))
PLUS(s(s(x'')), 0) -> PLUS(s(x''), 0)
PLUS(s(s(x'''')), 0) -> PLUS(s(x''''), 0)
PLUS(s(x''), 0) -> PLUS(x'', 0)
PLUS(s(s(x'')), y'') -> PLUS(s(x''), y'')
PLUS(s(s(x'')), s(y'')) -> PLUS(minus(x'', y''), s(s(double(y''))))
PLUS(s(x), s(x'')) -> PLUS(minus(x, s(x'')), s(s(double(x''))))
PLUS(s(x), y) -> PLUS(x, s(y))
PLUS(s(x), 0) -> PLUS(x, 0)
minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
double(0) -> 0
double(s(x)) -> s(s(double(x)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
plus(s(x), y) -> plus(x, s(y))
plus(s(x), y) -> s(plus(minus(x, y), double(y)))
plus(s(plus(x, y)), z) -> s(plus(plus(x, y), z))
innermost
four new Dependency Pairs are created:
PLUS(s(x), y) -> PLUS(x, s(y))
PLUS(s(s(x'')), y'') -> PLUS(s(x''), s(y''))
PLUS(s(s(x'')), y') -> PLUS(s(x''), s(y'))
PLUS(s(s(s(x''''))), y') -> PLUS(s(s(x'''')), s(y'))
PLUS(s(s(s(s(x'''''')))), y') -> PLUS(s(s(s(x''''''))), s(y'))
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polo
→DP Problem 3
↳Nar
→DP Problem 6
↳Rw
...
→DP Problem 11
↳Forward Instantiation Transformation
PLUS(s(s(s(s(x'''''')))), y') -> PLUS(s(s(s(x''''''))), s(y'))
PLUS(s(s(s(x''''))), y') -> PLUS(s(s(x'''')), s(y'))
PLUS(s(s(x'')), y') -> PLUS(s(x''), s(y'))
PLUS(s(s(x'')), s(x'''')) -> PLUS(s(x''), s(x''''))
PLUS(s(s(x'')), y'') -> PLUS(s(x''), s(y''))
PLUS(s(s(x'')), 0) -> PLUS(s(x''), 0)
PLUS(s(s(x'''')), 0) -> PLUS(s(x''''), 0)
PLUS(s(x), 0) -> PLUS(x, 0)
PLUS(s(x''), 0) -> PLUS(x'', 0)
PLUS(s(s(x'')), y'') -> PLUS(s(x''), y'')
PLUS(s(s(x'')), s(y'')) -> PLUS(minus(x'', y''), s(s(double(y''))))
PLUS(s(x), s(x'')) -> PLUS(minus(x, s(x'')), s(s(double(x''))))
PLUS(s(s(s(x''''))), s(y'''')) -> PLUS(s(s(x'''')), s(y''''))
minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
double(0) -> 0
double(s(x)) -> s(s(double(x)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
plus(s(x), y) -> plus(x, s(y))
plus(s(x), y) -> s(plus(minus(x, y), double(y)))
plus(s(plus(x, y)), z) -> s(plus(plus(x, y), z))
innermost
six new Dependency Pairs are created:
PLUS(s(x''), 0) -> PLUS(x'', 0)
PLUS(s(s(x'''')), 0) -> PLUS(s(x''''), 0)
PLUS(s(s(x''')), 0) -> PLUS(s(x'''), 0)
PLUS(s(s(s(x''''))), 0) -> PLUS(s(s(x'''')), 0)
PLUS(s(s(s(x''''''))), 0) -> PLUS(s(s(x'''''')), 0)
PLUS(s(s(s(s(x'''''')))), 0) -> PLUS(s(s(s(x''''''))), 0)
PLUS(s(s(s(s(s(x''''''''))))), 0) -> PLUS(s(s(s(s(x'''''''')))), 0)
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polo
→DP Problem 3
↳Nar
→DP Problem 6
↳Rw
...
→DP Problem 12
↳Forward Instantiation Transformation
PLUS(s(s(s(s(s(x''''''''))))), 0) -> PLUS(s(s(s(s(x'''''''')))), 0)
PLUS(s(s(s(s(x'''''')))), 0) -> PLUS(s(s(s(x''''''))), 0)
PLUS(s(s(s(x''''''))), 0) -> PLUS(s(s(x'''''')), 0)
PLUS(s(s(s(x''''))), 0) -> PLUS(s(s(x'''')), 0)
PLUS(s(s(x''')), 0) -> PLUS(s(x'''), 0)
PLUS(s(s(x'''')), 0) -> PLUS(s(x''''), 0)
PLUS(s(s(s(x''''))), y') -> PLUS(s(s(x'''')), s(y'))
PLUS(s(s(x'')), y') -> PLUS(s(x''), s(y'))
PLUS(s(s(s(x''''))), s(y'''')) -> PLUS(s(s(x'''')), s(y''''))
PLUS(s(s(x'')), s(x'''')) -> PLUS(s(x''), s(x''''))
PLUS(s(s(x'')), y'') -> PLUS(s(x''), s(y''))
PLUS(s(s(x'')), 0) -> PLUS(s(x''), 0)
PLUS(s(s(x'''')), 0) -> PLUS(s(x''''), 0)
PLUS(s(x), 0) -> PLUS(x, 0)
PLUS(s(s(x'')), y'') -> PLUS(s(x''), y'')
PLUS(s(s(x'')), s(y'')) -> PLUS(minus(x'', y''), s(s(double(y''))))
PLUS(s(x), s(x'')) -> PLUS(minus(x, s(x'')), s(s(double(x''))))
PLUS(s(s(s(s(x'''''')))), y') -> PLUS(s(s(s(x''''''))), s(y'))
minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
double(0) -> 0
double(s(x)) -> s(s(double(x)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
plus(s(x), y) -> plus(x, s(y))
plus(s(x), y) -> s(plus(minus(x, y), double(y)))
plus(s(plus(x, y)), z) -> s(plus(plus(x, y), z))
innermost
eight new Dependency Pairs are created:
PLUS(s(x), 0) -> PLUS(x, 0)
PLUS(s(s(x'')), 0) -> PLUS(s(x''), 0)
PLUS(s(s(s(x''''))), 0) -> PLUS(s(s(x'''')), 0)
PLUS(s(s(s(x''''''))), 0) -> PLUS(s(s(x'''''')), 0)
PLUS(s(s(s(s(x'''''')))), 0) -> PLUS(s(s(s(x''''''))), 0)
PLUS(s(s(s(s(s(x''''''''))))), 0) -> PLUS(s(s(s(s(x'''''''')))), 0)
PLUS(s(s(s(x'''''))), 0) -> PLUS(s(s(x''''')), 0)
PLUS(s(s(s(s(x'''''''')))), 0) -> PLUS(s(s(s(x''''''''))), 0)
PLUS(s(s(s(s(s(s(x'''''''''')))))), 0) -> PLUS(s(s(s(s(s(x''''''''''))))), 0)
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polo
→DP Problem 3
↳Nar
→DP Problem 6
↳Rw
...
→DP Problem 13
↳Remaining Obligation(s)
PLUS(s(s(s(s(s(s(x'''''''''')))))), 0) -> PLUS(s(s(s(s(s(x''''''''''))))), 0)
PLUS(s(s(s(s(x'''''''')))), 0) -> PLUS(s(s(s(x''''''''))), 0)
PLUS(s(s(s(x'''''))), 0) -> PLUS(s(s(x''''')), 0)
PLUS(s(s(s(s(s(x''''''''))))), 0) -> PLUS(s(s(s(s(x'''''''')))), 0)
PLUS(s(s(s(s(x'''''')))), 0) -> PLUS(s(s(s(x''''''))), 0)
PLUS(s(s(s(x''''''))), 0) -> PLUS(s(s(x'''''')), 0)
PLUS(s(s(s(x''''))), 0) -> PLUS(s(s(x'''')), 0)
PLUS(s(s(x'')), 0) -> PLUS(s(x''), 0)
PLUS(s(s(s(s(x'''''')))), 0) -> PLUS(s(s(s(x''''''))), 0)
PLUS(s(s(s(x''''''))), 0) -> PLUS(s(s(x'''''')), 0)
PLUS(s(s(s(x''''))), 0) -> PLUS(s(s(x'''')), 0)
PLUS(s(s(x''')), 0) -> PLUS(s(x'''), 0)
PLUS(s(s(x'''')), 0) -> PLUS(s(x''''), 0)
PLUS(s(s(x'')), 0) -> PLUS(s(x''), 0)
PLUS(s(s(x'''')), 0) -> PLUS(s(x''''), 0)
PLUS(s(s(s(s(x'''''')))), y') -> PLUS(s(s(s(x''''''))), s(y'))
PLUS(s(s(s(x''''))), y') -> PLUS(s(s(x'''')), s(y'))
PLUS(s(s(x'')), y') -> PLUS(s(x''), s(y'))
PLUS(s(s(x'')), y'') -> PLUS(s(x''), s(y''))
PLUS(s(s(s(x''''))), s(y'''')) -> PLUS(s(s(x'''')), s(y''''))
PLUS(s(s(x'')), s(x'''')) -> PLUS(s(x''), s(x''''))
PLUS(s(s(x'')), s(y'')) -> PLUS(minus(x'', y''), s(s(double(y''))))
PLUS(s(x), s(x'')) -> PLUS(minus(x, s(x'')), s(s(double(x''))))
PLUS(s(s(x'')), y'') -> PLUS(s(x''), y'')
PLUS(s(s(s(s(s(x''''''''))))), 0) -> PLUS(s(s(s(s(x'''''''')))), 0)
minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
double(0) -> 0
double(s(x)) -> s(s(double(x)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
plus(s(x), y) -> plus(x, s(y))
plus(s(x), y) -> s(plus(minus(x, y), double(y)))
plus(s(plus(x, y)), z) -> s(plus(plus(x, y), z))
innermost