Term Rewriting System R:

   [x, g, h, xs]
   ap(ap(f, x), x) -> ap(ap(x, ap(f, x)), ap(ap(cons, x), nil))
   ap(ap(ap(foldr, g), h), nil) -> h
   ap(ap(ap(foldr, g), h), ap(ap(cons, x), xs)) -> ap(ap(g, x), ap(ap(ap(foldr, g), h), xs))

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(f, x), x) -> AP(ap(x, ap(f, x)), ap(ap(cons, x), nil))
   AP(ap(f, x), x) -> AP(x, ap(f, x))
   AP(ap(f, x), x) -> AP(ap(cons, x), nil)
   AP(ap(f, x), x) -> AP(cons, x)
   AP(ap(ap(foldr, g), h), ap(ap(cons, x), xs)) -> AP(ap(g, x), ap(ap(ap(foldr, g), h), xs))
   AP(ap(ap(foldr, g), h), ap(ap(cons, x), xs)) -> AP(g, x)
   AP(ap(ap(foldr, g), h), ap(ap(cons, x), xs)) -> AP(ap(ap(foldr, g), h), xs)

Furthermore, R contains one SCC.


SCC1:

AP(ap(ap(foldr, g), h), ap(ap(cons, x), xs)) -> AP(ap(ap(foldr, g), h), xs)
AP(ap(ap(foldr, g), h), ap(ap(cons, x), xs)) -> AP(g, x)
AP(ap(ap(foldr, g), h), ap(ap(cons, x), xs)) -> AP(ap(g, x), ap(ap(ap(foldr, g), h), xs))
AP(ap(f, x), x) -> AP(ap(cons, x), nil)
AP(ap(f, x), x) -> AP(ap(x, ap(f, 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(f, x), x) -> AP(ap(cons, x), nil)
no new Dependency Pairs
are created.

none
The transformation is resulting in one subcycle:


SCC1.Nar1:

AP(ap(ap(foldr, g), h), ap(ap(cons, x), xs)) -> AP(g, x)
AP(ap(f, x), x) -> AP(ap(x, ap(f, x)), ap(ap(cons, x), nil))
AP(ap(ap(foldr, g), h), ap(ap(cons, x), xs)) -> AP(ap(g, x), ap(ap(ap(foldr, g), h), xs))
AP(ap(ap(foldr, g), h), ap(ap(cons, x), xs)) -> AP(ap(ap(foldr, g), h), xs)

Found an infinite P-chain over R:
P = AP(ap(ap(foldr, g), h), ap(ap(cons, x), xs)) -> AP(g, x)
AP(ap(f, x), x) -> AP(ap(x, ap(f, x)), ap(ap(cons, x), nil))
AP(ap(ap(foldr, g), h), ap(ap(cons, x), xs)) -> AP(ap(g, x), ap(ap(ap(foldr, g), h), xs))
AP(ap(ap(foldr, g), h), ap(ap(cons, x), xs)) -> AP(ap(ap(foldr, g), h), xs)
R = [ap(ap(f, x), x) -> ap(ap(x, ap(f, x)), ap(ap(cons, x), nil)), ap(ap(ap(foldr, g), h), nil) -> h, ap(ap(ap(foldr, g), h), ap(ap(cons, x), xs)) -> ap(ap(g, x), ap(ap(ap(foldr, g), h), xs))]
s = AP(ap(ap(foldr, ap(f, foldr)), ap(ap(cons, foldr), nil)), ap(ap(cons, foldr), nil)) evaluates to t = AP(ap(ap(foldr, ap(f, foldr)), ap(ap(cons, foldr), nil)), ap(ap(cons, foldr), nil))
Thus, s starts an infinite reduction.


Non-Termination of R could be shown.

Duration: 2.30 seconds.