YES(O(1), O(1)) 0.00/0.54 YES(O(1), O(1)) 0.00/0.55 0.00/0.55 0.00/0.55 0.00/0.55 0.00/0.55 0.00/0.55 Runtime Complexity (innermost) proof of /export/starexec/sandbox/benchmark/theBenchmark.xml.xml 0.00/0.55 0.00/0.55 0.00/0.55
0.00/0.55
0.00/0.55
0.00/0.55
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(O(1), O(1)).

0 CpxRelTRS
0.00/0.55 
↳1 CpxRelTrsToCDT (UPPER BOUND (ID))
0.00/0.55 
↳2 CdtProblem
0.00/0.55 
↳3 CdtLeafRemovalProof (ComplexityIfPolyImplication)
0.00/0.55 
↳4 CdtProblem
0.00/0.55 
↳5 SIsEmptyProof (BOTH BOUNDS(ID, ID))
0.00/0.55 
↳6 BOUNDS(O(1), O(1))
0.00/0.55
0.00/0.55 0.00/0.55
0.00/0.55
0.00/0.55

(0) Obligation:

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

ordered(Cons(x', Cons(x, xs))) → ordered[Ite][True][Ite][True][Ite](<(x', x), Cons(x', Cons(x, xs))) 0.00/0.55
ordered(Cons(x, Nil)) → True 0.00/0.55
ordered(Nil) → True 0.00/0.55
notEmpty(Cons(x, xs)) → True 0.00/0.55
notEmpty(Nil) → False 0.00/0.55
goal(xs) → ordered(xs)

The (relative) TRS S consists of the following rules:

<(S(x), S(y)) → <(x, y) 0.00/0.55
<(0, S(y)) → True 0.00/0.55
<(x, 0) → False

Rewrite Strategy: INNERMOST
0.00/0.55
0.00/0.55

(1) CpxRelTrsToCDT (UPPER BOUND (ID) transformation)

Relative innermost TRS to CDT Problem.
0.00/0.55
0.00/0.55

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

<(S(z0), S(z1)) → <(z0, z1) 0.00/0.55
<(0, S(z0)) → True 0.00/0.55
<(z0, 0) → False 0.00/0.55
ordered(Cons(z0, Cons(z1, z2))) → ordered[Ite][True][Ite][True][Ite](<(z0, z1), Cons(z0, Cons(z1, z2))) 0.00/0.55
ordered(Cons(z0, Nil)) → True 0.00/0.55
ordered(Nil) → True 0.00/0.55
notEmpty(Cons(z0, z1)) → True 0.00/0.55
notEmpty(Nil) → False 0.00/0.55
goal(z0) → ordered(z0)
Tuples:

<'(S(z0), S(z1)) → c(<'(z0, z1)) 0.00/0.55
ORDERED(Cons(z0, Cons(z1, z2))) → c3(<'(z0, z1)) 0.00/0.55
GOAL(z0) → c8(ORDERED(z0))
S tuples:

ORDERED(Cons(z0, Cons(z1, z2))) → c3(<'(z0, z1)) 0.00/0.55
GOAL(z0) → c8(ORDERED(z0))
K tuples:none
Defined Rule Symbols:

ordered, notEmpty, goal, <

Defined Pair Symbols:

<', ORDERED, GOAL

Compound Symbols:

c, c3, c8

0.00/0.55
0.00/0.55

(3) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 2 leading nodes:

GOAL(z0) → c8(ORDERED(z0)) 0.00/0.55
ORDERED(Cons(z0, Cons(z1, z2))) → c3(<'(z0, z1))
0.00/0.55
0.00/0.55

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

<(S(z0), S(z1)) → <(z0, z1) 0.00/0.55
<(0, S(z0)) → True 0.00/0.55
<(z0, 0) → False 0.00/0.55
ordered(Cons(z0, Cons(z1, z2))) → ordered[Ite][True][Ite][True][Ite](<(z0, z1), Cons(z0, Cons(z1, z2))) 0.00/0.55
ordered(Cons(z0, Nil)) → True 0.00/0.55
ordered(Nil) → True 0.00/0.55
notEmpty(Cons(z0, z1)) → True 0.00/0.55
notEmpty(Nil) → False 0.00/0.55
goal(z0) → ordered(z0)
Tuples:

<'(S(z0), S(z1)) → c(<'(z0, z1))
S tuples:none
K tuples:none
Defined Rule Symbols:

ordered, notEmpty, goal, <

Defined Pair Symbols:

<'

Compound Symbols:

c

0.00/0.55
0.00/0.55

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

The set S is empty
0.00/0.55
0.00/0.55

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

0.00/0.55
0.00/0.55
0.00/0.58 EOF