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