set FNB = Funcs (NAT,BOOLEAN);

defpred S_{1}[ Element of LTLB_WFF , Element of LTLB_WFF , set , set , set ] means ( ( $3 is sequence of BOOLEAN & $4 is sequence of BOOLEAN implies ex s3, s4, s5 being sequence of BOOLEAN st

( s3 = $3 & s4 = $4 & s5 = $5 & ( for n being Element of NAT holds s5 . n = (s3 . n) => (s4 . n) ) ) ) & ( ( not $3 is sequence of BOOLEAN or not $4 is sequence of BOOLEAN ) implies $5 = NAT --> FALSE ) );

defpred S_{2}[ Element of LTLB_WFF , Element of LTLB_WFF , set , set , set ] means ( ( $3 is sequence of BOOLEAN & $4 is sequence of BOOLEAN implies ex s3, s4, s5 being sequence of BOOLEAN st

( s3 = $3 & s4 = $4 & s5 = $5 & ( for n being Element of NAT holds

( s5 . n = 1 iff ex i being Element of NAT st

( 0 < i & s4 . (n + i) = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

s3 . (n + j) = 1 ) ) ) ) ) ) & ( ( not $3 is sequence of BOOLEAN or not $4 is sequence of BOOLEAN ) implies $5 = NAT --> FALSE ) );

defpred S_{3}[ Element of NAT , Function] means for n being Element of NAT holds

( $2 . n = 1 iff prop $1 in M . n );

A1: for p, q being Element of LTLB_WFF

for a, b being set ex d being set st S_{2}[p,q,a,b,d]

for a, b, c, d being set st S_{2}[p,q,a,b,c] & S_{2}[p,q,a,b,d] holds

c = d_{3}[x,y]

A19: for k being Element of NAT holds S_{3}[k,f1 . k]
from FUNCT_2:sch 3(A16);

A20: for p, q being Element of LTLB_WFF

for a, b, c, d being set st S_{1}[p,q,a,b,c] & S_{1}[p,q,a,b,d] holds

c = d_{1}( Element of NAT ) -> Element of Funcs (NAT,BOOLEAN) = f1 . $1;

A32: for p, q being Element of LTLB_WFF

for a, b being set ex d being set st S_{1}[p,q,a,b,d]

A34: ( sat . TFALSUM = NAT --> FALSE & ( for n being Element of NAT holds sat . (prop n) = H_{1}(n) ) & ( for p, q being Element of LTLB_WFF holds

( S_{2}[p,q,sat . p,sat . q,sat . (p 'U' q)] & S_{1}[p,q,sat . p,sat . q,sat . (p => q)] ) ) )
from HILBERT2:sch 3(A1, A32, A4, A20);

then reconsider sat = sat as Function of LTLB_WFF,(Funcs (NAT,BOOLEAN)) by A35, FUNCT_2:3;

deffunc H_{2}( Element of NAT , Element of LTLB_WFF ) -> Element of BOOLEAN = (sat . $2) . $1;

consider sat2 being Function of [:NAT,LTLB_WFF:],BOOLEAN such that

A43: for n being Element of NAT

for A being Element of LTLB_WFF holds sat2 . (n,A) = H_{2}(n,A)
from BINOP_1:sch 4();

( sat2 . [n,TFALSUM] = 0 & ( for k being Element of NAT holds

( sat2 . [n,(prop k)] = 1 iff prop k in M . n ) ) & ( for p, q being Element of LTLB_WFF holds

( sat2 . [n,(p => q)] = (sat2 . [n,p]) => (sat2 . [n,q]) & ( sat2 . [n,(p 'U' q)] = 1 implies ex i being Element of NAT st

( 0 < i & sat2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

sat2 . [(n + j),p] = 1 ) ) ) & ( ex i being Element of NAT st

( 0 < i & sat2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

sat2 . [(n + j),p] = 1 ) ) implies sat2 . [n,(p 'U' q)] = 1 ) ) ) )

( sat2 . [n,TFALSUM] = 0 & ( for k being Element of NAT holds

( sat2 . [n,(prop k)] = 1 iff prop k in M . n ) ) & ( for p, q being Element of LTLB_WFF holds

( sat2 . [n,(p => q)] = (sat2 . [n,p]) => (sat2 . [n,q]) & ( sat2 . [n,(p 'U' q)] = 1 implies ex i being Element of NAT st

( 0 < i & sat2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

sat2 . [(n + j),p] = 1 ) ) ) & ( ex i being Element of NAT st

( 0 < i & sat2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

sat2 . [(n + j),p] = 1 ) ) implies sat2 . [n,(p 'U' q)] = 1 ) ) ) ) by A45, A46; :: thesis: verum

defpred S

( s3 = $3 & s4 = $4 & s5 = $5 & ( for n being Element of NAT holds s5 . n = (s3 . n) => (s4 . n) ) ) ) & ( ( not $3 is sequence of BOOLEAN or not $4 is sequence of BOOLEAN ) implies $5 = NAT --> FALSE ) );

defpred S

( s3 = $3 & s4 = $4 & s5 = $5 & ( for n being Element of NAT holds

( s5 . n = 1 iff ex i being Element of NAT st

( 0 < i & s4 . (n + i) = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

s3 . (n + j) = 1 ) ) ) ) ) ) & ( ( not $3 is sequence of BOOLEAN or not $4 is sequence of BOOLEAN ) implies $5 = NAT --> FALSE ) );

defpred S

( $2 . n = 1 iff prop $1 in M . n );

A1: for p, q being Element of LTLB_WFF

for a, b being set ex d being set st S

proof

A4:
for p, q being Element of LTLB_WFF
let p, q be Element of LTLB_WFF ; :: thesis: for a, b being set ex d being set st S_{2}[p,q,a,b,d]

let a, b be set ; :: thesis: ex d being set st S_{2}[p,q,a,b,d]

end;let a, b be set ; :: thesis: ex d being set st S

per cases
( ( a is sequence of BOOLEAN & b is sequence of BOOLEAN ) or not a is sequence of BOOLEAN or not b is sequence of BOOLEAN )
;

end;

suppose
( a is sequence of BOOLEAN & b is sequence of BOOLEAN )
; :: thesis: ex d being set st S_{2}[p,q,a,b,d]

then reconsider a1 = a, b1 = b as sequence of BOOLEAN ;

defpred S_{4}[ Element of NAT , Element of BOOLEAN ] means ( $2 = 1 iff ex i being Element of NAT st

( 0 < i & b1 . ($1 + i) = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

a1 . ($1 + j) = 1 ) ) );

A3: for n being Element of NAT holds S_{4}[n,c . n]
from FUNCT_2:sch 3(A2);

thus ex d being set st S_{2}[p,q,a,b,d]
by A3; :: thesis: verum

end;defpred S

( 0 < i & b1 . ($1 + i) = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

a1 . ($1 + j) = 1 ) ) );

A2: now :: thesis: for n being Element of NAT ex y being Element of BOOLEAN st S_{4}[n,y]

consider c being sequence of BOOLEAN such that let n be Element of NAT ; :: thesis: ex y being Element of BOOLEAN st S_{4}[y,b_{2}]

end;per cases
( ex i being Element of NAT st

( 0 < i & b1 . (n + i) = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

a1 . (n + j) = 1 ) ) or for i being Element of NAT holds

( not 0 < i or not b1 . (n + i) = 1 or ex j being Element of NAT st

( 1 <= j & j < i & not a1 . (n + j) = 1 ) ) ) ;

end;

( 0 < i & b1 . (n + i) = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

a1 . (n + j) = 1 ) ) or for i being Element of NAT holds

( not 0 < i or not b1 . (n + i) = 1 or ex j being Element of NAT st

( 1 <= j & j < i & not a1 . (n + j) = 1 ) ) ) ;

suppose
ex i being Element of NAT st

( 0 < i & b1 . (n + i) = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

a1 . (n + j) = 1 ) ) ; :: thesis: ex y being Element of BOOLEAN st S_{4}[y,b_{2}]

end;

( 0 < i & b1 . (n + i) = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

a1 . (n + j) = 1 ) ) ; :: thesis: ex y being Element of BOOLEAN st S

end;

A3: for n being Element of NAT holds S

thus ex d being set st S

suppose
( not a is sequence of BOOLEAN or not b is sequence of BOOLEAN )
; :: thesis: ex d being set st S_{2}[p,q,a,b,d]

end;

end;

for a, b, c, d being set st S

c = d

proof

A16:
for x being Element of NAT ex y being Element of Funcs (NAT,BOOLEAN) st S
let p, q be Element of LTLB_WFF ; :: thesis: for a, b, c, d being set st S_{2}[p,q,a,b,c] & S_{2}[p,q,a,b,d] holds

c = d

let a, b, c, d be set ; :: thesis: ( S_{2}[p,q,a,b,c] & S_{2}[p,q,a,b,d] implies c = d )

assume that

A5: S_{2}[p,q,a,b,c]
and

A6: S_{2}[p,q,a,b,d]
; :: thesis: c = d

end;c = d

let a, b, c, d be set ; :: thesis: ( S

assume that

A5: S

A6: S

per cases
( ( a is sequence of BOOLEAN & b is sequence of BOOLEAN ) or not a is sequence of BOOLEAN or not b is sequence of BOOLEAN )
;

end;

suppose A7:
( a is sequence of BOOLEAN & b is sequence of BOOLEAN )
; :: thesis: c = d

then consider s31, s41, s51 being sequence of BOOLEAN such that

A8: ( s31 = a & s41 = b ) and

A9: s51 = d and

A10: for n being Element of NAT holds

( s51 . n = 1 iff ex i being Element of NAT st

( 0 < i & s41 . (n + i) = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

s31 . (n + j) = 1 ) ) ) by A6;

consider s3, s4, s5 being sequence of BOOLEAN such that

A11: ( s3 = a & s4 = b ) and

A12: s5 = c and

A13: for n being Element of NAT holds

( s5 . n = 1 iff ex i being Element of NAT st

( 0 < i & s4 . (n + i) = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

s3 . (n + j) = 1 ) ) ) by A5, A7;

end;A8: ( s31 = a & s41 = b ) and

A9: s51 = d and

A10: for n being Element of NAT holds

( s51 . n = 1 iff ex i being Element of NAT st

( 0 < i & s41 . (n + i) = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

s31 . (n + j) = 1 ) ) ) by A6;

consider s3, s4, s5 being sequence of BOOLEAN such that

A11: ( s3 = a & s4 = b ) and

A12: s5 = c and

A13: for n being Element of NAT holds

( s5 . n = 1 iff ex i being Element of NAT st

( 0 < i & s4 . (n + i) = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

s3 . (n + j) = 1 ) ) ) by A5, A7;

now :: thesis: for x being object st x in NAT holds

s5 . x = s51 . x

hence
c = d
by A12, A9, FUNCT_2:12; :: thesis: verums5 . x = s51 . x

let x be object ; :: thesis: ( x in NAT implies s5 . b_{1} = s51 . b_{1} )

assume x in NAT ; :: thesis: s5 . b_{1} = s51 . b_{1}

then reconsider x1 = x as Element of NAT ;

end;assume x in NAT ; :: thesis: s5 . b

then reconsider x1 = x as Element of NAT ;

per cases
( s5 . x1 = 1 or s5 . x1 = 0 )
by XBOOLEAN:def 3;

end;

suppose A14:
s5 . x1 = 1
; :: thesis: s5 . b_{1} = s51 . b_{1}

then
ex i being Element of NAT st

( 0 < i & s41 . (x1 + i) = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

s31 . (x1 + j) = 1 ) ) by A11, A13, A8;

hence s5 . x = s51 . x by A10, A14; :: thesis: verum

end;( 0 < i & s41 . (x1 + i) = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

s31 . (x1 + j) = 1 ) ) by A11, A13, A8;

hence s5 . x = s51 . x by A10, A14; :: thesis: verum

suppose A15:
s5 . x1 = 0
; :: thesis: s5 . b_{1} = s51 . b_{1}

then
for i being Element of NAT holds

( not 0 < i or not s41 . (x1 + i) = 1 or ex j being Element of NAT st

( 1 <= j & j < i & not s31 . (x1 + j) = 1 ) ) by A11, A13, A8;

hence s5 . x = s51 . x by A15, XBOOLEAN:def 3, A10; :: thesis: verum

end;( not 0 < i or not s41 . (x1 + i) = 1 or ex j being Element of NAT st

( 1 <= j & j < i & not s31 . (x1 + j) = 1 ) ) by A11, A13, A8;

hence s5 . x = s51 . x by A15, XBOOLEAN:def 3, A10; :: thesis: verum

proof

consider f1 being sequence of (Funcs (NAT,BOOLEAN)) such that
let x be Element of NAT ; :: thesis: ex y being Element of Funcs (NAT,BOOLEAN) st S_{3}[x,y]

defpred S_{4}[ Element of NAT , Element of BOOLEAN ] means ( $2 = 1 iff prop x in M . $1 );

A18: for n being Element of NAT holds S_{4}[n,y . n]
from FUNCT_2:sch 3(A17);

reconsider y = y as Element of Funcs (NAT,BOOLEAN) by FUNCT_2:8;

S_{3}[x,y]
by A18;

hence ex y being Element of Funcs (NAT,BOOLEAN) st S_{3}[x,y]
; :: thesis: verum

end;defpred S

A17: now :: thesis: for x1 being Element of NAT ex y1 being Element of BOOLEAN st S_{4}[x1,y1]

consider y being sequence of BOOLEAN such that let x1 be Element of NAT ; :: thesis: ex y1 being Element of BOOLEAN st S_{4}[y1,b_{2}]

end;A18: for n being Element of NAT holds S

reconsider y = y as Element of Funcs (NAT,BOOLEAN) by FUNCT_2:8;

S

hence ex y being Element of Funcs (NAT,BOOLEAN) st S

A19: for k being Element of NAT holds S

A20: for p, q being Element of LTLB_WFF

for a, b, c, d being set st S

c = d

proof

deffunc H
let p, q be Element of LTLB_WFF ; :: thesis: for a, b, c, d being set st S_{1}[p,q,a,b,c] & S_{1}[p,q,a,b,d] holds

c = d

let a, b, c, d be set ; :: thesis: ( S_{1}[p,q,a,b,c] & S_{1}[p,q,a,b,d] implies c = d )

assume that

A21: S_{1}[p,q,a,b,c]
and

A22: S_{1}[p,q,a,b,d]
; :: thesis: c = d

end;c = d

let a, b, c, d be set ; :: thesis: ( S

assume that

A21: S

A22: S

per cases
( ( a is sequence of BOOLEAN & b is sequence of BOOLEAN ) or not a is sequence of BOOLEAN or not b is sequence of BOOLEAN )
;

end;

suppose A23:
( a is sequence of BOOLEAN & b is sequence of BOOLEAN )
; :: thesis: c = d

then consider s31, s41, s51 being sequence of BOOLEAN such that

A24: s31 = a and

A25: s41 = b and

A26: s51 = d and

A27: for n being Element of NAT holds s51 . n = (s31 . n) => (s41 . n) by A22;

consider s3, s4, s5 being sequence of BOOLEAN such that

A28: s3 = a and

A29: s4 = b and

A30: s5 = c and

A31: for n being Element of NAT holds s5 . n = (s3 . n) => (s4 . n) by A21, A23;

end;A24: s31 = a and

A25: s41 = b and

A26: s51 = d and

A27: for n being Element of NAT holds s51 . n = (s31 . n) => (s41 . n) by A22;

consider s3, s4, s5 being sequence of BOOLEAN such that

A28: s3 = a and

A29: s4 = b and

A30: s5 = c and

A31: for n being Element of NAT holds s5 . n = (s3 . n) => (s4 . n) by A21, A23;

now :: thesis: for x being object st x in NAT holds

s5 . x = s51 . x

hence
c = d
by A30, A26, FUNCT_2:12; :: thesis: verums5 . x = s51 . x

let x be object ; :: thesis: ( x in NAT implies s5 . x = s51 . x )

assume x in NAT ; :: thesis: s5 . x = s51 . x

then reconsider x1 = x as Element of NAT ;

thus s5 . x = (s31 . x1) => (s4 . x1) by A28, A31, A24

.= s51 . x by A29, A25, A27 ; :: thesis: verum

end;assume x in NAT ; :: thesis: s5 . x = s51 . x

then reconsider x1 = x as Element of NAT ;

thus s5 . x = (s31 . x1) => (s4 . x1) by A28, A31, A24

.= s51 . x by A29, A25, A27 ; :: thesis: verum

A32: for p, q being Element of LTLB_WFF

for a, b being set ex d being set st S

proof

consider sat being ManySortedSet of LTLB_WFF such that
let p, q be Element of LTLB_WFF ; :: thesis: for a, b being set ex d being set st S_{1}[p,q,a,b,d]

let a, b be set ; :: thesis: ex d being set st S_{1}[p,q,a,b,d]

end;let a, b be set ; :: thesis: ex d being set st S

per cases
( ( a is sequence of BOOLEAN & b is sequence of BOOLEAN ) or not a is sequence of BOOLEAN or not b is sequence of BOOLEAN )
;

end;

suppose
( a is sequence of BOOLEAN & b is sequence of BOOLEAN )
; :: thesis: ex d being set st S_{1}[p,q,a,b,d]

then reconsider a1 = a, b1 = b as sequence of BOOLEAN ;

deffunc H_{2}( Element of NAT ) -> Element of BOOLEAN = 'not' ((a1 . $1) '&' ('not' (b1 . $1)));

consider d being sequence of BOOLEAN such that

A33: for n being Element of NAT holds d . n = H_{2}(n)
from FUNCT_2:sch 4();

for n being Element of NAT holds d . n = (a1 . n) => (b1 . n) by A33;

hence ex d being set st S_{1}[p,q,a,b,d]
; :: thesis: verum

end;deffunc H

consider d being sequence of BOOLEAN such that

A33: for n being Element of NAT holds d . n = H

for n being Element of NAT holds d . n = (a1 . n) => (b1 . n) by A33;

hence ex d being set st S

suppose
( not a is sequence of BOOLEAN or not b is sequence of BOOLEAN )
; :: thesis: ex d being set st S_{1}[p,q,a,b,d]

end;

end;

A34: ( sat . TFALSUM = NAT --> FALSE & ( for n being Element of NAT holds sat . (prop n) = H

( S

A35: now :: thesis: for x being object st x in LTLB_WFF holds

sat . x in Funcs (NAT,BOOLEAN)_{1} in Funcs (NAT,BOOLEAN) )

assume x in LTLB_WFF ; :: thesis: sat . b_{1} in Funcs (NAT,BOOLEAN)

then reconsider x1 = x as Element of LTLB_WFF ;

end;

dom sat = LTLB_WFF
by PARTFUN1:def 2;sat . x in Funcs (NAT,BOOLEAN)

A36: now :: thesis: for A, B being Element of LTLB_WFF holds sat . (A => B) in Funcs (NAT,BOOLEAN)

let A, B be Element of LTLB_WFF ; :: thesis: sat . (b_{1} => b_{2}) in Funcs (NAT,BOOLEAN)

A37: S_{1}[A,B,sat . A,sat . B,sat . (A => B)]
by A34;

end;A37: S

per cases
( ( sat . A is sequence of BOOLEAN & sat . B is sequence of BOOLEAN ) or not sat . A is sequence of BOOLEAN or not sat . B is sequence of BOOLEAN )
;

end;

suppose
( sat . A is sequence of BOOLEAN & sat . B is sequence of BOOLEAN )
; :: thesis: sat . (b_{1} => b_{2}) in Funcs (NAT,BOOLEAN)

then consider s3, s4, s5 being sequence of BOOLEAN such that

s3 = sat . A and

s4 = sat . B and

A38: s5 = sat . (A => B) and

for n being Element of NAT holds s5 . n = (s3 . n) => (s4 . n) by A34;

thus sat . (A => B) in Funcs (NAT,BOOLEAN) by A38, FUNCT_2:8; :: thesis: verum

end;s3 = sat . A and

s4 = sat . B and

A38: s5 = sat . (A => B) and

for n being Element of NAT holds s5 . n = (s3 . n) => (s4 . n) by A34;

thus sat . (A => B) in Funcs (NAT,BOOLEAN) by A38, FUNCT_2:8; :: thesis: verum

A39: now :: thesis: for A, B being Element of LTLB_WFF holds sat . (A 'U' B) in Funcs (NAT,BOOLEAN)

let x be object ; :: thesis: ( x in LTLB_WFF implies sat . blet A, B be Element of LTLB_WFF ; :: thesis: sat . (b_{1} 'U' b_{2}) in Funcs (NAT,BOOLEAN)

A40: S_{2}[A,B,sat . A,sat . B,sat . (A 'U' B)]
by A34;

end;A40: S

per cases
( ( sat . A is sequence of BOOLEAN & sat . B is sequence of BOOLEAN ) or not sat . A is sequence of BOOLEAN or not sat . B is sequence of BOOLEAN )
;

end;

suppose
( sat . A is sequence of BOOLEAN & sat . B is sequence of BOOLEAN )
; :: thesis: sat . (b_{1} 'U' b_{2}) in Funcs (NAT,BOOLEAN)

then consider s3, s4, s5 being sequence of BOOLEAN such that

s3 = sat . A and

s4 = sat . B and

A41: s5 = sat . (A 'U' B) and

for n being Element of NAT holds

( s5 . n = 1 iff ex i being Element of NAT st

( 0 < i & s4 . (n + i) = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

s3 . (n + j) = 1 ) ) ) by A34;

thus sat . (A 'U' B) in Funcs (NAT,BOOLEAN) by A41, FUNCT_2:8; :: thesis: verum

end;s3 = sat . A and

s4 = sat . B and

A41: s5 = sat . (A 'U' B) and

for n being Element of NAT holds

( s5 . n = 1 iff ex i being Element of NAT st

( 0 < i & s4 . (n + i) = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

s3 . (n + j) = 1 ) ) ) by A34;

thus sat . (A 'U' B) in Funcs (NAT,BOOLEAN) by A41, FUNCT_2:8; :: thesis: verum

assume x in LTLB_WFF ; :: thesis: sat . b

then reconsider x1 = x as Element of LTLB_WFF ;

A42: now :: thesis: for n being Element of NAT holds sat . (prop n) in Funcs (NAT,BOOLEAN)

let n be Element of NAT ; :: thesis: sat . (prop n) in Funcs (NAT,BOOLEAN)

sat . (prop n) = f1 . n by A34;

hence sat . (prop n) in Funcs (NAT,BOOLEAN) ; :: thesis: verum

end;sat . (prop n) = f1 . n by A34;

hence sat . (prop n) in Funcs (NAT,BOOLEAN) ; :: thesis: verum

per cases
( x1 = TFALSUM or ex n being Element of NAT st x1 = prop n or ex p, q being Element of LTLB_WFF st x1 = p 'U' q or ex p, q being Element of LTLB_WFF st x1 = p => q )
by Th4;

end;

suppose
ex n being Element of NAT st x1 = prop n
; :: thesis: sat . b_{1} in Funcs (NAT,BOOLEAN)

end;

end;

then reconsider sat = sat as Function of LTLB_WFF,(Funcs (NAT,BOOLEAN)) by A35, FUNCT_2:3;

deffunc H

consider sat2 being Function of [:NAT,LTLB_WFF:],BOOLEAN such that

A43: for n being Element of NAT

for A being Element of LTLB_WFF holds sat2 . (n,A) = H

A44: now :: thesis: for A being Element of LTLB_WFF

for n being Element of NAT holds sat2 . [n,A] = (sat . A) . n

for n being Element of NAT holds sat2 . [n,A] = (sat . A) . n

let A be Element of LTLB_WFF ; :: thesis: for n being Element of NAT holds sat2 . [n,A] = (sat . A) . n

let n be Element of NAT ; :: thesis: sat2 . [n,A] = (sat . A) . n

thus sat2 . [n,A] = sat2 . (n,A) by BINOP_1:def 1

.= (sat . A) . n by A43 ; :: thesis: verum

end;let n be Element of NAT ; :: thesis: sat2 . [n,A] = (sat . A) . n

thus sat2 . [n,A] = sat2 . (n,A) by BINOP_1:def 1

.= (sat . A) . n by A43 ; :: thesis: verum

A45: now :: thesis: for k, n being Element of NAT holds

( sat2 . [n,(prop k)] = 1 iff prop k in M . n )

( sat2 . [n,(prop k)] = 1 iff prop k in M . n )

let k, n be Element of NAT ; :: thesis: ( sat2 . [n,(prop k)] = 1 iff prop k in M . n )

sat2 . [n,(prop k)] = (sat . (prop k)) . n by A44

.= (f1 . k) . n by A34 ;

hence ( sat2 . [n,(prop k)] = 1 iff prop k in M . n ) by A19; :: thesis: verum

end;sat2 . [n,(prop k)] = (sat . (prop k)) . n by A44

.= (f1 . k) . n by A34 ;

hence ( sat2 . [n,(prop k)] = 1 iff prop k in M . n ) by A19; :: thesis: verum

A46: now :: thesis: for p, q being Element of LTLB_WFF

for n being Element of NAT holds

( sat2 . [n,(p => q)] = (sat2 . [n,p]) => (sat2 . [n,q]) & ( sat2 . [n,(p 'U' q)] = 1 implies ex i being Element of NAT st

( 0 < i & sat2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

sat2 . [(n + j),p] = 1 ) ) ) & ( ex i being Element of NAT st

( 0 < i & sat2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

sat2 . [(n + j),p] = 1 ) ) implies sat2 . [n,(p 'U' q)] = 1 ) )

take
sat2
; :: thesis: for n being Element of NAT holds for n being Element of NAT holds

( sat2 . [n,(p => q)] = (sat2 . [n,p]) => (sat2 . [n,q]) & ( sat2 . [n,(p 'U' q)] = 1 implies ex i being Element of NAT st

( 0 < i & sat2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

sat2 . [(n + j),p] = 1 ) ) ) & ( ex i being Element of NAT st

( 0 < i & sat2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

sat2 . [(n + j),p] = 1 ) ) implies sat2 . [n,(p 'U' q)] = 1 ) )

let p, q be Element of LTLB_WFF ; :: thesis: for n being Element of NAT holds

( sat2 . [n,(p => q)] = (sat2 . [n,p]) => (sat2 . [n,q]) & ( sat2 . [n,(p 'U' q)] = 1 implies ex i being Element of NAT st

( 0 < i & sat2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

sat2 . [(n + j),p] = 1 ) ) ) & ( ex i being Element of NAT st

( 0 < i & sat2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

sat2 . [(n + j),p] = 1 ) ) implies sat2 . [n,(p 'U' q)] = 1 ) )

let n be Element of NAT ; :: thesis: ( sat2 . [n,(p => q)] = (sat2 . [n,p]) => (sat2 . [n,q]) & ( sat2 . [n,(p 'U' q)] = 1 implies ex i being Element of NAT st

( 0 < i & sat2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

sat2 . [(n + j),p] = 1 ) ) ) & ( ex i being Element of NAT st

( 0 < i & sat2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

sat2 . [(n + j),p] = 1 ) ) implies sat2 . [n,(p 'U' q)] = 1 ) )

reconsider satp = sat . p, satq = sat . q as sequence of BOOLEAN by FUNCT_2:66;

consider s31, s41, s51 being sequence of BOOLEAN such that

A47: s31 = satp and

A48: s41 = satq and

A49: s51 = sat . (p 'U' q) and

A50: for n being Element of NAT holds

( s51 . n = 1 iff ex i being Element of NAT st

( 0 < i & s41 . (n + i) = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

s31 . (n + j) = 1 ) ) ) by A34;

consider s3, s4, s5 being sequence of BOOLEAN such that

A51: s3 = satp and

A52: s4 = satq and

A53: ( s5 = sat . (p => q) & ( for n being Element of NAT holds s5 . n = (s3 . n) => (s4 . n) ) ) by A34;

thus sat2 . [n,(p => q)] = (sat . (p => q)) . n by A44

.= ((sat . p) . n) => (s4 . n) by A51, A53

.= (sat2 . [n,p]) => ((sat . q) . n) by A44, A52

.= (sat2 . [n,p]) => (sat2 . [n,q]) by A44 ; :: thesis: ( sat2 . [n,(p 'U' q)] = 1 iff ex i being Element of NAT st

( 0 < i & sat2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

sat2 . [(n + j),p] = 1 ) ) )

thus ( sat2 . [n,(p 'U' q)] = 1 iff ex i being Element of NAT st

( 0 < i & sat2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

sat2 . [(n + j),p] = 1 ) ) ) :: thesis: verum

end;( sat2 . [n,(p => q)] = (sat2 . [n,p]) => (sat2 . [n,q]) & ( sat2 . [n,(p 'U' q)] = 1 implies ex i being Element of NAT st

( 0 < i & sat2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

sat2 . [(n + j),p] = 1 ) ) ) & ( ex i being Element of NAT st

( 0 < i & sat2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

sat2 . [(n + j),p] = 1 ) ) implies sat2 . [n,(p 'U' q)] = 1 ) )

let n be Element of NAT ; :: thesis: ( sat2 . [n,(p => q)] = (sat2 . [n,p]) => (sat2 . [n,q]) & ( sat2 . [n,(p 'U' q)] = 1 implies ex i being Element of NAT st

( 0 < i & sat2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

sat2 . [(n + j),p] = 1 ) ) ) & ( ex i being Element of NAT st

( 0 < i & sat2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

sat2 . [(n + j),p] = 1 ) ) implies sat2 . [n,(p 'U' q)] = 1 ) )

reconsider satp = sat . p, satq = sat . q as sequence of BOOLEAN by FUNCT_2:66;

consider s31, s41, s51 being sequence of BOOLEAN such that

A47: s31 = satp and

A48: s41 = satq and

A49: s51 = sat . (p 'U' q) and

A50: for n being Element of NAT holds

( s51 . n = 1 iff ex i being Element of NAT st

( 0 < i & s41 . (n + i) = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

s31 . (n + j) = 1 ) ) ) by A34;

consider s3, s4, s5 being sequence of BOOLEAN such that

A51: s3 = satp and

A52: s4 = satq and

A53: ( s5 = sat . (p => q) & ( for n being Element of NAT holds s5 . n = (s3 . n) => (s4 . n) ) ) by A34;

thus sat2 . [n,(p => q)] = (sat . (p => q)) . n by A44

.= ((sat . p) . n) => (s4 . n) by A51, A53

.= (sat2 . [n,p]) => ((sat . q) . n) by A44, A52

.= (sat2 . [n,p]) => (sat2 . [n,q]) by A44 ; :: thesis: ( sat2 . [n,(p 'U' q)] = 1 iff ex i being Element of NAT st

( 0 < i & sat2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

sat2 . [(n + j),p] = 1 ) ) )

thus ( sat2 . [n,(p 'U' q)] = 1 iff ex i being Element of NAT st

( 0 < i & sat2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

sat2 . [(n + j),p] = 1 ) ) ) :: thesis: verum

proof

( 0 < i & sat2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

sat2 . [(n + j),p] = 1 ) ) ; :: thesis: sat2 . [n,(p 'U' q)] = 1

then consider i being Element of NAT such that

A59: 0 < i and

A60: sat2 . [(n + i),q] = 1 and

A61: for j being Element of NAT st 1 <= j & j < i holds

sat2 . [(n + j),p] = 1 ;

A62: s41 . (n + i) = 1 by A44, A48, A60;

A63: for j being Element of NAT st 1 <= j & j < i holds

s31 . (n + j) = 1

.= 1 by A50, A59, A62, A63 ; :: thesis: verum

end;

hereby :: thesis: ( ex i being Element of NAT st

( 0 < i & sat2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

sat2 . [(n + j),p] = 1 ) ) implies sat2 . [n,(p 'U' q)] = 1 )

assume
ex i being Element of NAT st ( 0 < i & sat2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

sat2 . [(n + j),p] = 1 ) ) implies sat2 . [n,(p 'U' q)] = 1 )

assume
sat2 . [n,(p 'U' q)] = 1
; :: thesis: ex i being Element of NAT st

( 0 < i & sat2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

sat2 . [(n + j),p] = 1 ) )

then s51 . n = 1 by A44, A49;

then consider i being Element of NAT such that

A54: 0 < i and

A55: s41 . (n + i) = 1 and

A56: for j being Element of NAT st 1 <= j & j < i holds

s31 . (n + j) = 1 by A50;

hence ex i being Element of NAT st

( 0 < i & sat2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

sat2 . [(n + j),p] = 1 ) ) by A54, A57; :: thesis: verum

end;( 0 < i & sat2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

sat2 . [(n + j),p] = 1 ) )

then s51 . n = 1 by A44, A49;

then consider i being Element of NAT such that

A54: 0 < i and

A55: s41 . (n + i) = 1 and

A56: for j being Element of NAT st 1 <= j & j < i holds

s31 . (n + j) = 1 by A50;

A57: now :: thesis: for j being Element of NAT st 1 <= j & j < i holds

sat2 . [(n + j),p] = 1

sat2 . [(n + i),q] = 1
by A44, A48, A55;sat2 . [(n + j),p] = 1

let j be Element of NAT ; :: thesis: ( 1 <= j & j < i implies sat2 . [(n + j),p] = 1 )

assume A58: ( 1 <= j & j < i ) ; :: thesis: sat2 . [(n + j),p] = 1

thus sat2 . [(n + j),p] = (sat . p) . (n + j) by A44

.= 1 by A47, A56, A58 ; :: thesis: verum

end;assume A58: ( 1 <= j & j < i ) ; :: thesis: sat2 . [(n + j),p] = 1

thus sat2 . [(n + j),p] = (sat . p) . (n + j) by A44

.= 1 by A47, A56, A58 ; :: thesis: verum

hence ex i being Element of NAT st

( 0 < i & sat2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

sat2 . [(n + j),p] = 1 ) ) by A54, A57; :: thesis: verum

( 0 < i & sat2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

sat2 . [(n + j),p] = 1 ) ) ; :: thesis: sat2 . [n,(p 'U' q)] = 1

then consider i being Element of NAT such that

A59: 0 < i and

A60: sat2 . [(n + i),q] = 1 and

A61: for j being Element of NAT st 1 <= j & j < i holds

sat2 . [(n + j),p] = 1 ;

A62: s41 . (n + i) = 1 by A44, A48, A60;

A63: for j being Element of NAT st 1 <= j & j < i holds

s31 . (n + j) = 1

proof

thus sat2 . [n,(p 'U' q)] =
s51 . n
by A44, A49
let j be Element of NAT ; :: thesis: ( 1 <= j & j < i implies s31 . (n + j) = 1 )

assume A64: ( 1 <= j & j < i ) ; :: thesis: s31 . (n + j) = 1

thus s31 . (n + j) = sat2 . [(n + j),p] by A44, A47

.= 1 by A61, A64 ; :: thesis: verum

end;assume A64: ( 1 <= j & j < i ) ; :: thesis: s31 . (n + j) = 1

thus s31 . (n + j) = sat2 . [(n + j),p] by A44, A47

.= 1 by A61, A64 ; :: thesis: verum

.= 1 by A50, A59, A62, A63 ; :: thesis: verum

( sat2 . [n,TFALSUM] = 0 & ( for k being Element of NAT holds

( sat2 . [n,(prop k)] = 1 iff prop k in M . n ) ) & ( for p, q being Element of LTLB_WFF holds

( sat2 . [n,(p => q)] = (sat2 . [n,p]) => (sat2 . [n,q]) & ( sat2 . [n,(p 'U' q)] = 1 implies ex i being Element of NAT st

( 0 < i & sat2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

sat2 . [(n + j),p] = 1 ) ) ) & ( ex i being Element of NAT st

( 0 < i & sat2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

sat2 . [(n + j),p] = 1 ) ) implies sat2 . [n,(p 'U' q)] = 1 ) ) ) )

now :: thesis: for n being Element of NAT holds sat2 . [n,TFALSUM] = 0

hence
for n being Element of NAT holds let n be Element of NAT ; :: thesis: sat2 . [n,TFALSUM] = 0

thus sat2 . [n,TFALSUM] = (sat . TFALSUM) . n by A44

.= 0 by A34, FUNCOP_1:7 ; :: thesis: verum

end;thus sat2 . [n,TFALSUM] = (sat . TFALSUM) . n by A44

.= 0 by A34, FUNCOP_1:7 ; :: thesis: verum

( sat2 . [n,TFALSUM] = 0 & ( for k being Element of NAT holds

( sat2 . [n,(prop k)] = 1 iff prop k in M . n ) ) & ( for p, q being Element of LTLB_WFF holds

( sat2 . [n,(p => q)] = (sat2 . [n,p]) => (sat2 . [n,q]) & ( sat2 . [n,(p 'U' q)] = 1 implies ex i being Element of NAT st

( 0 < i & sat2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

sat2 . [(n + j),p] = 1 ) ) ) & ( ex i being Element of NAT st

( 0 < i & sat2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds

sat2 . [(n + j),p] = 1 ) ) implies sat2 . [n,(p 'U' q)] = 1 ) ) ) ) by A45, A46; :: thesis: verum