:: deftheorem defines len MODELC_3:def 25 :
for H being LTL-formula
for W being Subset of (Subformulae H)
for L being FinSequence holds len (L,W) = Sum ((Partial_seq (L,W)),(len L));