for H being LTL-formula st ( H is negative or H is next ) holds
( len H = 1 + (len (the_argument_of H)) & len (the_argument_of H) < len H )