:: LTLAXIO1 semantic presentation
begin
Lm1: for X being set
for f being FinSequence of X
for i being Nat st 1 <= i & i <= len f holds
f . i = f /. i
proof
let X be set ; ::_thesis: for f being FinSequence of X
for i being Nat st 1 <= i & i <= len f holds
f . i = f /. i
let f be FinSequence of X; ::_thesis: for i being Nat st 1 <= i & i <= len f holds
f . i = f /. i
let i be Nat; ::_thesis: ( 1 <= i & i <= len f implies f . i = f /. i )
assume ( 1 <= i & i <= len f ) ; ::_thesis: f . i = f /. i
then i in Seg (len f) by FINSEQ_1:1;
then i in dom f by FINSEQ_1:def_3;
hence f . i = f /. i by PARTFUN1:def_6; ::_thesis: verum
end;
theorem Th1: :: LTLAXIO1:1
for a, b, c being boolean number holds (a => (b '&' c)) => (a => b) = 1
proof
let a, b, c be boolean number ; ::_thesis: (a => (b '&' c)) => (a => b) = 1
A1: ( b = 0 or b = 1 ) by XBOOLEAN:def_3;
( a = 0 or a = 1 ) by XBOOLEAN:def_3;
hence (a => (b '&' c)) => (a => b) = 1 by A1; ::_thesis: verum
end;
theorem Th2: :: LTLAXIO1:2
for a, b, c being boolean number holds (a => (b => c)) => ((a '&' b) => c) = 1
proof
let a, b, c be boolean number ; ::_thesis: (a => (b => c)) => ((a '&' b) => c) = 1
A1: ( a = 0 or a = 1 ) by XBOOLEAN:def_3;
A2: ( b = 0 or b = 1 ) by XBOOLEAN:def_3;
( c = 0 or c = 1 ) by XBOOLEAN:def_3;
hence (a => (b => c)) => ((a '&' b) => c) = 1 by A1, A2; ::_thesis: verum
end;
theorem Th3: :: LTLAXIO1:3
for a, b, c being boolean number holds ((a '&' b) => c) => (a => (b => c)) = 1
proof
let a, b, c be boolean number ; ::_thesis: ((a '&' b) => c) => (a => (b => c)) = 1
A1: ( a = 0 or a = 1 ) by XBOOLEAN:def_3;
A2: ( b = 0 or b = 1 ) by XBOOLEAN:def_3;
( c = 0 or c = 1 ) by XBOOLEAN:def_3;
hence ((a '&' b) => c) => (a => (b => c)) = 1 by A1, A2; ::_thesis: verum
end;
begin
notation
synonym LTLB_WFF for HP-WFF ;
end;
notation
synonym TFALSUM for VERUM ;
end;
notation
let p, q be Element of LTLB_WFF ;
synonym p 'Us' q for p '&' q;
end;
theorem Th4: :: LTLAXIO1:4
for A being Element of LTLB_WFF holds
( A = TFALSUM or ex n being Element of NAT st
( A = prop n or ex p, q being Element of LTLB_WFF st
( A = p => q or ex p, q being Element of LTLB_WFF st A = p 'Us' q ) ) )
proof
let A be Element of LTLB_WFF ; ::_thesis: ( A = TFALSUM or ex n being Element of NAT st
( A = prop n or ex p, q being Element of LTLB_WFF st
( A = p => q or ex p, q being Element of LTLB_WFF st A = p 'Us' q ) ) )
( A = VERUM or A is simple or A is conjunctive or A is conditional ) by HILBERT2:9;
hence ( A = TFALSUM or ex n being Element of NAT st
( A = prop n or ex p, q being Element of LTLB_WFF st
( A = p => q or ex p, q being Element of LTLB_WFF st A = p 'Us' q ) ) ) by HILBERT2:def_6, HILBERT2:def_7, HILBERT2:def_8; ::_thesis: verum
end;
definition
let p be Element of LTLB_WFF ;
func 'not' p -> Element of LTLB_WFF equals :: LTLAXIO1:def 1
p => TFALSUM;
correctness
coherence
p => TFALSUM is Element of LTLB_WFF ;
;
func 'X' p -> Element of LTLB_WFF equals :: LTLAXIO1:def 2
TFALSUM 'Us' p;
correctness
coherence
TFALSUM 'Us' p is Element of LTLB_WFF ;
;
end;
:: deftheorem defines 'not' LTLAXIO1:def_1_:_
for p being Element of LTLB_WFF holds 'not' p = p => TFALSUM;
:: deftheorem defines 'X' LTLAXIO1:def_2_:_
for p being Element of LTLB_WFF holds 'X' p = TFALSUM 'Us' p;
definition
func TVERUM -> Element of LTLB_WFF equals :: LTLAXIO1:def 3
'not' TFALSUM;
correctness
coherence
'not' TFALSUM is Element of LTLB_WFF ;
;
end;
:: deftheorem defines TVERUM LTLAXIO1:def_3_:_
TVERUM = 'not' TFALSUM;
definition
let p, q be Element of LTLB_WFF ;
funcp '&&' q -> Element of LTLB_WFF equals :: LTLAXIO1:def 4
(p => (q => TFALSUM)) => TFALSUM;
correctness
coherence
(p => (q => TFALSUM)) => TFALSUM is Element of LTLB_WFF ;
;
end;
:: deftheorem defines '&&' LTLAXIO1:def_4_:_
for p, q being Element of LTLB_WFF holds p '&&' q = (p => (q => TFALSUM)) => TFALSUM;
definition
let p, q be Element of LTLB_WFF ;
funcp 'or' q -> Element of LTLB_WFF equals :: LTLAXIO1:def 5
'not' (('not' p) '&&' ('not' q));
correctness
coherence
'not' (('not' p) '&&' ('not' q)) is Element of LTLB_WFF ;
;
end;
:: deftheorem defines 'or' LTLAXIO1:def_5_:_
for p, q being Element of LTLB_WFF holds p 'or' q = 'not' (('not' p) '&&' ('not' q));
definition
let p be Element of LTLB_WFF ;
func 'G' p -> Element of LTLB_WFF equals :: LTLAXIO1:def 6
'not' (('not' p) 'or' (TVERUM '&&' (TVERUM 'Us' ('not' p))));
correctness
coherence
'not' (('not' p) 'or' (TVERUM '&&' (TVERUM 'Us' ('not' p)))) is Element of LTLB_WFF ;
;
end;
:: deftheorem defines 'G' LTLAXIO1:def_6_:_
for p being Element of LTLB_WFF holds 'G' p = 'not' (('not' p) 'or' (TVERUM '&&' (TVERUM 'Us' ('not' p))));
definition
let p be Element of LTLB_WFF ;
func 'F' p -> Element of LTLB_WFF equals :: LTLAXIO1:def 7
'not' ('G' ('not' p));
correctness
coherence
'not' ('G' ('not' p)) is Element of LTLB_WFF ;
;
end;
:: deftheorem defines 'F' LTLAXIO1:def_7_:_
for p being Element of LTLB_WFF holds 'F' p = 'not' ('G' ('not' p));
definition
let p, q be Element of LTLB_WFF ;
funcp 'U' q -> Element of LTLB_WFF equals :: LTLAXIO1:def 8
q 'or' (p '&&' (p 'Us' q));
correctness
coherence
q 'or' (p '&&' (p 'Us' q)) is Element of LTLB_WFF ;
;
end;
:: deftheorem defines 'U' LTLAXIO1:def_8_:_
for p, q being Element of LTLB_WFF holds p 'U' q = q 'or' (p '&&' (p 'Us' q));
definition
let p, q be Element of LTLB_WFF ;
funcp 'R' q -> Element of LTLB_WFF equals :: LTLAXIO1:def 9
'not' (('not' p) 'U' ('not' q));
correctness
coherence
'not' (('not' p) 'U' ('not' q)) is Element of LTLB_WFF ;
;
end;
:: deftheorem defines 'R' LTLAXIO1:def_9_:_
for p, q being Element of LTLB_WFF holds p 'R' q = 'not' (('not' p) 'U' ('not' q));
begin
definition
func props -> Subset of LTLB_WFF means :: LTLAXIO1:def 10
for x being set holds
( x in it iff ex n being Element of NAT st x = prop n );
existence
ex b1 being Subset of LTLB_WFF st
for x being set holds
( x in b1 iff ex n being Element of NAT st x = prop n )
proof
defpred S1[ set ] means ex n being Element of NAT st $1 = prop n;
consider X being set such that
A1: for x being set holds
( x in X iff ( x in LTLB_WFF & S1[x] ) ) from XBOOLE_0:sch_1();
X c= LTLB_WFF
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in LTLB_WFF )
assume x in X ; ::_thesis: x in LTLB_WFF
hence x in LTLB_WFF by A1; ::_thesis: verum
end;
then reconsider X = X as Subset of LTLB_WFF ;
take X ; ::_thesis: for x being set holds
( x in X iff ex n being Element of NAT st x = prop n )
thus for x being set holds
( x in X iff ex n being Element of NAT st x = prop n ) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Subset of LTLB_WFF st ( for x being set holds
( x in b1 iff ex n being Element of NAT st x = prop n ) ) & ( for x being set holds
( x in b2 iff ex n being Element of NAT st x = prop n ) ) holds
b1 = b2
proof
let A, B be Subset of LTLB_WFF; ::_thesis: ( ( for x being set holds
( x in A iff ex n being Element of NAT st x = prop n ) ) & ( for x being set holds
( x in B iff ex n being Element of NAT st x = prop n ) ) implies A = B )
assume that
A2: for x being set holds
( x in A iff ex n being Element of NAT st x = prop n ) and
A3: for x being set holds
( x in B iff ex n being Element of NAT st x = prop n ) ; ::_thesis: A = B
A4: B c= A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B or x in A )
assume x in B ; ::_thesis: x in A
then consider n being Element of NAT such that
A5: x = prop n by A3;
thus x in A by A2, A5; ::_thesis: verum
end;
A c= B
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in B )
assume x in A ; ::_thesis: x in B
then consider n being Element of NAT such that
A6: x = prop n by A2;
thus x in B by A3, A6; ::_thesis: verum
end;
hence A = B by A4, XBOOLE_0:def_10; ::_thesis: verum
end;
end;
:: deftheorem defines props LTLAXIO1:def_10_:_
for b1 being Subset of LTLB_WFF holds
( b1 = props iff for x being set holds
( x in b1 iff ex n being Element of NAT st x = prop n ) );
definition
mode LTLModel is sequence of (bool props);
end;
definition
let M be LTLModel;
func SAT M -> Function of [:NAT,LTLB_WFF:],BOOLEAN means :Def11: :: LTLAXIO1:def 11
for n being Element of NAT holds
( it . [n,TFALSUM] = 0 & ( for k being Element of NAT holds
( it . [n,(prop k)] = 1 iff prop k in M . n ) ) & ( for p, q being Element of LTLB_WFF holds
( it . [n,(p => q)] = (it . [n,p]) => (it . [n,q]) & ( it . [n,(p 'Us' q)] = 1 implies ex i being Element of NAT st
( 0 < i & it . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds
it . [(n + j),p] = 1 ) ) ) & ( ex i being Element of NAT st
( 0 < i & it . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds
it . [(n + j),p] = 1 ) ) implies it . [n,(p 'Us' q)] = 1 ) ) ) );
existence
ex b1 being Function of [:NAT,LTLB_WFF:],BOOLEAN st
for n being Element of NAT holds
( b1 . [n,TFALSUM] = 0 & ( for k being Element of NAT holds
( b1 . [n,(prop k)] = 1 iff prop k in M . n ) ) & ( for p, q being Element of LTLB_WFF holds
( b1 . [n,(p => q)] = (b1 . [n,p]) => (b1 . [n,q]) & ( b1 . [n,(p 'Us' q)] = 1 implies ex i being Element of NAT st
( 0 < i & b1 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds
b1 . [(n + j),p] = 1 ) ) ) & ( ex i being Element of NAT st
( 0 < i & b1 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds
b1 . [(n + j),p] = 1 ) ) implies b1 . [n,(p 'Us' q)] = 1 ) ) ) )
proof
set FNB = Funcs (NAT,BOOLEAN);
defpred S1[ 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 S2[ 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 S3[ 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 S2[p,q,a,b,d]
proof
let p, q be Element of LTLB_WFF ; ::_thesis: for a, b being set ex d being set st S2[p,q,a,b,d]
let a, b be set ; ::_thesis: ex d being set st S2[p,q,a,b,d]
percases ( ( a is sequence of BOOLEAN & b is sequence of BOOLEAN ) or not a is sequence of BOOLEAN or not b is sequence of BOOLEAN ) ;
suppose ( a is sequence of BOOLEAN & b is sequence of BOOLEAN ) ; ::_thesis: ex d being set st S2[p,q,a,b,d]
then reconsider a1 = a, b1 = b as sequence of BOOLEAN ;
defpred S4[ 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:_for_n_being_Element_of_NAT_ex_y_being_Element_of_BOOLEAN_st_S4[n,y]
let n be Element of NAT ; ::_thesis: ex y being Element of BOOLEAN st S4[y,b2]
percases ( 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 ) ) or 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 ) ) ) ;
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: ex y being Element of BOOLEAN st S4[y,b2]
hence ex y being Element of BOOLEAN st S4[n,y] ; ::_thesis: verum
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: ex y being Element of BOOLEAN st S4[y,b2]
then S4[n, FALSE ] ;
hence ex y being Element of BOOLEAN st S4[n,y] ; ::_thesis: verum
end;
end;
end;
consider c being Function of NAT,BOOLEAN such that
A3: for n being Element of NAT holds S4[n,c . n] from FUNCT_2:sch_3(A2);
thus ex d being set st S2[p,q,a,b,d] by A3; ::_thesis: verum
end;
suppose ( not a is sequence of BOOLEAN or not b is sequence of BOOLEAN ) ; ::_thesis: ex d being set st S2[p,q,a,b,d]
hence ex d being set st S2[p,q,a,b,d] ; ::_thesis: verum
end;
end;
end;
A4: 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
proof
let p, q be Element of LTLB_WFF ; ::_thesis: for a, b, c, d being set st S2[p,q,a,b,c] & S2[p,q,a,b,d] holds
c = d
let a, b, c, d be set ; ::_thesis: ( S2[p,q,a,b,c] & S2[p,q,a,b,d] implies c = d )
assume that
A5: S2[p,q,a,b,c] and
A6: S2[p,q,a,b,d] ; ::_thesis: c = d
percases ( ( a is sequence of BOOLEAN & b is sequence of BOOLEAN ) or not a is sequence of BOOLEAN or not b is sequence of BOOLEAN ) ;
supposeA7: ( a is sequence of BOOLEAN & b is sequence of BOOLEAN ) ; ::_thesis: c = d
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:_for_x_being_set_st_x_in_NAT_holds_
s5_._x_=_s51_._x
let x be set ; ::_thesis: ( x in NAT implies s5 . b1 = s51 . b1 )
assume x in NAT ; ::_thesis: s5 . b1 = s51 . b1
then reconsider x1 = x as Element of NAT ;
percases ( s5 . x1 = 1 or s5 . x1 = 0 ) by XBOOLEAN:def_3;
supposeA14: s5 . x1 = 1 ; ::_thesis: s5 . b1 = s51 . b1
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: verum
end;
supposeA15: s5 . x1 = 0 ; ::_thesis: s5 . b1 = s51 . b1
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;
then not s51 . x1 = 1 by A10;
hence s5 . x = s51 . x by A15, XBOOLEAN:def_3; ::_thesis: verum
end;
end;
end;
hence c = d by A12, A9, FUNCT_2:12; ::_thesis: verum
end;
suppose ( not a is sequence of BOOLEAN or not b is sequence of BOOLEAN ) ; ::_thesis: c = d
hence c = d by A5, A6; ::_thesis: verum
end;
end;
end;
A16: for x being Element of NAT ex y being Element of Funcs (NAT,BOOLEAN) st S3[x,y]
proof
let x be Element of NAT ; ::_thesis: ex y being Element of Funcs (NAT,BOOLEAN) st S3[x,y]
defpred S4[ Element of NAT , Element of BOOLEAN ] means ( $2 = 1 iff prop x in M . $1 );
A17: now__::_thesis:_for_x1_being_Element_of_NAT_ex_y1_being_Element_of_BOOLEAN_st_S4[x1,y1]
let x1 be Element of NAT ; ::_thesis: ex y1 being Element of BOOLEAN st S4[y1,b2]
percases ( prop x in M . x1 or not prop x in M . x1 ) ;
suppose prop x in M . x1 ; ::_thesis: ex y1 being Element of BOOLEAN st S4[y1,b2]
then S4[x1, TRUE ] ;
hence ex y1 being Element of BOOLEAN st S4[x1,y1] ; ::_thesis: verum
end;
suppose not prop x in M . x1 ; ::_thesis: ex y1 being Element of BOOLEAN st S4[y1,b2]
then S4[x1, FALSE ] ;
hence ex y1 being Element of BOOLEAN st S4[x1,y1] ; ::_thesis: verum
end;
end;
end;
consider y being Function of NAT,BOOLEAN such that
A18: for n being Element of NAT holds S4[n,y . n] from FUNCT_2:sch_3(A17);
reconsider y = y as Element of Funcs (NAT,BOOLEAN) by FUNCT_2:8;
S3[x,y] by A18;
hence ex y being Element of Funcs (NAT,BOOLEAN) st S3[x,y] ; ::_thesis: verum
end;
consider f1 being Function of NAT,(Funcs (NAT,BOOLEAN)) such that
A19: for k being Element of NAT holds S3[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 S1[p,q,a,b,c] & S1[p,q,a,b,d] holds
c = d
proof
let p, q be Element of LTLB_WFF ; ::_thesis: for a, b, c, d being set st S1[p,q,a,b,c] & S1[p,q,a,b,d] holds
c = d
let a, b, c, d be set ; ::_thesis: ( S1[p,q,a,b,c] & S1[p,q,a,b,d] implies c = d )
assume that
A21: S1[p,q,a,b,c] and
A22: S1[p,q,a,b,d] ; ::_thesis: c = d
percases ( ( a is sequence of BOOLEAN & b is sequence of BOOLEAN ) or not a is sequence of BOOLEAN or not b is sequence of BOOLEAN ) ;
supposeA23: ( a is sequence of BOOLEAN & b is sequence of BOOLEAN ) ; ::_thesis: c = d
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:_for_x_being_set_st_x_in_NAT_holds_
s5_._x_=_s51_._x
let x be set ; ::_thesis: ( x in NAT implies s5 . x = s51 . x )
assume x in NAT ; ::_thesis: s5 . x = s51 . x
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: verum
end;
hence c = d by A30, A26, FUNCT_2:12; ::_thesis: verum
end;
suppose ( not a is sequence of BOOLEAN or not b is sequence of BOOLEAN ) ; ::_thesis: c = d
hence c = d by A21, A22; ::_thesis: verum
end;
end;
end;
deffunc H1( 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 S1[p,q,a,b,d]
proof
let p, q be Element of LTLB_WFF ; ::_thesis: for a, b being set ex d being set st S1[p,q,a,b,d]
let a, b be set ; ::_thesis: ex d being set st S1[p,q,a,b,d]
percases ( ( a is sequence of BOOLEAN & b is sequence of BOOLEAN ) or not a is sequence of BOOLEAN or not b is sequence of BOOLEAN ) ;
suppose ( a is sequence of BOOLEAN & b is sequence of BOOLEAN ) ; ::_thesis: ex d being set st S1[p,q,a,b,d]
then reconsider a1 = a, b1 = b as sequence of BOOLEAN ;
deffunc H2( Element of NAT ) -> Element of BOOLEAN = 'not' ((a1 . $1) '&' ('not' (b1 . $1)));
consider d being Function of NAT,BOOLEAN such that
A33: for n being Element of NAT holds d . n = H2(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 S1[p,q,a,b,d] ; ::_thesis: verum
end;
suppose ( not a is sequence of BOOLEAN or not b is sequence of BOOLEAN ) ; ::_thesis: ex d being set st S1[p,q,a,b,d]
hence ex d being set st S1[p,q,a,b,d] ; ::_thesis: verum
end;
end;
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) = H1(n) ) & ( for p, q being Element of LTLB_WFF holds
( S2[p,q,sat . p,sat . q,sat . (p 'Us' q)] & S1[p,q,sat . p,sat . q,sat . (p => q)] ) ) ) from HILBERT2:sch_3(A1, A32, A4, A20);
A35: now__::_thesis:_for_x_being_set_st_x_in_LTLB_WFF_holds_
sat_._x_in_Funcs_(NAT,BOOLEAN)
A36: now__::_thesis:_for_A,_B_being_Element_of_LTLB_WFF_holds_sat_._(A_=>_B)_in_Funcs_(NAT,BOOLEAN)
let A, B be Element of LTLB_WFF ; ::_thesis: sat . (b1 => b2) in Funcs (NAT,BOOLEAN)
A37: S1[A,B,sat . A,sat . B,sat . (A => B)] by A34;
percases ( ( sat . A is sequence of BOOLEAN & sat . B is sequence of BOOLEAN ) or not sat . A is sequence of BOOLEAN or not sat . B is sequence of BOOLEAN ) ;
suppose ( sat . A is sequence of BOOLEAN & sat . B is sequence of BOOLEAN ) ; ::_thesis: sat . (b1 => b2) in Funcs (NAT,BOOLEAN)
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: verum
end;
suppose ( not sat . A is sequence of BOOLEAN or not sat . B is sequence of BOOLEAN ) ; ::_thesis: sat . (b1 => b2) in Funcs (NAT,BOOLEAN)
thus sat . (A => B) in Funcs (NAT,BOOLEAN) by A37, FUNCT_2:8; ::_thesis: verum
end;
end;
end;
A39: now__::_thesis:_for_A,_B_being_Element_of_LTLB_WFF_holds_sat_._(A_'Us'_B)_in_Funcs_(NAT,BOOLEAN)
let A, B be Element of LTLB_WFF ; ::_thesis: sat . (b1 'Us' b2) in Funcs (NAT,BOOLEAN)
A40: S2[A,B,sat . A,sat . B,sat . (A 'Us' B)] by A34;
percases ( ( sat . A is sequence of BOOLEAN & sat . B is sequence of BOOLEAN ) or not sat . A is sequence of BOOLEAN or not sat . B is sequence of BOOLEAN ) ;
suppose ( sat . A is sequence of BOOLEAN & sat . B is sequence of BOOLEAN ) ; ::_thesis: sat . (b1 'Us' b2) in Funcs (NAT,BOOLEAN)
then consider s3, s4, s5 being sequence of BOOLEAN such that
s3 = sat . A and
s4 = sat . B and
A41: s5 = sat . (A 'Us' 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 'Us' B) in Funcs (NAT,BOOLEAN) by A41, FUNCT_2:8; ::_thesis: verum
end;
suppose ( not sat . A is sequence of BOOLEAN or not sat . B is sequence of BOOLEAN ) ; ::_thesis: sat . (b1 'Us' b2) in Funcs (NAT,BOOLEAN)
thus sat . (A 'Us' B) in Funcs (NAT,BOOLEAN) by A40, FUNCT_2:8; ::_thesis: verum
end;
end;
end;
let x be set ; ::_thesis: ( x in LTLB_WFF implies sat . b1 in Funcs (NAT,BOOLEAN) )
assume x in LTLB_WFF ; ::_thesis: sat . b1 in Funcs (NAT,BOOLEAN)
then reconsider x1 = x as Element of LTLB_WFF ;
A42: now__::_thesis:_for_n_being_Element_of_NAT_holds_sat_._(prop_n)_in_Funcs_(NAT,BOOLEAN)
let n be Element of NAT ; ::_thesis: sat . (prop n) in Funcs (NAT,BOOLEAN)
sat . (prop n) = f1 . n by A34;
hence sat . (prop n) in Funcs (NAT,BOOLEAN) ; ::_thesis: verum
end;
percases ( 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 'Us' q or ex p, q being Element of LTLB_WFF st x1 = p => q ) by Th4;
suppose x1 = TFALSUM ; ::_thesis: sat . b1 in Funcs (NAT,BOOLEAN)
hence sat . x in Funcs (NAT,BOOLEAN) by A34, FUNCT_2:8; ::_thesis: verum
end;
suppose ex n being Element of NAT st x1 = prop n ; ::_thesis: sat . b1 in Funcs (NAT,BOOLEAN)
hence sat . x in Funcs (NAT,BOOLEAN) by A42; ::_thesis: verum
end;
suppose ex p, q being Element of LTLB_WFF st x1 = p 'Us' q ; ::_thesis: sat . b1 in Funcs (NAT,BOOLEAN)
hence sat . x in Funcs (NAT,BOOLEAN) by A39; ::_thesis: verum
end;
suppose ex p, q being Element of LTLB_WFF st x1 = p => q ; ::_thesis: sat . b1 in Funcs (NAT,BOOLEAN)
hence sat . x in Funcs (NAT,BOOLEAN) by A36; ::_thesis: verum
end;
end;
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 H2( 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) = H2(n,A) from BINOP_1:sch_4();
A44: now__::_thesis:_for_A_being_Element_of_LTLB_WFF_
for_n_being_Element_of_NAT_holds_sat2_._[n,A]_=_(sat_._A)_._n
let A be Element of LTLB_WFF ; ::_thesis: for n being Element of NAT holds sat2 . [n,A] = (sat . A) . n
let n be Element of NAT ; ::_thesis: sat2 . [n,A] = (sat . A) . n
thus sat2 . [n,A] = sat2 . (n,A) by BINOP_1:def_1
.= (sat . A) . n by A43 ; ::_thesis: verum
end;
A45: now__::_thesis:_for_k,_n_being_Element_of_NAT_holds_
(_sat2_._[n,(prop_k)]_=_1_iff_prop_k_in_M_._n_)
let k, n be Element of NAT ; ::_thesis: ( sat2 . [n,(prop k)] = 1 iff prop k in M . n )
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: verum
end;
A46: now__::_thesis:_for_p,_q_being_Element_of_LTLB_WFF_
for_n_being_Element_of_NAT_holds_
(_sat2_._[n,(p_=>_q)]_=_(sat2_._[n,p])_=>_(sat2_._[n,q])_&_(_sat2_._[n,(p_'Us'_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_'Us'_q)]_=_1_)_)
let p, q be Element of LTLB_WFF ; ::_thesis: for n being Element of NAT holds
( sat2 . [n,(p => q)] = (sat2 . [n,p]) => (sat2 . [n,q]) & ( sat2 . [n,(p 'Us' 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 'Us' q)] = 1 ) )
let n be Element of NAT ; ::_thesis: ( sat2 . [n,(p => q)] = (sat2 . [n,p]) => (sat2 . [n,q]) & ( sat2 . [n,(p 'Us' 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 'Us' q)] = 1 ) )
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 'Us' 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: ( sat2 . [n,(p 'Us' 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 ) ) )
thus ( sat2 . [n,(p 'Us' 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: verum
proof
hereby ::_thesis: ( 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 'Us' q)] = 1 )
assume sat2 . [n,(p 'Us' q)] = 1 ; ::_thesis: 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 ) )
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:_for_j_being_Element_of_NAT_st_1_<=_j_&_j_<_i_holds_
sat2_._[(n_+_j),p]_=_1
let j be Element of NAT ; ::_thesis: ( 1 <= j & j < i implies sat2 . [(n + j),p] = 1 )
assume A58: ( 1 <= j & j < i ) ; ::_thesis: sat2 . [(n + j),p] = 1
thus sat2 . [(n + j),p] = (sat . p) . (n + j) by A44
.= 1 by A47, A56, A58 ; ::_thesis: verum
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: verum
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: sat2 . [n,(p 'Us' q)] = 1
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: ( 1 <= j & j < i implies s31 . (n + j) = 1 )
assume A64: ( 1 <= j & j < i ) ; ::_thesis: s31 . (n + j) = 1
thus s31 . (n + j) = sat2 . [(n + j),p] by A44, A47
.= 1 by A61, A64 ; ::_thesis: verum
end;
thus sat2 . [n,(p 'Us' q)] = s51 . n by A44, A49
.= 1 by A50, A59, A62, A63 ; ::_thesis: verum
end;
end;
take sat2 ; ::_thesis: 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 'Us' 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 'Us' q)] = 1 ) ) ) )
now__::_thesis:_for_n_being_Element_of_NAT_holds_sat2_._[n,TFALSUM]_=_0
let n be Element of NAT ; ::_thesis: sat2 . [n,TFALSUM] = 0
thus sat2 . [n,TFALSUM] = (sat . TFALSUM) . n by A44
.= 0 by A34, FUNCOP_1:7 ; ::_thesis: verum
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 'Us' 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 'Us' q)] = 1 ) ) ) ) by A45, A46; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of [:NAT,LTLB_WFF:],BOOLEAN st ( for n being Element of NAT holds
( b1 . [n,TFALSUM] = 0 & ( for k being Element of NAT holds
( b1 . [n,(prop k)] = 1 iff prop k in M . n ) ) & ( for p, q being Element of LTLB_WFF holds
( b1 . [n,(p => q)] = (b1 . [n,p]) => (b1 . [n,q]) & ( b1 . [n,(p 'Us' q)] = 1 implies ex i being Element of NAT st
( 0 < i & b1 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds
b1 . [(n + j),p] = 1 ) ) ) & ( ex i being Element of NAT st
( 0 < i & b1 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds
b1 . [(n + j),p] = 1 ) ) implies b1 . [n,(p 'Us' q)] = 1 ) ) ) ) ) & ( for n being Element of NAT holds
( b2 . [n,TFALSUM] = 0 & ( for k being Element of NAT holds
( b2 . [n,(prop k)] = 1 iff prop k in M . n ) ) & ( for p, q being Element of LTLB_WFF holds
( b2 . [n,(p => q)] = (b2 . [n,p]) => (b2 . [n,q]) & ( b2 . [n,(p 'Us' q)] = 1 implies ex i being Element of NAT st
( 0 < i & b2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds
b2 . [(n + j),p] = 1 ) ) ) & ( ex i being Element of NAT st
( 0 < i & b2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds
b2 . [(n + j),p] = 1 ) ) implies b2 . [n,(p 'Us' q)] = 1 ) ) ) ) ) holds
b1 = b2
proof
let v1, v2 be Function of [:NAT,LTLB_WFF:],BOOLEAN; ::_thesis: ( ( for n being Element of NAT holds
( v1 . [n,TFALSUM] = 0 & ( for k being Element of NAT holds
( v1 . [n,(prop k)] = 1 iff prop k in M . n ) ) & ( for p, q being Element of LTLB_WFF holds
( v1 . [n,(p => q)] = (v1 . [n,p]) => (v1 . [n,q]) & ( v1 . [n,(p 'Us' q)] = 1 implies ex i being Element of NAT st
( 0 < i & v1 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds
v1 . [(n + j),p] = 1 ) ) ) & ( ex i being Element of NAT st
( 0 < i & v1 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds
v1 . [(n + j),p] = 1 ) ) implies v1 . [n,(p 'Us' q)] = 1 ) ) ) ) ) & ( for n being Element of NAT holds
( v2 . [n,TFALSUM] = 0 & ( for k being Element of NAT holds
( v2 . [n,(prop k)] = 1 iff prop k in M . n ) ) & ( for p, q being Element of LTLB_WFF holds
( v2 . [n,(p => q)] = (v2 . [n,p]) => (v2 . [n,q]) & ( v2 . [n,(p 'Us' q)] = 1 implies ex i being Element of NAT st
( 0 < i & v2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds
v2 . [(n + j),p] = 1 ) ) ) & ( ex i being Element of NAT st
( 0 < i & v2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds
v2 . [(n + j),p] = 1 ) ) implies v2 . [n,(p 'Us' q)] = 1 ) ) ) ) ) implies v1 = v2 )
assume A65: for n being Element of NAT holds
( v1 . [n,TFALSUM] = 0 & ( for k being Element of NAT holds
( v1 . [n,(prop k)] = 1 iff prop k in M . n ) ) & ( for p, q being Element of LTLB_WFF holds
( v1 . [n,(p => q)] = (v1 . [n,p]) => (v1 . [n,q]) & ( v1 . [n,(p 'Us' q)] = 1 implies ex i being Element of NAT st
( 0 < i & v1 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds
v1 . [(n + j),p] = 1 ) ) ) & ( ex i being Element of NAT st
( 0 < i & v1 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds
v1 . [(n + j),p] = 1 ) ) implies v1 . [n,(p 'Us' q)] = 1 ) ) ) ) ; ::_thesis: ( ex n being Element of NAT st
( v2 . [n,TFALSUM] = 0 & ( for k being Element of NAT holds
( v2 . [n,(prop k)] = 1 iff prop k in M . n ) ) implies ex p, q being Element of LTLB_WFF st
( v2 . [n,(p => q)] = (v2 . [n,p]) => (v2 . [n,q]) & ( v2 . [n,(p 'Us' q)] = 1 implies ex i being Element of NAT st
( 0 < i & v2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds
v2 . [(n + j),p] = 1 ) ) ) implies ( ex i being Element of NAT st
( 0 < i & v2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds
v2 . [(n + j),p] = 1 ) ) & not v2 . [n,(p 'Us' q)] = 1 ) ) ) or v1 = v2 )
assume A66: for n being Element of NAT holds
( v2 . [n,TFALSUM] = 0 & ( for k being Element of NAT holds
( v2 . [n,(prop k)] = 1 iff prop k in M . n ) ) & ( for p, q being Element of LTLB_WFF holds
( v2 . [n,(p => q)] = (v2 . [n,p]) => (v2 . [n,q]) & ( v2 . [n,(p 'Us' q)] = 1 implies ex i being Element of NAT st
( 0 < i & v2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds
v2 . [(n + j),p] = 1 ) ) ) & ( ex i being Element of NAT st
( 0 < i & v2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds
v2 . [(n + j),p] = 1 ) ) implies v2 . [n,(p 'Us' q)] = 1 ) ) ) ) ; ::_thesis: v1 = v2
thus v1 = v2 ::_thesis: verum
proof
defpred S1[ Element of LTLB_WFF ] means for n being Element of NAT holds v1 . [n,$1] = v2 . [n,$1];
A67: for n being Element of NAT holds S1[ prop n]
proof
let k be Element of NAT ; ::_thesis: S1[ prop k]
now__::_thesis:_for_n_being_Element_of_NAT_holds_v1_._[n,(prop_k)]_=_v2_._[n,(prop_k)]
let n be Element of NAT ; ::_thesis: v1 . [b1,(prop k)] = v2 . [b1,(prop k)]
percases ( prop k in M . n or not prop k in M . n ) ;
supposeA68: prop k in M . n ; ::_thesis: v1 . [b1,(prop k)] = v2 . [b1,(prop k)]
hence v1 . [n,(prop k)] = 1 by A65
.= v2 . [n,(prop k)] by A66, A68 ;
::_thesis: verum
end;
supposeA69: not prop k in M . n ; ::_thesis: v1 . [b1,(prop k)] = v2 . [b1,(prop k)]
then not v1 . [n,(prop k)] = 1 by A65;
then A70: v1 . [n,(prop k)] = 0 by XBOOLEAN:def_3;
not v2 . [n,(prop k)] = 1 by A66, A69;
hence v1 . [n,(prop k)] = v2 . [n,(prop k)] by A70, XBOOLEAN:def_3; ::_thesis: verum
end;
end;
end;
hence S1[ prop k] ; ::_thesis: verum
end;
A71: for p, q being Element of LTLB_WFF st S1[p] & S1[q] holds
( S1[p 'Us' q] & S1[p => q] )
proof
let p, q be Element of LTLB_WFF ; ::_thesis: ( S1[p] & S1[q] implies ( S1[p 'Us' q] & S1[p => q] ) )
assume that
A72: S1[p] and
A73: S1[q] ; ::_thesis: ( S1[p 'Us' q] & S1[p => q] )
thus S1[p 'Us' q] ::_thesis: S1[p => q]
proof
let n be Element of NAT ; ::_thesis: v1 . [n,(p 'Us' q)] = v2 . [n,(p 'Us' q)]
percases ( ex i being Element of NAT st
( 0 < i & v1 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds
v1 . [(n + j),p] = 1 ) ) or for i being Element of NAT holds
( not 0 < i or not v1 . [(n + i),q] = 1 or ex j being Element of NAT st
( 1 <= j & j < i & not v1 . [(n + j),p] = 1 ) ) ) ;
supposeA74: ex i being Element of NAT st
( 0 < i & v1 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds
v1 . [(n + j),p] = 1 ) ) ; ::_thesis: v1 . [n,(p 'Us' q)] = v2 . [n,(p 'Us' q)]
then consider i being Element of NAT such that
A75: 0 < i and
A76: v1 . [(n + i),q] = 1 and
A77: for j being Element of NAT st 1 <= j & j < i holds
v1 . [(n + j),p] = 1 ;
A78: v2 . [(n + i),q] = 1 by A73, A76;
A79: now__::_thesis:_for_j_being_Element_of_NAT_st_1_<=_j_&_j_<_i_holds_
v2_._[(n_+_j),p]_=_1
let j be Element of NAT ; ::_thesis: ( 1 <= j & j < i implies v2 . [(n + j),p] = 1 )
assume ( 1 <= j & j < i ) ; ::_thesis: v2 . [(n + j),p] = 1
then v1 . [(n + j),p] = 1 by A77;
hence v2 . [(n + j),p] = 1 by A72; ::_thesis: verum
end;
thus v1 . [n,(p 'Us' q)] = 1 by A65, A74
.= v2 . [n,(p 'Us' q)] by A66, A75, A78, A79 ; ::_thesis: verum
end;
supposeA80: for i being Element of NAT holds
( not 0 < i or not v1 . [(n + i),q] = 1 or ex j being Element of NAT st
( 1 <= j & j < i & not v1 . [(n + j),p] = 1 ) ) ; ::_thesis: v1 . [n,(p 'Us' q)] = v2 . [n,(p 'Us' q)]
now__::_thesis:_for_i_being_Element_of_NAT_holds_
(_not_0_<_i_or_not_v2_._[(n_+_i),q]_=_1_or_ex_j_being_Element_of_NAT_st_
(_1_<=_j_&_j_<_i_&_not_v2_._[(n_+_j),p]_=_1_)_)
let i be Element of NAT ; ::_thesis: ( not 0 < b1 or not v2 . [(n + b1),q] = 1 or ex j being Element of NAT st
( 1 <= b2 & b2 < j & not v2 . [(n + b2),p] = 1 ) )
percases ( not 0 < i or not v1 . [(n + i),q] = 1 or ex j being Element of NAT st
( 1 <= j & j < i & not v1 . [(n + j),p] = 1 ) ) by A80;
suppose not 0 < i ; ::_thesis: ( not 0 < b1 or not v2 . [(n + b1),q] = 1 or ex j being Element of NAT st
( 1 <= b2 & b2 < j & not v2 . [(n + b2),p] = 1 ) )
hence ( not 0 < i or not v2 . [(n + i),q] = 1 or ex j being Element of NAT st
( 1 <= j & j < i & not v2 . [(n + j),p] = 1 ) ) ; ::_thesis: verum
end;
suppose not v1 . [(n + i),q] = 1 ; ::_thesis: ( not 0 < b1 or not v2 . [(n + b1),q] = 1 or ex j being Element of NAT st
( 1 <= b2 & b2 < j & not v2 . [(n + b2),p] = 1 ) )
hence ( not 0 < i or not v2 . [(n + i),q] = 1 or ex j being Element of NAT st
( 1 <= j & j < i & not v2 . [(n + j),p] = 1 ) ) by A73; ::_thesis: verum
end;
suppose ex j being Element of NAT st
( 1 <= j & j < i & not v1 . [(n + j),p] = 1 ) ; ::_thesis: ( not 0 < b1 or not v2 . [(n + b1),q] = 1 or ex j being Element of NAT st
( 1 <= b2 & b2 < j & not v2 . [(n + b2),p] = 1 ) )
then consider j being Element of NAT such that
A81: ( 1 <= j & j < i ) and
A82: not v1 . [(n + j),p] = 1 ;
not v2 . [(n + j),p] = 1 by A72, A82;
hence ( not 0 < i or not v2 . [(n + i),q] = 1 or ex j being Element of NAT st
( 1 <= j & j < i & not v2 . [(n + j),p] = 1 ) ) by A81; ::_thesis: verum
end;
end;
end;
then A83: not v2 . [n,(p 'Us' q)] = 1 by A66;
not v1 . [n,(p 'Us' q)] = 1 by A65, A80;
then v1 . [n,(p 'Us' q)] = 0 by XBOOLEAN:def_3;
hence v1 . [n,(p 'Us' q)] = v2 . [n,(p 'Us' q)] by A83, XBOOLEAN:def_3; ::_thesis: verum
end;
end;
end;
thus S1[p => q] ::_thesis: verum
proof
let n be Element of NAT ; ::_thesis: v1 . [n,(p => q)] = v2 . [n,(p => q)]
thus v1 . [n,(p => q)] = (v1 . [n,p]) => (v1 . [n,q]) by A65
.= (v2 . [n,p]) => (v1 . [n,q]) by A72
.= (v2 . [n,p]) => (v2 . [n,q]) by A73
.= v2 . [n,(p => q)] by A66 ; ::_thesis: verum
end;
end;
now__::_thesis:_for_n_being_Element_of_NAT_holds_v1_._[n,TFALSUM]_=_v2_._[n,TFALSUM]
let n be Element of NAT ; ::_thesis: v1 . [n,TFALSUM] = v2 . [n,TFALSUM]
thus v1 . [n,TFALSUM] = 0 by A65
.= v2 . [n,TFALSUM] by A66 ; ::_thesis: verum
end;
then A84: S1[ TFALSUM ] ;
A85: for A being Element of LTLB_WFF holds S1[A] from HILBERT2:sch_2(A84, A67, A71);
A86: for x being Element of [:NAT,LTLB_WFF:] st x in dom v1 holds
v1 . x = v2 . x
proof
let x be Element of [:NAT,LTLB_WFF:]; ::_thesis: ( x in dom v1 implies v1 . x = v2 . x )
consider y, z being set such that
A87: y in NAT and
A88: z in LTLB_WFF and
A89: x = [y,z] by ZFMISC_1:def_2;
reconsider y1 = y as Element of NAT by A87;
assume x in dom v1 ; ::_thesis: v1 . x = v2 . x
thus v1 . x = v2 . x by A85, A87, A88, A89; ::_thesis: verum
reconsider z1 = z as Element of LTLB_WFF by A88;
end;
dom v1 = [:NAT,LTLB_WFF:] by FUNCT_2:def_1
.= dom v2 by FUNCT_2:def_1 ;
hence v1 = v2 by A86, PARTFUN1:5; ::_thesis: verum
end;
end;
end;
:: deftheorem Def11 defines SAT LTLAXIO1:def_11_:_
for M being LTLModel
for b2 being Function of [:NAT,LTLB_WFF:],BOOLEAN holds
( b2 = SAT M iff for n being Element of NAT holds
( b2 . [n,TFALSUM] = 0 & ( for k being Element of NAT holds
( b2 . [n,(prop k)] = 1 iff prop k in M . n ) ) & ( for p, q being Element of LTLB_WFF holds
( b2 . [n,(p => q)] = (b2 . [n,p]) => (b2 . [n,q]) & ( b2 . [n,(p 'Us' q)] = 1 implies ex i being Element of NAT st
( 0 < i & b2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds
b2 . [(n + j),p] = 1 ) ) ) & ( ex i being Element of NAT st
( 0 < i & b2 . [(n + i),q] = 1 & ( for j being Element of NAT st 1 <= j & j < i holds
b2 . [(n + j),p] = 1 ) ) implies b2 . [n,(p 'Us' q)] = 1 ) ) ) ) );
theorem Th5: :: LTLAXIO1:5
for A being Element of LTLB_WFF
for n being Element of NAT
for M being LTLModel holds
( (SAT M) . [n,('not' A)] = 1 iff (SAT M) . [n,A] = 0 )
proof
let A be Element of LTLB_WFF ; ::_thesis: for n being Element of NAT
for M being LTLModel holds
( (SAT M) . [n,('not' A)] = 1 iff (SAT M) . [n,A] = 0 )
let n be Element of NAT ; ::_thesis: for M being LTLModel holds
( (SAT M) . [n,('not' A)] = 1 iff (SAT M) . [n,A] = 0 )
let M be LTLModel; ::_thesis: ( (SAT M) . [n,('not' A)] = 1 iff (SAT M) . [n,A] = 0 )
hereby ::_thesis: ( (SAT M) . [n,A] = 0 implies (SAT M) . [n,('not' A)] = 1 )
assume (SAT M) . [n,('not' A)] = 1 ; ::_thesis: (SAT M) . [n,A] = 0
then A1: ((SAT M) . [n,A]) => ((SAT M) . [n,TFALSUM]) = 1 by Def11;
( (SAT M) . [n,A] = 1 or (SAT M) . [n,A] = 0 ) by XBOOLEAN:def_3;
hence (SAT M) . [n,A] = 0 by A1, Def11; ::_thesis: verum
end;
assume A2: (SAT M) . [n,A] = 0 ; ::_thesis: (SAT M) . [n,('not' A)] = 1
thus (SAT M) . [n,('not' A)] = ((SAT M) . [n,A]) => ((SAT M) . [n,TFALSUM]) by Def11
.= 1 by A2 ; ::_thesis: verum
end;
theorem Th6: :: LTLAXIO1:6
for n being Element of NAT
for M being LTLModel holds (SAT M) . [n,TVERUM] = 1
proof
let n be Element of NAT ; ::_thesis: for M being LTLModel holds (SAT M) . [n,TVERUM] = 1
let M be LTLModel; ::_thesis: (SAT M) . [n,TVERUM] = 1
assume not (SAT M) . [n,TVERUM] = 1 ; ::_thesis: contradiction
then not (SAT M) . [n,TFALSUM] = 0 by Th5;
hence contradiction by Def11; ::_thesis: verum
end;
theorem Th7: :: LTLAXIO1:7
for A, B being Element of LTLB_WFF
for n being Element of NAT
for M being LTLModel holds
( (SAT M) . [n,(A '&&' B)] = 1 iff ( (SAT M) . [n,A] = 1 & (SAT M) . [n,B] = 1 ) )
proof
let A, B be Element of LTLB_WFF ; ::_thesis: for n being Element of NAT
for M being LTLModel holds
( (SAT M) . [n,(A '&&' B)] = 1 iff ( (SAT M) . [n,A] = 1 & (SAT M) . [n,B] = 1 ) )
let n be Element of NAT ; ::_thesis: for M being LTLModel holds
( (SAT M) . [n,(A '&&' B)] = 1 iff ( (SAT M) . [n,A] = 1 & (SAT M) . [n,B] = 1 ) )
let M be LTLModel; ::_thesis: ( (SAT M) . [n,(A '&&' B)] = 1 iff ( (SAT M) . [n,A] = 1 & (SAT M) . [n,B] = 1 ) )
hereby ::_thesis: ( (SAT M) . [n,A] = 1 & (SAT M) . [n,B] = 1 implies (SAT M) . [n,(A '&&' B)] = 1 )
assume (SAT M) . [n,(A '&&' B)] = 1 ; ::_thesis: ( (SAT M) . [n,A] = 1 & (SAT M) . [n,B] = 1 )
then ((SAT M) . [n,(A => (B => TFALSUM))]) => ((SAT M) . [n,TFALSUM]) = 1 by Def11;
then ((SAT M) . [n,(A => (B => TFALSUM))]) => FALSE = 1 by Def11;
then ((SAT M) . [n,A]) => ((SAT M) . [n,(B => TFALSUM)]) = 0 by Def11;
then ((SAT M) . [n,A]) => (((SAT M) . [n,B]) => ((SAT M) . [n,TFALSUM])) = 0 by Def11;
then A1: ((SAT M) . [n,A]) => (((SAT M) . [n,B]) => FALSE) = 0 by Def11;
( (SAT M) . [n,A] = 0 or (SAT M) . [n,A] = 1 ) by XBOOLEAN:def_3;
hence ( (SAT M) . [n,A] = 1 & (SAT M) . [n,B] = 1 ) by A1; ::_thesis: verum
end;
assume that
A2: (SAT M) . [n,A] = 1 and
A3: (SAT M) . [n,B] = 1 ; ::_thesis: (SAT M) . [n,(A '&&' B)] = 1
((SAT M) . [n,B]) => ((SAT M) . [n,TFALSUM]) = 0 by A3, Def11;
then ((SAT M) . [n,A]) => ((SAT M) . [n,(B => TFALSUM)]) = 0 by A2, Def11;
then (SAT M) . [n,(A => (B => TFALSUM))] = 0 by Def11;
then ((SAT M) . [n,(A => (B => TFALSUM))]) => ((SAT M) . [n,TFALSUM]) = 1 ;
hence (SAT M) . [n,(A '&&' B)] = 1 by Def11; ::_thesis: verum
end;
theorem Th8: :: LTLAXIO1:8
for A, B being Element of LTLB_WFF
for n being Element of NAT
for M being LTLModel holds
( (SAT M) . [n,(A 'or' B)] = 1 iff ( (SAT M) . [n,A] = 1 or (SAT M) . [n,B] = 1 ) )
proof
let A, B be Element of LTLB_WFF ; ::_thesis: for n being Element of NAT
for M being LTLModel holds
( (SAT M) . [n,(A 'or' B)] = 1 iff ( (SAT M) . [n,A] = 1 or (SAT M) . [n,B] = 1 ) )
let n be Element of NAT ; ::_thesis: for M being LTLModel holds
( (SAT M) . [n,(A 'or' B)] = 1 iff ( (SAT M) . [n,A] = 1 or (SAT M) . [n,B] = 1 ) )
let M be LTLModel; ::_thesis: ( (SAT M) . [n,(A 'or' B)] = 1 iff ( (SAT M) . [n,A] = 1 or (SAT M) . [n,B] = 1 ) )
hereby ::_thesis: ( ( (SAT M) . [n,A] = 1 or (SAT M) . [n,B] = 1 ) implies (SAT M) . [n,(A 'or' B)] = 1 )
assume (SAT M) . [n,(A 'or' B)] = 1 ; ::_thesis: ( (SAT M) . [n,A] = 1 or (SAT M) . [n,B] = 1 )
then A1: (SAT M) . [n,(('not' A) '&&' ('not' B))] = 0 by Th5;
percases ( not (SAT M) . [n,('not' A)] = 1 or not (SAT M) . [n,('not' B)] = 1 ) by A1, Th7;
suppose not (SAT M) . [n,('not' A)] = 1 ; ::_thesis: ( (SAT M) . [n,A] = 1 or (SAT M) . [n,B] = 1 )
then not (SAT M) . [n,A] = 0 by Th5;
hence ( (SAT M) . [n,A] = 1 or (SAT M) . [n,B] = 1 ) by XBOOLEAN:def_3; ::_thesis: verum
end;
suppose not (SAT M) . [n,('not' B)] = 1 ; ::_thesis: ( (SAT M) . [n,A] = 1 or (SAT M) . [n,B] = 1 )
then not (SAT M) . [n,B] = 0 by Th5;
hence ( (SAT M) . [n,A] = 1 or (SAT M) . [n,B] = 1 ) by XBOOLEAN:def_3; ::_thesis: verum
end;
end;
end;
assume A2: ( (SAT M) . [n,A] = 1 or (SAT M) . [n,B] = 1 ) ; ::_thesis: (SAT M) . [n,(A 'or' B)] = 1
percases ( (SAT M) . [n,A] = 1 or (SAT M) . [n,B] = 1 ) by A2;
suppose (SAT M) . [n,A] = 1 ; ::_thesis: (SAT M) . [n,(A 'or' B)] = 1
then not (SAT M) . [n,('not' A)] = 1 by Th5;
then not (SAT M) . [n,(('not' A) '&&' ('not' B))] = 1 by Th7;
then (SAT M) . [n,(('not' A) '&&' ('not' B))] = 0 by XBOOLEAN:def_3;
hence (SAT M) . [n,(A 'or' B)] = 1 by Th5; ::_thesis: verum
end;
suppose (SAT M) . [n,B] = 1 ; ::_thesis: (SAT M) . [n,(A 'or' B)] = 1
then not (SAT M) . [n,('not' B)] = 1 by Th5;
then not (SAT M) . [n,(('not' A) '&&' ('not' B))] = 1 by Th7;
then (SAT M) . [n,(('not' A) '&&' ('not' B))] = 0 by XBOOLEAN:def_3;
hence (SAT M) . [n,(A 'or' B)] = 1 by Th5; ::_thesis: verum
end;
end;
end;
theorem Th9: :: LTLAXIO1:9
for A being Element of LTLB_WFF
for n being Element of NAT
for M being LTLModel holds (SAT M) . [n,('X' A)] = (SAT M) . [(n + 1),A]
proof
let A be Element of LTLB_WFF ; ::_thesis: for n being Element of NAT
for M being LTLModel holds (SAT M) . [n,('X' A)] = (SAT M) . [(n + 1),A]
let n be Element of NAT ; ::_thesis: for M being LTLModel holds (SAT M) . [n,('X' A)] = (SAT M) . [(n + 1),A]
let M be LTLModel; ::_thesis: (SAT M) . [n,('X' A)] = (SAT M) . [(n + 1),A]
set f = TFALSUM ;
set sm = SAT M;
percases ( (SAT M) . [n,(TFALSUM 'Us' A)] = 1 or (SAT M) . [n,(TFALSUM 'Us' A)] = 0 ) by XBOOLEAN:def_3;
supposeA1: (SAT M) . [n,(TFALSUM 'Us' A)] = 1 ; ::_thesis: (SAT M) . [n,('X' A)] = (SAT M) . [(n + 1),A]
then consider i being Element of NAT such that
A2: ( 0 < i & (SAT M) . [(n + i),A] = 1 ) and
A3: for j being Element of NAT st 1 <= j & j < i holds
(SAT M) . [(n + j),TFALSUM] = 1 by Def11;
now__::_thesis:_not_1_<_i
assume A4: 1 < i ; ::_thesis: contradiction
not (SAT M) . [(n + 1),TFALSUM] = 1 by Def11;
hence contradiction by A3, A4; ::_thesis: verum
end;
hence (SAT M) . [n,('X' A)] = (SAT M) . [(n + 1),A] by A1, A2, NAT_1:25; ::_thesis: verum
end;
supposeA5: (SAT M) . [n,(TFALSUM 'Us' A)] = 0 ; ::_thesis: (SAT M) . [n,('X' A)] = (SAT M) . [(n + 1),A]
now__::_thesis:_not_(SAT_M)_._[(n_+_1),A]_=_1
assume A6: (SAT M) . [(n + 1),A] = 1 ; ::_thesis: contradiction
( not 0 < 1 or not (SAT M) . [(n + 1),A] = 1 or ex j being Element of NAT st
( 1 <= j & j < 1 & not (SAT M) . [(n + j),TFALSUM] = 1 ) ) by A5, Def11;
hence contradiction by A6; ::_thesis: verum
end;
hence (SAT M) . [n,('X' A)] = (SAT M) . [(n + 1),A] by A5, XBOOLEAN:def_3; ::_thesis: verum
end;
end;
end;
theorem Th10: :: LTLAXIO1:10
for A being Element of LTLB_WFF
for n being Element of NAT
for M being LTLModel holds
( (SAT M) . [n,('G' A)] = 1 iff for i being Element of NAT holds (SAT M) . [(n + i),A] = 1 )
proof
let A be Element of LTLB_WFF ; ::_thesis: for n being Element of NAT
for M being LTLModel holds
( (SAT M) . [n,('G' A)] = 1 iff for i being Element of NAT holds (SAT M) . [(n + i),A] = 1 )
let n be Element of NAT ; ::_thesis: for M being LTLModel holds
( (SAT M) . [n,('G' A)] = 1 iff for i being Element of NAT holds (SAT M) . [(n + i),A] = 1 )
let M be LTLModel; ::_thesis: ( (SAT M) . [n,('G' A)] = 1 iff for i being Element of NAT holds (SAT M) . [(n + i),A] = 1 )
set f = TFALSUM ;
set t = TVERUM ;
set sm = SAT M;
hereby ::_thesis: ( ( for i being Element of NAT holds (SAT M) . [(n + i),A] = 1 ) implies (SAT M) . [n,('G' A)] = 1 )
assume (SAT M) . [n,('G' A)] = 1 ; ::_thesis: for i being Element of NAT holds (SAT M) . [(n + b2),A] = 1
then A1: (SAT M) . [n,(('not' A) 'or' (TVERUM '&&' (TVERUM 'Us' ('not' A))))] = 0 by Th5;
then not (SAT M) . [n,('not' A)] = 1 by Th8;
then A2: not (SAT M) . [n,A] = 0 by Th5;
let i be Element of NAT ; ::_thesis: (SAT M) . [(n + b1),A] = 1
not (SAT M) . [n,(TVERUM '&&' (TVERUM 'Us' ('not' A)))] = 1 by A1, Th8;
then A3: ( not (SAT M) . [n,TVERUM] = 1 or not (SAT M) . [n,(TVERUM 'Us' ('not' A))] = 1 ) by Th7;
percases ( i = 0 or 0 < i ) ;
suppose i = 0 ; ::_thesis: (SAT M) . [(n + b1),A] = 1
hence (SAT M) . [(n + i),A] = 1 by A2, XBOOLEAN:def_3; ::_thesis: verum
end;
suppose 0 < i ; ::_thesis: (SAT M) . [(n + b1),A] = 1
then ( not (SAT M) . [(n + i),('not' A)] = 1 or ex j being Element of NAT st
( 1 <= j & j < i & not (SAT M) . [(n + j),TVERUM] = 1 ) ) by A3, Def11, Th6;
then not (SAT M) . [(n + i),A] = 0 by Th5, Th6;
hence (SAT M) . [(n + i),A] = 1 by XBOOLEAN:def_3; ::_thesis: verum
end;
end;
end;
assume A4: for i being Element of NAT holds (SAT M) . [(n + i),A] = 1 ; ::_thesis: (SAT M) . [n,('G' A)] = 1
now__::_thesis:_not_(SAT_M)_._[n,('G'_A)]_=_0
assume (SAT M) . [n,('G' A)] = 0 ; ::_thesis: contradiction
then not (SAT M) . [n,(('not' A) 'or' (TVERUM '&&' (TVERUM 'Us' ('not' A))))] = 0 by Th5;
then A5: (SAT M) . [n,(('not' A) 'or' (TVERUM '&&' (TVERUM 'Us' ('not' A))))] = 1 by XBOOLEAN:def_3;
percases ( (SAT M) . [n,('not' A)] = 1 or (SAT M) . [n,(TVERUM '&&' (TVERUM 'Us' ('not' A)))] = 1 ) by A5, Th8;
suppose (SAT M) . [n,('not' A)] = 1 ; ::_thesis: contradiction
then (SAT M) . [(n + 0),A] = 0 by Th5;
hence contradiction by A4; ::_thesis: verum
end;
suppose (SAT M) . [n,(TVERUM '&&' (TVERUM 'Us' ('not' A)))] = 1 ; ::_thesis: contradiction
then (SAT M) . [n,(TVERUM 'Us' ('not' A))] = 1 by Th7;
then consider i being Element of NAT such that
0 < i and
A6: (SAT M) . [(n + i),('not' A)] = 1 and
for j being Element of NAT st 1 <= j & j < i holds
(SAT M) . [(n + j),TVERUM] = 1 by Def11;
(SAT M) . [(n + i),A] = 0 by A6, Th5;
hence contradiction by A4; ::_thesis: verum
end;
end;
end;
hence (SAT M) . [n,('G' A)] = 1 by XBOOLEAN:def_3; ::_thesis: verum
end;
theorem Th11: :: LTLAXIO1:11
for A being Element of LTLB_WFF
for n being Element of NAT
for M being LTLModel holds
( (SAT M) . [n,('F' A)] = 1 iff ex i being Element of NAT st (SAT M) . [(n + i),A] = 1 )
proof
let A be Element of LTLB_WFF ; ::_thesis: for n being Element of NAT
for M being LTLModel holds
( (SAT M) . [n,('F' A)] = 1 iff ex i being Element of NAT st (SAT M) . [(n + i),A] = 1 )
let n be Element of NAT ; ::_thesis: for M being LTLModel holds
( (SAT M) . [n,('F' A)] = 1 iff ex i being Element of NAT st (SAT M) . [(n + i),A] = 1 )
let M be LTLModel; ::_thesis: ( (SAT M) . [n,('F' A)] = 1 iff ex i being Element of NAT st (SAT M) . [(n + i),A] = 1 )
hereby ::_thesis: ( ex i being Element of NAT st (SAT M) . [(n + i),A] = 1 implies (SAT M) . [n,('F' A)] = 1 )
assume (SAT M) . [n,('F' A)] = 1 ; ::_thesis: ex i being Element of NAT st (SAT M) . [(n + i),A] = 1
then (SAT M) . [n,('G' ('not' A))] = 0 by Th5;
then consider i being Element of NAT such that
A1: not (SAT M) . [(n + i),('not' A)] = 1 by Th10;
not (SAT M) . [(n + i),A] = 0 by A1, Th5;
then (SAT M) . [(n + i),A] = 1 by XBOOLEAN:def_3;
hence ex i being Element of NAT st (SAT M) . [(n + i),A] = 1 ; ::_thesis: verum
end;
assume ex i being Element of NAT st (SAT M) . [(n + i),A] = 1 ; ::_thesis: (SAT M) . [n,('F' A)] = 1
then consider i being Element of NAT such that
A2: (SAT M) . [(n + i),A] = 1 ;
not (SAT M) . [(n + i),('not' A)] = 1 by A2, Th5;
then not (SAT M) . [n,('G' ('not' A))] = 1 by Th10;
then (SAT M) . [n,('G' ('not' A))] = 0 by XBOOLEAN:def_3;
hence (SAT M) . [n,('F' A)] = 1 by Th5; ::_thesis: verum
end;
theorem Th12: :: LTLAXIO1:12
for p, q being Element of LTLB_WFF
for n being Element of NAT
for M being LTLModel holds
( (SAT M) . [n,(p 'U' q)] = 1 iff ex i being Element of NAT st
( (SAT M) . [(n + i),q] = 1 & ( for j being Element of NAT st j < i holds
(SAT M) . [(n + j),p] = 1 ) ) )
proof
let p, q be Element of LTLB_WFF ; ::_thesis: for n being Element of NAT
for M being LTLModel holds
( (SAT M) . [n,(p 'U' q)] = 1 iff ex i being Element of NAT st
( (SAT M) . [(n + i),q] = 1 & ( for j being Element of NAT st j < i holds
(SAT M) . [(n + j),p] = 1 ) ) )
let n be Element of NAT ; ::_thesis: for M being LTLModel holds
( (SAT M) . [n,(p 'U' q)] = 1 iff ex i being Element of NAT st
( (SAT M) . [(n + i),q] = 1 & ( for j being Element of NAT st j < i holds
(SAT M) . [(n + j),p] = 1 ) ) )
let M be LTLModel; ::_thesis: ( (SAT M) . [n,(p 'U' q)] = 1 iff ex i being Element of NAT st
( (SAT M) . [(n + i),q] = 1 & ( for j being Element of NAT st j < i holds
(SAT M) . [(n + j),p] = 1 ) ) )
set sm = SAT M;
hereby ::_thesis: ( ex i being Element of NAT st
( (SAT M) . [(n + i),q] = 1 & ( for j being Element of NAT st j < i holds
(SAT M) . [(n + j),p] = 1 ) ) implies (SAT M) . [n,(p 'U' q)] = 1 )
assume A1: (SAT M) . [n,(p 'U' q)] = 1 ; ::_thesis: ex i being Element of NAT st
( (SAT M) . [(n + i),q] = 1 & ( for j being Element of NAT st j < i holds
(SAT M) . [(n + j),p] = 1 ) )
percases ( (SAT M) . [n,q] = 1 or (SAT M) . [n,(p '&&' (p 'Us' q))] = 1 ) by A1, Th8;
supposeA2: (SAT M) . [n,q] = 1 ; ::_thesis: ex i being Element of NAT st
( (SAT M) . [(n + i),q] = 1 & ( for j being Element of NAT st j < i holds
(SAT M) . [(n + j),p] = 1 ) )
A3: for j being Element of NAT st j < 0 holds
(SAT M) . [(n + j),p] = 1 ;
(SAT M) . [(n + 0),q] = 1 by A2;
hence ex i being Element of NAT st
( (SAT M) . [(n + i),q] = 1 & ( for j being Element of NAT st j < i holds
(SAT M) . [(n + j),p] = 1 ) ) by A3; ::_thesis: verum
end;
supposeA4: (SAT M) . [n,(p '&&' (p 'Us' q))] = 1 ; ::_thesis: ex i being Element of NAT st
( (SAT M) . [(n + i),q] = 1 & ( for j being Element of NAT st j < i holds
(SAT M) . [(n + j),p] = 1 ) )
then (SAT M) . [n,(p 'Us' q)] = 1 by Th7;
then consider i being Element of NAT such that
0 < i and
A5: (SAT M) . [(n + i),q] = 1 and
A6: for j being Element of NAT st 1 <= j & j < i holds
(SAT M) . [(n + j),p] = 1 by Def11;
now__::_thesis:_for_j_being_Element_of_NAT_st_j_<_i_holds_
(SAT_M)_._[(n_+_j),p]_=_1
let j be Element of NAT ; ::_thesis: ( j < i implies (SAT M) . [(n + b1),p] = 1 )
assume A7: j < i ; ::_thesis: (SAT M) . [(n + b1),p] = 1
percases ( j = 0 or not j = 0 ) ;
suppose j = 0 ; ::_thesis: (SAT M) . [(n + b1),p] = 1
hence (SAT M) . [(n + j),p] = 1 by A4, Th7; ::_thesis: verum
end;
suppose not j = 0 ; ::_thesis: (SAT M) . [(n + b1),p] = 1
then 1 <= j by NAT_1:25;
hence (SAT M) . [(n + j),p] = 1 by A6, A7; ::_thesis: verum
end;
end;
end;
hence ex i being Element of NAT st
( (SAT M) . [(n + i),q] = 1 & ( for j being Element of NAT st j < i holds
(SAT M) . [(n + j),p] = 1 ) ) by A5; ::_thesis: verum
end;
end;
end;
assume ex i being Element of NAT st
( (SAT M) . [(n + i),q] = 1 & ( for j being Element of NAT st j < i holds
(SAT M) . [(n + j),p] = 1 ) ) ; ::_thesis: (SAT M) . [n,(p 'U' q)] = 1
then consider i being Element of NAT such that
A8: (SAT M) . [(n + i),q] = 1 and
A9: for j being Element of NAT st j < i holds
(SAT M) . [(n + j),p] = 1 ;
percases ( i = 0 or not i = 0 ) ;
suppose i = 0 ; ::_thesis: (SAT M) . [n,(p 'U' q)] = 1
hence (SAT M) . [n,(p 'U' q)] = 1 by A8, Th8; ::_thesis: verum
end;
supposeA10: not i = 0 ; ::_thesis: (SAT M) . [n,(p 'U' q)] = 1
for j being Element of NAT st 1 <= j & j < i holds
(SAT M) . [(n + j),p] = 1 by A9;
then A11: (SAT M) . [n,(p 'Us' q)] = 1 by A8, A10, Def11;
(SAT M) . [(n + 0),p] = 1 by A9, A10;
then (SAT M) . [n,(p '&&' (p 'Us' q))] = 1 by A11, Th7;
hence (SAT M) . [n,(p 'U' q)] = 1 by Th8; ::_thesis: verum
end;
end;
end;
theorem :: LTLAXIO1:13
for p, q being Element of LTLB_WFF
for n being Element of NAT
for M being LTLModel holds
( (SAT M) . [n,(p 'R' q)] = 1 iff ( ex i being Element of NAT st
( (SAT M) . [(n + i),p] = 1 & ( for j being Element of NAT st j <= i holds
(SAT M) . [(n + j),q] = 1 ) ) or for i being Element of NAT holds (SAT M) . [(n + i),q] = 1 ) )
proof
let p, q be Element of LTLB_WFF ; ::_thesis: for n being Element of NAT
for M being LTLModel holds
( (SAT M) . [n,(p 'R' q)] = 1 iff ( ex i being Element of NAT st
( (SAT M) . [(n + i),p] = 1 & ( for j being Element of NAT st j <= i holds
(SAT M) . [(n + j),q] = 1 ) ) or for i being Element of NAT holds (SAT M) . [(n + i),q] = 1 ) )
let n be Element of NAT ; ::_thesis: for M being LTLModel holds
( (SAT M) . [n,(p 'R' q)] = 1 iff ( ex i being Element of NAT st
( (SAT M) . [(n + i),p] = 1 & ( for j being Element of NAT st j <= i holds
(SAT M) . [(n + j),q] = 1 ) ) or for i being Element of NAT holds (SAT M) . [(n + i),q] = 1 ) )
let M be LTLModel; ::_thesis: ( (SAT M) . [n,(p 'R' q)] = 1 iff ( ex i being Element of NAT st
( (SAT M) . [(n + i),p] = 1 & ( for j being Element of NAT st j <= i holds
(SAT M) . [(n + j),q] = 1 ) ) or for i being Element of NAT holds (SAT M) . [(n + i),q] = 1 ) )
set sm = SAT M;
set notp = 'not' p;
set notq = 'not' q;
thus ( not (SAT M) . [n,(p 'R' q)] = 1 or ex i being Element of NAT st
( (SAT M) . [(n + i),p] = 1 & ( for j being Element of NAT st j <= i holds
(SAT M) . [(n + j),q] = 1 ) ) or for i being Element of NAT holds (SAT M) . [(n + i),q] = 1 ) ::_thesis: ( ( ex i being Element of NAT st
( (SAT M) . [(n + i),p] = 1 & ( for j being Element of NAT st j <= i holds
(SAT M) . [(n + j),q] = 1 ) ) or for i being Element of NAT holds (SAT M) . [(n + i),q] = 1 ) implies (SAT M) . [n,(p 'R' q)] = 1 )
proof
defpred S1[ Nat] means ( (SAT M) . [(n + $1),q] = 1 & (SAT M) . [(n + $1),p] = 0 );
assume (SAT M) . [n,(p 'R' q)] = 1 ; ::_thesis: ( ex i being Element of NAT st
( (SAT M) . [(n + i),p] = 1 & ( for j being Element of NAT st j <= i holds
(SAT M) . [(n + j),q] = 1 ) ) or for i being Element of NAT holds (SAT M) . [(n + i),q] = 1 )
then A1: (SAT M) . [n,(('not' p) 'U' ('not' q))] = 0 by Th5;
A2: now__::_thesis:_for_i_being_Nat_holds_
(_not_(SAT_M)_._[(n_+_i),('not'_q)]_=_1_or_ex_j_being_Nat_st_
(_j_<_i_&_not_(SAT_M)_._[(n_+_j),('not'_p)]_=_1_)_)
let i be Nat; ::_thesis: ( not (SAT M) . [(n + b1),('not' q)] = 1 or ex j being Nat st
( b2 < j & not (SAT M) . [(n + b2),('not' p)] = 1 ) )
reconsider ii = i as Element of NAT by ORDINAL1:def_12;
percases ( not (SAT M) . [(n + ii),('not' q)] = 1 or ex j being Element of NAT st
( j < i & not (SAT M) . [(n + j),('not' p)] = 1 ) ) by A1, Th12;
suppose not (SAT M) . [(n + ii),('not' q)] = 1 ; ::_thesis: ( not (SAT M) . [(n + b1),('not' q)] = 1 or ex j being Nat st
( b2 < j & not (SAT M) . [(n + b2),('not' p)] = 1 ) )
hence ( not (SAT M) . [(n + i),('not' q)] = 1 or ex j being Nat st
( j < i & not (SAT M) . [(n + j),('not' p)] = 1 ) ) ; ::_thesis: verum
end;
suppose ex j being Element of NAT st
( j < i & not (SAT M) . [(n + j),('not' p)] = 1 ) ; ::_thesis: ( not (SAT M) . [(n + b1),('not' q)] = 1 or ex j being Nat st
( b2 < j & not (SAT M) . [(n + b2),('not' p)] = 1 ) )
hence ( not (SAT M) . [(n + i),('not' q)] = 1 or ex j being Nat st
( j < i & not (SAT M) . [(n + j),('not' p)] = 1 ) ) ; ::_thesis: verum
end;
end;
end;
assume that
A3: for i being Element of NAT holds
( not (SAT M) . [(n + i),p] = 1 or ex j being Element of NAT st
( j <= i & not (SAT M) . [(n + j),q] = 1 ) ) and
A4: not for i being Element of NAT holds (SAT M) . [(n + i),q] = 1 ; ::_thesis: contradiction
A5: now__::_thesis:_for_i_being_Nat_holds_
(_not_(SAT_M)_._[(n_+_i),p]_=_1_or_ex_j_being_Nat_st_
(_j_<=_i_&_not_(SAT_M)_._[(n_+_j),q]_=_1_)_)
let i be Nat; ::_thesis: ( not (SAT M) . [(n + i),p] = 1 or ex j being Nat st
( j <= i & not (SAT M) . [(n + j),q] = 1 ) )
reconsider ii = i as Element of NAT by ORDINAL1:def_12;
( not (SAT M) . [(n + ii),p] = 1 or ex j being Element of NAT st
( j <= ii & not (SAT M) . [(n + j),q] = 1 ) ) by A3;
hence ( not (SAT M) . [(n + i),p] = 1 or ex j being Nat st
( j <= i & not (SAT M) . [(n + j),q] = 1 ) ) ; ::_thesis: verum
end;
A6: for k being Nat st ( for m being Nat st m < k holds
S1[m] ) holds
S1[k]
proof
let k be Nat; ::_thesis: ( ( for m being Nat st m < k holds
S1[m] ) implies S1[k] )
assume A7: for m being Nat st m < k holds
S1[m] ; ::_thesis: S1[k]
now__::_thesis:_for_j_being_Nat_holds_
(_not_j_<_k_or_(SAT_M)_._[(n_+_j),('not'_p)]_=_1_)
assume ex j being Nat st
( j < k & not (SAT M) . [(n + j),('not' p)] = 1 ) ; ::_thesis: contradiction
then consider j being Nat such that
A8: j < k and
A9: not (SAT M) . [(n + j),('not' p)] = 1 ;
not (SAT M) . [(n + j),p] = 0 by A9, Th5;
hence contradiction by A7, A8; ::_thesis: verum
end;
then not (SAT M) . [(n + k),('not' q)] = 1 by A2;
then A10: not (SAT M) . [(n + k),q] = 0 by Th5;
then A11: (SAT M) . [(n + k),q] = 1 by XBOOLEAN:def_3;
now__::_thesis:_for_j_being_Nat_holds_
(_not_j_<=_k_or_(SAT_M)_._[(n_+_j),q]_=_1_)
assume ex j being Nat st
( j <= k & not (SAT M) . [(n + j),q] = 1 ) ; ::_thesis: contradiction
then consider j being Nat such that
A12: j <= k and
A13: not (SAT M) . [(n + j),q] = 1 ;
percases ( j < k or not j < k ) ;
suppose j < k ; ::_thesis: contradiction
hence contradiction by A7, A13; ::_thesis: verum
end;
suppose not j < k ; ::_thesis: contradiction
hence contradiction by A11, A12, A13, XXREAL_0:1; ::_thesis: verum
end;
end;
end;
then not (SAT M) . [(n + k),p] = 1 by A5;
hence S1[k] by A10, XBOOLEAN:def_3; ::_thesis: verum
end;
for i being Nat holds S1[i] from NAT_1:sch_4(A6);
hence contradiction by A4; ::_thesis: verum
end;
thus ( ( ex i being Element of NAT st
( (SAT M) . [(n + i),p] = 1 & ( for j being Element of NAT st j <= i holds
(SAT M) . [(n + j),q] = 1 ) ) or for i being Element of NAT holds (SAT M) . [(n + i),q] = 1 ) implies (SAT M) . [n,(p 'R' q)] = 1 ) ::_thesis: verum
proof
assume A14: ( ex i being Element of NAT st
( (SAT M) . [(n + i),p] = 1 & ( for j being Element of NAT st j <= i holds
(SAT M) . [(n + j),q] = 1 ) ) or for i being Element of NAT holds (SAT M) . [(n + i),q] = 1 ) ; ::_thesis: (SAT M) . [n,(p 'R' q)] = 1
assume not (SAT M) . [n,(p 'R' q)] = 1 ; ::_thesis: contradiction
then not (SAT M) . [n,(('not' p) 'U' ('not' q))] = 0 by Th5;
then A15: (SAT M) . [n,(('not' p) 'U' ('not' q))] = 1 by XBOOLEAN:def_3;
percases ( ex i being Element of NAT st
( (SAT M) . [(n + i),p] = 1 & ( for j being Element of NAT st j <= i holds
(SAT M) . [(n + j),q] = 1 ) ) or for i being Element of NAT holds (SAT M) . [(n + i),q] = 1 ) by A14;
suppose ex i being Element of NAT st
( (SAT M) . [(n + i),p] = 1 & ( for j being Element of NAT st j <= i holds
(SAT M) . [(n + j),q] = 1 ) ) ; ::_thesis: contradiction
then consider i being Element of NAT such that
A16: (SAT M) . [(n + i),p] = 1 and
A17: for j being Element of NAT st j <= i holds
(SAT M) . [(n + j),q] = 1 ;
consider k being Element of NAT such that
A18: (SAT M) . [(n + k),('not' q)] = 1 and
A19: for j being Element of NAT st j < k holds
(SAT M) . [(n + j),('not' p)] = 1 by A15, Th12;
percases ( k <= i or not k <= i ) ;
suppose k <= i ; ::_thesis: contradiction
then (SAT M) . [(n + k),q] = 1 by A17;
hence contradiction by A18, Th5; ::_thesis: verum
end;
suppose not k <= i ; ::_thesis: contradiction
then (SAT M) . [(n + i),('not' p)] = 1 by A19;
hence contradiction by A16, Th5; ::_thesis: verum
end;
end;
end;
supposeA20: for i being Element of NAT holds (SAT M) . [(n + i),q] = 1 ; ::_thesis: contradiction
consider i being Element of NAT such that
A21: (SAT M) . [(n + i),('not' q)] = 1 and
for j being Element of NAT st j < i holds
(SAT M) . [(n + j),('not' p)] = 1 by A15, Th12;
(SAT M) . [(n + i),q] = 0 by A21, Th5;
hence contradiction by A20; ::_thesis: verum
end;
end;
end;
end;
theorem Th14: :: LTLAXIO1:14
for B being Element of LTLB_WFF
for n being Element of NAT
for M being LTLModel holds (SAT M) . [n,('not' ('X' B))] = (SAT M) . [n,('X' ('not' B))]
proof
let B be Element of LTLB_WFF ; ::_thesis: for n being Element of NAT
for M being LTLModel holds (SAT M) . [n,('not' ('X' B))] = (SAT M) . [n,('X' ('not' B))]
let n be Element of NAT ; ::_thesis: for M being LTLModel holds (SAT M) . [n,('not' ('X' B))] = (SAT M) . [n,('X' ('not' B))]
let M be LTLModel; ::_thesis: (SAT M) . [n,('not' ('X' B))] = (SAT M) . [n,('X' ('not' B))]
thus (SAT M) . [n,('not' ('X' B))] = ((SAT M) . [n,('X' B)]) => ((SAT M) . [n,TFALSUM]) by Def11
.= ((SAT M) . [(n + 1),B]) => ((SAT M) . [n,TFALSUM]) by Th9
.= ((SAT M) . [(n + 1),B]) => FALSE by Def11
.= ((SAT M) . [(n + 1),B]) => ((SAT M) . [(n + 1),TFALSUM]) by Def11
.= (SAT M) . [(n + 1),(B => TFALSUM)] by Def11
.= (SAT M) . [n,('X' ('not' B))] by Th9 ; ::_thesis: verum
end;
theorem Th15: :: LTLAXIO1:15
for B being Element of LTLB_WFF
for n being Element of NAT
for M being LTLModel holds (SAT M) . [n,(('not' ('X' B)) => ('X' ('not' B)))] = 1
proof
let B be Element of LTLB_WFF ; ::_thesis: for n being Element of NAT
for M being LTLModel holds (SAT M) . [n,(('not' ('X' B)) => ('X' ('not' B)))] = 1
let n be Element of NAT ; ::_thesis: for M being LTLModel holds (SAT M) . [n,(('not' ('X' B)) => ('X' ('not' B)))] = 1
let M be LTLModel; ::_thesis: (SAT M) . [n,(('not' ('X' B)) => ('X' ('not' B)))] = 1
A1: ( (SAT M) . [n,('not' ('X' B))] = 0 or (SAT M) . [n,('not' ('X' B))] = 1 ) by XBOOLEAN:def_3;
thus (SAT M) . [n,(('not' ('X' B)) => ('X' ('not' B)))] = ((SAT M) . [n,('not' ('X' B))]) => ((SAT M) . [n,('X' ('not' B))]) by Def11
.= 1 by A1, Th14 ; ::_thesis: verum
end;
theorem Th16: :: LTLAXIO1:16
for B being Element of LTLB_WFF
for n being Element of NAT
for M being LTLModel holds (SAT M) . [n,(('X' ('not' B)) => ('not' ('X' B)))] = 1
proof
let B be Element of LTLB_WFF ; ::_thesis: for n being Element of NAT
for M being LTLModel holds (SAT M) . [n,(('X' ('not' B)) => ('not' ('X' B)))] = 1
let n be Element of NAT ; ::_thesis: for M being LTLModel holds (SAT M) . [n,(('X' ('not' B)) => ('not' ('X' B)))] = 1
let M be LTLModel; ::_thesis: (SAT M) . [n,(('X' ('not' B)) => ('not' ('X' B)))] = 1
A1: ( (SAT M) . [n,('not' ('X' B))] = 0 or (SAT M) . [n,('not' ('X' B))] = 1 ) by XBOOLEAN:def_3;
thus (SAT M) . [n,(('X' ('not' B)) => ('not' ('X' B)))] = ((SAT M) . [n,('X' ('not' B))]) => ((SAT M) . [n,('not' ('X' B))]) by Def11
.= 1 by A1, Th14 ; ::_thesis: verum
end;
theorem Th17: :: LTLAXIO1:17
for B, C being Element of LTLB_WFF
for n being Element of NAT
for M being LTLModel holds (SAT M) . [n,(('X' (B => C)) => (('X' B) => ('X' C)))] = 1
proof
let B, C be Element of LTLB_WFF ; ::_thesis: for n being Element of NAT
for M being LTLModel holds (SAT M) . [n,(('X' (B => C)) => (('X' B) => ('X' C)))] = 1
let n be Element of NAT ; ::_thesis: for M being LTLModel holds (SAT M) . [n,(('X' (B => C)) => (('X' B) => ('X' C)))] = 1
let M be LTLModel; ::_thesis: (SAT M) . [n,(('X' (B => C)) => (('X' B) => ('X' C)))] = 1
A1: ( (SAT M) . [(n + 1),B] = 0 or (SAT M) . [(n + 1),B] = 1 ) by XBOOLEAN:def_3;
A2: ( (SAT M) . [(n + 1),C] = 0 or (SAT M) . [(n + 1),C] = 1 ) by XBOOLEAN:def_3;
thus (SAT M) . [n,(('X' (B => C)) => (('X' B) => ('X' C)))] = ((SAT M) . [n,('X' (B => C))]) => ((SAT M) . [n,(('X' B) => ('X' C))]) by Def11
.= ((SAT M) . [(n + 1),(B => C)]) => ((SAT M) . [n,(('X' B) => ('X' C))]) by Th9
.= ((SAT M) . [(n + 1),(B => C)]) => (((SAT M) . [n,('X' B)]) => ((SAT M) . [n,('X' C)])) by Def11
.= ((SAT M) . [(n + 1),(B => C)]) => (((SAT M) . [(n + 1),B]) => ((SAT M) . [n,('X' C)])) by Th9
.= ((SAT M) . [(n + 1),(B => C)]) => (((SAT M) . [(n + 1),B]) => ((SAT M) . [(n + 1),C])) by Th9
.= 1 by A1, A2, Def11 ; ::_thesis: verum
end;
theorem Th18: :: LTLAXIO1:18
for B being Element of LTLB_WFF
for n being Element of NAT
for M being LTLModel holds (SAT M) . [n,(('G' B) => (B '&&' ('X' ('G' B))))] = 1
proof
let B be Element of LTLB_WFF ; ::_thesis: for n being Element of NAT
for M being LTLModel holds (SAT M) . [n,(('G' B) => (B '&&' ('X' ('G' B))))] = 1
let n be Element of NAT ; ::_thesis: for M being LTLModel holds (SAT M) . [n,(('G' B) => (B '&&' ('X' ('G' B))))] = 1
let M be LTLModel; ::_thesis: (SAT M) . [n,(('G' B) => (B '&&' ('X' ('G' B))))] = 1
A1: (SAT M) . [n,(('G' B) => (B '&&' ('X' ('G' B))))] = ((SAT M) . [n,('G' B)]) => ((SAT M) . [n,(B '&&' ('X' ('G' B)))]) by Def11;
percases ( (SAT M) . [n,('G' B)] = 0 or (SAT M) . [n,('G' B)] = 1 ) by XBOOLEAN:def_3;
suppose (SAT M) . [n,('G' B)] = 0 ; ::_thesis: (SAT M) . [n,(('G' B) => (B '&&' ('X' ('G' B))))] = 1
hence (SAT M) . [n,(('G' B) => (B '&&' ('X' ('G' B))))] = 1 by A1; ::_thesis: verum
end;
supposeA2: (SAT M) . [n,('G' B)] = 1 ; ::_thesis: (SAT M) . [n,(('G' B) => (B '&&' ('X' ('G' B))))] = 1
now__::_thesis:_for_i_being_Element_of_NAT_holds_(SAT_M)_._[((n_+_1)_+_i),B]_=_1
let i be Element of NAT ; ::_thesis: (SAT M) . [((n + 1) + i),B] = 1
(SAT M) . [(n + (i + 1)),B] = 1 by A2, Th10;
hence (SAT M) . [((n + 1) + i),B] = 1 ; ::_thesis: verum
end;
then (SAT M) . [(n + 1),('G' B)] = 1 by Th10;
then A3: (SAT M) . [n,('X' ('G' B))] = 1 by Th9;
(SAT M) . [(n + 0),B] = 1 by A2, Th10;
then (SAT M) . [n,(B '&&' ('X' ('G' B)))] = 1 by A3, Th7;
hence (SAT M) . [n,(('G' B) => (B '&&' ('X' ('G' B))))] = 1 by A1; ::_thesis: verum
end;
end;
end;
theorem Th19: :: LTLAXIO1:19
for B, C being Element of LTLB_WFF
for n being Element of NAT
for M being LTLModel holds (SAT M) . [n,((B 'Us' C) => (('X' C) 'or' ('X' (B '&&' (B 'Us' C)))))] = 1
proof
let B, C be Element of LTLB_WFF ; ::_thesis: for n being Element of NAT
for M being LTLModel holds (SAT M) . [n,((B 'Us' C) => (('X' C) 'or' ('X' (B '&&' (B 'Us' C)))))] = 1
let n be Element of NAT ; ::_thesis: for M being LTLModel holds (SAT M) . [n,((B 'Us' C) => (('X' C) 'or' ('X' (B '&&' (B 'Us' C)))))] = 1
let M be LTLModel; ::_thesis: (SAT M) . [n,((B 'Us' C) => (('X' C) 'or' ('X' (B '&&' (B 'Us' C)))))] = 1
set sm = SAT M;
A1: now__::_thesis:_(_(SAT_M)_._[n,(('X'_C)_'or'_('X'_(B_'&&'_(B_'Us'_C))))]_=_0_implies_not_(SAT_M)_._[n,(B_'Us'_C)]_=_1_)
assume that
A2: (SAT M) . [n,(('X' C) 'or' ('X' (B '&&' (B 'Us' C))))] = 0 and
A3: (SAT M) . [n,(B 'Us' C)] = 1 ; ::_thesis: contradiction
consider i being Element of NAT such that
A4: 0 < i and
A5: (SAT M) . [(n + i),C] = 1 and
A6: for j being Element of NAT st 1 <= j & j < i holds
(SAT M) . [(n + j),B] = 1 by A3, Def11;
A7: not (SAT M) . [n,('X' C)] = 1 by A2, Th8;
not (SAT M) . [n,('X' (B '&&' (B 'Us' C)))] = 1 by A2, Th8;
then (SAT M) . [n,('X' (B '&&' (B 'Us' C)))] = 0 by XBOOLEAN:def_3;
then A8: (SAT M) . [(n + 1),(B '&&' (B 'Us' C))] = 0 by Th9;
percases ( i = 1 or i > 1 ) by A4, NAT_1:25;
suppose i = 1 ; ::_thesis: contradiction
hence contradiction by A5, A7, Th9; ::_thesis: verum
end;
supposeA9: i > 1 ; ::_thesis: contradiction
A10: now__::_thesis:_for_j_being_Element_of_NAT_st_1_<=_j_&_j_<_i_-'_1_holds_
(SAT_M)_._[((n_+_1)_+_j),B]_=_1
let j be Element of NAT ; ::_thesis: ( 1 <= j & j < i -' 1 implies (SAT M) . [((n + 1) + j),B] = 1 )
assume that
A11: 1 <= j and
A12: j < i -' 1 ; ::_thesis: (SAT M) . [((n + 1) + j),B] = 1
j + 1 < (i -' 1) + 1 by A12, XREAL_1:8;
then A13: j + 1 < (i - 1) + 1 by A12, XREAL_0:def_2;
1 <= j + 1 by A11, NAT_1:19;
then (SAT M) . [(n + (j + 1)),B] = 1 by A6, A13;
hence (SAT M) . [((n + 1) + j),B] = 1 ; ::_thesis: verum
end;
A14: ( not (SAT M) . [(n + 1),B] = 1 or not (SAT M) . [(n + 1),(B 'Us' C)] = 1 ) by A8, Th7;
A15: i + (- 1) > 1 + (- 1) by A9, XREAL_1:8;
n + i = (n + 1) + (i - 1)
.= (n + 1) + (i -' 1) by A15, XREAL_0:def_2 ;
hence contradiction by A5, A6, A9, A15, A10, A14, Def11; ::_thesis: verum
end;
end;
end;
( (SAT M) . [n,(('X' C) 'or' ('X' (B '&&' (B 'Us' C))))] = 0 or (SAT M) . [n,(('X' C) 'or' ('X' (B '&&' (B 'Us' C))))] = 1 ) by XBOOLEAN:def_3;
then ((SAT M) . [n,(B 'Us' C)]) => ((SAT M) . [n,(('X' C) 'or' ('X' (B '&&' (B 'Us' C))))]) = 1 by A1, XBOOLEAN:def_3;
hence (SAT M) . [n,((B 'Us' C) => (('X' C) 'or' ('X' (B '&&' (B 'Us' C)))))] = 1 by Def11; ::_thesis: verum
end;
theorem Th20: :: LTLAXIO1:20
for C, B being Element of LTLB_WFF
for n being Element of NAT
for M being LTLModel holds (SAT M) . [n,((('X' C) 'or' ('X' (B '&&' (B 'Us' C)))) => (B 'Us' C))] = 1
proof
let C, B be Element of LTLB_WFF ; ::_thesis: for n being Element of NAT
for M being LTLModel holds (SAT M) . [n,((('X' C) 'or' ('X' (B '&&' (B 'Us' C)))) => (B 'Us' C))] = 1
let n be Element of NAT ; ::_thesis: for M being LTLModel holds (SAT M) . [n,((('X' C) 'or' ('X' (B '&&' (B 'Us' C)))) => (B 'Us' C))] = 1
let M be LTLModel; ::_thesis: (SAT M) . [n,((('X' C) 'or' ('X' (B '&&' (B 'Us' C)))) => (B 'Us' C))] = 1
set sm = SAT M;
A1: now__::_thesis:_(_(SAT_M)_._[n,(('X'_C)_'or'_('X'_(B_'&&'_(B_'Us'_C))))]_=_1_implies_not_(SAT_M)_._[n,(B_'Us'_C)]_=_0_)
assume that
A2: (SAT M) . [n,(('X' C) 'or' ('X' (B '&&' (B 'Us' C))))] = 1 and
A3: (SAT M) . [n,(B 'Us' C)] = 0 ; ::_thesis: contradiction
percases ( (SAT M) . [n,('X' C)] = 1 or (SAT M) . [n,('X' (B '&&' (B 'Us' C)))] = 1 ) by A2, Th8;
supposeA4: (SAT M) . [n,('X' C)] = 1 ; ::_thesis: contradiction
A5: for j being Element of NAT st 1 <= j & j < 1 holds
(SAT M) . [(n + j),B] = 1 ;
(SAT M) . [(n + 1),C] = 1 by A4, Th9;
hence contradiction by A3, A5, Def11; ::_thesis: verum
end;
suppose (SAT M) . [n,('X' (B '&&' (B 'Us' C)))] = 1 ; ::_thesis: contradiction
then A6: (SAT M) . [(n + 1),(B '&&' (B 'Us' C))] = 1 by Th9;
then (SAT M) . [(n + 1),(B 'Us' C)] = 1 by Th7;
then consider i being Element of NAT such that
i > 0 and
A7: (SAT M) . [((n + 1) + i),C] = 1 and
A8: for j being Element of NAT st 1 <= j & j < i holds
(SAT M) . [((n + 1) + j),B] = 1 by Def11;
A9: now__::_thesis:_for_j_being_Element_of_NAT_st_1_<=_j_&_j_<_1_+_i_holds_
(SAT_M)_._[(n_+_j),B]_=_1
let j be Element of NAT ; ::_thesis: ( 1 <= j & j < 1 + i implies (SAT M) . [(n + b1),B] = 1 )
assume A10: ( 1 <= j & j < 1 + i ) ; ::_thesis: (SAT M) . [(n + b1),B] = 1
percases ( 1 = j or ( 1 < j & j < i + 1 ) ) by A10, NAT_1:25;
suppose 1 = j ; ::_thesis: (SAT M) . [(n + b1),B] = 1
hence (SAT M) . [(n + j),B] = 1 by A6, Th7; ::_thesis: verum
end;
supposeA11: ( 1 < j & j < i + 1 ) ; ::_thesis: (SAT M) . [(n + b1),B] = 1
then A12: 1 + (- 1) < j + (- 1) by XREAL_1:8;
then j - 1 > 0 ;
then j -' 1 > 0 by XREAL_0:def_2;
then A13: 1 <= j -' 1 by NAT_1:25;
A14: ((n + j) + 1) - 1 = (n + 1) + (j - 1)
.= (n + 1) + (j -' 1) by A12, XREAL_0:def_2 ;
j + (- 1) < (i + 1) + (- 1) by A11, XREAL_1:8;
hence (SAT M) . [(n + j),B] = 1 by A8, A14, A13; ::_thesis: verum
end;
end;
end;
(SAT M) . [(n + (1 + i)),C] = 1 by A7;
hence contradiction by A3, A9, Def11; ::_thesis: verum
end;
end;
end;
( (SAT M) . [n,(('X' C) 'or' ('X' (B '&&' (B 'Us' C))))] = 0 or (SAT M) . [n,(('X' C) 'or' ('X' (B '&&' (B 'Us' C))))] = 1 ) by XBOOLEAN:def_3;
then ((SAT M) . [n,(('X' C) 'or' ('X' (B '&&' (B 'Us' C))))]) => ((SAT M) . [n,(B 'Us' C)]) = 1 by A1, XBOOLEAN:def_3;
hence (SAT M) . [n,((('X' C) 'or' ('X' (B '&&' (B 'Us' C)))) => (B 'Us' C))] = 1 by Def11; ::_thesis: verum
end;
theorem Th21: :: LTLAXIO1:21
for B, C being Element of LTLB_WFF
for n being Element of NAT
for M being LTLModel holds (SAT M) . [n,((B 'Us' C) => ('X' ('F' C)))] = 1
proof
let B, C be Element of LTLB_WFF ; ::_thesis: for n being Element of NAT
for M being LTLModel holds (SAT M) . [n,((B 'Us' C) => ('X' ('F' C)))] = 1
let n be Element of NAT ; ::_thesis: for M being LTLModel holds (SAT M) . [n,((B 'Us' C) => ('X' ('F' C)))] = 1
let M be LTLModel; ::_thesis: (SAT M) . [n,((B 'Us' C) => ('X' ('F' C)))] = 1
set sm = SAT M;
A1: now__::_thesis:_(_(SAT_M)_._[n,(B_'Us'_C)]_=_1_implies_not_(SAT_M)_._[n,('X'_('F'_C))]_=_0_)
assume that
A2: (SAT M) . [n,(B 'Us' C)] = 1 and
A3: (SAT M) . [n,('X' ('F' C))] = 0 ; ::_thesis: contradiction
consider i being Element of NAT such that
A4: 0 < i and
A5: (SAT M) . [(n + i),C] = 1 and
for j being Element of NAT st 1 <= j & j < i holds
(SAT M) . [(n + j),B] = 1 by A2, Def11;
i >= 1 by A4, NAT_1:25;
then i + (- 1) >= 1 + (- 1) by XREAL_1:6;
then A6: (n + 1) + (i -' 1) = (n + 1) + (i - 1) by XREAL_0:def_2
.= n + i ;
(SAT M) . [(n + 1),('F' C)] = 0 by A3, Th9;
hence contradiction by A5, A6, Th11; ::_thesis: verum
end;
( (SAT M) . [n,(B 'Us' C)] = 0 or (SAT M) . [n,(B 'Us' C)] = 1 ) by XBOOLEAN:def_3;
then ((SAT M) . [n,(B 'Us' C)]) => ((SAT M) . [n,('X' ('F' C))]) = 1 by A1, XBOOLEAN:def_3;
hence (SAT M) . [n,((B 'Us' C) => ('X' ('F' C)))] = 1 by Def11; ::_thesis: verum
end;
begin
definition
let M be LTLModel;
let p be Element of LTLB_WFF ;
predM |= p means :Def12: :: LTLAXIO1:def 12
for n being Element of NAT holds (SAT M) . [n,p] = 1;
end;
:: deftheorem Def12 defines |= LTLAXIO1:def_12_:_
for M being LTLModel
for p being Element of LTLB_WFF holds
( M |= p iff for n being Element of NAT holds (SAT M) . [n,p] = 1 );
definition
let M be LTLModel;
let F be Subset of LTLB_WFF;
predM |= F means :Def13: :: LTLAXIO1:def 13
for p being Element of LTLB_WFF st p in F holds
M |= p;
end;
:: deftheorem Def13 defines |= LTLAXIO1:def_13_:_
for M being LTLModel
for F being Subset of LTLB_WFF holds
( M |= F iff for p being Element of LTLB_WFF st p in F holds
M |= p );
definition
let F be Subset of LTLB_WFF;
let p be Element of LTLB_WFF ;
predF |= p means :Def14: :: LTLAXIO1:def 14
for M being LTLModel st M |= F holds
M |= p;
end;
:: deftheorem Def14 defines |= LTLAXIO1:def_14_:_
for F being Subset of LTLB_WFF
for p being Element of LTLB_WFF holds
( F |= p iff for M being LTLModel st M |= F holds
M |= p );
theorem Th22: :: LTLAXIO1:22
for F, G being Subset of LTLB_WFF
for M being LTLModel holds
( ( M |= F & M |= G ) iff M |= F \/ G )
proof
let F, G be Subset of LTLB_WFF; ::_thesis: for M being LTLModel holds
( ( M |= F & M |= G ) iff M |= F \/ G )
let M be LTLModel; ::_thesis: ( ( M |= F & M |= G ) iff M |= F \/ G )
hereby ::_thesis: ( M |= F \/ G implies ( M |= F & M |= G ) )
assume A1: ( M |= F & M |= G ) ; ::_thesis: M |= F \/ G
thus M |= F \/ G ::_thesis: verum
proof
let p be Element of LTLB_WFF ; :: according to LTLAXIO1:def_13 ::_thesis: ( p in F \/ G implies M |= p )
assume p in F \/ G ; ::_thesis: M |= p
then ( p in F or p in G ) by XBOOLE_0:def_3;
hence M |= p by A1, Def13; ::_thesis: verum
end;
end;
assume A2: M |= F \/ G ; ::_thesis: ( M |= F & M |= G )
thus M |= F ::_thesis: M |= G
proof
let p be Element of LTLB_WFF ; :: according to LTLAXIO1:def_13 ::_thesis: ( p in F implies M |= p )
assume p in F ; ::_thesis: M |= p
then p in F \/ G by XBOOLE_0:def_3;
hence M |= p by A2, Def13; ::_thesis: verum
end;
thus M |= G ::_thesis: verum
proof
let p be Element of LTLB_WFF ; :: according to LTLAXIO1:def_13 ::_thesis: ( p in G implies M |= p )
assume p in G ; ::_thesis: M |= p
then p in F \/ G by XBOOLE_0:def_3;
hence M |= p by A2, Def13; ::_thesis: verum
end;
end;
theorem Th23: :: LTLAXIO1:23
for A being Element of LTLB_WFF
for M being LTLModel holds
( M |= A iff M |= {A} )
proof
let A be Element of LTLB_WFF ; ::_thesis: for M being LTLModel holds
( M |= A iff M |= {A} )
let M be LTLModel; ::_thesis: ( M |= A iff M |= {A} )
hereby ::_thesis: ( M |= {A} implies M |= A )
assume A1: M |= A ; ::_thesis: M |= {A}
thus M |= {A} ::_thesis: verum
proof
let p be Element of LTLB_WFF ; :: according to LTLAXIO1:def_13 ::_thesis: ( p in {A} implies M |= p )
assume p in {A} ; ::_thesis: M |= p
hence M |= p by A1, TARSKI:def_1; ::_thesis: verum
end;
end;
A2: A in {A} by TARSKI:def_1;
assume M |= {A} ; ::_thesis: M |= A
hence M |= A by A2, Def13; ::_thesis: verum
end;
theorem Th24: :: LTLAXIO1:24
for A, B being Element of LTLB_WFF
for F being Subset of LTLB_WFF st F |= A & F |= A => B holds
F |= B
proof
let A, B be Element of LTLB_WFF ; ::_thesis: for F being Subset of LTLB_WFF st F |= A & F |= A => B holds
F |= B
let F be Subset of LTLB_WFF; ::_thesis: ( F |= A & F |= A => B implies F |= B )
assume that
A1: F |= A and
A2: F |= A => B ; ::_thesis: F |= B
let M be LTLModel; :: according to LTLAXIO1:def_14 ::_thesis: ( M |= F implies M |= B )
assume A3: M |= F ; ::_thesis: M |= B
let n be Element of NAT ; :: according to LTLAXIO1:def_12 ::_thesis: (SAT M) . [n,B] = 1
M |= A => B by A2, A3, Def14;
then (SAT M) . [n,(A => B)] = 1 by Def12;
then A4: ((SAT M) . [n,A]) => ((SAT M) . [n,B]) = 1 by Def11;
M |= A by A1, A3, Def14;
then (SAT M) . [n,A] = 1 by Def12;
hence (SAT M) . [n,B] = 1 by A4; ::_thesis: verum
end;
theorem Th25: :: LTLAXIO1:25
for A being Element of LTLB_WFF
for F being Subset of LTLB_WFF st F |= A holds
F |= 'X' A
proof
let A be Element of LTLB_WFF ; ::_thesis: for F being Subset of LTLB_WFF st F |= A holds
F |= 'X' A
let F be Subset of LTLB_WFF; ::_thesis: ( F |= A implies F |= 'X' A )
assume A1: F |= A ; ::_thesis: F |= 'X' A
let M be LTLModel; :: according to LTLAXIO1:def_14 ::_thesis: ( M |= F implies M |= 'X' A )
assume M |= F ; ::_thesis: M |= 'X' A
then A2: M |= A by A1, Def14;
let n be Element of NAT ; :: according to LTLAXIO1:def_12 ::_thesis: (SAT M) . [n,('X' A)] = 1
thus (SAT M) . [n,('X' A)] = (SAT M) . [(n + 1),A] by Th9
.= 1 by A2, Def12 ; ::_thesis: verum
end;
theorem :: LTLAXIO1:26
for A being Element of LTLB_WFF
for F being Subset of LTLB_WFF st F |= A holds
F |= 'G' A
proof
let A be Element of LTLB_WFF ; ::_thesis: for F being Subset of LTLB_WFF st F |= A holds
F |= 'G' A
let F be Subset of LTLB_WFF; ::_thesis: ( F |= A implies F |= 'G' A )
assume A1: F |= A ; ::_thesis: F |= 'G' A
let M be LTLModel; :: according to LTLAXIO1:def_14 ::_thesis: ( M |= F implies M |= 'G' A )
assume A2: M |= F ; ::_thesis: M |= 'G' A
let n be Element of NAT ; :: according to LTLAXIO1:def_12 ::_thesis: (SAT M) . [n,('G' A)] = 1
M |= A by A1, A2, Def14;
then for i being Element of NAT holds (SAT M) . [(n + i),A] = 1 by Def12;
hence (SAT M) . [n,('G' A)] = 1 by Th10; ::_thesis: verum
end;
theorem Th27: :: LTLAXIO1:27
for A, B being Element of LTLB_WFF
for F being Subset of LTLB_WFF st F |= A => B & F |= A => ('X' A) holds
F |= A => ('G' B)
proof
let A, B be Element of LTLB_WFF ; ::_thesis: for F being Subset of LTLB_WFF st F |= A => B & F |= A => ('X' A) holds
F |= A => ('G' B)
let F be Subset of LTLB_WFF; ::_thesis: ( F |= A => B & F |= A => ('X' A) implies F |= A => ('G' B) )
assume that
A1: F |= A => B and
A2: F |= A => ('X' A) ; ::_thesis: F |= A => ('G' B)
let M be LTLModel; :: according to LTLAXIO1:def_14 ::_thesis: ( M |= F implies M |= A => ('G' B) )
assume A3: M |= F ; ::_thesis: M |= A => ('G' B)
then A4: M |= A => B by A1, Def14;
A5: M |= A => ('X' A) by A2, A3, Def14;
let n be Element of NAT ; :: according to LTLAXIO1:def_12 ::_thesis: (SAT M) . [n,(A => ('G' B))] = 1
defpred S1[ Nat] means (SAT M) . [(n + $1),A] = 1;
percases ( (SAT M) . [n,A] = 1 or (SAT M) . [n,A] = 0 ) by XBOOLEAN:def_3;
supposeA6: (SAT M) . [n,A] = 1 ; ::_thesis: (SAT M) . [n,(A => ('G' B))] = 1
A7: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A8: S1[k] ; ::_thesis: S1[k + 1]
(SAT M) . [(n + k),(A => ('X' A))] = 1 by A5, Def12;
then ((SAT M) . [(n + k),A]) => ((SAT M) . [(n + k),('X' A)]) = 1 by Def11;
then (SAT M) . [((n + k) + 1),A] = 1 by A8, Th9;
hence S1[k + 1] ; ::_thesis: verum
end;
A9: S1[ 0 ] by A6;
A10: for i being Element of NAT holds S1[i] from NAT_1:sch_1(A9, A7);
now__::_thesis:_for_i_being_Element_of_NAT_holds_(SAT_M)_._[(n_+_i),B]_=_1
let i be Element of NAT ; ::_thesis: (SAT M) . [(n + i),B] = 1
(SAT M) . [(n + i),(A => B)] = 1 by A4, Def12;
then A11: ((SAT M) . [(n + i),A]) => ((SAT M) . [(n + i),B]) = 1 by Def11;
(SAT M) . [(n + i),A] = 1 by A10;
hence (SAT M) . [(n + i),B] = 1 by A11; ::_thesis: verum
end;
then (SAT M) . [n,('G' B)] = 1 by Th10;
then ((SAT M) . [n,A]) => ((SAT M) . [n,('G' B)]) = 1 ;
hence (SAT M) . [n,(A => ('G' B))] = 1 by Def11; ::_thesis: verum
end;
suppose (SAT M) . [n,A] = 0 ; ::_thesis: (SAT M) . [n,(A => ('G' B))] = 1
then ((SAT M) . [n,A]) => ((SAT M) . [n,('G' B)]) = 1 ;
hence (SAT M) . [n,(A => ('G' B))] = 1 by Def11; ::_thesis: verum
end;
end;
end;
theorem Th28: :: LTLAXIO1:28
for A being Element of LTLB_WFF
for i, j being Element of NAT
for M being LTLModel holds (SAT (M ^\ i)) . [j,A] = (SAT M) . [(i + j),A]
proof
let A be Element of LTLB_WFF ; ::_thesis: for i, j being Element of NAT
for M being LTLModel holds (SAT (M ^\ i)) . [j,A] = (SAT M) . [(i + j),A]
let i, j be Element of NAT ; ::_thesis: for M being LTLModel holds (SAT (M ^\ i)) . [j,A] = (SAT M) . [(i + j),A]
let M be LTLModel; ::_thesis: (SAT (M ^\ i)) . [j,A] = (SAT M) . [(i + j),A]
defpred S1[ Element of LTLB_WFF ] means for k being Element of NAT holds (SAT (M ^\ i)) . [k,$1] = (SAT M) . [(i + k),$1];
A1: for n being Element of NAT holds S1[ prop n]
proof
let n, k be Element of NAT ; ::_thesis: (SAT (M ^\ i)) . [k,(prop n)] = (SAT M) . [(i + k),(prop n)]
percases ( prop n in (M ^\ i) . k or not prop n in (M ^\ i) . k ) ;
supposeA2: prop n in (M ^\ i) . k ; ::_thesis: (SAT (M ^\ i)) . [k,(prop n)] = (SAT M) . [(i + k),(prop n)]
then A3: prop n in M . (i + k) by NAT_1:def_3;
thus (SAT (M ^\ i)) . [k,(prop n)] = 1 by A2, Def11
.= (SAT M) . [(i + k),(prop n)] by A3, Def11 ; ::_thesis: verum
end;
supposeA4: not prop n in (M ^\ i) . k ; ::_thesis: (SAT (M ^\ i)) . [k,(prop n)] = (SAT M) . [(i + k),(prop n)]
then not prop n in M . (i + k) by NAT_1:def_3;
then A5: not (SAT M) . [(i + k),(prop n)] = 1 by Def11;
not (SAT (M ^\ i)) . [k,(prop n)] = 1 by A4, Def11;
hence (SAT (M ^\ i)) . [k,(prop n)] = 0 by XBOOLEAN:def_3
.= (SAT M) . [(i + k),(prop n)] by A5, XBOOLEAN:def_3 ;
::_thesis: verum
end;
end;
end;
A6: for r, s being Element of LTLB_WFF st S1[r] & S1[s] holds
( S1[r 'Us' s] & S1[r => s] )
proof
let r, s be Element of LTLB_WFF ; ::_thesis: ( S1[r] & S1[s] implies ( S1[r 'Us' s] & S1[r => s] ) )
assume that
A7: S1[r] and
A8: S1[s] ; ::_thesis: ( S1[r 'Us' s] & S1[r => s] )
thus S1[r 'Us' s] ::_thesis: S1[r => s]
proof
let k be Element of NAT ; ::_thesis: (SAT (M ^\ i)) . [k,(r 'Us' s)] = (SAT M) . [(i + k),(r 'Us' s)]
A9: ( (SAT (M ^\ i)) . [k,(r 'Us' s)] = 1 iff (SAT M) . [(i + k),(r 'Us' s)] = 1 )
proof
hereby ::_thesis: ( (SAT M) . [(i + k),(r 'Us' s)] = 1 implies (SAT (M ^\ i)) . [k,(r 'Us' s)] = 1 )
assume (SAT (M ^\ i)) . [k,(r 'Us' s)] = 1 ; ::_thesis: (SAT M) . [(i + k),(r 'Us' s)] = 1
then consider m being Element of NAT such that
A10: 0 < m and
A11: (SAT (M ^\ i)) . [(k + m),s] = 1 and
A12: for j being Element of NAT st 1 <= j & j < m holds
(SAT (M ^\ i)) . [(k + j),r] = 1 by Def11;
A13: now__::_thesis:_for_j_being_Element_of_NAT_st_1_<=_j_&_j_<_m_holds_
(SAT_M)_._[((i_+_k)_+_j),r]_=_1
let j be Element of NAT ; ::_thesis: ( 1 <= j & j < m implies (SAT M) . [((i + k) + j),r] = 1 )
assume ( 1 <= j & j < m ) ; ::_thesis: (SAT M) . [((i + k) + j),r] = 1
then (SAT (M ^\ i)) . [(k + j),r] = 1 by A12;
then (SAT M) . [(i + (k + j)),r] = 1 by A7;
hence (SAT M) . [((i + k) + j),r] = 1 ; ::_thesis: verum
end;
(SAT M) . [(i + (k + m)),s] = 1 by A8, A11;
then (SAT M) . [((i + k) + m),s] = 1 ;
hence (SAT M) . [(i + k),(r 'Us' s)] = 1 by A10, A13, Def11; ::_thesis: verum
end;
assume (SAT M) . [(i + k),(r 'Us' s)] = 1 ; ::_thesis: (SAT (M ^\ i)) . [k,(r 'Us' s)] = 1
then consider m being Element of NAT such that
A14: 0 < m and
A15: (SAT M) . [((i + k) + m),s] = 1 and
A16: for j being Element of NAT st 1 <= j & j < m holds
(SAT M) . [((i + k) + j),r] = 1 by Def11;
A17: now__::_thesis:_for_j_being_Element_of_NAT_st_1_<=_j_&_j_<_m_holds_
(SAT_(M_^\_i))_._[(k_+_j),r]_=_1
let j be Element of NAT ; ::_thesis: ( 1 <= j & j < m implies (SAT (M ^\ i)) . [(k + j),r] = 1 )
assume ( 1 <= j & j < m ) ; ::_thesis: (SAT (M ^\ i)) . [(k + j),r] = 1
then (SAT M) . [((i + k) + j),r] = 1 by A16;
then (SAT M) . [(i + (k + j)),r] = 1 ;
hence (SAT (M ^\ i)) . [(k + j),r] = 1 by A7; ::_thesis: verum
end;
(SAT M) . [(i + (k + m)),s] = 1 by A15;
then (SAT (M ^\ i)) . [(k + m),s] = 1 by A8;
hence (SAT (M ^\ i)) . [k,(r 'Us' s)] = 1 by A14, A17, Def11; ::_thesis: verum
end;
percases ( (SAT (M ^\ i)) . [k,(r 'Us' s)] = 1 or not (SAT (M ^\ i)) . [k,(r 'Us' s)] = 1 ) ;
suppose (SAT (M ^\ i)) . [k,(r 'Us' s)] = 1 ; ::_thesis: (SAT (M ^\ i)) . [k,(r 'Us' s)] = (SAT M) . [(i + k),(r 'Us' s)]
hence (SAT (M ^\ i)) . [k,(r 'Us' s)] = (SAT M) . [(i + k),(r 'Us' s)] by A9; ::_thesis: verum
end;
suppose not (SAT (M ^\ i)) . [k,(r 'Us' s)] = 1 ; ::_thesis: (SAT (M ^\ i)) . [k,(r 'Us' s)] = (SAT M) . [(i + k),(r 'Us' s)]
then (SAT (M ^\ i)) . [k,(r 'Us' s)] = 0 by XBOOLEAN:def_3;
hence (SAT (M ^\ i)) . [k,(r 'Us' s)] = (SAT M) . [(i + k),(r 'Us' s)] by A9, XBOOLEAN:def_3; ::_thesis: verum
end;
end;
end;
thus S1[r => s] ::_thesis: verum
proof
let k be Element of NAT ; ::_thesis: (SAT (M ^\ i)) . [k,(r => s)] = (SAT M) . [(i + k),(r => s)]
thus (SAT (M ^\ i)) . [k,(r => s)] = ((SAT (M ^\ i)) . [k,r]) => ((SAT (M ^\ i)) . [k,s]) by Def11
.= ((SAT M) . [(i + k),r]) => ((SAT (M ^\ i)) . [k,s]) by A7
.= ((SAT M) . [(i + k),r]) => ((SAT M) . [(i + k),s]) by A8
.= (SAT M) . [(i + k),(r => s)] by Def11 ; ::_thesis: verum
end;
end;
now__::_thesis:_for_k_being_Element_of_NAT_holds_(SAT_(M_^\_i))_._[k,TFALSUM]_=_(SAT_M)_._[(i_+_k),TFALSUM]
let k be Element of NAT ; ::_thesis: (SAT (M ^\ i)) . [k,TFALSUM] = (SAT M) . [(i + k),TFALSUM]
thus (SAT (M ^\ i)) . [k,TFALSUM] = 0 by Def11
.= (SAT M) . [(i + k),TFALSUM] by Def11 ; ::_thesis: verum
end;
then A18: S1[ TFALSUM ] ;
for r being Element of LTLB_WFF holds S1[r] from HILBERT2:sch_2(A18, A1, A6);
hence (SAT (M ^\ i)) . [j,A] = (SAT M) . [(i + j),A] ; ::_thesis: verum
end;
theorem Th29: :: LTLAXIO1:29
for F being Subset of LTLB_WFF
for i being Element of NAT
for M being LTLModel st M |= F holds
M ^\ i |= F
proof
let F be Subset of LTLB_WFF; ::_thesis: for i being Element of NAT
for M being LTLModel st M |= F holds
M ^\ i |= F
let i be Element of NAT ; ::_thesis: for M being LTLModel st M |= F holds
M ^\ i |= F
let M be LTLModel; ::_thesis: ( M |= F implies M ^\ i |= F )
assume A1: M |= F ; ::_thesis: M ^\ i |= F
thus M ^\ i |= F ::_thesis: verum
proof
let p be Element of LTLB_WFF ; :: according to LTLAXIO1:def_13 ::_thesis: ( p in F implies M ^\ i |= p )
assume p in F ; ::_thesis: M ^\ i |= p
then A2: M |= p by A1, Def13;
thus M ^\ i |= p ::_thesis: verum
proof
let n be Element of NAT ; :: according to LTLAXIO1:def_12 ::_thesis: (SAT (M ^\ i)) . [n,p] = 1
(SAT M) . [(i + n),p] = 1 by A2, Def12;
hence (SAT (M ^\ i)) . [n,p] = 1 by Th28; ::_thesis: verum
end;
end;
end;
theorem :: LTLAXIO1:30
for A, B being Element of LTLB_WFF
for F being Subset of LTLB_WFF holds
( F \/ {A} |= B iff F |= ('G' A) => B )
proof
let A, B be Element of LTLB_WFF ; ::_thesis: for F being Subset of LTLB_WFF holds
( F \/ {A} |= B iff F |= ('G' A) => B )
let F be Subset of LTLB_WFF; ::_thesis: ( F \/ {A} |= B iff F |= ('G' A) => B )
hereby ::_thesis: ( F |= ('G' A) => B implies F \/ {A} |= B )
assume A1: F \/ {A} |= B ; ::_thesis: F |= ('G' A) => B
thus F |= ('G' A) => B ::_thesis: verum
proof
let M be LTLModel; :: according to LTLAXIO1:def_14 ::_thesis: ( M |= F implies M |= ('G' A) => B )
assume A2: M |= F ; ::_thesis: M |= ('G' A) => B
thus M |= ('G' A) => B ::_thesis: verum
proof
let n be Element of NAT ; :: according to LTLAXIO1:def_12 ::_thesis: (SAT M) . [n,(('G' A) => B)] = 1
percases ( (SAT M) . [n,('G' A)] = 0 or (SAT M) . [n,('G' A)] = 1 ) by XBOOLEAN:def_3;
supposeA3: (SAT M) . [n,('G' A)] = 0 ; ::_thesis: (SAT M) . [n,(('G' A) => B)] = 1
thus (SAT M) . [n,(('G' A) => B)] = ((SAT M) . [n,('G' A)]) => ((SAT M) . [n,B]) by Def11
.= 1 by A3 ; ::_thesis: verum
end;
supposeA4: (SAT M) . [n,('G' A)] = 1 ; ::_thesis: (SAT M) . [n,(('G' A) => B)] = 1
now__::_thesis:_for_j_being_Element_of_NAT_holds_(SAT_(M_^\_n))_._[j,A]_=_1
let j be Element of NAT ; ::_thesis: (SAT (M ^\ n)) . [j,A] = 1
(SAT M) . [(n + j),A] = 1 by A4, Th10;
hence (SAT (M ^\ n)) . [j,A] = 1 by Th28; ::_thesis: verum
end;
then M ^\ n |= A by Def12;
then A5: M ^\ n |= {A} by Th23;
M ^\ n |= F by A2, Th29;
then M ^\ n |= F \/ {A} by A5, Th22;
then M ^\ n |= B by A1, Def14;
then (SAT (M ^\ n)) . [0,B] = 1 by Def12;
then A6: (SAT M) . [(n + 0),B] = 1 by Th28;
thus (SAT M) . [n,(('G' A) => B)] = ((SAT M) . [n,('G' A)]) => ((SAT M) . [n,B]) by Def11
.= 1 by A6 ; ::_thesis: verum
end;
end;
end;
end;
end;
assume A7: F |= ('G' A) => B ; ::_thesis: F \/ {A} |= B
let M be LTLModel; :: according to LTLAXIO1:def_14 ::_thesis: ( M |= F \/ {A} implies M |= B )
assume A8: M |= F \/ {A} ; ::_thesis: M |= B
let i be Element of NAT ; :: according to LTLAXIO1:def_12 ::_thesis: (SAT M) . [i,B] = 1
M |= {A} by A8, Th22;
then M |= A by Th23;
then for j being Element of NAT holds (SAT M) . [(i + j),A] = 1 by Def12;
then A9: (SAT M) . [i,('G' A)] = 1 by Th10;
M |= F by A8, Th22;
then M |= ('G' A) => B by A7, Def14;
then (SAT M) . [i,(('G' A) => B)] = 1 by Def12;
then ((SAT M) . [i,('G' A)]) => ((SAT M) . [i,B]) = 1 by Def11;
hence (SAT M) . [i,B] = 1 by A9; ::_thesis: verum
end;
definition
let f be Function of LTLB_WFF,BOOLEAN;
func VAL f -> Function of LTLB_WFF,BOOLEAN means :Def15: :: LTLAXIO1:def 15
for A, B being Element of LTLB_WFF
for n being Element of NAT holds
( it . TFALSUM = 0 & it . (prop n) = f . (prop n) & it . (A => B) = (it . A) => (it . B) & it . (A 'Us' B) = f . (A 'Us' B) );
existence
ex b1 being Function of LTLB_WFF,BOOLEAN st
for A, B being Element of LTLB_WFF
for n being Element of NAT holds
( b1 . TFALSUM = 0 & b1 . (prop n) = f . (prop n) & b1 . (A => B) = (b1 . A) => (b1 . B) & b1 . (A 'Us' B) = f . (A 'Us' B) )
proof
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 'Us' $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]
percases ( ( x is Element of BOOLEAN & y is Element of BOOLEAN ) or not x is Element of BOOLEAN or not y is Element of BOOLEAN ) ;
supposethat 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;
percases ( a = 0 or a = 1 ) by XBOOLEAN:def_3;
supposeA4: 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;
supposeA5: a = 1 ; ::_thesis: ex z being set st S1[A,B,x,y,z]
percases ( b = 0 or b = 1 ) by XBOOLEAN:def_3;
supposeA6: 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;
supposeA7: 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 'Us' 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_set_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
percases ( ( 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 set ; ::_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_'Us'_B)_in_BOOLEAN
let A, B be Element of LTLB_WFF ; ::_thesis: val . (A 'Us' B) in BOOLEAN
val . (A 'Us' B) = f . (A 'Us' B) by A11;
hence val . (A 'Us' B) in BOOLEAN ; ::_thesis: verum
end;
percases ( 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 'Us' q or ex p, q being Element of LTLB_WFF st x1 = p => q ) by Th4;
suppose x1 = TFALSUM ; ::_thesis: val . b1 in BOOLEAN
hence val . x in BOOLEAN by A11, TARSKI:def_2; ::_thesis: verum
end;
suppose ex n being Element of NAT st x1 = prop n ; ::_thesis: val . b1 in BOOLEAN
hence val . x in BOOLEAN by A15; ::_thesis: verum
end;
suppose ex p, q being Element of LTLB_WFF st x1 = p 'Us' q ; ::_thesis: val . b1 in BOOLEAN
hence val . x in BOOLEAN by A16; ::_thesis: verum
end;
suppose ex p, q being Element of LTLB_WFF st x1 = p => q ; ::_thesis: val . b1 in BOOLEAN
hence val . x in BOOLEAN by A13; ::_thesis: verum
end;
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 'Us' B) = f . (A 'Us' 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 'Us' B) = f . (A 'Us' B) ) by A11; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of LTLB_WFF,BOOLEAN st ( for A, B being Element of LTLB_WFF
for n being Element of NAT holds
( b1 . TFALSUM = 0 & b1 . (prop n) = f . (prop n) & b1 . (A => B) = (b1 . A) => (b1 . B) & b1 . (A 'Us' B) = f . (A 'Us' B) ) ) & ( for A, B being Element of LTLB_WFF
for n being Element of NAT holds
( b2 . TFALSUM = 0 & b2 . (prop n) = f . (prop n) & b2 . (A => B) = (b2 . A) => (b2 . B) & b2 . (A 'Us' B) = f . (A 'Us' B) ) ) holds
b1 = b2
proof
let v1, v2 be Function of LTLB_WFF,BOOLEAN; ::_thesis: ( ( for A, B being Element of LTLB_WFF
for n being Element of NAT holds
( v1 . TFALSUM = 0 & v1 . (prop n) = f . (prop n) & v1 . (A => B) = (v1 . A) => (v1 . B) & v1 . (A 'Us' B) = f . (A 'Us' B) ) ) & ( for A, B being Element of LTLB_WFF
for n being Element of NAT holds
( v2 . TFALSUM = 0 & v2 . (prop n) = f . (prop n) & v2 . (A => B) = (v2 . A) => (v2 . B) & v2 . (A 'Us' B) = f . (A 'Us' B) ) ) implies v1 = v2 )
assume A17: for A, B being Element of LTLB_WFF
for n being Element of NAT holds
( v1 . TFALSUM = 0 & v1 . (prop n) = f . (prop n) & v1 . (A => B) = (v1 . A) => (v1 . B) & v1 . (A 'Us' B) = f . (A 'Us' B) ) ; ::_thesis: ( ex A, B being Element of LTLB_WFF ex n being Element of NAT st
( v2 . TFALSUM = 0 & v2 . (prop n) = f . (prop n) & v2 . (A => B) = (v2 . A) => (v2 . B) implies not v2 . (A 'Us' B) = f . (A 'Us' B) ) or v1 = v2 )
assume A18: for A, B being Element of LTLB_WFF
for n being Element of NAT holds
( v2 . TFALSUM = 0 & v2 . (prop n) = f . (prop n) & v2 . (A => B) = (v2 . A) => (v2 . B) & v2 . (A 'Us' B) = f . (A 'Us' B) ) ; ::_thesis: v1 = v2
thus v1 = v2 ::_thesis: verum
proof
defpred S1[ Element of LTLB_WFF ] means v1 . $1 = v2 . $1;
A19: for n being Element of NAT holds S1[ prop n]
proof
let n be Element of NAT ; ::_thesis: S1[ prop n]
v1 . (prop n) = f . (prop n) by A17
.= v2 . (prop n) by A18 ;
hence S1[ prop n] ; ::_thesis: verum
end;
A20: for r, s being Element of LTLB_WFF st S1[r] & S1[s] holds
( S1[r 'Us' s] & S1[r => s] )
proof
let r, s be Element of LTLB_WFF ; ::_thesis: ( S1[r] & S1[s] implies ( S1[r 'Us' s] & S1[r => s] ) )
assume A21: ( S1[r] & S1[s] ) ; ::_thesis: ( S1[r 'Us' s] & S1[r => s] )
A22: v1 . (r 'Us' s) = f . (r 'Us' s) by A17
.= v2 . (r 'Us' s) by A18 ;
v1 . (r => s) = (v1 . r) => (v1 . s) by A17
.= v2 . (r => s) by A18, A21 ;
hence ( S1[r 'Us' s] & S1[r => s] ) by A22; ::_thesis: verum
end;
A23: S1[ TFALSUM ] by A17, A18;
for x being Element of LTLB_WFF holds S1[x] from HILBERT2:sch_2(A23, A19, A20);
then A24: for x being Element of LTLB_WFF st x in dom v1 holds
S1[x] ;
dom v1 = LTLB_WFF by FUNCT_2:def_1
.= dom v2 by FUNCT_2:def_1 ;
hence v1 = v2 by A24, PARTFUN1:5; ::_thesis: verum
end;
end;
end;
:: deftheorem Def15 defines VAL LTLAXIO1:def_15_:_
for f, b2 being Function of LTLB_WFF,BOOLEAN holds
( b2 = VAL f iff for A, B being Element of LTLB_WFF
for n being Element of NAT holds
( b2 . TFALSUM = 0 & b2 . (prop n) = f . (prop n) & b2 . (A => B) = (b2 . A) => (b2 . B) & b2 . (A 'Us' B) = f . (A 'Us' B) ) );
theorem Th31: :: LTLAXIO1:31
for f being Function of LTLB_WFF,BOOLEAN
for p, q being Element of LTLB_WFF holds (VAL f) . (p '&&' q) = ((VAL f) . p) '&' ((VAL f) . q)
proof
let f be Function of LTLB_WFF,BOOLEAN; ::_thesis: for p, q being Element of LTLB_WFF holds (VAL f) . (p '&&' q) = ((VAL f) . p) '&' ((VAL f) . q)
let p, q be Element of LTLB_WFF ; ::_thesis: (VAL f) . (p '&&' q) = ((VAL f) . p) '&' ((VAL f) . q)
A1: ( (VAL f) . p = 0 or (VAL f) . p = 1 ) by XBOOLEAN:def_3;
A2: ( (VAL f) . q = 0 or (VAL f) . q = 1 ) by XBOOLEAN:def_3;
thus (VAL f) . (p '&&' q) = ((VAL f) . (p => (q => TFALSUM))) => ((VAL f) . TFALSUM) by Def15
.= (((VAL f) . p) => ((VAL f) . (q => TFALSUM))) => ((VAL f) . TFALSUM) by Def15
.= (((VAL f) . p) => (((VAL f) . q) => ((VAL f) . TFALSUM))) => ((VAL f) . TFALSUM) by Def15
.= (((VAL f) /. p) => (((VAL f) . q) => FALSE)) => ((VAL f) . TFALSUM) by Def15
.= ((VAL f) . p) '&' ((VAL f) . q) by A1, A2, Def15 ; ::_thesis: verum
end;
theorem Th32: :: LTLAXIO1:32
for A being Element of LTLB_WFF
for n being Element of NAT
for M being LTLModel
for f being Function of LTLB_WFF,BOOLEAN st ( for B being set st B in LTLB_WFF holds
f . B = (SAT M) . [n,B] ) holds
(VAL f) . A = (SAT M) . [n,A]
proof
let A be Element of LTLB_WFF ; ::_thesis: for n being Element of NAT
for M being LTLModel
for f being Function of LTLB_WFF,BOOLEAN st ( for B being set st B in LTLB_WFF holds
f . B = (SAT M) . [n,B] ) holds
(VAL f) . A = (SAT M) . [n,A]
let n be Element of NAT ; ::_thesis: for M being LTLModel
for f being Function of LTLB_WFF,BOOLEAN st ( for B being set st B in LTLB_WFF holds
f . B = (SAT M) . [n,B] ) holds
(VAL f) . A = (SAT M) . [n,A]
let M be LTLModel; ::_thesis: for f being Function of LTLB_WFF,BOOLEAN st ( for B being set st B in LTLB_WFF holds
f . B = (SAT M) . [n,B] ) holds
(VAL f) . A = (SAT M) . [n,A]
let f be Function of LTLB_WFF,BOOLEAN; ::_thesis: ( ( for B being set st B in LTLB_WFF holds
f . B = (SAT M) . [n,B] ) implies (VAL f) . A = (SAT M) . [n,A] )
defpred S1[ Element of LTLB_WFF ] means (VAL f) . $1 = (SAT M) . [n,$1];
assume A1: for B being set st B in LTLB_WFF holds
f . B = (SAT M) . [n,B] ; ::_thesis: (VAL f) . A = (SAT M) . [n,A]
A2: for k being Element of NAT holds S1[ prop k]
proof
let k be Element of NAT ; ::_thesis: S1[ prop k]
(SAT M) . [n,(prop k)] = f . (prop k) by A1
.= (VAL f) . (prop k) by Def15 ;
hence S1[ prop k] ; ::_thesis: verum
end;
A3: for r, s being Element of LTLB_WFF st S1[r] & S1[s] holds
( S1[r 'Us' s] & S1[r => s] )
proof
let r, s be Element of LTLB_WFF ; ::_thesis: ( S1[r] & S1[s] implies ( S1[r 'Us' s] & S1[r => s] ) )
assume A4: ( S1[r] & S1[s] ) ; ::_thesis: ( S1[r 'Us' s] & S1[r => s] )
(VAL f) . (r 'Us' s) = f . (r 'Us' s) by Def15
.= (SAT M) . [n,(r 'Us' s)] by A1 ;
hence S1[r 'Us' s] ; ::_thesis: S1[r => s]
(SAT M) . [n,(r => s)] = ((SAT M) . [n,r]) => ((SAT M) . [n,s]) by Def11
.= (VAL f) . (r => s) by A4, Def15 ;
hence S1[r => s] ; ::_thesis: verum
end;
(SAT M) . [n,TFALSUM] = 0 by Def11
.= (VAL f) . TFALSUM by Def15 ;
then A5: S1[ TFALSUM ] ;
for r being Element of LTLB_WFF holds S1[r] from HILBERT2:sch_2(A5, A2, A3);
hence (VAL f) . A = (SAT M) . [n,A] ; ::_thesis: verum
end;
definition
let p be Element of LTLB_WFF ;
attrp is LTL_TAUT_OF_PL means :Def16: :: LTLAXIO1:def 16
for f being Function of LTLB_WFF,BOOLEAN holds (VAL f) . p = 1;
end;
:: deftheorem Def16 defines LTL_TAUT_OF_PL LTLAXIO1:def_16_:_
for p being Element of LTLB_WFF holds
( p is LTL_TAUT_OF_PL iff for f being Function of LTLB_WFF,BOOLEAN holds (VAL f) . p = 1 );
theorem Th33: :: LTLAXIO1:33
for A being Element of LTLB_WFF
for F being Subset of LTLB_WFF st A is LTL_TAUT_OF_PL holds
F |= A
proof
let A be Element of LTLB_WFF ; ::_thesis: for F being Subset of LTLB_WFF st A is LTL_TAUT_OF_PL holds
F |= A
let F be Subset of LTLB_WFF; ::_thesis: ( A is LTL_TAUT_OF_PL implies F |= A )
assume A1: A is LTL_TAUT_OF_PL ; ::_thesis: F |= A
let M be LTLModel; :: according to LTLAXIO1:def_14 ::_thesis: ( M |= F implies M |= A )
assume M |= F ; ::_thesis: M |= A
let n be Element of NAT ; :: according to LTLAXIO1:def_12 ::_thesis: (SAT M) . [n,A] = 1
defpred S1[ set , set ] means $2 = (SAT M) . [n,$1];
A2: for x being set st x in LTLB_WFF holds
ex y being set st
( y in BOOLEAN & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in LTLB_WFF implies ex y being set st
( y in BOOLEAN & S1[x,y] ) )
set y = (SAT M) . [n,x];
assume x in LTLB_WFF ; ::_thesis: ex y being set st
( y in BOOLEAN & S1[x,y] )
then reconsider x1 = x as Element of LTLB_WFF ;
take (SAT M) . [n,x] ; ::_thesis: ( (SAT M) . [n,x] in BOOLEAN & S1[x,(SAT M) . [n,x]] )
(SAT M) . [n,x1] in BOOLEAN ;
hence ( (SAT M) . [n,x] in BOOLEAN & S1[x,(SAT M) . [n,x]] ) ; ::_thesis: verum
end;
consider f being Function of LTLB_WFF,BOOLEAN such that
A3: for B being set st B in LTLB_WFF holds
S1[B,f . B] from FUNCT_2:sch_1(A2);
thus (SAT M) . [n,A] = (VAL f) . A by A3, Th32
.= 1 by A1, Def16 ; ::_thesis: verum
end;
begin
definition
let D be set ;
attrD is with_LTL_axioms means :Def17: :: LTLAXIO1:def 17
for p, q being Element of LTLB_WFF holds
( ( p is LTL_TAUT_OF_PL implies p in D ) & ('not' ('X' p)) => ('X' ('not' p)) in D & ('X' ('not' p)) => ('not' ('X' p)) in D & ('X' (p => q)) => (('X' p) => ('X' q)) in D & ('G' p) => (p '&&' ('X' ('G' p))) in D & (p 'Us' q) => (('X' q) 'or' ('X' (p '&&' (p 'Us' q)))) in D & (('X' q) 'or' ('X' (p '&&' (p 'Us' q)))) => (p 'Us' q) in D & (p 'Us' q) => ('X' ('F' q)) in D );
end;
:: deftheorem Def17 defines with_LTL_axioms LTLAXIO1:def_17_:_
for D being set holds
( D is with_LTL_axioms iff for p, q being Element of LTLB_WFF holds
( ( p is LTL_TAUT_OF_PL implies p in D ) & ('not' ('X' p)) => ('X' ('not' p)) in D & ('X' ('not' p)) => ('not' ('X' p)) in D & ('X' (p => q)) => (('X' p) => ('X' q)) in D & ('G' p) => (p '&&' ('X' ('G' p))) in D & (p 'Us' q) => (('X' q) 'or' ('X' (p '&&' (p 'Us' q)))) in D & (('X' q) 'or' ('X' (p '&&' (p 'Us' q)))) => (p 'Us' q) in D & (p 'Us' q) => ('X' ('F' q)) in D ) );
definition
func LTL_axioms -> Subset of LTLB_WFF means :Def18: :: LTLAXIO1:def 18
( it is with_LTL_axioms & ( for D being Subset of LTLB_WFF st D is with_LTL_axioms holds
it c= D ) );
existence
ex b1 being Subset of LTLB_WFF st
( b1 is with_LTL_axioms & ( for D being Subset of LTLB_WFF st D is with_LTL_axioms holds
b1 c= D ) )
proof
defpred S1[ set ] means for D being set st D is with_LTL_axioms holds
$1 in D;
consider D0 being set such that
A1: for x being set holds
( x in D0 iff ( x in LTLB_WFF & S1[x] ) ) from XBOOLE_0:sch_1();
D0 c= LTLB_WFF
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D0 or x in LTLB_WFF )
assume x in D0 ; ::_thesis: x in LTLB_WFF
hence x in LTLB_WFF by A1; ::_thesis: verum
end;
then reconsider D0 = D0 as Subset of LTLB_WFF ;
take D0 ; ::_thesis: ( D0 is with_LTL_axioms & ( for D being Subset of LTLB_WFF st D is with_LTL_axioms holds
D0 c= D ) )
thus D0 is with_LTL_axioms ::_thesis: for D being Subset of LTLB_WFF st D is with_LTL_axioms holds
D0 c= D
proof
let p, q be Element of LTLB_WFF ; :: according to LTLAXIO1:def_17 ::_thesis: ( ( p is LTL_TAUT_OF_PL implies p in D0 ) & ('not' ('X' p)) => ('X' ('not' p)) in D0 & ('X' ('not' p)) => ('not' ('X' p)) in D0 & ('X' (p => q)) => (('X' p) => ('X' q)) in D0 & ('G' p) => (p '&&' ('X' ('G' p))) in D0 & (p 'Us' q) => (('X' q) 'or' ('X' (p '&&' (p 'Us' q)))) in D0 & (('X' q) 'or' ('X' (p '&&' (p 'Us' q)))) => (p 'Us' q) in D0 & (p 'Us' q) => ('X' ('F' q)) in D0 )
thus ( p is LTL_TAUT_OF_PL implies p in D0 ) ::_thesis: ( ('not' ('X' p)) => ('X' ('not' p)) in D0 & ('X' ('not' p)) => ('not' ('X' p)) in D0 & ('X' (p => q)) => (('X' p) => ('X' q)) in D0 & ('G' p) => (p '&&' ('X' ('G' p))) in D0 & (p 'Us' q) => (('X' q) 'or' ('X' (p '&&' (p 'Us' q)))) in D0 & (('X' q) 'or' ('X' (p '&&' (p 'Us' q)))) => (p 'Us' q) in D0 & (p 'Us' q) => ('X' ('F' q)) in D0 )
proof
assume p is LTL_TAUT_OF_PL ; ::_thesis: p in D0
then for D being set st D is with_LTL_axioms holds
p in D by Def17;
hence p in D0 by A1; ::_thesis: verum
end;
for D being set st D is with_LTL_axioms holds
('not' ('X' p)) => ('X' ('not' p)) in D by Def17;
hence ('not' ('X' p)) => ('X' ('not' p)) in D0 by A1; ::_thesis: ( ('X' ('not' p)) => ('not' ('X' p)) in D0 & ('X' (p => q)) => (('X' p) => ('X' q)) in D0 & ('G' p) => (p '&&' ('X' ('G' p))) in D0 & (p 'Us' q) => (('X' q) 'or' ('X' (p '&&' (p 'Us' q)))) in D0 & (('X' q) 'or' ('X' (p '&&' (p 'Us' q)))) => (p 'Us' q) in D0 & (p 'Us' q) => ('X' ('F' q)) in D0 )
for D being set st D is with_LTL_axioms holds
('X' ('not' p)) => ('not' ('X' p)) in D by Def17;
hence ('X' ('not' p)) => ('not' ('X' p)) in D0 by A1; ::_thesis: ( ('X' (p => q)) => (('X' p) => ('X' q)) in D0 & ('G' p) => (p '&&' ('X' ('G' p))) in D0 & (p 'Us' q) => (('X' q) 'or' ('X' (p '&&' (p 'Us' q)))) in D0 & (('X' q) 'or' ('X' (p '&&' (p 'Us' q)))) => (p 'Us' q) in D0 & (p 'Us' q) => ('X' ('F' q)) in D0 )
for D being set st D is with_LTL_axioms holds
('X' (p => q)) => (('X' p) => ('X' q)) in D by Def17;
hence ('X' (p => q)) => (('X' p) => ('X' q)) in D0 by A1; ::_thesis: ( ('G' p) => (p '&&' ('X' ('G' p))) in D0 & (p 'Us' q) => (('X' q) 'or' ('X' (p '&&' (p 'Us' q)))) in D0 & (('X' q) 'or' ('X' (p '&&' (p 'Us' q)))) => (p 'Us' q) in D0 & (p 'Us' q) => ('X' ('F' q)) in D0 )
for D being set st D is with_LTL_axioms holds
('G' p) => (p '&&' ('X' ('G' p))) in D by Def17;
hence ('G' p) => (p '&&' ('X' ('G' p))) in D0 by A1; ::_thesis: ( (p 'Us' q) => (('X' q) 'or' ('X' (p '&&' (p 'Us' q)))) in D0 & (('X' q) 'or' ('X' (p '&&' (p 'Us' q)))) => (p 'Us' q) in D0 & (p 'Us' q) => ('X' ('F' q)) in D0 )
for D being set st D is with_LTL_axioms holds
(p 'Us' q) => (('X' q) 'or' ('X' (p '&&' (p 'Us' q)))) in D by Def17;
hence (p 'Us' q) => (('X' q) 'or' ('X' (p '&&' (p 'Us' q)))) in D0 by A1; ::_thesis: ( (('X' q) 'or' ('X' (p '&&' (p 'Us' q)))) => (p 'Us' q) in D0 & (p 'Us' q) => ('X' ('F' q)) in D0 )
for D being set st D is with_LTL_axioms holds
(('X' q) 'or' ('X' (p '&&' (p 'Us' q)))) => (p 'Us' q) in D by Def17;
hence (('X' q) 'or' ('X' (p '&&' (p 'Us' q)))) => (p 'Us' q) in D0 by A1; ::_thesis: (p 'Us' q) => ('X' ('F' q)) in D0
for D being set st D is with_LTL_axioms holds
(p 'Us' q) => ('X' ('F' q)) in D by Def17;
hence (p 'Us' q) => ('X' ('F' q)) in D0 by A1; ::_thesis: verum
end;
let D be Subset of LTLB_WFF; ::_thesis: ( D is with_LTL_axioms implies D0 c= D )
assume A2: D is with_LTL_axioms ; ::_thesis: D0 c= D
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D0 or x in D )
assume x in D0 ; ::_thesis: x in D
hence x in D by A1, A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being Subset of LTLB_WFF st b1 is with_LTL_axioms & ( for D being Subset of LTLB_WFF st D is with_LTL_axioms holds
b1 c= D ) & b2 is with_LTL_axioms & ( for D being Subset of LTLB_WFF st D is with_LTL_axioms holds
b2 c= D ) holds
b1 = b2
proof
let D1, D2 be Subset of LTLB_WFF; ::_thesis: ( D1 is with_LTL_axioms & ( for D being Subset of LTLB_WFF st D is with_LTL_axioms holds
D1 c= D ) & D2 is with_LTL_axioms & ( for D being Subset of LTLB_WFF st D is with_LTL_axioms holds
D2 c= D ) implies D1 = D2 )
assume ( D1 is with_LTL_axioms & ( for D being Subset of LTLB_WFF st D is with_LTL_axioms holds
D1 c= D ) & D2 is with_LTL_axioms & ( for D being Subset of LTLB_WFF st D is with_LTL_axioms holds
D2 c= D ) ) ; ::_thesis: D1 = D2
then ( D1 c= D2 & D2 c= D1 ) ;
hence D1 = D2 by XBOOLE_0:def_10; ::_thesis: verum
end;
end;
:: deftheorem Def18 defines LTL_axioms LTLAXIO1:def_18_:_
for b1 being Subset of LTLB_WFF holds
( b1 = LTL_axioms iff ( b1 is with_LTL_axioms & ( for D being Subset of LTLB_WFF st D is with_LTL_axioms holds
b1 c= D ) ) );
registration
cluster LTL_axioms -> with_LTL_axioms ;
coherence
LTL_axioms is with_LTL_axioms by Def18;
end;
theorem Th34: :: LTLAXIO1:34
for p, q being Element of LTLB_WFF holds p => (q => p) in LTL_axioms
proof
let p, q be Element of LTLB_WFF ; ::_thesis: p => (q => p) in LTL_axioms
p => (q => p) is LTL_TAUT_OF_PL
proof
let f be Function of LTLB_WFF,BOOLEAN; :: according to LTLAXIO1:def_16 ::_thesis: (VAL f) . (p => (q => p)) = 1
A1: ( (VAL f) . p = 0 or (VAL f) . p = 1 ) by XBOOLEAN:def_3;
thus (VAL f) . (p => (q => p)) = ((VAL f) . p) => ((VAL f) . (q => p)) by Def15
.= ((VAL f) . p) => (((VAL f) . q) => ((VAL f) . p)) by Def15
.= 1 by A1 ; ::_thesis: verum
end;
hence p => (q => p) in LTL_axioms by Def17; ::_thesis: verum
end;
theorem Th35: :: LTLAXIO1:35
for p, q, r being Element of LTLB_WFF holds (p => (q => r)) => ((p => q) => (p => r)) in LTL_axioms
proof
let p, q, r be Element of LTLB_WFF ; ::_thesis: (p => (q => r)) => ((p => q) => (p => r)) in LTL_axioms
(p => (q => r)) => ((p => q) => (p => r)) is LTL_TAUT_OF_PL
proof
let f be Function of LTLB_WFF,BOOLEAN; :: according to LTLAXIO1:def_16 ::_thesis: (VAL f) . ((p => (q => r)) => ((p => q) => (p => r))) = 1
A1: ( (VAL f) . p = 0 or (VAL f) . p = 1 ) by XBOOLEAN:def_3;
A2: ( (VAL f) . q = 0 or (VAL f) . q = 1 ) by XBOOLEAN:def_3;
A3: ( (VAL f) . r = 0 or (VAL f) . r = 1 ) by XBOOLEAN:def_3;
thus (VAL f) . ((p => (q => r)) => ((p => q) => (p => r))) = ((VAL f) . (p => (q => r))) => ((VAL f) . ((p => q) => (p => r))) by Def15
.= (((VAL f) . p) => ((VAL f) . (q => r))) => ((VAL f) . ((p => q) => (p => r))) by Def15
.= (((VAL f) . p) => (((VAL f) . q) => ((VAL f) . r))) => ((VAL f) . ((p => q) => (p => r))) by Def15
.= (((VAL f) . p) => (((VAL f) . q) => ((VAL f) . r))) => (((VAL f) . (p => q)) => ((VAL f) . (p => r))) by Def15
.= (((VAL f) . p) => (((VAL f) . q) => ((VAL f) . r))) => ((((VAL f) . p) => ((VAL f) . q)) => ((VAL f) . (p => r))) by Def15
.= 1 by A1, A2, A3, Def15 ; ::_thesis: verum
end;
hence (p => (q => r)) => ((p => q) => (p => r)) in LTL_axioms by Def17; ::_thesis: verum
end;
definition
let p, q be Element of LTLB_WFF ;
predp NEX_rule q means :Def19: :: LTLAXIO1:def 19
q = 'X' p;
let r be Element of LTLB_WFF ;
predp,q MP_rule r means :Def20: :: LTLAXIO1:def 20
q = p => r;
predp,q IND_rule r means :Def21: :: LTLAXIO1:def 21
ex A, B being Element of LTLB_WFF st
( p = A => B & q = A => ('X' A) & r = A => ('G' B) );
end;
:: deftheorem Def19 defines NEX_rule LTLAXIO1:def_19_:_
for p, q being Element of LTLB_WFF holds
( p NEX_rule q iff q = 'X' p );
:: deftheorem Def20 defines MP_rule LTLAXIO1:def_20_:_
for p, q, r being Element of LTLB_WFF holds
( p,q MP_rule r iff q = p => r );
:: deftheorem Def21 defines IND_rule LTLAXIO1:def_21_:_
for p, q, r being Element of LTLB_WFF holds
( p,q IND_rule r iff ex A, B being Element of LTLB_WFF st
( p = A => B & q = A => ('X' A) & r = A => ('G' B) ) );
registration
cluster LTL_axioms -> non empty ;
coherence
not LTL_axioms is empty by Def17;
end;
definition
let A be Element of LTLB_WFF ;
attrA is axltl1 means :Def22: :: LTLAXIO1:def 22
ex B being Element of LTLB_WFF st A = ('not' ('X' B)) => ('X' ('not' B));
attrA is axltl1a means :Def23: :: LTLAXIO1:def 23
ex B being Element of LTLB_WFF st A = ('X' ('not' B)) => ('not' ('X' B));
attrA is axltl2 means :Def24: :: LTLAXIO1:def 24
ex B, C being Element of LTLB_WFF st A = ('X' (B => C)) => (('X' B) => ('X' C));
attrA is axltl3 means :Def25: :: LTLAXIO1:def 25
ex B being Element of LTLB_WFF st A = ('G' B) => (B '&&' ('X' ('G' B)));
attrA is axltl4 means :Def26: :: LTLAXIO1:def 26
ex B, C being Element of LTLB_WFF st A = (B 'Us' C) => (('X' C) 'or' ('X' (B '&&' (B 'Us' C))));
attrA is axltl5 means :Def27: :: LTLAXIO1:def 27
ex B, C being Element of LTLB_WFF st A = (('X' C) 'or' ('X' (B '&&' (B 'Us' C)))) => (B 'Us' C);
attrA is axltl6 means :Def28: :: LTLAXIO1:def 28
ex B, C being Element of LTLB_WFF st A = (B 'Us' C) => ('X' ('F' C));
end;
:: deftheorem Def22 defines axltl1 LTLAXIO1:def_22_:_
for A being Element of LTLB_WFF holds
( A is axltl1 iff ex B being Element of LTLB_WFF st A = ('not' ('X' B)) => ('X' ('not' B)) );
:: deftheorem Def23 defines axltl1a LTLAXIO1:def_23_:_
for A being Element of LTLB_WFF holds
( A is axltl1a iff ex B being Element of LTLB_WFF st A = ('X' ('not' B)) => ('not' ('X' B)) );
:: deftheorem Def24 defines axltl2 LTLAXIO1:def_24_:_
for A being Element of LTLB_WFF holds
( A is axltl2 iff ex B, C being Element of LTLB_WFF st A = ('X' (B => C)) => (('X' B) => ('X' C)) );
:: deftheorem Def25 defines axltl3 LTLAXIO1:def_25_:_
for A being Element of LTLB_WFF holds
( A is axltl3 iff ex B being Element of LTLB_WFF st A = ('G' B) => (B '&&' ('X' ('G' B))) );
:: deftheorem Def26 defines axltl4 LTLAXIO1:def_26_:_
for A being Element of LTLB_WFF holds
( A is axltl4 iff ex B, C being Element of LTLB_WFF st A = (B 'Us' C) => (('X' C) 'or' ('X' (B '&&' (B 'Us' C)))) );
:: deftheorem Def27 defines axltl5 LTLAXIO1:def_27_:_
for A being Element of LTLB_WFF holds
( A is axltl5 iff ex B, C being Element of LTLB_WFF st A = (('X' C) 'or' ('X' (B '&&' (B 'Us' C)))) => (B 'Us' C) );
:: deftheorem Def28 defines axltl6 LTLAXIO1:def_28_:_
for A being Element of LTLB_WFF holds
( A is axltl6 iff ex B, C being Element of LTLB_WFF st A = (B 'Us' C) => ('X' ('F' C)) );
theorem Th36: :: LTLAXIO1:36
for A being Element of LTL_axioms holds
( A is LTL_TAUT_OF_PL or A is axltl1 or A is axltl1a or A is axltl2 or A is axltl3 or A is axltl4 or A is axltl5 or A is axltl6 )
proof
defpred S1[ Element of LTL_axioms ] means ( $1 is LTL_TAUT_OF_PL or $1 is axltl1 or $1 is axltl1a or $1 is axltl2 or $1 is axltl3 or $1 is axltl4 or $1 is axltl5 or $1 is axltl6 );
set X = { p where p is Element of LTL_axioms : S1[p] } ;
{ p where p is Element of LTL_axioms : S1[p] } c= LTLB_WFF
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { p where p is Element of LTL_axioms : S1[p] } or x in LTLB_WFF )
assume x in { p where p is Element of LTL_axioms : S1[p] } ; ::_thesis: x in LTLB_WFF
then ex p being Element of LTL_axioms st
( x = p & S1[p] ) ;
hence x in LTLB_WFF ; ::_thesis: verum
end;
then reconsider X = { p where p is Element of LTL_axioms : S1[p] } as Subset of LTLB_WFF ;
let A be Element of LTL_axioms ; ::_thesis: ( A is LTL_TAUT_OF_PL or A is axltl1 or A is axltl1a or A is axltl2 or A is axltl3 or A is axltl4 or A is axltl5 or A is axltl6 )
X is with_LTL_axioms
proof
let p be Element of LTLB_WFF ; :: according to LTLAXIO1:def_17 ::_thesis: for q being Element of LTLB_WFF holds
( ( p is LTL_TAUT_OF_PL implies p in X ) & ('not' ('X' p)) => ('X' ('not' p)) in X & ('X' ('not' p)) => ('not' ('X' p)) in X & ('X' (p => q)) => (('X' p) => ('X' q)) in X & ('G' p) => (p '&&' ('X' ('G' p))) in X & (p 'Us' q) => (('X' q) 'or' ('X' (p '&&' (p 'Us' q)))) in X & (('X' q) 'or' ('X' (p '&&' (p 'Us' q)))) => (p 'Us' q) in X & (p 'Us' q) => ('X' ('F' q)) in X )
let q be Element of LTLB_WFF ; ::_thesis: ( ( p is LTL_TAUT_OF_PL implies p in X ) & ('not' ('X' p)) => ('X' ('not' p)) in X & ('X' ('not' p)) => ('not' ('X' p)) in X & ('X' (p => q)) => (('X' p) => ('X' q)) in X & ('G' p) => (p '&&' ('X' ('G' p))) in X & (p 'Us' q) => (('X' q) 'or' ('X' (p '&&' (p 'Us' q)))) in X & (('X' q) 'or' ('X' (p '&&' (p 'Us' q)))) => (p 'Us' q) in X & (p 'Us' q) => ('X' ('F' q)) in X )
thus ( p is LTL_TAUT_OF_PL implies p in X ) ::_thesis: ( ('not' ('X' p)) => ('X' ('not' p)) in X & ('X' ('not' p)) => ('not' ('X' p)) in X & ('X' (p => q)) => (('X' p) => ('X' q)) in X & ('G' p) => (p '&&' ('X' ('G' p))) in X & (p 'Us' q) => (('X' q) 'or' ('X' (p '&&' (p 'Us' q)))) in X & (('X' q) 'or' ('X' (p '&&' (p 'Us' q)))) => (p 'Us' q) in X & (p 'Us' q) => ('X' ('F' q)) in X )
proof
assume A1: p is LTL_TAUT_OF_PL ; ::_thesis: p in X
then reconsider p1 = p as Element of LTL_axioms by Def17;
S1[p1] by A1;
hence p in X ; ::_thesis: verum
end;
thus ('not' ('X' p)) => ('X' ('not' p)) in X ::_thesis: ( ('X' ('not' p)) => ('not' ('X' p)) in X & ('X' (p => q)) => (('X' p) => ('X' q)) in X & ('G' p) => (p '&&' ('X' ('G' p))) in X & (p 'Us' q) => (('X' q) 'or' ('X' (p '&&' (p 'Us' q)))) in X & (('X' q) 'or' ('X' (p '&&' (p 'Us' q)))) => (p 'Us' q) in X & (p 'Us' q) => ('X' ('F' q)) in X )
proof
reconsider pp = ('not' ('X' p)) => ('X' ('not' p)) as Element of LTL_axioms by Def17;
S1[pp] by Def22;
hence ('not' ('X' p)) => ('X' ('not' p)) in X ; ::_thesis: verum
end;
thus ('X' ('not' p)) => ('not' ('X' p)) in X ::_thesis: ( ('X' (p => q)) => (('X' p) => ('X' q)) in X & ('G' p) => (p '&&' ('X' ('G' p))) in X & (p 'Us' q) => (('X' q) 'or' ('X' (p '&&' (p 'Us' q)))) in X & (('X' q) 'or' ('X' (p '&&' (p 'Us' q)))) => (p 'Us' q) in X & (p 'Us' q) => ('X' ('F' q)) in X )
proof
reconsider pp = ('X' ('not' p)) => ('not' ('X' p)) as Element of LTL_axioms by Def17;
S1[pp] by Def23;
hence ('X' ('not' p)) => ('not' ('X' p)) in X ; ::_thesis: verum
end;
thus ('X' (p => q)) => (('X' p) => ('X' q)) in X ::_thesis: ( ('G' p) => (p '&&' ('X' ('G' p))) in X & (p 'Us' q) => (('X' q) 'or' ('X' (p '&&' (p 'Us' q)))) in X & (('X' q) 'or' ('X' (p '&&' (p 'Us' q)))) => (p 'Us' q) in X & (p 'Us' q) => ('X' ('F' q)) in X )
proof
reconsider pp = ('X' (p => q)) => (('X' p) => ('X' q)) as Element of LTL_axioms by Def17;
S1[pp] by Def24;
hence ('X' (p => q)) => (('X' p) => ('X' q)) in X ; ::_thesis: verum
end;
thus ('G' p) => (p '&&' ('X' ('G' p))) in X ::_thesis: ( (p 'Us' q) => (('X' q) 'or' ('X' (p '&&' (p 'Us' q)))) in X & (('X' q) 'or' ('X' (p '&&' (p 'Us' q)))) => (p 'Us' q) in X & (p 'Us' q) => ('X' ('F' q)) in X )
proof
reconsider pp = ('G' p) => (p '&&' ('X' ('G' p))) as Element of LTL_axioms by Def17;
S1[pp] by Def25;
hence ('G' p) => (p '&&' ('X' ('G' p))) in X ; ::_thesis: verum
end;
thus (p 'Us' q) => (('X' q) 'or' ('X' (p '&&' (p 'Us' q)))) in X ::_thesis: ( (('X' q) 'or' ('X' (p '&&' (p 'Us' q)))) => (p 'Us' q) in X & (p 'Us' q) => ('X' ('F' q)) in X )
proof
reconsider pp = (p 'Us' q) => (('X' q) 'or' ('X' (p '&&' (p 'Us' q)))) as Element of LTL_axioms by Def17;
S1[pp] by Def26;
hence (p 'Us' q) => (('X' q) 'or' ('X' (p '&&' (p 'Us' q)))) in X ; ::_thesis: verum
end;
thus (('X' q) 'or' ('X' (p '&&' (p 'Us' q)))) => (p 'Us' q) in X ::_thesis: (p 'Us' q) => ('X' ('F' q)) in X
proof
reconsider pp = (('X' q) 'or' ('X' (p '&&' (p 'Us' q)))) => (p 'Us' q) as Element of LTL_axioms by Def17;
S1[pp] by Def27;
hence (('X' q) 'or' ('X' (p '&&' (p 'Us' q)))) => (p 'Us' q) in X ; ::_thesis: verum
end;
thus (p 'Us' q) => ('X' ('F' q)) in X ::_thesis: verum
proof
reconsider pp = (p 'Us' q) => ('X' ('F' q)) as Element of LTL_axioms by Def17;
S1[pp] by Def28;
hence (p 'Us' q) => ('X' ('F' q)) in X ; ::_thesis: verum
end;
end;
then ( A in LTL_axioms & LTL_axioms c= X ) by Def18;
then A in X ;
then ex p being Element of LTL_axioms st
( A = p & S1[p] ) ;
hence S1[A] ; ::_thesis: verum
end;
theorem Th37: :: LTLAXIO1:37
for A being Element of LTLB_WFF
for F being Subset of LTLB_WFF st ( A is axltl1 or A is axltl1a or A is axltl2 or A is axltl3 or A is axltl4 or A is axltl5 or A is axltl6 ) holds
F |= A
proof
let A be Element of LTLB_WFF ; ::_thesis: for F being Subset of LTLB_WFF st ( A is axltl1 or A is axltl1a or A is axltl2 or A is axltl3 or A is axltl4 or A is axltl5 or A is axltl6 ) holds
F |= A
let F be Subset of LTLB_WFF; ::_thesis: ( ( A is axltl1 or A is axltl1a or A is axltl2 or A is axltl3 or A is axltl4 or A is axltl5 or A is axltl6 ) implies F |= A )
assume A1: ( A is axltl1 or A is axltl1a or A is axltl2 or A is axltl3 or A is axltl4 or A is axltl5 or A is axltl6 ) ; ::_thesis: F |= A
let M be LTLModel; :: according to LTLAXIO1:def_14 ::_thesis: ( M |= F implies M |= A )
assume M |= F ; ::_thesis: M |= A
let n be Element of NAT ; :: according to LTLAXIO1:def_12 ::_thesis: (SAT M) . [n,A] = 1
percases ( A is axltl1 or A is axltl1a or A is axltl2 or A is axltl3 or A is axltl4 or A is axltl5 or A is axltl6 ) by A1;
suppose A is axltl1 ; ::_thesis: (SAT M) . [n,A] = 1
then consider B being Element of LTLB_WFF such that
A2: A = ('not' ('X' B)) => ('X' ('not' B)) by Def22;
thus (SAT M) . [n,A] = 1 by A2, Th15; ::_thesis: verum
end;
suppose A is axltl1a ; ::_thesis: (SAT M) . [n,A] = 1
then consider B being Element of LTLB_WFF such that
A3: A = ('X' ('not' B)) => ('not' ('X' B)) by Def23;
thus (SAT M) . [n,A] = 1 by A3, Th16; ::_thesis: verum
end;
suppose A is axltl2 ; ::_thesis: (SAT M) . [n,A] = 1
then consider B, C being Element of LTLB_WFF such that
A4: A = ('X' (B => C)) => (('X' B) => ('X' C)) by Def24;
thus (SAT M) . [n,A] = 1 by A4, Th17; ::_thesis: verum
end;
suppose A is axltl3 ; ::_thesis: (SAT M) . [n,A] = 1
then consider B being Element of LTLB_WFF such that
A5: A = ('G' B) => (B '&&' ('X' ('G' B))) by Def25;
thus (SAT M) . [n,A] = 1 by A5, Th18; ::_thesis: verum
end;
suppose A is axltl4 ; ::_thesis: (SAT M) . [n,A] = 1
then consider B, C being Element of LTLB_WFF such that
A6: A = (B 'Us' C) => (('X' C) 'or' ('X' (B '&&' (B 'Us' C)))) by Def26;
thus (SAT M) . [n,A] = 1 by A6, Th19; ::_thesis: verum
end;
suppose A is axltl5 ; ::_thesis: (SAT M) . [n,A] = 1
then consider B, C being Element of LTLB_WFF such that
A7: A = (('X' C) 'or' ('X' (B '&&' (B 'Us' C)))) => (B 'Us' C) by Def27;
thus (SAT M) . [n,A] = 1 by A7, Th20; ::_thesis: verum
end;
suppose A is axltl6 ; ::_thesis: (SAT M) . [n,A] = 1
then consider B, C being Element of LTLB_WFF such that
A8: A = (B 'Us' C) => ('X' ('F' C)) by Def28;
thus (SAT M) . [n,A] = 1 by A8, Th21; ::_thesis: verum
end;
end;
end;
definition
let i be Nat;
let f be FinSequence of LTLB_WFF ;
let X be Subset of LTLB_WFF;
pred prc f,X,i means :Def29: :: LTLAXIO1:def 29
( f . i in LTL_axioms or f . i in X or ex j, k being Nat st
( 1 <= j & j < i & 1 <= k & k < i & ( f /. j,f /. k MP_rule f /. i or f /. j,f /. k IND_rule f /. i ) ) or ex j being Nat st
( 1 <= j & j < i & f /. j NEX_rule f /. i ) );
end;
:: deftheorem Def29 defines prc LTLAXIO1:def_29_:_
for i being Nat
for f being FinSequence of LTLB_WFF
for X being Subset of LTLB_WFF holds
( prc f,X,i iff ( f . i in LTL_axioms or f . i in X or ex j, k being Nat st
( 1 <= j & j < i & 1 <= k & k < i & ( f /. j,f /. k MP_rule f /. i or f /. j,f /. k IND_rule f /. i ) ) or ex j being Nat st
( 1 <= j & j < i & f /. j NEX_rule f /. i ) ) );
definition
let X be Subset of LTLB_WFF;
let p be Element of LTLB_WFF ;
predX |- p means :Def30: :: LTLAXIO1:def 30
ex f being FinSequence of LTLB_WFF st
( f . (len f) = p & 1 <= len f & ( for i being Nat st 1 <= i & i <= len f holds
prc f,X,i ) );
end;
:: deftheorem Def30 defines |- LTLAXIO1:def_30_:_
for X being Subset of LTLB_WFF
for p being Element of LTLB_WFF holds
( X |- p iff ex f being FinSequence of LTLB_WFF st
( f . (len f) = p & 1 <= len f & ( for i being Nat st 1 <= i & i <= len f holds
prc f,X,i ) ) );
theorem Th38: :: LTLAXIO1:38
for X being Subset of LTLB_WFF
for f, f2 being FinSequence of LTLB_WFF
for i, n being Nat st n + (len f) <= len f2 & ( for k being Nat st 1 <= k & k <= len f holds
f . k = f2 . (k + n) ) & 1 <= i & i <= len f & prc f,X,i holds
prc f2,X,i + n
proof
let X be Subset of LTLB_WFF; ::_thesis: for f, f2 being FinSequence of LTLB_WFF
for i, n being Nat st n + (len f) <= len f2 & ( for k being Nat st 1 <= k & k <= len f holds
f . k = f2 . (k + n) ) & 1 <= i & i <= len f & prc f,X,i holds
prc f2,X,i + n
let f, f2 be FinSequence of LTLB_WFF ; ::_thesis: for i, n being Nat st n + (len f) <= len f2 & ( for k being Nat st 1 <= k & k <= len f holds
f . k = f2 . (k + n) ) & 1 <= i & i <= len f & prc f,X,i holds
prc f2,X,i + n
let i, n be Nat; ::_thesis: ( n + (len f) <= len f2 & ( for k being Nat st 1 <= k & k <= len f holds
f . k = f2 . (k + n) ) & 1 <= i & i <= len f & prc f,X,i implies prc f2,X,i + n )
assume that
A1: n + (len f) <= len f2 and
A2: for k being Nat st 1 <= k & k <= len f holds
f . k = f2 . (k + n) and
A3: 1 <= i and
A4: i <= len f ; ::_thesis: ( not prc f,X,i or prc f2,X,i + n )
i + n <= (len f) + n by A4, XREAL_1:6;
then A5: i + n <= len f2 by A1, XXREAL_0:2;
A6: f /. i = f . i by A3, A4, Lm1
.= f2 . (i + n) by A2, A3, A4
.= f2 /. (i + n) by A3, A5, Lm1, NAT_1:12 ;
assume A7: prc f,X,i ; ::_thesis: prc f2,X,i + n
percases ( f . i in LTL_axioms or f . i in X or ex j, k being Nat st
( 1 <= j & j < i & 1 <= k & k < i & ( f /. j,f /. k MP_rule f /. i or f /. j,f /. k IND_rule f /. i ) ) or ex j being Nat st
( 1 <= j & j < i & f /. j NEX_rule f /. i ) ) by A7, Def29;
suppose f . i in LTL_axioms ; ::_thesis: prc f2,X,i + n
then f2 . (i + n) in LTL_axioms by A2, A3, A4;
hence prc f2,X,i + n by Def29; ::_thesis: verum
end;
suppose f . i in X ; ::_thesis: prc f2,X,i + n
then f2 . (i + n) in X by A2, A3, A4;
hence prc f2,X,i + n by Def29; ::_thesis: verum
end;
suppose ex j, k being Nat st
( 1 <= j & j < i & 1 <= k & k < i & ( f /. j,f /. k MP_rule f /. i or f /. j,f /. k IND_rule f /. i ) ) ; ::_thesis: prc f2,X,i + n
then consider j, k being Nat such that
A8: 1 <= j and
A9: j < i and
A10: 1 <= k and
A11: k < i and
A12: ( f /. j,f /. k MP_rule f /. i or f /. j,f /. k IND_rule f /. i ) ;
A13: ( 1 <= j + n & j + n < i + n ) by A8, A9, NAT_1:12, XREAL_1:8;
A14: k <= len f by A4, A11, XXREAL_0:2;
then k + n <= (len f) + n by XREAL_1:6;
then A15: k + n <= len f2 by A1, XXREAL_0:2;
A16: j <= len f by A4, A9, XXREAL_0:2;
then j + n <= (len f) + n by XREAL_1:6;
then A17: j + n <= len f2 by A1, XXREAL_0:2;
A18: f /. k = f . k by A10, A14, Lm1
.= f2 . (k + n) by A2, A10, A14
.= f2 /. (k + n) by A10, A15, Lm1, NAT_1:12 ;
A19: ( 1 <= k + n & k + n < i + n ) by A10, A11, NAT_1:12, XREAL_1:8;
f /. j = f . j by A8, A16, Lm1
.= f2 . (j + n) by A2, A8, A16
.= f2 /. (j + n) by A8, A17, Lm1, NAT_1:12 ;
hence prc f2,X,i + n by A6, A12, A13, A19, A18, Def29; ::_thesis: verum
end;
suppose ex j being Nat st
( 1 <= j & j < i & f /. j NEX_rule f /. i ) ; ::_thesis: prc f2,X,i + n
then consider j being Nat such that
A20: 1 <= j and
A21: j < i and
A22: f /. j NEX_rule f /. i ;
A23: ( 1 <= j + n & j + n < i + n ) by A20, A21, NAT_1:12, XREAL_1:8;
A24: j <= len f by A4, A21, XXREAL_0:2;
then j + n <= (len f) + n by XREAL_1:6;
then A25: j + n <= len f2 by A1, XXREAL_0:2;
f /. j = f . j by A20, A24, Lm1
.= f2 . (j + n) by A2, A20, A24
.= f2 /. (j + n) by A20, A25, Lm1, NAT_1:12 ;
hence prc f2,X,i + n by A6, A22, A23, Def29; ::_thesis: verum
end;
end;
end;
theorem Th39: :: LTLAXIO1:39
for X being Subset of LTLB_WFF
for f2, f, f1 being FinSequence of LTLB_WFF st f2 = f ^ f1 & 1 <= len f & 1 <= len f1 & ( for i being Nat st 1 <= i & i <= len f holds
prc f,X,i ) & ( for i being Nat st 1 <= i & i <= len f1 holds
prc f1,X,i ) holds
for i being Nat st 1 <= i & i <= len f2 holds
prc f2,X,i
proof
let X be Subset of LTLB_WFF; ::_thesis: for f2, f, f1 being FinSequence of LTLB_WFF st f2 = f ^ f1 & 1 <= len f & 1 <= len f1 & ( for i being Nat st 1 <= i & i <= len f holds
prc f,X,i ) & ( for i being Nat st 1 <= i & i <= len f1 holds
prc f1,X,i ) holds
for i being Nat st 1 <= i & i <= len f2 holds
prc f2,X,i
let f2, f, f1 be FinSequence of LTLB_WFF ; ::_thesis: ( f2 = f ^ f1 & 1 <= len f & 1 <= len f1 & ( for i being Nat st 1 <= i & i <= len f holds
prc f,X,i ) & ( for i being Nat st 1 <= i & i <= len f1 holds
prc f1,X,i ) implies for i being Nat st 1 <= i & i <= len f2 holds
prc f2,X,i )
assume that
A1: f2 = f ^ f1 and
1 <= len f and
1 <= len f1 and
A2: for i being Nat st 1 <= i & i <= len f holds
prc f,X,i and
A3: for i being Nat st 1 <= i & i <= len f1 holds
prc f1,X,i ; ::_thesis: for i being Nat st 1 <= i & i <= len f2 holds
prc f2,X,i
A4: len f2 = (len f) + (len f1) by A1, FINSEQ_1:22;
A5: for k being Nat st 1 <= k & k <= len f1 holds
f1 . k = f2 . (k + (len f)) by A1, FINSEQ_1:65;
let i be Nat; ::_thesis: ( 1 <= i & i <= len f2 implies prc f2,X,i )
assume that
A6: 1 <= i and
A7: i <= len f2 ; ::_thesis: prc f2,X,i
percases ( i <= len f or (len f) + 1 <= i ) by NAT_1:13;
supposeA8: i <= len f ; ::_thesis: prc f2,X,i
then A9: f /. i = f . i by A6, Lm1
.= f2 . i by A1, A6, A8, FINSEQ_1:64
.= f2 /. i by A6, A7, Lm1 ;
A10: prc f,X,i by A2, A6, A8;
percases ( f . i in LTL_axioms or f . i in X or ex j, k being Nat st
( 1 <= j & j < i & 1 <= k & k < i & ( f /. j,f /. k MP_rule f /. i or f /. j,f /. k IND_rule f /. i ) ) or ex j being Nat st
( 1 <= j & j < i & f /. j NEX_rule f /. i ) ) by A10, Def29;
suppose f . i in LTL_axioms ; ::_thesis: prc f2,X,i
then f2 . i in LTL_axioms by A1, A6, A8, FINSEQ_1:64;
hence prc f2,X,i by Def29; ::_thesis: verum
end;
suppose f . i in X ; ::_thesis: prc f2,X,i
then f2 . i in X by A1, A6, A8, FINSEQ_1:64;
hence prc f2,X,i by Def29; ::_thesis: verum
end;
suppose ex j, k being Nat st
( 1 <= j & j < i & 1 <= k & k < i & ( f /. j,f /. k MP_rule f /. i or f /. j,f /. k IND_rule f /. i ) ) ; ::_thesis: prc f2,X,i
then consider j, k being Nat such that
A11: 1 <= j and
A12: j < i and
A13: 1 <= k and
A14: k < i and
A15: ( f /. j,f /. k MP_rule f /. i or f /. j,f /. k IND_rule f /. i ) ;
A16: k <= len f by A8, A14, XXREAL_0:2;
then A17: k <= len f2 by A4, NAT_1:12;
A18: f /. k = f . k by A13, A16, Lm1
.= f2 . k by A1, A13, A16, FINSEQ_1:64
.= f2 /. k by A13, A17, Lm1 ;
A19: j <= len f by A8, A12, XXREAL_0:2;
then A20: j <= len f2 by A4, NAT_1:12;
f /. j = f . j by A11, A19, Lm1
.= f2 . j by A1, A11, A19, FINSEQ_1:64
.= f2 /. j by A11, A20, Lm1 ;
hence prc f2,X,i by A9, A11, A12, A13, A14, A15, A18, Def29; ::_thesis: verum
end;
suppose ex j being Nat st
( 1 <= j & j < i & f /. j NEX_rule f /. i ) ; ::_thesis: prc f2,X,i
then consider j being Nat such that
A21: 1 <= j and
A22: j < i and
A23: f /. j NEX_rule f /. i ;
A24: j <= len f by A8, A22, XXREAL_0:2;
then A25: j <= len f2 by A4, NAT_1:12;
f /. j = f . j by A21, A24, Lm1
.= f2 . j by A1, A21, A24, FINSEQ_1:64
.= f2 /. j by A21, A25, Lm1 ;
hence prc f2,X,i by A9, A21, A22, A23, Def29; ::_thesis: verum
end;
end;
end;
supposeA26: (len f) + 1 <= i ; ::_thesis: prc f2,X,i
set i1 = i -' (len f);
i <= (len f) + (len f1) by A1, A7, FINSEQ_1:22;
then i -' (len f) <= ((len f) + (len f1)) -' (len f) by NAT_D:42;
then A27: i -' (len f) <= len f1 by NAT_D:34;
1 <= i -' (len f) by A26, NAT_D:55;
then prc f2,X,(i -' (len f)) + (len f) by A3, A4, A5, A27, Th38;
hence prc f2,X,i by A26, NAT_D:43, NAT_D:55; ::_thesis: verum
end;
end;
end;
theorem Th40: :: LTLAXIO1:40
for p being Element of LTLB_WFF
for X being Subset of LTLB_WFF
for f, f1 being FinSequence of LTLB_WFF st f = f1 ^ <*p*> & 1 <= len f1 & ( for i being Nat st 1 <= i & i <= len f1 holds
prc f1,X,i ) & prc f,X, len f holds
( ( for i being Nat st 1 <= i & i <= len f holds
prc f,X,i ) & X |- p )
proof
let p be Element of LTLB_WFF ; ::_thesis: for X being Subset of LTLB_WFF
for f, f1 being FinSequence of LTLB_WFF st f = f1 ^ <*p*> & 1 <= len f1 & ( for i being Nat st 1 <= i & i <= len f1 holds
prc f1,X,i ) & prc f,X, len f holds
( ( for i being Nat st 1 <= i & i <= len f holds
prc f,X,i ) & X |- p )
let X be Subset of LTLB_WFF; ::_thesis: for f, f1 being FinSequence of LTLB_WFF st f = f1 ^ <*p*> & 1 <= len f1 & ( for i being Nat st 1 <= i & i <= len f1 holds
prc f1,X,i ) & prc f,X, len f holds
( ( for i being Nat st 1 <= i & i <= len f holds
prc f,X,i ) & X |- p )
let f, f1 be FinSequence of LTLB_WFF ; ::_thesis: ( f = f1 ^ <*p*> & 1 <= len f1 & ( for i being Nat st 1 <= i & i <= len f1 holds
prc f1,X,i ) & prc f,X, len f implies ( ( for i being Nat st 1 <= i & i <= len f holds
prc f,X,i ) & X |- p ) )
assume that
A1: f = f1 ^ <*p*> and
1 <= len f1 and
A2: for i being Nat st 1 <= i & i <= len f1 holds
prc f1,X,i ; ::_thesis: ( not prc f,X, len f or ( ( for i being Nat st 1 <= i & i <= len f holds
prc f,X,i ) & X |- p ) )
A3: len f = (len f1) + (len <*p*>) by A1, FINSEQ_1:22
.= (len f1) + 1 by FINSEQ_1:39 ;
then A4: 1 <= len f by XREAL_1:31;
assume A5: prc f,X, len f ; ::_thesis: ( ( for i being Nat st 1 <= i & i <= len f holds
prc f,X,i ) & X |- p )
A6: 0 + (len f1) <= len f by A3, NAT_1:12;
A7: now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<=_len_f_holds_
prc_f,X,i
let i be Nat; ::_thesis: ( 1 <= i & i <= len f implies prc f,X,b1 )
assume that
A8: 1 <= i and
A9: i <= len f ; ::_thesis: prc f,X,b1
A10: ( i < (len f1) + 1 or i = (len f1) + 1 ) by A3, A9, XXREAL_0:1;
A11: for k being Nat st 1 <= k & k <= len f1 holds
f1 . k = f . (k + 0) by A1, FINSEQ_1:64;
percases ( i <= len f1 or i = len f ) by A3, A10, NAT_1:13;
suppose i <= len f1 ; ::_thesis: prc f,X,b1
then prc f,X,i + 0 by A2, A6, A8, A11, Th38;
hence prc f,X,i ; ::_thesis: verum
end;
suppose i = len f ; ::_thesis: prc f,X,b1
hence prc f,X,i by A5; ::_thesis: verum
end;
end;
end;
hence for i being Nat st 1 <= i & i <= len f holds
prc f,X,i ; ::_thesis: X |- p
f . (len f) = f . ((len f1) + (len <*p*>)) by A1, FINSEQ_1:22
.= f . ((len f1) + 1) by FINSEQ_1:39
.= p by A1, FINSEQ_1:42 ;
hence X |- p by A4, A7, Def30; ::_thesis: verum
end;
theorem :: LTLAXIO1:41
for A being Element of LTLB_WFF
for F being Subset of LTLB_WFF st F |- A holds
F |= A
proof
let A be Element of LTLB_WFF ; ::_thesis: for F being Subset of LTLB_WFF st F |- A holds
F |= A
let F be Subset of LTLB_WFF; ::_thesis: ( F |- A implies F |= A )
assume F |- A ; ::_thesis: F |= A
then consider f being FinSequence of LTLB_WFF such that
A1: f . (len f) = A and
A2: 1 <= len f and
A3: for i being Nat st 1 <= i & i <= len f holds
prc f,F,i by Def30;
defpred S1[ Nat] means ( 1 <= $1 & $1 <= len f implies F |= f /. $1 );
A4: for i being Nat st ( for j being Nat st j < i holds
S1[j] ) holds
S1[i]
proof
let i be Nat; ::_thesis: ( ( for j being Nat st j < i holds
S1[j] ) implies S1[i] )
assume A5: for j being Nat st j < i holds
S1[j] ; ::_thesis: S1[i]
percases ( i = 0 or not i < 1 ) by NAT_1:14;
suppose i = 0 ; ::_thesis: S1[i]
hence S1[i] ; ::_thesis: verum
end;
suppose not i < 1 ; ::_thesis: S1[i]
assume that
A6: 1 <= i and
A7: i <= len f ; ::_thesis: F |= f /. i
A8: prc f,F,i by A3, A6, A7;
percases ( f . i in LTL_axioms or f . i in F or ex j, k being Nat st
( 1 <= j & j < i & 1 <= k & k < i & ( f /. j,f /. k MP_rule f /. i or f /. j,f /. k IND_rule f /. i ) ) or ex j being Nat st
( 1 <= j & j < i & f /. j NEX_rule f /. i ) ) by A8, Def29;
suppose f . i in LTL_axioms ; ::_thesis: F |= f /. i
then A9: f /. i in LTL_axioms by A6, A7, Lm1;
percases ( f /. i is LTL_TAUT_OF_PL or f /. i is axltl1 or f /. i is axltl1a or f /. i is axltl2 or f /. i is axltl3 or f /. i is axltl4 or f /. i is axltl5 or f /. i is axltl6 ) by A9, Th36;
suppose f /. i is LTL_TAUT_OF_PL ; ::_thesis: F |= f /. i
hence F |= f /. i by Th33; ::_thesis: verum
end;
suppose ( f /. i is axltl1 or f /. i is axltl1a or f /. i is axltl2 or f /. i is axltl3 or f /. i is axltl4 or f /. i is axltl5 or f /. i is axltl6 ) ; ::_thesis: F |= f /. i
hence F |= f /. i by Th37; ::_thesis: verum
end;
end;
end;
suppose f . i in F ; ::_thesis: F |= f /. i
then A10: f /. i in F by A6, A7, Lm1;
thus F |= f /. i ::_thesis: verum
proof
let M be LTLModel; :: according to LTLAXIO1:def_14 ::_thesis: ( M |= F implies M |= f /. i )
assume M |= F ; ::_thesis: M |= f /. i
hence M |= f /. i by A10, Def13; ::_thesis: verum
end;
end;
suppose ex j, k being Nat st
( 1 <= j & j < i & 1 <= k & k < i & ( f /. j,f /. k MP_rule f /. i or f /. j,f /. k IND_rule f /. i ) ) ; ::_thesis: F |= f /. i
then consider j, k being Nat such that
A11: 1 <= j and
A12: j < i and
A13: 1 <= k and
A14: k < i and
A15: ( f /. j,f /. k MP_rule f /. i or f /. j,f /. k IND_rule f /. i ) ;
k <= len f by A7, A14, XXREAL_0:2;
then A16: F |= f /. k by A5, A13, A14;
A17: j <= len f by A7, A12, XXREAL_0:2;
percases ( f /. j,f /. k MP_rule f /. i or f /. j,f /. k IND_rule f /. i ) by A15;
suppose f /. j,f /. k MP_rule f /. i ; ::_thesis: F |= f /. i
then F |= (f /. j) => (f /. i) by A16, Def20;
hence F |= f /. i by A5, A11, A12, A17, Th24; ::_thesis: verum
end;
suppose f /. j,f /. k IND_rule f /. i ; ::_thesis: F |= f /. i
then consider A, B being Element of LTLB_WFF such that
A18: f /. j = A => B and
A19: ( f /. k = A => ('X' A) & f /. i = A => ('G' B) ) by Def21;
F |= A => B by A5, A11, A12, A17, A18;
hence F |= f /. i by A16, A19, Th27; ::_thesis: verum
end;
end;
end;
suppose ex j being Nat st
( 1 <= j & j < i & f /. j NEX_rule f /. i ) ; ::_thesis: F |= f /. i
then consider j being Nat such that
A20: 1 <= j and
A21: j < i and
A22: f /. j NEX_rule f /. i ;
S1[j] by A5, A21;
then F |= 'X' (f /. j) by A7, A20, A21, Th25, XXREAL_0:2;
hence F |= f /. i by A22, Def19; ::_thesis: verum
end;
end;
end;
end;
end;
A23: for i being Nat holds S1[i] from NAT_1:sch_4(A4);
f /. (len f) = A by A1, A2, Lm1;
hence F |= A by A2, A23; ::_thesis: verum
end;
begin
theorem Th42: :: LTLAXIO1:42
for p being Element of LTLB_WFF
for X being Subset of LTLB_WFF st ( p in LTL_axioms or p in X ) holds
X |- p
proof
let p be Element of LTLB_WFF ; ::_thesis: for X being Subset of LTLB_WFF st ( p in LTL_axioms or p in X ) holds
X |- p
let X be Subset of LTLB_WFF; ::_thesis: ( ( p in LTL_axioms or p in X ) implies X |- p )
defpred S1[ set , set ] means $2 = p;
A1: for k being Nat st k in Seg 1 holds
ex x being Element of LTLB_WFF st S1[k,x] ;
consider g being FinSequence of LTLB_WFF such that
A2: ( dom g = Seg 1 & ( for k being Nat st k in Seg 1 holds
S1[k,g . k] ) ) from FINSEQ_1:sch_5(A1);
A3: len g = 1 by A2, FINSEQ_1:def_3;
1 in Seg 1 by FINSEQ_1:2, TARSKI:def_1;
then A4: g . 1 = p by A2;
assume A5: ( p in LTL_axioms or p in X ) ; ::_thesis: X |- p
for j being Nat st 1 <= j & j <= len g holds
prc g,X,j
proof
let j be Nat; ::_thesis: ( 1 <= j & j <= len g implies prc g,X,j )
assume A6: ( 1 <= j & j <= len g ) ; ::_thesis: prc g,X,j
percases ( p in LTL_axioms or p in X ) by A5;
suppose p in LTL_axioms ; ::_thesis: prc g,X,j
then g . j in LTL_axioms by A3, A4, A6, XXREAL_0:1;
hence prc g,X,j by Def29; ::_thesis: verum
end;
suppose p in X ; ::_thesis: prc g,X,j
then g . j in X by A3, A4, A6, XXREAL_0:1;
hence prc g,X,j by Def29; ::_thesis: verum
end;
end;
end;
hence X |- p by A3, A4, Def30; ::_thesis: verum
end;
theorem Th43: :: LTLAXIO1:43
for p, q being Element of LTLB_WFF
for X being Subset of LTLB_WFF st X |- p & X |- p => q holds
X |- q
proof
let p, q be Element of LTLB_WFF ; ::_thesis: for X being Subset of LTLB_WFF st X |- p & X |- p => q holds
X |- q
let X be Subset of LTLB_WFF; ::_thesis: ( X |- p & X |- p => q implies X |- q )
assume X |- p ; ::_thesis: ( not X |- p => q or X |- q )
then consider f being FinSequence of LTLB_WFF such that
A1: f . (len f) = p and
A2: 1 <= len f and
A3: for i being Nat st 1 <= i & i <= len f holds
prc f,X,i by Def30;
set j = len f;
assume X |- p => q ; ::_thesis: X |- q
then consider f1 being FinSequence of LTLB_WFF such that
A4: f1 . (len f1) = p => q and
A5: 1 <= len f1 and
A6: for i being Nat st 1 <= i & i <= len f1 holds
prc f1,X,i by Def30;
A7: 1 <= (len f) + (len f1) by A2, NAT_1:12;
set g = (f ^ f1) ^ <*q*>;
A8: (f ^ f1) ^ <*q*> = f ^ (f1 ^ <*q*>) by FINSEQ_1:32;
A9: for i being Nat st 1 <= i & i <= len f1 holds
((f ^ f1) ^ <*q*>) . ((len f) + i) = f1 . i
proof
let i be Nat; ::_thesis: ( 1 <= i & i <= len f1 implies ((f ^ f1) ^ <*q*>) . ((len f) + i) = f1 . i )
assume that
A10: 1 <= i and
A11: i <= len f1 ; ::_thesis: ((f ^ f1) ^ <*q*>) . ((len f) + i) = f1 . i
len (f1 ^ <*q*>) = (len f1) + (len <*q*>) by FINSEQ_1:22
.= (len f1) + 1 by FINSEQ_1:39 ;
then i <= len (f1 ^ <*q*>) by A11, NAT_1:12;
hence ((f ^ f1) ^ <*q*>) . ((len f) + i) = (f1 ^ <*q*>) . i by A8, A10, FINSEQ_1:65
.= f1 . i by A10, A11, FINSEQ_1:64 ;
::_thesis: verum
end;
A12: len ((f ^ f1) ^ <*q*>) = (len (f ^ f1)) + (len <*q*>) by FINSEQ_1:22
.= (len (f ^ f1)) + 1 by FINSEQ_1:39 ;
then A13: len ((f ^ f1) ^ <*q*>) = ((len f) + (len f1)) + 1 by FINSEQ_1:22;
then len ((f ^ f1) ^ <*q*>) = (len f) + ((len f1) + 1) ;
then A14: len f < len ((f ^ f1) ^ <*q*>) by NAT_1:16;
then A15: ((f ^ f1) ^ <*q*>) /. (len f) = ((f ^ f1) ^ <*q*>) . (len f) by A2, Lm1
.= p by A1, A2, A8, FINSEQ_1:64 ;
set k = (len f) + (len f1);
A16: 1 <= (len f) + (len f1) by A2, NAT_1:12;
( ((f ^ f1) ^ <*q*>) . (len ((f ^ f1) ^ <*q*>)) = q & 1 <= len ((f ^ f1) ^ <*q*>) ) by A12, FINSEQ_1:42, NAT_1:11;
then A17: ((f ^ f1) ^ <*q*>) /. (len ((f ^ f1) ^ <*q*>)) = q by Lm1;
A18: (len f) + (len f1) < len ((f ^ f1) ^ <*q*>) by A13, NAT_1:16;
then ((f ^ f1) ^ <*q*>) /. ((len f) + (len f1)) = ((f ^ f1) ^ <*q*>) . ((len f) + (len f1)) by A2, Lm1, NAT_1:12
.= p => q by A4, A5, A9 ;
then ((f ^ f1) ^ <*q*>) /. (len f),((f ^ f1) ^ <*q*>) /. ((len f) + (len f1)) MP_rule ((f ^ f1) ^ <*q*>) /. (len ((f ^ f1) ^ <*q*>)) by A15, A17, Def20;
then A19: ( len (f ^ f1) = (len f) + (len f1) & prc (f ^ f1) ^ <*q*>,X, len ((f ^ f1) ^ <*q*>) ) by A2, A14, A16, A18, Def29, FINSEQ_1:22;
for i being Nat st 1 <= i & i <= len (f ^ f1) holds
prc f ^ f1,X,i by A2, A3, A5, A6, Th39;
hence X |- q by A7, A19, Th40; ::_thesis: verum
end;
theorem Th44: :: LTLAXIO1:44
for p being Element of LTLB_WFF
for X being Subset of LTLB_WFF st X |- p holds
X |- 'X' p
proof
let p be Element of LTLB_WFF ; ::_thesis: for X being Subset of LTLB_WFF st X |- p holds
X |- 'X' p
let X be Subset of LTLB_WFF; ::_thesis: ( X |- p implies X |- 'X' p )
assume X |- p ; ::_thesis: X |- 'X' p
then consider f being FinSequence of LTLB_WFF such that
A1: f . (len f) = p and
A2: 1 <= len f and
A3: for i being Nat st 1 <= i & i <= len f holds
prc f,X,i by Def30;
set g = f ^ <*('X' p)*>;
A4: len (f ^ <*('X' p)*>) = (len f) + (len <*('X' p)*>) by FINSEQ_1:22
.= (len f) + 1 by FINSEQ_1:39 ;
then A5: len f < len (f ^ <*('X' p)*>) by NAT_1:16;
then A6: (f ^ <*('X' p)*>) /. (len f) = (f ^ <*('X' p)*>) . (len f) by A2, Lm1
.= p by A1, A2, FINSEQ_1:64 ;
1 <= len (f ^ <*('X' p)*>) by A2, A4, NAT_1:16;
then (f ^ <*('X' p)*>) /. (len (f ^ <*('X' p)*>)) = (f ^ <*('X' p)*>) . (len (f ^ <*('X' p)*>)) by Lm1
.= 'X' ((f ^ <*('X' p)*>) /. (len f)) by A4, A6, FINSEQ_1:42 ;
then (f ^ <*('X' p)*>) /. (len f) NEX_rule (f ^ <*('X' p)*>) /. (len (f ^ <*('X' p)*>)) by Def19;
then prc f ^ <*('X' p)*>,X, len (f ^ <*('X' p)*>) by A2, A5, Def29;
hence X |- 'X' p by A2, A3, Th40; ::_thesis: verum
end;
theorem Th45: :: LTLAXIO1:45
for p, q being Element of LTLB_WFF
for X being Subset of LTLB_WFF st X |- p => q & X |- p => ('X' p) holds
X |- p => ('G' q)
proof
let p, q be Element of LTLB_WFF ; ::_thesis: for X being Subset of LTLB_WFF st X |- p => q & X |- p => ('X' p) holds
X |- p => ('G' q)
let X be Subset of LTLB_WFF; ::_thesis: ( X |- p => q & X |- p => ('X' p) implies X |- p => ('G' q) )
assume that
A1: X |- p => q and
A2: X |- p => ('X' p) ; ::_thesis: X |- p => ('G' q)
consider f being FinSequence of LTLB_WFF such that
A3: f . (len f) = p => q and
A4: 1 <= len f and
A5: for i being Nat st 1 <= i & i <= len f holds
prc f,X,i by A1, Def30;
consider g being FinSequence of LTLB_WFF such that
A6: g . (len g) = p => ('X' p) and
A7: 1 <= len g and
A8: for i being Nat st 1 <= i & i <= len g holds
prc g,X,i by A2, Def30;
A9: for i being Nat st 1 <= i & i <= len (f ^ g) holds
prc f ^ g,X,i by A4, A5, A7, A8, Th39;
set h = (f ^ g) ^ <*(p => ('G' q))*>;
A10: (f ^ g) ^ <*(p => ('G' q))*> = f ^ (g ^ <*(p => ('G' q))*>) by FINSEQ_1:32;
A11: len (f ^ g) = (len f) + (len g) by FINSEQ_1:22;
then A12: 1 <= len (f ^ g) by A4, NAT_1:12;
A13: len ((f ^ g) ^ <*(p => ('G' q))*>) = (len (f ^ g)) + (len <*(p => ('G' q))*>) by FINSEQ_1:22
.= (len (f ^ g)) + 1 by FINSEQ_1:39 ;
then 1 <= len ((f ^ g) ^ <*(p => ('G' q))*>) by A4, A11, NAT_1:16;
then A14: ((f ^ g) ^ <*(p => ('G' q))*>) /. (len ((f ^ g) ^ <*(p => ('G' q))*>)) = ((f ^ g) ^ <*(p => ('G' q))*>) . (len ((f ^ g) ^ <*(p => ('G' q))*>)) by Lm1
.= p => ('G' q) by A13, FINSEQ_1:42 ;
len ((f ^ g) ^ <*(p => ('G' q))*>) = (len f) + ((len g) + 1) by A11, A13;
then A15: len f < len ((f ^ g) ^ <*(p => ('G' q))*>) by NAT_1:16;
then A16: ((f ^ g) ^ <*(p => ('G' q))*>) /. (len f) = ((f ^ g) ^ <*(p => ('G' q))*>) . (len f) by A4, Lm1
.= p => q by A3, A4, A10, FINSEQ_1:64 ;
A17: len (f ^ g) < len ((f ^ g) ^ <*(p => ('G' q))*>) by A13, NAT_1:16;
then ((f ^ g) ^ <*(p => ('G' q))*>) /. (len (f ^ g)) = ((f ^ g) ^ <*(p => ('G' q))*>) . (len (f ^ g)) by A12, Lm1
.= (f ^ g) . (len (f ^ g)) by A12, FINSEQ_1:64
.= (f ^ g) . ((len f) + (len g)) by FINSEQ_1:22
.= p => ('X' p) by A6, A7, FINSEQ_1:65 ;
then ((f ^ g) ^ <*(p => ('G' q))*>) /. (len f),((f ^ g) ^ <*(p => ('G' q))*>) /. (len (f ^ g)) IND_rule ((f ^ g) ^ <*(p => ('G' q))*>) /. (len ((f ^ g) ^ <*(p => ('G' q))*>)) by A16, A14, Def21;
then prc (f ^ g) ^ <*(p => ('G' q))*>,X, len ((f ^ g) ^ <*(p => ('G' q))*>) by A4, A12, A15, A17, Def29;
hence X |- p => ('G' q) by A12, A9, Th40; ::_thesis: verum
end;
theorem Th46: :: LTLAXIO1:46
for r, p, q being Element of LTLB_WFF
for X being Subset of LTLB_WFF st X |- r => (p '&&' q) holds
( X |- r => p & X |- r => q )
proof
let r, p, q be Element of LTLB_WFF ; ::_thesis: for X being Subset of LTLB_WFF st X |- r => (p '&&' q) holds
( X |- r => p & X |- r => q )
let X be Subset of LTLB_WFF; ::_thesis: ( X |- r => (p '&&' q) implies ( X |- r => p & X |- r => q ) )
assume A1: X |- r => (p '&&' q) ; ::_thesis: ( X |- r => p & X |- r => q )
set A = (r => (p '&&' q)) => (r => p);
(r => (p '&&' q)) => (r => p) is LTL_TAUT_OF_PL
proof
let f be Function of LTLB_WFF,BOOLEAN; :: according to LTLAXIO1:def_16 ::_thesis: (VAL f) . ((r => (p '&&' q)) => (r => p)) = 1
thus (VAL f) . ((r => (p '&&' q)) => (r => p)) = ((VAL f) . (r => (p '&&' q))) => ((VAL f) . (r => p)) by Def15
.= (((VAL f) . r) => ((VAL f) . (p '&&' q))) => ((VAL f) . (r => p)) by Def15
.= (((VAL f) . r) => (((VAL f) . p) '&' ((VAL f) . q))) => ((VAL f) . (r => p)) by Th31
.= (((VAL f) . r) => (((VAL f) . p) '&' ((VAL f) . q))) => (((VAL f) . r) => ((VAL f) . p)) by Def15
.= 1 by Th1 ; ::_thesis: verum
end;
then (r => (p '&&' q)) => (r => p) in LTL_axioms by Def17;
then X |- (r => (p '&&' q)) => (r => p) by Th42;
hence X |- r => p by A1, Th43; ::_thesis: X |- r => q
set A = (r => (p '&&' q)) => (r => q);
(r => (p '&&' q)) => (r => q) is LTL_TAUT_OF_PL
proof
let f be Function of LTLB_WFF,BOOLEAN; :: according to LTLAXIO1:def_16 ::_thesis: (VAL f) . ((r => (p '&&' q)) => (r => q)) = 1
thus (VAL f) . ((r => (p '&&' q)) => (r => q)) = ((VAL f) . (r => (p '&&' q))) => ((VAL f) . (r => q)) by Def15
.= (((VAL f) . r) => ((VAL f) . (p '&&' q))) => ((VAL f) . (r => q)) by Def15
.= (((VAL f) . r) => (((VAL f) . p) '&' ((VAL f) . q))) => ((VAL f) . (r => q)) by Th31
.= (((VAL f) . r) => (((VAL f) . p) '&' ((VAL f) . q))) => (((VAL f) . r) => ((VAL f) . q)) by Def15
.= 1 by Th1 ; ::_thesis: verum
end;
then (r => (p '&&' q)) => (r => q) in LTL_axioms by Def17;
then X |- (r => (p '&&' q)) => (r => q) by Th42;
hence X |- r => q by A1, Th43; ::_thesis: verum
end;
theorem Th47: :: LTLAXIO1:47
for p, q, r being Element of LTLB_WFF
for X being Subset of LTLB_WFF st X |- p => q & X |- q => r holds
X |- p => r
proof
let p, q, r be Element of LTLB_WFF ; ::_thesis: for X being Subset of LTLB_WFF st X |- p => q & X |- q => r holds
X |- p => r
let X be Subset of LTLB_WFF; ::_thesis: ( X |- p => q & X |- q => r implies X |- p => r )
assume that
A1: X |- p => q and
A2: X |- q => r ; ::_thesis: X |- p => r
set A = (p => q) => ((q => r) => (p => r));
now__::_thesis:_for_f_being_Function_of_LTLB_WFF,BOOLEAN_holds_(VAL_f)_._((p_=>_q)_=>_((q_=>_r)_=>_(p_=>_r)))_=_1
let f be Function of LTLB_WFF,BOOLEAN; ::_thesis: (VAL f) . ((p => q) => ((q => r) => (p => r))) = 1
thus (VAL f) . ((p => q) => ((q => r) => (p => r))) = ((VAL f) . (p => q)) => ((VAL f) . ((q => r) => (p => r))) by Def15
.= (((VAL f) . p) => ((VAL f) . q)) => ((VAL f) . ((q => r) => (p => r))) by Def15
.= (((VAL f) . p) => ((VAL f) . q)) => (((VAL f) . (q => r)) => ((VAL f) . (p => r))) by Def15
.= (((VAL f) . p) => ((VAL f) . q)) => ((((VAL f) . q) => ((VAL f) . r)) => ((VAL f) . (p => r))) by Def15
.= (((VAL f) . p) => ((VAL f) . q)) => ((((VAL f) . q) => ((VAL f) . r)) => (((VAL f) . p) => ((VAL f) . r))) by Def15
.= 1 by XBOOLEAN:106 ; ::_thesis: verum
end;
then (p => q) => ((q => r) => (p => r)) is LTL_TAUT_OF_PL by Def16;
then (p => q) => ((q => r) => (p => r)) in LTL_axioms by Def17;
then X |- (p => q) => ((q => r) => (p => r)) by Th42;
then X |- (q => r) => (p => r) by A1, Th43;
hence X |- p => r by A2, Th43; ::_thesis: verum
end;
theorem Th48: :: LTLAXIO1:48
for p, q, r being Element of LTLB_WFF
for X being Subset of LTLB_WFF st X |- p => (q => r) holds
X |- (p '&&' q) => r
proof
let p, q, r be Element of LTLB_WFF ; ::_thesis: for X being Subset of LTLB_WFF st X |- p => (q => r) holds
X |- (p '&&' q) => r
let X be Subset of LTLB_WFF; ::_thesis: ( X |- p => (q => r) implies X |- (p '&&' q) => r )
set A = (p => (q => r)) => ((p '&&' q) => r);
now__::_thesis:_for_f_being_Function_of_LTLB_WFF,BOOLEAN_holds_(VAL_f)_._((p_=>_(q_=>_r))_=>_((p_'&&'_q)_=>_r))_=_1
let f be Function of LTLB_WFF,BOOLEAN; ::_thesis: (VAL f) . ((p => (q => r)) => ((p '&&' q) => r)) = 1
thus (VAL f) . ((p => (q => r)) => ((p '&&' q) => r)) = ((VAL f) . (p => (q => r))) => ((VAL f) . ((p '&&' q) => r)) by Def15
.= (((VAL f) . p) => ((VAL f) . (q => r))) => ((VAL f) . ((p '&&' q) => r)) by Def15
.= (((VAL f) . p) => (((VAL f) . q) => ((VAL f) . r))) => ((VAL f) . ((p '&&' q) => r)) by Def15
.= (((VAL f) . p) => (((VAL f) . q) => ((VAL f) . r))) => (((VAL f) . (p '&&' q)) => ((VAL f) . r)) by Def15
.= (((VAL f) . p) => (((VAL f) . q) => ((VAL f) . r))) => ((((VAL f) . p) '&' ((VAL f) . q)) => ((VAL f) . r)) by Th31
.= 1 by Th2 ; ::_thesis: verum
end;
then (p => (q => r)) => ((p '&&' q) => r) is LTL_TAUT_OF_PL by Def16;
then (p => (q => r)) => ((p '&&' q) => r) in LTL_axioms by Def17;
then A1: X |- (p => (q => r)) => ((p '&&' q) => r) by Th42;
assume X |- p => (q => r) ; ::_thesis: X |- (p '&&' q) => r
hence X |- (p '&&' q) => r by A1, Th43; ::_thesis: verum
end;
theorem Th49: :: LTLAXIO1:49
for p, q, r being Element of LTLB_WFF
for X being Subset of LTLB_WFF st X |- (p '&&' q) => r holds
X |- p => (q => r)
proof
let p, q, r be Element of LTLB_WFF ; ::_thesis: for X being Subset of LTLB_WFF st X |- (p '&&' q) => r holds
X |- p => (q => r)
let X be Subset of LTLB_WFF; ::_thesis: ( X |- (p '&&' q) => r implies X |- p => (q => r) )
set A = ((p '&&' q) => r) => (p => (q => r));
now__::_thesis:_for_f_being_Function_of_LTLB_WFF,BOOLEAN_holds_(VAL_f)_._(((p_'&&'_q)_=>_r)_=>_(p_=>_(q_=>_r)))_=_1
let f be Function of LTLB_WFF,BOOLEAN; ::_thesis: (VAL f) . (((p '&&' q) => r) => (p => (q => r))) = 1
thus (VAL f) . (((p '&&' q) => r) => (p => (q => r))) = ((VAL f) . ((p '&&' q) => r)) => ((VAL f) . (p => (q => r))) by Def15
.= (((VAL f) . (p '&&' q)) => ((VAL f) . r)) => ((VAL f) . (p => (q => r))) by Def15
.= ((((VAL f) . p) '&' ((VAL f) . q)) => ((VAL f) . r)) => ((VAL f) . (p => (q => r))) by Th31
.= ((((VAL f) . p) '&' ((VAL f) . q)) => ((VAL f) . r)) => (((VAL f) . p) => ((VAL f) . (q => r))) by Def15
.= ((((VAL f) . p) '&' ((VAL f) . q)) => ((VAL f) . r)) => (((VAL f) . p) => (((VAL f) . q) => ((VAL f) . r))) by Def15
.= 1 by Th3 ; ::_thesis: verum
end;
then ((p '&&' q) => r) => (p => (q => r)) is LTL_TAUT_OF_PL by Def16;
then ((p '&&' q) => r) => (p => (q => r)) in LTL_axioms by Def17;
then A1: X |- ((p '&&' q) => r) => (p => (q => r)) by Th42;
assume X |- (p '&&' q) => r ; ::_thesis: X |- p => (q => r)
hence X |- p => (q => r) by A1, Th43; ::_thesis: verum
end;
theorem Th50: :: LTLAXIO1:50
for p, q, r, s being Element of LTLB_WFF
for X being Subset of LTLB_WFF st X |- (p '&&' q) => r & X |- p => s holds
X |- (p '&&' q) => (s '&&' r)
proof
let p, q, r, s be Element of LTLB_WFF ; ::_thesis: for X being Subset of LTLB_WFF st X |- (p '&&' q) => r & X |- p => s holds
X |- (p '&&' q) => (s '&&' r)
let X be Subset of LTLB_WFF; ::_thesis: ( X |- (p '&&' q) => r & X |- p => s implies X |- (p '&&' q) => (s '&&' r) )
assume that
A1: X |- (p '&&' q) => r and
A2: X |- p => s ; ::_thesis: X |- (p '&&' q) => (s '&&' r)
set A = ((p '&&' q) => r) => ((p => s) => ((p '&&' q) => (s '&&' r)));
now__::_thesis:_for_f_being_Function_of_LTLB_WFF,BOOLEAN_holds_(VAL_f)_._(((p_'&&'_q)_=>_r)_=>_((p_=>_s)_=>_((p_'&&'_q)_=>_(s_'&&'_r))))_=_1
let f be Function of LTLB_WFF,BOOLEAN; ::_thesis: (VAL f) . (((p '&&' q) => r) => ((p => s) => ((p '&&' q) => (s '&&' r)))) = 1
A3: ( (VAL f) . p = 0 or (VAL f) . p = 1 ) by XBOOLEAN:def_3;
A4: ( (VAL f) . q = 0 or (VAL f) . q = 1 ) by XBOOLEAN:def_3;
A5: ( (VAL f) . s = 0 or (VAL f) . s = 1 ) by XBOOLEAN:def_3;
A6: ( (VAL f) . r = 0 or (VAL f) . r = 1 ) by XBOOLEAN:def_3;
thus (VAL f) . (((p '&&' q) => r) => ((p => s) => ((p '&&' q) => (s '&&' r)))) = ((VAL f) . ((p '&&' q) => r)) => ((VAL f) . ((p => s) => ((p '&&' q) => (s '&&' r)))) by Def15
.= (((VAL f) . (p '&&' q)) => ((VAL f) . r)) => ((VAL f) . ((p => s) => ((p '&&' q) => (s '&&' r)))) by Def15
.= ((((VAL f) . p) '&' ((VAL f) . q)) => ((VAL f) . r)) => ((VAL f) . ((p => s) => ((p '&&' q) => (s '&&' r)))) by Th31
.= ((((VAL f) . p) '&' ((VAL f) . q)) => ((VAL f) . r)) => (((VAL f) . (p => s)) => ((VAL f) . ((p '&&' q) => (s '&&' r)))) by Def15
.= ((((VAL f) . p) '&' ((VAL f) . q)) => ((VAL f) . r)) => ((((VAL f) . p) => ((VAL f) . s)) => ((VAL f) . ((p '&&' q) => (s '&&' r)))) by Def15
.= ((((VAL f) . p) '&' ((VAL f) . q)) => ((VAL f) . r)) => ((((VAL f) . p) => ((VAL f) . s)) => (((VAL f) . (p '&&' q)) => ((VAL f) . (s '&&' r)))) by Def15
.= ((((VAL f) . p) '&' ((VAL f) . q)) => ((VAL f) . r)) => ((((VAL f) . p) => ((VAL f) . s)) => ((((VAL f) . p) '&' ((VAL f) . q)) => ((VAL f) . (s '&&' r)))) by Th31
.= 1 by A3, A4, A6, A5, Th31 ; ::_thesis: verum
end;
then ((p '&&' q) => r) => ((p => s) => ((p '&&' q) => (s '&&' r))) is LTL_TAUT_OF_PL by Def16;
then ((p '&&' q) => r) => ((p => s) => ((p '&&' q) => (s '&&' r))) in LTL_axioms by Def17;
then X |- ((p '&&' q) => r) => ((p => s) => ((p '&&' q) => (s '&&' r))) by Th42;
then X |- (p => s) => ((p '&&' q) => (s '&&' r)) by A1, Th43;
hence X |- (p '&&' q) => (s '&&' r) by A2, Th43; ::_thesis: verum
end;
theorem Th51: :: LTLAXIO1:51
for p, q, r, s being Element of LTLB_WFF
for X being Subset of LTLB_WFF st X |- p => (q => r) & X |- r => s holds
X |- p => (q => s)
proof
let p, q, r, s be Element of LTLB_WFF ; ::_thesis: for X being Subset of LTLB_WFF st X |- p => (q => r) & X |- r => s holds
X |- p => (q => s)
let X be Subset of LTLB_WFF; ::_thesis: ( X |- p => (q => r) & X |- r => s implies X |- p => (q => s) )
assume that
A1: X |- p => (q => r) and
A2: X |- r => s ; ::_thesis: X |- p => (q => s)
set A = (p => (q => r)) => ((r => s) => (p => (q => s)));
now__::_thesis:_for_f_being_Function_of_LTLB_WFF,BOOLEAN_holds_(VAL_f)_._((p_=>_(q_=>_r))_=>_((r_=>_s)_=>_(p_=>_(q_=>_s))))_=_1
let f be Function of LTLB_WFF,BOOLEAN; ::_thesis: (VAL f) . ((p => (q => r)) => ((r => s) => (p => (q => s)))) = 1
A3: ( (VAL f) . p = 0 or (VAL f) . p = 1 ) by XBOOLEAN:def_3;
A4: ( (VAL f) . r = 0 or (VAL f) . r = 1 ) by XBOOLEAN:def_3;
set B = (VAL f) . (p => (q => r));
set C = (VAL f) . (r => s);
set D = (VAL f) . (p => (q => s));
A5: ( (VAL f) . q = 0 or (VAL f) . q = 1 ) by XBOOLEAN:def_3;
A6: ( (VAL f) . s = 0 or (VAL f) . s = 1 ) by XBOOLEAN:def_3;
A7: (VAL f) . (p => (q => s)) = ((VAL f) . p) => ((VAL f) . (q => s)) by Def15
.= ((VAL f) . p) => (((VAL f) . q) => ((VAL f) . s)) by Def15 ;
A8: (VAL f) . (p => (q => r)) = ((VAL f) . p) => ((VAL f) . (q => r)) by Def15
.= ((VAL f) . p) => (((VAL f) . q) => ((VAL f) . r)) by Def15 ;
thus (VAL f) . ((p => (q => r)) => ((r => s) => (p => (q => s)))) = ((VAL f) . (p => (q => r))) => ((VAL f) . ((r => s) => (p => (q => s)))) by Def15
.= ((VAL f) . (p => (q => r))) => (((VAL f) . (r => s)) => ((VAL f) . (p => (q => s)))) by Def15
.= 1 by A3, A5, A4, A6, A8, A7, Def15 ; ::_thesis: verum
end;
then (p => (q => r)) => ((r => s) => (p => (q => s))) is LTL_TAUT_OF_PL by Def16;
then (p => (q => r)) => ((r => s) => (p => (q => s))) in LTL_axioms by Def17;
then X |- (p => (q => r)) => ((r => s) => (p => (q => s))) by Th42;
then X |- (r => s) => (p => (q => s)) by A1, Th43;
hence X |- p => (q => s) by A2, Th43; ::_thesis: verum
end;
theorem Th52: :: LTLAXIO1:52
for p, q being Element of LTLB_WFF
for X being Subset of LTLB_WFF st X |- p => q holds
X |- ('not' q) => ('not' p)
proof
let p, q be Element of LTLB_WFF ; ::_thesis: for X being Subset of LTLB_WFF st X |- p => q holds
X |- ('not' q) => ('not' p)
let X be Subset of LTLB_WFF; ::_thesis: ( X |- p => q implies X |- ('not' q) => ('not' p) )
set A = (p => q) => (('not' q) => ('not' p));
now__::_thesis:_for_f_being_Function_of_LTLB_WFF,BOOLEAN_holds_(VAL_f)_._((p_=>_q)_=>_(('not'_q)_=>_('not'_p)))_=_1
let f be Function of LTLB_WFF,BOOLEAN; ::_thesis: (VAL f) . ((p => q) => (('not' q) => ('not' p))) = 1
A1: ( (VAL f) . p = 0 or (VAL f) . p = 1 ) by XBOOLEAN:def_3;
A2: ( (VAL f) . q = 0 or (VAL f) . q = 1 ) by XBOOLEAN:def_3;
thus (VAL f) . ((p => q) => (('not' q) => ('not' p))) = ((VAL f) . (p => q)) => ((VAL f) . (('not' q) => ('not' p))) by Def15
.= (((VAL f) . p) => ((VAL f) . q)) => ((VAL f) . (('not' q) => ('not' p))) by Def15
.= (((VAL f) . p) => ((VAL f) . q)) => (((VAL f) . (q => TFALSUM)) => ((VAL f) . (p => TFALSUM))) by Def15
.= (((VAL f) . p) => ((VAL f) . q)) => ((((VAL f) . q) => ((VAL f) . TFALSUM)) => ((VAL f) . (p => TFALSUM))) by Def15
.= (((VAL f) . p) => ((VAL f) . q)) => ((((VAL f) . q) => FALSE) => ((VAL f) . (p => TFALSUM))) by Def15
.= (((VAL f) . p) => ((VAL f) . q)) => ((((VAL f) . q) => FALSE) => (((VAL f) . p) => ((VAL f) . TFALSUM))) by Def15
.= 1 by A1, A2 ; ::_thesis: verum
end;
then (p => q) => (('not' q) => ('not' p)) is LTL_TAUT_OF_PL by Def16;
then (p => q) => (('not' q) => ('not' p)) in LTL_axioms by Def17;
then A3: X |- (p => q) => (('not' q) => ('not' p)) by Th42;
assume X |- p => q ; ::_thesis: X |- ('not' q) => ('not' p)
hence X |- ('not' q) => ('not' p) by A3, Th43; ::_thesis: verum
end;
theorem Th53: :: LTLAXIO1:53
for p, q being Element of LTLB_WFF
for X being Subset of LTLB_WFF holds X |- (('X' p) '&&' ('X' q)) => ('X' (p '&&' q))
proof
let p, q be Element of LTLB_WFF ; ::_thesis: for X being Subset of LTLB_WFF holds X |- (('X' p) '&&' ('X' q)) => ('X' (p '&&' q))
let X be Subset of LTLB_WFF; ::_thesis: X |- (('X' p) '&&' ('X' q)) => ('X' (p '&&' q))
set Xp = 'X' p;
set nq = 'not' q;
set nXq = 'not' ('X' q);
set Xnq = 'X' ('not' q);
('X' ('not' q)) => ('not' ('X' q)) in LTL_axioms by Def17;
then A1: X |- ('X' ('not' q)) => ('not' ('X' q)) by Th42;
('not' ('X' (p => ('not' q)))) => ('X' ('not' (p => ('not' q)))) in LTL_axioms by Def17;
then A2: X |- ('not' ('X' (p => ('not' q)))) => ('X' ('not' (p => ('not' q)))) by Th42;
('X' (p => ('not' q))) => (('X' p) => ('X' ('not' q))) in LTL_axioms by Def17;
then X |- ('X' (p => ('not' q))) => (('X' p) => ('X' ('not' q))) by Th42;
then X |- ('X' (p => ('not' q))) => (('X' p) => ('not' ('X' q))) by A1, Th51;
then X |- ('not' (('X' p) => ('not' ('X' q)))) => ('not' ('X' (p => ('not' q)))) by Th52;
hence X |- (('X' p) '&&' ('X' q)) => ('X' (p '&&' q)) by A2, Th47; ::_thesis: verum
end;
theorem Th54: :: LTLAXIO1:54
for p being Element of LTLB_WFF
for F being Subset of LTLB_WFF st F |- p holds
F |- 'G' p
proof
let p be Element of LTLB_WFF ; ::_thesis: for F being Subset of LTLB_WFF st F |- p holds
F |- 'G' p
let F be Subset of LTLB_WFF; ::_thesis: ( F |- p implies F |- 'G' p )
assume A1: F |- p ; ::_thesis: F |- 'G' p
p => (p => p) in LTL_axioms by Th34;
then F |- p => (p => p) by Th42;
then A2: F |- p => p by A1, Th43;
('X' p) => (p => ('X' p)) in LTL_axioms by Th34;
then A3: F |- ('X' p) => (p => ('X' p)) by Th42;
F |- 'X' p by A1, Th44;
then F |- p => ('X' p) by A3, Th43;
then F |- p => ('G' p) by A2, Th45;
hence F |- 'G' p by A1, Th43; ::_thesis: verum
end;
theorem Th55: :: LTLAXIO1:55
for p, q being Element of LTLB_WFF
for F being Subset of LTLB_WFF st p => q in F holds
F \/ {p} |- 'G' q
proof
let p, q be Element of LTLB_WFF ; ::_thesis: for F being Subset of LTLB_WFF st p => q in F holds
F \/ {p} |- 'G' q
let F be Subset of LTLB_WFF; ::_thesis: ( p => q in F implies F \/ {p} |- 'G' q )
p in {p} by TARSKI:def_1;
then p in F \/ {p} by XBOOLE_0:def_3;
then A1: F \/ {p} |- p by Th42;
assume p => q in F ; ::_thesis: F \/ {p} |- 'G' q
then p => q in F \/ {p} by XBOOLE_0:def_3;
then F \/ {p} |- p => q by Th42;
then F \/ {p} |- q by A1, Th43;
hence F \/ {p} |- 'G' q by Th54; ::_thesis: verum
end;
theorem Th56: :: LTLAXIO1:56
for q, p being Element of LTLB_WFF
for F being Subset of LTLB_WFF st F |- q holds
F \/ {p} |- q
proof
let q, p be Element of LTLB_WFF ; ::_thesis: for F being Subset of LTLB_WFF st F |- q holds
F \/ {p} |- q
let F be Subset of LTLB_WFF; ::_thesis: ( F |- q implies F \/ {p} |- q )
assume F |- q ; ::_thesis: F \/ {p} |- q
then consider f being FinSequence of LTLB_WFF such that
A1: ( f . (len f) = q & 1 <= len f ) and
A2: for i being Nat st 1 <= i & i <= len f holds
prc f,F,i by Def30;
now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<=_len_f_holds_
prc_f,F_\/_{p},i
let i be Nat; ::_thesis: ( 1 <= i & i <= len f implies prc f,F \/ {p},i )
assume ( 1 <= i & i <= len f ) ; ::_thesis: prc f,F \/ {p},i
then prc f,F,i by A2;
then ( f . i in LTL_axioms or f . i in F or ex j, k being Nat st
( ( 1 <= j & j < i & 1 <= k & k < i & ( f /. j,f /. k MP_rule f /. i or f /. j,f /. k IND_rule f /. i ) ) or ex j being Nat st
( 1 <= j & j < i & f /. j NEX_rule f /. i ) ) ) by Def29;
then ( f . i in LTL_axioms or f . i in F \/ {p} or ex j, k being Nat st
( ( 1 <= j & j < i & 1 <= k & k < i & ( f /. j,f /. k MP_rule f /. i or f /. j,f /. k IND_rule f /. i ) ) or ex j being Nat st
( 1 <= j & j < i & f /. j NEX_rule f /. i ) ) ) by XBOOLE_0:def_3;
hence prc f,F \/ {p},i by Def29; ::_thesis: verum
end;
hence F \/ {p} |- q by A1, Def30; ::_thesis: verum
end;
theorem Th57: :: LTLAXIO1:57
for p, q being Element of LTLB_WFF
for F being Subset of LTLB_WFF st F \/ {p} |- q holds
F |- ('G' p) => q
proof
let p, q be Element of LTLB_WFF ; ::_thesis: for F being Subset of LTLB_WFF st F \/ {p} |- q holds
F |- ('G' p) => q
let F be Subset of LTLB_WFF; ::_thesis: ( F \/ {p} |- q implies F |- ('G' p) => q )
set G = F \/ {p};
assume F \/ {p} |- q ; ::_thesis: F |- ('G' p) => q
then consider f being FinSequence of LTLB_WFF such that
A1: f . (len f) = q and
A2: 1 <= len f and
A3: for i being Nat st 1 <= i & i <= len f holds
prc f,F \/ {p},i by Def30;
defpred S1[ Nat] means ( 1 <= $1 & $1 <= len f implies F |- ('G' p) => (f /. $1) );
A4: for i being Nat st ( for j being Nat st j < i holds
S1[j] ) holds
S1[i]
proof
let i be Nat; ::_thesis: ( ( for j being Nat st j < i holds
S1[j] ) implies S1[i] )
assume A5: for j being Nat st j < i holds
S1[j] ; ::_thesis: S1[i]
percases ( i = 0 or not i < 1 ) by NAT_1:14;
suppose i = 0 ; ::_thesis: S1[i]
hence S1[i] ; ::_thesis: verum
end;
suppose not i < 1 ; ::_thesis: S1[i]
assume that
A6: 1 <= i and
A7: i <= len f ; ::_thesis: F |- ('G' p) => (f /. i)
A8: prc f,F \/ {p},i by A3, A6, A7;
percases ( f . i in LTL_axioms or f . i in F \/ {p} or ex j, k being Nat st
( 1 <= j & j < i & 1 <= k & k < i & ( f /. j,f /. k MP_rule f /. i or f /. j,f /. k IND_rule f /. i ) ) or ex j being Nat st
( 1 <= j & j < i & f /. j NEX_rule f /. i ) ) by A8, Def29;
supposeA9: f . i in LTL_axioms ; ::_thesis: F |- ('G' p) => (f /. i)
set t = f /. i;
(f /. i) => (('G' p) => (f /. i)) in LTL_axioms by Th34;
then A10: F |- (f /. i) => (('G' p) => (f /. i)) by Th42;
f /. i in LTL_axioms by A6, A7, A9, Lm1;
then F |- f /. i by Th42;
hence F |- ('G' p) => (f /. i) by A10, Th43; ::_thesis: verum
end;
supposeA11: f . i in F \/ {p} ; ::_thesis: F |- ('G' p) => (f /. i)
percases ( f . i in F or f . i in {p} ) by A11, XBOOLE_0:def_3;
supposeA12: f . i in F ; ::_thesis: F |- ('G' p) => (f /. i)
set t = f /. i;
(f /. i) => (('G' p) => (f /. i)) in LTL_axioms by Th34;
then A13: F |- (f /. i) => (('G' p) => (f /. i)) by Th42;
f /. i in F by A6, A7, A12, Lm1;
then F |- f /. i by Th42;
hence F |- ('G' p) => (f /. i) by A13, Th43; ::_thesis: verum
end;
supposeA14: f . i in {p} ; ::_thesis: F |- ('G' p) => (f /. i)
('G' p) => (p '&&' ('X' ('G' p))) in LTL_axioms by Def17;
then A15: F |- ('G' p) => (p '&&' ('X' ('G' p))) by Th42;
f . i = p by A14, TARSKI:def_1;
then f /. i = p by A6, A7, Lm1;
hence F |- ('G' p) => (f /. i) by A15, Th46; ::_thesis: verum
end;
end;
end;
suppose ex j, k being Nat st
( 1 <= j & j < i & 1 <= k & k < i & ( f /. j,f /. k MP_rule f /. i or f /. j,f /. k IND_rule f /. i ) ) ; ::_thesis: F |- ('G' p) => (f /. i)
then consider j, k being Nat such that
A16: 1 <= j and
A17: j < i and
A18: 1 <= k and
A19: k < i and
A20: ( f /. j,f /. k MP_rule f /. i or f /. j,f /. k IND_rule f /. i ) ;
j <= len f by A7, A17, XXREAL_0:2;
then A21: F |- ('G' p) => (f /. j) by A5, A16, A17;
k <= len f by A7, A19, XXREAL_0:2;
then A22: F |- ('G' p) => (f /. k) by A5, A18, A19;
percases ( f /. j,f /. k MP_rule f /. i or f /. j,f /. k IND_rule f /. i ) by A20;
supposeA23: f /. j,f /. k MP_rule f /. i ; ::_thesis: F |- ('G' p) => (f /. i)
set t3 = (('G' p) => ((f /. j) => (f /. i))) => ((('G' p) => (f /. j)) => (('G' p) => (f /. i)));
(('G' p) => ((f /. j) => (f /. i))) => ((('G' p) => (f /. j)) => (('G' p) => (f /. i))) in LTL_axioms by Th35;
then A24: F |- (('G' p) => ((f /. j) => (f /. i))) => ((('G' p) => (f /. j)) => (('G' p) => (f /. i))) by Th42;
F |- ('G' p) => ((f /. j) => (f /. i)) by A22, A23, Def20;
then F |- (('G' p) => (f /. j)) => (('G' p) => (f /. i)) by A24, Th43;
hence F |- ('G' p) => (f /. i) by A21, Th43; ::_thesis: verum
end;
suppose f /. j,f /. k IND_rule f /. i ; ::_thesis: F |- ('G' p) => (f /. i)
then consider A, B being Element of LTLB_WFF such that
A25: f /. j = A => B and
A26: f /. k = A => ('X' A) and
A27: f /. i = A => ('G' B) by Def21;
set Gp = 'G' p;
set XGp = 'X' ('G' p);
set XA = 'X' A;
set Xq = 'X' q;
set GB = 'G' B;
('G' p) => (p '&&' ('X' ('G' p))) in LTL_axioms by Def17;
then F |- ('G' p) => (p '&&' ('X' ('G' p))) by Th42;
then A28: F |- ('G' p) => ('X' ('G' p)) by Th46;
F |- (('G' p) '&&' A) => ('X' A) by A22, A26, Th48;
then A29: F |- (('G' p) '&&' A) => (('X' ('G' p)) '&&' ('X' A)) by A28, Th50;
F |- (('X' ('G' p)) '&&' ('X' A)) => ('X' (('G' p) '&&' A)) by Th53;
then A30: F |- (('G' p) '&&' A) => ('X' (('G' p) '&&' A)) by A29, Th47;
F |- (('G' p) '&&' A) => B by A21, A25, Th48;
then F |- (('G' p) '&&' A) => ('G' B) by A30, Th45;
hence F |- ('G' p) => (f /. i) by A27, Th49; ::_thesis: verum
end;
end;
end;
supposeA31: ex j being Nat st
( 1 <= j & j < i & f /. j NEX_rule f /. i ) ; ::_thesis: F |- ('G' p) => (f /. i)
('G' p) => (p '&&' ('X' ('G' p))) in LTL_axioms by Def17;
then F |- ('G' p) => (p '&&' ('X' ('G' p))) by Th42;
then A32: F |- ('G' p) => ('X' ('G' p)) by Th46;
consider j being Nat, q, r being Element of LTLB_WFF such that
A33: 1 <= j and
A34: j < i and
A35: f /. j NEX_rule f /. i by A31;
('X' (('G' p) => (f /. j))) => (('X' ('G' p)) => ('X' (f /. j))) in LTL_axioms by Def17;
then A36: F |- ('X' (('G' p) => (f /. j))) => (('X' ('G' p)) => ('X' (f /. j))) by Th42;
j <= len f by A7, A34, XXREAL_0:2;
then F |- 'X' (('G' p) => (f /. j)) by A5, A33, A34, Th44;
then A37: F |- ('X' ('G' p)) => ('X' (f /. j)) by A36, Th43;
f /. i = 'X' (f /. j) by A35, Def19;
hence F |- ('G' p) => (f /. i) by A37, A32, Th47; ::_thesis: verum
end;
end;
end;
end;
end;
A38: for i being Nat holds S1[i] from NAT_1:sch_4(A4);
q = f /. (len f) by A1, A2, Lm1;
hence F |- ('G' p) => q by A2, A38; ::_thesis: verum
end;
theorem :: LTLAXIO1:58
for p, q being Element of LTLB_WFF
for F being Subset of LTLB_WFF st F |- p => q holds
F \/ {p} |- q
proof
let p, q be Element of LTLB_WFF ; ::_thesis: for F being Subset of LTLB_WFF st F |- p => q holds
F \/ {p} |- q
let F be Subset of LTLB_WFF; ::_thesis: ( F |- p => q implies F \/ {p} |- q )
p in {p} by TARSKI:def_1;
then p in F \/ {p} by XBOOLE_0:def_3;
then A1: F \/ {p} |- p by Th42;
assume F |- p => q ; ::_thesis: F \/ {p} |- q
then F \/ {p} |- p => q by Th56;
hence F \/ {p} |- q by A1, Th43; ::_thesis: verum
end;
theorem :: LTLAXIO1:59
for p, q being Element of LTLB_WFF
for F being Subset of LTLB_WFF st F |- ('G' p) => q holds
F \/ {p} |- q
proof
let p, q be Element of LTLB_WFF ; ::_thesis: for F being Subset of LTLB_WFF st F |- ('G' p) => q holds
F \/ {p} |- q
let F be Subset of LTLB_WFF; ::_thesis: ( F |- ('G' p) => q implies F \/ {p} |- q )
p in {p} by TARSKI:def_1;
then p in F \/ {p} by XBOOLE_0:def_3;
then F \/ {p} |- p by Th42;
then A1: F \/ {p} |- 'G' p by Th54;
assume F |- ('G' p) => q ; ::_thesis: F \/ {p} |- q
then F \/ {p} |- ('G' p) => q by Th56;
hence F \/ {p} |- q by A1, Th43; ::_thesis: verum
end;
theorem :: LTLAXIO1:60
for p, q being Element of LTLB_WFF
for F being Subset of LTLB_WFF holds F |- ('G' (p => q)) => (('G' p) => ('G' q))
proof
let p, q be Element of LTLB_WFF ; ::_thesis: for F being Subset of LTLB_WFF holds F |- ('G' (p => q)) => (('G' p) => ('G' q))
let F be Subset of LTLB_WFF; ::_thesis: F |- ('G' (p => q)) => (('G' p) => ('G' q))
reconsider G = (F \/ {(p => q)}) \/ {p} as Subset of LTLB_WFF ;
p => q in {(p => q)} by TARSKI:def_1;
then p => q in F \/ {(p => q)} by XBOOLE_0:def_3;
then G |- 'G' q by Th55;
then F \/ {(p => q)} |- ('G' p) => ('G' q) by Th57;
hence F |- ('G' (p => q)) => (('G' p) => ('G' q)) by Th57; ::_thesis: verum
end;