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(if, true), x), y) → x
app(app(app(if, false), x), y) → y
app(app(app(until, p), f), x) → app(app(app(if, app(p, x)), x), app(app(app(until, p), f), app(f, x)))

Q is empty.