Runtime Complexity (innermost) proof of /tmp/tmpGNimn5/cime1.xml

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(1)).

0 CpxTRS

↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID), 185 ms)

↳2 CdtProblem

↳3 CdtUnreachableProof (⇔, 0 ms)

↳4 CdtProblem

↳5 SIsEmptyProof (⇔, 0 ms)

↳6 BOUNDS(O(1), O(1))

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following 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)))))

Rewrite Strategy: INNERMOST

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted CpxTRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

sortSu(circ(sortSu(cons(te(z0), sortSu(z1))), sortSu(z2))) → sortSu(cons(te(msubst(te(z0), sortSu(z2))), sortSu(circ(sortSu(z1), sortSu(z2)))))
sortSu(circ(sortSu(cons(sop(lift), sortSu(z0))), sortSu(cons(te(z1), sortSu(z2))))) → sortSu(cons(te(z1), sortSu(circ(sortSu(z0), sortSu(z2)))))
sortSu(circ(sortSu(cons(sop(lift), sortSu(z0))), sortSu(cons(sop(lift), sortSu(z1))))) → sortSu(cons(sop(lift), sortSu(circ(sortSu(z0), sortSu(z1)))))
sortSu(circ(sortSu(circ(sortSu(z0), sortSu(z1))), sortSu(z2))) → sortSu(circ(sortSu(z0), sortSu(circ(sortSu(z1), sortSu(z2)))))
sortSu(circ(sortSu(z0), sortSu(id))) → sortSu(z0)
sortSu(circ(sortSu(id), sortSu(z0))) → sortSu(z0)
sortSu(circ(sortSu(cons(sop(lift), sortSu(z0))), sortSu(circ(sortSu(cons(sop(lift), sortSu(z1))), sortSu(z2))))) → sortSu(circ(sortSu(cons(sop(lift), sortSu(circ(sortSu(z0), sortSu(z1))))), sortSu(z2)))
te(subst(te(z0), sortSu(id))) → te(z0)
te(msubst(te(z0), sortSu(id))) → te(z0)
te(msubst(te(msubst(te(z0), sortSu(z1))), sortSu(z2))) → te(msubst(te(z0), sortSu(circ(sortSu(z1), sortSu(z2)))))

Tuples:

SORTSU(circ(sortSu(cons(te(z0), sortSu(z1))), sortSu(z2))) → c(SORTSU(cons(te(msubst(te(z0), sortSu(z2))), sortSu(circ(sortSu(z1), sortSu(z2))))), TE(msubst(te(z0), sortSu(z2))), TE(z0), SORTSU(z2), SORTSU(circ(sortSu(z1), sortSu(z2))), SORTSU(z1), SORTSU(z2))
SORTSU(circ(sortSu(cons(sop(lift), sortSu(z0))), sortSu(cons(te(z1), sortSu(z2))))) → c1(SORTSU(cons(te(z1), sortSu(circ(sortSu(z0), sortSu(z2))))), TE(z1), SORTSU(circ(sortSu(z0), sortSu(z2))), SORTSU(z0), SORTSU(z2))
SORTSU(circ(sortSu(cons(sop(lift), sortSu(z0))), sortSu(cons(sop(lift), sortSu(z1))))) → c2(SORTSU(cons(sop(lift), sortSu(circ(sortSu(z0), sortSu(z1))))), SORTSU(circ(sortSu(z0), sortSu(z1))), SORTSU(z0), SORTSU(z1))
SORTSU(circ(sortSu(circ(sortSu(z0), sortSu(z1))), sortSu(z2))) → c3(SORTSU(circ(sortSu(z0), sortSu(circ(sortSu(z1), sortSu(z2))))), SORTSU(z0), SORTSU(circ(sortSu(z1), sortSu(z2))), SORTSU(z1), SORTSU(z2))
SORTSU(circ(sortSu(z0), sortSu(id))) → c4(SORTSU(z0))
SORTSU(circ(sortSu(id), sortSu(z0))) → c5(SORTSU(z0))
SORTSU(circ(sortSu(cons(sop(lift), sortSu(z0))), sortSu(circ(sortSu(cons(sop(lift), sortSu(z1))), sortSu(z2))))) → c6(SORTSU(circ(sortSu(cons(sop(lift), sortSu(circ(sortSu(z0), sortSu(z1))))), sortSu(z2))), SORTSU(cons(sop(lift), sortSu(circ(sortSu(z0), sortSu(z1))))), SORTSU(circ(sortSu(z0), sortSu(z1))), SORTSU(z0), SORTSU(z1), SORTSU(z2))
TE(subst(te(z0), sortSu(id))) → c7(TE(z0))
TE(msubst(te(z0), sortSu(id))) → c8(TE(z0))
TE(msubst(te(msubst(te(z0), sortSu(z1))), sortSu(z2))) → c9(TE(msubst(te(z0), sortSu(circ(sortSu(z1), sortSu(z2))))), TE(z0), SORTSU(circ(sortSu(z1), sortSu(z2))), SORTSU(z1), SORTSU(z2))

S tuples:

SORTSU(circ(sortSu(cons(te(z0), sortSu(z1))), sortSu(z2))) → c(SORTSU(cons(te(msubst(te(z0), sortSu(z2))), sortSu(circ(sortSu(z1), sortSu(z2))))), TE(msubst(te(z0), sortSu(z2))), TE(z0), SORTSU(z2), SORTSU(circ(sortSu(z1), sortSu(z2))), SORTSU(z1), SORTSU(z2))
SORTSU(circ(sortSu(cons(sop(lift), sortSu(z0))), sortSu(cons(te(z1), sortSu(z2))))) → c1(SORTSU(cons(te(z1), sortSu(circ(sortSu(z0), sortSu(z2))))), TE(z1), SORTSU(circ(sortSu(z0), sortSu(z2))), SORTSU(z0), SORTSU(z2))
SORTSU(circ(sortSu(cons(sop(lift), sortSu(z0))), sortSu(cons(sop(lift), sortSu(z1))))) → c2(SORTSU(cons(sop(lift), sortSu(circ(sortSu(z0), sortSu(z1))))), SORTSU(circ(sortSu(z0), sortSu(z1))), SORTSU(z0), SORTSU(z1))
SORTSU(circ(sortSu(circ(sortSu(z0), sortSu(z1))), sortSu(z2))) → c3(SORTSU(circ(sortSu(z0), sortSu(circ(sortSu(z1), sortSu(z2))))), SORTSU(z0), SORTSU(circ(sortSu(z1), sortSu(z2))), SORTSU(z1), SORTSU(z2))
SORTSU(circ(sortSu(z0), sortSu(id))) → c4(SORTSU(z0))
SORTSU(circ(sortSu(id), sortSu(z0))) → c5(SORTSU(z0))
SORTSU(circ(sortSu(cons(sop(lift), sortSu(z0))), sortSu(circ(sortSu(cons(sop(lift), sortSu(z1))), sortSu(z2))))) → c6(SORTSU(circ(sortSu(cons(sop(lift), sortSu(circ(sortSu(z0), sortSu(z1))))), sortSu(z2))), SORTSU(cons(sop(lift), sortSu(circ(sortSu(z0), sortSu(z1))))), SORTSU(circ(sortSu(z0), sortSu(z1))), SORTSU(z0), SORTSU(z1), SORTSU(z2))
TE(subst(te(z0), sortSu(id))) → c7(TE(z0))
TE(msubst(te(z0), sortSu(id))) → c8(TE(z0))
TE(msubst(te(msubst(te(z0), sortSu(z1))), sortSu(z2))) → c9(TE(msubst(te(z0), sortSu(circ(sortSu(z1), sortSu(z2))))), TE(z0), SORTSU(circ(sortSu(z1), sortSu(z2))), SORTSU(z1), SORTSU(z2))

K tuples:none
Defined Rule Symbols:

sortSu, te

Defined Pair Symbols:

SORTSU, TE

Compound Symbols:

c, c1, c2, c3, c4, c5, c6, c7, c8, c9

(3) CdtUnreachableProof (EQUIVALENT transformation)

The following tuples could be removed as they are not reachable from basic start terms:

SORTSU(circ(sortSu(cons(te(z0), sortSu(z1))), sortSu(z2))) → c(SORTSU(cons(te(msubst(te(z0), sortSu(z2))), sortSu(circ(sortSu(z1), sortSu(z2))))), TE(msubst(te(z0), sortSu(z2))), TE(z0), SORTSU(z2), SORTSU(circ(sortSu(z1), sortSu(z2))), SORTSU(z1), SORTSU(z2))
SORTSU(circ(sortSu(cons(sop(lift), sortSu(z0))), sortSu(cons(te(z1), sortSu(z2))))) → c1(SORTSU(cons(te(z1), sortSu(circ(sortSu(z0), sortSu(z2))))), TE(z1), SORTSU(circ(sortSu(z0), sortSu(z2))), SORTSU(z0), SORTSU(z2))
SORTSU(circ(sortSu(cons(sop(lift), sortSu(z0))), sortSu(cons(sop(lift), sortSu(z1))))) → c2(SORTSU(cons(sop(lift), sortSu(circ(sortSu(z0), sortSu(z1))))), SORTSU(circ(sortSu(z0), sortSu(z1))), SORTSU(z0), SORTSU(z1))
SORTSU(circ(sortSu(circ(sortSu(z0), sortSu(z1))), sortSu(z2))) → c3(SORTSU(circ(sortSu(z0), sortSu(circ(sortSu(z1), sortSu(z2))))), SORTSU(z0), SORTSU(circ(sortSu(z1), sortSu(z2))), SORTSU(z1), SORTSU(z2))
SORTSU(circ(sortSu(z0), sortSu(id))) → c4(SORTSU(z0))
SORTSU(circ(sortSu(id), sortSu(z0))) → c5(SORTSU(z0))
SORTSU(circ(sortSu(cons(sop(lift), sortSu(z0))), sortSu(circ(sortSu(cons(sop(lift), sortSu(z1))), sortSu(z2))))) → c6(SORTSU(circ(sortSu(cons(sop(lift), sortSu(circ(sortSu(z0), sortSu(z1))))), sortSu(z2))), SORTSU(cons(sop(lift), sortSu(circ(sortSu(z0), sortSu(z1))))), SORTSU(circ(sortSu(z0), sortSu(z1))), SORTSU(z0), SORTSU(z1), SORTSU(z2))
TE(subst(te(z0), sortSu(id))) → c7(TE(z0))
TE(msubst(te(z0), sortSu(id))) → c8(TE(z0))
TE(msubst(te(msubst(te(z0), sortSu(z1))), sortSu(z2))) → c9(TE(msubst(te(z0), sortSu(circ(sortSu(z1), sortSu(z2))))), TE(z0), SORTSU(circ(sortSu(z1), sortSu(z2))), SORTSU(z1), SORTSU(z2))

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

sortSu(circ(sortSu(cons(te(z0), sortSu(z1))), sortSu(z2))) → sortSu(cons(te(msubst(te(z0), sortSu(z2))), sortSu(circ(sortSu(z1), sortSu(z2)))))
sortSu(circ(sortSu(cons(sop(lift), sortSu(z0))), sortSu(cons(te(z1), sortSu(z2))))) → sortSu(cons(te(z1), sortSu(circ(sortSu(z0), sortSu(z2)))))
sortSu(circ(sortSu(cons(sop(lift), sortSu(z0))), sortSu(cons(sop(lift), sortSu(z1))))) → sortSu(cons(sop(lift), sortSu(circ(sortSu(z0), sortSu(z1)))))
sortSu(circ(sortSu(circ(sortSu(z0), sortSu(z1))), sortSu(z2))) → sortSu(circ(sortSu(z0), sortSu(circ(sortSu(z1), sortSu(z2)))))
sortSu(circ(sortSu(z0), sortSu(id))) → sortSu(z0)
sortSu(circ(sortSu(id), sortSu(z0))) → sortSu(z0)
sortSu(circ(sortSu(cons(sop(lift), sortSu(z0))), sortSu(circ(sortSu(cons(sop(lift), sortSu(z1))), sortSu(z2))))) → sortSu(circ(sortSu(cons(sop(lift), sortSu(circ(sortSu(z0), sortSu(z1))))), sortSu(z2)))
te(subst(te(z0), sortSu(id))) → te(z0)
te(msubst(te(z0), sortSu(id))) → te(z0)
te(msubst(te(msubst(te(z0), sortSu(z1))), sortSu(z2))) → te(msubst(te(z0), sortSu(circ(sortSu(z1), sortSu(z2)))))

Tuples:none
S tuples:none
K tuples:none
Defined Rule Symbols:

sortSu, te

Defined Pair Symbols:none

Compound Symbols:none

(5) SIsEmptyProof (EQUIVALENT transformation)