Term Rewriting System R:
[x, y, z, k, l]
minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))

Termination of R to be shown. 



   R
     ↳Dependency Pair Analysis



R contains the following Dependency Pairs:

MINUS(s(x), s(y)) -> MINUS(x, y)
MINUS(minus(x, y), z) -> MINUS(x, plus(y, z))
MINUS(minus(x, y), z) -> PLUS(y, z)
QUOT(s(x), s(y)) -> QUOT(minus(x, y), s(y))
QUOT(s(x), s(y)) -> MINUS(x, y)
PLUS(s(x), y) -> PLUS(x, y)
APP(cons(x, l), k) -> APP(l, k)
SUM(cons(x, cons(y, l))) -> SUM(cons(plus(x, y), l))
SUM(cons(x, cons(y, l))) -> PLUS(x, y)
SUM(app(l, cons(x, cons(y, k)))) -> SUM(app(l, sum(cons(x, cons(y, k)))))
SUM(app(l, cons(x, cons(y, k)))) -> APP(l, sum(cons(x, cons(y, k))))
SUM(app(l, cons(x, cons(y, k)))) -> SUM(cons(x, cons(y, k)))

Furthermore, R contains six SCCs. 


   R
     ↳DPs
       →DP Problem 1
         ↳Size-Change Principle
       →DP Problem 2
         ↳SCP
       →DP Problem 3
         ↳SCP
       →DP Problem 4
         ↳MRR
       →DP Problem 5
         ↳Neg POLO
       →DP Problem 6
         ↳MRR


Dependency Pair:

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


Rules:


minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))





We number the DPs as follows:
  1. PLUS(s(x), y) -> PLUS(x, y)
and get the following Size-Change Graph(s):
{1} , {1}
1>1
2=2

which lead(s) to this/these maximal multigraph(s):
{1} , {1}
1>1
2=2

DP: empty set
Oriented Rules: none

We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial

with Argument Filtering System:
s(x1) -> s(x1)

We obtain no new DP problems. 


   R
     ↳DPs
       →DP Problem 1
         ↳SCP
       →DP Problem 2
         ↳Size-Change Principle
       →DP Problem 3
         ↳SCP
       →DP Problem 4
         ↳MRR
       →DP Problem 5
         ↳Neg POLO
       →DP Problem 6
         ↳MRR


Dependency Pair:

APP(cons(x, l), k) -> APP(l, k)


Rules:


minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))





We number the DPs as follows:
  1. APP(cons(x, l), k) -> APP(l, k)
and get the following Size-Change Graph(s):
{1} , {1}
1>1
2=2

which lead(s) to this/these maximal multigraph(s):
{1} , {1}
1>1
2=2

DP: empty set
Oriented Rules: none

We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial

with Argument Filtering System:
cons(x1, x2) -> cons(x1, x2)

We obtain no new DP problems. 


   R
     ↳DPs
       →DP Problem 1
         ↳SCP
       →DP Problem 2
         ↳SCP
       →DP Problem 3
         ↳Size-Change Principle
       →DP Problem 4
         ↳MRR
       →DP Problem 5
         ↳Neg POLO
       →DP Problem 6
         ↳MRR


Dependency Pairs:

MINUS(minus(x, y), z) -> MINUS(x, plus(y, z))
MINUS(s(x), s(y)) -> MINUS(x, y)


Rules:


minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))





We number the DPs as follows:
  1. MINUS(minus(x, y), z) -> MINUS(x, plus(y, z))
  2. MINUS(s(x), s(y)) -> MINUS(x, y)
and get the following Size-Change Graph(s):
{2, 1} , {2, 1}
1>1
{2, 1} , {2, 1}
1>1
2>2

which lead(s) to this/these maximal multigraph(s):
{2, 1} , {2, 1}
1>1
2>2
{2, 1} , {2, 1}
1>1

DP: empty set
Oriented Rules: none

We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial

with Argument Filtering System:
minus(x1, x2) -> minus(x1, x2)
s(x1) -> s(x1)

We obtain no new DP problems. 


   R
     ↳DPs
       →DP Problem 1
         ↳SCP
       →DP Problem 2
         ↳SCP
       →DP Problem 3
         ↳SCP
       →DP Problem 4
         ↳Modular Removal of Rules
       →DP Problem 5
         ↳Neg POLO
       →DP Problem 6
         ↳MRR


Dependency Pair:

SUM(cons(x, cons(y, l))) -> SUM(cons(plus(x, y), l))


Rules:


minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))





We have the following set of usable rules:

plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
Polynomial interpretation:
  POL(plus(x1, x2))=  x1 + x2  
  POL(SUM(x1))=  1 + x1  
  POL(0)=  1  
  POL(cons(x1, x2))=  x1 + x2  
  POL(s(x1))=  x1  

We have the following set D of usable symbols: {plus, SUM, cons, s}
No Dependency Pairs can be deleted.
The following rules can be deleted as they contain symbols in their lhs which do not occur in D:

plus(0, y) -> y
11 non usable rules have been deleted.

The result of this processor delivers one new DP problem.



   R
     ↳DPs
       →DP Problem 1
         ↳SCP
       →DP Problem 2
         ↳SCP
       →DP Problem 3
         ↳SCP
       →DP Problem 4
         ↳MRR
           →DP Problem 7
             ↳Modular Removal of Rules
       →DP Problem 5
         ↳Neg POLO
       →DP Problem 6
         ↳MRR


Dependency Pair:

SUM(cons(x, cons(y, l))) -> SUM(cons(plus(x, y), l))


Rule:


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





We have the following set of usable rules:

plus(s(x), y) -> s(plus(x, y))
To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
Polynomial interpretation:
  POL(plus(x1, x2))=  x1 + x2  
  POL(SUM(x1))=  1 + x1  
  POL(cons(x1, x2))=  1 + x1 + x2  
  POL(s(x1))=  x1  

We have the following set D of usable symbols: {plus, SUM, cons, s}
The following Dependency Pairs can be deleted as the lhs is strictly greater than the corresponding rhs:

SUM(cons(x, cons(y, l))) -> SUM(cons(plus(x, y), l))

No Rules can be deleted.

After the removal, there are no SCCs in the dependency graph which results in no DP problems which have to be solved. 



   R
     ↳DPs
       →DP Problem 1
         ↳SCP
       →DP Problem 2
         ↳SCP
       →DP Problem 3
         ↳SCP
       →DP Problem 4
         ↳MRR
       →DP Problem 5
         ↳Negative Polynomial Order
       →DP Problem 6
         ↳MRR


Dependency Pair:

QUOT(s(x), s(y)) -> QUOT(minus(x, y), s(y))


Rules:


minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))





The following Dependency Pair can be strictly oriented using the given order.

QUOT(s(x), s(y)) -> QUOT(minus(x, y), s(y))


Moreover, the following usable rules (regarding the implicit AFS) are oriented.

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))


Used ordering:
Polynomial Order with Interpretation:

POL( QUOT(x1, x2) ) = x1

POL( s(x1) ) = x1 + 1

POL( minus(x1, x2) ) = x1

POL( plus(x1, x2) ) = x1 + x2


This results in one new DP problem. 


   R
     ↳DPs
       →DP Problem 1
         ↳SCP
       →DP Problem 2
         ↳SCP
       →DP Problem 3
         ↳SCP
       →DP Problem 4
         ↳MRR
       →DP Problem 5
         ↳Neg POLO
           →DP Problem 8
             ↳Dependency Graph
       →DP Problem 6
         ↳MRR


Dependency Pair:


Rules:


minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))





Using the Dependency Graph resulted in no new DP problems.


   R
     ↳DPs
       →DP Problem 1
         ↳SCP
       →DP Problem 2
         ↳SCP
       →DP Problem 3
         ↳SCP
       →DP Problem 4
         ↳MRR
       →DP Problem 5
         ↳Neg POLO
       →DP Problem 6
         ↳Modular Removal of Rules


Dependency Pair:

SUM(app(l, cons(x, cons(y, k)))) -> SUM(app(l, sum(cons(x, cons(y, k)))))


Rules:


minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))





We have the following set of usable rules:

app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(cons(x, nil)) -> cons(x, nil)
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
Polynomial interpretation:
  POL(plus(x1, x2))=  x1 + x2  
  POL(SUM(x1))=  1 + x1  
  POL(0)=  1  
  POL(cons(x1, x2))=  x1 + x2  
  POL(nil)=  0  
  POL(sum(x1))=  x1  
  POL(s(x1))=  x1  
  POL(app(x1, x2))=  x1 + x2  

We have the following set D of usable symbols: {plus, SUM, cons, nil, s, sum, app}
No Dependency Pairs can be deleted.
The following rules can be deleted as they contain symbols in their lhs which do not occur in D:

plus(0, y) -> y
6 non usable rules have been deleted.

The result of this processor delivers one new DP problem.



   R
     ↳DPs
       →DP Problem 1
         ↳SCP
       →DP Problem 2
         ↳SCP
       →DP Problem 3
         ↳SCP
       →DP Problem 4
         ↳MRR
       →DP Problem 5
         ↳Neg POLO
       →DP Problem 6
         ↳MRR
           →DP Problem 9
             ↳Modular Removal of Rules


Dependency Pair:

SUM(app(l, cons(x, cons(y, k)))) -> SUM(app(l, sum(cons(x, cons(y, k)))))


Rules:


app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(cons(x, nil)) -> cons(x, nil)
plus(s(x), y) -> s(plus(x, y))





We have the following set of usable rules:

app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(cons(x, nil)) -> cons(x, nil)
plus(s(x), y) -> s(plus(x, y))
To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
Polynomial interpretation:
  POL(plus(x1, x2))=  x1 + x2  
  POL(SUM(x1))=  1 + x1  
  POL(cons(x1, x2))=  x1 + x2  
  POL(nil)=  0  
  POL(sum(x1))=  x1  
  POL(s(x1))=  x1  
  POL(app(x1, x2))=  1 + x1 + x2  

We have the following set D of usable symbols: {plus, SUM, cons, nil, s, sum, app}
No Dependency Pairs can be deleted.
The following rules can be deleted as the lhs is strictly greater than the corresponding rhs:

app(nil, k) -> k
app(l, nil) -> l


The result of this processor delivers one new DP problem.



   R
     ↳DPs
       →DP Problem 1
         ↳SCP
       →DP Problem 2
         ↳SCP
       →DP Problem 3
         ↳SCP
       →DP Problem 4
         ↳MRR
       →DP Problem 5
         ↳Neg POLO
       →DP Problem 6
         ↳MRR
           →DP Problem 9
             ↳MRR
             ...
               →DP Problem 10
                 ↳Modular Removal of Rules


Dependency Pair:

SUM(app(l, cons(x, cons(y, k)))) -> SUM(app(l, sum(cons(x, cons(y, k)))))


Rules:


app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(cons(x, nil)) -> cons(x, nil)
plus(s(x), y) -> s(plus(x, y))





We have the following set of usable rules:

app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(cons(x, nil)) -> cons(x, nil)
plus(s(x), y) -> s(plus(x, y))
To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
Polynomial interpretation:
  POL(plus(x1, x2))=  x1 + x2  
  POL(SUM(x1))=  1 + x1  
  POL(cons(x1, x2))=  1 + x1 + x2  
  POL(nil)=  0  
  POL(sum(x1))=  x1  
  POL(s(x1))=  x1  
  POL(app(x1, x2))=  x1 + x2  

We have the following set D of usable symbols: {plus, SUM, cons, nil, s, sum, app}
No Dependency Pairs can be deleted.
The following rules can be deleted as the lhs is strictly greater than the corresponding rhs:

sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))


The result of this processor delivers one new DP problem.



   R
     ↳DPs
       →DP Problem 1
         ↳SCP
       →DP Problem 2
         ↳SCP
       →DP Problem 3
         ↳SCP
       →DP Problem 4
         ↳MRR
       →DP Problem 5
         ↳Neg POLO
       →DP Problem 6
         ↳MRR
           →DP Problem 9
             ↳MRR
             ...
               →DP Problem 11
                 ↳Modular Removal of Rules


Dependency Pair:

SUM(app(l, cons(x, cons(y, k)))) -> SUM(app(l, sum(cons(x, cons(y, k)))))


Rules:


app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, nil)) -> cons(x, nil)
plus(s(x), y) -> s(plus(x, y))





We have the following set of usable rules:

app(cons(x, l), k) -> cons(x, app(l, k))
To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
Polynomial interpretation:
  POL(SUM(x1))=  1 + x1  
  POL(cons(x1, x2))=  x1 + x2  
  POL(sum(x1))=  x1  
  POL(app(x1, x2))=  x1 + x2  

We have the following set D of usable symbols: {SUM, cons, sum, app}
No Dependency Pairs can be deleted.
2 non usable rules have been deleted.

The result of this processor delivers one new DP problem.



   R
     ↳DPs
       →DP Problem 1
         ↳SCP
       →DP Problem 2
         ↳SCP
       →DP Problem 3
         ↳SCP
       →DP Problem 4
         ↳MRR
       →DP Problem 5
         ↳Neg POLO
       →DP Problem 6
         ↳MRR
           →DP Problem 9
             ↳MRR
             ...
               →DP Problem 12
                 ↳Narrowing Transformation


Dependency Pair:

SUM(app(l, cons(x, cons(y, k)))) -> SUM(app(l, sum(cons(x, cons(y, k)))))


Rule:


app(cons(x, l), k) -> cons(x, app(l, k))





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

SUM(app(l, cons(x, cons(y, k)))) -> SUM(app(l, sum(cons(x, cons(y, k)))))
one new Dependency Pair is created:

SUM(app(cons(x'', l''), cons(x0, cons(y', k'')))) -> SUM(cons(x'', app(l'', sum(cons(x0, cons(y', k''))))))

The transformation is resulting in no new DP problems.


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