MAYBE Problem: 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))))) Proof: DP Processor: DPs: sortSu#(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) -> sortSu#(circ(sortSu(s),sortSu(t))) sortSu#(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) -> te#(msubst(te(a),sortSu(t))) 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#(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#(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(t),sortSu(u))) sortSu#(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u))) -> sortSu#(circ(sortSu(s),sortSu(circ(sortSu(t),sortSu(u))))) sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu(cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(circ(sortSu(s),sortSu(t))) sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu(cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(cons(sop(lift()),sortSu(circ(sortSu(s),sortSu(t))))) 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#(msubst(te(msubst(te(a),sortSu(s))),sortSu(t))) -> sortSu#(circ(sortSu(s),sortSu(t))) te#(msubst(te(msubst(te(a),sortSu(s))),sortSu(t))) -> te#(msubst(te(a),sortSu(circ(sortSu(s),sortSu(t))))) TRS: 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))))) TDG Processor: DPs: sortSu#(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) -> sortSu#(circ(sortSu(s),sortSu(t))) sortSu#(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) -> te#(msubst(te(a),sortSu(t))) 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#(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#(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(t),sortSu(u))) sortSu#(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u))) -> sortSu#(circ(sortSu(s),sortSu(circ(sortSu(t),sortSu(u))))) sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(circ(sortSu(s),sortSu(t))) sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(cons(sop(lift()),sortSu(circ(sortSu(s),sortSu(t))))) 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#(msubst(te(msubst(te(a),sortSu(s))),sortSu(t))) -> sortSu#(circ(sortSu(s),sortSu(t))) te#(msubst(te(msubst(te(a),sortSu(s))),sortSu(t))) -> te#(msubst(te(a),sortSu(circ(sortSu(s),sortSu(t))))) TRS: 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))))) graph: te#(msubst(te(msubst(te(a),sortSu(s))),sortSu(t))) -> te#(msubst(te(a),sortSu(circ(sortSu(s),sortSu(t))))) -> te#(msubst(te(msubst(te(a),sortSu(s))),sortSu(t))) -> te#(msubst(te(a),sortSu(circ(sortSu(s),sortSu(t))))) te#(msubst(te(msubst(te(a),sortSu(s))),sortSu(t))) -> te#(msubst(te(a),sortSu(circ(sortSu(s),sortSu(t))))) -> te#(msubst(te(msubst(te(a),sortSu(s))),sortSu(t))) -> sortSu#(circ(sortSu(s),sortSu(t))) te#(msubst(te(msubst(te(a),sortSu(s))),sortSu(t))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> 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#(msubst(te(msubst(te(a),sortSu(s))),sortSu(t))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(cons(sop(lift()),sortSu(circ(sortSu(s),sortSu(t))))) te#(msubst(te(msubst(te(a),sortSu(s))),sortSu(t))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(circ(sortSu(s),sortSu(t))) te#(msubst(te(msubst(te(a),sortSu(s))),sortSu(t))) -> 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))))) te#(msubst(te(msubst(te(a),sortSu(s))),sortSu(t))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u))) -> sortSu#(circ(sortSu(t),sortSu(u))) te#(msubst(te(msubst(te(a),sortSu(s))),sortSu(t))) -> 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))))) te#(msubst(te(msubst(te(a),sortSu(s))),sortSu(t))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(sop(lift()),sortSu(t))))) -> sortSu#(circ(sortSu(s),sortSu(t))) te#(msubst(te(msubst(te(a),sortSu(s))),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))))) te#(msubst(te(msubst(te(a),sortSu(s))),sortSu(t))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(te(a),sortSu(t))))) -> sortSu#(circ(sortSu(s),sortSu(t))) te#(msubst(te(msubst(te(a),sortSu(s))),sortSu(t))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) -> sortSu#(cons(te(msubst(te(a),sortSu(t))),sortSu(circ(sortSu(s),sortSu(t))))) te#(msubst(te(msubst(te(a),sortSu(s))),sortSu(t))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) -> te#(msubst(te(a),sortSu(t))) te#(msubst(te(msubst(te(a),sortSu(s))),sortSu(t))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) -> sortSu#(circ(sortSu(s),sortSu(t))) sortSu#(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u))) -> sortSu#(circ(sortSu(t),sortSu(u))) -> 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))) sortSu#(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u))) -> sortSu#(circ(sortSu(t),sortSu(u))) -> sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(cons(sop(lift()),sortSu(circ(sortSu(s),sortSu(t))))) sortSu#(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u))) -> sortSu#(circ(sortSu(t),sortSu(u))) -> sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(circ(sortSu(s),sortSu(t))) sortSu#(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u))) -> sortSu#(circ(sortSu(t),sortSu(u))) -> sortSu#(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u))) -> sortSu#(circ(sortSu(s),sortSu(circ(sortSu(t),sortSu(u))))) sortSu#(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u))) -> sortSu#(circ(sortSu(t),sortSu(u))) -> sortSu#(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u))) -> sortSu#(circ(sortSu(t),sortSu(u))) sortSu#(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u))) -> sortSu#(circ(sortSu(t),sortSu(u))) -> 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(t),sortSu(u))) -> sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(sop(lift()),sortSu(t))))) -> sortSu#(circ(sortSu(s),sortSu(t))) sortSu#(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u))) -> sortSu#(circ(sortSu(t),sortSu(u))) -> 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(circ(sortSu(s),sortSu(t))),sortSu(u))) -> sortSu#(circ(sortSu(t),sortSu(u))) -> sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(te(a),sortSu(t))))) -> sortSu#(circ(sortSu(s),sortSu(t))) sortSu#(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u))) -> sortSu#(circ(sortSu(t),sortSu(u))) -> 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(circ(sortSu(s),sortSu(t))),sortSu(u))) -> sortSu#(circ(sortSu(t),sortSu(u))) -> sortSu#(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) -> te#(msubst(te(a),sortSu(t))) sortSu#(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u))) -> sortSu#(circ(sortSu(t),sortSu(u))) -> sortSu#(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) -> 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(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))) sortSu#(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u))) -> sortSu#(circ(sortSu(s),sortSu(circ(sortSu(t),sortSu(u))))) -> sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> 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(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> 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(circ(sortSu(s),sortSu(t))),sortSu(u))) -> sortSu#(circ(sortSu(s),sortSu(circ(sortSu(t),sortSu(u))))) sortSu#(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u))) -> sortSu#(circ(sortSu(s),sortSu(circ(sortSu(t),sortSu(u))))) -> sortSu#(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u))) -> sortSu#(circ(sortSu(t),sortSu(u))) sortSu#(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u))) -> sortSu#(circ(sortSu(s),sortSu(circ(sortSu(t),sortSu(u))))) -> 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(cons(sop(lift()),sortSu(s))),sortSu(cons(sop(lift()),sortSu(t))))) -> 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(cons(sop(lift()),sortSu(s))),sortSu(cons(te(a),sortSu(t))))) -> sortSu#(cons(te(a),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(cons(sop(lift()),sortSu(s))),sortSu(cons(te(a),sortSu(t))))) -> 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(cons(te(a),sortSu(s))),sortSu(t))) -> sortSu#(cons(te(msubst(te(a),sortSu(t))),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(cons(te(a),sortSu(s))),sortSu(t))) -> te#(msubst(te(a),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(cons(te(a),sortSu(s))),sortSu(t))) -> sortSu#(circ(sortSu(s),sortSu(t))) 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))) -> 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))) 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))) -> sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(cons(sop(lift()),sortSu(circ(sortSu(s),sortSu(t))))) 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))) -> sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(circ(sortSu(s),sortSu(t))) 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))) -> sortSu#(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u))) -> sortSu#(circ(sortSu(s),sortSu(circ(sortSu(t),sortSu(u))))) 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))) -> sortSu#(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u))) -> sortSu#(circ(sortSu(t),sortSu(u))) 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))) -> 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(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))) -> sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(sop(lift()),sortSu(t))))) -> sortSu#(circ(sortSu(s),sortSu(t))) 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))) -> 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(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(circ(sortSu(cons(sop(lift()),sortSu(circ(sortSu(s),sortSu(t))))),sortSu(u))) -> sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(te(a),sortSu(t))))) -> sortSu#(circ(sortSu(s),sortSu(t))) 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))) -> 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(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(circ(sortSu(cons(sop(lift()),sortSu(circ(sortSu(s),sortSu(t))))),sortSu(u))) -> sortSu#(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) -> te#(msubst(te(a),sortSu(t))) 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))) -> sortSu#(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) -> sortSu#(circ(sortSu(s),sortSu(t))) sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> 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))) sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(cons(sop(lift()),sortSu(circ(sortSu(s),sortSu(t))))) sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(circ(sortSu(s),sortSu(t))) sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> 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(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u))) -> sortSu#(circ(sortSu(t),sortSu(u))) sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> 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(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(sop(lift()),sortSu(t))))) -> sortSu#(circ(sortSu(s),sortSu(t))) sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> 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(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(te(a),sortSu(t))))) -> sortSu#(circ(sortSu(s),sortSu(t))) sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> 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(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) -> te#(msubst(te(a),sortSu(t))) sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) -> sortSu#(circ(sortSu(s),sortSu(t))) sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(cons(sop(lift()),sortSu(circ(sortSu(s),sortSu(t))))) -> 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))) sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(cons(sop(lift()),sortSu(circ(sortSu(s),sortSu(t))))) -> sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(cons(sop(lift()),sortSu(circ(sortSu(s),sortSu(t))))) sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(cons(sop(lift()),sortSu(circ(sortSu(s),sortSu(t))))) -> sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(circ(sortSu(s),sortSu(t))) sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> 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(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(cons(sop(lift()),sortSu(circ(sortSu(s),sortSu(t))))) -> sortSu#(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u))) -> sortSu#(circ(sortSu(t),sortSu(u))) sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(cons(sop(lift()),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(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(cons(sop(lift()),sortSu(circ(sortSu(s),sortSu(t))))) -> sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(sop(lift()),sortSu(t))))) -> sortSu#(circ(sortSu(s),sortSu(t))) sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(cons(sop(lift()),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(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(cons(sop(lift()),sortSu(circ(sortSu(s),sortSu(t))))) -> sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(te(a),sortSu(t))))) -> sortSu#(circ(sortSu(s),sortSu(t))) sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(cons(sop(lift()),sortSu(circ(sortSu(s),sortSu(t))))) -> 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(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(cons(sop(lift()),sortSu(circ(sortSu(s),sortSu(t))))) -> sortSu#(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) -> te#(msubst(te(a),sortSu(t))) sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(cons(sop(lift()),sortSu(circ(sortSu(s),sortSu(t))))) -> sortSu#(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) -> sortSu#(circ(sortSu(s),sortSu(t))) sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(sop(lift()),sortSu(t))))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> 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))) sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(sop(lift()),sortSu(t))))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(cons(sop(lift()),sortSu(circ(sortSu(s),sortSu(t))))) sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(sop(lift()),sortSu(t))))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(circ(sortSu(s),sortSu(t))) sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(sop(lift()),sortSu(t))))) -> 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(cons(sop(lift()),sortSu(s))),sortSu(cons(sop(lift()),sortSu(t))))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u))) -> sortSu#(circ(sortSu(t),sortSu(u))) sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(sop(lift()),sortSu(t))))) -> 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(cons(sop(lift()),sortSu(s))),sortSu(cons(sop(lift()),sortSu(t))))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(sop(lift()),sortSu(t))))) -> sortSu#(circ(sortSu(s),sortSu(t))) sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(sop(lift()),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#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(te(a),sortSu(t))))) -> sortSu#(circ(sortSu(s),sortSu(t))) sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(sop(lift()),sortSu(t))))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> 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(sop(lift()),sortSu(t))))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) -> te#(msubst(te(a),sortSu(t))) sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(sop(lift()),sortSu(t))))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) -> 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(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))) 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(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(cons(sop(lift()),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(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> 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(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(t),sortSu(u))) 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(cons(sop(lift()),sortSu(s))),sortSu(cons(sop(lift()),sortSu(t))))) -> sortSu#(cons(sop(lift()),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(cons(sop(lift()),sortSu(s))),sortSu(cons(sop(lift()),sortSu(t))))) -> 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(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(cons(sop(lift()),sortSu(s))),sortSu(cons(te(a),sortSu(t))))) -> 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(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(sop(lift()),sortSu(t))))) -> sortSu#(cons(sop(lift()),sortSu(circ(sortSu(s),sortSu(t))))) -> sortSu#(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) -> te#(msubst(te(a),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(cons(te(a),sortSu(s))),sortSu(t))) -> sortSu#(circ(sortSu(s),sortSu(t))) sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(te(a),sortSu(t))))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> 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))) sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(te(a),sortSu(t))))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(cons(sop(lift()),sortSu(circ(sortSu(s),sortSu(t))))) sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(te(a),sortSu(t))))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(circ(sortSu(s),sortSu(t))) sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(te(a),sortSu(t))))) -> 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(cons(sop(lift()),sortSu(s))),sortSu(cons(te(a),sortSu(t))))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u))) -> sortSu#(circ(sortSu(t),sortSu(u))) sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(te(a),sortSu(t))))) -> 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(cons(sop(lift()),sortSu(s))),sortSu(cons(te(a),sortSu(t))))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(sop(lift()),sortSu(t))))) -> sortSu#(circ(sortSu(s),sortSu(t))) sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(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(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#(circ(sortSu(s),sortSu(t))) sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(te(a),sortSu(t))))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> 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#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) -> te#(msubst(te(a),sortSu(t))) sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(te(a),sortSu(t))))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(cons(te(a),sortSu(s))),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(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(circ(sortSu(cons(sop(lift()),sortSu(circ(sortSu(s),sortSu(t))))),sortSu(u))) 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(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(cons(sop(lift()),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(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> 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(circ(sortSu(s),sortSu(t))),sortSu(u))) -> sortSu#(circ(sortSu(s),sortSu(circ(sortSu(t),sortSu(u))))) 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(circ(sortSu(s),sortSu(t))),sortSu(u))) -> sortSu#(circ(sortSu(t),sortSu(u))) 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(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#(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(te(a),sortSu(t))))) -> sortSu#(cons(te(a),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(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(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(te(a),sortSu(s))),sortSu(t))) -> te#(msubst(te(a),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(te(a),sortSu(s))),sortSu(t))) -> sortSu#(circ(sortSu(s),sortSu(t))) sortSu#(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) -> te#(msubst(te(a),sortSu(t))) -> te#(msubst(te(msubst(te(a),sortSu(s))),sortSu(t))) -> te#(msubst(te(a),sortSu(circ(sortSu(s),sortSu(t))))) sortSu#(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) -> te#(msubst(te(a),sortSu(t))) -> te#(msubst(te(msubst(te(a),sortSu(s))),sortSu(t))) -> sortSu#(circ(sortSu(s),sortSu(t))) sortSu#(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> 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))) sortSu#(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(cons(sop(lift()),sortSu(circ(sortSu(s),sortSu(t))))) sortSu#(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(circ(sortSu(s),sortSu(t))) sortSu#(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) -> 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(cons(te(a),sortSu(s))),sortSu(t))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u))) -> sortSu#(circ(sortSu(t),sortSu(u))) sortSu#(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) -> 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(cons(te(a),sortSu(s))),sortSu(t))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(sop(lift()),sortSu(t))))) -> sortSu#(circ(sortSu(s),sortSu(t))) sortSu#(circ(sortSu(cons(te(a),sortSu(s))),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(te(a),sortSu(s))),sortSu(t))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(te(a),sortSu(t))))) -> sortSu#(circ(sortSu(s),sortSu(t))) sortSu#(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> 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(te(a),sortSu(s))),sortSu(t))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) -> te#(msubst(te(a),sortSu(t))) sortSu#(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) -> sortSu#(circ(sortSu(s),sortSu(t))) 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(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(circ(sortSu(cons(sop(lift()),sortSu(circ(sortSu(s),sortSu(t))))),sortSu(u))) 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(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(cons(sop(lift()),sortSu(circ(sortSu(s),sortSu(t))))) 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(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(circ(sortSu(s),sortSu(t))) 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(circ(sortSu(s),sortSu(t))),sortSu(u))) -> sortSu#(circ(sortSu(s),sortSu(circ(sortSu(t),sortSu(u))))) 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(circ(sortSu(s),sortSu(t))),sortSu(u))) -> sortSu#(circ(sortSu(t),sortSu(u))) 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(sop(lift()),sortSu(t))))) -> sortSu#(cons(sop(lift()),sortSu(circ(sortSu(s),sortSu(t))))) 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(sop(lift()),sortSu(t))))) -> sortSu#(circ(sortSu(s),sortSu(t))) 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(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#(circ(sortSu(s),sortSu(t))) 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(te(a),sortSu(s))),sortSu(t))) -> sortSu#(cons(te(msubst(te(a),sortSu(t))),sortSu(circ(sortSu(s),sortSu(t))))) 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(te(a),sortSu(s))),sortSu(t))) -> te#(msubst(te(a),sortSu(t))) 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(te(a),sortSu(s))),sortSu(t))) -> sortSu#(circ(sortSu(s),sortSu(t))) EDG Processor: DPs: sortSu#(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) -> sortSu#(circ(sortSu(s),sortSu(t))) sortSu#(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) -> te#(msubst(te(a),sortSu(t))) 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#(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#(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(t),sortSu(u))) sortSu#(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u))) -> sortSu#(circ(sortSu(s),sortSu(circ(sortSu(t),sortSu(u))))) sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(circ(sortSu(s),sortSu(t))) sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(cons(sop(lift()),sortSu(circ(sortSu(s),sortSu(t))))) 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#(msubst(te(msubst(te(a),sortSu(s))),sortSu(t))) -> sortSu#(circ(sortSu(s),sortSu(t))) te#(msubst(te(msubst(te(a),sortSu(s))),sortSu(t))) -> te#(msubst(te(a),sortSu(circ(sortSu(s),sortSu(t))))) TRS: 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))))) graph: te#(msubst(te(msubst(te(a),sortSu(s))),sortSu(t))) -> te#(msubst(te(a),sortSu(circ(sortSu(s),sortSu(t))))) -> te#(msubst(te(msubst(te(a),sortSu(s))),sortSu(t))) -> sortSu#(circ(sortSu(s),sortSu(t))) te#(msubst(te(msubst(te(a),sortSu(s))),sortSu(t))) -> te#(msubst(te(a),sortSu(circ(sortSu(s),sortSu(t))))) -> te#(msubst(te(msubst(te(a),sortSu(s))),sortSu(t))) -> te#(msubst(te(a),sortSu(circ(sortSu(s),sortSu(t))))) te#(msubst(te(msubst(te(a),sortSu(s))),sortSu(t))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) -> sortSu#(circ(sortSu(s),sortSu(t))) te#(msubst(te(msubst(te(a),sortSu(s))),sortSu(t))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) -> te#(msubst(te(a),sortSu(t))) te#(msubst(te(msubst(te(a),sortSu(s))),sortSu(t))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) -> sortSu#(cons(te(msubst(te(a),sortSu(t))),sortSu(circ(sortSu(s),sortSu(t))))) te#(msubst(te(msubst(te(a),sortSu(s))),sortSu(t))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(te(a),sortSu(t))))) -> sortSu#(circ(sortSu(s),sortSu(t))) te#(msubst(te(msubst(te(a),sortSu(s))),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))))) te#(msubst(te(msubst(te(a),sortSu(s))),sortSu(t))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(sop(lift()),sortSu(t))))) -> sortSu#(circ(sortSu(s),sortSu(t))) te#(msubst(te(msubst(te(a),sortSu(s))),sortSu(t))) -> 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))))) te#(msubst(te(msubst(te(a),sortSu(s))),sortSu(t))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u))) -> sortSu#(circ(sortSu(t),sortSu(u))) te#(msubst(te(msubst(te(a),sortSu(s))),sortSu(t))) -> 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))))) te#(msubst(te(msubst(te(a),sortSu(s))),sortSu(t))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(circ(sortSu(s),sortSu(t))) te#(msubst(te(msubst(te(a),sortSu(s))),sortSu(t))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(cons(sop(lift()),sortSu(circ(sortSu(s),sortSu(t))))) te#(msubst(te(msubst(te(a),sortSu(s))),sortSu(t))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> 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))) sortSu#(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u))) -> sortSu#(circ(sortSu(t),sortSu(u))) -> sortSu#(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) -> sortSu#(circ(sortSu(s),sortSu(t))) sortSu#(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u))) -> sortSu#(circ(sortSu(t),sortSu(u))) -> sortSu#(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) -> te#(msubst(te(a),sortSu(t))) sortSu#(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u))) -> sortSu#(circ(sortSu(t),sortSu(u))) -> 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(circ(sortSu(s),sortSu(t))),sortSu(u))) -> sortSu#(circ(sortSu(t),sortSu(u))) -> sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(te(a),sortSu(t))))) -> sortSu#(circ(sortSu(s),sortSu(t))) sortSu#(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u))) -> sortSu#(circ(sortSu(t),sortSu(u))) -> 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(circ(sortSu(s),sortSu(t))),sortSu(u))) -> sortSu#(circ(sortSu(t),sortSu(u))) -> sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(sop(lift()),sortSu(t))))) -> sortSu#(circ(sortSu(s),sortSu(t))) sortSu#(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u))) -> sortSu#(circ(sortSu(t),sortSu(u))) -> 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(t),sortSu(u))) -> sortSu#(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u))) -> sortSu#(circ(sortSu(t),sortSu(u))) sortSu#(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u))) -> sortSu#(circ(sortSu(t),sortSu(u))) -> sortSu#(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u))) -> sortSu#(circ(sortSu(s),sortSu(circ(sortSu(t),sortSu(u))))) sortSu#(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u))) -> sortSu#(circ(sortSu(t),sortSu(u))) -> sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(circ(sortSu(s),sortSu(t))) sortSu#(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u))) -> sortSu#(circ(sortSu(t),sortSu(u))) -> sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(cons(sop(lift()),sortSu(circ(sortSu(s),sortSu(t))))) sortSu#(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u))) -> sortSu#(circ(sortSu(t),sortSu(u))) -> 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))) sortSu#(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u))) -> sortSu#(circ(sortSu(s),sortSu(circ(sortSu(t),sortSu(u))))) -> sortSu#(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) -> 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(cons(te(a),sortSu(s))),sortSu(t))) -> te#(msubst(te(a),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(cons(te(a),sortSu(s))),sortSu(t))) -> sortSu#(cons(te(msubst(te(a),sortSu(t))),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(cons(sop(lift()),sortSu(s))),sortSu(cons(te(a),sortSu(t))))) -> 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(cons(sop(lift()),sortSu(s))),sortSu(cons(te(a),sortSu(t))))) -> sortSu#(cons(te(a),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(cons(sop(lift()),sortSu(s))),sortSu(cons(sop(lift()),sortSu(t))))) -> 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(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(circ(sortSu(s),sortSu(t))),sortSu(u))) -> sortSu#(circ(sortSu(t),sortSu(u))) sortSu#(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u))) -> sortSu#(circ(sortSu(s),sortSu(circ(sortSu(t),sortSu(u))))) -> sortSu#(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u))) -> sortSu#(circ(sortSu(s),sortSu(circ(sortSu(t),sortSu(u))))) sortSu#(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u))) -> sortSu#(circ(sortSu(s),sortSu(circ(sortSu(t),sortSu(u))))) -> sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> 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(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> 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(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))) 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))) -> sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(te(a),sortSu(t))))) -> sortSu#(circ(sortSu(s),sortSu(t))) 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))) -> 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(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(circ(sortSu(cons(sop(lift()),sortSu(circ(sortSu(s),sortSu(t))))),sortSu(u))) -> sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(sop(lift()),sortSu(t))))) -> sortSu#(circ(sortSu(s),sortSu(t))) 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))) -> 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(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))) -> sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(circ(sortSu(s),sortSu(t))) 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))) -> sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(cons(sop(lift()),sortSu(circ(sortSu(s),sortSu(t))))) 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))) -> 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))) sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) -> sortSu#(circ(sortSu(s),sortSu(t))) sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) -> te#(msubst(te(a),sortSu(t))) sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> 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(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(te(a),sortSu(t))))) -> sortSu#(circ(sortSu(s),sortSu(t))) sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> 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(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(sop(lift()),sortSu(t))))) -> sortSu#(circ(sortSu(s),sortSu(t))) sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> 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(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u))) -> sortSu#(circ(sortSu(t),sortSu(u))) sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> 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(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(circ(sortSu(s),sortSu(t))) sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(cons(sop(lift()),sortSu(circ(sortSu(s),sortSu(t))))) sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> 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))) sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(sop(lift()),sortSu(t))))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) -> sortSu#(circ(sortSu(s),sortSu(t))) sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(sop(lift()),sortSu(t))))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) -> te#(msubst(te(a),sortSu(t))) sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(sop(lift()),sortSu(t))))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> 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(sop(lift()),sortSu(t))))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(te(a),sortSu(t))))) -> sortSu#(circ(sortSu(s),sortSu(t))) sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(sop(lift()),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#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(sop(lift()),sortSu(t))))) -> sortSu#(circ(sortSu(s),sortSu(t))) sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(sop(lift()),sortSu(t))))) -> 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(cons(sop(lift()),sortSu(s))),sortSu(cons(sop(lift()),sortSu(t))))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u))) -> sortSu#(circ(sortSu(t),sortSu(u))) sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(sop(lift()),sortSu(t))))) -> 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(cons(sop(lift()),sortSu(s))),sortSu(cons(sop(lift()),sortSu(t))))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(circ(sortSu(s),sortSu(t))) sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(sop(lift()),sortSu(t))))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(cons(sop(lift()),sortSu(circ(sortSu(s),sortSu(t))))) sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(sop(lift()),sortSu(t))))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> 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))) sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(te(a),sortSu(t))))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) -> sortSu#(circ(sortSu(s),sortSu(t))) sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(te(a),sortSu(t))))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) -> te#(msubst(te(a),sortSu(t))) sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(te(a),sortSu(t))))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> 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#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(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#(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(te(a),sortSu(t))))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(sop(lift()),sortSu(t))))) -> sortSu#(circ(sortSu(s),sortSu(t))) sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(te(a),sortSu(t))))) -> 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(cons(sop(lift()),sortSu(s))),sortSu(cons(te(a),sortSu(t))))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u))) -> sortSu#(circ(sortSu(t),sortSu(u))) sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(te(a),sortSu(t))))) -> 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(cons(sop(lift()),sortSu(s))),sortSu(cons(te(a),sortSu(t))))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(circ(sortSu(s),sortSu(t))) sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(te(a),sortSu(t))))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(cons(sop(lift()),sortSu(circ(sortSu(s),sortSu(t))))) sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(te(a),sortSu(t))))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> 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))) sortSu#(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) -> te#(msubst(te(a),sortSu(t))) -> te#(msubst(te(msubst(te(a),sortSu(s))),sortSu(t))) -> sortSu#(circ(sortSu(s),sortSu(t))) sortSu#(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) -> te#(msubst(te(a),sortSu(t))) -> te#(msubst(te(msubst(te(a),sortSu(s))),sortSu(t))) -> te#(msubst(te(a),sortSu(circ(sortSu(s),sortSu(t))))) sortSu#(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) -> sortSu#(circ(sortSu(s),sortSu(t))) sortSu#(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) -> te#(msubst(te(a),sortSu(t))) sortSu#(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> 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(te(a),sortSu(s))),sortSu(t))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(te(a),sortSu(t))))) -> sortSu#(circ(sortSu(s),sortSu(t))) sortSu#(circ(sortSu(cons(te(a),sortSu(s))),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(te(a),sortSu(s))),sortSu(t))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(sop(lift()),sortSu(t))))) -> sortSu#(circ(sortSu(s),sortSu(t))) sortSu#(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) -> 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(cons(te(a),sortSu(s))),sortSu(t))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(circ(sortSu(s),sortSu(t))),sortSu(u))) -> sortSu#(circ(sortSu(t),sortSu(u))) sortSu#(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) -> 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(cons(te(a),sortSu(s))),sortSu(t))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(circ(sortSu(s),sortSu(t))) sortSu#(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> sortSu#(cons(sop(lift()),sortSu(circ(sortSu(s),sortSu(t))))) sortSu#(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) -> sortSu#(circ(sortSu(s),sortSu(t))) -> 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))) SCC Processor: #sccs: 1 #rules: 10 #arcs: 95/196 DPs: te#(msubst(te(msubst(te(a),sortSu(s))),sortSu(t))) -> te#(msubst(te(a),sortSu(circ(sortSu(s),sortSu(t))))) te#(msubst(te(msubst(te(a),sortSu(s))),sortSu(t))) -> sortSu#(circ(sortSu(s),sortSu(t))) 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))) sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(circ(sortSu (cons(sop(lift()),sortSu(t))), sortSu (u))))) -> 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(circ(sortSu(s),sortSu(t))),sortSu(u))) -> sortSu#(circ(sortSu(t),sortSu(u))) sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(sop(lift()),sortSu(t))))) -> sortSu#(circ(sortSu(s),sortSu(t))) sortSu#(circ(sortSu(cons(sop(lift()),sortSu(s))),sortSu(cons(te(a),sortSu(t))))) -> sortSu#(circ(sortSu(s),sortSu(t))) sortSu#(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) -> te#(msubst(te(a),sortSu(t))) sortSu#(circ(sortSu(cons(te(a),sortSu(s))),sortSu(t))) -> sortSu#(circ(sortSu(s),sortSu(t))) TRS: 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))))) Open