:: deftheorem Def36 defines choice_succ_func MODELC_3:def 36 :
for w being Element of Inf_seq AtomicFamily
for v being LTL-formula
for U being Choice_Function of (BOOL (Subformulae v))
for b₄ being Function of (LTLNodes v),(LTLNodes v) holds
( b₄ = choice_succ_func (w,v,U) iff for x being set st x in LTLNodes v holds
b₄ . x = chosen_succ (w,v,U,(CastNode (x,v))) );