Term Rewriting System R:
[x]
f(s(x)) -> s(s(f(p(s(x)))))
f(0) -> 0
p(s(x)) -> x

Termination of R to be shown.



   TRS
Removing Redundant Rules



Removing the following rules from R which fullfill a polynomial ordering:

f(0) -> 0

where the Polynomial interpretation:
  POL(0)=  1  
  POL(s(x1))=  x1  
  POL(f(x1))=  2·x1  
  POL(p(x1))=  x1  
was used.

Not all Rules of R can be deleted, so we still have to regard a part of R.


   TRS
RRRPolo
       →TRS2
Dependency Pair Analysis



R contains the following Dependency Pairs:

F(s(x)) -> F(p(s(x)))
F(s(x)) -> P(s(x))

Furthermore, R contains one SCC.


   TRS
RRRPolo
       →TRS2
DPs
           →DP Problem 1
Non-Overlappingness Check


Dependency Pair:

F(s(x)) -> F(p(s(x)))


Rules:


f(s(x)) -> s(s(f(p(s(x)))))
p(s(x)) -> x





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:


   TRS
RRRPolo
       →TRS2
DPs
           →DP Problem 1
NOC
             ...
               →DP Problem 2
Usable Rules (Innermost)


Dependency Pair:

F(s(x)) -> F(p(s(x)))


Rules:


f(s(x)) -> s(s(f(p(s(x)))))
p(s(x)) -> x


Strategy:

innermost




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


   TRS
RRRPolo
       →TRS2
DPs
           →DP Problem 1
NOC
             ...
               →DP Problem 3
Modular Removal of Rules


Dependency Pair:

F(s(x)) -> F(p(s(x)))


Rule:


p(s(x)) -> x


Strategy:

innermost




We have the following set of usable rules:

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

We have the following set D of usable symbols: {s, F, p}
No Dependency Pairs can be deleted.
The following rules can be deleted as the lhs is strictly greater than the corresponding rhs:

p(s(x)) -> x


The result of this processor delivers one new DP problem.



   TRS
RRRPolo
       →TRS2
DPs
           →DP Problem 1
NOC
             ...
               →DP Problem 4
Dependency Graph


Dependency Pair:

F(s(x)) -> F(p(s(x)))


Rule:

none


Strategy:

innermost




Using the Dependency Graph resulted in no new DP problems.

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