:: deftheorem defines failure MODELC_3:def 10 :
for v being LTL-formula
for N being LTLnode over v holds
( N is failure iff ex H, F being LTL-formula st
( H is atomic & F = 'not' H & H in the LTLold of N & F in the LTLold of N ) );