YES
0 QTRS
↳1 Overlay + Local Confluence (⇔, 0 ms)
↳2 QTRS
↳3 DependencyPairsProof (⇔, 24 ms)
↳4 QDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 QDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 QDP
↳10 ATransformationProof (⇔, 0 ms)
↳11 QDP
↳12 QReductionProof (⇔, 0 ms)
↳13 QDP
↳14 QDPSizeChangeProof (⇔, 0 ms)
↳15 YES
↳16 QDP
↳17 UsableRulesProof (⇔, 0 ms)
↳18 QDP
↳19 ATransformationProof (⇔, 0 ms)
↳20 QDP
↳21 QReductionProof (⇔, 0 ms)
↳22 QDP
↳23 QDPOrderProof (⇔, 14 ms)
↳24 QDP
↳25 PisEmptyProof (⇔, 0 ms)
↳26 YES
↳27 QDP
↳28 QDPSizeChangeProof (⇔, 0 ms)
↳29 YES
app(app(minus, x), 0) → x
app(app(minus, app(s, x)), app(s, y)) → app(app(minus, x), y)
app(f, 0) → app(s, 0)
app(f, app(s, x)) → app(app(minus, app(s, x)), app(g, app(f, x)))
app(g, 0) → 0
app(g, app(s, x)) → app(app(minus, app(s, x)), app(f, app(g, 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(minus, x), 0) → x
app(app(minus, app(s, x)), app(s, y)) → app(app(minus, x), y)
app(f, 0) → app(s, 0)
app(f, app(s, x)) → app(app(minus, app(s, x)), app(g, app(f, x)))
app(g, 0) → 0
app(g, app(s, x)) → app(app(minus, app(s, x)), app(f, app(g, 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(minus, x0), 0)
app(app(minus, app(s, x0)), app(s, x1))
app(f, 0)
app(f, app(s, x0))
app(g, 0)
app(g, app(s, x0))
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
app(app(filter, x0), nil)
app(app(filter, x0), app(app(cons, x1), x2))
app(app(app(app(filter2, true), x0), x1), x2)
app(app(app(app(filter2, false), x0), x1), x2)
APP(app(minus, app(s, x)), app(s, y)) → APP(app(minus, x), y)
APP(app(minus, app(s, x)), app(s, y)) → APP(minus, x)
APP(f, 0) → APP(s, 0)
APP(f, app(s, x)) → APP(app(minus, app(s, x)), app(g, app(f, x)))
APP(f, app(s, x)) → APP(minus, app(s, x))
APP(f, app(s, x)) → APP(g, app(f, x))
APP(f, app(s, x)) → APP(f, x)
APP(g, app(s, x)) → APP(app(minus, app(s, x)), app(f, app(g, x)))
APP(g, app(s, x)) → APP(minus, app(s, x))
APP(g, app(s, x)) → APP(f, app(g, x))
APP(g, app(s, x)) → APP(g, 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(app(minus, x), 0) → x
app(app(minus, app(s, x)), app(s, y)) → app(app(minus, x), y)
app(f, 0) → app(s, 0)
app(f, app(s, x)) → app(app(minus, app(s, x)), app(g, app(f, x)))
app(g, 0) → 0
app(g, app(s, x)) → app(app(minus, app(s, x)), app(f, app(g, 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(minus, x0), 0)
app(app(minus, app(s, x0)), app(s, x1))
app(f, 0)
app(f, app(s, x0))
app(g, 0)
app(g, app(s, x0))
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
app(app(filter, x0), nil)
app(app(filter, x0), app(app(cons, x1), x2))
app(app(app(app(filter2, true), x0), x1), x2)
app(app(app(app(filter2, false), x0), x1), x2)
APP(app(minus, app(s, x)), app(s, y)) → APP(app(minus, x), y)
app(app(minus, x), 0) → x
app(app(minus, app(s, x)), app(s, y)) → app(app(minus, x), y)
app(f, 0) → app(s, 0)
app(f, app(s, x)) → app(app(minus, app(s, x)), app(g, app(f, x)))
app(g, 0) → 0
app(g, app(s, x)) → app(app(minus, app(s, x)), app(f, app(g, 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(minus, x0), 0)
app(app(minus, app(s, x0)), app(s, x1))
app(f, 0)
app(f, app(s, x0))
app(g, 0)
app(g, app(s, x0))
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
app(app(filter, x0), nil)
app(app(filter, x0), app(app(cons, x1), x2))
app(app(app(app(filter2, true), x0), x1), x2)
app(app(app(app(filter2, false), x0), x1), x2)
APP(app(minus, app(s, x)), app(s, y)) → APP(app(minus, x), y)
app(app(minus, x0), 0)
app(app(minus, app(s, x0)), app(s, x1))
app(f, 0)
app(f, app(s, x0))
app(g, 0)
app(g, app(s, x0))
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
app(app(filter, x0), nil)
app(app(filter, x0), app(app(cons, x1), x2))
app(app(app(app(filter2, true), x0), x1), x2)
app(app(app(app(filter2, false), x0), x1), x2)
minus1(s(x), s(y)) → minus1(x, y)
minus(x0, 0)
minus(s(x0), s(x1))
f(0)
f(s(x0))
g(0)
g(s(x0))
map(x0, nil)
map(x0, cons(x1, x2))
filter(x0, nil)
filter(x0, cons(x1, x2))
filter2(true, x0, x1, x2)
filter2(false, x0, x1, x2)
minus(x0, 0)
minus(s(x0), s(x1))
f(0)
f(s(x0))
g(0)
g(s(x0))
map(x0, nil)
map(x0, cons(x1, x2))
filter(x0, nil)
filter(x0, cons(x1, x2))
filter2(true, x0, x1, x2)
filter2(false, x0, x1, x2)
minus1(s(x), s(y)) → minus1(x, y)
From the DPs we obtained the following set of size-change graphs:
APP(f, app(s, x)) → APP(g, app(f, x))
APP(g, app(s, x)) → APP(f, app(g, x))
APP(f, app(s, x)) → APP(f, x)
APP(g, app(s, x)) → APP(g, x)
app(app(minus, x), 0) → x
app(app(minus, app(s, x)), app(s, y)) → app(app(minus, x), y)
app(f, 0) → app(s, 0)
app(f, app(s, x)) → app(app(minus, app(s, x)), app(g, app(f, x)))
app(g, 0) → 0
app(g, app(s, x)) → app(app(minus, app(s, x)), app(f, app(g, 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(minus, x0), 0)
app(app(minus, app(s, x0)), app(s, x1))
app(f, 0)
app(f, app(s, x0))
app(g, 0)
app(g, app(s, x0))
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
app(app(filter, x0), nil)
app(app(filter, x0), app(app(cons, x1), x2))
app(app(app(app(filter2, true), x0), x1), x2)
app(app(app(app(filter2, false), x0), x1), x2)
APP(f, app(s, x)) → APP(g, app(f, x))
APP(g, app(s, x)) → APP(f, app(g, x))
APP(f, app(s, x)) → APP(f, x)
APP(g, app(s, x)) → APP(g, x)
app(g, 0) → 0
app(g, app(s, x)) → app(app(minus, app(s, x)), app(f, app(g, x)))
app(f, 0) → app(s, 0)
app(f, app(s, x)) → app(app(minus, app(s, x)), app(g, app(f, x)))
app(app(minus, x), 0) → x
app(app(minus, app(s, x)), app(s, y)) → app(app(minus, x), y)
app(app(minus, x0), 0)
app(app(minus, app(s, x0)), app(s, x1))
app(f, 0)
app(f, app(s, x0))
app(g, 0)
app(g, app(s, x0))
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
app(app(filter, x0), nil)
app(app(filter, x0), app(app(cons, x1), x2))
app(app(app(app(filter2, true), x0), x1), x2)
app(app(app(app(filter2, false), x0), x1), x2)
f1(s(x)) → g1(f(x))
g1(s(x)) → f1(g(x))
f1(s(x)) → f1(x)
g1(s(x)) → g1(x)
g(0) → 0
g(s(x)) → minus(s(x), f(g(x)))
f(0) → s(0)
f(s(x)) → minus(s(x), g(f(x)))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
minus(x0, 0)
minus(s(x0), s(x1))
f(0)
f(s(x0))
g(0)
g(s(x0))
map(x0, nil)
map(x0, cons(x1, x2))
filter(x0, nil)
filter(x0, cons(x1, x2))
filter2(true, x0, x1, x2)
filter2(false, x0, x1, x2)
map(x0, nil)
map(x0, cons(x1, x2))
filter(x0, nil)
filter(x0, cons(x1, x2))
filter2(true, x0, x1, x2)
filter2(false, x0, x1, x2)
f1(s(x)) → g1(f(x))
g1(s(x)) → f1(g(x))
f1(s(x)) → f1(x)
g1(s(x)) → g1(x)
g(0) → 0
g(s(x)) → minus(s(x), f(g(x)))
f(0) → s(0)
f(s(x)) → minus(s(x), g(f(x)))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
minus(x0, 0)
minus(s(x0), s(x1))
f(0)
f(s(x0))
g(0)
g(s(x0))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
f1(s(x)) → g1(f(x))
g1(s(x)) → f1(g(x))
f1(s(x)) → f1(x)
g1(s(x)) → g1(x)
0 > [f11, s1, f1] > g11
f11: multiset
s1: multiset
g11: multiset
f1: multiset
0: multiset
f(0) → s(0)
f(s(x)) → minus(s(x), g(f(x)))
g(0) → 0
g(s(x)) → minus(s(x), f(g(x)))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
g(0) → 0
g(s(x)) → minus(s(x), f(g(x)))
f(0) → s(0)
f(s(x)) → minus(s(x), g(f(x)))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
minus(x0, 0)
minus(s(x0), s(x1))
f(0)
f(s(x0))
g(0)
g(s(x0))
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(app(app(app(filter2, app(fun, x)), fun), x), xs)
APP(app(app(app(filter2, true), fun), x), xs) → APP(app(filter, fun), xs)
APP(app(filter, fun), app(app(cons, x), xs)) → APP(fun, x)
APP(app(app(app(filter2, false), fun), x), xs) → APP(app(filter, fun), xs)
app(app(minus, x), 0) → x
app(app(minus, app(s, x)), app(s, y)) → app(app(minus, x), y)
app(f, 0) → app(s, 0)
app(f, app(s, x)) → app(app(minus, app(s, x)), app(g, app(f, x)))
app(g, 0) → 0
app(g, app(s, x)) → app(app(minus, app(s, x)), app(f, app(g, 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(minus, x0), 0)
app(app(minus, app(s, x0)), app(s, x1))
app(f, 0)
app(f, app(s, x0))
app(g, 0)
app(g, app(s, x0))
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
app(app(filter, x0), nil)
app(app(filter, x0), app(app(cons, x1), x2))
app(app(app(app(filter2, true), x0), x1), x2)
app(app(app(app(filter2, false), x0), x1), x2)
From the DPs we obtained the following set of size-change graphs: