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:

circ(cons(a, s), t) → cons(msubst(a, t), circ(s, t))
circ(cons(lift, s), cons(a, t)) → cons(a, circ(s, t))
circ(cons(lift, s), cons(lift, t)) → cons(lift, circ(s, t))
circ(circ(s, t), u) → circ(s, circ(t, u))
circ(s, id) → s
circ(id, s) → s
circ(cons(lift, s), circ(cons(lift, t), u)) → circ(cons(lift, circ(s, t)), u)
subst(a, id) → a
msubst(a, id) → a
msubst(msubst(a, s), t) → msubst(a, circ(s, t))

Q is empty.