Term Rewriting System R:

   [x]
   ap(ap(ff, x), x) -> ap(ap(x, ap(ff, x)), ap(ap(cons, x), nil))

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: 


   AP(ap(ff, x), x) -> AP(ap(x, ap(ff, x)), ap(ap(cons, x), nil))
   AP(ap(ff, x), x) -> AP(x, ap(ff, x))
   AP(ap(ff, x), x) -> AP(ap(cons, x), nil)
   AP(ap(ff, x), x) -> AP(cons, x)

Furthermore, R contains one SCC.


SCC1:

AP(ap(ff, x), x) -> AP(ap(cons, x), nil)
AP(ap(ff, x), x) -> AP(ap(x, ap(ff, x)), ap(ap(cons, x), nil))

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

   AP(ap(ff, x), x) -> AP(ap(x, ap(ff, x)), ap(ap(cons, x), nil))
no new Dependency Pairs
are created.

none
The transformation is resulting in one subcycle:


SCC1.Nar1:

AP(ap(ff, x), x) -> AP(ap(cons, x), nil)

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

   AP(ap(ff, x), x) -> AP(ap(cons, x), nil)
no new Dependency Pairs
are created.

none
The transformation is resulting in no subcycles.




Termination of R successfully shown.


Duration: 0.462 seconds.