:: deftheorem Def3 defines LTLNext MODELC_3:def 3 :
for H being LTL-formula holds
( ( H is conjunctive implies LTLNext H = {} ) & ( H is disjunctive implies LTLNext H = {} ) & ( H is next implies LTLNext H = {(the_argument_of H)} ) & ( H is Until implies LTLNext H = {H} ) & ( H is Release implies LTLNext H = {H} ) & ( not H is conjunctive & not H is disjunctive & not H is next & not H is Until & not H is Release implies LTLNext H = {} ) );