for F, v being LTL-formula
for N1, N2 being strict LTLnode over v st N2 is_succ_of N1,F holds
F in the LTLold of N2