:: deftheorem Def49 defines chosen_next MODELC_3:def 49 :
for w being Element of Inf_seq AtomicFamily
for v being neg-inner-most LTL-formula
for U being Choice_Function of (BOOL (Subformulae v))
for N being strict LTLnode over v st w |= * ('X' N) holds
( ( not 'X' N is elementary implies chosen_next (w,v,U,N) = CastNode ((((choice_succ_func (w,v,U)) |** (chosen_succ_end_num (w,v,U,('X' N)))) . ('X' N)),v) ) & ( 'X' N is elementary implies chosen_next (w,v,U,N) = FinalNode v ) );