sortSu(circ(sortSu(cons(te(

sortSu(circ(sortSu(cons(sop(lift), sortSu(

sortSu(circ(sortSu(cons(sop(lift), sortSu(

sortSu(circ(sortSu(circ(sortSu(

sortSu(circ(sortSu(

sortSu(circ(sortSu(id), sortSu(

sortSu(circ(sortSu(cons(sop(lift), sortSu(

te(subst(te(

te(msubst(te(

te(msubst(te(msubst(te(

R

↳Dependency Pair Analysis

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(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(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(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(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(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)))

Furthermore,

R

↳DPs

→DP Problem 1

↳Remaining Obligation(s)

The following remains to be proven:

**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(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)))))

innermost

Duration:

0:02 minutes