TIMEOUT

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

The following DP Processors were used


Problem 1 remains open; application of the following processors failed [DependencyGraph (1466ms), SubtermCriterion (3ms), DependencyGraph (1385ms), PolynomialLinearRange4iUR (8523ms), DependencyGraph (1299ms), PolynomialLinearRange8NegiUR (29074ms), DependencyGraph (1233ms), ReductionPairSAT (timeout)].

The following open problems remain:

Open Dependency Pair Problem 1

Dependency Pairs

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#(f, x)
app#(app(app(app(filter2, true), f), x), xs) → app#(app(cons, x), app(app(filter, f), xs))app#(app(filter, f), app(app(cons, x), xs)) → app#(f, x)
app#(app(app(app(filter2, true), f), x), xs) → app#(filter, f)app#(D, app(app(-, x), y)) → app#(app(-, app(D, x)), app(D, y))
app#(D, app(app(-, x), y)) → app#(-, app(D, x))app#(app(app(app(filter2, true), f), x), xs) → app#(app(filter, f), xs)
app#(app(filter, f), app(app(cons, x), xs)) → app#(app(app(app(filter2, app(f, x)), f), x), xs)app#(D, app(app(*, x), y)) → app#(+, app(app(*, y), app(D, x)))
app#(D, app(app(*, x), y)) → app#(*, y)app#(D, app(app(*, x), y)) → app#(app(+, app(app(*, y), app(D, x))), app(app(*, x), app(D, y)))
app#(app(filter, f), app(app(cons, x), xs)) → app#(filter2, app(f, x))app#(D, app(app(*, x), y)) → app#(*, x)
app#(D, app(app(*, x), y)) → app#(app(*, x), app(D, y))app#(app(map, f), app(app(cons, x), xs)) → app#(map, f)
app#(app(app(app(filter2, false), f), x), xs) → app#(filter, f)app#(D, app(app(-, x), y)) → app#(D, y)
app#(D, app(app(*, x), y)) → app#(D, y)app#(app(map, f), app(app(cons, x), xs)) → app#(app(map, f), xs)
app#(D, app(app(-, x), y)) → app#(D, x)app#(app(filter, f), app(app(cons, x), xs)) → app#(app(app(filter2, app(f, x)), f), x)
app#(D, app(app(+, x), y)) → app#(app(+, app(D, x)), app(D, y))app#(app(app(app(filter2, true), f), x), xs) → app#(cons, x)
app#(app(filter, f), app(app(cons, x), xs)) → app#(app(filter2, app(f, x)), f)app#(D, app(app(+, x), y)) → app#(+, app(D, x))
app#(D, app(app(+, x), y)) → app#(D, x)app#(app(app(app(filter2, false), f), x), xs) → app#(app(filter, f), xs)
app#(D, app(app(*, x), y)) → app#(app(*, y), app(D, x))app#(app(map, f), app(app(cons, x), xs)) → app#(cons, app(f, x))
app#(D, app(app(+, x), y)) → app#(D, y)app#(D, app(app(*, x), y)) → app#(D, x)

Rewrite Rules

app(D, t) → 1app(D, constant) → 0
app(D, app(app(+, x), y)) → app(app(+, app(D, x)), app(D, y))app(D, app(app(*, x), y)) → app(app(+, app(app(*, y), app(D, x))), app(app(*, x), app(D, y)))
app(D, app(app(-, x), y)) → app(app(-, app(D, x)), app(D, y))app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, x), xs)) → app(app(cons, app(f, x)), app(app(map, f), xs))app(app(filter, f), nil) → nil
app(app(filter, f), app(app(cons, x), xs)) → app(app(app(app(filter2, app(f, x)), f), x), xs)app(app(app(app(filter2, true), f), x), xs) → app(app(cons, x), app(app(filter, f), xs))
app(app(app(app(filter2, false), f), x), xs) → app(app(filter, f), xs)

Original Signature

Termination of terms over the following signature is verified: D, app, constant, *, true, +, -, 1, t, 0, map, false, filter2, filter, nil, cons