:: deftheorem Def24 defines Partial_seq MODELC_3:def 24 :
for H being LTL-formula
for W being Subset of (Subformulae H)
for L being FinSequence
for b₄ being Real_Sequence holds
( b₄ = Partial_seq (L,W) iff for k being Nat holds
( ( L . k in W implies b₄ . k = len (CastLTL (L . k)) ) & ( not L . k in W implies b₄ . k = 0 ) ) );