YES
0 QTRS
↳1 DependencyPairsProof (⇔, 0 ms)
↳2 QDP
↳3 DependencyGraphProof (⇔, 0 ms)
↳4 AND
↳5 QDP
↳6 UsableRulesProof (⇔, 0 ms)
↳7 QDP
↳8 QDPSizeChangeProof (⇔, 0 ms)
↳9 YES
↳10 QDP
↳11 UsableRulesProof (⇔, 0 ms)
↳12 QDP
↳13 QDPSizeChangeProof (⇔, 0 ms)
↳14 YES
app(f, app(f, x)) → app(g, app(f, x))
app(g, app(g, x)) → app(f, x)
app(app(map, fun), nil) → nil
app(app(map, fun), app(app(cons, x), xs)) → app(app(cons, app(fun, x)), app(app(map, fun), xs))
app(app(filter, fun), nil) → nil
app(app(filter, fun), app(app(cons, x), xs)) → app(app(app(app(filter2, app(fun, x)), fun), x), xs)
app(app(app(app(filter2, true), fun), x), xs) → app(app(cons, x), app(app(filter, fun), xs))
app(app(app(app(filter2, false), fun), x), xs) → app(app(filter, fun), xs)
APP(f, app(f, x)) → APP(g, app(f, x))
APP(g, app(g, x)) → APP(f, x)
APP(app(map, fun), app(app(cons, x), xs)) → APP(app(cons, app(fun, x)), app(app(map, fun), xs))
APP(app(map, fun), app(app(cons, x), xs)) → APP(cons, app(fun, x))
APP(app(map, fun), app(app(cons, x), xs)) → APP(fun, x)
APP(app(map, fun), app(app(cons, x), xs)) → APP(app(map, fun), xs)
APP(app(filter, fun), app(app(cons, x), xs)) → APP(app(app(app(filter2, app(fun, x)), fun), x), xs)
APP(app(filter, fun), app(app(cons, x), xs)) → APP(app(app(filter2, app(fun, x)), fun), x)
APP(app(filter, fun), app(app(cons, x), xs)) → APP(app(filter2, app(fun, x)), fun)
APP(app(filter, fun), app(app(cons, x), xs)) → APP(filter2, app(fun, x))
APP(app(filter, fun), app(app(cons, x), xs)) → APP(fun, x)
APP(app(app(app(filter2, true), fun), x), xs) → APP(app(cons, x), app(app(filter, fun), xs))
APP(app(app(app(filter2, true), fun), x), xs) → APP(cons, x)
APP(app(app(app(filter2, true), fun), x), xs) → APP(app(filter, fun), xs)
APP(app(app(app(filter2, true), fun), x), xs) → APP(filter, fun)
APP(app(app(app(filter2, false), fun), x), xs) → APP(app(filter, fun), xs)
APP(app(app(app(filter2, false), fun), x), xs) → APP(filter, fun)
app(f, app(f, x)) → app(g, app(f, x))
app(g, app(g, x)) → app(f, x)
app(app(map, fun), nil) → nil
app(app(map, fun), app(app(cons, x), xs)) → app(app(cons, app(fun, x)), app(app(map, fun), xs))
app(app(filter, fun), nil) → nil
app(app(filter, fun), app(app(cons, x), xs)) → app(app(app(app(filter2, app(fun, x)), fun), x), xs)
app(app(app(app(filter2, true), fun), x), xs) → app(app(cons, x), app(app(filter, fun), xs))
app(app(app(app(filter2, false), fun), x), xs) → app(app(filter, fun), xs)
APP(g, app(g, x)) → APP(f, x)
APP(f, app(f, x)) → APP(g, app(f, x))
app(f, app(f, x)) → app(g, app(f, x))
app(g, app(g, x)) → app(f, x)
app(app(map, fun), nil) → nil
app(app(map, fun), app(app(cons, x), xs)) → app(app(cons, app(fun, x)), app(app(map, fun), xs))
app(app(filter, fun), nil) → nil
app(app(filter, fun), app(app(cons, x), xs)) → app(app(app(app(filter2, app(fun, x)), fun), x), xs)
app(app(app(app(filter2, true), fun), x), xs) → app(app(cons, x), app(app(filter, fun), xs))
app(app(app(app(filter2, false), fun), x), xs) → app(app(filter, fun), xs)
APP(g, app(g, x)) → APP(f, x)
APP(f, app(f, x)) → APP(g, app(f, x))
app(g, app(g, x)) → app(f, x)
app(f, app(f, x)) → app(g, app(f, x))
From the DPs we obtained the following set of size-change graphs:
APP(app(map, fun), app(app(cons, x), xs)) → APP(app(map, fun), xs)
APP(app(map, fun), app(app(cons, x), xs)) → APP(fun, x)
APP(app(filter, fun), app(app(cons, x), xs)) → APP(fun, x)
APP(app(app(app(filter2, true), fun), x), xs) → APP(app(filter, fun), xs)
APP(app(app(app(filter2, false), fun), x), xs) → APP(app(filter, fun), xs)
app(f, app(f, x)) → app(g, app(f, x))
app(g, app(g, x)) → app(f, x)
app(app(map, fun), nil) → nil
app(app(map, fun), app(app(cons, x), xs)) → app(app(cons, app(fun, x)), app(app(map, fun), xs))
app(app(filter, fun), nil) → nil
app(app(filter, fun), app(app(cons, x), xs)) → app(app(app(app(filter2, app(fun, x)), fun), x), xs)
app(app(app(app(filter2, true), fun), x), xs) → app(app(cons, x), app(app(filter, fun), xs))
app(app(app(app(filter2, false), fun), x), xs) → app(app(filter, fun), xs)
APP(app(map, fun), app(app(cons, x), xs)) → APP(app(map, fun), xs)
APP(app(map, fun), app(app(cons, x), xs)) → APP(fun, x)
APP(app(filter, fun), app(app(cons, x), xs)) → APP(fun, x)
APP(app(app(app(filter2, true), fun), x), xs) → APP(app(filter, fun), xs)
APP(app(app(app(filter2, false), fun), x), xs) → APP(app(filter, fun), xs)
From the DPs we obtained the following set of size-change graphs: