:: deftheorem Def1 defines LTLNew1 MODELC_3:def 1 :
for H being LTL-formula holds
( ( H is conjunctive implies LTLNew1 H = {(the_left_argument_of H),(the_right_argument_of H)} ) & ( H is disjunctive implies LTLNew1 H = {(the_left_argument_of H)} ) & ( H is next implies LTLNew1 H = {} ) & ( H is Until implies LTLNew1 H = {(the_left_argument_of H)} ) & ( H is Release implies LTLNew1 H = {(the_right_argument_of H)} ) & ( not H is conjunctive & not H is disjunctive & not H is next & not H is Until & not H is Release implies LTLNew1 H = {} ) );