NO Initial ITS Start location: l3 0: l0 -> l1 : 0 <= 0, cost: 1 1: l1 -> l0 : 0 <= 0, cost: 1 2: l2 -> l0 : 0 <= 0, cost: 1 3: l3 -> l2 : 0 <= 0, cost: 1 Eliminating location l2 by chaining: Applied chaining First rule: l3 -> l2 : 0 <= 0, cost: 1 Second rule: l2 -> l0 : 0 <= 0, cost: 1 New rule: l3 -> l0 : 0 <= 0, cost: 2 Applied deletion Removed the following rules: 2 3 Eliminating location l1 by chaining: Applied chaining First rule: l0 -> l1 : 0 <= 0, cost: 1 Second rule: l1 -> l0 : 0 <= 0, cost: 1 New rule: l0 -> l0 : 0 <= 0, cost: 2 Applied deletion Removed the following rules: 0 1 Eliminated locations on linear paths Start location: l3 5: l0 -> l0 : 0 <= 0, cost: 2 4: l3 -> l0 : 0 <= 0, cost: 2 Applied nonterm Original rule: l0 -> l0 : 0 <= 0, cost: 2 New rule: l0 -> [4] : (0 >= 0 /\ n >= 0), cost: NONTERM Sub-proof via acceration calculus written to file:///tmp/tmpnam_iFIbiC.txt Applied simplification Original rule: l0 -> [4] : (0 >= 0 /\ n >= 0), cost: NONTERM New rule: l0 -> [4] : n >= 0, cost: NONTERM Applied deletion Removed the following rules: 5 Accelerated simple loops Start location: l3 7: l0 -> [4] : n >= 0, cost: NONTERM 4: l3 -> l0 : 0 <= 0, cost: 2 Applied chaining First rule: l3 -> l0 : 0 <= 0, cost: 2 Second rule: l0 -> [4] : n >= 0, cost: NONTERM New rule: l3 -> [4] : 0 <= 0, cost: NONTERM Applied deletion Removed the following rules: 7 Chained accelerated rules with incoming rules Start location: l3 4: l3 -> l0 : 0 <= 0, cost: 2 8: l3 -> [4] : 0 <= 0, cost: NONTERM Removed unreachable locations and irrelevant leafs Start location: l3 8: l3 -> [4] : 0 <= 0, cost: NONTERM Computing asymptotic complexity Proved nontermination of rule 8 via SMT. Proved the following lower bound Complexity: Nonterm Cpx degree: Nonterm Solved cost: NONTERM Rule cost: NONTERM Rule guard: 0 <= 0