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

Innermost Termination of R to be shown.



   R
Dependency Pair Analysis



R contains the following Dependency Pairs:

LEQ(s(x), s(y)) -> LEQ(x, y)
-'(s(x), s(y)) -> -'(x, y)
MOD(s(x), s(y)) -> IF(leq(y, x), mod(-(s(x), s(y)), s(y)), s(x))
MOD(s(x), s(y)) -> LEQ(y, x)
MOD(s(x), s(y)) -> MOD(-(s(x), s(y)), s(y))
MOD(s(x), s(y)) -> -'(s(x), s(y))

Furthermore, R contains three SCCs.


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


Dependency Pair:

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


Rules:


leq(0, y) -> true
leq(s(x), 0) -> false
leq(s(x), s(y)) -> leq(x, y)
if(true, x, y) -> x
if(false, x, y) -> y
-(x, 0) -> x
-(s(x), s(y)) -> -(x, y)
mod(0, y) -> 0
mod(s(x), 0) -> 0
mod(s(x), s(y)) -> if(leq(y, x), mod(-(s(x), s(y)), s(y)), s(x))


Strategy:

innermost




The following dependency pair can be strictly oriented:

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


There are no usable rules for innermost w.r.t. to the AFS that need to be oriented.
Used ordering: Homeomorphic Embedding Order with EMB
resulting in one new DP problem.
Used Argument Filtering System:
LEQ(x1, x2) -> LEQ(x1, x2)
s(x1) -> s(x1)


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


Dependency Pair:


Rules:


leq(0, y) -> true
leq(s(x), 0) -> false
leq(s(x), s(y)) -> leq(x, y)
if(true, x, y) -> x
if(false, x, y) -> y
-(x, 0) -> x
-(s(x), s(y)) -> -(x, y)
mod(0, y) -> 0
mod(s(x), 0) -> 0
mod(s(x), s(y)) -> if(leq(y, x), mod(-(s(x), s(y)), s(y)), s(x))


Strategy:

innermost




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
Rw


Dependency Pair:

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


Rules:


leq(0, y) -> true
leq(s(x), 0) -> false
leq(s(x), s(y)) -> leq(x, y)
if(true, x, y) -> x
if(false, x, y) -> y
-(x, 0) -> x
-(s(x), s(y)) -> -(x, y)
mod(0, y) -> 0
mod(s(x), 0) -> 0
mod(s(x), s(y)) -> if(leq(y, x), mod(-(s(x), s(y)), s(y)), s(x))


Strategy:

innermost




The following dependency pair can be strictly oriented:

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


There are no usable rules for innermost w.r.t. to the AFS that need to be oriented.
Used ordering: Homeomorphic Embedding Order with EMB
resulting in one new DP problem.
Used Argument Filtering System:
-'(x1, x2) -> -'(x1, x2)
s(x1) -> s(x1)


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


Dependency Pair:


Rules:


leq(0, y) -> true
leq(s(x), 0) -> false
leq(s(x), s(y)) -> leq(x, y)
if(true, x, y) -> x
if(false, x, y) -> y
-(x, 0) -> x
-(s(x), s(y)) -> -(x, y)
mod(0, y) -> 0
mod(s(x), 0) -> 0
mod(s(x), s(y)) -> if(leq(y, x), mod(-(s(x), s(y)), s(y)), s(x))


Strategy:

innermost




Using the Dependency Graph resulted in no new DP problems.


   R
DPs
       →DP Problem 1
AFS
       →DP Problem 2
AFS
       →DP Problem 3
Rewriting Transformation


Dependency Pair:

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


Rules:


leq(0, y) -> true
leq(s(x), 0) -> false
leq(s(x), s(y)) -> leq(x, y)
if(true, x, y) -> x
if(false, x, y) -> y
-(x, 0) -> x
-(s(x), s(y)) -> -(x, y)
mod(0, y) -> 0
mod(s(x), 0) -> 0
mod(s(x), s(y)) -> if(leq(y, x), mod(-(s(x), s(y)), s(y)), s(x))


Strategy:

innermost




On this DP problem, a Rewriting SCC transformation can be performed.
As a result of transforming the rule

MOD(s(x), s(y)) -> MOD(-(s(x), s(y)), s(y))
one new Dependency Pair is created:

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

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
AFS
       →DP Problem 2
AFS
       →DP Problem 3
Rw
           →DP Problem 6
Argument Filtering and Ordering


Dependency Pair:

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


Rules:


leq(0, y) -> true
leq(s(x), 0) -> false
leq(s(x), s(y)) -> leq(x, y)
if(true, x, y) -> x
if(false, x, y) -> y
-(x, 0) -> x
-(s(x), s(y)) -> -(x, y)
mod(0, y) -> 0
mod(s(x), 0) -> 0
mod(s(x), s(y)) -> if(leq(y, x), mod(-(s(x), s(y)), s(y)), s(x))


Strategy:

innermost




The following dependency pair can be strictly oriented:

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


The following usable rules for innermost w.r.t. to the AFS can be oriented:

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


Used ordering: Homeomorphic Embedding Order with EMB
resulting in one new DP problem.
Used Argument Filtering System:
MOD(x1, x2) -> MOD(x1, x2)
s(x1) -> s(x1)
-(x1, x2) -> x1


   R
DPs
       →DP Problem 1
AFS
       →DP Problem 2
AFS
       →DP Problem 3
Rw
           →DP Problem 6
AFS
             ...
               →DP Problem 7
Dependency Graph


Dependency Pair:


Rules:


leq(0, y) -> true
leq(s(x), 0) -> false
leq(s(x), s(y)) -> leq(x, y)
if(true, x, y) -> x
if(false, x, y) -> y
-(x, 0) -> x
-(s(x), s(y)) -> -(x, y)
mod(0, y) -> 0
mod(s(x), 0) -> 0
mod(s(x), s(y)) -> if(leq(y, x), mod(-(s(x), s(y)), s(y)), s(x))


Strategy:

innermost




Using the Dependency Graph resulted in no new DP problems.

Innermost Termination of R successfully shown.
Duration:
0:00 minutes