:: deftheorem Def35 defines chosen_succ MODELC_3:def 35 :
for w being Element of Inf_seq AtomicFamily
for v being LTL-formula
for U being Choice_Function of (BOOL (Subformulae v))
for N being strict LTLnode over v holds
( ( ( ( not chosen_formula (U,N) is Until & w |= * (SuccNode1 ((chosen_formula (U,N)),N)) ) or ( chosen_formula (U,N) is Until & w |/= the_right_argument_of (chosen_formula (U,N)) ) ) implies chosen_succ (w,v,U,N) = SuccNode1 ((chosen_formula (U,N)),N) ) & ( ( not chosen_formula (U,N) is Until & w |= * (SuccNode1 ((chosen_formula (U,N)),N)) ) or ( chosen_formula (U,N) is Until & w |/= the_right_argument_of (chosen_formula (U,N)) ) or chosen_succ (w,v,U,N) = SuccNode2 ((chosen_formula (U,N)),N) ) );