Term Rewriting System R:

   [x]
   f(s(x)) -> s(f(f(p(s(x)))))
   f(0) -> 0
   p(s(x)) -> x

Termination of R to be shown.


This program has no overlaps, so it is sufficient to show innermost termination. 


R contains the following Dependency Pairs: 


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

Furthermore, R contains one SCC.


SCC1:

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

On this Scc, a Rewriting SCC transformation can be performed.
 
As a result of transforming the rule 

   F(s(x)) -> F(f(p(s(x))))
one new Dependency Pair
is created:


   F(s(x)) -> F(f(x))

The transformation is resulting in one subcycle:


SCC1.Rewr1:

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

On this Scc, a Rewriting SCC transformation can be performed.
 
As a result of transforming the rule 

   F(s(x)) -> F(p(s(x)))
one new Dependency Pair
is created:


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

The transformation is resulting in one subcycle:


SCC1.Rewr1.Rewr1:

F(s(x)) -> F(x)
F(s(x)) -> F(f(x))

Using RFC Match Bounds, the Scc could be solved. The Match Bound was 2.
The certificate found is represented by the following graph.
The certificate consists of the following enumerated nodes:
34, 35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45

Node 34 is start node and node 35 is final node.

Those nodes are connect through the following edges:

* 35 to 35 labelled #(0)
* 34 to 35 labelled F(0)
* 34 to 36 labelled F(0)
* 36 to 35 labelled f(0)
* 36 to 37 labelled s(1)
* 37 to 38 labelled f(1)
* 38 to 39 labelled f(1)
* 39 to 40 labelled p(1)
* 40 to 35 labelled s(1)
* 34 to 35 labelled F(1)
* 35 to 35 labelled f(1)
* 35 to 37 labelled f(1)
* 34 to 37 labelled F(1)
* 35 to 37 labelled s(1)
* 35 to 41 labelled s(2)
* 41 to 42 labelled f(2)
* 42 to 43 labelled f(2)
* 43 to 44 labelled p(2)
* 44 to 37 labelled s(2)
* 34 to 45 labelled F(2)
* 45 to 37 labelled f(2)
* 34 to 37 labelled F(2)
* 40 to 37 labelled s(1)
* 44 to 41 labelled s(2)
* 35 to 41 labelled f(1)
* 34 to 41 labelled F(1)
* 40 to 41 labelled s(1)
* 45 to 41 labelled f(2)
* 34 to 41 labelled F(2)




Termination of R successfully shown.


Duration: 10.798 seconds.