YES
0 QTRS
↳1 Overlay + Local Confluence (⇔, 3 ms)
↳2 QTRS
↳3 DependencyPairsProof (⇔, 0 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 QDPSizeChangeProof (⇔, 0 ms)
↳24 YES
↳25 QDP
↳26 UsableRulesProof (⇔, 0 ms)
↳27 QDP
↳28 ATransformationProof (⇔, 0 ms)
↳29 QDP
↳30 QReductionProof (⇔, 0 ms)
↳31 QDP
↳32 QDPSizeChangeProof (⇔, 0 ms)
↳33 YES
↳34 QDP
↳35 UsableRulesProof (⇔, 0 ms)
↳36 QDP
↳37 QDPSizeChangeProof (⇔, 0 ms)
↳38 YES
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(append, xs), nil) → xs
app(app(append, nil), ys) → ys
app(app(append, app(app(cons, x), xs)), ys) → app(app(cons, x), app(app(append, xs), ys))
app(app(zip, nil), yss) → yss
app(app(zip, xss), nil) → xss
app(app(zip, app(app(cons, xs), xss)), app(app(cons, ys), yss)) → app(app(cons, app(app(append, xs), ys)), app(app(zip, xss), yss))
app(app(combine, xs), nil) → xs
app(app(combine, xs), app(app(cons, ys), yss)) → app(app(combine, app(app(zip, xs), ys)), yss)
app(levels, app(app(node, x), xs)) → app(app(cons, app(app(cons, x), nil)), app(app(combine, nil), app(app(map, levels), xs)))
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(append, xs), nil) → xs
app(app(append, nil), ys) → ys
app(app(append, app(app(cons, x), xs)), ys) → app(app(cons, x), app(app(append, xs), ys))
app(app(zip, nil), yss) → yss
app(app(zip, xss), nil) → xss
app(app(zip, app(app(cons, xs), xss)), app(app(cons, ys), yss)) → app(app(cons, app(app(append, xs), ys)), app(app(zip, xss), yss))
app(app(combine, xs), nil) → xs
app(app(combine, xs), app(app(cons, ys), yss)) → app(app(combine, app(app(zip, xs), ys)), yss)
app(levels, app(app(node, x), xs)) → app(app(cons, app(app(cons, x), nil)), app(app(combine, nil), app(app(map, levels), xs)))
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
app(app(append, x0), nil)
app(app(append, nil), x0)
app(app(append, app(app(cons, x0), x1)), x2)
app(app(zip, nil), x0)
app(app(zip, x0), nil)
app(app(zip, app(app(cons, x0), x1)), app(app(cons, x2), x3))
app(app(combine, x0), nil)
app(app(combine, x0), app(app(cons, x1), x2))
app(levels, app(app(node, x0), x1))
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(cons, app(f, x))
APP(app(map, f), app(app(cons, x), xs)) → APP(f, x)
APP(app(map, f), app(app(cons, x), xs)) → APP(app(map, f), xs)
APP(app(append, app(app(cons, x), xs)), ys) → APP(app(cons, x), app(app(append, xs), ys))
APP(app(append, app(app(cons, x), xs)), ys) → APP(app(append, xs), ys)
APP(app(append, app(app(cons, x), xs)), ys) → APP(append, xs)
APP(app(zip, app(app(cons, xs), xss)), app(app(cons, ys), yss)) → APP(app(cons, app(app(append, xs), ys)), app(app(zip, xss), yss))
APP(app(zip, app(app(cons, xs), xss)), app(app(cons, ys), yss)) → APP(cons, app(app(append, xs), ys))
APP(app(zip, app(app(cons, xs), xss)), app(app(cons, ys), yss)) → APP(app(append, xs), ys)
APP(app(zip, app(app(cons, xs), xss)), app(app(cons, ys), yss)) → APP(append, xs)
APP(app(zip, app(app(cons, xs), xss)), app(app(cons, ys), yss)) → APP(app(zip, xss), yss)
APP(app(zip, app(app(cons, xs), xss)), app(app(cons, ys), yss)) → APP(zip, xss)
APP(app(combine, xs), app(app(cons, ys), yss)) → APP(app(combine, app(app(zip, xs), ys)), yss)
APP(app(combine, xs), app(app(cons, ys), yss)) → APP(combine, app(app(zip, xs), ys))
APP(app(combine, xs), app(app(cons, ys), yss)) → APP(app(zip, xs), ys)
APP(app(combine, xs), app(app(cons, ys), yss)) → APP(zip, xs)
APP(levels, app(app(node, x), xs)) → APP(app(cons, app(app(cons, x), nil)), app(app(combine, nil), app(app(map, levels), xs)))
APP(levels, app(app(node, x), xs)) → APP(cons, app(app(cons, x), nil))
APP(levels, app(app(node, x), xs)) → APP(app(cons, x), nil)
APP(levels, app(app(node, x), xs)) → APP(cons, x)
APP(levels, app(app(node, x), xs)) → APP(app(combine, nil), app(app(map, levels), xs))
APP(levels, app(app(node, x), xs)) → APP(combine, nil)
APP(levels, app(app(node, x), xs)) → APP(app(map, levels), xs)
APP(levels, app(app(node, x), xs)) → APP(map, levels)
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(append, xs), nil) → xs
app(app(append, nil), ys) → ys
app(app(append, app(app(cons, x), xs)), ys) → app(app(cons, x), app(app(append, xs), ys))
app(app(zip, nil), yss) → yss
app(app(zip, xss), nil) → xss
app(app(zip, app(app(cons, xs), xss)), app(app(cons, ys), yss)) → app(app(cons, app(app(append, xs), ys)), app(app(zip, xss), yss))
app(app(combine, xs), nil) → xs
app(app(combine, xs), app(app(cons, ys), yss)) → app(app(combine, app(app(zip, xs), ys)), yss)
app(levels, app(app(node, x), xs)) → app(app(cons, app(app(cons, x), nil)), app(app(combine, nil), app(app(map, levels), xs)))
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
app(app(append, x0), nil)
app(app(append, nil), x0)
app(app(append, app(app(cons, x0), x1)), x2)
app(app(zip, nil), x0)
app(app(zip, x0), nil)
app(app(zip, app(app(cons, x0), x1)), app(app(cons, x2), x3))
app(app(combine, x0), nil)
app(app(combine, x0), app(app(cons, x1), x2))
app(levels, app(app(node, x0), x1))
APP(app(append, app(app(cons, x), xs)), ys) → APP(app(append, xs), ys)
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(append, xs), nil) → xs
app(app(append, nil), ys) → ys
app(app(append, app(app(cons, x), xs)), ys) → app(app(cons, x), app(app(append, xs), ys))
app(app(zip, nil), yss) → yss
app(app(zip, xss), nil) → xss
app(app(zip, app(app(cons, xs), xss)), app(app(cons, ys), yss)) → app(app(cons, app(app(append, xs), ys)), app(app(zip, xss), yss))
app(app(combine, xs), nil) → xs
app(app(combine, xs), app(app(cons, ys), yss)) → app(app(combine, app(app(zip, xs), ys)), yss)
app(levels, app(app(node, x), xs)) → app(app(cons, app(app(cons, x), nil)), app(app(combine, nil), app(app(map, levels), xs)))
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
app(app(append, x0), nil)
app(app(append, nil), x0)
app(app(append, app(app(cons, x0), x1)), x2)
app(app(zip, nil), x0)
app(app(zip, x0), nil)
app(app(zip, app(app(cons, x0), x1)), app(app(cons, x2), x3))
app(app(combine, x0), nil)
app(app(combine, x0), app(app(cons, x1), x2))
app(levels, app(app(node, x0), x1))
APP(app(append, app(app(cons, x), xs)), ys) → APP(app(append, xs), ys)
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
app(app(append, x0), nil)
app(app(append, nil), x0)
app(app(append, app(app(cons, x0), x1)), x2)
app(app(zip, nil), x0)
app(app(zip, x0), nil)
app(app(zip, app(app(cons, x0), x1)), app(app(cons, x2), x3))
app(app(combine, x0), nil)
app(app(combine, x0), app(app(cons, x1), x2))
app(levels, app(app(node, x0), x1))
append1(cons(x, xs), ys) → append1(xs, ys)
map(x0, nil)
map(x0, cons(x1, x2))
append(x0, nil)
append(nil, x0)
append(cons(x0, x1), x2)
zip(nil, x0)
zip(x0, nil)
zip(cons(x0, x1), cons(x2, x3))
combine(x0, nil)
combine(x0, cons(x1, x2))
levels(node(x0, x1))
map(x0, nil)
map(x0, cons(x1, x2))
append(x0, nil)
append(nil, x0)
append(cons(x0, x1), x2)
zip(nil, x0)
zip(x0, nil)
zip(cons(x0, x1), cons(x2, x3))
combine(x0, nil)
combine(x0, cons(x1, x2))
levels(node(x0, x1))
append1(cons(x, xs), ys) → append1(xs, ys)
From the DPs we obtained the following set of size-change graphs:
APP(app(zip, app(app(cons, xs), xss)), app(app(cons, ys), yss)) → APP(app(zip, xss), yss)
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(append, xs), nil) → xs
app(app(append, nil), ys) → ys
app(app(append, app(app(cons, x), xs)), ys) → app(app(cons, x), app(app(append, xs), ys))
app(app(zip, nil), yss) → yss
app(app(zip, xss), nil) → xss
app(app(zip, app(app(cons, xs), xss)), app(app(cons, ys), yss)) → app(app(cons, app(app(append, xs), ys)), app(app(zip, xss), yss))
app(app(combine, xs), nil) → xs
app(app(combine, xs), app(app(cons, ys), yss)) → app(app(combine, app(app(zip, xs), ys)), yss)
app(levels, app(app(node, x), xs)) → app(app(cons, app(app(cons, x), nil)), app(app(combine, nil), app(app(map, levels), xs)))
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
app(app(append, x0), nil)
app(app(append, nil), x0)
app(app(append, app(app(cons, x0), x1)), x2)
app(app(zip, nil), x0)
app(app(zip, x0), nil)
app(app(zip, app(app(cons, x0), x1)), app(app(cons, x2), x3))
app(app(combine, x0), nil)
app(app(combine, x0), app(app(cons, x1), x2))
app(levels, app(app(node, x0), x1))
APP(app(zip, app(app(cons, xs), xss)), app(app(cons, ys), yss)) → APP(app(zip, xss), yss)
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
app(app(append, x0), nil)
app(app(append, nil), x0)
app(app(append, app(app(cons, x0), x1)), x2)
app(app(zip, nil), x0)
app(app(zip, x0), nil)
app(app(zip, app(app(cons, x0), x1)), app(app(cons, x2), x3))
app(app(combine, x0), nil)
app(app(combine, x0), app(app(cons, x1), x2))
app(levels, app(app(node, x0), x1))
zip1(cons(xs, xss), cons(ys, yss)) → zip1(xss, yss)
map(x0, nil)
map(x0, cons(x1, x2))
append(x0, nil)
append(nil, x0)
append(cons(x0, x1), x2)
zip(nil, x0)
zip(x0, nil)
zip(cons(x0, x1), cons(x2, x3))
combine(x0, nil)
combine(x0, cons(x1, x2))
levels(node(x0, x1))
map(x0, nil)
map(x0, cons(x1, x2))
append(x0, nil)
append(nil, x0)
append(cons(x0, x1), x2)
zip(nil, x0)
zip(x0, nil)
zip(cons(x0, x1), cons(x2, x3))
combine(x0, nil)
combine(x0, cons(x1, x2))
levels(node(x0, x1))
zip1(cons(xs, xss), cons(ys, yss)) → zip1(xss, yss)
From the DPs we obtained the following set of size-change graphs:
APP(app(combine, xs), app(app(cons, ys), yss)) → APP(app(combine, app(app(zip, xs), ys)), yss)
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(append, xs), nil) → xs
app(app(append, nil), ys) → ys
app(app(append, app(app(cons, x), xs)), ys) → app(app(cons, x), app(app(append, xs), ys))
app(app(zip, nil), yss) → yss
app(app(zip, xss), nil) → xss
app(app(zip, app(app(cons, xs), xss)), app(app(cons, ys), yss)) → app(app(cons, app(app(append, xs), ys)), app(app(zip, xss), yss))
app(app(combine, xs), nil) → xs
app(app(combine, xs), app(app(cons, ys), yss)) → app(app(combine, app(app(zip, xs), ys)), yss)
app(levels, app(app(node, x), xs)) → app(app(cons, app(app(cons, x), nil)), app(app(combine, nil), app(app(map, levels), xs)))
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
app(app(append, x0), nil)
app(app(append, nil), x0)
app(app(append, app(app(cons, x0), x1)), x2)
app(app(zip, nil), x0)
app(app(zip, x0), nil)
app(app(zip, app(app(cons, x0), x1)), app(app(cons, x2), x3))
app(app(combine, x0), nil)
app(app(combine, x0), app(app(cons, x1), x2))
app(levels, app(app(node, x0), x1))
APP(app(combine, xs), app(app(cons, ys), yss)) → APP(app(combine, app(app(zip, xs), ys)), yss)
app(app(zip, nil), yss) → yss
app(app(zip, xss), nil) → xss
app(app(zip, app(app(cons, xs), xss)), app(app(cons, ys), yss)) → app(app(cons, app(app(append, xs), ys)), app(app(zip, xss), yss))
app(app(append, xs), nil) → xs
app(app(append, nil), ys) → ys
app(app(append, app(app(cons, x), xs)), ys) → app(app(cons, x), app(app(append, xs), ys))
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
app(app(append, x0), nil)
app(app(append, nil), x0)
app(app(append, app(app(cons, x0), x1)), x2)
app(app(zip, nil), x0)
app(app(zip, x0), nil)
app(app(zip, app(app(cons, x0), x1)), app(app(cons, x2), x3))
app(app(combine, x0), nil)
app(app(combine, x0), app(app(cons, x1), x2))
app(levels, app(app(node, x0), x1))
combine1(xs, cons(ys, yss)) → combine1(zip(xs, ys), yss)
zip(nil, yss) → yss
zip(xss, nil) → xss
zip(cons(xs, xss), cons(ys, yss)) → cons(append(xs, ys), zip(xss, yss))
append(xs, nil) → xs
append(nil, ys) → ys
append(cons(x, xs), ys) → cons(x, append(xs, ys))
map(x0, nil)
map(x0, cons(x1, x2))
append(x0, nil)
append(nil, x0)
append(cons(x0, x1), x2)
zip(nil, x0)
zip(x0, nil)
zip(cons(x0, x1), cons(x2, x3))
combine(x0, nil)
combine(x0, cons(x1, x2))
levels(node(x0, x1))
map(x0, nil)
map(x0, cons(x1, x2))
combine(x0, nil)
combine(x0, cons(x1, x2))
levels(node(x0, x1))
combine1(xs, cons(ys, yss)) → combine1(zip(xs, ys), yss)
zip(nil, yss) → yss
zip(xss, nil) → xss
zip(cons(xs, xss), cons(ys, yss)) → cons(append(xs, ys), zip(xss, yss))
append(xs, nil) → xs
append(nil, ys) → ys
append(cons(x, xs), ys) → cons(x, append(xs, ys))
append(x0, nil)
append(nil, x0)
append(cons(x0, x1), x2)
zip(nil, x0)
zip(x0, nil)
zip(cons(x0, x1), cons(x2, x3))
From the DPs we obtained the following set of size-change graphs:
APP(app(map, f), app(app(cons, x), xs)) → APP(app(map, f), xs)
APP(app(map, f), app(app(cons, x), xs)) → APP(f, x)
APP(levels, app(app(node, x), xs)) → APP(app(map, levels), xs)
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(append, xs), nil) → xs
app(app(append, nil), ys) → ys
app(app(append, app(app(cons, x), xs)), ys) → app(app(cons, x), app(app(append, xs), ys))
app(app(zip, nil), yss) → yss
app(app(zip, xss), nil) → xss
app(app(zip, app(app(cons, xs), xss)), app(app(cons, ys), yss)) → app(app(cons, app(app(append, xs), ys)), app(app(zip, xss), yss))
app(app(combine, xs), nil) → xs
app(app(combine, xs), app(app(cons, ys), yss)) → app(app(combine, app(app(zip, xs), ys)), yss)
app(levels, app(app(node, x), xs)) → app(app(cons, app(app(cons, x), nil)), app(app(combine, nil), app(app(map, levels), xs)))
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
app(app(append, x0), nil)
app(app(append, nil), x0)
app(app(append, app(app(cons, x0), x1)), x2)
app(app(zip, nil), x0)
app(app(zip, x0), nil)
app(app(zip, app(app(cons, x0), x1)), app(app(cons, x2), x3))
app(app(combine, x0), nil)
app(app(combine, x0), app(app(cons, x1), x2))
app(levels, app(app(node, x0), x1))
APP(app(map, f), app(app(cons, x), xs)) → APP(app(map, f), xs)
APP(app(map, f), app(app(cons, x), xs)) → APP(f, x)
APP(levels, app(app(node, x), xs)) → APP(app(map, levels), xs)
app(app(map, x0), nil)
app(app(map, x0), app(app(cons, x1), x2))
app(app(append, x0), nil)
app(app(append, nil), x0)
app(app(append, app(app(cons, x0), x1)), x2)
app(app(zip, nil), x0)
app(app(zip, x0), nil)
app(app(zip, app(app(cons, x0), x1)), app(app(cons, x2), x3))
app(app(combine, x0), nil)
app(app(combine, x0), app(app(cons, x1), x2))
app(levels, app(app(node, x0), x1))
From the DPs we obtained the following set of size-change graphs: