MAYBE

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

The following DP Processors were used


Problem 1 remains open; application of the following processors failed [DependencyGraph (30ms), SubtermCriterion (1ms), DependencyGraph (13ms), PolynomialLinearRange4iUR (671ms), DependencyGraph (10ms), PolynomialLinearRange8NegiUR (3521ms), DependencyGraph (7ms), ReductionPairSAT (15219ms), DependencyGraph (7ms), SizeChangePrinciple (14ms)].

The following open problems remain:

Open Dependency Pair Problem 1

Dependency Pairs

app#(app(map, f), app(app(cons, x), xs)) → app#(f, x)app#(app(map, f), app(app(cons, x), xs)) → app#(app(cons, app(f, x)), app(app(map, f), xs))
app#(app(map, f), app(app(cons, x), xs)) → app#(app(map, f), xs)app#(app(map, f), app(app(cons, x), xs)) → app#(map, f)
app#(app(map, f), app(app(cons, x), xs)) → app#(cons, app(f, x))

Rewrite Rules

app(app(map, f), nil) → nilapp(app(map, f), app(app(cons, x), xs)) → app(app(cons, app(f, x)), app(app(map, f), xs))

Original Signature

Termination of terms over the following signature is verified: app, map, cons, nil