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

0 CpxTRS
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID), 0 ms)
↳2 CdtProblem
↳3 CdtLeafRemovalProof (ComplexityIfPolyImplication, 0 ms)
↳4 CdtProblem
↳5 CdtUsableRulesProof (⇔, 0 ms)
↳6 CdtProblem
↳7 CdtRuleRemovalProof (UPPER BOUND (ADD(O(n^1))), 112 ms)
↳8 CdtProblem
↳9 SIsEmptyProof (BOTH BOUNDS(ID, ID), 0 ms)
↳10 BOUNDS(O(1), O(1))

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

dec(Cons(Nil, Nil)) → Nil
dec(Cons(Nil, Cons(x, xs))) → dec(Cons(x, xs))
dec(Cons(Cons(x, xs), Nil)) → dec(Nil)
dec(Cons(Cons(x', xs'), Cons(x, xs))) → dec(Cons(x, xs))
isNilNil(Cons(Nil, Nil)) → True
isNilNil(Cons(Nil, Cons(x, xs))) → False
isNilNil(Cons(Cons(x, xs), Nil)) → False
isNilNil(Cons(Cons(x', xs'), Cons(x, xs))) → False
nestdec(Nil) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))))))))))))))))
nestdec(Cons(x, xs)) → nestdec(dec(Cons(x, xs)))
number17(n) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))))))))))))))))
goal(x) → nestdec(x)

Rewrite Strategy: INNERMOST

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

Converted Cpx (relative) TRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

dec(Cons(Nil, Nil)) → Nil
dec(Cons(Nil, Cons(z0, z1))) → dec(Cons(z0, z1))
dec(Cons(Cons(z0, z1), Nil)) → dec(Nil)
dec(Cons(Cons(z0, z1), Cons(z2, z3))) → dec(Cons(z2, z3))
isNilNil(Cons(Nil, Nil)) → True
isNilNil(Cons(Nil, Cons(z0, z1))) → False
isNilNil(Cons(Cons(z0, z1), Nil)) → False
isNilNil(Cons(Cons(z0, z1), Cons(z2, z3))) → False
nestdec(Nil) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))))))))))))))))
nestdec(Cons(z0, z1)) → nestdec(dec(Cons(z0, z1)))
number17(z0) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))))))))))))))))
goal(z0) → nestdec(z0)
Tuples:

DEC(Cons(Nil, Nil)) → c
DEC(Cons(Nil, Cons(z0, z1))) → c1(DEC(Cons(z0, z1)))
DEC(Cons(Cons(z0, z1), Nil)) → c2(DEC(Nil))
DEC(Cons(Cons(z0, z1), Cons(z2, z3))) → c3(DEC(Cons(z2, z3)))
ISNILNIL(Cons(Nil, Nil)) → c4
ISNILNIL(Cons(Nil, Cons(z0, z1))) → c5
ISNILNIL(Cons(Cons(z0, z1), Nil)) → c6
ISNILNIL(Cons(Cons(z0, z1), Cons(z2, z3))) → c7
NESTDEC(Nil) → c8
NESTDEC(Cons(z0, z1)) → c9(NESTDEC(dec(Cons(z0, z1))), DEC(Cons(z0, z1)))
NUMBER17(z0) → c10
GOAL(z0) → c11(NESTDEC(z0))
S tuples:

DEC(Cons(Nil, Nil)) → c
DEC(Cons(Nil, Cons(z0, z1))) → c1(DEC(Cons(z0, z1)))
DEC(Cons(Cons(z0, z1), Nil)) → c2(DEC(Nil))
DEC(Cons(Cons(z0, z1), Cons(z2, z3))) → c3(DEC(Cons(z2, z3)))
ISNILNIL(Cons(Nil, Nil)) → c4
ISNILNIL(Cons(Nil, Cons(z0, z1))) → c5
ISNILNIL(Cons(Cons(z0, z1), Nil)) → c6
ISNILNIL(Cons(Cons(z0, z1), Cons(z2, z3))) → c7
NESTDEC(Nil) → c8
NESTDEC(Cons(z0, z1)) → c9(NESTDEC(dec(Cons(z0, z1))), DEC(Cons(z0, z1)))
NUMBER17(z0) → c10
GOAL(z0) → c11(NESTDEC(z0))
K tuples:none
Defined Rule Symbols:

dec, isNilNil, nestdec, number17, goal

Defined Pair Symbols:

DEC, ISNILNIL, NESTDEC, NUMBER17, GOAL

Compound Symbols:

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

(3) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 1 leading nodes:

GOAL(z0) → c11(NESTDEC(z0))
Removed 8 trailing nodes:

ISNILNIL(Cons(Nil, Nil)) → c4
ISNILNIL(Cons(Cons(z0, z1), Nil)) → c6
DEC(Cons(Cons(z0, z1), Nil)) → c2(DEC(Nil))
ISNILNIL(Cons(Cons(z0, z1), Cons(z2, z3))) → c7
DEC(Cons(Nil, Nil)) → c
NUMBER17(z0) → c10
NESTDEC(Nil) → c8
ISNILNIL(Cons(Nil, Cons(z0, z1))) → c5

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

dec(Cons(Nil, Nil)) → Nil
dec(Cons(Nil, Cons(z0, z1))) → dec(Cons(z0, z1))
dec(Cons(Cons(z0, z1), Nil)) → dec(Nil)
dec(Cons(Cons(z0, z1), Cons(z2, z3))) → dec(Cons(z2, z3))
isNilNil(Cons(Nil, Nil)) → True
isNilNil(Cons(Nil, Cons(z0, z1))) → False
isNilNil(Cons(Cons(z0, z1), Nil)) → False
isNilNil(Cons(Cons(z0, z1), Cons(z2, z3))) → False
nestdec(Nil) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))))))))))))))))
nestdec(Cons(z0, z1)) → nestdec(dec(Cons(z0, z1)))
number17(z0) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))))))))))))))))
goal(z0) → nestdec(z0)
Tuples:

DEC(Cons(Nil, Cons(z0, z1))) → c1(DEC(Cons(z0, z1)))
DEC(Cons(Cons(z0, z1), Cons(z2, z3))) → c3(DEC(Cons(z2, z3)))
NESTDEC(Cons(z0, z1)) → c9(NESTDEC(dec(Cons(z0, z1))), DEC(Cons(z0, z1)))
S tuples:

DEC(Cons(Nil, Cons(z0, z1))) → c1(DEC(Cons(z0, z1)))
DEC(Cons(Cons(z0, z1), Cons(z2, z3))) → c3(DEC(Cons(z2, z3)))
NESTDEC(Cons(z0, z1)) → c9(NESTDEC(dec(Cons(z0, z1))), DEC(Cons(z0, z1)))
K tuples:none
Defined Rule Symbols:

dec, isNilNil, nestdec, number17, goal

Defined Pair Symbols:

DEC, NESTDEC

Compound Symbols:

c1, c3, c9

(5) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

isNilNil(Cons(Nil, Nil)) → True
isNilNil(Cons(Nil, Cons(z0, z1))) → False
isNilNil(Cons(Cons(z0, z1), Nil)) → False
isNilNil(Cons(Cons(z0, z1), Cons(z2, z3))) → False
nestdec(Nil) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))))))))))))))))
nestdec(Cons(z0, z1)) → nestdec(dec(Cons(z0, z1)))
number17(z0) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))))))))))))))))
goal(z0) → nestdec(z0)

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

dec(Cons(Nil, Nil)) → Nil
dec(Cons(Nil, Cons(z0, z1))) → dec(Cons(z0, z1))
dec(Cons(Cons(z0, z1), Nil)) → dec(Nil)
dec(Cons(Cons(z0, z1), Cons(z2, z3))) → dec(Cons(z2, z3))
Tuples:

DEC(Cons(Nil, Cons(z0, z1))) → c1(DEC(Cons(z0, z1)))
DEC(Cons(Cons(z0, z1), Cons(z2, z3))) → c3(DEC(Cons(z2, z3)))
NESTDEC(Cons(z0, z1)) → c9(NESTDEC(dec(Cons(z0, z1))), DEC(Cons(z0, z1)))
S tuples:

DEC(Cons(Nil, Cons(z0, z1))) → c1(DEC(Cons(z0, z1)))
DEC(Cons(Cons(z0, z1), Cons(z2, z3))) → c3(DEC(Cons(z2, z3)))
NESTDEC(Cons(z0, z1)) → c9(NESTDEC(dec(Cons(z0, z1))), DEC(Cons(z0, z1)))
K tuples:none
Defined Rule Symbols:

dec

Defined Pair Symbols:

DEC, NESTDEC

Compound Symbols:

c1, c3, c9

(7) CdtRuleRemovalProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

DEC(Cons(Nil, Cons(z0, z1))) → c1(DEC(Cons(z0, z1)))
DEC(Cons(Cons(z0, z1), Cons(z2, z3))) → c3(DEC(Cons(z2, z3)))
NESTDEC(Cons(z0, z1)) → c9(NESTDEC(dec(Cons(z0, z1))), DEC(Cons(z0, z1)))
We considered the (Usable) Rules:

dec(Cons(Nil, Cons(z0, z1))) → dec(Cons(z0, z1))
dec(Cons(Nil, Nil)) → Nil
dec(Cons(Cons(z0, z1), Nil)) → dec(Nil)
dec(Cons(Cons(z0, z1), Cons(z2, z3))) → dec(Cons(z2, z3))
And the Tuples:

DEC(Cons(Nil, Cons(z0, z1))) → c1(DEC(Cons(z0, z1)))
DEC(Cons(Cons(z0, z1), Cons(z2, z3))) → c3(DEC(Cons(z2, z3)))
NESTDEC(Cons(z0, z1)) → c9(NESTDEC(dec(Cons(z0, z1))), DEC(Cons(z0, z1)))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(Cons(x1, x2)) = [4] + x2   
POL(DEC(x1)) = [1] + x1   
POL(NESTDEC(x1)) = [2]x1   
POL(Nil) = 0   
POL(c1(x1)) = x1   
POL(c3(x1)) = x1   
POL(c9(x1, x2)) = x1 + x2   
POL(dec(x1)) = 0   

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

dec(Cons(Nil, Nil)) → Nil
dec(Cons(Nil, Cons(z0, z1))) → dec(Cons(z0, z1))
dec(Cons(Cons(z0, z1), Nil)) → dec(Nil)
dec(Cons(Cons(z0, z1), Cons(z2, z3))) → dec(Cons(z2, z3))
Tuples:

DEC(Cons(Nil, Cons(z0, z1))) → c1(DEC(Cons(z0, z1)))
DEC(Cons(Cons(z0, z1), Cons(z2, z3))) → c3(DEC(Cons(z2, z3)))
NESTDEC(Cons(z0, z1)) → c9(NESTDEC(dec(Cons(z0, z1))), DEC(Cons(z0, z1)))
S tuples:none
K tuples:

DEC(Cons(Nil, Cons(z0, z1))) → c1(DEC(Cons(z0, z1)))
DEC(Cons(Cons(z0, z1), Cons(z2, z3))) → c3(DEC(Cons(z2, z3)))
NESTDEC(Cons(z0, z1)) → c9(NESTDEC(dec(Cons(z0, z1))), DEC(Cons(z0, z1)))
Defined Rule Symbols:

dec

Defined Pair Symbols:

DEC, NESTDEC

Compound Symbols:

c1, c3, c9

(9) SIsEmptyProof (BOTH BOUNDS(ID, ID) transformation)

The set S is empty

(10) BOUNDS(O(1), O(1))