set bltl = bool LTLB_WFF;
defpred S1[ Element of LTLB_WFF , Element of LTLB_WFF , set , set , set ] means $5 = {($1 'U' $2)};
deffunc H3( Element of NAT ) -> Element of bool LTLB_WFF = {(prop $1)};
defpred S2[ 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 S2[A,B,x,y,z]
proof
let A,
B be
Element of
LTLB_WFF ;
for x, y being set ex z being set st S2[A,B,x,y,z]let x,
y be
set ;
ex z being set st S2[A,B,x,y,z]
end;
A5:
for A, B being Element of LTLB_WFF
for x, y being set ex z being set st S1[A,B,x,y,z]
;
A6:
for p, q being Element of LTLB_WFF
for a, b, c, d being set st S1[p,q,a,b,c] & S1[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 S2[p,q,a,b,c] & S2[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) = H3(n) ) & ( for p, q being Element of LTLB_WFF holds
( S1[p,q,val . p,val . q,val . (p 'U' q)] & S2[p,q,val . p,val . q,val . (p => q)] ) ) )
from HILBERT2:sch 3(A5, A1, A6, A7);
dom val = LTLB_WFF
by PARTFUN1:def 2;
then reconsider val = val as Function of LTLB_WFF,(bool LTLB_WFF) by A9, FUNCT_2:3;
take
val
; 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)} )
hence
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)} )
by A8; verum