for F, H being LTL-formula holds
( not H is_immediate_constituent_of F or F is negative or F is next or F is conjunctive or F is disjunctive or F is Until or F is Release ) ;