### Pre-processing the ITS problem ###
Initial linear ITS problem
Start location: f0
0: f0 -> f : [], cost: 0
1: f -> f : x'=-1+x, f : x'=x-y, [ x>0 && y>x ], 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, f : x'=x-y, [ x>0 && y>x ], cost: 1
Accelerated rule 1 with metering function x (after partial deletion), 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 : [], cost: 0
2: f -> f : x'=0, [ x>0 && y>x ], cost: x
Chained accelerated rules (with incoming rules):
Start location: f0
0: f0 -> f : [], cost: 0
3: f0 -> f : x'=0, [ x>0 && y>x ], cost: x
Removed unreachable locations (and leaf rules with constant cost):
Start location: f0
3: f0 -> f : x'=0, [ x>0 && y>x ], cost: x
### Obtained a tail recursive problem, continuing simplification ###
### Computing asymptotic complexity ###
Fully simplified ITS problem
Start location: f0
3: f0 -> f : x'=0, [ x>0 && y>x ], cost: x
Computing asymptotic complexity for rule 3
Solved the limit problem by the following transformations:
Created initial limit problem:
x (+), -x+y (+/+!) [not solved]
removing all constraints (solved by SMT)
resulting limit problem: [solved]
applying transformation rule (C) using substitution {x==n,y==2*n}
resulting limit problem:
[solved]
Solution:
x / n
y / 2*n
Resulting cost n has complexity: Poly(n^1)
Found new complexity Poly(n^1).
Obtained the following overall complexity (w.r.t. the length of the input n):
Complexity: Poly(n^1)
Cpx degree: 1
Solved cost: n
Rule cost: x
Rule guard: [ x>0 && y>x ]
WORST_CASE(Omega(n^1),?)