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 S_{1}[ 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 S_{1}[ prop k]
_{1}[r] & S_{1}[s] holds

( S_{1}[r 'U' s] & S_{1}[r => s] )

.= (VAL f) . TFALSUM by Def15 ;

then A5: S_{1}[ TFALSUM ]
;

for r being Element of LTLB_WFF holds S_{1}[r]
from HILBERT2:sch 2(A5, A2, A3);

hence (VAL f) . A = (SAT M) . [n,A] ; :: thesis: verum

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 S

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 S

proof

A3:
for r, s being Element of LTLB_WFF st S
let k be Element of NAT ; :: thesis: S_{1}[ prop k]

(SAT M) . [n,(prop k)] = f . (prop k) by A1

.= (VAL f) . (prop k) by Def15 ;

hence S_{1}[ prop k]
; :: thesis: verum

end;(SAT M) . [n,(prop k)] = f . (prop k) by A1

.= (VAL f) . (prop k) by Def15 ;

hence S

( S

proof

(SAT M) . [n,TFALSUM] =
0
by Def11
let r, s be Element of LTLB_WFF ; :: thesis: ( S_{1}[r] & S_{1}[s] implies ( S_{1}[r 'U' s] & S_{1}[r => s] ) )

assume A4: ( S_{1}[r] & S_{1}[s] )
; :: thesis: ( S_{1}[r 'U' s] & S_{1}[r => s] )

(VAL f) . (r 'U' s) = f . (r 'U' s) by Def15

.= (SAT M) . [n,(r 'U' s)] by A1 ;

hence S_{1}[r 'U' s]
; :: thesis: S_{1}[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 S_{1}[r => s]
; :: thesis: verum

end;assume A4: ( S

(VAL f) . (r 'U' s) = f . (r 'U' s) by Def15

.= (SAT M) . [n,(r 'U' s)] by A1 ;

hence S

(SAT M) . [n,(r => s)] = ((SAT M) . [n,r]) => ((SAT M) . [n,s]) by Def11

.= (VAL f) . (r => s) by A4, Def15 ;

hence S

.= (VAL f) . TFALSUM by Def15 ;

then A5: S

for r being Element of LTLB_WFF holds S

hence (VAL f) . A = (SAT M) . [n,A] ; :: thesis: verum