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:

merge(Cons(x, xs), Nil) → Cons(x, xs) 0.00/0.55
merge(Cons(x', xs'), Cons(x, xs)) → merge[Ite][False][Ite][False][Ite](<=(x', x), Cons(x', xs'), Cons(x, xs)) 0.00/0.55
merge(Nil, ys) → ys 0.00/0.55
goal(xs, ys) → merge(xs, ys)

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

<=(S(x), S(y)) → <=(x, y) 0.00/0.55
<=(0, y) → True 0.00/0.55
<=(S(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, z0) → True 0.00/0.55
<=(S(z0), 0) → False 0.00/0.55
merge(Cons(z0, z1), Nil) → Cons(z0, z1) 0.00/0.55
merge(Cons(z0, z1), Cons(z2, z3)) → merge[Ite][False][Ite][False][Ite](<=(z0, z2), Cons(z0, z1), Cons(z2, z3)) 0.00/0.55
merge(Nil, z0) → z0 0.00/0.55
goal(z0, z1) → merge(z0, z1)
Tuples:

<='(S(z0), S(z1)) → c(<='(z0, z1)) 0.00/0.55
MERGE(Cons(z0, z1), Cons(z2, z3)) → c4(<='(z0, z2)) 0.00/0.55
GOAL(z0, z1) → c6(MERGE(z0, z1))
S tuples:

MERGE(Cons(z0, z1), Cons(z2, z3)) → c4(<='(z0, z2)) 0.00/0.55
GOAL(z0, z1) → c6(MERGE(z0, z1))
K tuples:none
Defined Rule Symbols:

merge, goal, <=

Defined Pair Symbols:

<=', MERGE, GOAL

Compound Symbols:

c, c4, c6

0.00/0.55
0.00/0.55

(3) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 2 leading nodes:

GOAL(z0, z1) → c6(MERGE(z0, z1)) 0.00/0.55
MERGE(Cons(z0, z1), Cons(z2, z3)) → c4(<='(z0, z2))
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, z0) → True 0.00/0.55
<=(S(z0), 0) → False 0.00/0.55
merge(Cons(z0, z1), Nil) → Cons(z0, z1) 0.00/0.55
merge(Cons(z0, z1), Cons(z2, z3)) → merge[Ite][False][Ite][False][Ite](<=(z0, z2), Cons(z0, z1), Cons(z2, z3)) 0.00/0.55
merge(Nil, z0) → z0 0.00/0.55
goal(z0, z1) → merge(z0, z1)
Tuples:

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

merge, 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