:: deftheorem defines is_immediate_constituent_of MODELC_2:def 21 :
for H, F being LTL-formula holds
( H is_immediate_constituent_of F iff ( F = 'not' H or F = 'X' H or ex H1 being LTL-formula st
( F = H '&' H1 or F = H1 '&' H or F = H 'or' H1 or F = H1 'or' H or F = H 'U' H1 or F = H1 'U' H or F = H 'R' H1 or F = H1 'R' H ) ) );