:: deftheorem defines is_succ_homomorphism MODELC_3:def 32 :
for v being LTL-formula
for w being Element of Inf_seq AtomicFamily
for f being Function holds
( f is_succ_homomorphism v,w iff for x being set st x in LTLNodes v & not CastNode (x,v) is elementary & w |= * (CastNode (x,v)) holds
( CastNode ((f . x),v) is_succ_of CastNode (x,v) & w |= * (CastNode ((f . x),v)) ) );