MAYBE

The TRS could not be proven terminating. The proof attempt took 56047 ms.

The following DP Processors were used

Problem 1 remains open; application of the following processors failed [DependencyGraph (72ms), SubtermCriterion (1ms), DependencyGraph (39ms), PolynomialLinearRange4iUR (1582ms), DependencyGraph (35ms), PolynomialLinearRange8NegiUR (8590ms), DependencyGraph (58ms), ReductionPairSAT (45431ms), DependencyGraph (49ms), SizeChangePrinciple (30ms)].

The following open problems remain:

Open Dependency Pair Problem 1

Dependency Pairs

ap^#(ap(ap(foldr, g), h), ap(ap(cons, x), xs))	→	ap^#(ap(foldr, g), h)		ap^#(ap(ap(foldr, g), h), ap(ap(cons, x), xs))	→	ap^#(g, x)
ap^#(ap(f, x), x)	→	ap^#(cons, x)		ap^#(ap(ap(foldr, g), h), ap(ap(cons, x), xs))	→	ap^#(ap(ap(foldr, g), h), xs)
ap^#(ap(f, x), x)	→	ap^#(f, x)		ap^#(ap(f, x), 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(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^#(foldr, g)		ap^#(ap(f, x), x)	→	ap^#(x, ap(f, x))

Rewrite Rules

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))

Original Signature

Termination of terms over the following signature is verified: f, foldr, ap, cons, nil