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