Termination w.r.t. Q of the given QTRS could not be shown:

(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

app(app(app(fold, f), nil), x) → x
app(app(app(fold, f), app(app(cons, h), t)), x) → app(app(app(fold, f), t), app(app(f, x), h))
app(sum, l) → app(app(app(fold, add), l), 0)
app(app(app(fold, mul), l), 1) → app(prod, l)

Q is empty.