:: deftheorem Def23 defines Length_fun MODELC_3:def 23 :
for H being LTL-formula
for W being Subset of (Subformulae H)
for L being FinSequence
for x being set holds
( ( L . x in W implies Length_fun (L,W,x) = len (CastLTL (L . x)) ) & ( not L . x in W implies Length_fun (L,W,x) = 0 ) );