:: deftheorem Def48 defines chosen_succ_end_num MODELC_3:def 48 :
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 not N is elementary & w |= * N holds
for b₅ being Nat holds
( b₅ = chosen_succ_end_num (w,v,U,N) iff ( ( for i being Nat st i < b₅ holds
( not CastNode ((((choice_succ_func (w,v,U)) |** i) . N),v) is elementary & CastNode ((((choice_succ_func (w,v,U)) |** (i + 1)) . N),v) is_succ_of CastNode ((((choice_succ_func (w,v,U)) |** i) . N),v) ) ) & CastNode ((((choice_succ_func (w,v,U)) |** b₅) . N),v) is elementary & ( for i being Nat st i <= b₅ holds
w |= * (CastNode ((((choice_succ_func (w,v,U)) |** i) . N),v)) ) ) );