for H, v being LTL-formula
for s0, s1 being strict elementary LTLnode over v st s1 is_next_of s0 & H in the LTLold of s1 holds
( ( H is conjunctive implies ( the_left_argument_of H in the LTLold of s1 & the_right_argument_of H in the LTLold of s1 ) ) & ( ( not H is disjunctive & not H is Until ) or the_left_argument_of H in the LTLold of s1 or the_right_argument_of H in the LTLold of s1 ) & ( H is next implies the_argument_of H in the LTLnext of s1 ) & ( H is Release implies the_right_argument_of H in the LTLold of s1 ) )