:: deftheorem Def17 defines with_LTL_axioms LTLAXIO1:def 17 :
for D being set holds
( D is with_LTL_axioms iff for p, q being Element of LTLB_WFF holds
( ( p is LTL_TAUT_OF_PL implies p in D ) & ('not' ('X' p)) => ('X' ('not' p)) in D & ('X' ('not' p)) => ('not' ('X' p)) in D & ('X' (p => q)) => (('X' p) => ('X' q)) in D & ('G' p) => (p '&&' ('X' ('G' p))) in D & (p 'U' q) => (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) in D & (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) => (p 'U' q) in D & (p 'U' q) => ('X' ('F' q)) in D ) );