### Pre-processing the ITS problem ###
Initial linear ITS problem
Start location: f
0: f -> fib : [], cost: 0
1: fib -> fib : x'=-1+x, fib : x'=-2+x, [ x>1 ], cost: 1
2: fib -> sink : [ x<=1 ], cost: 1
Checking for constant complexity:
Could not prove constant complexity.
Removed unreachable and leaf rules:
Start location: f
0: f -> fib : [], cost: 0
1: fib -> fib : x'=-1+x, fib : x'=-2+x, [ x>1 ], cost: 1
### Simplification by acceleration and chaining ###
Accelerating simple loops of location 1.
Accelerating the following rules:
1: fib -> fib : x'=-1+x, fib : x'=-2+x, [ x>1 ], cost: 1
Accelerated rule 1 with metering function meter (where 2*meter==-1+x), yielding the new rule 3.
Removing the simple loops: 1.
Accelerated all simple loops using metering functions (where possible):
Start location: f
0: f -> fib : [], cost: 0
3: fib -> [3] : [ x>1 && 2*meter==-1+x ], cost: -1+2^meter
Chained accelerated rules (with incoming rules):
Start location: f
0: f -> fib : [], cost: 0
4: f -> [3] : [ x>1 && 2*meter==-1+x ], cost: -1+2^meter
Removed unreachable locations (and leaf rules with constant cost):
Start location: f
4: f -> [3] : [ x>1 && 2*meter==-1+x ], cost: -1+2^meter
### Obtained a tail recursive problem, continuing simplification ###
### Computing asymptotic complexity ###
Fully simplified ITS problem
Start location: f
4: f -> [3] : [ x>1 && 2*meter==-1+x ], cost: -1+2^meter
Computing asymptotic complexity for rule 4
Solved the limit problem by the following transformations:
Created initial limit problem:
-1+x (+/+!), -1+2^meter (+), -2*meter+x (+/+!), 2+2*meter-x (+/+!) [not solved]
applying transformation rule (C) using substitution {x==1+2*meter}
resulting limit problem:
1 (+/+!), -1+2^meter (+), 2*meter (+/+!) [not solved]
applying transformation rule (B), deleting 1 (+/+!)
resulting limit problem:
-1+2^meter (+), 2*meter (+/+!) [not solved]
applying transformation rule (E), replacing -1+2^meter (+) by 1 (+/+!) and meter (+)
resulting limit problem:
1 (+/+!), meter (+), 2*meter (+/+!) [not solved]
applying transformation rule (B), deleting 1 (+/+!)
resulting limit problem:
meter (+), 2*meter (+/+!) [not solved]
applying transformation rule (A), replacing 2*meter (+) by meter (+) and 2 (+!) using + limit vector (+,+!)
resulting limit problem:
meter (+), 2 (+!) [not solved]
applying transformation rule (B), deleting 2 (+!)
resulting limit problem:
meter (+) [solved]
Solved the limit problem by the following transformations:
Created initial limit problem:
-1+x (+/+!), -1+2^meter (+), -2*meter+x (+/+!), 2+2*meter-x (+/+!) [not solved]
applying transformation rule (C) using substitution {x==1+2*meter}
resulting limit problem:
1 (+/+!), -1+2^meter (+), 2*meter (+/+!) [not solved]
applying transformation rule (B), deleting 1 (+/+!)
resulting limit problem:
-1+2^meter (+), 2*meter (+/+!) [not solved]
applying transformation rule (E), replacing -1+2^meter (+) by 1 (+/+!) and meter (+)
resulting limit problem:
1 (+/+!), meter (+), 2*meter (+/+!) [not solved]
applying transformation rule (B), deleting 1 (+/+!)
resulting limit problem:
meter (+), 2*meter (+/+!) [not solved]
applying transformation rule (A), replacing 2*meter (+) by meter (+) and 2 (+!) using + limit vector (+,+!)
resulting limit problem:
meter (+), 2 (+!) [not solved]
applying transformation rule (B), deleting 2 (+!)
resulting limit problem:
meter (+) [solved]
Solution:
meter / n
x / 1+2*n
Resulting cost -1+2^n has complexity: Exp
Found new complexity Exp.
Obtained the following overall complexity (w.r.t. the length of the input n):
Complexity: Exp
Cpx degree: Exp
Solved cost: -1+2^n
Rule cost: -1+2^meter
Rule guard: [ x>1 && 2*meter==-1+x ]
WORST_CASE(EXP,?)