:: deftheorem defines is_subformula_of MODELC_2:def 22 :
for H, F being LTL-formula holds
( H is_subformula_of F iff ex n being Nat ex L being FinSequence st
( 1 <= n & len L = n & L . 1 = H & L . n = F & ( for k being Nat st 1 <= k & k < n holds
ex H1, F1 being LTL-formula st
( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) ) );