defpred S1[ Element of LTLB_WFF , Element of LTLB_WFF , set , set , set ] means ( ( $3 is Element of BOOLEAN & $4 is Element of BOOLEAN implies ex a, b, c being Element of BOOLEAN st
( a = $3 & b = $4 & c = $5 & c = a => b ) ) & ( ( not $3 is Element of BOOLEAN or not $4 is Element of BOOLEAN ) implies $5 = {} ) );
defpred S2[ Element of LTLB_WFF , Element of LTLB_WFF , set , set , set ] means $5 = f . ($1 'U' $2);
deffunc H1( Element of NAT ) -> Element of BOOLEAN = f . (prop $1);
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 BOOLEAN & y is Element of BOOLEAN ) or not x is Element of BOOLEAN or not y is Element of BOOLEAN ) ;
suppose that A2: x is Element of BOOLEAN and
A3: y is Element of BOOLEAN ; :: thesis: ex z being set st S1[A,B,x,y,z]
reconsider b = y as Element of BOOLEAN by A3;
reconsider a = x as Element of BOOLEAN by A2;
per cases ( a = 0 or a = 1 ) by XBOOLEAN:def 3;
suppose A4: a = 0 ; :: thesis: ex z being set st S1[A,B,x,y,z]
set c = TRUE ;
TRUE = a => b by A4;
hence ex z being set st S1[A,B,x,y,z] ; :: thesis: verum
end;
suppose A5: a = 1 ; :: thesis: ex z being set st S1[A,B,x,y,z]
per cases ( b = 0 or b = 1 ) by XBOOLEAN:def 3;
suppose A6: b = 0 ; :: thesis: ex z being set st S1[A,B,x,y,z]
set c = FALSE ;
FALSE = a => b by A5, A6;
hence ex z being set st S1[A,B,x,y,z] ; :: thesis: verum
end;
suppose A7: b = 1 ; :: thesis: ex z being set st S1[A,B,x,y,z]
set c = TRUE ;
TRUE = a => b by A7;
hence ex z being set st S1[A,B,x,y,z] ; :: thesis: verum
end;
end;
end;
end;
end;
suppose ( not x is Element of BOOLEAN or not y is Element of BOOLEAN ) ; :: 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;
A8: 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 ;
A9: 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 ;
A10: for A, B being Element of LTLB_WFF
for x, y being set ex z being set st S2[A,B,x,y,z] ;
consider val being ManySortedSet of LTLB_WFF such that
A11: ( val . TFALSUM = 0 & ( for n being Element of NAT holds val . (prop n) = H1(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(A10, A1, A8, A9);
A12: now :: thesis: for x being object st x in LTLB_WFF holds
val . x in BOOLEAN
A13: now :: thesis: for A, B being Element of LTLB_WFF holds val . (A => B) in BOOLEAN
let A, B be Element of LTLB_WFF ; :: thesis: val . (b1 => b2) in BOOLEAN
per cases ( ( val . A is Element of BOOLEAN & val . B is Element of BOOLEAN ) or not val . A is Element of BOOLEAN or not val . B is Element of BOOLEAN ) ;
suppose ( val . A is Element of BOOLEAN & val . B is Element of BOOLEAN ) ; :: thesis: val . (b1 => b2) in BOOLEAN
then consider a, b, c being Element of BOOLEAN such that
a = val . A and
b = val . B and
A14: c = val . (A => B) and
c = a => b by A11;
thus val . (A => B) in BOOLEAN by A14; :: thesis: verum
end;
suppose ( not val . A is Element of BOOLEAN or not val . B is Element of BOOLEAN ) ; :: thesis: val . (b1 => b2) in BOOLEAN
then val . (A => B) = FALSE by A11;
hence val . (A => B) in BOOLEAN ; :: thesis: verum
end;
end;
end;
let x be object ; :: thesis: ( x in LTLB_WFF implies val . b1 in BOOLEAN )
assume x in LTLB_WFF ; :: thesis: val . b1 in BOOLEAN
then reconsider x1 = x as Element of LTLB_WFF ;
A15: now :: thesis: for n being Element of NAT holds val . (prop n) in BOOLEAN
let n be Element of NAT ; :: thesis: val . (prop n) in BOOLEAN
val . (prop n) = f . (prop n) by A11;
hence val . (prop n) in BOOLEAN ; :: thesis: verum
end;
A16: now :: thesis: for A, B being Element of LTLB_WFF holds val . (A 'U' B) in BOOLEAN
let A, B be Element of LTLB_WFF ; :: thesis: val . (A 'U' B) in BOOLEAN
val . (A 'U' B) = f . (A 'U' B) by A11;
hence val . (A 'U' B) in BOOLEAN ; :: 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 Th4;
end;
end;
dom val = LTLB_WFF by PARTFUN1:def 2;
then reconsider val = val as Function of LTLB_WFF,BOOLEAN by A12, FUNCT_2:3;
take val ; :: thesis: for A, B being Element of LTLB_WFF
for n being Element of NAT holds
( val . TFALSUM = 0 & val . (prop n) = f . (prop n) & val . (A => B) = (val . A) => (val . B) & val . (A 'U' B) = f . (A 'U' B) )
now :: thesis: for A, B being Element of LTLB_WFF holds val . (A => B) = (val . A) => (val . B)
let A, B be Element of LTLB_WFF ; :: thesis: val . (A => B) = (val . A) => (val . B)
S1[A,B,val . A,val . B,val . (A => B)] by A11;
hence val . (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 = 0 & val . (prop n) = f . (prop n) & val . (A => B) = (val . A) => (val . B) & val . (A 'U' B) = f . (A 'U' B) ) by A11; :: thesis: verum