set bltl = bool LTLB_WFF;
deffunc H3( Element of NAT ) -> Element of bool LTLB_WFF = {(prop $1)};
defpred S1[ 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 ) );
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 = ((tau1 . (untn ($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 S1[A,B,x,y,z]
proof
let A, B be Element of LTLB_WFF ; :: thesis: for x, y being set ex z being set st S1[A,B,x,y,z]
let x, y be set ; :: thesis: ex z being set st S1[A,B,x,y,z]
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 ) ;
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 S1[A,B,x,y,z]
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: S1[A,B,x,y,z]
thus S1[A,B,x,y,z] by A4; :: thesis: verum
end;
suppose ( not x is Element of bool LTLB_WFF or not y is Element of bool LTLB_WFF ) ; :: thesis: ex z being set st S1[A,B,x,y,z]
hence ex z being set st S1[A,B,x,y,z] ; :: thesis: verum
end;
end;
end;
A5: 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 ; :: thesis: for x, y being set ex z being set st S2[A,B,x,y,z]
let x, y be set ; :: thesis: ex z being set st S2[A,B,x,y,z]
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 ) ;
suppose that A6: x is Element of bool LTLB_WFF and
A7: y is Element of bool LTLB_WFF ; :: thesis: ex z being set st S2[A,B,x,y,z]
reconsider b = y as Element of bool LTLB_WFF by A7;
reconsider a = x as Element of bool LTLB_WFF by A6;
consider z being set such that
A8: z = ((tau1 . (untn (A,B))) \/ a) \/ b ;
take z ; :: thesis: S2[A,B,x,y,z]
thus S2[A,B,x,y,z] by A8; :: thesis: verum
end;
suppose ( not x is Element of bool LTLB_WFF or not y is Element of bool LTLB_WFF ) ; :: thesis: ex z being set st S2[A,B,x,y,z]
hence ex z being set st S2[A,B,x,y,z] ; :: thesis: verum
end;
end;
end;
A9: 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 ;
A10: 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 ;
consider val being ManySortedSet of LTLB_WFF such that
A11: ( val . TFALSUM = {TFALSUM} & ( for n being Element of NAT holds val . (prop n) = H3(n) ) & ( for p, q being Element of LTLB_WFF holds
( S2[p,q,val . p,val . q,val . (p 'U' q)] & S1[p,q,val . p,val . q,val . (p => q)] ) ) ) from HILBERT2:sch 3(A5, A1, A9, A10);
A12: now :: thesis: for x being object st x in LTLB_WFF holds
val . x in bool LTLB_WFF
A13: now :: thesis: for A, B being Element of LTLB_WFF holds val . (A => B) in bool LTLB_WFF
let A, B be Element of LTLB_WFF ; :: thesis: val . (A => B) in bool LTLB_WFF
S1[A,B,val . A,val . B,val . (A => B)] by A11;
hence val . (A => B) in bool LTLB_WFF ; :: thesis: verum
end;
A14: 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
S2[A,B,val . A,val . B,val . (A 'U' B)] by A11;
hence val . (A 'U' B) in bool LTLB_WFF ; :: thesis: verum
end;
let x be object ; :: thesis: ( x in LTLB_WFF implies val . b1 in bool LTLB_WFF )
assume x in LTLB_WFF ; :: thesis: val . b1 in bool LTLB_WFF
then reconsider x1 = x as Element of LTLB_WFF ;
A15: 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 A11;
hence val . (prop n) in bool LTLB_WFF ; :: thesis: verum
end;
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;
end;
dom val = LTLB_WFF by PARTFUN1:def 2;
then reconsider val = val as Function of LTLB_WFF,(bool LTLB_WFF) by A12, FUNCT_2:3;
A16: now :: thesis: for A, B being Element of LTLB_WFF holds val . (A => B) = ({(A => B)} \/ (val . A)) \/ (val . B)
let A, B be Element of LTLB_WFF ; :: thesis: val . (A => B) = ({(A => B)} \/ (val . A)) \/ (val . B)
S1[A,B,val . A,val . B,val . (A => B)] by A11;
hence val . (A => B) = ({(A => B)} \/ (val . A)) \/ (val . B) ; :: thesis: verum
end;
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) = ((tau1 . (untn (A,B))) \/ (val . A)) \/ (val . B) )
now :: thesis: for A, B being Element of LTLB_WFF holds val . (A 'U' B) = ((tau1 . (untn (A,B))) \/ (val . A)) \/ (val . B)
let A, B be Element of LTLB_WFF ; :: thesis: val . (A 'U' B) = ((tau1 . (untn (A,B))) \/ (val . A)) \/ (val . B)
S2[A,B,val . A,val . B,val . (A 'U' B)] by A11;
hence val . (A 'U' B) = ((tau1 . (untn (A,B))) \/ (val . A)) \/ (val . B) ; :: thesis: verum
end;
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) = ((tau1 . (untn (A,B))) \/ (val . A)) \/ (val . B) ) by A16, A11; :: thesis: verum