YES(O(1), O(n^1)) 3.13/1.29 YES(O(1), O(n^1)) 3.51/1.39 3.51/1.39 3.51/1.39 3.51/1.39 3.51/1.39 3.51/1.39 Runtime Complexity (innermost) proof of /export/starexec/sandbox/benchmark/theBenchmark.xml.xml 3.51/1.39 3.51/1.39 3.51/1.39
3.51/1.39
3.51/1.39
3.51/1.39
The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^1)).

0 CpxTRS
3.51/1.39 
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))
3.51/1.39 
↳2 CdtProblem
3.51/1.39 
↳3 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
3.51/1.39 
↳4 CdtProblem
3.51/1.39 
↳5 CdtLeafRemovalProof (ComplexityIfPolyImplication)
3.51/1.39 
↳6 CdtProblem
3.51/1.39 
↳7 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
3.51/1.39 
↳8 CdtProblem
3.51/1.39 
↳9 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
3.51/1.39 
↳10 CdtProblem
3.51/1.39 
↳11 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
3.51/1.39 
↳12 CdtProblem
3.51/1.39 
↳13 SIsEmptyProof (BOTH BOUNDS(ID, ID))
3.51/1.39 
↳14 BOUNDS(O(1), O(1))
3.51/1.39
3.51/1.39 3.51/1.39
3.51/1.39
3.51/1.39

(0) Obligation:

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

dec(Cons(Nil, Nil)) → Nil 3.51/1.39
dec(Cons(Nil, Cons(x, xs))) → dec(Cons(x, xs)) 3.51/1.39
dec(Cons(Cons(x, xs), Nil)) → dec(Nil) 3.51/1.39
dec(Cons(Cons(x', xs'), Cons(x, xs))) → dec(Cons(x, xs)) 3.51/1.39
isNilNil(Cons(Nil, Nil)) → True 3.51/1.39
isNilNil(Cons(Nil, Cons(x, xs))) → False 3.51/1.39
isNilNil(Cons(Cons(x, xs), Nil)) → False 3.51/1.39
isNilNil(Cons(Cons(x', xs'), Cons(x, xs))) → False 3.51/1.39
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))))))))))))))))) 3.51/1.39
nestdec(Cons(x, xs)) → nestdec(dec(Cons(x, xs))) 3.51/1.39
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))))))))))))))))) 3.51/1.39
goal(x) → nestdec(x)

Rewrite Strategy: INNERMOST
3.51/1.39
3.51/1.39

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

Converted CpxTRS to CDT
3.51/1.39
3.51/1.39

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

dec(Cons(Nil, Nil)) → Nil 3.51/1.39
dec(Cons(Nil, Cons(z0, z1))) → dec(Cons(z0, z1)) 3.51/1.39
dec(Cons(Cons(z0, z1), Nil)) → dec(Nil) 3.51/1.39
dec(Cons(Cons(z0, z1), Cons(z2, z3))) → dec(Cons(z2, z3)) 3.51/1.39
isNilNil(Cons(Nil, Nil)) → True 3.51/1.39
isNilNil(Cons(Nil, Cons(z0, z1))) → False 3.51/1.39
isNilNil(Cons(Cons(z0, z1), Nil)) → False 3.51/1.39
isNilNil(Cons(Cons(z0, z1), Cons(z2, z3))) → False 3.51/1.39
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))))))))))))))))) 3.51/1.39
nestdec(Cons(z0, z1)) → nestdec(dec(Cons(z0, z1))) 3.51/1.39
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))))))))))))))))) 3.51/1.39
goal(z0) → nestdec(z0)
Tuples:

DEC(Cons(Nil, Cons(z0, z1))) → c1(DEC(Cons(z0, z1))) 3.51/1.39
DEC(Cons(Cons(z0, z1), Nil)) → c2(DEC(Nil)) 3.51/1.39
DEC(Cons(Cons(z0, z1), Cons(z2, z3))) → c3(DEC(Cons(z2, z3))) 3.51/1.39
NESTDEC(Cons(z0, z1)) → c9(NESTDEC(dec(Cons(z0, z1))), DEC(Cons(z0, z1))) 3.51/1.39
GOAL(z0) → c11(NESTDEC(z0))
S tuples:

DEC(Cons(Nil, Cons(z0, z1))) → c1(DEC(Cons(z0, z1))) 3.51/1.39
DEC(Cons(Cons(z0, z1), Nil)) → c2(DEC(Nil)) 3.51/1.39
DEC(Cons(Cons(z0, z1), Cons(z2, z3))) → c3(DEC(Cons(z2, z3))) 3.51/1.39
NESTDEC(Cons(z0, z1)) → c9(NESTDEC(dec(Cons(z0, z1))), DEC(Cons(z0, z1))) 3.51/1.39
GOAL(z0) → c11(NESTDEC(z0))
K tuples:none
Defined Rule Symbols:

dec, isNilNil, nestdec, number17, goal

Defined Pair Symbols:

DEC, NESTDEC, GOAL

Compound Symbols:

c1, c2, c3, c9, c11

3.51/1.39
3.51/1.39

(3) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing tuple parts
3.51/1.39
3.51/1.39

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

dec(Cons(Nil, Nil)) → Nil 3.51/1.39
dec(Cons(Nil, Cons(z0, z1))) → dec(Cons(z0, z1)) 3.51/1.39
dec(Cons(Cons(z0, z1), Nil)) → dec(Nil) 3.51/1.39
dec(Cons(Cons(z0, z1), Cons(z2, z3))) → dec(Cons(z2, z3)) 3.51/1.39
isNilNil(Cons(Nil, Nil)) → True 3.51/1.39
isNilNil(Cons(Nil, Cons(z0, z1))) → False 3.51/1.39
isNilNil(Cons(Cons(z0, z1), Nil)) → False 3.51/1.39
isNilNil(Cons(Cons(z0, z1), Cons(z2, z3))) → False 3.51/1.39
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))))))))))))))))) 3.51/1.39
nestdec(Cons(z0, z1)) → nestdec(dec(Cons(z0, z1))) 3.51/1.39
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))))))))))))))))) 3.51/1.39
goal(z0) → nestdec(z0)
Tuples:

DEC(Cons(Nil, Cons(z0, z1))) → c1(DEC(Cons(z0, z1))) 3.51/1.39
DEC(Cons(Cons(z0, z1), Cons(z2, z3))) → c3(DEC(Cons(z2, z3))) 3.90/1.41
NESTDEC(Cons(z0, z1)) → c9(NESTDEC(dec(Cons(z0, z1))), DEC(Cons(z0, z1))) 3.90/1.41
GOAL(z0) → c11(NESTDEC(z0)) 3.90/1.41
DEC(Cons(Cons(z0, z1), Nil)) → c2
S tuples:

DEC(Cons(Nil, Cons(z0, z1))) → c1(DEC(Cons(z0, z1))) 3.90/1.41
DEC(Cons(Cons(z0, z1), Cons(z2, z3))) → c3(DEC(Cons(z2, z3))) 3.90/1.41
NESTDEC(Cons(z0, z1)) → c9(NESTDEC(dec(Cons(z0, z1))), DEC(Cons(z0, z1))) 3.90/1.41
GOAL(z0) → c11(NESTDEC(z0)) 3.90/1.41
DEC(Cons(Cons(z0, z1), Nil)) → c2
K tuples:none
Defined Rule Symbols:

dec, isNilNil, nestdec, number17, goal

Defined Pair Symbols:

DEC, NESTDEC, GOAL

Compound Symbols:

c1, c3, c9, c11, c2

3.90/1.41
3.90/1.41

(5) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 1 leading nodes:

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

DEC(Cons(Cons(z0, z1), Nil)) → c2
3.90/1.41
3.90/1.41

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

dec(Cons(Nil, Nil)) → Nil 3.90/1.41
dec(Cons(Nil, Cons(z0, z1))) → dec(Cons(z0, z1)) 3.90/1.41
dec(Cons(Cons(z0, z1), Nil)) → dec(Nil) 3.90/1.41
dec(Cons(Cons(z0, z1), Cons(z2, z3))) → dec(Cons(z2, z3)) 3.90/1.41
isNilNil(Cons(Nil, Nil)) → True 3.90/1.41
isNilNil(Cons(Nil, Cons(z0, z1))) → False 3.90/1.41
isNilNil(Cons(Cons(z0, z1), Nil)) → False 3.90/1.41
isNilNil(Cons(Cons(z0, z1), Cons(z2, z3))) → False 3.90/1.41
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))))))))))))))))) 3.90/1.41
nestdec(Cons(z0, z1)) → nestdec(dec(Cons(z0, z1))) 3.90/1.41
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))))))))))))))))) 3.90/1.41
goal(z0) → nestdec(z0)
Tuples:

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

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

dec, isNilNil, nestdec, number17, goal

Defined Pair Symbols:

DEC, NESTDEC

Compound Symbols:

c1, c3, c9, c2

3.90/1.41
3.90/1.41

(7) CdtPolyRedPairProof (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(Cons(z0, z1), Nil)) → c2
We considered the (Usable) Rules:

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

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

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

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

dec(Cons(Nil, Nil)) → Nil 3.90/1.41
dec(Cons(Nil, Cons(z0, z1))) → dec(Cons(z0, z1)) 3.90/1.41
dec(Cons(Cons(z0, z1), Nil)) → dec(Nil) 3.90/1.41
dec(Cons(Cons(z0, z1), Cons(z2, z3))) → dec(Cons(z2, z3)) 3.90/1.41
isNilNil(Cons(Nil, Nil)) → True 3.90/1.41
isNilNil(Cons(Nil, Cons(z0, z1))) → False 3.90/1.41
isNilNil(Cons(Cons(z0, z1), Nil)) → False 3.90/1.41
isNilNil(Cons(Cons(z0, z1), Cons(z2, z3))) → False 3.90/1.41
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))))))))))))))))) 3.90/1.41
nestdec(Cons(z0, z1)) → nestdec(dec(Cons(z0, z1))) 3.90/1.41
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))))))))))))))))) 3.90/1.41
goal(z0) → nestdec(z0)
Tuples:

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

DEC(Cons(Nil, Cons(z0, z1))) → c1(DEC(Cons(z0, z1))) 3.90/1.41
DEC(Cons(Cons(z0, z1), Cons(z2, z3))) → c3(DEC(Cons(z2, z3))) 3.90/1.41
NESTDEC(Cons(z0, z1)) → c9(NESTDEC(dec(Cons(z0, z1))), DEC(Cons(z0, z1)))
K tuples:

DEC(Cons(Cons(z0, z1), Nil)) → c2
Defined Rule Symbols:

dec, isNilNil, nestdec, number17, goal

Defined Pair Symbols:

DEC, NESTDEC

Compound Symbols:

c1, c3, c9, c2

3.90/1.41
3.90/1.41

(9) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

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

NESTDEC(Cons(z0, z1)) → c9(NESTDEC(dec(Cons(z0, z1))), DEC(Cons(z0, z1)))
We considered the (Usable) Rules:

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

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

POL(Cons(x1, x2)) = [4]    3.90/1.41
POL(DEC(x1)) = 0    3.90/1.41
POL(NESTDEC(x1)) = x1    3.90/1.41
POL(Nil) = 0    3.90/1.41
POL(c1(x1)) = x1    3.90/1.41
POL(c2) = 0    3.90/1.41
POL(c3(x1)) = x1    3.90/1.41
POL(c9(x1, x2)) = x1 + x2    3.90/1.41
POL(dec(x1)) = 0   
3.90/1.41
3.90/1.41

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

dec(Cons(Nil, Nil)) → Nil 3.90/1.41
dec(Cons(Nil, Cons(z0, z1))) → dec(Cons(z0, z1)) 3.90/1.41
dec(Cons(Cons(z0, z1), Nil)) → dec(Nil) 3.90/1.41
dec(Cons(Cons(z0, z1), Cons(z2, z3))) → dec(Cons(z2, z3)) 3.90/1.41
isNilNil(Cons(Nil, Nil)) → True 3.90/1.41
isNilNil(Cons(Nil, Cons(z0, z1))) → False 3.90/1.41
isNilNil(Cons(Cons(z0, z1), Nil)) → False 3.90/1.41
isNilNil(Cons(Cons(z0, z1), Cons(z2, z3))) → False 3.90/1.41
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))))))))))))))))) 3.90/1.41
nestdec(Cons(z0, z1)) → nestdec(dec(Cons(z0, z1))) 3.90/1.41
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))))))))))))))))) 3.90/1.41
goal(z0) → nestdec(z0)
Tuples:

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

DEC(Cons(Nil, Cons(z0, z1))) → c1(DEC(Cons(z0, z1))) 3.90/1.41
DEC(Cons(Cons(z0, z1), Cons(z2, z3))) → c3(DEC(Cons(z2, z3)))
K tuples:

DEC(Cons(Cons(z0, z1), Nil)) → c2 3.90/1.41
NESTDEC(Cons(z0, z1)) → c9(NESTDEC(dec(Cons(z0, z1))), DEC(Cons(z0, z1)))
Defined Rule Symbols:

dec, isNilNil, nestdec, number17, goal

Defined Pair Symbols:

DEC, NESTDEC

Compound Symbols:

c1, c3, c9, c2

3.90/1.41
3.90/1.41

(11) CdtPolyRedPairProof (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))) 3.90/1.41
DEC(Cons(Cons(z0, z1), Cons(z2, z3))) → c3(DEC(Cons(z2, z3)))
We considered the (Usable) Rules:

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

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

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

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

dec(Cons(Nil, Nil)) → Nil 3.90/1.41
dec(Cons(Nil, Cons(z0, z1))) → dec(Cons(z0, z1)) 3.90/1.41
dec(Cons(Cons(z0, z1), Nil)) → dec(Nil) 3.90/1.41
dec(Cons(Cons(z0, z1), Cons(z2, z3))) → dec(Cons(z2, z3)) 3.90/1.41
isNilNil(Cons(Nil, Nil)) → True 3.90/1.41
isNilNil(Cons(Nil, Cons(z0, z1))) → False 3.90/1.41
isNilNil(Cons(Cons(z0, z1), Nil)) → False 3.90/1.41
isNilNil(Cons(Cons(z0, z1), Cons(z2, z3))) → False 3.90/1.41
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))))))))))))))))) 3.90/1.41
nestdec(Cons(z0, z1)) → nestdec(dec(Cons(z0, z1))) 3.90/1.41
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))))))))))))))))) 3.90/1.41
goal(z0) → nestdec(z0)
Tuples:

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

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

dec, isNilNil, nestdec, number17, goal

Defined Pair Symbols:

DEC, NESTDEC

Compound Symbols:

c1, c3, c9, c2

3.90/1.41
3.90/1.41

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

The set S is empty
3.90/1.41
3.90/1.41

(14) BOUNDS(O(1), O(1))

3.90/1.41
3.90/1.41
3.90/1.49 EOF