Term Rewriting System R:
[x, y, z]
cons(x, cons(y, z)) -> big
inf(x) -> cons(x, inf(s(x)))

Termination of R to be shown. 



   R
     ↳Dependency Pair Analysis



R contains the following Dependency Pairs:

INF(x) -> CONS(x, inf(s(x)))
INF(x) -> INF(s(x))

Furthermore, R contains one SCC. 


   R
     ↳DPs
       →DP Problem 1
         ↳Modular Removal of Rules


Dependency Pair:

INF(x) -> INF(s(x))


Rules:


cons(x, cons(y, z)) -> big
inf(x) -> cons(x, inf(s(x)))





We have the following set of usable rules: none
To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
Polynomial interpretation:
  POL(INF(x1))=  x1  
  POL(s(x1))=  x1  

We have the following set D of usable symbols: {INF, s}
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
         ↳MRR
           →DP Problem 2
             ↳Non-Overlappingness Check


Dependency Pair:

INF(x) -> INF(s(x))


Rule:

none





R does not overlap into P. Moreover, R is locally confluent (all critical pairs are trivially joinable).Hence we can switch to innermost.
The transformation is resulting in one subcycle: 


   R
     ↳DPs
       →DP Problem 1
         ↳MRR
           →DP Problem 2
             ↳NOC
             ...
               →DP Problem 3
                 ↳Non Termination


Dependency Pair:

INF(x) -> INF(s(x))


Rule:

none


Strategy:

innermost




Found an infinite P-chain over R:
P =

INF(x) -> INF(s(x))

R = none

s = INF(x)
evaluates to t =INF(s(x))

Thus, s starts an infinite chain as s matches t.

Non-Termination of R could be shown.
Duration:
0:01 minutes