:: deftheorem defines is_succ_of MODELC_3:def 6 :
for v being LTL-formula
for N1, N2 being LTLnode over v
for H being LTL-formula holds
( N2 is_succ_of N1,H iff ( H in the LTLnew of N1 & ( N2 = SuccNode1 (H,N1) or ( ( H is disjunctive or H is Until or H is Release ) & N2 = SuccNode2 (H,N1) ) ) ) );