let A be Element of LTLB_WFF ; :: thesis: for n being Element of NAT
for M being LTLModel
for f being Function of LTLB_WFF,BOOLEAN st ( for B being object st B in LTLB_WFF holds
f . B = (SAT M) . [n,B] ) holds
(VAL f) . A = (SAT M) . [n,A]
let n be Element of NAT ; :: thesis: for M being LTLModel
for f being Function of LTLB_WFF,BOOLEAN st ( for B being object st B in LTLB_WFF holds
f . B = (SAT M) . [n,B] ) holds
(VAL f) . A = (SAT M) . [n,A]
let M be LTLModel; :: thesis: for f being Function of LTLB_WFF,BOOLEAN st ( for B being object st B in LTLB_WFF holds
f . B = (SAT M) . [n,B] ) holds
(VAL f) . A = (SAT M) . [n,A]
let f be Function of LTLB_WFF,BOOLEAN; :: thesis: ( ( for B being object st B in LTLB_WFF holds
f . B = (SAT M) . [n,B] ) implies (VAL f) . A = (SAT M) . [n,A] )
defpred S1[ Element of LTLB_WFF ] means (VAL f) . $1 = (SAT M) . [n,$1];
assume A1: for B being object st B in LTLB_WFF holds
f . B = (SAT M) . [n,B] ; :: thesis: (VAL f) . A = (SAT M) . [n,A]
A2: for k being Element of NAT holds S1[ prop k]
proof
let k be Element of NAT ; :: thesis: S1[ prop k]
(SAT M) . [n,(prop k)] = f . (prop k) by A1
.= (VAL f) . (prop k) by Def15 ;
hence S1[ prop k] ; :: thesis: verum
end;
A3: for r, s being Element of LTLB_WFF st S1[r] & S1[s] holds
( S1[r 'U' s] & S1[r => s] )
proof
let r, s be Element of LTLB_WFF ; :: thesis: ( S1[r] & S1[s] implies ( S1[r 'U' s] & S1[r => s] ) )
assume A4: ( S1[r] & S1[s] ) ; :: thesis: ( S1[r 'U' s] & S1[r => s] )
(VAL f) . (r 'U' s) = f . (r 'U' s) by Def15
.= (SAT M) . [n,(r 'U' s)] by A1 ;
hence S1[r 'U' s] ; :: thesis: S1[r => s]
(SAT M) . [n,(r => s)] = ((SAT M) . [n,r]) => ((SAT M) . [n,s]) by Def11
.= (VAL f) . (r => s) by A4, Def15 ;
hence S1[r => s] ; :: thesis: verum
end;
(SAT M) . [n,TFALSUM] = 0 by Def11
.= (VAL f) . TFALSUM by Def15 ;
then A5: S1[ TFALSUM ] ;
for r being Element of LTLB_WFF holds S1[r] from HILBERT2:sch 2(A5, A2, A3);
 hence (VAL f) . A = (SAT M) . [n,A] ; :: thesis: verum