### Pre-processing the ITS problem ### Initial linear ITS problem Start location: f0 0: f0 -> f : [], cost: 0 1: f -> f : x'=1+x, [ 0 f : [], cost: 0 1: f -> f : x'=1+x, [ 0=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, [ 0=0 ], cost: y Accelerated rule 1 with NONTERM, 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 -> [2] : [ 0=1 ], cost: NONTERM Chained accelerated rules (with incoming rules): Start location: f0 0: f0 -> f : [], cost: 0 3: f0 -> [2] : [ 0=1 ], cost: NONTERM Removed unreachable locations (and leaf rules with constant cost): Start location: f0 3: f0 -> [2] : [ 0=1 ], cost: NONTERM ### Computing asymptotic complexity ### Fully simplified ITS problem Start location: f0 3: f0 -> [2] : [ 0=1 ], cost: NONTERM Computing asymptotic complexity for rule 3 Guard is satisfiable, yielding nontermination Resulting cost NONTERM has complexity: Nonterm Found new complexity Nonterm. Obtained the following overall complexity (w.r.t. the length of the input n): Complexity: Nonterm Cpx degree: Nonterm Solved cost: NONTERM Rule cost: NONTERM Rule guard: [ 0=1 ] NO