(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
sortSu(circ(sortSu(cons(te(a), sortSu(s))), sortSu(t))) → sortSu(cons(te(msubst(te(a), sortSu(t))), sortSu(circ(sortSu(s), sortSu(t)))))
sortSu(circ(sortSu(cons(sop(lift), sortSu(s))), sortSu(cons(te(a), sortSu(t))))) → sortSu(cons(te(a), sortSu(circ(sortSu(s), sortSu(t)))))
sortSu(circ(sortSu(cons(sop(lift), sortSu(s))), sortSu(cons(sop(lift), sortSu(t))))) → sortSu(cons(sop(lift), sortSu(circ(sortSu(s), sortSu(t)))))
sortSu(circ(sortSu(circ(sortSu(s), sortSu(t))), sortSu(u))) → sortSu(circ(sortSu(s), sortSu(circ(sortSu(t), sortSu(u)))))
sortSu(circ(sortSu(s), sortSu(id))) → sortSu(s)
sortSu(circ(sortSu(id), sortSu(s))) → sortSu(s)
sortSu(circ(sortSu(cons(sop(lift), sortSu(s))), sortSu(circ(sortSu(cons(sop(lift), sortSu(t))), sortSu(u))))) → sortSu(circ(sortSu(cons(sop(lift), sortSu(circ(sortSu(s), sortSu(t))))), sortSu(u)))
te(subst(te(a), sortSu(id))) → te(a)
te(msubst(te(a), sortSu(id))) → te(a)
te(msubst(te(msubst(te(a), sortSu(s))), sortSu(t))) → te(msubst(te(a), sortSu(circ(sortSu(s), sortSu(t)))))
Q is empty.