:: deftheorem Def50 defines chosen_run MODELC_3:def 50 :
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 b₄ being sequence of (LTLStates v) holds
( b₄ = chosen_run (w,v,U) iff ( b₄ . 0 = init v & ( for n being Nat holds b₄ . (n + 1) = chosen_next ((Shift (w,n)),v,U,(CastNode ((b₄ . n),v))) ) ) );