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

↳Narrowing Transformation

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

On this DP problem, a Narrowing SCC transformation can be performed.

As a result of transforming the rule

six new Dependency Pairs are created:

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

R

↳DPs

→DP Problem 1

↳Nar

→DP Problem 2

↳Polynomial Ordering

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

The following dependency pairs can be strictly oriented:

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

Additionally, the following usable rules w.r.t. the implicit AFS can be oriented:

te(msubst(te(a), sortSu(id))) -> te(a)

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

sortSu(circ(sortSu(s), sortSu(id))) -> sortSu(s)

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

sortSu(circ(sortSu(id), sortSu(s))) -> sortSu(s)

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

Used ordering: Polynomial ordering with Polynomial interpretation:

_{ }^{ }POL(circ(x)_{1}, x_{2})= x _{1}+ x_{1}·x_{2}_{ }^{ }_{ }^{ }POL(TE(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(lift)= 0 _{ }^{ }_{ }^{ }POL(cons(x)_{1}, x_{2})= x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(subst(x)_{1}, x_{2})= 1 + x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(msubst(x)_{1}, x_{2})= x _{1}+ x_{1}·x_{2}+ x_{2}_{ }^{ }_{ }^{ }POL(SORTSU(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(te(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(id)= 0 _{ }^{ }_{ }^{ }POL(sortSu(x)_{1})= 1 + x _{1}_{ }^{ }_{ }^{ }POL(sop(x)_{1})= 0 _{ }^{ }

resulting in one new DP problem.

R

↳DPs

→DP Problem 1

↳Nar

→DP Problem 2

↳Polo

...

→DP Problem 3

↳Dependency Graph

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

Using the Dependency Graph resulted in no new DP problems.

Duration:

0:51 minutes