Term Rewriting System R:
[N, X, Y]
terms(N) -> cons(recip(sqr(N)))
sqr(0) -> 0
sqr(s(X)) -> s(add(sqr(X), dbl(X)))
dbl(0) -> 0
dbl(s(X)) -> s(s(dbl(X)))
add(0, X) -> X
add(s(X), Y) -> s(add(X, Y))
first(0, X) -> nil
first(s(X), cons(Y)) -> cons(Y)

Termination of R to be shown.



   R
Overlay and local confluence Check



The TRS is overlay and locally confluent (all critical pairs are trivially joinable).Hence, we can switch to innermost.


   R
OC
       →TRS2
Dependency Pair Analysis



R contains the following Dependency Pairs:

TERMS(N) -> SQR(N)
SQR(s(X)) -> ADD(sqr(X), dbl(X))
SQR(s(X)) -> SQR(X)
SQR(s(X)) -> DBL(X)
DBL(s(X)) -> DBL(X)
ADD(s(X), Y) -> ADD(X, Y)

Furthermore, R contains three SCCs.


   R
OC
       →TRS2
DPs
           →DP Problem 1
Usable Rules (Innermost)
           →DP Problem 2
UsableRules
           →DP Problem 3
UsableRules


Dependency Pair:

ADD(s(X), Y) -> ADD(X, Y)


Rules:


terms(N) -> cons(recip(sqr(N)))
sqr(0) -> 0
sqr(s(X)) -> s(add(sqr(X), dbl(X)))
dbl(0) -> 0
dbl(s(X)) -> s(s(dbl(X)))
add(0, X) -> X
add(s(X), Y) -> s(add(X, Y))
first(0, X) -> nil
first(s(X), cons(Y)) -> cons(Y)


Strategy:

innermost




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


   R
OC
       →TRS2
DPs
           →DP Problem 1
UsableRules
             ...
               →DP Problem 4
Size-Change Principle
           →DP Problem 2
UsableRules
           →DP Problem 3
UsableRules


Dependency Pair:

ADD(s(X), Y) -> ADD(X, Y)


Rule:

none


Strategy:

innermost




We number the DPs as follows:
  1. ADD(s(X), Y) -> ADD(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
OC
       →TRS2
DPs
           →DP Problem 1
UsableRules
           →DP Problem 2
Usable Rules (Innermost)
           →DP Problem 3
UsableRules


Dependency Pair:

DBL(s(X)) -> DBL(X)


Rules:


terms(N) -> cons(recip(sqr(N)))
sqr(0) -> 0
sqr(s(X)) -> s(add(sqr(X), dbl(X)))
dbl(0) -> 0
dbl(s(X)) -> s(s(dbl(X)))
add(0, X) -> X
add(s(X), Y) -> s(add(X, Y))
first(0, X) -> nil
first(s(X), cons(Y)) -> cons(Y)


Strategy:

innermost




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


   R
OC
       →TRS2
DPs
           →DP Problem 1
UsableRules
           →DP Problem 2
UsableRules
             ...
               →DP Problem 5
Size-Change Principle
           →DP Problem 3
UsableRules


Dependency Pair:

DBL(s(X)) -> DBL(X)


Rule:

none


Strategy:

innermost




We number the DPs as follows:
  1. DBL(s(X)) -> DBL(X)
and get the following Size-Change Graph(s):
{1} , {1}
1>1

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

We obtain no new DP problems.


   R
OC
       →TRS2
DPs
           →DP Problem 1
UsableRules
           →DP Problem 2
UsableRules
           →DP Problem 3
Usable Rules (Innermost)


Dependency Pair:

SQR(s(X)) -> SQR(X)


Rules:


terms(N) -> cons(recip(sqr(N)))
sqr(0) -> 0
sqr(s(X)) -> s(add(sqr(X), dbl(X)))
dbl(0) -> 0
dbl(s(X)) -> s(s(dbl(X)))
add(0, X) -> X
add(s(X), Y) -> s(add(X, Y))
first(0, X) -> nil
first(s(X), cons(Y)) -> cons(Y)


Strategy:

innermost




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


   R
OC
       →TRS2
DPs
           →DP Problem 1
UsableRules
           →DP Problem 2
UsableRules
           →DP Problem 3
UsableRules
             ...
               →DP Problem 6
Size-Change Principle


Dependency Pair:

SQR(s(X)) -> SQR(X)


Rule:

none


Strategy:

innermost




We number the DPs as follows:
  1. SQR(s(X)) -> SQR(X)
and get the following Size-Change Graph(s):
{1} , {1}
1>1

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

We obtain no new DP problems.

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