let A be Element of LTLB_WFF ; 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 ; 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; 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; ( ( 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]
; (VAL f) . A = (SAT M) . [n,A]
A2:
for k being Element of NAT holds S1[ prop k]
A3:
for r, s being Element of LTLB_WFF st S1[r] & S1[s] holds
( S1[r 'U' s] & S1[r => s] )
(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]
; verum