set bltl = bool LTLB_WFF;

defpred S_{1}[ Element of LTLB_WFF , Element of LTLB_WFF , set , set , set ] means $5 = {($1 'U' $2)};

deffunc H_{3}( Element of NAT ) -> Element of bool LTLB_WFF = {(prop $1)};

defpred S_{2}[ Element of LTLB_WFF , Element of LTLB_WFF , set , set , set ] means ( ( $3 is Element of bool LTLB_WFF & $4 is Element of bool LTLB_WFF implies ex a, b, c being Element of bool LTLB_WFF st

( a = $3 & b = $4 & c = $5 & c = ({($1 => $2)} \/ $3) \/ $4 ) ) & ( ( not $3 is Element of bool LTLB_WFF or not $4 is Element of bool LTLB_WFF ) implies $5 = {} LTLB_WFF ) );

A1: for A, B being Element of LTLB_WFF

for x, y being set ex z being set st S_{2}[A,B,x,y,z]

for x, y being set ex z being set st S_{1}[A,B,x,y,z]
;

A6: 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 ;

A7: for p, q being Element of LTLB_WFF

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 ;

consider val being ManySortedSet of LTLB_WFF such that

A8: ( val . TFALSUM = {TFALSUM} & ( for n being Element of NAT holds val . (prop n) = H_{3}(n) ) & ( for p, q being Element of LTLB_WFF holds

( S_{1}[p,q,val . p,val . q,val . (p 'U' q)] & S_{2}[p,q,val . p,val . q,val . (p => q)] ) ) )
from HILBERT2:sch 3(A5, A1, A6, A7);

then reconsider val = val as Function of LTLB_WFF,(bool LTLB_WFF) by A9, FUNCT_2:3;

take val ; :: thesis: for A, B being Element of LTLB_WFF

for n being Element of NAT holds

( val . TFALSUM = {TFALSUM} & val . (prop n) = {(prop n)} & val . (A => B) = ({(A => B)} \/ (val . A)) \/ (val . B) & val . (A 'U' B) = {(A 'U' B)} )

for n being Element of NAT holds

( val . TFALSUM = {TFALSUM} & val . (prop n) = {(prop n)} & val . (A => B) = ({(A => B)} \/ (val . A)) \/ (val . B) & val . (A 'U' B) = {(A 'U' B)} ) by A8; :: thesis: verum

defpred S

deffunc H

defpred S

( a = $3 & b = $4 & c = $5 & c = ({($1 => $2)} \/ $3) \/ $4 ) ) & ( ( not $3 is Element of bool LTLB_WFF or not $4 is Element of bool LTLB_WFF ) implies $5 = {} LTLB_WFF ) );

A1: for A, B being Element of LTLB_WFF

for x, y being set ex z being set st S

proof

A5:
for A, B being Element of LTLB_WFF
let A, B be Element of LTLB_WFF ; :: thesis: for x, y being set ex z being set st S_{2}[A,B,x,y,z]

let x, y be set ; :: thesis: ex z being set st S_{2}[A,B,x,y,z]

end;let x, y be set ; :: thesis: ex z being set st S

per cases
( ( x is Element of bool LTLB_WFF & y is Element of bool LTLB_WFF ) or not x is Element of bool LTLB_WFF or not y is Element of bool LTLB_WFF )
;

end;

suppose that A2:
x is Element of bool LTLB_WFF
and

A3: y is Element of bool LTLB_WFF ; :: thesis: ex z being set st S_{2}[A,B,x,y,z]

A3: y is Element of bool LTLB_WFF ; :: thesis: ex z being set st S

reconsider b = y as Element of bool LTLB_WFF by A3;

reconsider a = x as Element of bool LTLB_WFF by A2;

consider z being set such that

A4: z = ({(A => B)} \/ a) \/ b ;

take z ; :: thesis: S_{2}[A,B,x,y,z]

thus S_{2}[A,B,x,y,z]
by A4; :: thesis: verum

end;reconsider a = x as Element of bool LTLB_WFF by A2;

consider z being set such that

A4: z = ({(A => B)} \/ a) \/ b ;

take z ; :: thesis: S

thus S

suppose
( not x is Element of bool LTLB_WFF or not y is Element of bool LTLB_WFF )
; :: thesis: ex z being set st S_{2}[A,B,x,y,z]

end;

end;

for x, y being set ex z being set st S

A6: for p, q being Element of LTLB_WFF

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

c = d ;

A7: for p, q being Element of LTLB_WFF

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

c = d ;

consider val being ManySortedSet of LTLB_WFF such that

A8: ( val . TFALSUM = {TFALSUM} & ( for n being Element of NAT holds val . (prop n) = H

( S

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

val . x in bool LTLB_WFF_{1} in bool LTLB_WFF )

assume x in LTLB_WFF ; :: thesis: val . b_{1} in bool LTLB_WFF

then reconsider x1 = x as Element of LTLB_WFF ;

end;

dom val = LTLB_WFF
by PARTFUN1:def 2;val . x in bool LTLB_WFF

A10: now :: thesis: for A, B being Element of LTLB_WFF holds val . (A => B) in bool LTLB_WFF

let x be object ; :: thesis: ( x in LTLB_WFF implies val . blet A, B be Element of LTLB_WFF ; :: thesis: val . (b_{1} => b_{2}) in bool LTLB_WFF

A11: S_{2}[A,B,val . A,val . B,val . (A => B)]
by A8;

end;A11: S

per cases
( ( val . A is Element of bool LTLB_WFF & val . B is Element of bool LTLB_WFF ) or not val . A is Element of bool LTLB_WFF or not val . B is Element of bool LTLB_WFF )
;

end;

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

then reconsider x1 = x as Element of LTLB_WFF ;

A12: now :: thesis: for n being Element of NAT holds val . (prop n) in bool LTLB_WFF

let n be Element of NAT ; :: thesis: val . (prop n) in bool LTLB_WFF

val . (prop n) = {(prop n)} by A8;

hence val . (prop n) in bool LTLB_WFF ; :: thesis: verum

end;val . (prop n) = {(prop n)} by A8;

hence val . (prop n) in bool LTLB_WFF ; :: thesis: verum

A13: now :: thesis: for A, B being Element of LTLB_WFF holds val . (A 'U' B) in bool LTLB_WFF

let A, B be Element of LTLB_WFF ; :: thesis: val . (A 'U' B) in bool LTLB_WFF

val . (A 'U' B) = {(A 'U' B)} by A8;

hence val . (A 'U' B) in bool LTLB_WFF ; :: thesis: verum

end;val . (A 'U' B) = {(A 'U' B)} by A8;

hence val . (A 'U' B) in bool LTLB_WFF ; :: 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 LTLAXIO1:4;

end;

then reconsider val = val as Function of LTLB_WFF,(bool LTLB_WFF) by A9, FUNCT_2:3;

take val ; :: thesis: for A, B being Element of LTLB_WFF

for n being Element of NAT holds

( val . TFALSUM = {TFALSUM} & val . (prop n) = {(prop n)} & val . (A => B) = ({(A => B)} \/ (val . A)) \/ (val . B) & val . (A 'U' B) = {(A 'U' B)} )

now :: thesis: for A, B being Element of LTLB_WFF holds val . (A => B) = ({(A => B)} \/ (val . A)) \/ (val . B)

hence
for A, B being Element of LTLB_WFF let A, B be Element of LTLB_WFF ; :: thesis: val . (A => B) = ({(A => B)} \/ (val . A)) \/ (val . B)

S_{2}[A,B,val . A,val . B,val . (A => B)]
by A8;

hence val . (A => B) = ({(A => B)} \/ (val . A)) \/ (val . B) ; :: thesis: verum

end;S

hence val . (A => B) = ({(A => B)} \/ (val . A)) \/ (val . B) ; :: thesis: verum

for n being Element of NAT holds

( val . TFALSUM = {TFALSUM} & val . (prop n) = {(prop n)} & val . (A => B) = ({(A => B)} \/ (val . A)) \/ (val . B) & val . (A 'U' B) = {(A 'U' B)} ) by A8; :: thesis: verum