YES(O(1), O(n^1)) 0.00/0.73 YES(O(1), O(n^1)) 0.00/0.75 0.00/0.75 0.00/0.75
0.00/0.75 0.00/0.750 CpxTRS0.00/0.75
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))0.00/0.75
↳2 CdtProblem0.00/0.75
↳3 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))0.00/0.75
↳4 CdtProblem0.00/0.75
↳5 CdtLeafRemovalProof (ComplexityIfPolyImplication)0.00/0.75
↳6 CdtProblem0.00/0.75
↳7 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))0.00/0.75
↳8 CdtProblem0.00/0.75
↳9 SIsEmptyProof (BOTH BOUNDS(ID, ID))0.00/0.75
↳10 BOUNDS(O(1), O(1))0.00/0.75
decrease(Cons(x, xs)) → decrease(xs) 0.00/0.75
decrease(Nil) → number42(Nil) 0.00/0.75
number42(x) → 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, 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, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))))))))))))))))))))))))))))))))))))))))) 0.00/0.75
goal(x) → decrease(x)
Tuples:
decrease(Cons(z0, z1)) → decrease(z1) 0.00/0.75
decrease(Nil) → number42(Nil) 0.00/0.75
number42(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, 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, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))))))))))))))))))))))))))))))))))))))))) 0.00/0.75
goal(z0) → decrease(z0)
S tuples:
DECREASE(Cons(z0, z1)) → c(DECREASE(z1)) 0.00/0.75
DECREASE(Nil) → c1(NUMBER42(Nil)) 0.00/0.75
GOAL(z0) → c3(DECREASE(z0))
K tuples:none
DECREASE(Cons(z0, z1)) → c(DECREASE(z1)) 0.00/0.75
DECREASE(Nil) → c1(NUMBER42(Nil)) 0.00/0.75
GOAL(z0) → c3(DECREASE(z0))
decrease, number42, goal
DECREASE, GOAL
c, c1, c3
Tuples:
decrease(Cons(z0, z1)) → decrease(z1) 0.00/0.75
decrease(Nil) → number42(Nil) 0.00/0.75
number42(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, 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, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))))))))))))))))))))))))))))))))))))))))) 0.00/0.75
goal(z0) → decrease(z0)
S tuples:
DECREASE(Cons(z0, z1)) → c(DECREASE(z1)) 0.00/0.75
GOAL(z0) → c3(DECREASE(z0)) 0.00/0.75
DECREASE(Nil) → c1
K tuples:none
DECREASE(Cons(z0, z1)) → c(DECREASE(z1)) 0.00/0.75
GOAL(z0) → c3(DECREASE(z0)) 0.00/0.75
DECREASE(Nil) → c1
decrease, number42, goal
DECREASE, GOAL
c, c3, c1
Removed 1 trailing nodes:
GOAL(z0) → c3(DECREASE(z0))
DECREASE(Nil) → c1
Tuples:
decrease(Cons(z0, z1)) → decrease(z1) 0.00/0.75
decrease(Nil) → number42(Nil) 0.00/0.75
number42(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, 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, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))))))))))))))))))))))))))))))))))))))))) 0.00/0.75
goal(z0) → decrease(z0)
S tuples:
DECREASE(Cons(z0, z1)) → c(DECREASE(z1)) 0.00/0.75
DECREASE(Nil) → c1
K tuples:none
DECREASE(Cons(z0, z1)) → c(DECREASE(z1)) 0.00/0.75
DECREASE(Nil) → c1
decrease, number42, goal
DECREASE
c, c1
We considered the (Usable) Rules:none
DECREASE(Cons(z0, z1)) → c(DECREASE(z1)) 0.00/0.75
DECREASE(Nil) → c1
The order we found is given by the following interpretation:
DECREASE(Cons(z0, z1)) → c(DECREASE(z1)) 0.00/0.75
DECREASE(Nil) → c1
POL(Cons(x1, x2)) = [3] + x2 0.00/0.75
POL(DECREASE(x1)) = [3] + [3]x1 0.00/0.75
POL(Nil) = [5] 0.00/0.75
POL(c(x1)) = x1 0.00/0.75
POL(c1) = 0
Tuples:
decrease(Cons(z0, z1)) → decrease(z1) 0.00/0.75
decrease(Nil) → number42(Nil) 0.00/0.75
number42(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, 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, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))))))))))))))))))))))))))))))))))))))))) 0.00/0.75
goal(z0) → decrease(z0)
S tuples:none
DECREASE(Cons(z0, z1)) → c(DECREASE(z1)) 0.00/0.75
DECREASE(Nil) → c1
Defined Rule Symbols:
DECREASE(Cons(z0, z1)) → c(DECREASE(z1)) 0.00/0.75
DECREASE(Nil) → c1
decrease, number42, goal
DECREASE
c, c1