defpred S_{1}[ object ] means for D being set st D is with_LTL_axioms holds

$1 in D;

consider D0 being set such that

A1: for x being object holds

( x in D0 iff ( x in LTLB_WFF & S_{1}[x] ) )
from XBOOLE_0:sch 1();

D0 c= LTLB_WFF by A1;

then reconsider D0 = D0 as Subset of LTLB_WFF ;

take D0 ; :: thesis: ( D0 is with_LTL_axioms & ( for D being Subset of LTLB_WFF st D is with_LTL_axioms holds

D0 c= D ) )

thus D0 is with_LTL_axioms :: thesis: for D being Subset of LTLB_WFF st D is with_LTL_axioms holds

D0 c= D

assume A2: D is with_LTL_axioms ; :: thesis: D0 c= D

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in D0 or x in D )

assume x in D0 ; :: thesis: x in D

hence x in D by A1, A2; :: thesis: verum

$1 in D;

consider D0 being set such that

A1: for x being object holds

( x in D0 iff ( x in LTLB_WFF & S

D0 c= LTLB_WFF by A1;

then reconsider D0 = D0 as Subset of LTLB_WFF ;

take D0 ; :: thesis: ( D0 is with_LTL_axioms & ( for D being Subset of LTLB_WFF st D is with_LTL_axioms holds

D0 c= D ) )

thus D0 is with_LTL_axioms :: thesis: for D being Subset of LTLB_WFF st D is with_LTL_axioms holds

D0 c= D

proof

let D be Subset of LTLB_WFF; :: thesis: ( D is with_LTL_axioms implies D0 c= D )
let p, q be Element of LTLB_WFF ; :: according to LTLAXIO1:def 17 :: thesis: ( ( p is LTL_TAUT_OF_PL implies p in D0 ) & ('not' ('X' p)) => ('X' ('not' p)) in D0 & ('X' ('not' p)) => ('not' ('X' p)) in D0 & ('X' (p => q)) => (('X' p) => ('X' q)) in D0 & ('G' p) => (p '&&' ('X' ('G' p))) in D0 & (p 'U' q) => (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) in D0 & (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) => (p 'U' q) in D0 & (p 'U' q) => ('X' ('F' q)) in D0 )

thus ( p is LTL_TAUT_OF_PL implies p in D0 ) :: thesis: ( ('not' ('X' p)) => ('X' ('not' p)) in D0 & ('X' ('not' p)) => ('not' ('X' p)) in D0 & ('X' (p => q)) => (('X' p) => ('X' q)) in D0 & ('G' p) => (p '&&' ('X' ('G' p))) in D0 & (p 'U' q) => (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) in D0 & (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) => (p 'U' q) in D0 & (p 'U' q) => ('X' ('F' q)) in D0 )

('not' ('X' p)) => ('X' ('not' p)) in D ;

hence ('not' ('X' p)) => ('X' ('not' p)) in D0 by A1; :: thesis: ( ('X' ('not' p)) => ('not' ('X' p)) in D0 & ('X' (p => q)) => (('X' p) => ('X' q)) in D0 & ('G' p) => (p '&&' ('X' ('G' p))) in D0 & (p 'U' q) => (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) in D0 & (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) => (p 'U' q) in D0 & (p 'U' q) => ('X' ('F' q)) in D0 )

for D being set st D is with_LTL_axioms holds

('X' ('not' p)) => ('not' ('X' p)) in D ;

hence ('X' ('not' p)) => ('not' ('X' p)) in D0 by A1; :: thesis: ( ('X' (p => q)) => (('X' p) => ('X' q)) in D0 & ('G' p) => (p '&&' ('X' ('G' p))) in D0 & (p 'U' q) => (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) in D0 & (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) => (p 'U' q) in D0 & (p 'U' q) => ('X' ('F' q)) in D0 )

for D being set st D is with_LTL_axioms holds

('X' (p => q)) => (('X' p) => ('X' q)) in D ;

hence ('X' (p => q)) => (('X' p) => ('X' q)) in D0 by A1; :: thesis: ( ('G' p) => (p '&&' ('X' ('G' p))) in D0 & (p 'U' q) => (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) in D0 & (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) => (p 'U' q) in D0 & (p 'U' q) => ('X' ('F' q)) in D0 )

for D being set st D is with_LTL_axioms holds

('G' p) => (p '&&' ('X' ('G' p))) in D ;

hence ('G' p) => (p '&&' ('X' ('G' p))) in D0 by A1; :: thesis: ( (p 'U' q) => (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) in D0 & (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) => (p 'U' q) in D0 & (p 'U' q) => ('X' ('F' q)) in D0 )

for D being set st D is with_LTL_axioms holds

(p 'U' q) => (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) in D ;

hence (p 'U' q) => (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) in D0 by A1; :: thesis: ( (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) => (p 'U' q) in D0 & (p 'U' q) => ('X' ('F' q)) in D0 )

for D being set st D is with_LTL_axioms holds

(('X' q) 'or' ('X' (p '&&' (p 'U' q)))) => (p 'U' q) in D ;

hence (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) => (p 'U' q) in D0 by A1; :: thesis: (p 'U' q) => ('X' ('F' q)) in D0

for D being set st D is with_LTL_axioms holds

(p 'U' q) => ('X' ('F' q)) in D ;

hence (p 'U' q) => ('X' ('F' q)) in D0 by A1; :: thesis: verum

end;thus ( p is LTL_TAUT_OF_PL implies p in D0 ) :: thesis: ( ('not' ('X' p)) => ('X' ('not' p)) in D0 & ('X' ('not' p)) => ('not' ('X' p)) in D0 & ('X' (p => q)) => (('X' p) => ('X' q)) in D0 & ('G' p) => (p '&&' ('X' ('G' p))) in D0 & (p 'U' q) => (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) in D0 & (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) => (p 'U' q) in D0 & (p 'U' q) => ('X' ('F' q)) in D0 )

proof

for D being set st D is with_LTL_axioms holds
assume
p is LTL_TAUT_OF_PL
; :: thesis: p in D0

then for D being set st D is with_LTL_axioms holds

p in D ;

hence p in D0 by A1; :: thesis: verum

end;then for D being set st D is with_LTL_axioms holds

p in D ;

hence p in D0 by A1; :: thesis: verum

('not' ('X' p)) => ('X' ('not' p)) in D ;

hence ('not' ('X' p)) => ('X' ('not' p)) in D0 by A1; :: thesis: ( ('X' ('not' p)) => ('not' ('X' p)) in D0 & ('X' (p => q)) => (('X' p) => ('X' q)) in D0 & ('G' p) => (p '&&' ('X' ('G' p))) in D0 & (p 'U' q) => (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) in D0 & (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) => (p 'U' q) in D0 & (p 'U' q) => ('X' ('F' q)) in D0 )

for D being set st D is with_LTL_axioms holds

('X' ('not' p)) => ('not' ('X' p)) in D ;

hence ('X' ('not' p)) => ('not' ('X' p)) in D0 by A1; :: thesis: ( ('X' (p => q)) => (('X' p) => ('X' q)) in D0 & ('G' p) => (p '&&' ('X' ('G' p))) in D0 & (p 'U' q) => (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) in D0 & (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) => (p 'U' q) in D0 & (p 'U' q) => ('X' ('F' q)) in D0 )

for D being set st D is with_LTL_axioms holds

('X' (p => q)) => (('X' p) => ('X' q)) in D ;

hence ('X' (p => q)) => (('X' p) => ('X' q)) in D0 by A1; :: thesis: ( ('G' p) => (p '&&' ('X' ('G' p))) in D0 & (p 'U' q) => (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) in D0 & (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) => (p 'U' q) in D0 & (p 'U' q) => ('X' ('F' q)) in D0 )

for D being set st D is with_LTL_axioms holds

('G' p) => (p '&&' ('X' ('G' p))) in D ;

hence ('G' p) => (p '&&' ('X' ('G' p))) in D0 by A1; :: thesis: ( (p 'U' q) => (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) in D0 & (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) => (p 'U' q) in D0 & (p 'U' q) => ('X' ('F' q)) in D0 )

for D being set st D is with_LTL_axioms holds

(p 'U' q) => (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) in D ;

hence (p 'U' q) => (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) in D0 by A1; :: thesis: ( (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) => (p 'U' q) in D0 & (p 'U' q) => ('X' ('F' q)) in D0 )

for D being set st D is with_LTL_axioms holds

(('X' q) 'or' ('X' (p '&&' (p 'U' q)))) => (p 'U' q) in D ;

hence (('X' q) 'or' ('X' (p '&&' (p 'U' q)))) => (p 'U' q) in D0 by A1; :: thesis: (p 'U' q) => ('X' ('F' q)) in D0

for D being set st D is with_LTL_axioms holds

(p 'U' q) => ('X' ('F' q)) in D ;

hence (p 'U' q) => ('X' ('F' q)) in D0 by A1; :: thesis: verum

assume A2: D is with_LTL_axioms ; :: thesis: D0 c= D

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in D0 or x in D )

assume x in D0 ; :: thesis: x in D

hence x in D by A1, A2; :: thesis: verum