0 QTRS
↳1 Overlay + Local Confluence (⇔)
↳2 QTRS
↳3 DependencyPairsProof (⇔)
↳4 QDP
↳5 DependencyGraphProof (⇔)
↳6 AND
↳7 QDP
↳8 UsableRulesProof (⇔)
↳9 QDP
↳10 ATransformationProof (⇔)
↳11 QDP
↳12 QReductionProof (⇔)
↳13 QDP
↳14 QDPSizeChangeProof (⇔)
↳15 TRUE
↳16 QDP
↳17 UsableRulesProof (⇔)
↳18 QDP
↳19 ATransformationProof (⇔)
↳20 QDP
↳21 QReductionProof (⇔)
↳22 QDP
↳23 QDPSizeChangeProof (⇔)
↳24 TRUE
↳25 QDP
↳26 UsableRulesProof (⇔)
↳27 QDP
↳28 ATransformationProof (⇔)
↳29 QDP
↳30 QReductionProof (⇔)
↳31 QDP
↳32 QDPSizeChangeProof (⇔)
↳33 TRUE
↳34 QDP
↳35 UsableRulesProof (⇔)
↳36 QDP
↳37 QDPSizeChangeProof (⇔)
↳38 TRUE
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: