:: deftheorem Def5 defines SuccNode2 MODELC_3:def 5 :
for v being LTL-formula
for N being LTLnode over v
for H being LTL-formula st H in the LTLnew of N holds
for b₄ being strict LTLnode over v holds
( b₄ = SuccNode2 (H,N) iff ( the LTLold of b₄ = the LTLold of N \/ {H} & the LTLnew of b₄ = ( the LTLnew of N \ {H}) \/ ((LTLNew2 H) \ the LTLold of N) & the LTLnext of b₄ = the LTLnext of N ) );