Termination Proof using AProVE

Term Rewriting System R:
[a, s, t, 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(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 Termination of R to be shown.

     ↳Dependency Pair Analysis

R contains the following Dependency Pairs:

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 contains one SCC.

     ↳DPs

       →DP Problem 1

         ↳Narrowing Transformation

Dependency Pairs:

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

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

Strategy:

innermost

On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule

SORTSU(circ(sortSu(circ(sortSu(s), sortSu(t))), sortSu(u))) -> SORTSU(circ(sortSu(s), sortSu(circ(sortSu(t), sortSu(u)))))

six new Dependency Pairs are created:

SORTSU(circ(sortSu(circ(sortSu(s), sortSu(cons(te(a'), sortSu(s''))))), sortSu(u'))) -> SORTSU(circ(sortSu(s), sortSu(cons(te(msubst(te(a'), sortSu(u'))), sortSu(circ(sortSu(s''), sortSu(u')))))))
SORTSU(circ(sortSu(circ(sortSu(s), sortSu(cons(sop(lift), sortSu(s''))))), sortSu(cons(te(a'), sortSu(t''))))) -> SORTSU(circ(sortSu(s), sortSu(cons(te(a'), sortSu(circ(sortSu(s''), sortSu(t'')))))))
SORTSU(circ(sortSu(circ(sortSu(s), sortSu(cons(sop(lift), sortSu(s''))))), sortSu(cons(sop(lift), sortSu(t''))))) -> SORTSU(circ(sortSu(s), sortSu(cons(sop(lift), sortSu(circ(sortSu(s''), sortSu(t'')))))))
SORTSU(circ(sortSu(circ(sortSu(s), sortSu(circ(sortSu(s''), sortSu(t''))))), sortSu(u''))) -> SORTSU(circ(sortSu(s), sortSu(circ(sortSu(s''), sortSu(circ(sortSu(t''), sortSu(u'')))))))
SORTSU(circ(sortSu(circ(sortSu(s), sortSu(t'))), sortSu(id))) -> SORTSU(circ(sortSu(s), sortSu(t')))
SORTSU(circ(sortSu(circ(sortSu(s), sortSu(cons(sop(lift), sortSu(s''))))), sortSu(circ(sortSu(cons(sop(lift), sortSu(t''))), sortSu(u''))))) -> SORTSU(circ(sortSu(s), sortSu(circ(sortSu(cons(sop(lift), sortSu(circ(sortSu(s''), sortSu(t''))))), sortSu(u'')))))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Narrowing Transformation

Dependency Pairs:

SORTSU(circ(sortSu(circ(sortSu(s), sortSu(circ(sortSu(s''), sortSu(t''))))), sortSu(u''))) -> SORTSU(circ(sortSu(s), 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(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))) -> 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)))
SORTSU(circ(sortSu(cons(sop(lift), sortSu(s))), sortSu(circ(sortSu(cons(sop(lift), sortSu(t))), sortSu(u))))) -> SORTSU(circ(sortSu(s), sortSu(t)))

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

Strategy:

innermost

On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule

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

seven new Dependency Pairs are created:

SORTSU(circ(sortSu(cons(sop(lift), sortSu(cons(te(a'), sortSu(s''))))), sortSu(circ(sortSu(cons(sop(lift), sortSu(t''))), sortSu(u))))) -> SORTSU(circ(sortSu(cons(sop(lift), sortSu(cons(te(msubst(te(a'), sortSu(t''))), sortSu(circ(sortSu(s''), sortSu(t''))))))), sortSu(u)))
SORTSU(circ(sortSu(cons(sop(lift), sortSu(cons(sop(lift), sortSu(s''))))), sortSu(circ(sortSu(cons(sop(lift), sortSu(cons(te(a'), sortSu(t''))))), sortSu(u))))) -> SORTSU(circ(sortSu(cons(sop(lift), sortSu(cons(te(a'), sortSu(circ(sortSu(s''), sortSu(t''))))))), sortSu(u)))
SORTSU(circ(sortSu(cons(sop(lift), sortSu(cons(sop(lift), sortSu(s''))))), sortSu(circ(sortSu(cons(sop(lift), sortSu(cons(sop(lift), sortSu(t''))))), sortSu(u))))) -> SORTSU(circ(sortSu(cons(sop(lift), sortSu(cons(sop(lift), sortSu(circ(sortSu(s''), sortSu(t''))))))), sortSu(u)))
SORTSU(circ(sortSu(cons(sop(lift), sortSu(circ(sortSu(s''), sortSu(t''))))), sortSu(circ(sortSu(cons(sop(lift), sortSu(t0))), sortSu(u))))) -> SORTSU(circ(sortSu(cons(sop(lift), sortSu(circ(sortSu(s''), sortSu(circ(sortSu(t''), sortSu(t0))))))), sortSu(u)))
SORTSU(circ(sortSu(cons(sop(lift), sortSu(s''))), sortSu(circ(sortSu(cons(sop(lift), sortSu(id))), sortSu(u))))) -> SORTSU(circ(sortSu(cons(sop(lift), sortSu(s''))), sortSu(u)))
SORTSU(circ(sortSu(cons(sop(lift), sortSu(id))), sortSu(circ(sortSu(cons(sop(lift), sortSu(t'))), sortSu(u))))) -> SORTSU(circ(sortSu(cons(sop(lift), sortSu(t'))), sortSu(u)))
SORTSU(circ(sortSu(cons(sop(lift), sortSu(cons(sop(lift), sortSu(s''))))), sortSu(circ(sortSu(cons(sop(lift), sortSu(circ(sortSu(cons(sop(lift), sortSu(t''))), sortSu(u''))))), sortSu(u))))) -> SORTSU(circ(sortSu(cons(sop(lift), sortSu(circ(sortSu(cons(sop(lift), sortSu(circ(sortSu(s''), sortSu(t''))))), sortSu(u''))))), sortSu(u)))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 3

                 ↳Remaining Obligation(s)

The following remains to be proven:
Dependency Pairs:

SORTSU(circ(sortSu(cons(sop(lift), sortSu(cons(sop(lift), sortSu(s''))))), sortSu(circ(sortSu(cons(sop(lift), sortSu(circ(sortSu(cons(sop(lift), sortSu(t''))), sortSu(u''))))), sortSu(u))))) -> SORTSU(circ(sortSu(cons(sop(lift), sortSu(circ(sortSu(cons(sop(lift), sortSu(circ(sortSu(s''), sortSu(t''))))), sortSu(u''))))), sortSu(u)))
SORTSU(circ(sortSu(cons(sop(lift), sortSu(circ(sortSu(s''), sortSu(t''))))), sortSu(circ(sortSu(cons(sop(lift), sortSu(t0))), sortSu(u))))) -> SORTSU(circ(sortSu(cons(sop(lift), sortSu(circ(sortSu(s''), sortSu(circ(sortSu(t''), sortSu(t0))))))), sortSu(u)))
SORTSU(circ(sortSu(cons(sop(lift), sortSu(cons(sop(lift), sortSu(s''))))), sortSu(circ(sortSu(cons(sop(lift), sortSu(cons(sop(lift), sortSu(t''))))), sortSu(u))))) -> SORTSU(circ(sortSu(cons(sop(lift), sortSu(cons(sop(lift), sortSu(circ(sortSu(s''), sortSu(t''))))))), sortSu(u)))
SORTSU(circ(sortSu(cons(sop(lift), sortSu(cons(sop(lift), sortSu(s''))))), sortSu(circ(sortSu(cons(sop(lift), sortSu(cons(te(a'), sortSu(t''))))), sortSu(u))))) -> SORTSU(circ(sortSu(cons(sop(lift), sortSu(cons(te(a'), sortSu(circ(sortSu(s''), sortSu(t''))))))), sortSu(u)))
SORTSU(circ(sortSu(cons(sop(lift), sortSu(cons(te(a'), sortSu(s''))))), sortSu(circ(sortSu(cons(sop(lift), sortSu(t''))), sortSu(u))))) -> SORTSU(circ(sortSu(cons(sop(lift), sortSu(cons(te(msubst(te(a'), sortSu(t''))), 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(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)))
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)))
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(circ(sortSu(s''), sortSu(t''))))), sortSu(u''))) -> SORTSU(circ(sortSu(s), sortSu(circ(sortSu(s''), sortSu(circ(sortSu(t''), sortSu(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)))))

Strategy:

innermost

Innermost Termination of R could not be shown.
Duration:
0:14 minutes