### Pre-processing the ITS problem ###
Initial linear ITS problem
Start location: f0
0: f0 -> f : x'=free, [], cost: 0
1: f -> f : x'=-1+x, [ x>0 ], cost: 1
Checking for constant complexity:
Could not prove constant complexity.
### Simplification by acceleration and chaining ###
Accelerating simple loops of location 1.
Accelerating the following rules:
1: f -> f : x'=-1+x, [ x>0 ], cost: 1
Accelerated rule 1 with metering function x, yielding the new rule 2.
Removing the simple loops: 1.
Accelerated all simple loops using metering functions (where possible):
Start location: f0
0: f0 -> f : x'=free, [], cost: 0
2: f -> f : x'=0, [ x>0 ], cost: x
Chained accelerated rules (with incoming rules):
Start location: f0
0: f0 -> f : x'=free, [], cost: 0
3: f0 -> f : x'=0, [ free>0 ], cost: free
Removed unreachable locations (and leaf rules with constant cost):
Start location: f0
3: f0 -> f : x'=0, [ free>0 ], cost: free
### Computing asymptotic complexity ###
Fully simplified ITS problem
Start location: f0
3: f0 -> f : x'=0, [ free>0 ], cost: free
Computing asymptotic complexity for rule 3
Solved the limit problem by the following transformations:
Created initial limit problem:
free (+) [solved]
removing all constraints (solved by SMT)
resulting limit problem: [solved]
applying transformation rule (C) using substitution {free==n}
resulting limit problem:
[solved]
Solution:
free / n
Resulting cost n has complexity: Unbounded
Found new complexity Unbounded.
Obtained the following overall complexity (w.r.t. the length of the input n):
Complexity: Unbounded
Cpx degree: Unbounded
Solved cost: n
Rule cost: free
Rule guard: [ free>0 ]
WORST_CASE(INF,?)