(VAR a s t u)
(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))))))
(COMMENT Contribution by Eduardo Bonelli)
(STRATEGY INNERMOST)