### Pre-processing the ITS problem ###
Initial linear ITS problem
Start location: f0
0: f0 -> f : [], cost: 0
1: f -> f : x'=-1+x, y'=2*y, [ x>0 ], cost: y
Added constraints to the guards to ensure costs are nonnegative:
Start location: f0
0: f0 -> f : [], cost: 0
1: f -> f : x'=-1+x, y'=2*y, [ x>0 && y>=0 ], cost: y
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, y'=2*y, [ x>0 && y>=0 ], cost: y
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 : [], cost: 0
2: f -> f : x'=0, y'=2^x*y, [ x>0 && y>=0 ], cost: 2^x*y-y
Chained accelerated rules (with incoming rules):
Start location: f0
0: f0 -> f : [], cost: 0
3: f0 -> f : x'=0, y'=2^x*y, [ x>0 && y>=0 ], cost: 2^x*y-y
Removed unreachable locations (and leaf rules with constant cost):
Start location: f0
3: f0 -> f : x'=0, y'=2^x*y, [ x>0 && y>=0 ], cost: 2^x*y-y
### Computing asymptotic complexity ###
Fully simplified ITS problem
Start location: f0
3: f0 -> f : x'=0, y'=2^x*y, [ x>0 && y>=0 ], cost: 2^x*y-y
Computing asymptotic complexity for rule 3
Solved the limit problem by the following transformations:
Created initial limit problem:
x (+/+!), 1+y (+/+!), 2^x*y-y (+) [not solved]
applying transformation rule (A), replacing 1+y (+!) by y (+!) and 1 (+!) using +! limit vector (+!,+!)
resulting limit problem:
1 (+!), x (+/+!), 2^x*y-y (+), y (+!) [not solved]
applying transformation rule (B), deleting 1 (+!)
resulting limit problem:
x (+/+!), 2^x*y-y (+), y (+!) [not solved]
applying transformation rule (A), replacing 2^x*y-y (+) by -y (-!) and 2^x*y (+) using + limit vector (-!,+)
resulting limit problem:
-y (-!), 2^x*y (+), x (+/+!), y (+!) [not solved]
applying transformation rule (A), replacing -y (-!) by y (+!) and -1 (-!) using -! limit vector (+!,-!)
resulting limit problem:
2^x*y (+), x (+/+!), y (+!), -1 (-!) [not solved]
applying transformation rule (B), deleting -1 (-!)
resulting limit problem:
2^x*y (+), x (+/+!), y (+!) [not solved]
applying transformation rule (A), replacing 2^x*y (+) by 2^x (+) and y (+!) using + limit vector (+,+!)
resulting limit problem:
x (+/+!), 2^x (+), y (+!) [not solved]
applying transformation rule (E), replacing 2^x (+) by 1 (+/+!) and x (+)
resulting limit problem:
1 (+/+!), x (+), y (+!) [not solved]
applying transformation rule (B), deleting 1 (+/+!)
resulting limit problem:
x (+), y (+!) [solved]
Solution:
x / n
y / 1
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: 2^x*y-y
Rule guard: [ x>0 && y>=0 ]
WORST_CASE(EXP,?)