for H being LTL-formula st ( H is conjunctive or H is disjunctive or H is Until or H is Release ) holds
( len H = (1 + (len (the_left_argument_of H))) + (len (the_right_argument_of H)) & len (the_left_argument_of H) < len H & len (the_right_argument_of H) < len H )