### Pre-processing the ITS problem ###
Initial linear ITS problem
Start location: f0
0: f0 -> f : [], cost: 0
1: f -> f : x'=-z+x-y, [ x>0 && z+y==1 ], 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'=-z+x-y, [ x>0 && z+y==1 ], cost: 1
Accelerated rule 1 with metering function 1-z+x-y, 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'=z*(-1+z-x+y)+x+(-1+z-x+y)*y, [ x>0 && z+y==1 && 1-z+x-y>=1 ], cost: 1-z+x-y
Chained accelerated rules (with incoming rules):
Start location: f0
0: f0 -> f : [], cost: 0
3: f0 -> f : x'=z*(-1+z-x+y)+x+(-1+z-x+y)*y, [ x>0 && z+y==1 && 1-z+x-y>=1 ], cost: 1-z+x-y
Removed unreachable locations (and leaf rules with constant cost):
Start location: f0
3: f0 -> f : x'=z*(-1+z-x+y)+x+(-1+z-x+y)*y, [ x>0 && z+y==1 && 1-z+x-y>=1 ], cost: 1-z+x-y
### Computing asymptotic complexity ###
Fully simplified ITS problem
Start location: f0
3: f0 -> f : x'=z*(-1+z-x+y)+x+(-1+z-x+y)*y, [ x>0 && z+y==1 && 1-z+x-y>=1 ], cost: 1-z+x-y
Computing asymptotic complexity for rule 3
Solved the limit problem by the following transformations:
Created initial limit problem:
1-z+x-y (+), x (+/+!), z+y (+/+!), 2-z-y (+/+!) [not solved]
removing all constraints (solved by SMT)
resulting limit problem: [solved]
applying transformation rule (C) using substitution {z==1,x==n,y==0}
resulting limit problem:
[solved]
Solution:
z / 1
x / n
y / 0
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: 1-z+x-y
Rule guard: [ x>0 && z+y==1 ]
WORST_CASE(Omega(n^1),?)