MAYBE Initial complexity problem: 1: T: (?, 1) f(a) -> f(a) [ 0 >= a^2 + 1 ] (1, 1) start(a) -> f(a) start location: start leaf cost: 0 By chaining the transition start(a) -> f(a) with all transitions in problem 1, the following new transition is obtained: start(a) -> f(a) [ 0 >= a^2 + 1 ] We thus obtain the following problem: 2: T: (1, 2) start(a) -> f(a) [ 0 >= a^2 + 1 ] (?, 1) f(a) -> f(a) [ 0 >= a^2 + 1 ] start location: start leaf cost: 0 Complexity upper bound ? Time: 0.089 sec (SMT: 0.083 sec)