We give a sound and complete labeled natural deduction system for an interesting fragment of , namely the until-free version of . The logic is obtained by referring to a more general semantics than that of , where we only require that the set of paths in a model is closed under taking suffixes (i.e. is suffix-closed) and is closed under putting together a finite prefix of one path with the suffix of any other path beginning at the same state where the prefix ends (i.e. is fusion-closed). In other words, this logic does not enjoy the so-called limit-closure property of the standard validity semantics.