set FNB = Funcs (NAT,BOOLEAN);
defpred S₁[ 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₂[ 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₃[ 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₂[p,q,a,b,d]

let p, q be Element of LTLB_WFF ; :: thesis:
let a, b be set ; :: thesis:

suppose ( a is sequence of BOOLEAN & b is sequence of BOOLEAN ) ; :: thesis:

then reconsider a1 = a, b1 = b as sequence of BOOLEAN ;
defpred S₄[ 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 ) ) );

A2: now :: thesis:

let n be Element of NAT ; :: thesis:

per cases ;

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:

hence ex y being Element of BOOLEAN st S₄[n,y] ; :: thesis:

end;

suppose 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 ) ) ; :: thesis:

then S₄[n, FALSE ] ;
hence ex y being Element of BOOLEAN st S₄[n,y] ; :: thesis:

end;

consider c being sequence of BOOLEAN such that
A3: for n being Element of NAT holds S₄[n,c . n] from FUNCT_2:sch 3(A2);
thus ex d being set st S₂[p,q,a,b,d] by A3; :: thesis:

end;

suppose ( not a is sequence of BOOLEAN or not b is sequence of BOOLEAN ) ; :: thesis:

hence ex d being set st S₂[p,q,a,b,d] ; :: thesis:

end;

A4: for p, q being Element of LTLB_WFF
for a, b, c, d being set st S₂[p,q,a,b,c] & S₂[p,q,a,b,d] holds
c = d

proof

let p, q be Element of LTLB_WFF ; :: thesis:
let a, b, c, d be set ; :: thesis:
assume that
A5: S₂[p,q,a,b,c] and
A6: S₂[p,q,a,b,d] ; :: thesis:

per cases ;

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

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;

now :: thesis:

let x be object ; :: thesis:
assume x in NAT ; :: thesis:
then reconsider x1 = x as Element of NAT ;

per cases by XBOOLEAN:def 3;

suppose A14: s5 . x1 = 1 ; :: thesis:

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:

end;

suppose A15: s5 . x1 = 0 ; :: thesis:

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:

end;

hence c = d by A12, A9, FUNCT_2:12; :: thesis:

end;

suppose ( not a is sequence of BOOLEAN or not b is sequence of BOOLEAN ) ; :: thesis:

hence c = d by A5, A6; :: thesis:

end;

A16: for x being Element of NAT ex y being Element of Funcs (NAT,BOOLEAN) st S₃[x,y]

proof

let x be Element of NAT ; :: thesis:
defpred S₄[ Element of NAT , Element of BOOLEAN ] means ( $2 = 1 iff prop x in M . $1 );

A17: now :: thesis:

let x1 be Element of NAT ; :: thesis:

per cases ;

suppose prop x in M . x1 ; :: thesis:

then S₄[x1, TRUE ] ;
hence ex y1 being Element of BOOLEAN st S₄[x1,y1] ; :: thesis:

end;

suppose not prop x in M . x1 ; :: thesis:

then S₄[x1, FALSE ] ;
hence ex y1 being Element of BOOLEAN st S₄[x1,y1] ; :: thesis:

end;

consider y being sequence of BOOLEAN such that
A18: for n being Element of NAT holds S₄[n,y . n] from FUNCT_2:sch 3(A17);
reconsider y = y as Element of Funcs (NAT,BOOLEAN) by FUNCT_2:8;
S₃[x,y] by A18;
hence ex y being Element of Funcs (NAT,BOOLEAN) st S₃[x,y] ; :: thesis:

end;

consider f1 being sequence of (Funcs (NAT,BOOLEAN)) such that
A19: for k being Element of NAT holds S₃[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₁[p,q,a,b,c] & S₁[p,q,a,b,d] holds
c = d

proof

let p, q be Element of LTLB_WFF ; :: thesis:
let a, b, c, d be set ; :: thesis:
assume that
A21: S₁[p,q,a,b,c] and
A22: S₁[p,q,a,b,d] ; :: thesis:

per cases ;

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

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;

now :: thesis:

let x be object ; :: thesis:
assume x in NAT ; :: thesis:
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:

end;

hence c = d by A30, A26, FUNCT_2:12; :: thesis:

end;

suppose ( not a is sequence of BOOLEAN or not b is sequence of BOOLEAN ) ; :: thesis:

hence c = d by A21, A22; :: thesis:

end;

deffunc H₁( 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₁[p,q,a,b,d]

proof

let p, q be Element of LTLB_WFF ; :: thesis:
let a, b be set ; :: thesis:

per cases ;

suppose ( a is sequence of BOOLEAN & b is sequence of BOOLEAN ) ; :: thesis:

then reconsider a1 = a, b1 = b as sequence of BOOLEAN ;
deffunc H₂( 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₂(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₁[p,q,a,b,d] ; :: thesis:

end;

suppose ( not a is sequence of BOOLEAN or not b is sequence of BOOLEAN ) ; :: thesis:

hence ex d being set st S₁[p,q,a,b,d] ; :: thesis:

end;

consider sat being ManySortedSet of LTLB_WFF such that
A34: ( sat . TFALSUM = NAT --> FALSE & ( for n being Element of NAT holds sat . (prop n) = H₁(n) ) & ( for p, q being Element of LTLB_WFF holds
( S₂[p,q,sat . p,sat . q,sat . (p 'U' q)] & S₁[p,q,sat . p,sat . q,sat . (p => q)] ) ) ) from HILBERT2:sch 3(A1, A32, A4, A20);

A35: now :: thesis:

A36: now :: thesis:

let A, B be Element of LTLB_WFF ; :: thesis:
A37: S₁[A,B,sat . A,sat . B,sat . (A => B)] by A34;

per cases ;

suppose ( sat . A is sequence of BOOLEAN & sat . B is sequence of BOOLEAN ) ; :: thesis:

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:

end;

suppose ( not sat . A is sequence of BOOLEAN or not sat . B is sequence of BOOLEAN ) ; :: thesis:

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

end;

A39: now :: thesis:

let A, B be Element of LTLB_WFF ; :: thesis:
A40: S₂[A,B,sat . A,sat . B,sat . (A 'U' B)] by A34;

per cases ;

suppose ( sat . A is sequence of BOOLEAN & sat . B is sequence of BOOLEAN ) ; :: thesis:

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:

end;

suppose ( not sat . A is sequence of BOOLEAN or not sat . B is sequence of BOOLEAN ) ; :: thesis:

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

end;

let x be object ; :: thesis:
assume x in LTLB_WFF ; :: thesis:
then reconsider x1 = x as Element of LTLB_WFF ;

A42: now :: thesis:

let n be Element of NAT ; :: thesis:
sat . (prop n) = f1 . n by A34;
hence sat . (prop n) in Funcs (NAT,BOOLEAN) ; :: thesis:

end;

per cases by Th4;

suppose x1 = TFALSUM ; :: thesis:

hence sat . x in Funcs (NAT,BOOLEAN) by A34, FUNCT_2:8; :: thesis:

end;

suppose ex n being Element of NAT st x1 = prop n ; :: thesis:

hence sat . x in Funcs (NAT,BOOLEAN) by A42; :: thesis:

end;

suppose ex p, q being Element of LTLB_WFF st x1 = p 'U' q ; :: thesis:

hence sat . x in Funcs (NAT,BOOLEAN) by A39; :: thesis:

end;

suppose ex p, q being Element of LTLB_WFF st x1 = p => q ; :: thesis:

hence sat . x in Funcs (NAT,BOOLEAN) by A36; :: thesis:

end;

dom sat = LTLB_WFF by PARTFUN1:def 2;
then reconsider sat = sat as Function of LTLB_WFF,(Funcs (NAT,BOOLEAN)) by A35, FUNCT_2:3;
deffunc H₂( 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₂(n,A) from BINOP_1:sch 4();

A44: now :: thesis:

let A be Element of LTLB_WFF ; :: thesis:
let n be Element of NAT ; :: thesis:
thus sat2 . [n,A] = sat2 . (n,A) by BINOP_1:def 1
.= (sat . A) . n by A43 ; :: thesis:

end;

A45: now :: thesis:

let k, n be Element of NAT ; :: thesis:
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:

end;

A46: now :: thesis:

let p, q be Element of LTLB_WFF ; :: thesis:
let n be Element of NAT ; :: thesis:
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:
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:

proof

hereby :: thesis:

assume sat2 . [n,(p 'U' q)] = 1 ; :: thesis:
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:

let j be Element of NAT ; :: thesis:
assume A58: ( 1 <= j & j < i ) ; :: thesis:
thus sat2 . [(n + j),p] = (sat . p) . (n + j) by A44
.= 1 by A47, A56, A58 ; :: thesis:

end;

sat2 . [(n + i),q] = 1 by A44, A48, A55;
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:

end;

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 ) ) ; :: thesis:
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

let j be Element of NAT ; :: thesis:
assume A64: ( 1 <= j & j < i ) ; :: thesis:
thus s31 . (n + j) = sat2 . [(n + j),p] by A44, A47
.= 1 by A61, A64 ; :: thesis:

end;

thus sat2 . [n,(p 'U' q)] = s51 . n by A44, A49
.= 1 by A50, A59, A62, A63 ; :: thesis:

end;

take sat2 ; :: thesis:

now :: thesis:

let n be Element of NAT ; :: thesis:
thus sat2 . [n,TFALSUM] = (sat . TFALSUM) . n by A44
.= 0 by A34, FUNCOP_1:7 ; :: thesis:

end;

hence for n being Element of NAT holds
( 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: