:: deftheorem Def2 defines LTLNew2 MODELC_3:def 2 :
for H being LTL-formula holds
( ( H is conjunctive implies LTLNew2 H = {} ) & ( H is disjunctive implies LTLNew2 H = {(the_right_argument_of H)} ) & ( H is next implies LTLNew2 H = {} ) & ( H is Until implies LTLNew2 H = {(the_right_argument_of H)} ) & ( H is Release implies LTLNew2 H = {(the_left_argument_of 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 LTLNew2 H = {} ) );