(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
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(flatwith, f), app(leaf, x)) → app(app(cons, app(f, x)), nil)
app(app(flatwith, f), app(node, xs)) → app(app(flatwithsub, f), xs)
app(app(flatwithsub, f), nil) → nil
app(app(flatwithsub, f), app(app(cons, x), xs)) → app(app(append, app(app(flatwith, f), x)), app(app(flatwithsub, f), xs))
Q is empty.