YES
0 QTRS
↳1 DependencyPairsProof (⇔, 0 ms)
↳2 QDP
↳3 DependencyGraphProof (⇔, 0 ms)
↳4 QDP
↳5 UsableRulesProof (⇔, 1 ms)
↳6 QDP
↳7 QDPSizeChangeProof (⇔, 0 ms)
↳8 YES
app(app(app(if, true), x), y) → x
app(app(app(if, true), x), y) → y
app(app(takeWhile, p), nil) → nil
app(app(takeWhile, p), app(app(cons, x), xs)) → app(app(app(if, app(p, x)), app(app(cons, x), app(app(takeWhile, p), xs))), nil)
app(app(dropWhile, p), nil) → nil
app(app(dropWhile, p), app(app(cons, x), xs)) → app(app(app(if, app(p, x)), app(app(dropWhile, p), xs)), app(app(cons, x), xs))
APP(app(takeWhile, p), app(app(cons, x), xs)) → APP(app(app(if, app(p, x)), app(app(cons, x), app(app(takeWhile, p), xs))), nil)
APP(app(takeWhile, p), app(app(cons, x), xs)) → APP(app(if, app(p, x)), app(app(cons, x), app(app(takeWhile, p), xs)))
APP(app(takeWhile, p), app(app(cons, x), xs)) → APP(if, app(p, x))
APP(app(takeWhile, p), app(app(cons, x), xs)) → APP(p, x)
APP(app(takeWhile, p), app(app(cons, x), xs)) → APP(app(cons, x), app(app(takeWhile, p), xs))
APP(app(takeWhile, p), app(app(cons, x), xs)) → APP(app(takeWhile, p), xs)
APP(app(dropWhile, p), app(app(cons, x), xs)) → APP(app(app(if, app(p, x)), app(app(dropWhile, p), xs)), app(app(cons, x), xs))
APP(app(dropWhile, p), app(app(cons, x), xs)) → APP(app(if, app(p, x)), app(app(dropWhile, p), xs))
APP(app(dropWhile, p), app(app(cons, x), xs)) → APP(if, app(p, x))
APP(app(dropWhile, p), app(app(cons, x), xs)) → APP(p, x)
APP(app(dropWhile, p), app(app(cons, x), xs)) → APP(app(dropWhile, p), xs)
app(app(app(if, true), x), y) → x
app(app(app(if, true), x), y) → y
app(app(takeWhile, p), nil) → nil
app(app(takeWhile, p), app(app(cons, x), xs)) → app(app(app(if, app(p, x)), app(app(cons, x), app(app(takeWhile, p), xs))), nil)
app(app(dropWhile, p), nil) → nil
app(app(dropWhile, p), app(app(cons, x), xs)) → app(app(app(if, app(p, x)), app(app(dropWhile, p), xs)), app(app(cons, x), xs))
APP(app(takeWhile, p), app(app(cons, x), xs)) → APP(app(takeWhile, p), xs)
APP(app(takeWhile, p), app(app(cons, x), xs)) → APP(p, x)
APP(app(dropWhile, p), app(app(cons, x), xs)) → APP(p, x)
APP(app(dropWhile, p), app(app(cons, x), xs)) → APP(app(dropWhile, p), xs)
app(app(app(if, true), x), y) → x
app(app(app(if, true), x), y) → y
app(app(takeWhile, p), nil) → nil
app(app(takeWhile, p), app(app(cons, x), xs)) → app(app(app(if, app(p, x)), app(app(cons, x), app(app(takeWhile, p), xs))), nil)
app(app(dropWhile, p), nil) → nil
app(app(dropWhile, p), app(app(cons, x), xs)) → app(app(app(if, app(p, x)), app(app(dropWhile, p), xs)), app(app(cons, x), xs))
APP(app(takeWhile, p), app(app(cons, x), xs)) → APP(app(takeWhile, p), xs)
APP(app(takeWhile, p), app(app(cons, x), xs)) → APP(p, x)
APP(app(dropWhile, p), app(app(cons, x), xs)) → APP(p, x)
APP(app(dropWhile, p), app(app(cons, x), xs)) → APP(app(dropWhile, p), xs)
From the DPs we obtained the following set of size-change graphs: