Term Rewriting System R:
[x, y]
-(x, 0) -> x
-(0, s(y)) -> 0
-(s(x), s(y)) -> -(x, y)
lt(x, 0) -> false
lt(0, s(y)) -> true
lt(s(x), s(y)) -> lt(x, y)
if(true, x, y) -> x
if(false, x, y) -> y
div(x, 0) -> 0
div(0, y) -> 0
div(s(x), s(y)) -> if(lt(x, y), 0, s(div(-(x, y), s(y))))

Termination of R to be shown.

`   R`
`     ↳Dependency Pair Analysis`

R contains the following Dependency Pairs:

-'(s(x), s(y)) -> -'(x, y)
LT(s(x), s(y)) -> LT(x, y)
DIV(s(x), s(y)) -> IF(lt(x, y), 0, s(div(-(x, y), s(y))))
DIV(s(x), s(y)) -> LT(x, y)
DIV(s(x), s(y)) -> DIV(-(x, y), s(y))
DIV(s(x), s(y)) -> -'(x, y)

Furthermore, R contains three SCCs.

`   R`
`     ↳DPs`
`       →DP Problem 1`
`         ↳Argument Filtering and Ordering`
`       →DP Problem 2`
`         ↳AFS`
`       →DP Problem 3`
`         ↳AFS`

Dependency Pair:

-'(s(x), s(y)) -> -'(x, y)

Rules:

-(x, 0) -> x
-(0, s(y)) -> 0
-(s(x), s(y)) -> -(x, y)
lt(x, 0) -> false
lt(0, s(y)) -> true
lt(s(x), s(y)) -> lt(x, y)
if(true, x, y) -> x
if(false, x, y) -> y
div(x, 0) -> 0
div(0, y) -> 0
div(s(x), s(y)) -> if(lt(x, y), 0, s(div(-(x, y), s(y))))

The following dependency pair can be strictly oriented:

-'(s(x), s(y)) -> -'(x, y)

The following rules can be oriented:

-(x, 0) -> x
-(0, s(y)) -> 0
-(s(x), s(y)) -> -(x, y)
lt(x, 0) -> false
lt(0, s(y)) -> true
lt(s(x), s(y)) -> lt(x, y)
if(true, x, y) -> x
if(false, x, y) -> y
div(x, 0) -> 0
div(0, y) -> 0
div(s(x), s(y)) -> if(lt(x, y), 0, s(div(-(x, y), s(y))))

Used ordering: Polynomial ordering with Polynomial interpretation:
 POL(if(x1, x2)) =  x1 + x2 POL(-'(x1, x2)) =  1 + x1 + x2 POL(0) =  0 POL(false) =  0 POL(lt(x1, x2)) =  x1 + x2 POL(true) =  0 POL(s(x1)) =  1 + x1 POL(div(x1, x2)) =  x1 + x2

resulting in one new DP problem.
Used Argument Filtering System:
-'(x1, x2) -> -'(x1, x2)
s(x1) -> s(x1)
-(x1, x2) -> x1
lt(x1, x2) -> lt(x1, x2)
if(x1, x2, x3) -> if(x2, x3)
div(x1, x2) -> div(x1, x2)

`   R`
`     ↳DPs`
`       →DP Problem 1`
`         ↳AFS`
`           →DP Problem 4`
`             ↳Dependency Graph`
`       →DP Problem 2`
`         ↳AFS`
`       →DP Problem 3`
`         ↳AFS`

Dependency Pair:

Rules:

-(x, 0) -> x
-(0, s(y)) -> 0
-(s(x), s(y)) -> -(x, y)
lt(x, 0) -> false
lt(0, s(y)) -> true
lt(s(x), s(y)) -> lt(x, y)
if(true, x, y) -> x
if(false, x, y) -> y
div(x, 0) -> 0
div(0, y) -> 0
div(s(x), s(y)) -> if(lt(x, y), 0, s(div(-(x, y), s(y))))

Using the Dependency Graph resulted in no new DP problems.

`   R`
`     ↳DPs`
`       →DP Problem 1`
`         ↳AFS`
`       →DP Problem 2`
`         ↳Argument Filtering and Ordering`
`       →DP Problem 3`
`         ↳AFS`

Dependency Pair:

LT(s(x), s(y)) -> LT(x, y)

Rules:

-(x, 0) -> x
-(0, s(y)) -> 0
-(s(x), s(y)) -> -(x, y)
lt(x, 0) -> false
lt(0, s(y)) -> true
lt(s(x), s(y)) -> lt(x, y)
if(true, x, y) -> x
if(false, x, y) -> y
div(x, 0) -> 0
div(0, y) -> 0
div(s(x), s(y)) -> if(lt(x, y), 0, s(div(-(x, y), s(y))))

The following dependency pair can be strictly oriented:

LT(s(x), s(y)) -> LT(x, y)

The following rules can be oriented:

-(x, 0) -> x
-(0, s(y)) -> 0
-(s(x), s(y)) -> -(x, y)
lt(x, 0) -> false
lt(0, s(y)) -> true
lt(s(x), s(y)) -> lt(x, y)
if(true, x, y) -> x
if(false, x, y) -> y
div(x, 0) -> 0
div(0, y) -> 0
div(s(x), s(y)) -> if(lt(x, y), 0, s(div(-(x, y), s(y))))

Used ordering: Polynomial ordering with Polynomial interpretation:
 POL(if(x1, x2)) =  x1 + x2 POL(0) =  0 POL(false) =  0 POL(LT(x1, x2)) =  1 + x1 + x2 POL(lt(x1, x2)) =  x1 + x2 POL(true) =  0 POL(s(x1)) =  1 + x1 POL(div(x1, x2)) =  x1 + x2

resulting in one new DP problem.
Used Argument Filtering System:
LT(x1, x2) -> LT(x1, x2)
s(x1) -> s(x1)
-(x1, x2) -> x1
lt(x1, x2) -> lt(x1, x2)
if(x1, x2, x3) -> if(x2, x3)
div(x1, x2) -> div(x1, x2)

`   R`
`     ↳DPs`
`       →DP Problem 1`
`         ↳AFS`
`       →DP Problem 2`
`         ↳AFS`
`           →DP Problem 5`
`             ↳Dependency Graph`
`       →DP Problem 3`
`         ↳AFS`

Dependency Pair:

Rules:

-(x, 0) -> x
-(0, s(y)) -> 0
-(s(x), s(y)) -> -(x, y)
lt(x, 0) -> false
lt(0, s(y)) -> true
lt(s(x), s(y)) -> lt(x, y)
if(true, x, y) -> x
if(false, x, y) -> y
div(x, 0) -> 0
div(0, y) -> 0
div(s(x), s(y)) -> if(lt(x, y), 0, s(div(-(x, y), s(y))))

Using the Dependency Graph resulted in no new DP problems.

`   R`
`     ↳DPs`
`       →DP Problem 1`
`         ↳AFS`
`       →DP Problem 2`
`         ↳AFS`
`       →DP Problem 3`
`         ↳Argument Filtering and Ordering`

Dependency Pair:

DIV(s(x), s(y)) -> DIV(-(x, y), s(y))

Rules:

-(x, 0) -> x
-(0, s(y)) -> 0
-(s(x), s(y)) -> -(x, y)
lt(x, 0) -> false
lt(0, s(y)) -> true
lt(s(x), s(y)) -> lt(x, y)
if(true, x, y) -> x
if(false, x, y) -> y
div(x, 0) -> 0
div(0, y) -> 0
div(s(x), s(y)) -> if(lt(x, y), 0, s(div(-(x, y), s(y))))

The following dependency pair can be strictly oriented:

DIV(s(x), s(y)) -> DIV(-(x, y), s(y))

The following rules can be oriented:

-(x, 0) -> x
-(0, s(y)) -> 0
-(s(x), s(y)) -> -(x, y)
lt(x, 0) -> false
lt(0, s(y)) -> true
lt(s(x), s(y)) -> lt(x, y)
if(true, x, y) -> x
if(false, x, y) -> y
div(x, 0) -> 0
div(0, y) -> 0
div(s(x), s(y)) -> if(lt(x, y), 0, s(div(-(x, y), s(y))))

Used ordering: Polynomial ordering with Polynomial interpretation:
 POL(if(x1, x2)) =  x1 + x2 POL(0) =  0 POL(false) =  0 POL(DIV(x1, x2)) =  1 + x1 + x2 POL(lt(x1, x2)) =  x1 + x2 POL(true) =  0 POL(s(x1)) =  1 + x1 POL(div(x1, x2)) =  x1 + x2

resulting in one new DP problem.
Used Argument Filtering System:
DIV(x1, x2) -> DIV(x1, x2)
s(x1) -> s(x1)
-(x1, x2) -> x1
lt(x1, x2) -> lt(x1, x2)
if(x1, x2, x3) -> if(x2, x3)
div(x1, x2) -> div(x1, x2)

`   R`
`     ↳DPs`
`       →DP Problem 1`
`         ↳AFS`
`       →DP Problem 2`
`         ↳AFS`
`       →DP Problem 3`
`         ↳AFS`
`           →DP Problem 6`
`             ↳Dependency Graph`

Dependency Pair:

Rules:

-(x, 0) -> x
-(0, s(y)) -> 0
-(s(x), s(y)) -> -(x, y)
lt(x, 0) -> false
lt(0, s(y)) -> true
lt(s(x), s(y)) -> lt(x, y)
if(true, x, y) -> x
if(false, x, y) -> y
div(x, 0) -> 0
div(0, y) -> 0
div(s(x), s(y)) -> if(lt(x, y), 0, s(div(-(x, y), s(y))))

Using the Dependency Graph resulted in no new DP problems.

Termination of R successfully shown.
Duration:
0:01 minutes