:: deftheorem Def14 defines complete LTLAXIO4:def 14 :
for P being consistent PNPair
for T being pnptree of P
for t being path of T holds
( t is complete iff for A, B being Element of LTLB_WFF
for i being Nat st A 'U' B in rng ((T . (t . i)) `1) holds
ex j being Element of NAT st
( j > i & B in rng ((T . (t . j)) `1) & ( for k being Element of NAT st i < k & k < j holds
A in rng ((T . (t . k)) `1) ) ) );