The TRS could not be proven terminating. The proof attempt took 60000 ms.
Problem 1 remains open; application of the following processors failed [DependencyGraph (6260ms), SubtermCriterion (1ms), DependencyGraph (5655ms), PolynomialLinearRange4iUR (10006ms), DependencyGraph (timeout), PolynomialLinearRange8NegiUR (30007ms), DependencyGraph (timeout), ReductionPairSAT (timeout)].
| 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(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#(minsort, app(app(cons, x), y)) | → | app#(app(min, x), y) | app#(app(app(app(filter2, true), f), x), xs) | → | app#(filter, f) | |
| app#(app(del, x), app(app(cons, y), z)) | → | app#(app(del, x), z) | app#(app(app(app(filter2, true), f), x), xs) | → | app#(app(filter, f), xs) | |
| app#(app(min, x), app(app(cons, y), z)) | → | app#(if, app(app(le, x), y)) | app#(minsort, app(app(cons, x), y)) | → | app#(app(del, app(app(min, x), y)), app(app(cons, x), y)) | |
| app#(minsort, app(app(cons, x), y)) | → | app#(minsort, app(app(del, app(app(min, x), y)), app(app(cons, x), y))) | app#(app(filter, f), app(app(cons, x), xs)) | → | app#(app(app(app(filter2, app(f, x)), f), x), xs) | |
| app#(app(del, x), app(app(cons, y), z)) | → | app#(app(if, app(app(eq, x), y)), z) | app#(app(eq, app(s, x)), app(s, y)) | → | app#(eq, x) | |
| app#(minsort, app(app(cons, x), y)) | → | app#(app(cons, x), y) | app#(app(min, x), app(app(cons, y), z)) | → | app#(app(min, x), z) | |
| app#(app(filter, f), app(app(cons, x), xs)) | → | app#(filter2, app(f, x)) | app#(app(min, x), app(app(cons, y), z)) | → | app#(app(min, y), z) | |
| app#(app(map, f), app(app(cons, x), xs)) | → | app#(map, f) | app#(app(min, x), app(app(cons, y), z)) | → | app#(app(app(if, app(app(le, x), y)), app(app(min, x), z)), app(app(min, y), z)) | |
| app#(minsort, app(app(cons, x), y)) | → | app#(del, app(app(min, x), y)) | app#(app(le, app(s, x)), app(s, y)) | → | app#(le, x) | |
| app#(app(app(app(filter2, false), f), x), xs) | → | app#(filter, f) | app#(app(del, x), app(app(cons, y), z)) | → | app#(app(cons, y), app(app(del, x), z)) | |
| app#(minsort, app(app(cons, x), y)) | → | app#(min, x) | app#(minsort, app(app(cons, x), y)) | → | app#(cons, x) | |
| app#(app(min, x), app(app(cons, y), z)) | → | app#(min, x) | app#(app(eq, app(s, x)), app(s, y)) | → | app#(app(eq, x), y) | |
| app#(app(map, f), app(app(cons, x), xs)) | → | app#(app(map, f), xs) | app#(app(del, x), app(app(cons, y), z)) | → | app#(cons, y) | |
| app#(app(del, x), app(app(cons, y), z)) | → | app#(del, x) | app#(app(min, x), app(app(cons, y), z)) | → | app#(min, y) | |
| app#(app(del, x), app(app(cons, y), z)) | → | app#(app(app(if, app(app(eq, x), y)), z), app(app(cons, y), app(app(del, x), z))) | app#(minsort, app(app(cons, x), y)) | → | app#(app(cons, app(app(min, x), y)), app(minsort, app(app(del, app(app(min, x), y)), app(app(cons, x), y)))) | |
| app#(app(filter, f), app(app(cons, x), xs)) | → | app#(app(app(filter2, app(f, x)), f), x) | app#(minsort, app(app(cons, x), y)) | → | app#(cons, app(app(min, x), y)) | |
| app#(app(le, app(s, x)), app(s, y)) | → | app#(app(le, x), y) | app#(app(del, x), app(app(cons, y), z)) | → | app#(if, app(app(eq, x), y)) | |
| app#(app(del, x), app(app(cons, y), z)) | → | app#(app(eq, x), 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#(app(min, x), app(app(cons, y), z)) | → | app#(app(le, x), y) | |
| app#(app(min, x), app(app(cons, y), z)) | → | app#(app(if, app(app(le, x), y)), app(app(min, x), z)) | app#(app(app(app(filter2, false), f), x), xs) | → | app#(app(filter, f), xs) | |
| app#(app(del, x), app(app(cons, y), z)) | → | app#(eq, x) | app#(app(map, f), app(app(cons, x), xs)) | → | app#(cons, app(f, x)) | |
| app#(app(min, x), app(app(cons, y), z)) | → | app#(le, x) |
| app(app(le, 0), y) | → | true | app(app(le, app(s, x)), 0) | → | false | |
| app(app(le, app(s, x)), app(s, y)) | → | app(app(le, x), y) | app(app(eq, 0), 0) | → | true | |
| app(app(eq, 0), app(s, y)) | → | false | app(app(eq, app(s, x)), 0) | → | false | |
| app(app(eq, app(s, x)), app(s, y)) | → | app(app(eq, x), y) | app(app(app(if, true), x), y) | → | x | |
| app(app(app(if, false), x), y) | → | y | app(minsort, nil) | → | nil | |
| app(minsort, app(app(cons, x), y)) | → | app(app(cons, app(app(min, x), y)), app(minsort, app(app(del, app(app(min, x), y)), app(app(cons, x), y)))) | app(app(min, x), nil) | → | x | |
| app(app(min, x), app(app(cons, y), z)) | → | app(app(app(if, app(app(le, x), y)), app(app(min, x), z)), app(app(min, y), z)) | app(app(del, x), nil) | → | nil | |
| app(app(del, x), app(app(cons, y), z)) | → | app(app(app(if, app(app(eq, x), y)), z), app(app(cons, y), app(app(del, x), z))) | 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) |
Termination of terms over the following signature is verified: minsort, min, app, true, 0, le, s, if, map, false, del, filter2, filter, eq, nil, cons