Meaning of the annotations for the proof of each method: - local_polyh: uses a local linear ranking function for the binary unfolding with polyhedra - local_mono: uses a local linear ranking function for the binary unfolding with monotonicity constraints - global_affrnkfn: uses a global affine ranking function with polyhedra - numerical: the ranking function uses numerical variables or fields - structural: the ranking function uses reference variables or fields - loop: the method seems to be part of a loop or recursion All calls to these methods terminate: [loop,numerical,local_polyh] public static Sequence.main(java.lang.String[]):void Some calls to these methods might not terminate: none There are no warnings