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

Termination of R to be shown. 



   R
     ↳Dependency Pair Analysis



R contains the following Dependency Pairs:

APP'(app'(minus, app'(s, x)), app'(s, y)) -> APP'(app'(minus, x), y)
APP'(app'(minus, app'(s, x)), app'(s, y)) -> APP'(minus, x)
APP'(app'(minus, app'(app'(minus, x), y)), z) -> APP'(app'(minus, x), app'(app'(plus, y), z))
APP'(app'(minus, app'(app'(minus, x), y)), z) -> APP'(app'(plus, y), z)
APP'(app'(minus, app'(app'(minus, x), y)), z) -> APP'(plus, y)
APP'(app'(quot, app'(s, x)), app'(s, y)) -> APP'(s, app'(app'(quot, app'(app'(minus, x), y)), app'(s, y)))
APP'(app'(quot, app'(s, x)), app'(s, y)) -> APP'(app'(quot, app'(app'(minus, x), y)), app'(s, y))
APP'(app'(quot, app'(s, x)), app'(s, y)) -> APP'(quot, app'(app'(minus, x), y))
APP'(app'(quot, app'(s, x)), app'(s, y)) -> APP'(app'(minus, x), y)
APP'(app'(quot, app'(s, x)), app'(s, y)) -> APP'(minus, x)
APP'(app'(plus, app'(s, x)), y) -> APP'(s, app'(app'(plus, x), y))
APP'(app'(plus, app'(s, x)), y) -> APP'(app'(plus, x), y)
APP'(app'(plus, app'(s, x)), y) -> APP'(plus, x)
APP'(app'(app, app'(app'(cons, x), l)), k) -> APP'(app'(cons, x), app'(app'(app, l), k))
APP'(app'(app, app'(app'(cons, x), l)), k) -> APP'(app'(app, l), k)
APP'(app'(app, app'(app'(cons, x), l)), k) -> APP'(app, l)
APP'(sum, app'(app'(cons, x), app'(app'(cons, y), l))) -> APP'(sum, app'(app'(cons, app'(app'(plus, x), y)), l))
APP'(sum, app'(app'(cons, x), app'(app'(cons, y), l))) -> APP'(app'(cons, app'(app'(plus, x), y)), l)
APP'(sum, app'(app'(cons, x), app'(app'(cons, y), l))) -> APP'(cons, app'(app'(plus, x), y))
APP'(sum, app'(app'(cons, x), app'(app'(cons, y), l))) -> APP'(app'(plus, x), y)
APP'(sum, app'(app'(cons, x), app'(app'(cons, y), l))) -> APP'(plus, x)
APP'(sum, app'(app'(app, l), app'(app'(cons, x), app'(app'(cons, y), k)))) -> APP'(sum, app'(app'(app, l), app'(sum, app'(app'(cons, x), app'(app'(cons, y), k)))))
APP'(sum, app'(app'(app, l), app'(app'(cons, x), app'(app'(cons, y), k)))) -> APP'(app'(app, l), app'(sum, app'(app'(cons, x), app'(app'(cons, y), k))))
APP'(sum, app'(app'(app, l), app'(app'(cons, x), app'(app'(cons, y), k)))) -> APP'(sum, app'(app'(cons, x), app'(app'(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:

APP'(app'(plus, app'(s, x)), y) -> APP'(app'(plus, x), y)


Rules:


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





The original DP problem is in applicative form. Its DPs and usable rules are the following.

APP'(app'(plus, app'(s, x)), y) -> APP'(app'(plus, x), y)

none


It is proper and hence, it can be A-transformed which results in the DP problem

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

none


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'(app'(app, app'(app'(cons, x), l)), k) -> APP'(app'(app, l), k)


Rules:


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





The original DP problem is in applicative form. Its DPs and usable rules are the following.

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

none


It is proper and hence, it can be A-transformed which results in the DP problem

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

none


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:

APP'(app'(minus, app'(app'(minus, x), y)), z) -> APP'(app'(minus, x), app'(app'(plus, y), z))
APP'(app'(minus, app'(s, x)), app'(s, y)) -> APP'(app'(minus, x), y)


Rules:


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





The original DP problem is in applicative form. Its DPs and usable rules are the following.

APP'(app'(minus, app'(app'(minus, x), y)), z) -> APP'(app'(minus, x), app'(app'(plus, y), z))
APP'(app'(minus, app'(s, x)), app'(s, y)) -> APP'(app'(minus, x), y)


app'(app'(plus, 0), y) -> y
app'(app'(plus, app'(s, x)), y) -> app'(s, app'(app'(plus, x), y))


It is proper and hence, it can be A-transformed which results in the DP problem

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


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


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):
{1, 2} , {1, 2}
1>1
{1, 2} , {1, 2}
1>1
2>2

which lead(s) to this/these maximal multigraph(s):
{1, 2} , {1, 2}
1>1
{1, 2} , {1, 2}
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:
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:

APP'(sum, app'(app'(cons, x), app'(app'(cons, y), l))) -> APP'(sum, app'(app'(cons, app'(app'(plus, x), y)), l))


Rules:


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





The original DP problem is in applicative form. Its DPs and usable rules are the following.

APP'(sum, app'(app'(cons, x), app'(app'(cons, y), l))) -> APP'(sum, app'(app'(cons, app'(app'(plus, x), y)), l))


app'(app'(plus, 0), y) -> y
app'(app'(plus, app'(s, x)), y) -> app'(s, app'(app'(plus, x), y))


It is proper and hence, it can be A-transformed which results in the DP problem

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


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.
Note that we keep the A-transformed DP problem as result of this processor.



   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:

APP'(app'(quot, app'(s, x)), app'(s, y)) -> APP'(app'(quot, app'(app'(minus, x), y)), app'(s, y))


Rules:


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





The original DP problem is in applicative form. Its DPs and usable rules are the following.

APP'(app'(quot, app'(s, x)), app'(s, y)) -> APP'(app'(quot, app'(app'(minus, x), y)), app'(s, y))


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


It is proper and hence, it can be A-transformed which results in the DP problem

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


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))


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

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

This corresponds to the following dependency pair in applicative form:

APP'(app'(quot, app'(s, x)), app'(s, y)) -> APP'(app'(quot, app'(app'(minus, x), y)), app'(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:


app'(app'(minus, x), 0) -> x
app'(app'(minus, app'(s, x)), app'(s, y)) -> app'(app'(minus, x), y)
app'(app'(minus, app'(app'(minus, x), y)), z) -> app'(app'(minus, x), app'(app'(plus, y), z))
app'(app'(quot, 0), app'(s, y)) -> 0
app'(app'(quot, app'(s, x)), app'(s, y)) -> app'(s, app'(app'(quot, app'(app'(minus, x), y)), app'(s, y)))
app'(app'(plus, 0), y) -> y
app'(app'(plus, app'(s, x)), y) -> app'(s, app'(app'(plus, x), y))
app'(app'(app, nil), k) -> k
app'(app'(app, l), nil) -> l
app'(app'(app, app'(app'(cons, x), l)), k) -> app'(app'(cons, x), app'(app'(app, l), k))
app'(sum, app'(app'(cons, x), nil)) -> app'(app'(cons, x), nil)
app'(sum, app'(app'(cons, x), app'(app'(cons, y), l))) -> app'(sum, app'(app'(cons, app'(app'(plus, x), y)), l))
app'(sum, app'(app'(app, l), app'(app'(cons, x), app'(app'(cons, y), k)))) -> app'(sum, app'(app'(app, l), app'(sum, app'(app'(cons, x), app'(app'(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:

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


Rules:


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





The original DP problem is in applicative form. Its DPs and usable rules are the following.

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


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


It is proper and hence, it can be A-transformed which results in the DP problem

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


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.
Note that we keep the A-transformed DP problem as result of this processor.



   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:01 minutes