:: deftheorem defines len MODELC_3:def 29 :
for v being LTL-formula
for N being strict LTLnode over v holds len N = [\(len the LTLnew of N)/];