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

Innermost 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
Usable Rules (Innermost)
       →DP Problem 2
UsableRules
       →DP Problem 3
UsableRules
       →DP Problem 4
UsableRules
       →DP Problem 5
UsableRules
       →DP Problem 6
UsableRules


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


Strategy:

innermost




As we are in the innermost case, we can delete all 13 non-usable-rules.


   R
DPs
       →DP Problem 1
UsableRules
           →DP Problem 7
Size-Change Principle
       →DP Problem 2
UsableRules
       →DP Problem 3
UsableRules
       →DP Problem 4
UsableRules
       →DP Problem 5
UsableRules
       →DP Problem 6
UsableRules


Dependency Pair:

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


Rule:

none


Strategy:

innermost




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
UsableRules
       →DP Problem 2
Usable Rules (Innermost)
       →DP Problem 3
UsableRules
       →DP Problem 4
UsableRules
       →DP Problem 5
UsableRules
       →DP Problem 6
UsableRules


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


Strategy:

innermost




As we are in the innermost case, we can delete all 13 non-usable-rules.


   R
DPs
       →DP Problem 1
UsableRules
       →DP Problem 2
UsableRules
           →DP Problem 8
Size-Change Principle
       →DP Problem 3
UsableRules
       →DP Problem 4
UsableRules
       →DP Problem 5
UsableRules
       →DP Problem 6
UsableRules


Dependency Pair:

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


Rule:

none


Strategy:

innermost




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
UsableRules
       →DP Problem 2
UsableRules
       →DP Problem 3
Usable Rules (Innermost)
       →DP Problem 4
UsableRules
       →DP Problem 5
UsableRules
       →DP Problem 6
UsableRules


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


Strategy:

innermost




As we are in the innermost case, we can delete all 11 non-usable-rules.


   R
DPs
       →DP Problem 1
UsableRules
       →DP Problem 2
UsableRules
       →DP Problem 3
UsableRules
           →DP Problem 9
Size-Change Principle
       →DP Problem 4
UsableRules
       →DP Problem 5
UsableRules
       →DP Problem 6
UsableRules


Dependency Pairs:

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


Rules:


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


Strategy:

innermost




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

which lead(s) to this/these maximal multigraph(s):
{2} , {2}
1>1
2>2
{2} , {1}
1>1
{1} , {2}
1>1
{2} , {2}
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
UsableRules
       →DP Problem 2
UsableRules
       →DP Problem 3
UsableRules
       →DP Problem 4
Usable Rules (Innermost)
       →DP Problem 5
UsableRules
       →DP Problem 6
UsableRules


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


Strategy:

innermost




As we are in the innermost case, we can delete all 11 non-usable-rules.


   R
DPs
       →DP Problem 1
UsableRules
       →DP Problem 2
UsableRules
       →DP Problem 3
UsableRules
       →DP Problem 4
UsableRules
           →DP Problem 10
Modular Removal of Rules
       →DP Problem 5
UsableRules
       →DP Problem 6
UsableRules


Dependency Pair:

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


Rules:


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


Strategy:

innermost




We have the following set of usable rules:

plus(s(x), y) -> s(plus(x, y))
plus(0, y) -> 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


The result of this processor delivers one new DP problem.



   R
DPs
       →DP Problem 1
UsableRules
       →DP Problem 2
UsableRules
       →DP Problem 3
UsableRules
       →DP Problem 4
UsableRules
           →DP Problem 10
MRR
             ...
               →DP Problem 11
Modular Removal of Rules
       →DP Problem 5
UsableRules
       →DP Problem 6
UsableRules


Dependency Pair:

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


Rule:


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


Strategy:

innermost




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
UsableRules
       →DP Problem 2
UsableRules
       →DP Problem 3
UsableRules
       →DP Problem 4
UsableRules
       →DP Problem 5
Usable Rules (Innermost)
       →DP Problem 6
UsableRules


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


Strategy:

innermost




As we are in the innermost case, we can delete all 8 non-usable-rules.


   R
DPs
       →DP Problem 1
UsableRules
       →DP Problem 2
UsableRules
       →DP Problem 3
UsableRules
       →DP Problem 4
UsableRules
       →DP Problem 5
UsableRules
           →DP Problem 12
Negative Polynomial Order
       →DP Problem 6
UsableRules


Dependency Pair:

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


Rules:


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


Strategy:

innermost




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(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
minus(x, 0) -> x
plus(s(x), y) -> s(plus(x, y))
plus(0, y) -> 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
UsableRules
       →DP Problem 2
UsableRules
       →DP Problem 3
UsableRules
       →DP Problem 4
UsableRules
       →DP Problem 5
UsableRules
           →DP Problem 12
Neg POLO
             ...
               →DP Problem 13
Dependency Graph
       →DP Problem 6
UsableRules


Dependency Pair:


Rules:


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


Strategy:

innermost




Using the Dependency Graph resulted in no new DP problems.


   R
DPs
       →DP Problem 1
UsableRules
       →DP Problem 2
UsableRules
       →DP Problem 3
UsableRules
       →DP Problem 4
UsableRules
       →DP Problem 5
UsableRules
       →DP Problem 6
Usable Rules (Innermost)


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


Strategy:

innermost




As we are in the innermost case, we can delete all 8 non-usable-rules.


   R
DPs
       →DP Problem 1
UsableRules
       →DP Problem 2
UsableRules
       →DP Problem 3
UsableRules
       →DP Problem 4
UsableRules
       →DP Problem 5
UsableRules
       →DP Problem 6
UsableRules
           →DP Problem 14
Rewriting Transformation


Dependency Pair:

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


Rules:


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


Strategy:

innermost




On this DP problem, a Rewriting 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(l, cons(x, cons(y, k)))) -> SUM(app(l, sum(cons(plus(x, y), k))))

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
UsableRules
       →DP Problem 2
UsableRules
       →DP Problem 3
UsableRules
       →DP Problem 4
UsableRules
       →DP Problem 5
UsableRules
       →DP Problem 6
UsableRules
           →DP Problem 14
Rw
             ...
               →DP Problem 15
Modular Removal of Rules


Dependency Pair:

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


Rules:


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


Strategy:

innermost




We have the following set of usable rules:

app(l, nil) -> l
sum(cons(x, nil)) -> cons(x, nil)
plus(s(x), y) -> s(plus(x, y))
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
plus(0, y) -> 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))=  1 + x1 + x2  

We have the following set D of usable symbols: {plus, SUM, cons, nil, sum, s, 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
The following rules can be deleted as the lhs is strictly greater than the corresponding rhs:

app(l, nil) -> l


The result of this processor delivers one new DP problem.



   R
DPs
       →DP Problem 1
UsableRules
       →DP Problem 2
UsableRules
       →DP Problem 3
UsableRules
       →DP Problem 4
UsableRules
       →DP Problem 5
UsableRules
       →DP Problem 6
UsableRules
           →DP Problem 14
Rw
             ...
               →DP Problem 16
Modular Removal of Rules


Dependency Pair:

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


Rules:


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


Strategy:

innermost




We have the following set of usable rules:

sum(cons(x, nil)) -> cons(x, nil)
plus(s(x), y) -> s(plus(x, y))
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
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))=  1 + x1 + x2  

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

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

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.


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