:: deftheorem defines Tran_LTL MODELC_3:def 43 :
for v being neg-inner-most LTL-formula holds Tran_LTL v = { y where y is Element of [:(LTLStates v),AtomicFamily,(LTLStates v):] : ex s, s1 being strict elementary LTLnode over v ex x being set st
( y = [[s,x],s1] & s1 is_next_of s & x in Label_ s1 ) } ;